PS: What about a function that supports backward-chaining with Z
theorems, something like z_bc_tac and z_bc_thm_tac? I suppose this
could be quite useful too. Is there anything more that needs to be
done other than rewriting the Z universal quantifier into a HOL one,
and using the HOL backwar
Hi Rob,
Many thanks for the reply and clarification.
All below makes sense. I can see how effectively excluding terms such as
|- n = 1 /\ n = {1}
would in any case impose a big overhead on run-time, requiring some
dynamic type-checking when rules are applied, etc. To exclude such cases
nonet
Frank,
On 7 Apr 2009, at 14:39, Frank Zeyda wrote:
Dear Roger,
Many thanks for the reply.
The additional feature of better error handling is easily supported
with another line of code handling possible exceptions.
The idea behind the caller parameter in many of these internal
funct
Dear Roger,
Many thanks for the reply.
> It looks like apply_matches_rule will tolerate universal
> quantifiers on the conclusions better than yours, so it
> will just work more often than yours.
> It also has a "caller" parameter to make error reports
> more intelligible, and is complicated by
On Thursday 02 April 2009 18:30:48 Frank Zeyda wrote:
>My question is whether
>apply_matches_rule behaves differently (better, more powerful?) than the
>version above.
I'm not the right person to answer this, but since no-one else
has I'll say what I can.
It looks like apply_matches_rule will to
Dear ProofPower Users,
I'm currently finalising an implementation of the (hypothetical) tactic
language ArcAngel in ProofPower and hit upon the following. In some
cases I need to instantiate free variables in a theorem of the form
ASS |- P according to some sub expression of P matching some ter
