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 term T. For this I use term_match together with asm_inst_term_type and asm_inst_term_rule. I implemented the following function to encapsulate this functionality.

fun asm_match_inst_rule
                (term : TERM) (extract : TERM -> TERM) (thm : THM) =
        let val match_against = (extract (concl thm));
        val (tym, tmm) = (term_match term match_against) in
                (asm_inst_term_rule tmm
                        (asm_inst_type_rule tym thm))

This function has a very similar signature to apply_matches_rule in imp007.doc, the latter is however not expose. My question is whether apply_matches_rule behaves differently (better, more powerful?) than the version above. Were there any reasons for not exposing it?

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. 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. Any experience contrary to this would be great to know about.

Best Regards,

 Dr Dipl.-Inform. Frank Zeyda
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Phone: 0044-(0)1904-433244

Proofpower mailing list

Reply via email to