[isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170831/d3fd27e3/attachment.sig>