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 list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://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
