Re: [isabelle] Proof breaks when stronger fact is used

It is not stronger than ax1. In fact, ax1a can be proved as a theorem using auto. This is because P could simply denote the empty set.

Larry Paulson

On 30 May 2010, at 21:16, John Munroe wrote:

> axioms
> ax1: "\<exists>P. \<exists>s1\<in>P. \<exists>s2\<in>P. s1 \<noteq>
> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
> ax1a: "\<exists>P. \<forall>s1\<in>P. \<forall>s2\<in>P. s1 \<noteq>
> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
> ax2: "F p > 0"
> ax3: "C > 0"
> I can prove that "\<exists> func s. func s \<noteq> (\<lambda> s. (F
> s, (C  / F s)))" with
> lemma lem1: "\<exists> func s. func s \<noteq> (\<lambda> s. (F s, (C  / F s)))"
> proof (intro exI)
> have "\<forall> s1 s2 t. (F s1< F s2) --> (C  / F s1) > (C  / F s2)"
>   using ax3 ax2
>   by (simp add: divide_inverse real_less_def)
> then show "(\<lambda> s. (F s, G s)) \<noteq> (\<lambda> s. (F s, (C
> / F s)))"
>   using ax1
>   apply (intro notI)
>   apply (simp add: expand_fun_eq real_mult_commute)
>   by (metis linorder_not_le)
> qed
> However, if I want to *not* use ax1 but use ax1a instead, the proof
> breaks. Isn't ax1a stronger than ax1? If so, why can a proof using ax1
> break when a stronger ax1a is used as a fact instead?

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