*To*: "isabelle-users at cl.cam.ac.uk Users" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Lemma [OF ..] unification with \<And> parts*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Sat, 11 May 2013 18:12:37 +0200*Sender*: c.diekmann at googlemail.com

Hello, 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. I get (\<And>E E'. E' \<subseteq> E ==> ?P E ==> ?E'1 E E' \<subseteq> ?E1 E E') ==> (\<And>E E'. E' ⊆ E ==> ?P E ==> ?P1 E E' (?E1 E E')) ==> ?D [%E E'. ?P1 E E' (?E'1 E E') =?= %E. ?P] What am I doing wrong, what is happening? In lemma l1, I conclude D from some (anti-monotonicity) of P. In lemma l2 I show this anti-monotonicity. Is there a better way to express this? Symbols: \<And> corresponds to /\, or !! written in ASCII. Regards Cornelius

**Follow-Ups**:**Re: [isabelle] Lemma [OF ..] unification with \<And> parts***From:*Tobias Nipkow

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

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

- Previous by Date: [isabelle] (CFP) Certified Programs and Proofs 2013 - Second Call for Papers
- Next by Date: Re: [isabelle] Lemma [OF ..] unification with \<And> parts
- Previous by Thread: [isabelle] (CFP) Certified Programs and Proofs 2013 - Second Call for Papers
- Next by Thread: Re: [isabelle] Lemma [OF ..] unification with \<And> parts
- 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