Re: [isabelle] Proving lemmas containing a squareroot



On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> 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" ?
>

Indeed, I've sent a follow-up about the typo but it hasn't reached the
mailing list yet. What I meant is indeed EX rather than ALL. Any idea
on what theorems should be used here and why sledgehammer fails to
find any when it's sqrt?

Thanks
Michael

> - Brian
>





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