Re: [isabelle] Proving lemmas containing a squareroot

On Thu, Jun 3, 2010 at 9:15 PM, Michael Daniels <dayzman at> wrote:
> Hi
> I'm hoping some of you could help me with the following lemma:
> lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
> using gt
> sledgehammer;
> It seems like a rather simple lemma but sledgehammer (E, SPASS, and
> Vampire) can't seem to return the set of theorems for metis. Does
> anyone know how to prove it?

This lemma rt4 is obviously false. Consider the case where a and b are equal.

lemma rt4_wrong: "~ (ALL a b. sqrt(4) / pl a > sqrt(4) / pl b)"
apply simp
apply (rule exI [where x=1])
apply (rule exI [where x=1])
apply simp

Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?

- Brian

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