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

On 1 June 2010 06:38, Lawrence Paulson <lp15 at> 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.


Attachment: Scratch.thy
Description: Binary data

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