[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
lammich at in.tum.de
Tue Jul 17 19:04:32 CEST 2012
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 .
*** 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
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.
More information about the isabelle-dev