*To*: C. Diekmann <diekmann at in.tum.de>*Subject*: Re: [isabelle] Lemma [OF ..] unification with \<And> parts*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 14 May 2013 14:48:34 +0100*Cc*: "isabelle-users at cl.cam.ac.uk Users" <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <CAGbqCMzBcGWS7mOBhiDupfcMrdz=Q-1LGn54WWPvdR6v4=x9Aw@mail.gmail.com>*References*: <CAGbqCMxCtfKVeXtwbiamL-wVsj5+H0ka0Vyh=o0QzuD_Y3y5Gg@mail.gmail.com> <alpine.LNX.2.00.1305131611090.12255@macbroy21.informatik.tu-muenchen.de> <CAGbqCMzBcGWS7mOBhiDupfcMrdz=Q-1LGn54WWPvdR6v4=x9Aw@mail.gmail.com>

Another possibility might be to structure your proof something like this: have "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')" sorry hence "D" Larry On 14 May 2013, at 13:40, C. Diekmann <diekmann at in.tum.de> wrote: > 2013/5/13 Makarius <makarius at sketis.net>: >> On Sat, 11 May 2013, C. Diekmann wrote: >> >>> given these two lemmata >>> lemma l1: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E') ==> D" >>> sorry >>> >>> lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')" >>> sorry >>> >>> writing >>> thm l1[OF l2] >>> I expected to get D. However, I get something very strange. >> >> >> As already pointed out by Larry, rule composition via "OF" (or "THEN" with >> different argument order), or "rule" as a proof method works exactly like >> that. You should study relevant Isabelle documentation until you expect the >> correct outcome and don't consider it to be strange. This is about >> higher-order natural deduction in Isabelle/Pure. Applications should not >> step out of that comfortable environment without good reason (which means >> you need to understand first what is its very purpose). > > Thank you all for your answers. Today I learned that I want to use ! > (∀), the ordinary FOL all quantifier. >

**References**:**[isabelle] Lemma [OF ..] unification with \<And> parts***From:*C. Diekmann

**Re: [isabelle] Lemma [OF ..] unification with \<And> parts***From:*Makarius

**Re: [isabelle] Lemma [OF ..] unification with \<And> parts***From:*C. Diekmann

- Previous by Date: Re: [isabelle] Lemma [OF ..] unification with \<And> parts
- Next by Date: [isabelle] type_synonym and fixed type arguments in a locale?
- Previous by Thread: Re: [isabelle] Lemma [OF ..] unification with \<And> parts
- Next by Thread: Re: [isabelle] goals_limit in error-output
- Cl-isabelle-users May 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