*To*: Andrew Boyton <Andrew.Boyton at nicta.com.au>*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Michael Vu <michael.vu at rwth-aachen.de>*Date*: Fri, 11 Oct 2013 16:23:20 +0200*Cc*: "<cl-isabelle-users at lists.cam.ac.uk>" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <04A0610B-87DE-4F3E-9581-AEAFD43B0E28@nicta.com.au>*References*: <fb86700f35dac.52544b91@rwth-aachen.de> <04A0610B-87DE-4F3E-9581-AEAFD43B0E28@nicta.com.au>*User-agent*: K-9 Mail for Android

Hi Andrew, Thank you for your kind answer, that's what I searched for. Regarding the first (and more important question) : the relation symbol can be treated as a "<" relation. Andrew Boyton <Andrew.Boyton at nicta.com.au> schrieb: >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

**Re: [isabelle] Evaluation of record expressions***From:*Andrew Boyton

- Previous by Date: Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing]
- Next by Date: Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them
- 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