In both cases it sounds like the problem is that rewriting is rewriting too
much - you only want to rewrite a particular occurrence of a term.
You might try using ONCE_REWRITE_RULE or Once.
If that doesn't work, you can be much more specific about where you apply
rewriting by using the rewriting conversion directly and other
conversion-builders above it to specify a particular position in the term.
For example, in your situation (1), if D looks like !a b c. D0 ==> (D1 /\
D2), I would do:
CONV_TAC(STRIP_QUANT_CONV(RAND_CONV(LAND_CONV(REWRITE_CONV[UNDISCH_ALL
rewrite_th])))). The various _CONV functions help me locate the specific
part of the term where I want to apply REWRITE_CONV. I used UNDISCH_ALL on
the theorem that actually does the rewrite, because you said the
assumptions are necessary, so I'm assuming rewrite_th looks like |- A ==> B
==> C ==> D1 = D1'.
On 21 May 2015 at 12:39, Robert White <ai.robert.wangsh...@gmail.com> wrote:
> Dear all,
>
> Happy proving :)
>
> 1) I wonder how I suppose to tackle situation like this
> A, B, C |- D.
> and D is a complicated term with D1 and D2 somewhere in it.
>
> D1 can be rewrite to D1' under assumption of A,B,C while if I simply use
> the ASM_REWRITE_RULE then I will do some other changes in D which I don't
> want to.
>
> 2) Another related question: is there any way I can deal with situation
> like
> A, B, C |- D but I want to replace C by C' where C = C'
> one way in my mind is to get
> A, B |- C ==> D then use rewrite to get C' ==> D as concl but, that may
> lead to the change in D as well.
>
> It would be very nice if you can give me some advice.
>
> Thanks very much!
>
> --
>
> Regards,
> Robert
>
>
> ------------------------------------------------------------------------------
> One dashboard for servers and applications across Physical-Virtual-Cloud
> Widest out-of-the-box monitoring support with 50+ applications
> Performance metrics, stats and reports that give you Actionable Insights
> Deep dive visibility with transaction tracing using APM Insight.
> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
