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.