Re: [isabelle] Proving lemmas containing a squareroot



On Thu, Jun 3, 2010 at 9:15 PM, Michael Daniels <dayzman at gmail.com> 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
done

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.