*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Uniqueness quantification*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Fri, 27 Jul 2012 14:54:56 +1000*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAP0k5J5RUq-0OHb92ikK=A7UcvDGiP4ePkvwc-ELUqmQ0Wdt9g@mail.gmail.com>*References*: <CAP0k5J7YFMS9gRKpj_LQdW16vLp662TKFP6LTx7FHRXE19W_vA@mail.gmail.com> <5010AABA.4080701@nicta.com.au> <CAP0k5J5RUq-0OHb92ikK=A7UcvDGiP4ePkvwc-ELUqmQ0Wdt9g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

Here is a slightly stronger formulation which can be solved by auto: lemmas axs = ax1 ax2 ax3 ax4 ax5 lemma lem: "length (filter (%p. p q) [p1, p2, p3, p4, p5]) = 1" using axs[symmetric] by auto This helper rule might also be helpful: lemma ex_unique_from_length: "length (filter P xs) = 1 ==> (EX! x : set xs. P x)" apply (induct xs) apply (auto simp add: filter_empty_conv split: split_if_asm) done lemmas lem2 = ex_unique_from_length[OF lem, unfolded set.simps] Yours, Thomas. On 26/07/12 22:39, John Munroe wrote:

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:*John Munroe

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

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

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

- Previous by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Date: [isabelle] "Illegal equation head" ---an error in func definition
- 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