Re: [isabelle] Evaluation of record expressions



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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.