*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Comparing square roots*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 13 Aug 2010 09:44:15 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTikRMceKeupCHgTXeGzzMhx8e+ibXxUxYTjLFb6f@mail.gmail.com>*Organization*: Technische Universität München*References*: <AANLkTikRMceKeupCHgTXeGzzMhx8e+ibXxUxYTjLFb6f@mail.gmail.com>

Am Donnerstag, den 12.08.2010, 23:28 +0100 schrieb John Munroe: > Hi all, > > Does anyone know how to prove > > lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 & > q1 >= q2 & q2 > 0 & d1 < d2) --> k*sqrt(q1*p/d1) > k*sqrt(q2*p/d2)" > > ? The goal is easy to solve directly just use C-c C-f to find the correct lemmas: First you want to remove the k, hence we search for: "?x * _ < ?x * <" We find some introduction rules, but also the rewrite rule mult_less_cancel_left (which is easier to handle). The simplifier already rewrites "sqrt ?a < sqrt ?b" by "?a < ?b". Now we have a division on a field, here we use the simp set: field_simps This results into: "q1 * d2 < q2 * d1" This isn't handled by mult_less_cancel_left, however there are nice introduction rules for this cases, just search for "_ ==> _ * _ < _ * _" and we find: mult_less_le_imp_less hence the lemma is solved by: lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 & q1 >= q2 & q2 > 0 & d1 < d2) --> k*sqrt(q1*p/d1) > k*sqrt(q2*p/d2)" by (auto simp: mult_less_cancel_left field_simps intro: mult_less_le_imp_less) You might add the introduction rule mult_less_le_imp_less with intro! instead of just intro, this has the advantage to see the goals the auto tactic can not solve, however it might apply the wrong rule and result into an unprovable goal. Greetings, - Johannes > Even with the lemma: > > lemma "ALL (d1::real) d2 p q1 q2. (d1 > 0 & d2 > 0 & p > 0 & q1 >= q2 > & q2 > 0 & d1 < d2) --> sqrt(q1*p/d1) > sqrt(q2*p/d2)" > by (simp add: frac_less2 real_mult_order) > > I can't seem to make use of it to prove the first. Sledgehammer helped > me prove the second, but it couldn't find anything for the first even > it looks like a rather straightforward extension of the second. Any > help will definitely be useful. > > Thanks > John >

**References**:**[isabelle] Comparing square roots***From:*John Munroe

- Previous by Date: Re: [isabelle] Comparing square roots
- Next by Date: Re: [isabelle] Unfolding setsum
- Previous by Thread: Re: [isabelle] Comparing square roots
- Next by Thread: [isabelle] Unfolding setsum
- Cl-isabelle-users August 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list