# HG changeset patch # User wenzelm # Date 1003766666 -7200 # Node ID 73b2c277974fee75ed34fe57983ef7173974bc00 # Parent 39a3ece437723c6350f4f2fcbd668f115bfdfab1 moved goal related stuff to goals.ML; diff -r 39a3ece43772 -r 73b2c277974f src/Pure/Thy/thm_database.ML --- 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;