src/Pure/Thy/thm_database.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 8049 61eea7c23c5b
child 10894 ce58d2de6ea8
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
     1 (*  Title:      Pure/Thy/thm_database.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 User level interface to thm database (see also Pure/pure_thy.ML).
     6 *)
     7 
     8 signature BASIC_THM_DATABASE =
     9 sig
    10   val store_thm: string * thm -> thm
    11   val store_thms: string * thm list -> thm list
    12   val bind_thm: string * thm -> unit
    13   val bind_thms: string * thm list -> unit
    14   val qed: string -> unit
    15   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    16   val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit
    17   val no_qed: unit -> unit
    18   (*these peek at the proof state!*)
    19   val thms_containing: xstring list -> (string * thm) list
    20   val findI: int -> (string * thm) list
    21   val findEs: int -> (string * thm) list
    22   val findE: int -> int -> (string * thm) list
    23 end;
    24 
    25 signature THM_DATABASE =
    26 sig
    27   include BASIC_THM_DATABASE
    28   val qed_thms: thm list ref
    29   val ml_store_thm: string * thm -> unit
    30   val ml_store_thms: string * thm list -> unit
    31   val is_ml_identifier: string -> bool
    32   val print_thms_containing: theory -> xstring list -> unit
    33 end;
    34 
    35 structure ThmDatabase: THM_DATABASE =
    36 struct
    37 
    38 (** store theorems **)
    39 
    40 (* store in theory and generate HTML *)
    41 
    42 fun store_thm (name, thm) =
    43   let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
    44   in Present.theorem name thm'; thm' end;
    45 
    46 fun store_thms (name, thms) =
    47   let val thms' = PureThy.smart_store_thms (name, thms)
    48   in Present.theorems name thms'; thms' end;
    49 
    50 
    51 (* store on ML toplevel *)
    52 
    53 val qed_thms: thm list ref = ref [];
    54 
    55 val ml_reserved =
    56  ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    57   "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    58   "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    59   "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    60   "eqtype", "functor", "include", "sharing", "sig", "signature",
    61   "struct", "structure", "where"];
    62 
    63 fun is_ml_identifier name =
    64   Syntax.is_identifier name andalso not (name mem ml_reserved);
    65 
    66 fun warn_ml name =
    67   if is_ml_identifier name then false
    68   else if name = "" then true
    69   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
    70 
    71 val use_text_verbose = use_text writeln true;
    72 
    73 fun ml_store_thm (name, thm) =
    74   let val thm' = store_thm (name, thm) in
    75     if warn_ml name then ()
    76     else (qed_thms := [thm']; use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
    77   end;
    78 
    79 fun ml_store_thms (name, thms) =
    80   let val thms' = store_thms (name, thms) in
    81     if warn_ml name then ()
    82     else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    83   end;
    84 
    85 fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
    86 fun bind_thms (name, thms) = ml_store_thms (name, map standard thms);
    87 
    88 fun qed name = ml_store_thm (name, Goals.result ());
    89 fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
    90 fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
    91 
    92 fun no_qed () = ();
    93 
    94 
    95 
    96 (** retrieve theorems **)
    97 
    98 (*get theorems that contain all of given constants*)
    99 fun thms_containing_thy thy raw_consts =
   100   let val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
   101   in PureThy.thms_containing thy consts end
   102   handle THEORY (msg,_) => error msg;
   103 
   104 fun thms_containing cs =
   105   thms_containing_thy (ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()))) cs;
   106 
   107 fun prt_thm (a, th) =
   108   Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
   109     Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
   110 
   111 fun print_thms_containing thy cs =
   112   Pretty.writeln (Pretty.blk (0, Pretty.fbreaks (map prt_thm (thms_containing_thy thy cs))));
   113 
   114 
   115 (*top_const: main constant, ignoring Trueprop*)
   116 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
   117   | top_const _ = None;
   118 
   119 val intro_const = top_const o concl_of;
   120 
   121 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
   122 
   123 (* In case faster access is necessary, the thm db should provide special
   124 functions
   125 
   126 index_intros, index_elims: string -> (string * thm) list
   127 
   128 where thm [| A1 ; ...; An |] ==> B is returned by
   129 - index_intros c if B  is of the form c t1 ... tn
   130 - index_elims c  if A1 is of the form c t1 ... tn
   131 *)
   132 
   133 (* could be provided by thm db *)
   134 fun index_intros c =
   135   let fun topc(_,thm) = intro_const thm = Some(c);
   136       val named_thms = thms_containing [c]
   137   in filter topc named_thms end;
   138 
   139 (* could be provided by thm db *)
   140 fun index_elims c =
   141   let fun topc(_,thm) = elim_const thm = Some(c);
   142       val named_thms = thms_containing [c]
   143   in filter topc named_thms end;
   144 
   145 (*assume that parameters have unique names; reverse them for substitution*)
   146 fun goal_params i =
   147   let val gi = getgoal i
   148       val rfrees = rev(map Free (Logic.strip_params gi))
   149   in (gi,rfrees) end;
   150 
   151 fun concl_of_goal i =
   152   let val (gi,rfrees) = goal_params i
   153       val B = Logic.strip_assums_concl gi
   154   in subst_bounds(rfrees,B) end;
   155 
   156 fun prems_of_goal i =
   157   let val (gi,rfrees) = goal_params i
   158       val As = Logic.strip_assums_hyp gi
   159   in map (fn A => subst_bounds(rfrees,A)) As end;
   160 
   161 (*returns all those named_thms whose subterm extracted by extract can be
   162   instantiated to obj; the list is sorted according to the number of premises
   163   and the size of the required substitution.*)
   164 fun select_match(obj, signobj, named_thms, extract) =
   165   let fun matches(prop, tsig) =
   166             case extract prop of
   167               None => false
   168             | Some pat => Pattern.matches tsig (pat, obj);
   169 
   170       fun substsize(prop, tsig) =
   171             let val Some pat = extract prop
   172                 val (_,subst) = Pattern.match tsig (pat,obj)
   173             in foldl op+
   174                 (0, map (fn (_,t) => size_of_term t) subst)
   175             end
   176 
   177       fun thm_ord ((p0,s0,_),(p1,s1,_)) =
   178             prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
   179 
   180       fun select((p as (_,thm))::named_thms, sels) =
   181             let val {prop, sign, ...} = rep_thm thm
   182             in select(named_thms,
   183                       if Sign.subsig(sign, signobj) andalso
   184                          matches(prop,#tsig(Sign.rep_sg signobj))
   185                       then
   186                         (nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
   187                       else sels)
   188             end
   189         | select([],sels) = sels
   190 
   191   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
   192 
   193 fun find_matching(prop,sign,index,extract) =
   194   (case top_const prop of
   195      Some c => select_match(prop,sign,index c,extract)
   196    | _      => []);
   197 
   198 fun find_intros(prop,sign) =
   199   find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
   200 
   201 fun find_elims sign prop =
   202   let fun major prop = case Logic.strip_imp_prems prop of
   203                          [] => None | p::_ => Some p
   204   in find_matching(prop,sign,index_elims,major) end;
   205 
   206 fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
   207 
   208 fun findEs i =
   209   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
   210       val sign = #sign(rep_thm(topthm()))
   211       val thmss = map (find_elims sign) (prems_of_goal i)
   212   in foldl (gen_union eq_nth) ([],thmss) end;
   213 
   214 fun findE i j =
   215   let val sign = #sign(rep_thm(topthm()))
   216   in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
   217 
   218 
   219 end;
   220 
   221 
   222 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
   223 open BasicThmDatabase;