*To*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Subject*: Re: [isabelle] Uniqueness quantification*From*: John Munroe <munddr at gmail.com>*Date*: Fri, 27 Jul 2012 12:02:52 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <50121F20.5020602@nicta.com.au>*References*: <CAP0k5J7YFMS9gRKpj_LQdW16vLp662TKFP6LTx7FHRXE19W_vA@mail.gmail.com> <5010AABA.4080701@nicta.com.au> <CAP0k5J5RUq-0OHb92ikK=A7UcvDGiP4ePkvwc-ELUqmQ0Wdt9g@mail.gmail.com> <50121F20.5020602@nicta.com.au>

Thanks again for your help. > > I suppose I should ask the obvious: these equalities on predicates seem a > bit strange. The "p1 = p2" possibilities all over the place are complicating > things. Do you want the property "p q" to hold for exactly one of the 5 > *expressions* p1, p2, ... or for exactly one of the *values*, of which there > might be less than 5? Note that "EX! p : {p1, p2, p3, p4, p5}. p q" would be > true if "p1 q" and "p2 q" but "p1 = p2" (although that's impossible in this > case). I indeed want "p q" to hold for exactly one of the 5 expressions, i.e. only one of the 5 predicates returns true for all arguments. Applying clarify/clarsimp seems to work indeed. However, if I change the type of the predicates from "nat => bool" to "(nat*nat) => bool", the proof breaks. Do you know why the input type of the predicates affects the proof? > > 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)" Right, but how come the reverse doesn't hold? If there's exactly one of the predicates returning true, then isn't the length of the filtered list one? Thanks again. John

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

**Re: [isabelle] Uniqueness quantification***From:*Tjark Weber

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

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

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

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

- Previous by Date: [isabelle] Windows Command Line 2012
- Next by Date: Re: [isabelle] Uniqueness quantification
- 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