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 )
On Fri, Nov 16, 2012 at 7:11 PM, Vincent Aravantinos <
[email protected]> wrote:
> I guess it depends a lot on the context, but both the following can be
> useful I think:
>
> ASSUM_LIST (fn ths => ASSUME_TAC (REWRITE_CONV (HD::map
> (REWRITE_RULE[Abbrev_def]) ths) ``HD (l:num list)``))
>
> or:
>
> IMP_RES_THEN (ASSUME_TAC o REWRITE_RULE[HD]) (METIS_PROVE[] ``Abbrev(l=y)
> ==> (HD l = HD y)``)
>
> They are pretty verbose but their use could probably be automatized if you
> use this kind of reasoning a lot.
> For instance, in the second case, the theorem ``!f. Abbrev(x=y) ==> (f x =
> f y)`` can be stored independently.
>
> HTH,
> V.
>
> Le 16/11/2012 12:53, Ramana Kumar a écrit :
>
> In the middle of an interactive proof with lots of abbreviations to
> prevent unmanageably large terms, I might at some point want to prove
> something by expanding all the abbreviations.
>
> For example, `HD ls` might be obvious when you unabbreviate ls (and all
> abbreviations inside it), since it is ultimately a known CONS. It may,
> however, be a CONS of a large term.
>
> The only way I know how to do this is to write the term out by hand and
> prove it as a subgoal:
> `HD ls = blah blah blah blah blah blah blah` by (unabbrev_all_tac >> rw[])
>
> How can I get that without manually typing out all the blahs?
>
>
> ------------------------------------------------------------------------------
> 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
> [email protected]https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> --
> Vincent Aravantinos
> Postdoctoral Fellow, Concordia University, Hardware Verification
> Grouphttp://users.encs.concordia.ca/~vincent
>
>
>
> ------------------------------------------------------------------------------
> 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
