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



This new version of your axiom still provable using auto and therefore completely weak. You might have better luck with this formulation:

lemma "\<exists>P. P \<noteq> {} \<and> (\<forall>s1\<in>P. \<forall>s2\<in>P. s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2)"

Larry Paulson


On 31 May 2010, at 18:16, John Munroe wrote:

> I see. But even if ax1 was:
> 
> ax1: "\<exists>P. \<exists>s1\<in>P. \<exists>s2\<in>P. P \<noteq> {}
> \<and> s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
> 
> and ax1a was:
> 
> ax1a: "\<exists>P. \<forall>s1\<in>P. \<forall>s2\<in>P. P \<noteq> {}
> \<and> s1 \<noteq> s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
> 
> The second part of the proof still breaks. Am I supposed to simplify
> the goal further?






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