# 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;