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 classes).

Clemens


Quoting Peter Lammich <lammich at in.tum.de>:

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










This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.