*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] schematic variables and assumption*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 16 May 2012 14:32:06 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1205161843470.24797@macbroy21.informatik.tu-muenchen.de>*References*: <4FB22629.4000202@in.tum.de> <4FB23EA3.3000305@abo.fi> <CAAPnxw2xsBL8Q7OFKjU0wNrZuX4WFSDoQ=H1RQJ1DWBsNox8hg@mail.gmail.com> <alpine.LNX.2.00.1205161843470.24797@macbroy21.informatik.tu-muenchen.de>*Sender*: alfio.martini at gmail.com

Dear Makarius, The corresponding Isar proof I had done, which follows the procedural one below was this one: lemma assumes p: "(¬ (∀ x . P x))" shows "(∃ x . ¬ P x)" proof (rule ccontr) assume h1: "¬ (∃x. ¬ P x)" have "∀x. P x" proof (rule allI) fix x0 show "P x0" proof (rule ccontr) assume "¬ P x0" from this have "∃ x. ¬P x" by (rule exI) with h1 show False by (rule notE) qed qed with p show False by (rule notE) qed But since I am still learning Isar, it does not look as elegant as yours! best! On Wed, May 16, 2012 at 1:55 PM, Makarius <makarius at sketis.net> wrote: > On Tue, 15 May 2012, Alfio Martini wrote: > > If I am not wrong, this is a classical conjecture. Here goes a >> possible proof: >> >> lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)" >> apply (rule ccontr) >> apply (erule notE) >> apply (rule allI) >> apply (rule ccontr) >> apply (erule notE) >> apply (rule exI) >> apply (assumption) >> done >> > > We've been an the same point just yesterday in our Isabelle tutorial at > Paris Sud point, but nobody could give me the proof on the spot. See > http://www.lri.fr/~wenzel/**Isabelle_Orsay_2012/**Calculation.thy<http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/Calculation.thy>Exercise (2) about the Drinker's principle. > > The idea was to play with proof structure and automated tools to bridge > the gaps, and show the possibilities and limitations of this approach. The > question of the assignment "Do you believe the proof?" (a skeleton > involving 3 "blast" steps) was answered negatively by everybody. Afterwards > I've made a fully explicit Isar proof, and managed to convince at least > half of the audience that this is correct classical nonsense. > > To complete my own exercise from yesterday, here is now de_Morgan as above > (using the more generic rule classical instead of ccontr) together with the > explicit version of the Drinker's principle: > > lemma de_Morgan: > assumes "¬ (∀x. P x)" > shows "∃x. ¬ P x" > proof (rule classical) > assume "¬ (∃x. ¬ P x)" > have "∀x. P x" > proof > fix x show "P x" > proof (rule classical) > assume "¬ P x" > then have "∃x. ¬ P x" .. > with `¬ (∃x. ¬ P x)` show ?thesis .. > qed > qed > with `¬ (∀x. P x)` show ?thesis .. > qed > > theorem "∃a. drunk a ⟶ (∀x. drunk x)" > proof cases > assume "∀x. drunk x" > fix a > have "drunk a ⟶ (∀x. drunk x)" > using `∀x. drunk x` .. > then show ?thesis .. > next > assume "¬ (∀x. drunk x)" > then have "∃a. ¬ drunk a" by (rule de_Morgan) > then obtain a where "¬ drunk a" .. > have "drunk a ⟶ (∀x. drunk x)" > proof > assume "drunk a" > with `¬ drunk a` show "∀x. drunk x" by contradiction > qed > then show ?thesis .. > qed > > > For demonstration purposes in such Pure examples, I usually refer to > previous facts literally with `prop`, to avoid the Spaghetti tendency of > named references like *, **, *** or 1, 2, 3 etc. > > > Makarius -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**References**:**[isabelle] jedit***From:*Tobias Nipkow

**[isabelle] schematic variables and assumption***From:*Viorel Preoteasa

**Re: [isabelle] schematic variables and assumption***From:*Alfio Martini

**Re: [isabelle] schematic variables and assumption***From:*Makarius

- Previous by Date: Re: [isabelle] schematic variables and assumption
- Next by Date: Re: [isabelle] jedit
- Previous by Thread: Re: [isabelle] schematic variables and assumption
- Next by Thread: Re: [isabelle] jedit
- Cl-isabelle-users May 2012 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