Oh great!
These really do help a lot!
Many thanks to both Ramana and Petros.
Regards,
Robert
On 21 May 2015 at 14:22, Petros Papapanagiotou <[email protected]> wrote:
> Hello Robert,
>
> 1) There may be better ways of doing this, but I often use PAT_CONV or
> PATH_CONV as such:
>
> ASM (CONV_TAC o PAT_CONV pat o REWRITE_CONV) [];;
>
> where 'pat' is a lambda-abstraction with the pattern that you want to
> match in your goal. See
> http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/PAT_CONV.html for more
> details.
>
> PATH_CONV can sometimes be more convenient and precise.
>
> There are also other such conversions as Ramana suggested.
>
>
> 2) You can use something like:
> POP_ASSUM (ASSUME_TAC o REWRITE_RULE [...])
>
> You can change ASSUME_TAC if you want to do something more complicated
> with the result.
>
> Hope this helps.
>
> Regards,
> Petros
>
>
>
>
> On 21/05/2015 12:39, Robert White 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
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
> --
> Petros Papapanagiotou, Ph.D.
> CISA, School of Informatics
> The University of Edinburgh
>
> Email: [email protected]
>
> ---
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
