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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to