*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Michael Vu <michael.vu at rwth-aachen.de>*Date*: Mon, 14 Oct 2013 19:34:39 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1381768130.4401.40.camel@macbroy12.informatik.tu-muenchen.de>*Priority*: normal*References*: <fb86700f35dac.52544b91@rwth-aachen.de> <1381768130.4401.40.camel@macbroy12.informatik.tu-muenchen.de>

Hello Johannes, Yes, "⊩" basically means "≤". I tried to define a similar lemma: lemma test_bounded: "0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b ⟹ ∀s. ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) + (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)) ≤ ((if c s ≠ 1 then 1 else 0) * ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) + (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)))" apply(rule allI) apply(auto) In this case the simplifier is able to split all possible cases, it's just the matter that it won't evaluate all expressions afterwards. So my question is if there's a way how i can deduce this test_bounded lemma from the first one I posted and then make Isabelle evaluate all cases. Thanks! Michael Am 14-10-13, schrieb Johannes Hölzl <hoelzl at in.tum.de>: > Am Dienstag, den 08.10.2013, 18:14 +0200 schrieb Michael Vu: > > Dear isabelle experts, > > > > I am currently working with records and I'm trying to write a small automation tool for generating calculations. But I'm stuck at proving some simple expressions like this one: > > > > record state = > > t :: real > > c :: real > > > > lemma weakly_bounded: > > "0 < a ⟹ > > a < 1 ⟹ > > 0 < b ⟹ > > b < 1 ⟹ > > 0 < a + b - a * b ⟹ > > ∀s. t s = 0 ∨ t s = 1 ⟹ > > ∀s. c s = 0 ∨ c s = 1 ⟹ > > λs. (if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) + > > (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / > > (a + b - > > a * b) ⊩ λs. (if c s ≠ 1 then 1 else 0) * > > ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) + > > (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b))" > > > > I thought simp would be enough to evaluate this, but it seems not to be the case. So I am looking for a way to make isabelle automatically verify > > all possible states (the space is finite due to the conditions). I would appreciate every help. > > Is ⊩ point wise less or equal? If yes, you first should > unfold fun_le_def, then the splitter can operate on it. Also I don't > think that the simplifier can deduce that the set of states is finite. > > > And secondly I've another cosmetic question. Given following subgoals: > > > > 1. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a > > 2. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ 1 - b > > 3. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a > > 4. some complicated subgoal > > apply(simp) > > apply(simp) > > apply(simp) > > > > Is there any more elegant way other than to invoke simp 3 times? I also tried "auto" but it gets stuck on subgoal 4. > > You can use Isar to proof subgoal 4 first and subgoal 1, 2, 3 by the > qed-command: > > proof - > assumes "" then show "" ... > qed simp_all > > > - Johannes

**Follow-Ups**:**Re: [isabelle] Evaluation of record expressions***From:*Thomas Sewell

**References**:**[isabelle] Evaluation of record expressions***From:*Michael Vu

**Re: [isabelle] Evaluation of record expressions***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore
- Next by Date: Re: [isabelle] Evaluation of record expressions
- Previous by Thread: Re: [isabelle] Evaluation of record expressions
- Next by Thread: Re: [isabelle] Evaluation of record expressions
- Cl-isabelle-users October 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