Re: [isabelle] Proving lemmas containing a squareroot



On Fri, Jun 4, 2010 at 6:07 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> On Fri, Jun 4, 2010 at 8:11 AM, Michael Daniels <dayzman at gmail.com> wrote:
>> On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
>>> Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?
>>>
>
> If you are just interested in finding a proof, then here's one that works:
>
> lemma exists_gt_conv_neq:
>  fixes f :: "real => real"
>  shows "(EX x y. f x > f y) = (EX x y. f x ~= f y)"
> unfolding neq_iff by auto
>
> lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
> using gt unfolding exists_gt_conv_neq by simp
>

I have a somewhat related question. How come the subgoal in rt2a isn't
unfolded, given:

consts
pl :: "real => real => real"
pm :: "real => real"
j :: real

axioms
gt1: "EX a b x y. pl (pm a) x > pl (pm b) y"
gt2: "EX x y. pl (pm j) x > pl (pm j) y"

lemma rt2a: "EX x y. ( 1/(pl (pm j) x)) > ( 1/ (pl (pm j) y))"
using gt2
unfolding exists_gt_conv_neq2
oops

whereas, the following is unfolded:

lemma rt2b: "EX x y. ( (pl (pm j) x)) > ( (pl (pm j) y))"
using gt2
unfolding exists_gt_conv_neq2
by simp

Also, if the argument to pm was an existential variable, then it is
also unfolded:

lemma exists_gt_conv_neq1:
 fixes f :: "real => real => real"
 shows "(EX a b x y. f a x > f b y) = (EX a b x y. f a x ~= f b y)"
unfolding neq_iff by blast

lemma rt1: "EX a b x y. ( 1/ (pl (pm a) x)) > ( 1/ (pl (pm b) y))"
using gt1
unfolding exists_gt_conv_neq1
by simp

How come giving pm a constant disables unfolding?

Thanks again.
Michael

> - Brian
>
>>
>> Thanks
>> Michael
>>
>>> - Brian
>>>
>>
>





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