# HG changeset patch # User berghofe # Date 1006187889 -3600 # Node ID 5fa04fc9b254e355beb68139884d60eb4b3de5d8 # Parent 9d86f1cd2969ead628c351312957d562fd14912f Further restructuring of theorem naming functions. diff -r 9d86f1cd2969 -r 5fa04fc9b254 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Nov 19 17:36:40 2001 +0100 +++ b/src/Pure/pure_thy.ML Mon Nov 19 17:38:09 2001 +0100 @@ -227,11 +227,15 @@ fun gen_names j len name = map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len); -fun name_thm name [x] = [Thm.name_thm (name, x)]; fun name_multi name xs = gen_names 0 (length xs) name ~~ xs; -fun name_thms name xs = map Thm.name_thm (name_multi name xs); -fun name_thmss name = snd o foldl_map (fn (i, (ys, z)) => (i + length ys, - (map Thm.name_thm (gen_names i (length ys) name ~~ ys), z))) o pair 0; + +fun name_thms name [x] = [Thm.name_thm (name, x)] + | name_thms name xs = map Thm.name_thm (name_multi name xs); + +fun name_thmss name xs = (case filter_out (null o fst) xs of + [([x], z)] => [([Thm.name_thm (name, x)], z)] + | _ => snd (foldl_map (fn (i, (ys, z)) => (i + length ys, + (map Thm.name_thm (gen_names i (length ys) name ~~ ys), z))) (0, xs))); (* enter_thms *) @@ -267,19 +271,18 @@ (* add_thms(s) *) -fun add_thms' app_name ((bname, thms), atts) thy = - enter_thms (Theory.sign_of thy) app_name app_name +fun add_thms_atts pre_name ((bname, thms), atts) thy = + enter_thms (Theory.sign_of thy) pre_name name_thms (Thm.applys_attributes o rpair atts) thy (bname, thms); -fun add_thms args theory = - (theory, args) - |> foldl_map (fn (thy, ((bname, thm), atts)) => add_thms' name_thm - ((bname, [thm]), atts) thy) - |> apsnd (map hd); +fun gen_add_thmss pre_name args theory = + foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args); -fun add_thmss args theory = - (theory, args) - |> foldl_map (fn (thy, arg) => add_thms' name_thms arg thy); +fun gen_add_thms pre_name args = + apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); + +val add_thmss = gen_add_thmss name_thms; +val add_thms = gen_add_thms name_thms; (* have_thmss *) @@ -301,24 +304,24 @@ (* store_thm *) fun store_thm ((bname, thm), atts) thy = - let val (thy', [th']) = add_thms' name_thm ((bname, [thm]), atts) thy + let val (thy', [th']) = add_thms_atts name_thms ((bname, [thm]), atts) thy in (thy', th') end; (* smart_store_thms *) -fun gen_smart_store_thms _ _ (name, []) = +fun gen_smart_store_thms _ (name, []) = error ("Cannot store empty list of theorems: " ^ quote name) - | gen_smart_store_thms name_thm _ (name, [thm]) = + | gen_smart_store_thms name_thm (name, [thm]) = snd (enter_thms (Thm.sign_of_thm thm) name_thm name_thm I () (name, [thm])) - | gen_smart_store_thms _ name_thm (name, thms) = + | gen_smart_store_thms name_thm (name, thms) = let val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm); val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms); in snd (enter_thms (Sign.deref sg_ref) name_thm name_thm I () (name, thms)) end; -val smart_store_thms = gen_smart_store_thms name_thm name_thms; -val smart_store_thms_open = gen_smart_store_thms (K I) (K I); +val smart_store_thms = gen_smart_store_thms name_thms; +val smart_store_thms_open = gen_smart_store_thms (K I); (* forall_elim_vars (belongs to drule.ML) *) @@ -350,14 +353,14 @@ val named_ax = [(name, ax)]; val thy' = add named_ax thy; val thm = hd (get_axs thy' named_ax); - in apsnd hd (add_thms [((name, thm), atts)] thy') end; + in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end; fun add_multi add (thy, ((name, axs), atts)) = let val named_axs = name_multi name axs; val thy' = add named_axs thy; val thms = get_axs thy' named_axs; - in apsnd hd (add_thmss [((name, thms), atts)] thy') end; + in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; fun add_singles add args thy = foldl_map (add_single add) (thy, args); fun add_multis add args thy = foldl_map (add_multi add) (thy, args);