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

Peter Lammich lammich at in.tum.de
Tue Jul 17 19:04:32 CEST 2012

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?


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

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

More information about the isabelle-dev mailing list