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

Reply via email to