On 19/11/12 03:46, Ramana Kumar wrote: > Thanks for those. > I just used > IMP_RES_THEN (assume_tac o SIMP_RULE(srw_ss())[]) > (METIS_PROVE[]``Abbrev(x=y)==>(x.out = y.out)``) > which worked great for getting an equation for the x.out of every x, but I'm > not > sure if I can get it for just one of them...
> There's probably a way along these lines.
> But perhaps there is a simpler way?
> The effect I'd like is:
> `foo.out = X` by (
> rw[Abbr`foo`] >>
> now jump out of this subgoal and give me an assumption saying foo.out equals
> the lhs of the subgoal )
Ignoring abbreviations, you could use
fun simpterm q =
ASSUM_LIST (fn ths => Q_TAC (ASSUME_TAC o SIMP_CONV (srw_ss()) ths) q)
This simplifies the term corresponding to assumption q and gives you back the
resulting assumption. You could write a simp_then function version easily,
replacing ASSUME_TAC with the ttac parameter.
Handling the abbreviations requires a bit of work to be done on the ths first,
perhaps
local
val deabbr = CONV_RULE (TRY_CONV (REWR_CONV markerTheory.Abbrev_def))
in
fun abbsimpterm q =
ASSUM_LIST
(fn ths => Q_TAC (ASSUME_TAC o SIMP_CONV (srw_ss()) (map deabbr ths)) q)
end
which will expand all abbreviations.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
