28 val thms_containing: theory -> string list -> (string * thm) list |
28 val thms_containing: theory -> string list -> (string * thm) list |
29 val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm |
29 val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm |
30 val smart_store_thms: (bstring * thm list) -> thm list |
30 val smart_store_thms: (bstring * thm list) -> thm list |
31 val forall_elim_var: int -> thm -> thm |
31 val forall_elim_var: int -> thm -> thm |
32 val forall_elim_vars: int -> thm -> thm |
32 val forall_elim_vars: int -> thm -> thm |
33 val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory |
33 val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list |
34 val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory |
34 val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list |
35 val have_thmss: bstring -> theory attribute list -> |
35 val have_thmss: bstring -> theory attribute list -> |
36 (thm list * theory attribute list) list -> theory -> theory * thm list |
36 (thm list * theory attribute list) list -> theory -> theory * thm list |
37 val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory |
37 val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list |
38 val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory |
38 val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list |
39 val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory |
39 val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list |
40 val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory |
40 val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list |
41 val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory |
41 val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list |
42 val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory |
42 val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list |
43 val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory |
43 val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list |
44 val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory |
44 val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list |
45 val get_name: theory -> string |
45 val get_name: theory -> string |
46 val put_name: string -> theory -> theory |
46 val put_name: string -> theory -> theory |
47 val global_path: theory -> theory |
47 val global_path: theory -> theory |
48 val local_path: theory -> theory |
48 val local_path: theory -> theory |
49 val begin_theory: string -> theory list -> theory |
49 val begin_theory: string -> theory list -> theory |
230 let |
230 let |
231 val (thy', thmx') = app_att ((thy, thmx), atts); |
231 val (thy', thmx') = app_att ((thy, thmx), atts); |
232 val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx'); |
232 val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx'); |
233 in (thy', thms'') end; |
233 in (thy', thms'') end; |
234 |
234 |
235 fun add_thmxs name app = Library.apply o map (fst oo add_thmx name app); |
235 fun add_thms args theory = |
236 |
236 (theory, args) |
237 val add_thms = add_thmxs name_single Thm.apply_attributes; |
237 |> foldl_map (fn (thy, arg) => add_thmx name_single Thm.apply_attributes arg thy) |
238 val add_thmss = add_thmxs name_multi Thm.applys_attributes; |
238 |> apsnd (map hd); |
|
239 |
|
240 fun add_thmss args theory = |
|
241 (theory, args) |
|
242 |> foldl_map (fn (thy, arg) => add_thmx name_multi Thm.applys_attributes arg thy); |
239 |
243 |
240 |
244 |
241 (* have_thmss *) |
245 (* have_thmss *) |
242 |
246 |
243 fun have_thmss bname more_atts ths_atts thy = |
247 fun have_thmss bname more_atts ths_atts thy = |
290 |
294 |
291 local |
295 local |
292 fun get_axs thy named_axs = |
296 fun get_axs thy named_axs = |
293 map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs; |
297 map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs; |
294 |
298 |
295 fun add_single add ((name, ax), atts) thy = |
299 fun add_single add (thy, ((name, ax), atts)) = |
296 let |
300 let |
297 val named_ax = name_single name ax; |
301 val named_ax = name_single name ax; |
298 val thy' = add named_ax thy; |
302 val thy' = add named_ax thy; |
299 val thm = hd (get_axs thy' named_ax); |
303 val thm = hd (get_axs thy' named_ax); |
300 in add_thms [((name, thm), atts)] thy' end; |
304 in apsnd hd (add_thms [((name, thm), atts)] thy') end; |
301 |
305 |
302 fun add_multi add ((name, axs), atts) thy = |
306 fun add_multi add (thy, ((name, axs), atts)) = |
303 let |
307 let |
304 val named_axs = name_multi name axs; |
308 val named_axs = name_multi name axs; |
305 val thy' = add named_axs thy; |
309 val thy' = add named_axs thy; |
306 val thms = get_axs thy' named_axs; |
310 val thms = get_axs thy' named_axs; |
307 in add_thmss [((name, thms), atts)] thy' end; |
311 in apsnd hd (add_thmss [((name, thms), atts)] thy') end; |
308 |
312 |
309 fun add_singles add = Library.apply o map (add_single add); |
313 fun add_singles add args thy = foldl_map (add_single add) (thy, args); |
310 fun add_multis add = Library.apply o map (add_multi add); |
314 fun add_multis add args thy = foldl_map (add_multi add) (thy, args); |
311 in |
315 in |
312 val add_axioms = add_singles Theory.add_axioms; |
316 val add_axioms = add_singles Theory.add_axioms; |
313 val add_axioms_i = add_singles Theory.add_axioms_i; |
317 val add_axioms_i = add_singles Theory.add_axioms_i; |
314 val add_axiomss = add_multis Theory.add_axioms; |
318 val add_axiomss = add_multis Theory.add_axioms; |
315 val add_axiomss_i = add_multis Theory.add_axioms_i; |
319 val add_axiomss_i = add_multis Theory.add_axioms_i; |
439 ("TYPE", "'a itself", NoSyn), |
443 ("TYPE", "'a itself", NoSyn), |
440 (dummy_patternN, "'a", Delimfix "'_")] |
444 (dummy_patternN, "'a", Delimfix "'_")] |
441 |> Theory.add_modesyntax ("", false) |
445 |> Theory.add_modesyntax ("", false) |
442 [("Goal", "prop => prop", Mixfix ("_", [0], 0))] |
446 [("Goal", "prop => prop", Mixfix ("_", [0], 0))] |
443 |> local_path |
447 |> local_path |
444 |> (add_defs o map Thm.no_attributes) |
448 |> (#1 oo (add_defs o map Thm.no_attributes)) |
445 [("flexpair_def", "(t =?= u) == (t == u::'a::{})"), |
449 [("flexpair_def", "(t =?= u) == (t == u::'a::{})"), |
446 ("Goal_def", "GOAL (PROP A) == PROP A")] |
450 ("Goal_def", "GOAL (PROP A) == PROP A")] |
447 |> end_theory; |
451 |> end_theory; |
448 |
452 |
449 structure ProtoPure = |
453 structure ProtoPure = |