# Re: [isabelle] Uniqueness quantification

```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

```

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