Re: [isabelle] Evaluation of record expressions
I tried to define a similar lemma:
"0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b ⟹
∀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)) ≤ ((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)))"
In this case the simplifier is able to split all possible cases, it's just the matter that it won't evaluate all expressions afterwards.
So my question is if there's a way how i can deduce this test_bounded lemma from the first one I posted and then make Isabelle evaluate all
Regarding the variables a and b: That's my fault again, happens when I try to cut a snippet from my code..You can assume that they are defined as ::real.
Am 14-10-13, schrieb Jasmin Blanchette <jasmin.blanchette at gmail.com>:
> Hi Michael,
> Am 14.10.2013 um 15:53 schrieb Michael Vu <michael.vu at rwth-aachen.de>:
> > Indeed, that was my fault. I work with custom theories where this symbol is treated as "<" (less relation) and I forgot to replace it. Hope you could somehow help me now. My goal is just to make isabelle split all possible cases as they are finite and then solve every case for itself.
> I fail to see why your problem is finite. The pair of assumptions "forall s. ..." quantify over all states, of which there are infinitely many. I see some "if"s that could perhaps be split into separate cases, but they are under the scope of lambdas that bind again an infinite variable.
> Also, some of your variables seem to have overly general types, e.g. "a" has type 'a. Indeed, Nitpick reports a "potentially spurious" counterexample that appears to be genuine.
This archive was generated by a fusion of
Pipermail (Mailman edition) and