Email Gateway (Aug 18 2022 at 20:30): Email Gateway (Aug 18 2022 at 20:30):From: Peter Lammich <lammich@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
Email Gateway (Aug 18 2022 at 20:32):From: Clemens Ballarin <ballarin@in.tum.de>
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@in.tum.de>:
Last updated: Apr 20 2024 at 04:19 UTC