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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
