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
