# [isabelle] Evaluation of record expressions

```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.