src/Pure/Thy/thm_database.ML
author paulson
Thu Aug 20 09:25:59 1998 +0200 (1998-08-20)
changeset 5346 bc9748ad8491
parent 5155 21177b8a4d7f
child 5744 9e73738f2307
permissions -rw-r--r--
Now qed_spec_mp respects locales, by calling ml_store_thm
instead of bind_thm
     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 THM_DATABASE =
     9 sig
    10   val ml_store_thm: string * thm -> unit
    11   val store_thm: string * thm -> thm
    12   val qed_thm: thm option ref
    13   val bind_thm: string * thm -> 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   (*these peek at the proof state!*)
    18   val thms_containing: xstring list -> (string * thm) list
    19   val findI: int -> (string * thm) list
    20   val findEs: int -> (string * thm) list
    21   val findE: int -> int -> (string * thm) list
    22 end;
    23 
    24 structure ThmDatabase: THM_DATABASE =
    25 struct
    26 
    27 (** store theorems **)
    28 
    29 (* store in theory and generate HTML *)
    30 
    31 fun store_thm (name, thm) =
    32   let val thm' = PureThy.smart_store_thm (name, thm) in
    33     BrowserInfo.thm_to_html thm' name; thm'
    34   end;
    35 
    36 
    37 (* store on ML toplevel *)
    38 
    39 val qed_thm: thm option ref = ref None;
    40 
    41 val ml_reserved =
    42  ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    43   "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    44   "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    45   "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    46   "eqtype", "functor", "include", "sharing", "sig", "signature",
    47   "struct", "structure", "where"];
    48 
    49 fun is_ml_identifier name =
    50   Syntax.is_identifier name andalso not (name mem ml_reserved);
    51 
    52 fun ml_store_thm (name, thm) =
    53   let val thm' = store_thm (name, thm) in
    54     if is_ml_identifier name then
    55       (qed_thm := Some thm';
    56         use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
    57     else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
    58   end;
    59 
    60 fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
    61 fun qed name = ml_store_thm (name, result ());
    62 fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
    63 fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
    64 
    65 
    66 
    67 (** retrieve theorems **)
    68 
    69 (*get theorems that contain all of given constants*)
    70 fun thms_containing raw_consts =
    71   let
    72     val sign = sign_of_thm (topthm ());
    73     val consts = map (Sign.intern_const sign) raw_consts;
    74     val thy = ThyInfo.theory_of_sign sign;
    75   in PureThy.thms_containing thy consts end;
    76 
    77 
    78 (*top_const: main constant, ignoring Trueprop*)
    79 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
    80   | top_const _ = None;
    81 
    82 val intro_const = top_const o concl_of;
    83 
    84 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
    85 
    86 (* In case faster access is necessary, the thm db should provide special
    87 functions
    88 
    89 index_intros, index_elims: string -> (string * thm) list
    90 
    91 where thm [| A1 ; ...; An |] ==> B is returned by
    92 - index_intros c if B  is of the form c t1 ... tn
    93 - index_elims c  if A1 is of the form c t1 ... tn
    94 *)
    95 
    96 (* could be provided by thm db *)
    97 fun index_intros c =
    98   let fun topc(_,thm) = intro_const thm = Some(c);
    99       val named_thms = thms_containing [c]
   100   in filter topc named_thms end;
   101 
   102 (* could be provided by thm db *)
   103 fun index_elims c =
   104   let fun topc(_,thm) = elim_const thm = Some(c);
   105       val named_thms = thms_containing [c]
   106   in filter topc named_thms end;
   107 
   108 (*assume that parameters have unique names*)
   109 fun goal_params i =
   110   let val gi = getgoal i
   111       val frees = map Free (Logic.strip_params gi)
   112   in (gi,frees) end;
   113 
   114 fun concl_of_goal i =
   115   let val (gi,frees) = goal_params i
   116       val B = Logic.strip_assums_concl gi
   117   in subst_bounds(frees,B) end;
   118 
   119 fun prems_of_goal i =
   120   let val (gi,frees) = goal_params i
   121       val As = Logic.strip_assums_hyp gi
   122   in map (fn A => subst_bounds(frees,A)) As end;
   123 
   124 (*returns all those named_thms whose subterm extracted by extract can be
   125   instantiated to obj; the list is sorted according to the number of premises
   126   and the size of the required substitution.*)
   127 fun select_match(obj, signobj, named_thms, extract) =
   128   let fun matches(prop, tsig) =
   129             case extract prop of
   130               None => false
   131             | Some pat => Pattern.matches tsig (pat, obj);
   132 
   133       fun substsize(prop, tsig) =
   134             let val Some pat = extract prop
   135                 val (_,subst) = Pattern.match tsig (pat,obj)
   136             in foldl op+
   137 		(0, map (fn (_,t) => size_of_term t) subst)
   138             end
   139 
   140       fun thm_ord ((p0,s0,_),(p1,s1,_)) =
   141             prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
   142 
   143       fun select((p as (_,thm))::named_thms, sels) =
   144             let val {prop, sign, ...} = rep_thm thm
   145             in select(named_thms,
   146                       if Sign.subsig(sign, signobj) andalso
   147                          matches(prop,#tsig(Sign.rep_sg signobj))
   148                       then
   149 			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
   150                       else sels)
   151             end
   152         | select([],sels) = sels
   153 
   154   in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 
   155 
   156 fun find_matching(prop,sign,index,extract) =
   157   (case top_const prop of
   158      Some c => select_match(prop,sign,index c,extract)
   159    | _      => []);
   160 
   161 fun find_intros(prop,sign) =
   162   find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
   163 
   164 fun find_elims sign prop =
   165   let fun major prop = case Logic.strip_imp_prems prop of
   166                          [] => None | p::_ => Some p
   167   in find_matching(prop,sign,index_elims,major) end;
   168 
   169 fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
   170 
   171 fun findEs i =
   172   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
   173       val sign = #sign(rep_thm(topthm()))
   174       val thmss = map (find_elims sign) (prems_of_goal i)
   175   in foldl (gen_union eq_nth) ([],thmss) end;
   176 
   177 fun findE i j =
   178   let val sign = #sign(rep_thm(topthm()))
   179   in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
   180 
   181 
   182 end;