Thanks Michael.
But it doesn't look easy to just remove some of the abbreviations
selectively (the way the Abbr`foo` theorem works if I'm just using a
rewrite tactic in a subgoal).
Actually I guess that just means defining deabbr in a more selective way...
I will look into this next time I feel I want this kind of tactic. It's
difficult to know the best way to attack a massively unwieldy goal. The
approaches include: use tactics like this, be more declarative and just
create a lot of truth using subgoals ignoring the current goal until you
reach it, use ever smarter abbreviations, and change stuff further upstream
so the unwieldy goal never comes up in the first place.
On Mon, Nov 19, 2012 at 12:01 AM, Michael Norrish <
[email protected]> wrote:
> 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
>
>
>
> ------------------------------------------------------------------------------
> 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
>
>
------------------------------------------------------------------------------
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
