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
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev