*To*: "Isabelle.in.tum.de" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] prove simple inequality*From*: Steffen Juilf Smolka <steffen.smolka at in.tum.de>*Date*: Fri, 5 Jul 2013 19:22:39 +0200*Cc*: "michael.vu at rwth-aachen.de" <michael.vu at rwth-aachen.de>*References*: <mailman.37300.1373044827.23908.cl-isabelle-users@lists.cam.ac.uk>

There is actually another option since recently (assuming you are using the repository version of Isabelle). If you are interested in a step-by-step proof but don't won't to do the work yourself, you can try calling sledgehammer with the isar_proofs option: lemma test: assumes a1: "(a::real)>0" and a2: "a<1" and b1: "(b::real)>0" and b2: "b<1" shows "a+b - a*b > 0" sledgehammer [isar_proofs, isar_compress=2] The isar_compress option lets you control the level of detail of the generated proof(s). On my machine, sledgehammer came up with the following proof: proof - have "a * b < b" by (metis a2 b1 comm_semiring_1_class.normalizing_semiring_rules(11) mult_strict_right_mono) hence "a * b < a + b" by (metis a1 pos_add_strict) thus "0 < a + b - a * b" by (metis add_less_imp_less_right comm_semiring_1_class.normalizing_semiring_rules(5) diff_add_cancel) qed I think the resulting proof is actually quite nice and easy to follow. (Unfortunately, it doesn't always work that well.) The proof gets even nicer after some manual post-processing (which may be done automatically in the near future): proof - have "a * b < b" by (simp add: algebra_simps a2 b1) hence "a * b < a + b" by (simp add: a1 pos_add_strict) thus "0 < a + b - a * b" by simp qed Regards, Steffen On 05.07.2013, at 15:02, cl-isabelle-users-request at lists.cam.ac.uk wrote: > Dear Isabelle experts, > > i have following simple lemma: > > lemma ineq: > "(a::real) > 0 ⟹ a < 1 ⟹ (b::real) > 0 ⟹ b < 1 ⟹ (a + b - a * b) > 0" > > My problem is that i cannot prove this lemma, i tried tools like 'simp' with algebra/field_simps etc. but i cannot figure out > which rule to use. Any help would be appreciated! > > Regards, > Michael

- Previous by Date: [isabelle] SMT and bound variables.
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: Re: [isabelle] SMT and bound variables.
- Next by Thread: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?
- Cl-isabelle-users July 2013 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