--- a/src/Pure/Thy/thm_database.ML Mon Oct 22 18:04:11 2001 +0200
+++ b/src/Pure/Thy/thm_database.ML Mon Oct 22 18:04:26 2001 +0200
@@ -1,29 +1,15 @@
(* Title: Pure/Thy/thm_database.ML
ID: $Id$
- Author: Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen
+ Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-User level interface to thm database (see also Pure/pure_thy.ML).
+Interface to thm database (see also Pure/pure_thy.ML).
*)
signature BASIC_THM_DATABASE =
sig
val store_thm: string * thm -> thm
val store_thms: string * thm list -> thm list
- val bind_thm: string * thm -> unit
- val bind_thms: string * thm list -> unit
- val qed: string -> unit
- 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 qed_spec_mp: string -> unit
- val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
- val qed_goalw_spec_mp: string -> theory -> thm list -> string
- -> (thm list -> tactic list) -> unit
- val no_qed: unit -> unit
- (*these peek at the proof state!*)
- val thms_containing: xstring list -> (string * thm) list
- val findI: int -> (string * thm) list
- val findEs: int -> (string * thm) list
- val findE: int -> int -> (string * thm) list
end;
signature THM_DATABASE =
@@ -34,6 +20,7 @@
val ml_store_thms: string * thm list -> unit
val is_ml_identifier: string -> bool
val ml_reserved: string list
+ val thms_containing: theory -> string list -> (string * thm) list
val print_thms_containing: theory -> term list -> unit
end;
@@ -87,35 +74,13 @@
else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
end;
-fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
-fun bind_thms (name, thms) = ml_store_thms (name, map standard thms);
-
-fun qed name = ml_store_thm (name, Goals.result ());
-fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
-fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
-fun qed_spec_mp name = ml_store_thm (name, ObjectLogic.rulify_no_asm (Goals.result ()));
-fun qed_goal_spec_mp name thy s p =
- bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
-fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
-
-fun no_qed () = ();
-
(** retrieve theorems **)
-fun thms_containing_thy thy consts = PureThy.thms_containing thy consts
+fun thms_containing thy consts = PureThy.thms_containing thy consts
handle THEORY (msg, _) => error msg | THM (msg, _, _) => error msg;
-fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()));
-
-fun thms_containing raw_consts =
- let
- val thy = theory_of_goal ();
- val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
- in thms_containing_thy thy consts end;
-
fun print_thms_containing thy ts =
let
val prt_const =
@@ -131,115 +96,11 @@
in
if Library.null cs andalso not (Library.null ts) then
warning "thms_containing: no constants in specification"
- else (header @ map prt_thm (thms_containing_thy thy cs)) |> Pretty.chunks |> Pretty.writeln
+ else (header @ map prt_thm (thms_containing thy cs)) |> Pretty.chunks |> Pretty.writeln
end;
-(*top_const: main constant, ignoring Trueprop*)
-fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
- | top_const _ = None;
-
-val intro_const = top_const o concl_of;
-
-fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
-
-(* In case faster access is necessary, the thm db should provide special
-functions
-
-index_intros, index_elims: string -> (string * thm) list
-
-where thm [| A1 ; ...; An |] ==> B is returned by
-- index_intros c if B is of the form c t1 ... tn
-- index_elims c if A1 is of the form c t1 ... tn
-*)
-
-(* could be provided by thm db *)
-fun index_intros c =
- let fun topc(_,thm) = intro_const thm = Some(c);
- val named_thms = thms_containing_thy (theory_of_goal ()) [c]
- in filter topc named_thms end;
-
-(* could be provided by thm db *)
-fun index_elims c =
- let fun topc(_,thm) = elim_const thm = Some(c);
- val named_thms = thms_containing_thy (theory_of_goal ()) [c]
- in filter topc named_thms end;
-
-(*assume that parameters have unique names; reverse them for substitution*)
-fun goal_params i =
- let val gi = getgoal i
- val rfrees = rev(map Free (Logic.strip_params gi))
- in (gi,rfrees) end;
-
-fun concl_of_goal i =
- let val (gi,rfrees) = goal_params i
- val B = Logic.strip_assums_concl gi
- in subst_bounds(rfrees,B) end;
-
-fun prems_of_goal i =
- let val (gi,rfrees) = goal_params i
- val As = Logic.strip_assums_hyp gi
- in map (fn A => subst_bounds(rfrees,A)) As end;
-
-(*returns all those named_thms whose subterm extracted by extract can be
- instantiated to obj; the list is sorted according to the number of premises
- and the size of the required substitution.*)
-fun select_match(obj, signobj, named_thms, extract) =
- let fun matches(prop, tsig) =
- case extract prop of
- None => false
- | Some pat => Pattern.matches tsig (pat, obj);
-
- fun substsize(prop, tsig) =
- let val Some pat = extract prop
- val (_,subst) = Pattern.match tsig (pat,obj)
- in foldl op+
- (0, map (fn (_,t) => size_of_term t) subst)
- end
-
- fun thm_ord ((p0,s0,_),(p1,s1,_)) =
- prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
-
- fun select((p as (_,thm))::named_thms, sels) =
- let val {prop, sign, ...} = rep_thm thm
- in select(named_thms,
- if Sign.subsig(sign, signobj) andalso
- matches(prop,#tsig(Sign.rep_sg signobj))
- then
- (nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
- else sels)
- end
- | select([],sels) = sels
-
- in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
-
-fun find_matching(prop,sign,index,extract) =
- (case top_const prop of
- Some c => select_match(prop,sign,index c,extract)
- | _ => []);
-
-fun find_intros(prop,sign) =
- find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
-
-fun find_elims sign prop =
- let fun major prop = case Logic.strip_imp_prems prop of
- [] => None | p::_ => Some p
- in find_matching(prop,sign,index_elims,major) end;
-
-fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
-
-fun findEs i =
- let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
- val sign = #sign(rep_thm(topthm()))
- val thmss = map (find_elims sign) (prems_of_goal i)
- in foldl (gen_union eq_nth) ([],thmss) end;
-
-fun findE i j =
- let val sign = #sign(rep_thm(topthm()))
- in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
-
end;
-
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
open BasicThmDatabase;