Re: [isabelle] Evaluation of record expressions
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 the following
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> 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
> 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 attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and