Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Define datatypes and functions in setup block?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC