From: isabelle-users@florianmaerkl.de

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"

begin

definition "final_result = somefunc 42"

end

locale DetailThing =

fixes someval :: "nat"

assumes "someval = 1336"

context DetailThing

begin

fun thefunc :: "nat ⇒ nat" where

"thefunc _ = someval + 1"

end

sublocale DetailThing ⊆ DetailSub: FinalThing

where somefunc = thefunc

(...)

Now I interpret DetailThing and want to execute final_result from this

interpretation:

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

final_result_impl".

I found this old thread describing the same problem as far as I

understood:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-October/msg00034.html

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.

Cheers

Florian

SublocaleTest.thy

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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 simpfind_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

permanent_interpretation.

Cheers,

Florian

signature.asc

Last updated: Jan 25 2022 at 02:35 UTC