Re: [isabelle] Non-exhaustive case certificates



Hi Florian,

thanks for the clarifiction.

> If you still want proper case expressions, add a case certificate manually.
Yes, I do want them, because otherwise ML evaluates all parameters too foo_case, which might raise an exception. And I do not want to add closures everywhere.

> Case certificates must always be exhaustive!
Exhaustive with respect to what? The lemma below is exhaustive with respect to the code generator setup -- there are three code_datatype constructors and there is one conclusion for each). I do not see why code certificates need to be exhaustive with respect to the logic other than restrictions in the code generator implementation.

>> lemma new_foo_case_cert:
>> assumes "CASE == foo_case a b c d"
>> shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
>> using assms by auto
>> setup {*
>> Code.add_case @{thm new_foo_case_cert}
>> *}
>
> What is suspicicious is that »d« never occurs in the conclusion. I guess they
> should read »a d« etc.
I do not fully understand your remark, but let me explain in a bit more detail:
foo_case is not changed by the code_datatype command. Logically, type foo still has 4 constructors, so the case combinator needs to have 4 parameters for the cases, which are a, b, c, and d in the above lemma. However, the code generator only knows about three constructors A, B, and C. As soon as I try to prove a case certificate with 4 conclusions, I get a "bad case certificate" error. For example:

lemma new_foo_case_cert:
  assumes "CASE == foo_case a b c d"
  shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c) &&& (CASE D = d)"
  using assms by auto
setup {* Code.add_case @{thm new_foo_case_cert} *}

I also tried the following version without success:

lemma new_foo_case_cert:
  assumes "CASE == foo_case a b c"
  shows "(CASE d A == a) &&& (CASE d B == b) &&& (CASE d C == c)"

So what is the right form of the certificate?

Note that I cannot define a specialised case combinator such as

foo_case' a b c = foo_case a b c 3

and use the symmetric equation as code_unfold, because other constants might need different specialised case combinators and the code generator supports only one.

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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