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