# HG changeset patch # User berghofe # Date 1004553424 -3600 # Node ID b14e7686ce843ddb94c41eae08db031229ab0741 # Parent 402ae1a172aed66804bfd35fd2ec5042274dee36 - enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments diff -r 402ae1a172ae -r b14e7686ce84 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Oct 31 19:32:05 2001 +0100 +++ b/src/Pure/pure_thy.ML Wed Oct 31 19:37:04 2001 +0100 @@ -223,23 +223,27 @@ (* naming *) -fun gen_names len name = - map (fn i => name ^ ":" ^ string_of_int i) (1 upto len); +fun gen_names j len name = + map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len); -fun name_single name x = [(name, x)]; -fun name_multi name xs = gen_names (length xs) name ~~ xs; +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; -(* enter_thmx *) +(* enter_thms *) fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); -fun enter_thmx _ _ app_name ("", thmx) = map snd (app_name "" thmx) - | enter_thmx sg name_thm app_name (bname, thmx) = +fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms) + | enter_thms sg pre_name post_name app_att thy (bname, thms) = let val name = Sign.full_name sg bname; - val named_thms = map name_thm (app_name name thmx); + val (thy', thms') = app_att (thy, pre_name name thms); + val named_thms = post_name name thms'; val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg; @@ -255,25 +259,26 @@ val const_idx' = if overwrite then make_const_idx thms_tab' else foldl add_const_idx (const_idx, named_thms); - in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; named_thms end; + in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; + (thy', named_thms) + end; (* add_thms(s) *) -fun add_thmx app_name app_att ((bname, thmx), atts) thy = - let - val (thy', thmx') = app_att ((thy, thmx), atts); - val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm app_name (bname, thmx'); - in (thy', thms'') end; +fun add_thms' app_name ((bname, thms), atts) thy = + enter_thms (Theory.sign_of thy) app_name app_name + (Thm.applys_attributes o rpair atts) thy (bname, thms); fun add_thms args theory = (theory, args) - |> foldl_map (fn (thy, arg) => add_thmx name_single Thm.apply_attributes arg thy) + |> foldl_map (fn (thy, ((bname, thm), atts)) => add_thms' name_thm + ((bname, [thm]), atts) thy) |> apsnd (map hd); fun add_thmss args theory = (theory, args) - |> foldl_map (fn (thy, arg) => add_thmx name_multi Thm.applys_attributes arg thy); + |> foldl_map (fn (thy, arg) => add_thms' name_thms arg thy); (* have_thmss *) @@ -282,11 +287,11 @@ fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) = let fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); - val (thy', thmss') = - foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts @ kind_atts)) ths_atts); - val thms' = flat thmss'; - val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm name_multi (bname, thms'); - in (thy', (bname, thms'')) end; + val (thy', thms) = enter_thms (Theory.sign_of thy) + name_thmss name_thms (apsnd flat o foldl_map app) thy + (bname, map (fn (ths, atts) => + (ths, atts @ more_atts @ kind_atts)) ths_atts); + in (thy', (bname, thms)) end; in fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args); end; @@ -294,25 +299,25 @@ (* store_thm *) -fun store_thm th_atts thy = - let val (thy', [th']) = add_thmx name_single Thm.apply_attributes th_atts thy +fun store_thm ((bname, thm), atts) thy = + let val (thy', [th']) = add_thms' name_thm ((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]) = - enter_thmx (Thm.sign_of_thm thm) name_thm name_single (name, thm) - | gen_smart_store_thms name_thm (name, thms) = + | 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) = 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 enter_thmx (Sign.deref sg_ref) name_thm name_multi (name, thms) end; + in snd (enter_thms (Sign.deref sg_ref) name_thm name_thm I () (name, thms)) end; -val smart_store_thms = gen_smart_store_thms Thm.name_thm; -val open_smart_store_thms = gen_smart_store_thms snd; +val smart_store_thms = gen_smart_store_thms name_thm name_thms; +val open_smart_store_thms = gen_smart_store_thms (K I) (K I); (* forall_elim_vars (belongs to drule.ML) *) @@ -341,7 +346,7 @@ fun add_single add (thy, ((name, ax), atts)) = let - val named_ax = name_single name ax; + 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;