Re: [isabelle] Evaluation of record expressions
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
>you can go
>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
>which will limit simp+ to working on just three subgoals, but I suspect
>you don't need to.
>Hope this helps.
>On 09/10/2013, at 3:14 AM, Michael Vu <michael.vu at rwth-aachen.de>
>> 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
>> 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
>> 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
>> 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!
>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
This archive was generated by a fusion of
Pipermail (Mailman edition) and