theory NamedThmsimports "../Base"beginsection {* Accumulate a List of Theorems under a Name\label{rec:named} *} 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" sorrylemma rule2[foo]: "B" sorrylemma rule3[foo]: "C" sorrytext {* and undeclare the first one by: *}declare rule1[foo del]text {* and query the remaining ones with: \begin{isabelle} \isacommand{thm}~@{text "foo"}\\ @{text "> ?C"}\\ @{text "> ?B"}\\ \end{isabelle} 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