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))
end;
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,
Frank
--
Dr Dipl.-Inform. Frank Zeyda
Research Associate
High Integrity Systems Engineering Group
Department of Computer Science
University of York (UK)
Email: [email protected]
Phone: 0044-(0)1904-433244
WWW: http://www-users.cs.york.ac.uk/~zeyda/
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
