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
