*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Eliminating two quantifiers in structural proof*From*: Edward Schwartz <edmcman at cmu.edu>*Date*: Sat, 15 Sep 2012 16:15:25 -0400*Sender*: edmcman at gmail.com

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

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

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

- Previous by Date: [isabelle] eduTPS Sept.22 deadline extension
- Next by Date: [isabelle] Code generation for sorts from locales
- Previous by Thread: [isabelle] eduTPS Sept.22 deadline extension
- 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