[isabelle] Uniqueness quantification



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





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