src/Pure/Thy/thm_database.ML
author clasohm
Wed Oct 04 12:59:52 1995 +0100 (1995-10-04)
changeset 1262 8f40ff1299d8
parent 1245 934183dfc786
child 1272 dd877dc7c1f4
permissions -rw-r--r--
added removal of theorems if theory is to be reloaded; changed functions for
local simpsets
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
clasohm@1262
     7
datatype thm_db_type =
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
clasohm@1132
    17
signature THMDB =
clasohm@1132
    18
sig
clasohm@1262
    19
  val thm_db: thm_db_type 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
clasohm@1132
    26
end;
clasohm@1132
    27
clasohm@1262
    28
functor ThmDBFun(): THMDB =
nipkow@1221
    29
struct
clasohm@1132
    30
nipkow@1221
    31
(*** ignore and top_const could be turned into functor-parameters, but are
nipkow@1221
    32
currently identical for all object logics ***)
nipkow@1221
    33
nipkow@1221
    34
(* Constants not to be used for theorem indexing *)
nipkow@1221
    35
val ignore = ["Trueprop", "all", "==>", "=="];
nipkow@1221
    36
nipkow@1221
    37
(* top_const: main constant, ignoring Trueprop *)
nipkow@1221
    38
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
nipkow@1221
    39
                                         | _          => None);
clasohm@1132
    40
clasohm@1132
    41
(*Symtab which associates a constant with a list of theorems that contain the
clasohm@1262
    42
  constant (theorems are tagged with numbers)*)
clasohm@1262
    43
