src/Pure/Thy/thm_database.ML
author wenzelm
Wed Aug 06 14:12:03 1997 +0200 (1997-08-06)
changeset 3627 3d0d5f2a2e33
parent 3601 43c7912aac8d
child 3631 88a279998f90
permissions -rw-r--r--
tuned names;
clasohm@1132
     1
(*  Title:      Pure/Thy/thm_database.ML
clasohm@1132
     2
    ID:         $Id$
nipkow@1221
     3
    Author:     Carsten Clasohm and Tobias Nipkow
clasohm@1132
     4
    Copyright   1995 TU Muenchen
clasohm@1132
     5
*)
clasohm@1132
     6
wenzelm@3627
     7
datatype thm_db =
clasohm@1262
     8
  ThmDB of {count: int,
clasohm@1262
     9
            thy_idx: (Sign.sg * (string list * int list)) list,
clasohm@1262
    10
            const_idx: ((int * (string * thm)) list) Symtab.table};
clasohm@1262
    11
    (*count: number of theorems in database (used as unique ID for next thm)
clasohm@1262
    12
      thy_idx: constants and IDs of theorems
clasohm@1262
    13
               indexed by the theory's signature they belong to
clasohm@1262
    14
      const_idx: named theorems tagged by numbers and
clasohm@1262
    15
                 indexed by the constants they contain*)
clasohm@1262
    16
wenzelm@3627
    17
signature THM_DATABASE =
paulson@1512
    18
  sig
wenzelm@3627
    19
  val thm_db: thm_db ref
clasohm@1132
    20
  val store_thm_db: string * thm -> thm
clasohm@1262
    21
  val delete_thm_db: theory -> unit
clasohm@1132
    22
  val thms_containing: string list -> (string * thm) list
nipkow@1221
    23
  val findI:         int -> (string * thm)list
nipkow@1221
    24
  val findEs:        int -> (string * thm)list
nipkow@1221
    25
  val findE:  int -> int -> (string * thm)list
berghofe@3601
    26
berghofe@3601
    27
  val store_thm      : string * thm -> thm
berghofe@3601
    28
  val bind_thm       : string * thm -> unit
berghofe@3601
    29
  val qed            : string -> unit
berghofe@3601
    30
  val qed_thm        : thm ref
berghofe@3601
    31
  val qed_goal       : string -> theory -> string 
berghofe@3601
    32
                       -> (thm list -> tactic list) -> unit
berghofe@3601
    33
  val qed_goalw      : string -> theory -> thm list -> string 
berghofe@3601
    34
                       -> (thm list -> tactic list) -> unit
berghofe@3601
    35
  val get_thm        : theory -> string -> thm
berghofe@3601
    36
  val thms_of        : theory -> (string * thm) list
berghofe@3601
    37
  val delete_thms    : string -> unit
berghofe@3601
    38
berghofe@3601
    39
  val print_theory   : theory -> unit
paulson@1512
    40
  end;
clasohm@1132
    41
wenzelm@3627
    42
structure ThmDatabase: THM_DATABASE =
nipkow@1221
    43
struct
clasohm@1132
    44
berghofe@3601
    45
open ThyInfo BrowserInfo;
berghofe@3601
    46
nipkow@1221
    47
(*** ignore and top_const could be turned into functor-parameters, but are
nipkow@1221
    48
currently identical for all object logics ***)
nipkow@1221
    49
nipkow@1221
    50
(* Constants not to be used for theorem indexing *)
nipkow@1221
    51
val ignore = ["Trueprop", "all", "==>", "=="];
nipkow@1221
    52
nipkow@1221
    53
(* top_const: main constant, ignoring Trueprop *)
nipkow@1221
    54
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
nipkow@1749
    55
                                         | _          => None)
nipkow@1749
    56
  | top_const _ = None;
clasohm@1132
    57
clasohm@1132
    58
(*Symtab which associates a constant with a list of theorems that contain the
clasohm@1262
    59
  constant (theorems are tagged with numbers)*)
clasohm@1262
    60
