Hello. Suppose that in a tactic-based proof I have just proved with “by” a lemma of the form “P = Q”, where “P” can be matched against a proper subterm of the goal. I want to use this lemma to rewrite the respective subterm of the goal. What is the preferred approach to do this?
The obvious approach is “POP_ASSUM (fn thm => REWRITE_TAC [thm])” (or another rewriter in place of “REWRITE_TAC”). But I feel that embedding a lambda expression in a proof is an inelegant approach. I am aware that “ASM_REWRITE_TAC” or “FULL_SIMP_TAC” can be used in some of these cases, but sometimes there are assumptions that would lead to an undesired rewriting. Is there something like “SUBST1_TAC” that does matching? Thanks. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
