Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation of a definition obtained throu...

view this post on Zulip Email Gateway (Aug 08 2020 at 10:10):

Hello everyone,

I am currently struggling with the following issue, which I tried to
condense into a minimal example:
I have two locales "FinalThing" and "DetailThing" where FinalThing
defines some useful definition "final_result" and DetailThing is made a
sublocale of FinalThing:

locale FinalThing =
  fixes somefunc :: "nat ⇒ nat"
  assumes "somefunc 42 = 1337"
definition "final_result = somefunc 42"

locale DetailThing =
  fixes someval :: "nat"
  assumes "someval = 1336"

context DetailThing
fun thefunc :: "nat ⇒ nat" where
  "thefunc _ = someval + 1"
sublocale DetailThing ⊆ DetailSub: FinalThing
  where somefunc = thefunc


Now I interpret DetailThing and want to execute final_result from this

global_interpretation DetailThing
  where someval = "1334 + 2"
  defines final_result_impl = DetailSub.final_result
  and the_func_impl = thefunc
  by (standard, simp)

export_code the_func_impl in SML ― ‹works because of the "defines
final_result_impl = FinalThing.final_result"›
export_code final_result_impl in SML ― ‹doesn't work despite the
"defines the_func_impl = thefunc"›

Here, I can generate code for thefunc since as it is defined directly in
DetailThing, but for final_result I get the error "No code equations for
I found this old thread describing the same problem as far as I
However the proposed solution uses permanent_interpretation which
apparently doesn't exist anymore and I am unsure what the equivalent in
Isabelle 2020 would be.

I've attached the full theory.



view this post on Zulip Email Gateway (Aug 17 2020 at 17:50):

From: Florian Haftmann <>
Hi Florian,

I did not study your example in full but from

global_interpretation DetailThing
where someval = "1334 + 2"
defines the_func_impl = thefunc
and final_result_impl = DetailSub.final_result
by standard simp

find_theorems final_result_impl

you see that no suitable code equations is provided for
final_result_impl, and looking at the theorems

thm final_result_impl_def DetailSub.final_result_def

I guess this is due to your definitions not forming a confluent system,
maybe due to the construction

fun thefunc :: "nat ⇒ nat" where
"thefunc _ = someval + 1"

which drops an argument. (A rough first guess).

In this case you have to provide your code equation explicitly.

Note that global_interpretation is the offical successor of prototypic


Last updated: Jan 25 2022 at 02:35 UTC