Re: [isabelle] Evaluation of record expressions



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





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