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 not using the
> asm_inst_ things (i.e. by incorporating that functionality).
I had a closer look at apply_matches_rule and the main difference, as
you explained, is that it will allow the conclusion to be universally
quantified; it eliminates such a quantifier while avoiding clashes with
the free variables of the term prior to performing the matching. Rather
than using asm_inst_term_rule it employs inst_term_rule and therefore
requires a bit more effort to introduce (and eliminate) assumptions into
(and from) the conclusion. As you mentioned, it also gives more
informative error messages mentioning the area of the caller.
Since I don't need this additional feature of removing outer universal
quantifiers in the conclusion of the theorem, I think there is no
genuine advantage in using it in the context of my application. The
additional feature of better error handling is easily supported with
another line of code handling possible exceptions. Maybe
apply_matches_rule could be a nice function to have in the general
interface, what about exposing it?
>> A second case is when y occurs free in both thm and term,
>> is not substituted but nonetheless introduced through the substitution.
>> I presume this is okay
>> as long as the types of y are identical in thm and term.
>
> Its still OK if the types are not the same, they will be
> logically distinct variables and its a confusing situation
> you shold seek to avoid.
This sounds a little bit curious, is there a document that explains more
about this situation? So although the variables have the same name they
are actually treated as logical distinct by the fact that they have
different types? So instantiation would have be sensitive to variable
types (not just names) and might result in one variables n to be
substitution, while another n is left unaffected e.g. if it has a
different type?
For example, assume we have a theorem thm
n = 1 |- n = {1}
Then (asm_inst_term_rule [(2, n)] thm) would yield
2 = 1 |- n = {1} ?
Thanks for pointing this out, it clarified one or two behaviours of
ProofPower for me which I could not explain before.
> I think the main problem you will have is in matching against terms
> containing bound variables.
I haven't given considerations to this, but as far as I can see such a
situation may not arise in the particular application. Thanks for
pointing this out!
Cheers once more,
Frank
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 backward-chaining tactics?
PPS: A final comment. To implement some custom error handling I noticed
that there was no functions that could be used to infer the id of an
error message (of type MESSAGE). Since the MESSAGE datatype is not
exposed, we cannot take the message apart; the only solution seems to be
to dissect the string of the error message. If I'm overlooking something
please let me know, otherwise it would be beneficial to have some
function get_id in the general interface of BasicError to extract the id
of an error message ;-).
Roger Bishop Jones wrote:
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 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 not using the
asm_inst_ things (i.e. by incorporating that functionality).
Were there any reasons for not exposing it?
The caller parameter would be one.
A second problem: assume that the sub-expression of thm I'm matching
against contains some free variable y (of variable type), and that y
will be associated with some sub-term t according to the matching.
Further, let t also have y free in it. Could there be a problem in this
case? Since y will be substituted anywhere in thm, I would think there
is no risks with substituting y for a term that contains y.
I don't see a problem, but if there was one it would fail
so you don't risk making an unsound inference.
A second case is when y occurs free in both thm and term,
is not substituted but nonetheless introduced through the substitution.
I presume this is okay
as long as the types of y are identical in thm and term.
Its still OK if the types are not the same, they will be
logically distinct variables and its a confusing situation
you shold seek to avoid.
I think the main problem you will have is in matching
against terms containing bound variables.
Roger Jones
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
