*To*: Michael Vu <michael.vu at rwth-aachen.de>*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 14 Oct 2013 18:28:50 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <fb86700f35dac.52544b91@rwth-aachen.de>*Organization*: Technische Universität München*References*: <fb86700f35dac.52544b91@rwth-aachen.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:*Michael Vu

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

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