Hi Rene, > ===== > locale foo = fixes f :: "nat => nat" > assumes f_mono[termination_simp]: "f x <= x" > begin > > fun bar :: "nat => nat" where > "bar 0 = 0" > | "bar (Suc x) = Suc (bar (f x))" > > end > > definition com where > [code del]: "com = foo.bar id" > > interpretation foo id > rewrites "foo.bar id = com" > unfolding com_def by (unfold_locales, auto) > > lemma "com 5 = 5" by eval > export_code com in Haskell > ===== > > > This works perfectly fine in Isabelle 2016-1, and especially > the [code del] is required to make the final export_code and eval succeed. > > In contrast, in a recent development version, the [code del] still is > accepted, > but the export_code will deliver “com _ = error …” and the “eval” will fail. > > The solution is easy: remove the previously required [code del].
this is due to subtle changes in the semantics of [code del] which now
merely removes a single equation from a list of concrete function
equations; strict removal of a function declaration is now done using
[[code drop: …]].
Note that the pattern above is avoided nowadays by an interpretation
with mixin definitions:
theory Bar
imports Main
begin
locale foo = fixes f :: "nat => nat"
assumes f_mono [termination_simp]: "f x ≤ x"
begin
fun bar :: "nat => nat" where
"bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"
end
global_interpretation foo id
defines com = bar
by standard simp
lemma "com 5 = 5" by eval
export_code com in Haskell
end
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
