author | wenzelm |
Sat, 15 Mar 2014 11:59:18 +0100 | |
changeset 56161 | 300f613060b0 |
parent 56140 | ed92ce2ac88e |
child 57887 | 44354c99d754 |
permissions | -rw-r--r-- |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
1 |
(* Title: Pure/global_theory.ML |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
2 |
Author: Makarius |
3987 | 3 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
4 |
Global theory content: stored facts. |
3987 | 5 |
*) |
6 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
7 |
signature GLOBAL_THEORY = |
3987 | 8 |
sig |
27198 | 9 |
val facts_of: theory -> Facts.T |
56003 | 10 |
val check_fact: theory -> xstring * Position.T -> string |
26666 | 11 |
val intern_fact: theory -> xstring -> string |
26693 | 12 |
val defined_fact: theory -> string -> bool |
27198 | 13 |
val hide_fact: bool -> string -> theory -> theory |
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
14 |
val get_thms: theory -> xstring -> thm list |
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
15 |
val get_thm: theory -> xstring -> thm |
56161 | 16 |
val all_thms_of: theory -> bool -> (string * thm) list |
21580 | 17 |
val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
21567 | 18 |
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
21580 | 19 |
val burrow_facts: ('a list -> 'b list) -> |
20 |
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
|
21 |
val name_multi: string -> 'a list -> (string * 'a) list |
|
33700 | 22 |
val name_thm: bool -> bool -> string -> thm -> thm |
23 |
val name_thms: bool -> bool -> string -> thm list -> thm list |
|
24 |
val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list |
|
29579 | 25 |
val store_thms: binding * thm list -> theory -> thm list * theory |
26 |
val store_thm: binding * thm -> theory -> thm * theory |
|
27 |
val store_thm_open: binding * thm -> theory -> thm * theory |
|
28 |
val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory |
|
29 |
val add_thm: (binding * thm) * attribute list -> theory -> thm * theory |
|
30 |
val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory |
|
31 |
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory |
|
30853 | 32 |
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list |
33 |
-> theory -> (string * thm list) list * theory |
|
29579 | 34 |
val add_defs: bool -> ((binding * term) * attribute list) list -> |
18377 | 35 |
theory -> thm list * theory |
29579 | 36 |
val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> |
37 |
theory -> thm list * theory |
|
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset
|
38 |
val add_defs_cmd: bool -> ((binding * string) * attribute list) list -> |
18377 | 39 |
theory -> thm list * theory |
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset
|
40 |
val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list -> |
19629 | 41 |
theory -> thm list * theory |
3987 | 42 |
end; |
43 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
44 |
structure Global_Theory: GLOBAL_THEORY = |
3987 | 45 |
struct |
46 |
||
27198 | 47 |
(** theory data **) |
26282
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset
|
48 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
49 |
structure Data = Theory_Data |
24713 | 50 |
( |
49010 | 51 |
type T = Facts.T; |
52 |
val empty = Facts.empty; |
|
53 |
val extend = I; |
|
54 |
val merge = Facts.merge; |
|
24713 | 55 |
); |
3987 | 56 |
|
49010 | 57 |
val facts_of = Data.get; |
26666 | 58 |
|
56003 | 59 |
fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy); |
26666 | 60 |
val intern_fact = Facts.intern o facts_of; |
26693 | 61 |
val defined_fact = Facts.defined o facts_of; |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
62 |
|
49010 | 63 |
fun hide_fact fully name = Data.map (Facts.hide fully name); |
6367 | 64 |
|
3987 | 65 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
66 |
(* retrieve theorems *) |
27198 | 67 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
68 |
fun get_thms thy xname = |
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
69 |
#2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); |
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
70 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
71 |
fun get_thm thy xname = |
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
72 |
Facts.the_single (xname, Position.none) (get_thms thy xname); |
4783 | 73 |
|
56161 | 74 |
fun all_thms_of thy verbose = |
75 |
let |
|
76 |
val facts = facts_of thy; |
|
77 |
fun add (name, ths) = |
|
78 |
if not verbose andalso Facts.is_concealed facts name then I |
|
79 |
else append (map (`(Thm.get_name_hint)) ths); |
|
80 |
in Facts.fold_static add facts [] end; |
|
16336 | 81 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
82 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
83 |
|
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
84 |
(** store theorems **) |
3987 | 85 |
|
21580 | 86 |
(* fact specifications *) |
87 |
||
88 |
fun map_facts f = map (apsnd (map (apfst (map f)))); |
|
89 |
fun burrow_fact f = split_list #>> burrow f #> op ~~; |
|
90 |
fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; |
|
91 |
||
92 |
||
4853 | 93 |
(* naming *) |
94 |
||
18801 | 95 |
fun name_multi name [x] = [(name, x)] |
26457 | 96 |
| name_multi "" xs = map (pair "") xs |
97 |
| name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
98 |
|
33700 | 99 |
fun name_thm pre official name thm = thm |
41696 | 100 |
|> (if not official orelse pre andalso Thm.derivation_name thm <> "" then I |
101 |
else Thm.name_derivation name) |
|
102 |
|> (if name = "" orelse pre andalso Thm.has_name_hint thm then I |
|
103 |
else Thm.put_name_hint name); |
|
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
104 |
|
33700 | 105 |
fun name_thms pre official name xs = |
106 |
map (uncurry (name_thm pre official)) (name_multi name xs); |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
107 |
|
33700 | 108 |
fun name_thmss official name fact = |
109 |
burrow_fact (name_thms true official name) fact; |
|
4853 | 110 |
|
111 |
||
11998 | 112 |
(* enter_thms *) |
4853 | 113 |
|
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset
|
114 |
fun register_proofs thms thy = (thms, Thm.register_proofs thms thy); |
49010 | 115 |
|
28861 | 116 |
fun enter_thms pre_name post_name app_att (b, thms) thy = |
28965 | 117 |
if Binding.is_empty b |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
118 |
then app_att thms thy |-> register_proofs |
30211 | 119 |
else |
120 |
let |
|
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46775
diff
changeset
|
121 |
val name = Sign.full_name thy b; |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
122 |
val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs; |
30211 | 123 |
val thms'' = map (Thm.transfer thy') thms'; |
49747 | 124 |
val thy'' = thy' |> Data.map |
125 |
(Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd); |
|
30211 | 126 |
in (thms'', thy'') end; |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
127 |
|
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
128 |
|
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
129 |
(* store_thm(s) *) |
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
130 |
|
33700 | 131 |
fun store_thms (b, thms) = |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
132 |
enter_thms (name_thms true true) (name_thms false true) pair (b, thms); |
28076 | 133 |
|
29579 | 134 |
fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
135 |
|
29579 | 136 |
fun store_thm_open (b, th) = |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
137 |
enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single; |
3987 | 138 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
139 |
|
6091 | 140 |
(* add_thms(s) *) |
4853 | 141 |
|
29579 | 142 |
fun add_thms_atts pre_name ((b, thms), atts) = |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
143 |
enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms); |
4853 | 144 |
|
18377 | 145 |
fun gen_add_thmss pre_name = |
146 |
fold_map (add_thms_atts pre_name); |
|
5907 | 147 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
148 |
fun gen_add_thms pre_name args = |
18377 | 149 |
apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
150 |
|
33700 | 151 |
val add_thmss = gen_add_thmss (name_thms true true); |
152 |
val add_thms = gen_add_thms (name_thms true true); |
|
27683 | 153 |
val add_thm = yield_singleton add_thms; |
5907 | 154 |
|
155 |
||
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
156 |
(* add_thms_dynamic *) |
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
157 |
|
29579 | 158 |
fun add_thms_dynamic (b, f) thy = thy |
49010 | 159 |
|> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd); |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
160 |
|
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
161 |
|
27728 | 162 |
(* note_thmss *) |
5907 | 163 |
|
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
164 |
fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy => |
12711 | 165 |
let |
28965 | 166 |
val name = Sign.full_name thy b; |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
167 |
fun app (ths, atts) = |
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
168 |
fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; |
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
169 |
val (thms, thy') = |
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
170 |
enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app) |
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset
|
171 |
(b, facts) thy; |
28076 | 172 |
in ((name, thms), thy') end); |
12711 | 173 |
|
5280 | 174 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
175 |
(* store axioms as theorems *) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
176 |
|
4853 | 177 |
local |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
178 |
|
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
179 |
fun no_read _ (_, t) = t; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
180 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
41696
diff
changeset
|
181 |
fun read ctxt (b, str) = |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
41696
diff
changeset
|
182 |
Syntax.read_prop ctxt str handle ERROR msg => |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42379
diff
changeset
|
183 |
cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b); |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
184 |
|
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
185 |
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy => |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
186 |
let |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
41696
diff
changeset
|
187 |
val ctxt = Syntax.init_pretty_global thy; |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
41696
diff
changeset
|
188 |
val prop = prep ctxt (b, raw_prop); |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
41696
diff
changeset
|
189 |
val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy; |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
190 |
val thm = def |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
191 |
|> Thm.forall_intr_frees |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
192 |
|> Thm.forall_elim_vars 0 |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
193 |
|> Thm.varifyT_global; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
194 |
in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end); |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
195 |
|
4853 | 196 |
in |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
197 |
|
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
198 |
val add_defs = add no_read false; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
199 |
val add_defs_unchecked = add no_read true; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
200 |
val add_defs_cmd = add read false; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
201 |
val add_defs_unchecked_cmd = add read true; |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
202 |
|
4853 | 203 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
204 |
|
3987 | 205 |
end; |