Another option is to abbreviate the parts of the term that you don't want
to be rewritten. See Q.PAT_ABBREV_TAC for example.
On 21 May 2015 at 13:12, Ramana Kumar <ram...@member.fsf.org> wrote:
> 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
