*To*: Edward Schwartz <edmcman at cmu.edu>*Subject*: Re: [isabelle] Eliminating two quantifiers in structural proof*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sun, 16 Sep 2012 08:04:33 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*References*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*Sender*: alfio.martini at gmail.com

Hi Edward, I am not sure if this is what you what, but in Isar is fairly natural to do such proofs. I use it to teach natural deduction to students. Here goes three proofs of this conjecture: theorem th11a: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule spec) thus "P a b" by (rule spec) qed theorem th11b: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule allE) thus "P a b" by (rule allE) qed theorem th11c: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule spec[where x =a]) from this show "P a b" by (rule spec[where x=b]) qed I assume you hardly have to use the qualifieres (e(limination), d(estruction)) when working in Isar. I use this style only when I am playing with linear scripts. All the Best! On Sat, Sep 15, 2012 at 5:15 PM, Edward Schwartz <edmcman at cmu.edu> wrote: > Hi, > > I am new to Isabelle, and am stuck on a fairly trivial part of my > proof. I have an assumption "\forall x y. P x y". I'd simply like to > show (P a b) for two terms I have (a and b). Surprisingly, I am > having trouble doing this in a structural way. > > With one quantified variable, there is no problem: > > lemma single_proof : "(\<forall>x. P x) \<Longrightarrow> P a" > proof (erule allE) > fix c > assume A: "P c" > from A show "P c" by assumption > qed > > My understanding of what is happening is that allE removes the > quantifier, and so we really just prove /\ c. P c ==> P c. It seems > like a better proof would be of /\ c. P ?c ==> P c. Is there any way > to do this instead? > > lemma double : "(\<forall>x y. P x y) \<Longrightarrow> P a b" > apply (erule allE, erule allE) > apply assumption > done > > Here is a way to do the proof with tactics. Unfortunately, in my > larger proof, the erule commands do not find the correct assumption, > and so I must specify P manually, which is *very* ugly. > > lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b" > proof (erule allE) > fix c > assume "\<forall>y. P c y" > have "P c b" > proof (erule allE) (* error: proof command failed *) > > Finally, I try to do a structural proof, eliminating one quantifier at > a time, and fail. I've tried many variations, but can't seem to > understand how to do this. If someone could show how to finish this > proof, and explain why it works, I would greatly appreciate it. > > Overall, Isabelle/HOL seems to make it very difficult to instantiate > free variables in foralls. In Coq, this is very easy, since \forall > x. P x is actually a function that accepts a variable v and returns > proof that (P v). What am I missing? > > Thanks, > > Ed > > -- 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

**Follow-Ups**:**Re: [isabelle] Eliminating two quantifiers in structural proof***From:*Alfio Martini

**Re: [isabelle] Eliminating two quantifiers in structural proof***From:*Makarius

**References**:**[isabelle] Eliminating two quantifiers in structural proof***From:*Edward Schwartz

- Previous by Date: Re: [isabelle] Eliminating two quantifiers in structural proof
- Next by Date: Re: [isabelle] Eliminating two quantifiers in structural proof
- Previous by Thread: Re: [isabelle] Eliminating two quantifiers in structural proof
- Next by Thread: Re: [isabelle] Eliminating two quantifiers in structural proof
- Cl-isabelle-users September 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