Email Gateway (Aug 19 2022 at 12:21): Email Gateway (Aug 19 2022 at 12:21):From: Michael Vu <michael.vu@rwth-aachen.de>
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:
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
Last updated: Apr 26 2024 at 08:19 UTC