# HG changeset patch # User wenzelm # Date 911308092 -3600 # Node ID 4b9f4e310891d69c44fd93c27ddc7171a5fe57d5 # Parent 1f58694fc3e227c594eaa4c6c271804a69fb6c68 added default_name; added have_tthmss; diff -r 1f58694fc3e2 -r 4b9f4e310891 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Nov 17 14:07:25 1998 +0100 +++ b/src/Pure/pure_thy.ML Tue Nov 17 14:08:12 1998 +0100 @@ -28,10 +28,13 @@ val get_tthms: theory -> xstring -> tthm list val get_tthmss: theory -> xstring list -> tthm list val thms_containing: theory -> string list -> (string * thm) list + val default_name: string -> string val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm val smart_store_thm: (bstring * thm) -> thm val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory + val have_tthmss: bstring -> theory attribute list -> + (tthm list * theory attribute list) list -> theory -> theory * tthm list val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory @@ -201,11 +204,13 @@ (* naming *) +val default_name = fn "" => "it" | name => name; + fun gen_names len name = map (fn i => name ^ "_" ^ string_of_int i) (1 upto len); -fun name_single name x = [(name, x)]; -fun name_multi name xs = gen_names (length xs) name ~~ xs; +fun name_single name x = [(default_name name, x)]; +fun name_multi name xs = gen_names (length xs) (default_name name) ~~ xs; (* enter_tthmx *) @@ -253,10 +258,21 @@ val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx'); in (thy', tthms'') end; -val add_tthms = - Theory.apply o map (fn th_atts => fst o add_tthmx name_single Attribute.apply th_atts); -val add_tthmss = - Theory.apply o map (fn th_atts => fst o add_tthmx name_multi Attribute.applys th_atts); +fun add_tthmxs name app = Library.apply o map (fst oo add_tthmx name app); + +val add_tthms = add_tthmxs name_single Attribute.apply; +val add_tthmss = add_tthmxs name_multi Attribute.applys; + + +(* have_tthmss *) + +fun have_tthmss bname more_atts ths_atts thy = + let + fun app (x, (ths, atts)) = Attribute.applys ((x, ths), atts); + val (thy', tthmss') = + foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts); + val tthms'' = enter_tthmx (Theory.sign_of thy') name_multi (bname, flat tthmss'); + in (thy, tthms'') end; (* store_tthm *) @@ -283,7 +299,7 @@ val tthms = map (Attribute.tthm_of o Thm.get_axiom thy' o fst) named_axs; in add_tthmss [((name, tthms), atts)] thy' end; - fun add_axs app_name add = Theory.apply o map (add_ax app_name add); + fun add_axs app_name add = Library.apply o map (add_ax app_name add); in val add_axioms = add_axs name_single Theory.add_axioms; val add_axioms_i = add_axs name_single Theory.add_axioms_i; @@ -390,7 +406,7 @@ val proto_pure = Theory.pre_pure - |> Theory.apply [TheoremsData.init, TheoryManagementData.init] + |> Library.apply [TheoremsData.init, TheoryManagementData.init] |> put_name "ProtoPure" |> global_path |> Theory.add_types