val thm_db = ref (ThmDB
clasohm@1262
    61
 {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
clasohm@1262
    62
  const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
clasohm@1132
    63
clasohm@1272
    64
(*List all relevant constants a term contains*)
clasohm@1132
    65
fun list_consts t =
clasohm@1136
    66
  let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
clasohm@1132
    67
        | consts (Free _) = []
clasohm@1132
    68
        | consts (Var _) = []
clasohm@1132
    69
        | consts (Bound _) = []
clasohm@1132
    70
        | consts (Abs (_, _, t)) = consts t
clasohm@1132
    71
        | consts (t1$t2) = (consts t1) union (consts t2);
clasohm@1136
    72
  in distinct (consts t) end;
clasohm@1132
    73
clasohm@1272
    74
(*Store a theorem in database*)
clasohm@1236
    75
fun store_thm_db (named_thm as (name, thm)) =
clasohm@1262
    76
  let val {prop, hyps, sign, ...} = rep_thm thm;
clasohm@1132
    77
clasohm@1136
    78
      val consts = distinct (flat (map list_consts (prop :: hyps)));
clasohm@1136
    79
clasohm@1262
    80
      val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1141
    81
clasohm@1262
    82
      fun update_thys [] = [(sign, (consts, [count]))]
clasohm@1262
    83
        | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
clasohm@1262
    84
            if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
    85
              (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
clasohm@1262
    86
            else thy :: update_thys ts;
clasohm@1132
    87
clasohm@1262
    88
      val tagged_thm = (count, named_thm);
clasohm@1262
    89
clasohm@1262
    90
      fun update_db _ [] result = Some result
clasohm@1262
    91
        | update_db checked (c :: cs) result =
clasohm@1236
    92
            let
clasohm@1236
    93
              val old_thms = Symtab.lookup_multi (result, c);
clasohm@1236
    94
clasohm@1262
    95
              val duplicate =
clasohm@1262
    96
                if checked then false
clasohm@1262
    97
                else case find_first (fn (_, (n, _)) => n = name) old_thms of
clasohm@1262
    98
                       Some (_, (_, t)) => eq_thm (t, thm)
clasohm@1262
    99
                     | None => false
clasohm@1308
   100
            in if duplicate then None
clasohm@1262
   101
               else update_db true
clasohm@1262
   102
                      cs (Symtab.update ((c, tagged_thm :: old_thms), result))
clasohm@1132
   103
            end;
clasohm@1262
   104
clasohm@1262
   105
      val const_idx' = update_db false consts const_idx;
berghofe@1580
   106
  in if consts = [] then warning ("Theorem " ^ name ^
clasohm@1136
   107
                                  " cannot be stored in ThmDB\n\t because it \
clasohm@1136
   108
                                  \contains no or only ignored constants.")
clasohm@1262
   109
     else if is_some const_idx' then
clasohm@1262
   110
       thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
clasohm@1262
   111
                        const_idx = the const_idx'}
clasohm@1262
   112
     else ();
clasohm@1236
   113
     thm
clasohm@1132
   114
  end;
clasohm@1132
   115
clasohm@1272
   116
(*Remove all theorems with given signature from database*)
clasohm@1262
   117
fun delete_thm_db thy =
clasohm@1262
   118
  let
clasohm@1262
   119
    val sign = sign_of thy;
clasohm@1262
   120
clasohm@1262
   121
    val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1262
   122
clasohm@1272
   123
    (*Remove theory from thy_idx and get the data associated with it*)
clasohm@1262
   124
    fun update_thys [] result = (result, [], [])
clasohm@1262
   125
      | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
clasohm@1262
   126
                    result =
clasohm@1262
   127
          if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
   128
            (result @ ts, thy_consts, thy_nums)
clasohm@1262
   129
          else update_thys ts (thy :: result);
clasohm@1262
   130
clasohm@1262
   131
    val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
clasohm@1262
   132
clasohm@1272
   133
    (*Remove all theorems belonging to a theory*)
clasohm@1262
   134
    fun update_db [] result = result
clasohm@1262
   135
      | update_db (c :: cs) result =
clasohm@1262
   136
        let val thms' = filter_out (fn (num, _) => num mem thy_nums)
clasohm@1262
   137
                                   (Symtab.lookup_multi (result, c));
clasohm@1262
   138
        in update_db cs (Symtab.update ((c, thms'), result)) end;
clasohm@1262
   139
  in thm_db := ThmDB {count = count, thy_idx = thy_idx',
clasohm@1262
   140
                      const_idx = update_db thy_consts const_idx}
clasohm@1262
   141
  end;
clasohm@1262
   142
clasohm@1272
   143
(*Intersection of two theorem lists with descending tags*)
clasohm@1132
   144
infix desc_inter;
clasohm@1132
   145
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
clasohm@1132
   146
  | xs desc_inter [] = []
clasohm@1132
   147
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
clasohm@1132
   148
      if xi = yi then x :: (xs desc_inter ys)
clasohm@1132
   149
      else if xi > yi then xs desc_inter yss
clasohm@1132
   150
      else xss desc_inter ys;
clasohm@1132
   151
clasohm@1272
   152
(*Get all theorems from database that contain a list of constants*)
clasohm@1132
   153
fun thms_containing constants =
clasohm@1132
   154
  let fun collect [] _ result = map snd result
clasohm@1132
   155
        | collect (c :: cs) first result =
clasohm@1262
   156
            let val ThmDB {const_idx, ...} = !thm_db;
clasohm@1262
   157
clasohm@1262
   158
                val new_thms = Symtab.lookup_multi (const_idx, c);
clasohm@1132
   159
            in collect cs false (if first then new_thms
clasohm@1132
   160
                                          else (result desc_inter new_thms))
clasohm@1132
   161
            end;
clasohm@1132
   162
clasohm@1134
   163
      val look_for = constants \\ ignore;
clasohm@1134
   164
  in if null look_for then
clasohm@1136
   165
       error ("No or only ignored constants were specified for theorem \
clasohm@1136
   166
              \database search:\n  " ^ commas (map quote ignore))
clasohm@1134
   167
     else ();
clasohm@1134
   168
     collect look_for true [] end;
clasohm@1136
   169
nipkow@1221
   170
val intro_const = top_const o concl_of;
nipkow@1221
   171
nipkow@1221
   172
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
nipkow@1221
   173
nipkow@1221
   174
(* In case faster access is necessary, the thm db should provide special
nipkow@1221
   175
functions
nipkow@1221
   176
nipkow@1221
   177
index_intros, index_elims: string -> (string * thm) list
nipkow@1221
   178
nipkow@1221
   179
where thm [| A1 ; ...; An |] ==> B is returned by
nipkow@1221
   180
- index_intros c if B  is of the form c t1 ... tn
nipkow@1221
   181
- index_elims c  if A1 is of the form c t1 ... tn
nipkow@1221
   182
*)
nipkow@1221
   183
nipkow@1221
   184
(* could be provided by thm db *)
nipkow@1221
   185
fun index_intros c =
nipkow@1221
   186
  let fun topc(_,thm) = intro_const thm = Some(c);
nipkow@1221
   187
      val named_thms = thms_containing [c]
nipkow@1221
   188
  in filter topc named_thms end;
nipkow@1221
   189
nipkow@1221
   190
(* could be provided by thm db *)
nipkow@1221
   191
fun index_elims c =
nipkow@1221
   192
  let fun topc(_,thm) = elim_const thm = Some(c);
nipkow@1221
   193
      val named_thms = thms_containing [c]
nipkow@1221
   194
  in filter topc named_thms end;
nipkow@1221
   195
nipkow@1221
   196
(*assume that parameters have unique names*)
nipkow@1221
   197
fun goal_params i =
nipkow@1221
   198
  let val gi = getgoal i
nipkow@1221
   199
      val frees = map Free (Logic.strip_params gi)
nipkow@1221
   200
  in (gi,frees) end;
nipkow@1221
   201
nipkow@1221
   202
fun concl_of_goal i =
nipkow@1221
   203
  let val (gi,frees) = goal_params i
nipkow@1221
   204
      val B = Logic.strip_assums_concl gi
nipkow@1221
   205
  in subst_bounds(frees,B) end;
nipkow@1221
   206
nipkow@1221
   207
fun prems_of_goal i =
nipkow@1221
   208
  let val (gi,frees) = goal_params i
nipkow@1221
   209
      val As = Logic.strip_assums_hyp gi
nipkow@1221
   210
  in map (fn A => subst_bounds(frees,A)) As end;
nipkow@1221
   211
clasohm@1262
   212
fun select_match(obj, signobj, named_thms, extract) =
clasohm@1262
   213
  let fun matches(prop, tsig) =
nipkow@1221
   214
            case extract prop of
nipkow@1221
   215
              None => false
clasohm@1262
   216
            | Some pat => Pattern.matches tsig (pat, obj);
nipkow@1221
   217
berghofe@1654
   218
      fun substsize(prop, tsig) =
berghofe@1654
   219
            let val Some pat = extract prop
berghofe@1654
   220
                val (_,subst) = Pattern.match tsig (pat,obj)
paulson@2150
   221
            in foldl op+
paulson@2150
   222
		(0, map (fn (_,t) => size_of_term t) subst)
paulson@2150
   223
            end
berghofe@1654
   224
berghofe@1654
   225
      fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
berghofe@1654
   226
            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
berghofe@1654
   227
            orelse (p0=0 andalso p1<>0)
berghofe@1654
   228
clasohm@1262
   229
      fun select((p as (_,thm))::named_thms, sels) =
clasohm@1262
   230
            let val {prop, sign, ...} = rep_thm thm
nipkow@1221
   231
            in select(named_thms,
clasohm@1262
   232
                      if Sign.subsig(sign, signobj) andalso
nipkow@1230
   233
                         matches(prop,#tsig(Sign.rep_sg signobj))
berghofe@1654
   234
                      then
berghofe@1654
   235
			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
berghofe@1654
   236
                      else sels)
clasohm@1136
   237
            end
clasohm@1136
   238
        | select([],sels) = sels
nipkow@1221
   239
berghofe@1654
   240
  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
nipkow@1221
   241
nipkow@1221
   242
fun find_matching(prop,sign,index,extract) =
nipkow@1221
   243
  (case top_const prop of
nipkow@1221
   244
     Some c => select_match(prop,sign,index c,extract)
nipkow@1221
   245
   | _      => []);
nipkow@1221
   246
nipkow@1221
   247
fun find_intros(prop,sign) =
nipkow@1221
   248
  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
clasohm@1136
   249
nipkow@1221
   250
fun find_elims sign prop =
nipkow@1221
   251
  let fun major prop = case Logic.strip_imp_prems prop of
nipkow@1221
   252
                         [] => None | p::_ => Some p
nipkow@1221
   253
  in find_matching(prop,sign,index_elims,major) end;
nipkow@1221
   254
nipkow@1221
   255
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
nipkow@1221
   256
nipkow@1221
   257
fun findEs i =
nipkow@1230
   258
  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
nipkow@1230
   259
      val sign = #sign(rep_thm(topthm()))
nipkow@1230
   260
      val thmss = map (find_elims sign) (prems_of_goal i)
nipkow@1230
   261
  in foldl (gen_union eq_nth) ([],thmss) end;
nipkow@1221
   262
nipkow@1221
   263
fun findE i j =
nipkow@1221
   264
  let val sign = #sign(rep_thm(topthm()))
nipkow@1221
   265
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
nipkow@1221
   266
berghofe@3601
   267
berghofe@3601
   268
(*** Store and retrieve theorems ***)
berghofe@3601
   269
berghofe@3601
   270
(** Store theorems **)
berghofe@3601
   271
berghofe@3601
   272
(*Store a theorem in the thy_info of its theory,
berghofe@3601
   273
  and in the theory's HTML file*)
berghofe@3601
   274
fun store_thm (name, thm) =
berghofe@3601
   275
  let
berghofe@3601
   276
    val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
berghofe@3601
   277
                            theory, thms, methods, data}) =
berghofe@3601
   278
      thyinfo_of_sign (#sign (rep_thm thm))
berghofe@3601
   279
berghofe@3601
   280
    val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
berghofe@3601
   281
      handle Symtab.DUPLICATE s => 
berghofe@3601
   282
        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
berghofe@3601
   283
           (warning ("Theory database already contains copy of\
berghofe@3601
   284
                     \ theorem " ^ quote name);
berghofe@3601
   285
            (thms, true))
berghofe@3601
   286
         else error ("Duplicate theorem name " ^ quote s
berghofe@3601
   287
                     ^ " used in theory database"));
berghofe@3601
   288
berghofe@3601
   289
    (*Label this theorem*)
berghofe@3601
   290
    val thm' = Thm.name_thm (name, thm)
berghofe@3601
   291
  in
berghofe@3601
   292
    loaded_thys := Symtab.update
berghofe@3601
   293
     ((thy_name, ThyInfo {path = path, children = children, parents = parents,
berghofe@3601
   294
                          thy_time = thy_time, ml_time = ml_time,
berghofe@3601
   295
                          theory = theory, thms = thms',
berghofe@3601
   296
                          methods = methods, data = data}),
berghofe@3601
   297
      !loaded_thys);
berghofe@3601
   298
    thm_to_html thm name;
berghofe@3601
   299
    if duplicate then thm' else store_thm_db (name, thm')
berghofe@3601
   300
  end;
berghofe@3601
   301
berghofe@3601
   302
berghofe@3601
   303
(*Store result of proof in loaded_thys and as ML value*)
berghofe@3601
   304
berghofe@3601
   305
val qed_thm = ref flexpair_def(*dummy*);
berghofe@3601
   306
berghofe@3601
   307
berghofe@3601
   308
fun bind_thm (name, thm) =
berghofe@3601
   309
 (qed_thm := store_thm (name, (standard thm));
berghofe@3601
   310
  use_string ["val " ^ name ^ " = !qed_thm;"]);
berghofe@3601
   311
berghofe@3601
   312
berghofe@3601
   313
fun qed name =
berghofe@3601
   314
 (qed_thm := store_thm (name, result ());
berghofe@3601
   315
  use_string ["val " ^ name ^ " = !qed_thm;"]);
berghofe@3601
   316
berghofe@3601
   317
berghofe@3601
   318
fun qed_goal name thy agoal tacsf =
berghofe@3601
   319
 (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
berghofe@3601
   320
  use_string ["val " ^ name ^ " = !qed_thm;"]);
berghofe@3601
   321
berghofe@3601
   322
berghofe@3601
   323
fun qed_goalw name thy rths agoal tacsf =
berghofe@3601
   324
 (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
berghofe@3601
   325
  use_string ["val " ^ name ^ " = !qed_thm;"]);
berghofe@3601
   326
berghofe@3601
   327
berghofe@3601
   328
(** Retrieve theorems **)
berghofe@3601
   329
berghofe@3601
   330
(*Get all theorems belonging to a given theory*)
berghofe@3601
   331
fun thmtab_of_thy thy =
berghofe@3601
   332
  let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
berghofe@3601
   333
  in thms end;
berghofe@3601
   334
berghofe@3601
   335
berghofe@3601
   336
fun thmtab_of_name name =
berghofe@3601
   337
  let val ThyInfo {thms, ...} = the (get_thyinfo name);
berghofe@3601
   338
  in thms end;
berghofe@3601
   339
berghofe@3601
   340
berghofe@3601
   341
(*Get a stored theorem specified by theory and name. *)
berghofe@3601
   342
fun get_thm thy name =
berghofe@3601
   343
  let fun get [] [] searched =
berghofe@3601
   344
           raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
berghofe@3601
   345
        | get [] ng searched =
berghofe@3601
   346
            get (ng \\ searched) [] searched
berghofe@3601
   347
        | get (t::ts) ng searched =
berghofe@3601
   348
            (case Symtab.lookup (thmtab_of_name t, name) of
berghofe@3601
   349
                 Some thm => thm
berghofe@3601
   350
               | None => get ts (ng union (parents_of_name t)) (t::searched));
berghofe@3601
   351
berghofe@3601
   352
      val (tname, _) = thyinfo_of_sign (sign_of thy);
berghofe@3601
   353
  in get [tname] [] [] end;
berghofe@3601
   354
berghofe@3601
   355
berghofe@3601
   356
(*Get stored theorems of a theory (original derivations) *)
berghofe@3601
   357
val thms_of = Symtab.dest o thmtab_of_thy;
berghofe@3601
   358
berghofe@3601
   359
berghofe@3601
   360
(*Remove theorems associated with a theory from theory and theorem database*)
berghofe@3601
   361
fun delete_thms tname =
berghofe@3601
   362
  let
berghofe@3601
   363
    val tinfo = case get_thyinfo tname of
berghofe@3601
   364
        Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
berghofe@3601
   365
                       methods, data, ...}) =>
berghofe@3601
   366
          ThyInfo {path = path, children = children, parents = parents,
berghofe@3601
   367
                   thy_time = thy_time, ml_time = ml_time,
berghofe@3601
   368
                   theory = theory, thms = Symtab.null,
berghofe@3601
   369
                   methods = methods, data = data}
berghofe@3601
   370
      | None => error ("Theory " ^ tname ^ " not stored by loader");
berghofe@3601
   371
berghofe@3601
   372
    val ThyInfo {theory, ...} = tinfo;
berghofe@3601
   373
  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
berghofe@3601
   374
     case theory of
berghofe@3601
   375
         Some t => delete_thm_db t
berghofe@3601
   376
       | None => ()
berghofe@3601
   377
  end;
berghofe@3601
   378
berghofe@3601
   379
berghofe@3601
   380
(*** Print theory ***)
berghofe@3601
   381
berghofe@3601
   382
fun print_thms thy =
berghofe@3601
   383
  let
berghofe@3601
   384
    val thms = thms_of thy;
berghofe@3601
   385
    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
berghofe@3601
   386
      Pretty.quote (pretty_thm th)];
berghofe@3601
   387
  in
berghofe@3601
   388
    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
berghofe@3601
   389
  end;
berghofe@3601
   390
berghofe@3601
   391
berghofe@3601
   392
fun print_theory thy = (Display.print_theory thy; print_thms thy);
berghofe@3601
   393
clasohm@1132
   394
end;