src/Pure/pure_thy.ML

--- a/src/Pure/pure_thy.ML	Fri Apr 03 14:36:20 1998 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 03 14:37:48 1998 +0200
@@ -2,7 +2,10 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Init 'theorems' data.  The Pure theories.
+The Pure theories.
+
+TODO:
+  - tagged axioms / defs;
 *)
 
 signature BASIC_PURE_THY =
@@ -15,9 +18,13 @@
 signature PURE_THY =
 sig
   include BASIC_PURE_THY
+  val get_tthm: theory -> xstring -> tthm
+  val get_tthms: theory -> xstring -> tthm list
   val thms_containing: theory -> string list -> (string * thm) list
   val store_thms: (bstring * thm) list -> theory -> theory
   val store_thmss: (bstring * thm list) list -> theory -> theory
+  val store_tthms: (bstring * tthm) list -> theory -> theory
+  val store_tthmss: (bstring * tthm list) list -> theory -> theory
   val smart_store_thm: (bstring * thm) -> thm
   val add_store_axioms: (bstring * string) list -> theory -> theory
   val add_store_axioms_i: (bstring * term) list -> theory -> theory
@@ -34,14 +41,14 @@
 
 (*** init theorems data ***)
 
-(** data kind theorems **)
+(** data kind 'theorems' **)
 
-val theoremsK = "theorems";
+val theoremsK = "Pure/theorems";
 
 exception Theorems of
  {space: NameSpace.T,
-  thms_tab: thm list Symtab.table,
-  const_idx: int * (int * thm) list Symtab.table} ref;
+  thms_tab: tthm list Symtab.table,
+  const_idx: int * (int * tthm) list Symtab.table} ref;
 
 
 (* methods *)
@@ -54,7 +61,7 @@
 
 fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) =
   let
-    val prt_thm = Pretty.quote o Display.pretty_thm o Thm.transfer_sg sg;
+    val prt_thm = Attribute.pretty_tthm o apfst (Thm.transfer_sg sg);
     fun prt_thms (name, [th]) =
           Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
       | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
@@ -69,9 +76,7 @@
 
 in
 
-val theorems_data: string * (object * (object -> object) *
-  (object * object -> object) * (Sign.sg -> object -> unit)) =
-    (theoremsK, (mk_empty (), mk_empty, mk_empty, print));
+val theorems_setup = Theory.init_data [(theoremsK, (mk_empty (), mk_empty, mk_empty, print))];
 
 end;
 
@@ -83,7 +88,7 @@
     Theorems r => r
   | _ => sys_error "get_theorems_sg");
 
-val get_theorems = get_theorems_sg o sign_of;
+val get_theorems = get_theorems_sg o Theory.sign_of;
 
 
 
@@ -102,22 +107,25 @@
       | some => some);
 
 
-(* get_thm(s) *)
+(* get_thms etc. *)
 
-fun get_thms thy name =
+fun get_tthms thy name =
   (case all_local_thms (thy :: Theory.ancestors_of thy) name of
     None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
   | Some thms => thms);
 
-fun get_thm thy name =
-  (case get_thms thy name of
+fun get_tthm thy name =
+  (case get_tthms thy name of
     [thm] => thm
   | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
 
+fun get_thms thy = map Attribute.thm_of o get_tthms thy;
+fun get_thm thy = Attribute.thm_of o get_tthm thy;
+
 
 (* thms_of *)
 
-fun attach_name thm = (Thm.name_of_thm thm, thm);
+fun attach_name (thm, _) = (Thm.name_of_thm thm, thm);
 
 fun thms_of thy =
   let val ref {thms_tab, ...} = get_theorems thy in
@@ -132,14 +140,14 @@
 
 val ignore = ["Trueprop", "all", "==>", "=="];
 
-fun add_const_idx ((next, table), thm) =
+fun add_const_idx ((next, table), tthm as (thm, _)) =
   let
     val {hyps, prop, ...} = Thm.rep_thm thm;
     val consts =
       foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
 
     fun add (tab, c) =
-      Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
+      Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab);
   in (next + 1, foldl add (table, consts)) end;
 
 fun make_const_idx thm_tab =
@@ -182,49 +190,52 @@
 fun warn_same name =
   warning ("Theorem database already contains a copy of " ^ quote name);
 
-fun enter_thms sg single (raw_name, thms) =
+fun enter_tthms sg single (raw_name, tthms) =
   let
-    val len = length thms;
+    val len = length tthms;
     val name = Sign.full_name sg raw_name;
     val names =
       if single then replicate len name
       else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1));
-    val named_thms = ListPair.map Thm.name_thm (names, thms);
+    val named_tthms = map2 (fn (x, (th, tg)) => (Thm.name_thm (x, th), tg)) (names, tthms);
 
-    val eq_thms = ListPair.all Thm.eq_thm;
+    fun eq_tthm ((th1, _), (th2, _)) = Thm.eq_thm (th1, th2);
 
     val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
 
     val overwrite =
       (case Symtab.lookup (thms_tab, name) of
         None => false
-      | Some thms' =>
-          if length thms' = len andalso eq_thms (thms', named_thms) then
+      | Some tthms' =>
+          if length tthms' = len andalso forall2 eq_tthm (tthms', named_tthms) then
             (warn_same name; false)
           else (warn_overwrite name; true));
 
     val space' = NameSpace.extend (space, [name]);
-    val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
+    val thms_tab' = Symtab.update ((name, named_tthms), thms_tab);
     val const_idx' =
       if overwrite then make_const_idx thms_tab'
-      else foldl add_const_idx (const_idx, named_thms);
+      else foldl add_const_idx (const_idx, named_tthms);
   in
     r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
-    named_thms
+    named_tthms
   end;
 
-fun do_enter_thms sg single thms = (enter_thms sg single thms; ());
+fun do_enter_tthms sg single tthms = (enter_tthms sg single tthms; ());
 
 
-fun store_thmss thmss thy =
-  (seq (do_enter_thms (sign_of thy) false) thmss; thy);
+fun store_tthmss tthmss thy =
+  (seq (do_enter_tthms (Theory.sign_of thy) false) tthmss; thy);
 
-fun store_thms thms thy =
-  (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
+fun store_tthms tthms thy =
+  (seq (do_enter_tthms (Theory.sign_of thy) true) (map (apsnd (fn th => [th])) tthms); thy);
+
+fun store_thmss thmss = store_tthmss (map (apsnd (map Attribute.tthm_of)) thmss);
+fun store_thms thms = store_tthms (map (apsnd Attribute.tthm_of) thms);
 
 fun smart_store_thm (name, thm) =
-  let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
-  in named_thm end;
+  let val [(thm', _)] = enter_tthms (Thm.sign_of_thm thm) true (name, [Attribute.tthm_of thm])
+  in thm' end;
 
 
 (* store axioms as theorems *)
@@ -246,7 +257,8 @@
 
 val proto_pure =
   Theory.pre_pure
-  |> Theory.init_data [theorems_data]
+  |> Attribute.setup
+  |> theorems_setup
   |> Theory.add_types
    (("fun", 2, NoSyn) ::
     ("prop", 0, NoSyn) ::