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

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to