Re: [isabelle] Non-exhaustive case certificates

Hi Andreas,

However, when I restrict foo to some subset of constructors, say

code_datatype A B C

then export_code on test generates the error message

*** "" is not a constructor, on left hand side of equation:
*** case D of A => ?f1.0 | B => ?f2.0 | C => ?f3.0 | D => ?f4.0 == ?f4.0
*** At command "export_code"

This has nothing to do with the case certificate, but stems from the code equations for »foo_case«. The case certificate should be thrown away on »code_datatype«, so code generation falls back on the corresponding code equations.

So do something like:

lemma [code, code del]:
  "foo_case = foo_case" ..

lemma [code]:
  "foo_case … = …"
  "foo_case … = …"
  "foo_case … = …"
  "foo_case … = …"

If you still want proper case expressions, add a case certificate manually.

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.



PGP available:

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