To prevent "explicit" lambda expressions in this case, what I've learnt
from Joe Hurd is the following simple helper ML function:
fun wrap a = [a];
then your "POP_ASSUM (fn thm => REWRITE_TAC [thm])" becomes "POP_ASSUM
(REWRITE_TAC o wrap)".
Hope this helps,
Chun
On 25 September 2017 at 20:03, Mario Castelán Castro <marioxcc...@yandex.com
> wrote:
> 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
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
