added theorem database which contains axioms and theorems indexed by the
constants they contain

--- a/src/Pure/Thy/ROOT.ML	Sun May 28 17:18:06 1995 +0200
+++ b/src/Pure/Thy/ROOT.ML	Mon May 29 13:55:06 1995 +0200
@@ -13,22 +13,21 @@
 structure ThyParse = ThyParseFun(structure Symtab = Symtab
   and ThyScan = ThyScan);
 
-(* hide functors; saves space in PolyML *)
-functor ThyScanFun() = struct end;
-functor ThyParseFun() = struct end;
-
 use "thy_syn.ML";
+use "thm_database.ML";
 use "thy_read.ML";
 
 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
-structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
-open Readthy;
 
-(* Do not hide ThySynFun and ReadthyFUN; they are still used *)
+(* hide functors; saves space in PolyML *)
+functor ThyScanFun() = struct end;
+functor ThyParseFun() = struct end;
+functor ThySynFun() = struct end;
 
 fun init_thy_reader () =
   use_string
-   ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",
-    "Readthy.loaded_thys := ! loaded_thys;",
-    "open Readthy;"];
-
+   ["structure ThmDB = \
+    \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);",
+    "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
+                                   \and ThmDB = ThmDB);",
+    "open Readthy ThmDB;"];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thm_database.ML	Mon May 29 13:55:06 1995 +0200
@@ -0,0 +1,82 @@
+(*  Title:      Pure/Thy/thm_database.ML
+    ID:         $Id$
+    Author:     Carsten Clasohm
+    Copyright   1995 TU Muenchen
+*)
+
+signature THMDB =
+sig
+  val thm_db: (int * (string * thm)) list Symtab.table ref
+  val thm_num: int ref
+  val store_thm_db: string * thm -> thm
+  val thms_containing: string list -> (string * thm) list
+end;
+
+
+functor ThmdbFUN(val ignore: string list): THMDB =
+               (*ignore: constants that must not be used for theorem indexing*)
+struct
+
+(*Symtab which associates a constant with a list of theorems that contain the
+  constant (theorems are represented as numbers)*)
+val thm_db =
+      ref (Symtab.make ([] : (string * ((int * (string * thm)) list)) list));
+val thm_num = ref 0;                                 (*number of next theorem*)
+
+(*list all relevant constants a theorem contains*)
+fun list_consts t =
+  let val {prop, hyps, ...} = rep_thm t;
+
+      fun consts (Const (c, _)) = if c mem ignore then [] else [c]
+        | consts (Free _) = []
+        | consts (Var _) = []
+        | consts (Bound _) = []
+        | consts (Abs (_, _, t)) = consts t
+        | consts (t1$t2) = (consts t1) union (consts t2);
+  in distinct (flat (map consts (prop :: hyps))) end;
+
+(*store a theorem in database*)
+fun store_thm_db (thm as (name, t)) =
+  let val consts = list_consts t;
+
+      val tagged_thm = (!thm_num + 1, thm);
+
+      fun update_db [] = ()
+        | update_db (c :: cs) =
+            let val old_thms = Symtab.lookup_multi (!thm_db, c);
+            in thm_db := Symtab.update ((c, tagged_thm :: old_thms), !thm_db);
+               update_db cs
+            end;
+  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
+                                  " cannot be stored in ThmDB because it \
+                                  \contains no constants.")
+                    else ();
+     update_db consts;
+     thm_num := !thm_num+1;
+     t
+  end;
+
+(*intersection of two descending theorem lists*)
+infix desc_inter;
+fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
+  | xs desc_inter [] = []
+  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
+      if xi = yi then x :: (xs desc_inter ys)
+      else if xi > yi then xs desc_inter yss
+      else xss desc_inter ys;
+
+(*get all theorems from database that contain a list of constants*)
+fun thms_containing constants =
+  let fun collect [] _ result = map snd result
+        | collect (c :: cs) first result =
+            let val new_thms = Symtab.lookup_multi (!thm_db, c);
+            in collect cs false (if first then new_thms
+                                          else (result desc_inter new_thms))
+            end;
+
+      val ignored = constants inter ignore;
+  in if null ignored then () else
+       error ("The following constant(s) must not be used for searching the \
+              \theorem database:\n  " ^ commas (map quote ignored));
+     collect constants true [] end;
+end;

--- a/src/Pure/Thy/thy_read.ML	Sun May 28 17:18:06 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Mon May 29 13:55:06 1995 +0200
@@ -51,8 +51,9 @@
 end;
 
 
-functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
+functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
 struct
+local open ThmDB in
 
 datatype basetype = Thy  of string
                   | File of string;
@@ -284,7 +285,8 @@
          else (writeln ("Reading \"" ^ name ^ ".ML\"");
                use ml_file);
 
-         use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
+         use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");",
+                     "map store_thm_db (axioms_of " ^ tname ^ ".thy);"];
                     (*Store theory again because it could have been redefined*)
 
          (*Now set the correct info*)
@@ -441,7 +443,7 @@
         merge_thy_list mk_draft (map get_theory mergelist) end;
 
 (*Change theory object for an existent item of loaded_thys
-  or create a new item *)
+  or create a new item; also store axioms in Thm database*)
 fun store_theory (thy, tname) =
   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
                Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) =>
@@ -451,8 +453,8 @@
              | None => ThyInfo {path = "", children = [],
                                 thy_time = None, ml_time = None,
                                 theory = Some thy, thms = Symtab.null};
-  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
-
+  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
+  end;
 
 
 (** store and retrieve theorems **)
@@ -506,7 +508,7 @@
      ((thy_name, ThyInfo {path = path, children = children,
        thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}),
       ! loaded_thys);
-    thm
+    store_thm_db (name, thm)
   end;
 
 (*Store result of proof in loaded_thys and as ML value*)
@@ -578,5 +580,5 @@
 
 fun print_theory thy = (Drule.print_theory thy; print_thms thy);
 
-
+end
 end;