1 theory NamedThms

     2 imports "../Base"

     3 begin

     4 

     5 section {* Accumulate a List of Theorems under a Name\label{rec:named} *} 

     6 

     7 

     8 text {*

     9   {\bf Problem:} 

    10   Your tool @{text foo} works with special rules, called @{text foo}-rules.

    11   Users should be able to declare @{text foo}-rules in the theory,

    12   which are then used in a method.\smallskip

    13 

    14   {\bf Solution:} This can be achieved using named theorem lists.\smallskip

    15 

    16   Named theorem lists can be set up using the code

    17 

    18   *}

    19 

    20 ML{*structure FooRules = NamedThmsFun (

    21   val name = "foo" 

    22   val description = "Rules for foo"); *}

    23 

    24 text {*

    25   and the command

    26 *}

    27 

    28 setup {* FooRules.setup *}

    29 

    30 text {*

    31   This code declares a context data slot where the theorems are stored,

    32   an attribute @{text foo} (with the usual @{text add} and @{text del} options

    33   for adding and deleting theorems) and an internal ML interface to retrieve and 

    34   modify the theorems.

    35 

    36   Furthermore, the facts are made available on the user level under the dynamic 

    37   fact name @{text foo}. For example we can declare three lemmas to be of the kind

    38   @{text foo} by:

    39 *}

    40 

    41 lemma rule1[foo]: "A" sorry

    42 lemma rule2[foo]: "B" sorry

    43 lemma rule3[foo]: "C" sorry

    44 

    45 text {* and undeclare the first one by: *}

    46 

    47 declare rule1[foo del]

    48 

    49 text {* and query the remaining ones with:

    50 

    51   \begin{isabelle}

    52   \isacommand{thm}~@{text "foo"}\\

    53   @{text "> ?C"}\\

    54   @{text "> ?B"}\\

    55   \end{isabelle}

    56 

    57   On the ML-level the rules marked with @{text "foo"} an be retrieved

    58   using the function @{ML FooRules.get}:

    59 

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

    61 

    62   \begin{readmore}

    63   For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also

    64   the recipe in Section~\ref{recipe:storingdata} about storing arbitrary

    65   data.

    66   \end{readmore}

    67  *}

    68 

    69 text {*

    70   (FIXME: maybe add a comment about the case when the theorems 

    71   to be added need to satisfy certain properties)

    72 

    73 *}

    74 

    75 

    76 end

    77   

    78 

    79 

    80