19 val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
19 val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
20 val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
20 val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
21 val burrow_facts: ('a list -> 'b list) -> |
21 val burrow_facts: ('a list -> 'b list) -> |
22 ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
22 ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
23 val name_multi: string -> 'a list -> (string * 'a) list |
23 val name_multi: string -> 'a list -> (string * 'a) list |
24 val name_thm: bool -> bool -> string -> thm -> thm |
24 type name_flags = {pre: bool, official: bool} |
25 val name_thms: bool -> bool -> string -> thm list -> thm list |
25 val official1: name_flags |
|
26 val official2: name_flags |
|
27 val unofficial1: name_flags |
|
28 val unofficial2: name_flags |
|
29 val name_thm: name_flags -> string -> thm -> thm |
|
30 val name_thms: name_flags -> string -> thm list -> thm list |
26 val check_thms_lazy: thm list lazy -> thm list lazy |
31 val check_thms_lazy: thm list lazy -> thm list lazy |
27 val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory |
32 val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory |
28 val store_thm: binding * thm -> theory -> thm * theory |
33 val store_thm: binding * thm -> theory -> thm * theory |
29 val store_thm_open: binding * thm -> theory -> thm * theory |
34 val store_thm_open: binding * thm -> theory -> thm * theory |
30 val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory |
35 val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory |
105 fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; |
110 fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; |
106 |
111 |
107 |
112 |
108 (* naming *) |
113 (* naming *) |
109 |
114 |
110 fun name_multi name [x] = [(name, x)] |
115 type name_flags = {pre: bool, official: bool}; |
111 | name_multi "" xs = map (pair "") xs |
116 |
112 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
117 val official1 : name_flags = {pre = true, official = true}; |
113 |
118 val official2 : name_flags = {pre = false, official = true}; |
114 fun name_thm pre official name thm = thm |
119 val unofficial1 : name_flags = {pre = true, official = false}; |
|
120 val unofficial2 : name_flags = {pre = false, official = false}; |
|
121 |
|
122 fun name_thm {pre, official} name thm = thm |
115 |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ? |
123 |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ? |
116 Thm.name_derivation name |
124 Thm.name_derivation name |
117 |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ? |
125 |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ? |
118 Thm.put_name_hint name; |
126 Thm.put_name_hint name; |
119 |
127 |
120 fun name_thms pre official name thms = |
128 |
121 map (uncurry (name_thm pre official)) (name_multi name thms); |
129 fun name_multi name [x] = [(name, x)] |
|
130 | name_multi "" xs = map (pair "") xs |
|
131 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
|
132 |
|
133 fun name_thms name_flags name thms = |
|
134 map (uncurry (name_thm name_flags)) (name_multi name thms); |
122 |
135 |
123 |
136 |
124 (* apply theorems and attributes *) |
137 (* apply theorems and attributes *) |
125 |
138 |
126 fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); |
139 fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); |
162 else |
175 else |
163 let |
176 let |
164 val name = Sign.full_name thy b; |
177 val name = Sign.full_name thy b; |
165 val thms' = |
178 val thms' = |
166 check_thms_lazy thms |
179 check_thms_lazy thms |
167 |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind)); |
180 |> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind)); |
168 in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end; |
181 in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end; |
169 |
182 |
170 val app_facts = |
183 val app_facts = |
171 apfst flat oo fold_map (fn (thms, atts) => fold_map (Thm.theory_attributes atts) thms); |
184 apfst flat oo fold_map (fn (thms, atts) => fold_map (Thm.theory_attributes atts) thms); |
172 |
185 |
183 |
196 |
184 |
197 |
185 (* store_thm *) |
198 (* store_thm *) |
186 |
199 |
187 fun store_thm (b, th) = |
200 fun store_thm (b, th) = |
188 apply_facts (name_thms true true) (name_thms false true) (b, [([th], [])]) #>> the_single; |
201 apply_facts (name_thms official1) (name_thms official2) (b, [([th], [])]) #>> the_single; |
189 |
202 |
190 fun store_thm_open (b, th) = |
203 fun store_thm_open (b, th) = |
191 apply_facts (name_thms true false) (name_thms false false) (b, [([th], [])]) #>> the_single; |
204 apply_facts (name_thms unofficial1) (name_thms unofficial2) (b, [([th], [])]) #>> the_single; |
192 |
205 |
193 |
206 |
194 (* add_thms(s) *) |
207 (* add_thms(s) *) |
195 |
208 |
196 fun add_thms_atts pre_name ((b, thms), atts) = |
209 fun add_thms_atts pre_name ((b, thms), atts) = |
197 apply_facts pre_name (name_thms false true) (b, [(thms, atts)]); |
210 apply_facts pre_name (name_thms official2) (b, [(thms, atts)]); |
198 |
211 |
199 fun gen_add_thmss pre_name = |
212 fun gen_add_thmss pre_name = |
200 fold_map (add_thms_atts pre_name); |
213 fold_map (add_thms_atts pre_name); |
201 |
214 |
202 fun gen_add_thms pre_name args = |
215 fun gen_add_thms pre_name args = |
203 apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
216 apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
204 |
217 |
205 val add_thmss = gen_add_thmss (name_thms true true); |
218 val add_thmss = gen_add_thmss (name_thms official1); |
206 val add_thms = gen_add_thms (name_thms true true); |
219 val add_thms = gen_add_thms (name_thms official1); |
207 val add_thm = yield_singleton add_thms; |
220 val add_thm = yield_singleton add_thms; |
208 |
221 |
209 |
222 |
210 (* dynamic theorems *) |
223 (* dynamic theorems *) |
211 |
224 |
221 |
234 |
222 fun note_thms kind ((b, more_atts), facts) thy = |
235 fun note_thms kind ((b, more_atts), facts) thy = |
223 let |
236 let |
224 val name = Sign.full_name thy b; |
237 val name = Sign.full_name thy b; |
225 val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts))); |
238 val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts))); |
226 val (thms', thy') = thy |> apply_facts (name_thms true true) (name_thms false true) (b, facts'); |
239 val (thms', thy') = thy |> apply_facts (name_thms official1) (name_thms official2) (b, facts'); |
227 in ((name, thms'), thy') end; |
240 in ((name, thms'), thy') end; |
228 |
241 |
229 val note_thmss = fold_map o note_thms; |
242 val note_thmss = fold_map o note_thms; |
230 |
243 |
231 |
244 |