val thm_db = ref (ThmDB
clasohm@1262
    44
 {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
clasohm@1262
    45
  const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
clasohm@1132
    46
clasohm@1136
    47
(*list all relevant constants a term contains*)
clasohm@1132
    48
fun list_consts t =
clasohm@1136
    49
  let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
clasohm@1132
    50
        | consts (Free _) = []
clasohm@1132
    51
        | consts (Var _) = []
clasohm@1132
    52
        | consts (Bound _) = []
clasohm@1132
    53
        | consts (Abs (_, _, t)) = consts t
clasohm@1132
    54
        | consts (t1$t2) = (consts t1) union (consts t2);
clasohm@1136
    55
  in distinct (consts t) end;
clasohm@1132
    56
clasohm@1132
    57
(*store a theorem in database*)
clasohm@1236
    58
fun store_thm_db (named_thm as (name, thm)) =
clasohm@1262
    59
  let val {prop, hyps, sign, ...} = rep_thm thm;
clasohm@1132
    60
clasohm@1136
    61
      val consts = distinct (flat (map list_consts (prop :: hyps)));
clasohm@1136
    62
clasohm@1262
    63
      val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1141
    64
clasohm@1262
    65
      fun update_thys [] = [(sign, (consts, [count]))]
clasohm@1262
    66
        | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
clasohm@1262
    67
            if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
    68
              (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
clasohm@1262
    69
            else thy :: update_thys ts;
clasohm@1132
    70
clasohm@1262
    71
      val tagged_thm = (count, named_thm);
clasohm@1262
    72
clasohm@1262
    73
      fun update_db _ [] result = Some result
clasohm@1262
    74
        | update_db checked (c :: cs) result =
clasohm@1236
    75
            let
clasohm@1236
    76
              val old_thms = Symtab.lookup_multi (result, c);
clasohm@1236
    77
clasohm@1262
    78
              val duplicate =
clasohm@1262
    79
                if checked then false
clasohm@1262
    80
                else case find_first (fn (_, (n, _)) => n = name) old_thms of
clasohm@1262
    81
                       Some (_, (_, t)) => eq_thm (t, thm)
clasohm@1262
    82
                     | None => false
clasohm@1262
    83
            in if duplicate then
clasohm@1262
    84
                 (writeln ("Warning: Theorem database already contains copy of\
clasohm@1262
    85
                           \ theorem " ^ quote name);
clasohm@1262
    86
                  None)
clasohm@1262
    87
               else update_db true
clasohm@1262
    88
                      cs (Symtab.update ((c, tagged_thm :: old_thms), result))
clasohm@1132
    89
            end;
clasohm@1262
    90
clasohm@1262
    91
      val const_idx' = update_db false consts const_idx;
clasohm@1132
    92
  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
clasohm@1136
    93
                                  " cannot be stored in ThmDB\n\t because it \
clasohm@1136
    94
                                  \contains no or only ignored constants.")
clasohm@1262
    95
     else if is_some const_idx' then
clasohm@1262
    96
       thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
clasohm@1262
    97
                        const_idx = the const_idx'}
clasohm@1262
    98
     else ();
clasohm@1236
    99
     thm
clasohm@1132
   100
  end;
clasohm@1132
   101
clasohm@1262
   102
(*remove all theorems with given signature from database*)
clasohm@1262
   103
fun delete_thm_db thy =
clasohm@1262
   104
  let
clasohm@1262
   105
    val sign = sign_of thy;
clasohm@1262
   106
clasohm@1262
   107
    val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1262
   108
clasohm@1262
   109
    fun update_thys [] result = (result, [], [])
clasohm@1262
   110
      | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
clasohm@1262
   111
                    result =
clasohm@1262
   112
          if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
   113
            (result @ ts, thy_consts, thy_nums)
clasohm@1262
   114
          else update_thys ts (thy :: result);
clasohm@1262
   115
clasohm@1262
   116
    val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
clasohm@1262
   117
clasohm@1262
   118
    fun update_db [] result = result
clasohm@1262
   119
      | update_db (c :: cs) result =
clasohm@1262
   120
        let val thms' = filter_out (fn (num, _) => num mem thy_nums)
clasohm@1262
   121
                                   (Symtab.lookup_multi (result, c));
clasohm@1262
   122
        in update_db cs (Symtab.update ((c, thms'), result)) end;
clasohm@1262
   123
  in thm_db := ThmDB {count = count, thy_idx = thy_idx',
clasohm@1262
   124
                      const_idx = update_db thy_consts const_idx}
clasohm@1262
   125
  end;
clasohm@1262
   126
clasohm@1262
   127
(*intersection of two theorem lists with descending tags*)
clasohm@1132
   128
infix desc_inter;
clasohm@1132
   129
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
clasohm@1132
   130
  | xs desc_inter [] = []
clasohm@1132
   131
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
clasohm@1132
   132
      if xi = yi then x :: (xs desc_inter ys)
clasohm@1132
   133
      else if xi > yi then xs desc_inter yss
clasohm@1132
   134
      else xss desc_inter ys;
clasohm@1132
   135
clasohm@1132
   136
(*get all theorems from database that contain a list of constants*)
clasohm@1132
   137
fun thms_containing constants =
clasohm@1132
   138
  let fun collect [] _ result = map snd result
clasohm@1132
   139
        | collect (c :: cs) first result =
clasohm@1262
   140
            let val ThmDB {const_idx, ...} = !thm_db;
clasohm@1262
   141
clasohm@1262
   142
                val new_thms = Symtab.lookup_multi (const_idx, c);
clasohm@1132
   143
            in collect cs false (if first then new_thms
clasohm@1132
   144
                                          else (result desc_inter new_thms))
clasohm@1132
   145
            end;
clasohm@1132
   146
clasohm@1134
   147
      val look_for = constants \\ ignore;
clasohm@1134
   148
  in if null look_for then
clasohm@1136
   149
       error ("No or only ignored constants were specified for theorem \
clasohm@1136
   150
              \database search:\n  " ^ commas (map quote ignore))
clasohm@1134
   151
     else ();
clasohm@1134
   152
     collect look_for true [] end;
clasohm@1136
   153
nipkow@1221
   154
val intro_const = top_const o concl_of;
nipkow@1221
   155
nipkow@1221
   156
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
nipkow@1221
   157
nipkow@1221
   158
(* In case faster access is necessary, the thm db should provide special
nipkow@1221
   159
functions
nipkow@1221
   160
nipkow@1221
   161
index_intros, index_elims: string -> (string * thm) list
nipkow@1221
   162
nipkow@1221
   163
where thm [| A1 ; ...; An |] ==> B is returned by
nipkow@1221
   164
- index_intros c if B  is of the form c t1 ... tn
nipkow@1221
   165
- index_elims c  if A1 is of the form c t1 ... tn
nipkow@1221
   166
*)
nipkow@1221
   167
nipkow@1221
   168
(* could be provided by thm db *)
nipkow@1221
   169
fun index_intros c =
nipkow@1221
   170
  let fun topc(_,thm) = intro_const thm = Some(c);
nipkow@1221
   171
      val named_thms = thms_containing [c]
nipkow@1221
   172
  in filter topc named_thms end;
nipkow@1221
   173
nipkow@1221
   174
(* could be provided by thm db *)
nipkow@1221
   175
fun index_elims c =
nipkow@1221
   176
  let fun topc(_,thm) = elim_const thm = Some(c);
nipkow@1221
   177
      val named_thms = thms_containing [c]
nipkow@1221
   178
  in filter topc named_thms end;
nipkow@1221
   179
nipkow@1221
   180
(*assume that parameters have unique names*)
nipkow@1221
   181
fun goal_params i =
nipkow@1221
   182
  let val gi = getgoal i
nipkow@1221
   183
      val frees = map Free (Logic.strip_params gi)
nipkow@1221
   184
  in (gi,frees) end;
nipkow@1221
   185
nipkow@1221
   186
fun concl_of_goal i =
nipkow@1221
   187
  let val (gi,frees) = goal_params i
nipkow@1221
   188
      val B = Logic.strip_assums_concl gi
nipkow@1221
   189
  in subst_bounds(frees,B) end;
nipkow@1221
   190
nipkow@1221
   191
fun prems_of_goal i =
nipkow@1221
   192
  let val (gi,frees) = goal_params i
nipkow@1221
   193
      val As = Logic.strip_assums_hyp gi
nipkow@1221
   194
  in map (fn A => subst_bounds(frees,A)) As end;
nipkow@1221
   195
clasohm@1262
   196
fun select_match(obj, signobj, named_thms, extract) =
clasohm@1262
   197
  let fun matches(prop, tsig) =
nipkow@1221
   198
            case extract prop of
nipkow@1221
   199
              None => false
clasohm@1262
   200
            | Some pat => Pattern.matches tsig (pat, obj);
nipkow@1221
   201
clasohm@1262
   202
      fun select((p as (_,thm))::named_thms, sels) =
clasohm@1262
   203
            let val {prop, sign, ...} = rep_thm thm
nipkow@1221
   204
            in select(named_thms,
clasohm@1262
   205
                      if Sign.subsig(sign, signobj) andalso
nipkow@1230
   206
                         matches(prop,#tsig(Sign.rep_sg signobj))
nipkow@1221
   207
                      then p::sels else sels)
clasohm@1136
   208
            end
clasohm@1136
   209
        | select([],sels) = sels
nipkow@1221
   210
clasohm@1262
   211
  in select(named_thms, []) end;
nipkow@1221
   212
nipkow@1221
   213
fun find_matching(prop,sign,index,extract) =
nipkow@1221
   214
  (case top_const prop of
nipkow@1221
   215
     Some c => select_match(prop,sign,index c,extract)
nipkow@1221
   216
   | _      => []);
nipkow@1221
   217
nipkow@1221
   218
fun find_intros(prop,sign) =
nipkow@1221
   219
  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
clasohm@1136
   220
nipkow@1221
   221
fun find_elims sign prop =
nipkow@1221
   222
  let fun major prop = case Logic.strip_imp_prems prop of
nipkow@1221
   223
                         [] => None | p::_ => Some p
nipkow@1221
   224
  in find_matching(prop,sign,index_elims,major) end;
nipkow@1221
   225
nipkow@1221
   226
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
nipkow@1221
   227
nipkow@1221
   228
fun findEs i =
nipkow@1230
   229
  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
nipkow@1230
   230
      val sign = #sign(rep_thm(topthm()))
nipkow@1230
   231
      val thmss = map (find_elims sign) (prems_of_goal i)
nipkow@1230
   232
  in foldl (gen_union eq_nth) ([],thmss) end;
nipkow@1221
   233
nipkow@1221
   234
fun findE i j =
nipkow@1221
   235
  let val sign = #sign(rep_thm(topthm()))
nipkow@1221
   236
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
nipkow@1221
   237
clasohm@1132
   238
end;