Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] named theorems in Isabelle/ML


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

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

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


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


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