*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Eliminating two quantifiers in structural proof*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 16 Sep 2012 00:35:41 +0200*In-reply-to*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*References*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:15.0) Gecko/20120907 Thunderbird/15.0.1

Try to use the meta-quantifier !! instead of \<forall> whenever you can, and in your examples you can. Now if you have an assumption A: "!!x y. P x y" you can instantiate the quantifiers very easily: just write A[of "t1" "t2"]. Then it is hardly more verbose than Coq. Note that the instantiation order is not the order of quantification but the order in which x and y occur in P (from left to right). In fact, if you inspect A in the proof (eg via command thm) you see that the !! have disappeared and x/y became ?x/?y. Unfortunately the "of" operator only works for !!, and !! can only occur at the "outermost" level, ie not inside HOL formulas. But in many situations that suffices. Tobias Am 15/09/2012 22:15, schrieb Edward Schwartz: > 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 >

**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: [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