- enter_thmx -> enter_thms
authorberghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998b14e7686ce84
parent 11997 402ae1a172ae
child 11999 43b4385445bf
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Wed Oct 31 19:32:05 2001 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Oct 31 19:37:04 2001 +0100
     1.3 @@ -223,23 +223,27 @@
     1.4  
     1.5  (* naming *)
     1.6  
     1.7 -fun gen_names len name =
     1.8 -  map (fn i => name ^ ":" ^ string_of_int i) (1 upto len);
     1.9 +fun gen_names j len name =
    1.10 +  map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len);
    1.11  
    1.12 -fun name_single name x = [(name, x)];
    1.13 -fun name_multi name xs = gen_names (length xs) name ~~ xs;
    1.14 +fun name_thm name [x] = [Thm.name_thm (name, x)];
    1.15 +fun name_multi name xs = gen_names 0 (length xs) name ~~ xs;
    1.16 +fun name_thms name xs = map Thm.name_thm (name_multi name xs);
    1.17 +fun name_thmss name = snd o foldl_map (fn (i, (ys, z)) => (i + length ys,
    1.18 +  (map Thm.name_thm (gen_names i (length ys) name ~~ ys), z))) o pair 0;
    1.19  
    1.20  
    1.21 -(* enter_thmx *)
    1.22 +(* enter_thms *)
    1.23  
    1.24  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
    1.25  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
    1.26  
    1.27 -fun enter_thmx _ _ app_name ("", thmx) = map snd (app_name "" thmx)
    1.28 -  | enter_thmx sg name_thm app_name (bname, thmx) =
    1.29 +fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms)
    1.30 +  | enter_thms sg pre_name post_name app_att thy (bname, thms) =
    1.31        let
    1.32          val name = Sign.full_name sg bname;
    1.33 -        val named_thms = map name_thm (app_name name thmx);
    1.34 +        val (thy', thms') = app_att (thy, pre_name name thms);
    1.35 +        val named_thms = post_name name thms';
    1.36  
    1.37          val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
    1.38  
    1.39 @@ -255,25 +259,26 @@
    1.40          val const_idx' =
    1.41            if overwrite then make_const_idx thms_tab'
    1.42            else foldl add_const_idx (const_idx, named_thms);
    1.43 -      in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; named_thms end;
    1.44 +      in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
    1.45 +        (thy', named_thms)
    1.46 +      end;
    1.47  
    1.48  
    1.49  (* add_thms(s) *)
    1.50  
    1.51 -fun add_thmx app_name app_att ((bname, thmx), atts) thy =
    1.52 -  let
    1.53 -    val (thy', thmx') = app_att ((thy, thmx), atts);
    1.54 -    val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm app_name (bname, thmx');
    1.55 -  in (thy', thms'') end;
    1.56 +fun add_thms' app_name ((bname, thms), atts) thy =
    1.57 +  enter_thms (Theory.sign_of thy) app_name app_name
    1.58 +    (Thm.applys_attributes o rpair atts) thy (bname, thms);
    1.59  
    1.60  fun add_thms args theory =
    1.61    (theory, args)
    1.62 -  |> foldl_map (fn (thy, arg) => add_thmx name_single Thm.apply_attributes arg thy)
    1.63 +  |> foldl_map (fn (thy, ((bname, thm), atts)) => add_thms' name_thm
    1.64 +       ((bname, [thm]), atts) thy)
    1.65    |> apsnd (map hd);
    1.66  
    1.67  fun add_thmss args theory =
    1.68    (theory, args)
    1.69 -  |> foldl_map (fn (thy, arg) => add_thmx name_multi Thm.applys_attributes arg thy);
    1.70 +  |> foldl_map (fn (thy, arg) => add_thms' name_thms arg thy);
    1.71  
    1.72  
    1.73  (* have_thmss *)
    1.74 @@ -282,11 +287,11 @@
    1.75    fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) =
    1.76      let
    1.77        fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
    1.78 -      val (thy', thmss') =
    1.79 -        foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts @ kind_atts)) ths_atts);
    1.80 -      val thms' = flat thmss';
    1.81 -      val thms'' = enter_thmx (Theory.sign_of thy') Thm.name_thm name_multi (bname, thms');
    1.82 -    in (thy', (bname, thms'')) end;
    1.83 +      val (thy', thms) = enter_thms (Theory.sign_of thy)
    1.84 +        name_thmss name_thms (apsnd flat o foldl_map app) thy
    1.85 +        (bname, map (fn (ths, atts) =>
    1.86 +          (ths, atts @ more_atts @ kind_atts)) ths_atts);
    1.87 +    in (thy', (bname, thms)) end;
    1.88  in
    1.89    fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args);
    1.90  end;
    1.91 @@ -294,25 +299,25 @@
    1.92  
    1.93  (* store_thm *)
    1.94  
    1.95 -fun store_thm th_atts thy =
    1.96 -  let val (thy', [th']) = add_thmx name_single Thm.apply_attributes th_atts thy
    1.97 +fun store_thm ((bname, thm), atts) thy =
    1.98 +  let val (thy', [th']) = add_thms' name_thm ((bname, [thm]), atts) thy
    1.99    in (thy', th') end;
   1.100  
   1.101  
   1.102  (* smart_store_thms *)
   1.103  
   1.104 -fun gen_smart_store_thms _ (name, []) =
   1.105 +fun gen_smart_store_thms _ _ (name, []) =
   1.106        error ("Cannot store empty list of theorems: " ^ quote name)
   1.107 -  | gen_smart_store_thms name_thm (name, [thm]) =
   1.108 -      enter_thmx (Thm.sign_of_thm thm) name_thm name_single (name, thm)
   1.109 -  | gen_smart_store_thms name_thm (name, thms) =
   1.110 +  | gen_smart_store_thms name_thm _ (name, [thm]) =
   1.111 +      snd (enter_thms (Thm.sign_of_thm thm) name_thm name_thm I () (name, [thm]))
   1.112 +  | gen_smart_store_thms _ name_thm (name, thms) =
   1.113        let
   1.114          val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
   1.115          val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
   1.116 -      in enter_thmx (Sign.deref sg_ref) name_thm name_multi (name, thms) end;
   1.117 +      in snd (enter_thms (Sign.deref sg_ref) name_thm name_thm I () (name, thms)) end;
   1.118  
   1.119 -val smart_store_thms = gen_smart_store_thms Thm.name_thm;
   1.120 -val open_smart_store_thms = gen_smart_store_thms snd;
   1.121 +val smart_store_thms = gen_smart_store_thms name_thm name_thms;
   1.122 +val open_smart_store_thms = gen_smart_store_thms (K I) (K I);
   1.123  
   1.124  
   1.125  (* forall_elim_vars (belongs to drule.ML) *)
   1.126 @@ -341,7 +346,7 @@
   1.127  
   1.128    fun add_single add (thy, ((name, ax), atts)) =
   1.129      let
   1.130 -      val named_ax = name_single name ax;
   1.131 +      val named_ax = [(name, ax)];
   1.132        val thy' = add named_ax thy;
   1.133        val thm = hd (get_axs thy' named_ax);
   1.134      in apsnd hd (add_thms [((name, thm), atts)] thy') end;