[isabelle] Proof breaks when stronger fact is used



Hi all,

I have a rather basic question:

Given the following constants and axioms:

typedecl T1

consts
 F :: "T1 \<Rightarrow> real"
 G :: "T1 \<Rightarrow> real"
 C :: real

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?

Any help will be appreciated.

Thanks
John





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