*To*: René Neumann <rene.neumann at in.tum.de>*Subject*: Re: [isabelle] Replacing COMP*From*: Makarius <makarius at sketis.net>*Date*: Wed, 31 Jul 2013 14:15:04 +0200 (CEST)*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <51F75F5C.1060105@inf.ethz.ch>*References*: <51F6B685.30203@in.tum.de> <alpine.LNX.2.00.1307292235390.11573@macbroy21.informatik.tu-muenchen.de> <51F6D5C5.3020703@in.tum.de> <51F75F5C.1060105@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 30 Jul 2013, Andreas Lochbihler wrote:

You will have to restructure your lemmas or proofs unless you want to defineyour own COMP attribute, there's no way to do it as before with THEN/OF. Hereare a few ideas.lemma lift_foo: assumes "asm ==> concl" shows "asm ==> concl'" proof - ... qed lemmas foo1_impl = foo1[COMP lift_foo] lemmas foo2_impl = foo2[COMP lift_foo] lemmas foo3_impl = foo3[COMP lift_foo] ...I suspect that foo1 has the form "asm ==> concl", right?1. The clean way: Use --> instead of ==> for those parts that you want tounify in one step, i.e.,

2. Note that "asm" as a premise in the assumes is redundant in lift_foo. Thefollowing lemma is equivalent:3. Hide the assumption asm in a local context to hide the asm in rulecompositions. Instead of an unnamed context, you might also want to considera locale which you can reopen later on.4. The hack: You can use unfold with an appropriate lemma to get rid of the"asm ==> asm" premise as follows:

thm lift_foo [unfolded atomize_all atomize_imp] Can you explain the application behind all this? Makarius

**Follow-Ups**:**Re: [isabelle] Replacing COMP***From:*René Neumann

**References**:**[isabelle] Replacing COMP***From:*René Neumann

**Re: [isabelle] Replacing COMP***From:*Makarius

**Re: [isabelle] Replacing COMP***From:*René Neumann

**Re: [isabelle] Replacing COMP***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule
- Next by Date: Re: [isabelle] Replacing COMP
- Previous by Thread: Re: [isabelle] Replacing COMP
- Next by Thread: Re: [isabelle] Replacing COMP
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list