src/Pure/Thy/thm_database.ML
author wenzelm
Wed Sep 22 20:58:23 1999 +0200 (1999-09-22 ago)
changeset 7573 aa87cf5a15f5
parent 7446 f43d3670a3cd
child 7609 1acbed762fc6
permissions -rw-r--r--
ml_store_thm: no warning for "";
     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 end;
    33 
    34 structure ThmDatabase: THM_DATABASE =
    35 struct
    36 
    37 (** store theorems **)
    38 
    39 (* store in theory and generate HTML *)
    40 
    41 fun store_thm (name, thm) =
    42   let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
    43   in Present.theorem name thm'; thm' end;
    44 
    45 fun store_thms (name, thms) =
    46   let val thms' = PureThy.smart_store_thms (name, thms)
    47   in Present.theorems name thms'; thms' end;
    48 
    49 
    50 (* store on ML toplevel *)
    51 
    52 val qed_thms: thm list ref = ref [];
    53 
    54 val ml_reserved =
    55  ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    56   "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    57   "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    58   "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    59   "eqtype", "functor", "include", "sharing", "sig", "signature",
    60   "struct", "structure", "where"];
    61 
    62 fun is_ml_identifier name =
    63   Syntax.is_identifier name andalso not (name mem ml_reserved);
    64 
    65 fun warn_ml name =
    66   if is_ml_identifier name then false
    67   else if name = "" then true
    68   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
    69 
    70 fun ml_store_thm (name, thm) =
    71   let val thm' = store_thm (name, thm) in
    72     if warn_ml name then ()
    73     else (qed_thms := [thm]; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
    74   end;
    75 
    76 fun ml_store_thms (name, thms) =
    77   let val thms' = store_thms (name, thms) in
    78     if warn_ml name then ()
    79     else (qed_thms := thms; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    80   end;
    81 
    82 fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
    83 fun bind_thms (name, thms) = ml_store_thms (name, map standard thms);
    84 
    85 fun qed name = ml_store_thm (name, Goals.result ());
    86 fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
    87 fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
    88 
    89 fun no_qed () = ();
    90 
    91 
    92 
    93 (** retrieve theorems **)
    94 
    95 (*get theorems that contain all of given constants*)
    96 fun thms_containing raw_consts =
    97   let
    98     val sign = sign_of_thm (topthm ());
    99     val consts = map (Sign.intern_const sign) raw_consts;
   100     val thy = ThyInfo.theory_of_sign sign;
   101   in PureThy.thms_containing thy consts end
   102   handle THEORY (msg,_) => error msg;
   103 
   104 
   105 (*top_const: main constant, ignoring Trueprop*)
   106 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
   107   | top_const _ = None;
   108 
   109 val intro_const = top_const o concl_of;
   110 
   111 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
   112 
   113 (* In case faster access is necessary, the thm db should provide special
   114 functions
   115 
   116 index_intros, index_elims: string -> (string * thm) list
   117 
   118 where thm [| A1 ; ...; An |] ==> B is returned by
   119 - index_intros c if B  is of the form c t1 ... tn
   120 - index_elims c  if A1 is of the form c t1 ... tn
   121 *)
   122 
   123 (* could be provided by thm db *)
   124 fun index_intros c =
   125   let fun topc(_,thm) = intro_const thm = Some(c);
   126       val named_thms = thms_containing [c]
   127   in filter topc named_thms end;
   128 
   129 (* could be provided by thm db *)
   130 fun index_elims c =
   131   let fun topc(_,thm) = elim_const thm = Some(c);
   132       val named_thms = thms_containing [c]
   133   in filter topc named_thms end;
   134 
   135 (*assume that parameters have unique names*)
   136 fun goal_params i =
   137   let val gi = getgoal i
   138       val frees = map Free (Logic.strip_params gi)
   139   in (gi,frees) end;
   140 
   141 fun concl_of_goal i =
   142   let val (gi,frees) = goal_params i
   143       val B = Logic.strip_assums_concl gi
   144   in subst_bounds(frees,B) end;
   145 
   146 fun prems_of_goal i =
   147   let val (gi,frees) = goal_params i
   148       val As = Logic.strip_assums_hyp gi
   149   in map (fn A => subst_bounds(frees,A)) As end;
   150 
   151 (*returns all those named_thms whose subterm extracted by extract can be
   152   instantiated to obj; the list is sorted according to the number of premises
   153   and the size of the required substitution.*)
   154 fun select_match(obj, signobj, named_thms, extract) =
   155   let fun matches(prop, tsig) =
   156             case extract prop of
   157               None => false
   158             | Some pat => Pattern.matches tsig (pat, obj);
   159 
   160       fun substsize(prop, tsig) =
   161             let val Some pat = extract prop
   162                 val (_,subst) = Pattern.match tsig (pat,obj)
   163             in foldl op+
   164                 (0, map (fn (_,t) => size_of_term t) subst)
   165             end
   166 
   167       fun thm_ord ((p0,s0,_),(p1,s1,_)) =
   168             prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
   169 
   170       fun select((p as (_,thm))::named_thms, sels) =
   171             let val {prop, sign, ...} = rep_thm thm
   172             in select(named_thms,
   173                       if Sign.subsig(sign, signobj) andalso
   174                          matches(prop,#tsig(Sign.rep_sg signobj))
   175                       then
   176                         (nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
   177                       else sels)
   178             end
   179         | select([],sels) = sels
   180 
   181   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
   182 
   183 fun find_matching(prop,sign,index,extract) =
   184   (case top_const prop of
   185      Some c => select_match(prop,sign,index c,extract)
   186    | _      => []);
   187 
   188 fun find_intros(prop,sign) =
   189   find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
   190 
   191 fun find_elims sign prop =
   192   let fun major prop = case Logic.strip_imp_prems prop of
   193                          [] => None | p::_ => Some p
   194   in find_matching(prop,sign,index_elims,major) end;
   195 
   196 fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
   197 
   198 fun findEs i =
   199   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
   200       val sign = #sign(rep_thm(topthm()))
   201       val thmss = map (find_elims sign) (prems_of_goal i)
   202   in foldl (gen_union eq_nth) ([],thmss) end;
   203 
   204 fun findE i j =
   205   let val sign = #sign(rep_thm(topthm()))
   206   in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
   207 
   208 
   209 end;
   210 
   211 
   212 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
   213 open BasicThmDatabase;