Hi Mario,
I believe, there is nothing bad about using inline functions (i.e. a
lambda) per se. If I understood correctly, you are currently using the
following from
`some goal` by (
tactic_goal
) >>
POP_ASSM (fn thm => REWRITE_TAC[thm])
A slightly more elegant way might be (it's all a matter of opinion :-))
Q.SUBGOAL_THEN `some_goal` (fn thm => REWRITE_TAC[thm]) >- (
tactic_goal
)
However, this keeps the inline function. I don't know of a SUBST1_TAC
like function. However, it is easy to define. You could use REWR_CONV
(or it's higher order corresponding function) and combine it with
tacticals. You would end up with something like
fun REWRITE1_TAC thm = CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV thm)))
Depending on your circumstances, ONCE_ASM_REWRITE_TAC or similar
existing tactics might do the trick for you as well.
Cheers
Thomas Tuerk
On 25.09.2017 20:03, Mario Castelán Castro 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.
>
>
>
> ------------------------------------------------------------------------------
> 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
------------------------------------------------------------------------------
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
