*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Eliminating two quantifiers in structural proof*From*: Edward Schwartz <edmcman at cmu.edu>*Date*: Sat, 15 Sep 2012 17:51:10 -0400*In-reply-to*: <17766_1347740206_q8FKGjuS027503_CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*References*: <17766_1347740206_q8FKGjuS027503_CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com>*Sender*: edmcman at gmail.com

Hi all, I made a few breakthroughs in understand Isar: 1. "proof" is not the same thing as "proof -". In particular, proof looks for a classical logic introduction rule that matches the current goal. It will not work with goals like "A ==> B" as I had. "proof -" works on these. This is really confusing, and if any Isabelle devs read this, please consider changing it! 2. Here are the modified proofs of my examples: The first example can be rewritten where the assumption is more general: lemma single_proof : "(\<forall>x. P x) \<Longrightarrow> P a" proof - assume A: "\<forall>x. P x" fix c from A show "P c" .. qed And here is the two variable example: lemma double_proof : "(\<forall>x y. P x y) \<Longrightarrow> P a b" proof - assume H: "\<forall>x y. P x y" fix a b from H have "\<forall>y. P a y" .. thus "P a b" .. qed This is a big improvement over my previous attempts, but still seems overly verbose for just instantiating bound variables. Is there a quicker way that works on multiple bound variables at the same time? Thanks again, Ed On Sat, Sep 15, 2012 at 4: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 >

- Previous by Date: [isabelle] Code generation for sorts from locales
- 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: [isabelle] Code generation for sorts from locales
- 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