Re: [isabelle] Locale interpretation introduces abbreviations rather than definitions
It is better to define the constants before making the interpretation,
because then interpretation can do the require replacements for you
(as outlined in Florian's tutorial). If your definitions don't depend
on the assumption, the approach suggested by Lukas is also appealing.
It exploits the interpretation on the foundational constants that is
generated automatically for every locale.
Interpretation can only add syntax and theorems to local theories, it
cannot make definitions. Which definitions should be made, even if
you want all, is only obvious in simple examples. Sublocale
declarations may remap constants of other involved locales, and then
probably for those no constants should be defined. My design decision
was to leave this to the discretion of the user.
This decision shouldn't prevent providing commands that solve
important special cases, like exporting all constants and then
interpreting onto them. This seems to be an important use case for
code generation. In fact, in my terminology, this operation would
compute a locale instance, not an interpretation (in analogy to type
Quoting Peter Lammich <lammich at in.tum.de>:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and