*To*: Michael Vu <michael.vu at rwth-aachen.de>*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Andrew Boyton <Andrew.Boyton at nicta.com.au>*Date*: Wed, 9 Oct 2013 21:44:11 +0000*Accept-language*: en-AU, en-US*Cc*: "<cl-isabelle-users at lists.cam.ac.uk>" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <fb86700f35dac.52544b91@rwth-aachen.de>*References*: <fb86700f35dac.52544b91@rwth-aachen.de>*Thread-index*: AQHOxN9MuIA1Db9+cU+Io8G3pujeB5nsLzwA*Thread-topic*: [isabelle] Evaluation of record expressions

To answer the simple question. Instead of apply(simp) apply(simp) apply(simp) you can go apply(simp)+ or apply(simp_all) Strictly speaking, simp+ and simp_all have different semantics. simp_all works on all subgoals, where as simp+ works on the first subgoal, and if that discharges, it works on the second. Neither does exactly what the calling simp 3 times does, as they both try applying simp to the fourth goal. If you don't want that to happen, you can do the following apply (simp+)[3] which will limit simp+ to working on just three subgoals, but I suspect you don't need to. Hope this helps. Andrew On 09/10/2013, at 3:14 AM, Michael Vu <michael.vu at rwth-aachen.de> wrote: > 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. > > 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. > > Thanks in advance! > Michael > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

**Follow-Ups**:**Re: [isabelle] Evaluation of record expressions***From:*Michael Vu

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

- Previous by Date: [isabelle] "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: call for starting school application and workshop registration
- Next by Date: Re: [isabelle] General code_abort'd constant
- Previous by Thread: [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