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

*** "Test.foo.D" 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.

Cheers,
	Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de





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