# HG changeset patch
# User berghofe
# Date 870819514 -7200
# Node ID 43c7912aac8d825b26a699f86b5c204637565c34
# Parent  5366dde08dbaf44578ac71b08e97b160efb9e9e1
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.

diff -r 5366dde08dba -r 43c7912aac8d src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Aug 06 00:15:14 1997 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Aug 06 00:18:34 1997 +0200
@@ -23,11 +23,27 @@
   val findI:         int -> (string * thm)list
   val findEs:        int -> (string * thm)list
   val findE:  int -> int -> (string * thm)list
+
+  val store_thm      : string * thm -> thm
+  val bind_thm       : string * thm -> unit
+  val qed            : string -> unit
+  val qed_thm        : thm ref
+  val qed_goal       : string -> theory -> string 
+                       -> (thm list -> tactic list) -> unit
+  val qed_goalw      : string -> theory -> thm list -> string 
+                       -> (thm list -> tactic list) -> unit
+  val get_thm        : theory -> string -> thm
+  val thms_of        : theory -> (string * thm) list
+  val delete_thms    : string -> unit
+
+  val print_theory   : theory -> unit
   end;
 
-functor ThmDBFun(): THMDB =
+structure ThmDB: THMDB =
 struct
 
+open ThyInfo BrowserInfo;
+
 (*** ignore and top_const could be turned into functor-parameters, but are
 currently identical for all object logics ***)
 
@@ -248,4 +264,131 @@
   let val sign = #sign(rep_thm(topthm()))
   in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
 
+
+(*** Store and retrieve theorems ***)
+
+(** Store theorems **)
+
+(*Store a theorem in the thy_info of its theory,
+  and in the theory's HTML file*)
+fun store_thm (name, thm) =
+  let
+    val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
+                            theory, thms, methods, data}) =
+      thyinfo_of_sign (#sign (rep_thm thm))
+
+    val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
+      handle Symtab.DUPLICATE s => 
+        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
+           (warning ("Theory database already contains copy of\
+                     \ theorem " ^ quote name);
+            (thms, true))
+         else error ("Duplicate theorem name " ^ quote s
+                     ^ " used in theory database"));
+
+    (*Label this theorem*)
+    val thm' = Thm.name_thm (name, thm)
+  in
+    loaded_thys := Symtab.update
+     ((thy_name, ThyInfo {path = path, children = children, parents = parents,
+                          thy_time = thy_time, ml_time = ml_time,
+                          theory = theory, thms = thms',
+                          methods = methods, data = data}),
+      !loaded_thys);
+    thm_to_html thm name;
+    if duplicate then thm' else store_thm_db (name, thm')
+  end;
+
+
+(*Store result of proof in loaded_thys and as ML value*)
+
+val qed_thm = ref flexpair_def(*dummy*);
+
+
+fun bind_thm (name, thm) =
+ (qed_thm := store_thm (name, (standard thm));
+  use_string ["val " ^ name ^ " = !qed_thm;"]);
+
+
+fun qed name =
+ (qed_thm := store_thm (name, result ());
+  use_string ["val " ^ name ^ " = !qed_thm;"]);
+
+
+fun qed_goal name thy agoal tacsf =
+ (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
+  use_string ["val " ^ name ^ " = !qed_thm;"]);
+
+
+fun qed_goalw name thy rths agoal tacsf =
+ (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
+  use_string ["val " ^ name ^ " = !qed_thm;"]);
+
+
+(** Retrieve theorems **)
+
+(*Get all theorems belonging to a given theory*)
+fun thmtab_of_thy thy =
+  let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
+  in thms end;
+
+
+fun thmtab_of_name name =
+  let val ThyInfo {thms, ...} = the (get_thyinfo name);
+  in thms end;
+
+
+(*Get a stored theorem specified by theory and name. *)
+fun get_thm thy name =
+  let fun get [] [] searched =
+           raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
+        | get [] ng searched =
+            get (ng \\ searched) [] searched
+        | get (t::ts) ng searched =
+            (case Symtab.lookup (thmtab_of_name t, name) of
+                 Some thm => thm
+               | None => get ts (ng union (parents_of_name t)) (t::searched));
+
+      val (tname, _) = thyinfo_of_sign (sign_of thy);
+  in get [tname] [] [] end;
+
+
+(*Get stored theorems of a theory (original derivations) *)
+val thms_of = Symtab.dest o thmtab_of_thy;
+
+
+(*Remove theorems associated with a theory from theory and theorem database*)
+fun delete_thms tname =
+  let
+    val tinfo = case get_thyinfo tname of
+        Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
+                       methods, data, ...}) =>
+          ThyInfo {path = path, children = children, parents = parents,
+                   thy_time = thy_time, ml_time = ml_time,
+                   theory = theory, thms = Symtab.null,
+                   methods = methods, data = data}
+      | None => error ("Theory " ^ tname ^ " not stored by loader");
+
+    val ThyInfo {theory, ...} = tinfo;
+  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
+     case theory of
+         Some t => delete_thm_db t
+       | None => ()
+  end;
+
+
+(*** Print theory ***)
+
+fun print_thms thy =
+  let
+    val thms = thms_of thy;
+    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
+      Pretty.quote (pretty_thm th)];
+  in
+    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
+  end;
+
+
+fun print_theory thy = (Display.print_theory thy; print_thms thy);
+
 end;