Email Gateway (Aug 22 2022 at 16:27): Email Gateway (Aug 22 2022 at 16:27):From: Mark Wassell <mpwassell@gmail.com>
Hello,
Is is possible to include in a
setup {*
*}
block code that will create datatypes and functions? If it is possible, are
there some examples of where this has been done?
I have a lot of boilerplate code and am looking at options to
programmatically create it.
I have browsed the Isabelle Cookbook and have seen examples such as
setup {* fn thy => let
val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
val (_, thy') = Sign.declare_const @{context} bar_const thy
in
thy'
end
*}
but I think this is only part of the story.
Cheers
Mark
Email Gateway (Aug 22 2022 at 16:28):From: Makarius <makarius@sketis.net>
The cookbook is indeed only a small part of the story, and it contains a
lot of outdated and inaccurate information. Low-level theory operations
like Sign.declare_const above have no practical relevance.
Isabelle specifications are usually done in a proper local_theory
context. The corresponding command for experimentation is 'local_setup'
and for real implementations Outer_Syntax.local_theory -- see also
$ISABELLE_HOME/src/HOL/ex/Commands.thy and the "implementation" manual
chapter 8 for the context of it.
Makarius
Email Gateway (Aug 22 2022 at 16:28):From: Lars Hupel <hupel@in.tum.de>
Dear Mark,
yes, there are examples, but unfortunately not many. The keywords to
look out for are "Function.add_function" to define a function and
"BNF_FP_Def_Sugar.co_datatypes". You can look for that in the AFP.
Alternatively, you can also look here:
<https://github.com/epfl-lara/leon/blob/master/src/main/isabelle/stateful_ops.ML>.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC