Email Gateway (Aug 19 2022 at 16:46): Email Gateway (Aug 19 2022 at 16:46):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
how do I imitate addition and retrieval of named theorems in
Isabelle/ML. More specifically, to obtain all theorems in a named
theorem bundle "a" I currently do
Proof_Context.get_thms ctxt "Theory_Name.a"
This works, but it feels strange to add this Theory name prefix
(although it would not be strictly necessary, I like to avoid potential
clashes).
Moreover, how do I add new theorems to an existing bundle? I.e., the
equivalent of
declare some_thm [a]
in Isabelle/ML?
cheers
chris
Email Gateway (Aug 19 2022 at 16:46):From: Christian Sternagel <c.sternagel@gmail.com>
Thanks Lars!
just for the record. Another way I spotted in the implementation manual is
Named_Theorems.get ctxt @{named_theorems "a"}
(I couldn't find documentation for this antiquotation though.)
cheers
chris
Email Gateway (Aug 19 2022 at 16:47):From: Makarius <makarius@sketis.net>
As usual the default documentation is two-fold:
(1) The definition in ML, which is accessible by C-hover click on the
antiquotation name.
(2) Example applications that are lying around in the Isabelle sources,
which can be found by a hyper-search of "@{named_theorems".
The implementation idiom to have an abstract formal concept like
"named_theorems" with a command to define it and an antiquotation to refer
to it in the ML sources is similar to 'simproc_setup' and @{simproc}.
The formal antiquotation also has the advantage to participate in
completion, without further ado.
BTW, this updated version of named_theorems actually belongs to the
ongoing development after Isabelle2014, i.e. is not present in the
official release. At the moment we are talking about something like
Isabelle/364992cd3c50.
Makarius
https://stop-ttip.org/signatures-member-states
Email Gateway (Aug 19 2022 at 16:47):From: Makarius <makarius@sketis.net>
(Back to the start of this thread.)
The wording above confuses me.
Did you actually mean "bundle" in the formal sense of a bundle as defined
by the 'bundle' command?
A "named theorem" is just a specific implementation of a "dynamic fact".
A fact is a list of thm, and a dynamic fact a function that produces such
a thm list from the context. No "bundle" here.
Makarius
http://stop-ttip.org 1,070,206 people so far
Email Gateway (Aug 19 2022 at 16:47):From: Christian Sternagel <c.sternagel@gmail.com>
Sorry for the confusion (in fact, awareness of the potential confusion
seeped in directly after pressing the "send" button of my email client).
To clarify, what I meant was "collection" of theorems (and after your
explanation I guess what I really meant was the "dynamic fact"
implementation corresponding to the "named_theorems" command).
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC