*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:15:10 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com>*References*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com> <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com>*Sender*: alfio.martini at gmail.com

Forgot this one: theorem th11d: "∀x. ∀y. P x y ==> P a b" proof - assume "∀x. ∀y. P x y" from this have "∀y. P a y" by (rule spec[where x =a]) from this show "P a b" by (rule spec[where x=b]) qed On Sun, Sep 16, 2012 at 8:04 AM, Alfio Martini <alfio.martini at acm.org>wrote: > 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 > > -- 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**:

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

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

- Previous by Date: Re: [isabelle] Eliminating two quantifiers in structural proof
- Next by Date: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- 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