*To*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Subject*: Re: [isabelle] Uniqueness quantification*From*: John Munroe <munddr at gmail.com>*Date*: Thu, 26 Jul 2012 13:39:17 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5010AABA.4080701@nicta.com.au>*References*: <CAP0k5J7YFMS9gRKpj_LQdW16vLp662TKFP6LTx7FHRXE19W_vA@mail.gmail.com> <5010AABA.4080701@nicta.com.au>

Hi Thomas, Thanks so much for your detailed explanation. I've tried your suggestion and it works! However, I've tried extending the model to 5 predicates: axiomatization p1 :: "nat => bool" and p2 :: "nat => bool" and p3 :: "nat => bool" and p4 :: "nat => bool" and p5 :: "nat => bool" where ax1: "p1 x == ~p2 x & ~p3 x & ~p4 x & ~p5 x" and ax2: "p2 x == ~p1 x & ~p3 x & ~p4 x & ~p5 x" and ax3: "p3 x == ~p1 x & ~p2 x & ~p4 x & ~p5 x" and ax4: "p4 x == ~p1 x & ~p2 x & ~p3 x & ~p5 x" and ax5: "p5 x == ~p1 x & ~p2 x & ~p3 x & ~p4 x" and metis loops at: lemma lem: "EX! p:{p1,p2,p3,p4,p5}. p q" using ax1[symmetric] ax2[symmetric] ax3[symmetric] ax4[symmetric] ax5[symmetric] apply simp apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib) apply metis Do you know why it's fine for a smaller number of predicates, e.g., 3, but not when there are 5? Do you happen to know how to simplify the goal further? Thanks a lot for your time. John On Thu, Jul 26, 2012 at 3:26 AM, Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote: > I can prove your lemma a bit like this: > > > axiomatization > p1 :: "nat => bool" and > p2 :: "nat => bool" and > p3 :: "nat => bool" > where > ax1: "p1 x == ~p2 x & ~p3 x" and > ax2: "p2 x == ~p1 x & ~p3 x" and > ax3: "p3 x == ~p1 x & ~p2 x" > > lemma lem: "EX! p:{p1,p2,p3}. p q" > apply simp > apply (simp add: conj_disj_distribR cong: conj_cong) > apply (metis ax1 ax2 ax3) > done > > Let me say a little about how I knew to do that. > > Firstly, introducing ax1 ax2 or ax3 as assumptions will loop the simplifier. > It will take them as rewrite rules and apply them to each other, and they're > directed towards their complex ends. I could introduce them safely the other > way around, e.g. > > > lemma lem: "EX! p:{p1,p2,p3}. p q" > using ax1[symmetric] ax2[symmetric] ax3[symmetric] > apply simp > apply (simp add: conj_disj_distribR cong: conj_cong) > apply metis > done > > The syntax "EX! p: S. P p" is an abbreviation for "EX! p. p : S --> P p". > The first simp statement reveals this by reducing "p : {p1, p2, p3}" to "p = > p1 | p = p2 | p = p3". If you are using an old enough version of Isabelle, > the syntax comes with a constant Bex1, which should be unfolded in the first > line with (simp add Bex1_def) to get to the same state. > > Secondly, I wanted to avoid the (very general) application "p q" in your > term where "p" is a quantified variable (an intrinsically higher-order > expression). If we move this statement together with the three different > equalities, and supply the "conj_cong" congruence rule (which allows the > left-hand side of conjunctions to be used to rewrite their right hand sides > in the simplifier) then the applications are of the three specific > predicates p1 p2 and p3. The equalities are still higher-order, but for some > reason metis can solve the problem already (mirabile dictu). > > The quantifiers can be removed more completely with "apply (simp add: > conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)", from which > point it is even more clear that metis should be able to solve the problem. > Maybe. > > Yours, > Thomas. > > > On 26/07/12 00:20, John Munroe wrote: >> >> Hi, >> >> I'm trying to prove a lemma containing a uniqueness quantification: >> >> axiomatization >> p1 :: "nat => bool" and >> p2 :: "nat => bool" and >> p3 :: "nat => bool" >> where >> ax1: "p1 x == ~p2 x& ~p3 x" and >> ax2: "p2 x == ~p1 x& ~p3 x" and >> ax3: "p3 x == ~p1 x& ~p2 x" >> >> >> lemma lem: "EX! p:{p1,p2,p3}. p q" >> using ax1 ax2 ax3 >> apply auto >> >> but unfortunately no proof is found. Don't ax1, ax2 and ax3 together >> imply that for all values, there's one and only one predicate that is >> true? >> >> I must be missing something here... >> >> Thanks a lot for your time. >> >> John >> > >

**Follow-Ups**:**Re: [isabelle] Uniqueness quantification***From:*Thomas Sewell

**References**:**[isabelle] Uniqueness quantification***From:*John Munroe

**Re: [isabelle] Uniqueness quantification***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Next by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Previous by Thread: Re: [isabelle] Uniqueness quantification
- Next by Thread: Re: [isabelle] Uniqueness quantification
- Cl-isabelle-users July 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