Re: [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.


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