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.