[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions

[Peter Lammich]

Hi all, 

I have the problem that locale interpretation introduces abbreviations
for locally defined constants, rather than definitions. This does not
work well with the code generator. Is there a way to make locale
interpretation introduce real definitions, and, if not, how much effort
would it be to implement such a feature?

Example:

locale l =
  fixes g::"'a => 'b"
begin
  definition "foo x == (g x,x)"
  lemma lem: "snd (foo x) = x" unfolding foo_def by simp
end

interpretation i: l id .
thm i.lem
export_code i.foo
*** Not a constant: l.foo id


What I would like here is, that the interpretation command introduces a
new constant i.foo, with the definition (or at least code equation)
"i.foo x == (g x,x)", and that this constant is also used in the
instantiated facts.

For this, the code generator could then generate code.

Currently, I am defining those constants by hand, after the
interpretation, which causes lots of boilerplate in my real applications
with more than a dozen of definitions.


-- Peter