src/Pure/Thy/thm_database.ML
author clasohm
Wed Oct 25 13:41:45 1995 +0100 (1995-10-25)
changeset 1308 396ef8aa37b7
parent 1272 dd877dc7c1f4
child 1512 ce37c64244c0
permissions -rw-r--r--
removed "duplicate" warning from store_thm_db;
changed place where store_thm_db is called for a theory's axioms
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@1272
    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@1272
    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@1308
    83
            in if duplicate then None
clasohm@1262
    84
               else update_db true
clasohm@1262
    85
                      cs (Symtab.update ((c, tagged_thm :: old_thms), result))
clasohm@1132
    86
            end;
clasohm@1262
    87
clasohm@1262
    88
      val const_idx' = update_db false consts const_idx;
clasohm@1132
    89
  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
clasohm@1136
    90
                                  " cannot be stored in ThmDB\n\t because it \
clasohm@1136
    91
                                  \contains no or only ignored constants.")
clasohm@1262
    92
     else if is_some const_idx' then
clasohm@1262
    93
       thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
clasohm@1262
    94
                        const_idx = the const_idx'}
clasohm@1262
    95
     else ();
clasohm@1236
    96
     thm
clasohm@1132
    97
  end;
clasohm@1132
    98
clasohm@1272
    99
(*Remove all theorems with given signature from database*)
clasohm@1262
   100
fun delete_thm_db thy =
clasohm@1262
   101
  let
clasohm@1262
   102
    val sign = sign_of thy;
clasohm@1262
   103
clasohm@1262
   104
    val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1262
   105
clasohm@1272
   106
    (*Remove theory from thy_idx and get the data associated with it*)
clasohm@1262
   107
    fun update_thys [] result = (result, [], [])
clasohm@1262
   108
      | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
clasohm@1262
   109
                    result =
clasohm@1262
   110
          if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
   111
            (result @ ts, thy_consts, thy_nums)
clasohm@1262
   112
          else update_thys ts (thy :: result);
clasohm@1262
   113
clasohm@1262
   114
    val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
clasohm@1262
   115
clasohm@1272
   116
    (*Remove all theorems belonging to a theory*)
clasohm@1262
   117
    fun update_db [] result = result
clasohm@1262
   118
      | update_db (c :: cs) result =
clasohm@1262
   119
        let val thms' = filter_out (fn (num, _) => num mem thy_nums)
clasohm@1262
   120
                                   (Symtab.lookup_multi (result, c));
