# [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.
Thanks in advance!
Michael

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