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");
*}
(*<*)setup FooRules.setup(*>*)

text {*
  and the command

  @{ML_text [display] "setup FooRules.setup"}

  This code declares a context data slot where the theorems are stored,
  an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options
  to 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 two lemmas to be of the kind
  @{ML_text foo}:
*}

lemma rule1[foo]: "A" sorry
lemma rule2[foo]: "B" sorry
lemma rule3[foo]: "C" sorry

text {* undeclare them: *}

declare rule1[foo del]

text {* and query them: *}

thm foo

text {* 
  In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
  using

  @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}

  \begin{readmore}
  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
  \end{readmore}
 *}

text {*
  (FIXME: maybe add a comment about the case when the theorems 
  to be added need to satisfy certain properties)

*}


end