clasohm@1262
   121
        in update_db cs (Symtab.update ((c, thms'), result)) end;
clasohm@1262
   122
  in thm_db := ThmDB {count = count, thy_idx = thy_idx',
clasohm@1262
   123
                      const_idx = update_db thy_consts const_idx}
clasohm@1262
   124
  end;
clasohm@1262
   125
clasohm@1272
   126
(*Intersection of two theorem lists with descending tags*)
clasohm@1132
   127
infix desc_inter;
clasohm@1132
   128
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
clasohm@1132
   129
  | xs desc_inter [] = []
clasohm@1132
   130
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
clasohm@1132
   131
      if xi = yi then x :: (xs desc_inter ys)
clasohm@1132
   132
      else if xi > yi then xs desc_inter yss
clasohm@1132
   133
      else xss desc_inter ys;
clasohm@1132
   134
clasohm@1272
   135
(*Get all theorems from database that contain a list of constants*)
clasohm@1132
   136
fun thms_containing constants =
clasohm@1132
   137
  let fun collect [] _ result = map snd result
clasohm@1132
   138
        | collect (c :: cs) first result =
clasohm@1262
   139
            let val ThmDB {const_idx, ...} = !thm_db;
clasohm@1262
   140
clasohm@1262
   141
                val new_thms = Symtab.lookup_multi (const_idx, c);
clasohm@1132
   142
            in collect cs false (if first then new_thms
clasohm@1132
   143
                                          else (result desc_inter new_thms))
clasohm@1132
   144
            end;
clasohm@1132
   145
clasohm@1134
   146
      val look_for = constants \\ ignore;
clasohm@1134
   147
  in if null look_for then
clasohm@1136
   148
       error ("No or only ignored constants were specified for theorem \
clasohm@1136
   149
              \database search:\n  " ^ commas (map quote ignore))
clasohm@1134
   150
     else ();
clasohm@1134
   151
     collect look_for true [] end;
clasohm@1136
   152
nipkow@1221
   153
val intro_const = top_const o concl_of;
nipkow@1221
   154
nipkow@1221
   155
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
nipkow@1221
   156
nipkow@1221
   157
(* In case faster access is necessary, the thm db should provide special
nipkow@1221
   158
functions
nipkow@1221
   159
nipkow@1221
   160
index_intros, index_elims: string -> (string * thm) list
nipkow@1221
   161
nipkow@1221
   162
where thm [| A1 ; ...; An |] ==> B is returned by
nipkow@1221
   163
- index_intros c if B  is of the form c t1 ... tn
nipkow@1221
   164
- index_elims c  if A1 is of the form c t1 ... tn
nipkow@1221
   165
*)
nipkow@1221
   166
nipkow@1221
   167
(* could be provided by thm db *)
nipkow@1221
   168
fun index_intros c =
nipkow@1221
   169
  let fun topc(_,thm) = intro_const thm = Some(c);
nipkow@1221
   170
      val named_thms = thms_containing [c]
nipkow@1221
   171
  in filter topc named_thms end;
nipkow@1221
   172
nipkow@1221
   173
(* could be provided by thm db *)
nipkow@1221
   174
fun index_elims c =
nipkow@1221
   175
  let fun topc(_,thm) = elim_const thm = Some(c);
nipkow@1221
   176
      val named_thms = thms_containing [c]
nipkow@1221
   177
  in filter topc named_thms end;
nipkow@1221
   178
nipkow@1221
   179
(*assume that parameters have unique names*)
nipkow@1221
   180
fun goal_params i =
nipkow@1221
   181
  let val gi = getgoal i
nipkow@1221
   182
      val frees = map Free (Logic.strip_params gi)
nipkow@1221
   183
  in (gi,frees) end;
nipkow@1221
   184
nipkow@1221
   185
fun concl_of_goal i =
nipkow@1221
   186
  let val (gi,frees) = goal_params i
nipkow@1221
   187
      val B = Logic.strip_assums_concl gi
nipkow@1221
   188
  in subst_bounds(frees,B) end;
nipkow@1221
   189
nipkow@1221
   190
fun prems_of_goal i =
nipkow@1221
   191
  let val (gi,frees) = goal_params i
nipkow@1221
   192
      val As = Logic.strip_assums_hyp gi
nipkow@1221
   193
  in map (fn A => subst_bounds(frees,A)) As end;
nipkow@1221
   194
clasohm@1262
   195
fun select_match(obj, signobj, named_thms, extract) =
clasohm@1262
   196
  let fun matches(prop, tsig) =
nipkow@1221
   197
            case extract prop of
nipkow@1221
   198
              None => false
clasohm@1262
   199
            | Some pat => Pattern.matches tsig (pat, obj);
nipkow@1221
   200
clasohm@1262
   201
      fun select((p as (_,thm))::named_thms, sels) =
clasohm@1262
   202
            let val {prop, sign, ...} = rep_thm thm
nipkow@1221
   203
            in select(named_thms,
clasohm@1262
   204
                      if Sign.subsig(sign, signobj) andalso
nipkow@1230
   205
                         matches(prop,#tsig(Sign.rep_sg signobj))
nipkow@1221
   206
                      then p::sels else sels)
clasohm@1136
   207
            end
clasohm@1136
   208
        | select([],sels) = sels
nipkow@1221
   209
clasohm@1262
   210
  in select(named_thms, []) end;
nipkow@1221
   211
nipkow@1221
   212
fun find_matching(prop,sign,index,extract) =
nipkow@1221
   213
  (case top_const prop of
nipkow@1221
   214
     Some c => select_match(prop,sign,index c,extract)
nipkow@1221
   215
   | _      => []);
nipkow@1221
   216
nipkow@1221
   217
fun find_intros(prop,sign) =
nipkow@1221
   218
  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
clasohm@1136
   219
nipkow@1221
   220
fun find_elims sign prop =
nipkow@1221
   221
  let fun major prop = case Logic.strip_imp_prems prop of
nipkow@1221
   222
                         [] => None | p::_ => Some p
nipkow@1221
   223
  in find_matching(prop,sign,index_elims,major) end;
nipkow@1221
   224
nipkow@1221
   225
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
nipkow@1221
   226
nipkow@1221
   227
fun findEs i =
nipkow@1230
   228
  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
nipkow@1230
   229
      val sign = #sign(rep_thm(topthm()))
nipkow@1230
   230
      val thmss = map (find_elims sign) (prems_of_goal i)
nipkow@1230
   231
  in foldl (gen_union eq_nth) ([],thmss) end;
nipkow@1221
   232
nipkow@1221
   233
fun findE i j =
nipkow@1221
   234
  let val sign = #sign(rep_thm(topthm()))
nipkow@1221
   235
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
nipkow@1221
   236
clasohm@1132
   237
end;