7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 Your tool @{text foo} works with special rules, called @{text foo}-rules. |
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, |
11 Users should be able to declare @{text foo}-rules in the theory, |
12 which are then used by some method.\smallskip |
12 which are then used in a method.\smallskip |
13 |
13 |
14 {\bf Solution:} This can be achieved using |
14 {\bf Solution:} This can be achieved using named theorem lists.\smallskip |
|
15 |
|
16 Named theorem lists can be set up using the code |
15 |
17 |
16 *} |
18 *} |
|
19 |
17 ML {* |
20 ML {* |
18 structure FooRules = NamedThmsFun( |
21 structure FooRules = NamedThmsFun ( |
19 val name = "foo" |
22 val name = "foo" |
20 val description = "Rules for foo" |
23 val description = "Rules for foo"); |
21 ); |
|
22 *} |
24 *} |
23 |
25 (*<*)setup FooRules.setup(*>*) |
24 setup FooRules.setup |
|
25 |
26 |
26 text {* |
27 text {* |
|
28 and the command |
|
29 |
|
30 @{ML_text [display] "setup FooRules.setup"} |
|
31 |
27 This code declares a context data slot where the theorems are stored, |
32 This code declares a context data slot where the theorems are stored, |
28 an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options |
33 an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options |
29 to adding and deleting theorems) and an internal ML interface to retrieve and |
34 to adding and deleting theorems) and an internal ML interface to retrieve and |
30 modify the theorems. |
35 modify the theorems. |
31 |
36 |
32 Furthermore, the facts are made available on the user level under the dynamic |
37 Furthermore, the facts are made available on the user level under the dynamic |
33 fact name @{text foo}. For example: |
38 fact name @{text foo}. For example we can declare two lemmas to be of the kind |
|
39 @{ML_text foo}: |
34 *} |
40 *} |
35 |
41 |
36 lemma rule1[foo]: "A" sorry |
42 lemma rule1[foo]: "A" sorry |
37 lemma rule2[foo]: "B" sorry |
43 lemma rule2[foo]: "B" sorry |
38 |
44 |
|
45 text {* undeclare them: *} |
|
46 |
39 declare rule1[foo del] |
47 declare rule1[foo del] |
|
48 |
|
49 text {* and query them: *} |
40 |
50 |
41 thm foo |
51 thm foo |
42 |
52 |
43 text {* |
53 text {* |
44 In an ML-context the rules marked with @{ML_text "foo"} an be retrieved |
54 In an ML-context the rules marked with @{ML_text "foo"} an be retrieved |
45 using |
55 using |
46 *} |
|
47 |
56 |
48 ML {* FooRules.get @{context} *} |
57 @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"} |
49 |
58 |
50 |
|
51 text {* |
|
52 \begin{readmore} |
59 \begin{readmore} |
53 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
60 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
54 \end{readmore} |
61 \end{readmore} |
55 *} |
62 *} |
56 |
63 |