author | wenzelm |
Sun, 10 Aug 2014 19:53:30 +0200 | |
changeset 57888 | 9c193dcc8ec8 |
parent 57886 | 7cae177c9084 |
child 57927 | f14c1248d064 |
permissions | -rw-r--r-- |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/named_theorems.ML |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
3 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
4 |
Named collections of theorems in canonical order. |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
5 |
*) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
6 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
7 |
signature NAMED_THEOREMS = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
8 |
sig |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
9 |
val member: Proof.context -> string -> thm -> bool |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
10 |
val get: Proof.context -> string -> thm list |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
11 |
val add_thm: string -> thm -> Context.generic -> Context.generic |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
12 |
val del_thm: string -> thm -> Context.generic -> Context.generic |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
13 |
val add: string -> attribute |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
14 |
val del: string -> attribute |
57888 | 15 |
val declare: binding -> string -> local_theory -> string * local_theory |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
16 |
end; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
17 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
18 |
structure Named_Theorems: NAMED_THEOREMS = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
19 |
struct |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
20 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
21 |
(* context data *) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
22 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
23 |
structure Data = Generic_Data |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
24 |
( |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
25 |
type T = thm Item_Net.T Symtab.table; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
26 |
val empty: T = Symtab.empty; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
27 |
val extend = I; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
28 |
val merge = Symtab.join (K Item_Net.merge); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
29 |
); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
30 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
31 |
fun new_entry name = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
32 |
Data.map (fn data => |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
33 |
if Symtab.defined data name |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
34 |
then error ("Duplicate declaration of named theorems: " ^ quote name) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
35 |
else Symtab.update (name, Thm.full_rules) data); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
36 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
37 |
fun the_entry context name = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
38 |
(case Symtab.lookup (Data.get context) name of |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
39 |
NONE => error ("Undeclared named theorems " ^ quote name) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
40 |
| SOME entry => entry); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
41 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
42 |
fun map_entry name f context = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
43 |
(the_entry context name; Data.map (Symtab.map_entry name f) context); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
44 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
45 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
46 |
(* maintain content *) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
47 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
48 |
fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
49 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
50 |
fun content context = rev o Item_Net.content o the_entry context; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
51 |
val get = content o Context.Proof; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
52 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
53 |
fun add_thm name = map_entry name o Item_Net.update; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
54 |
fun del_thm name = map_entry name o Item_Net.remove; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
55 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
56 |
val add = Thm.declaration_attribute o add_thm; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
57 |
val del = Thm.declaration_attribute o del_thm; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
58 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
59 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
60 |
(* declaration *) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
61 |
|
57888 | 62 |
fun declare binding descr lthy = |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
63 |
let |
57888 | 64 |
val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding; |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
65 |
val description = |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
66 |
"declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
57888 | 67 |
val lthy' = lthy |
68 |
|> Local_Theory.background_theory |
|
69 |
(Global_Theory.add_thms_dynamic (binding, fn context => content context name) #> |
|
70 |
Attrib.setup binding (Attrib.add_del (add name) (del name)) description #> |
|
71 |
Context.theory_map (new_entry name)) |
|
72 |
|> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |
|
73 |
|> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
|
74 |
let |
|
75 |
val binding' = Morphism.binding phi binding; |
|
76 |
val context' = |
|
77 |
context |> Context.mapping |
|
78 |
(Global_Theory.alias_fact binding' name) |
|
79 |
(fn ctxt => |
|
80 |
if Facts.defined (Proof_Context.facts_of ctxt) name |
|
81 |
then Proof_Context.fact_alias binding' name ctxt |
|
82 |
else ctxt); |
|
83 |
in context' end); |
|
84 |
in (name, lthy') end; |
|
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
85 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
86 |
val _ = |
57888 | 87 |
Outer_Syntax.local_theory @{command_spec "named_theorems"} |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
88 |
"declare named collection of theorems" |
57888 | 89 |
(Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr)); |
57886
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
90 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
91 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
92 |
(* ML antiquotation *) |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
93 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
94 |
val _ = Theory.setup |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
95 |
(ML_Antiquotation.inline @{binding named_theorems} |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
96 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) => |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
97 |
let |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
98 |
val thy = Proof_Context.theory_of ctxt; |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
99 |
val name = Global_Theory.check_fact thy (xname, pos); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
100 |
val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
101 |
in ML_Syntax.print_string name end))); |
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
102 |
|
7cae177c9084
support for named collections of theorems in canonical order;
wenzelm
parents:
diff
changeset
|
103 |
end; |