Re: [isabelle] Uniqueness quantification



Hi Thomas,

Thanks so much for your detailed explanation.

I've tried your suggestion and it works! However, I've tried extending
the model to 5 predicates:


axiomatization
p1 :: "nat => bool" and
p2 :: "nat => bool" and
p3 :: "nat => bool" and
p4 :: "nat => bool" and
p5 :: "nat => bool"
where
ax1: "p1 x == ~p2 x & ~p3 x & ~p4 x & ~p5 x" and
ax2: "p2 x == ~p1 x & ~p3 x & ~p4 x & ~p5 x" and
ax3: "p3 x == ~p1 x & ~p2 x & ~p4 x & ~p5 x" and
ax4: "p4 x == ~p1 x & ~p2 x & ~p3 x & ~p5 x" and
ax5: "p5 x == ~p1 x & ~p2 x & ~p3 x & ~p4 x"

and

metis loops at:

lemma lem: "EX! p:{p1,p2,p3,p4,p5}. p q"
using ax1[symmetric] ax2[symmetric] ax3[symmetric] ax4[symmetric]
ax5[symmetric]
apply simp
apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)
apply metis

Do you know why it's fine for a smaller number of predicates, e.g., 3,
but not when there are 5? Do you happen to know how to simplify the
goal further?

Thanks a lot for your time.

John

On Thu, Jul 26, 2012 at 3:26 AM, Thomas Sewell
<Thomas.Sewell at nicta.com.au> wrote:
> 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.