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



On 1 June 2010 06:38, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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)"

Certainly this will make it easier to prove the desired result, since
this formulation (as an axiom) allows you to derive a contradiction.
See attached.

Timothy
<><

Attachment: Scratch.thy
Description: Binary data



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