*To*: René Neumann <rene.neumann at in.tum.de>*Subject*: Re: [isabelle] Replacing COMP*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 30 Jul 2013 08:38:20 +0200*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <51F6D5C5.3020703@in.tum.de>*References*: <51F6B685.30203@in.tum.de> <alpine.LNX.2.00.1307292235390.11573@macbroy21.informatik.tu-muenchen.de> <51F6D5C5.3020703@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Dear René,

> 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?

lemma lift_foo: assumes "asm --> concl" shows "asm --> concl'" proof ... qed lemmas foo1_impl = foo1[THEN lift_foo]

lift_foo': "[| concl; asm |] ==> concl" If you now do rule composition with THEN, you get "[| asm; asm |] ==> concl'" instead of "[| asm ==> asm; asm |] ==> concl'". I don't know if that's better. If you can prove "concl ==> concl'" without the assumption asm, then that works perfectly.

context assumes asm begin lemma lift_foo: "concl ==> concl'" proof - ... qed lemma foo1: "concl" lemmas foo1_impl = foo1[THEN lift_foo] end

lemma remove_trivial_assumption: "((PROP A ==> PROP A) ==> PROP B) == PROP B" by(rule equal_intr_rule) lemmas foo1_impl = foo1[THEN lift_foo, unfolded remove_trivial_assumption] lemma remove_double_assumption: "(PROP A ==> PROP A ==> PROP B) == (PROP A ==> PROP B)" by(rule equal_intr_rule) lemmas foo1_impl = foo[THEN lift_foo', unfolded remove_double_assumption] Hope this helps, Andreas On 29/07/13 22:51, René Neumann wrote:

Am 29.07.2013 22:39, schrieb Makarius:On Mon, 29 Jul 2013, René Neumann wrote:Now I'm porting to Isabelle2013, where COMP has been removed.In such situations, the NEWS file is the first place to look. It says:I had a look there. That's how I noted it was gone ...* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, use regular rule composition via "OF" / "THEN",Can't make it work (that's why I asked here on the list).or explicit proof structure instead.Don't want it that way.Note that Isabelle/ML provides a variety of operators like COMP, INCR_COMP, COMP_INCR, which need to be applied with some care where this is really required.I don't know Isabelle/ML in a way to make it work.Unfortunately, THEN is no sufficient replacement as the resulting foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.The usual game is to write statements and proofs in a way that one does not have to disobey the nice structure of rules provided by Larry Paulson in 1989. There are many ways to do that, but from the given example it is hard to guess what is right.Could you, nevertheless, provide some pointers here, please? Because currently, I'm unsure how I'd have to refine my example to make my intention more visible. - René

**Follow-Ups**:**Re: [isabelle] Replacing COMP***From:*Makarius

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

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

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

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

- Previous by Date: Re: [isabelle] Replacing COMP
- Next by Date: [isabelle] Automatic case splitting for Isar proofs with polymorphic rule
- 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