*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Michael Vu <michael.vu at rwth-aachen.de>*Date*: Mon, 14 Oct 2013 19:36:38 +0200*Cc*: "<cl-isabelle-users at lists.cam.ac.uk>" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <06546317-AC73-414A-9D3C-23889E006AC0@gmail.com>*Priority*: normal*References*: <fb86700f35dac.52544b91@rwth-aachen.de> <04A0610B-87DE-4F3E-9581-AEAFD43B0E28@nicta.com.au> <fee33879-f903-4146-96a2-933b5a19a58f@email.android.com> <4213fa15-8dd3-424b-a28a-266aa4aeb6ea@email.android.com> <6E26786F-A2F2-467B-B364-391286794FB7@gmail.com> <8189b330-2acb-4866-b345-2f82f9e911f3@email.android.com> <06546317-AC73-414A-9D3C-23889E006AC0@gmail.com>

I tried to define a similar lemma: lemma test_bounded: "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)))" apply(rule allI) apply(auto) 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 cases. 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. Michael 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. > > Regards, > > Jasmin

**References**:**[isabelle] Evaluation of record expressions***From:*Michael Vu

**Re: [isabelle] Evaluation of record expressions***From:*Andrew Boyton

**Re: [isabelle] Evaluation of record expressions***From:*Michael Vu

**Re: [isabelle] Evaluation of record expressions***From:*Michael Vu

**Re: [isabelle] Evaluation of record expressions***From:*Jasmin Blanchette

**Re: [isabelle] Evaluation of record expressions***From:*Michael Vu

**Re: [isabelle] Evaluation of record expressions***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Evaluation of record expressions
- Next by Date: Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore
- Previous by Thread: Re: [isabelle] Evaluation of record expressions
- Next by Thread: Re: [isabelle] Evaluation of record expressions
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list