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