# Re: [isabelle] Uniqueness quantification

I can prove your lemma a bit like this:
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"
apply simp
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (metis ax1 ax2 ax3)
done
Let me say a little about how I knew to do that.

`Firstly, introducing ax1 ax2 or ax3 as assumptions will loop the
``simplifier. It will take them as rewrite rules and apply them to each
``other, and they're directed towards their complex ends. I could
``introduce them safely the other way around, e.g.
`
lemma lem: "EX! p:{p1,p2,p3}. p q"
using ax1[symmetric] ax2[symmetric] ax3[symmetric]
apply simp
apply (simp add: conj_disj_distribR cong: conj_cong)
apply metis
done

`The syntax "EX! p: S. P p" is an abbreviation for "EX! p. p : S --> P
``p". The first simp statement reveals this by reducing "p : {p1, p2, p3}"
``to "p = p1 | p = p2 | p = p3". If you are using an old enough version of
``Isabelle, the syntax comes with a constant Bex1, which should be
``unfolded in the first line with (simp add Bex1_def) to get to the same
``state.
`

`Secondly, I wanted to avoid the (very general) application "p q" in your
``term where "p" is a quantified variable (an intrinsically higher-order
``expression). If we move this statement together with the three different
``equalities, and supply the "conj_cong" congruence rule (which allows the
``left-hand side of conjunctions to be used to rewrite their right hand
``sides in the simplifier) then the applications are of the three specific
``predicates p1 p2 and p3. The equalities are still higher-order, but for
``some reason metis can solve the problem already (mirabile dictu).
`

`The quantifiers can be removed more completely with "apply (simp add:
``conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)", from
``which point it is even more clear that metis should be able to solve the
``problem. Maybe.
`
Yours,
Thomas.
On 26/07/12 00:20, John Munroe wrote:

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.*