theory NamedThms+ −
imports "../Base"+ −
begin+ −
+ −
section {* Accumulate a List of Theorems under a Name *} + −
+ −
+ −
text {*+ −
{\bf Problem:} + −
Your tool @{text foo} works with special rules, called @{text foo}-rules.+ −
Users should be able to declare @{text foo}-rules in the theory,+ −
which are then used in a method.\smallskip+ −
+ −
{\bf Solution:} This can be achieved using named theorem lists.\smallskip+ −
+ −
Named theorem lists can be set up using the code+ −
+ −
*}+ −
+ −
ML{*structure FooRules = NamedThmsFun (+ −
val name = "foo" + −
val description = "Rules for foo"); *}+ −
+ −
text {*+ −
and the command+ −
*}+ −
+ −
setup {* FooRules.setup *}+ −
+ −
text {*+ −
This code declares a context data slot where the theorems are stored,+ −
an attribute @{text foo} (with the usual @{text add} and @{text del} options+ −
for adding and deleting theorems) and an internal ML interface to retrieve and + −
modify the theorems.+ −
+ −
Furthermore, the facts are made available on the user level under the dynamic + −
fact name @{text foo}. For example we can declare three lemmas to be of the kind+ −
@{text foo} by:+ −
*}+ −
+ −
lemma rule1[foo]: "A" sorry+ −
lemma rule2[foo]: "B" sorry+ −
lemma rule3[foo]: "C" sorry+ −
+ −
text {* and undeclare the first one by: *}+ −
+ −
declare rule1[foo del]+ −
+ −
text {* and query the remaining ones with:+ −
+ −
@{ML_response_fake_both [display,gray] "thm foo" + −
"?C+ −
?B"}+ −
+ −
On the ML-level the rules marked with @{text "foo"} an be retrieved+ −
using the function @{ML FooRules.get}:+ −
+ −
@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}+ −
+ −
\begin{readmore}+ −
For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also+ −
the recipe in Section~\ref{recipe:storingdata} about storing arbitrary+ −
data.+ −
\end{readmore}+ −
*}+ −
+ −
text {*+ −
(FIXME: maybe add a comment about the case when the theorems + −
to be added need to satisfy certain properties)+ −
+ −
*}+ −
+ −
+ −
end+ −
+ −
+ −
+ −
+ −