# Re: [isabelle] Uniqueness quantification

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?

`No particularly good ideas here, except that things are becoming more
``complicated.
`

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?

`No. To phrase what I said before in different language again, the
``cardinality of the set you've been talking about "{p1, p2, p3, p4, p5}"
``isn't necessarily 5. If "p1 = p2" then there are less than 5 unique
``elements of the set "{p1, p2, p3, p4, p5}".
`

`To rephrase this once more: if you add a p6 to your axiomatization with
``the axiom ax6: "p6 = p5", then the equivalent lemma is still provable:
`
lemma lem: "EX! p:{p1,p2,p3,p4,p5, p6}. p q"

` apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib
``ex_disj_distrib)
` apply clarsimp
apply (metis axs)
done

`The reason this is provable is because "{p1, p2, p3, p4, p5, p6} = {p1,
``p2, p3, p4, p5}", so it's really just the same as the 5 example.
`
Yours,
Thomas.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*