src/Pure/Thy/thm_database.ML
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 2150 084218afaf4b
child 3601 43c7912aac8d
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
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 =
paulson@1512
    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
paulson@1512
    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@1749
    39
                                         | _          => None)
nipkow@1749
    40
  | top_const _ = None;
clasohm@1132
    41
clasohm@1132
    42
(*Symtab which associates a constant with a list of theorems that contain the
clasohm@1262
    43
  constant (theorems are tagged with numbers)*)
clasohm@1262
    44
val thm_db = ref (ThmDB
clasohm@1262
    45
 {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
clasohm@1262
    46
  const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
clasohm@1132
    47
clasohm@1272
    48
(*List all relevant constants a term contains*)
clasohm@1132
    49
fun list_consts t =
clasohm@1136
    50
  let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
clasohm@1132
    51
        | consts (Free _) = []
clasohm@1132
    52
        | consts (Var _) = []
clasohm@1132
    53
        | consts (Bound _) = []
clasohm@1132
    54
        | consts (Abs (_, _, t)) = consts t
clasohm@1132
    55
        | consts (t1$t2) = (consts t1) union (consts t2);
clasohm@1136
    56
  in distinct (consts t) end;
clasohm@1132
    57
clasohm@1272
    58
(*Store a theorem in database*)
clasohm@1236
    59
fun store_thm_db (named_thm as (name, thm)) =
clasohm@1262
    60
  let val {prop, hyps, sign, ...} = rep_thm thm;
clasohm@1132
    61
clasohm@1136
    62
      val consts = distinct (flat (map list_consts (prop :: hyps)));
clasohm@1136
    63
clasohm@1262
    64
      val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1141
    65
clasohm@1262
    66
      fun update_thys [] = [(sign, (consts, [count]))]
clasohm@1262
    67
        | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
clasohm@1262
    68
            if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
    69
              (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
clasohm@1262
    70
            else thy :: update_thys ts;
clasohm@1132
    71
clasohm@1262
    72
      val tagged_thm = (count, named_thm);
clasohm@1262
    73
clasohm@1262
    74
      fun update_db _ [] result = Some result
clasohm@1262
    75
        | update_db checked (c :: cs) result =
clasohm@1236
    76
            let
clasohm@1236
    77
              val old_thms = Symtab.lookup_multi (result, c);
clasohm@1236
    78
clasohm@1262
    79
              val duplicate =
clasohm@1262
    80
                if checked then false
clasohm@1262
    81
                else case find_first (fn (_, (n, _)) => n = name) old_thms of
clasohm@1262
    82
                       Some (_, (_, t)) => eq_thm (t, thm)
clasohm@1262
    83
                     | None => false
clasohm@1308
    84
            in if duplicate then None
clasohm@1262
    85
               else update_db true
clasohm@1262
    86
                      cs (Symtab.update ((c, tagged_thm :: old_thms), result))
clasohm@1132
    87
            end;
clasohm@1262
    88
clasohm@1262
    89
      val const_idx' = update_db false consts const_idx;
berghofe@1580
    90
  in if consts = [] then warning ("Theorem " ^ name ^
clasohm@1136
    91
                                  " cannot be stored in ThmDB\n\t because it \
clasohm@1136
    92
                                  \contains no or only ignored constants.")
clasohm@1262
    93
     else if is_some const_idx' then
clasohm@1262
    94
       thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
clasohm@1262
    95
                        const_idx = the const_idx'}
clasohm@1262
    96
     else ();
clasohm@1236
    97
     thm
clasohm@1132
    98
  end;
clasohm@1132
    99
clasohm@1272
   100
(*Remove all theorems with given signature from database*)
clasohm@1262
   101
fun delete_thm_db thy =
clasohm@1262
   102
  let
clasohm@1262
   103
    val sign = sign_of thy;
clasohm@1262
   104
clasohm@1262
   105
    val ThmDB {count, thy_idx, const_idx} = !thm_db;
clasohm@1262
   106
clasohm@1272
   107
    (*Remove theory from thy_idx and get the data associated with it*)
clasohm@1262
   108
    fun update_thys [] result = (result, [], [])
clasohm@1262
   109
      | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
clasohm@1262
   110
                    result =
clasohm@1262
   111
          if Sign.eq_sg (sign, thy_sign) then
clasohm@1262
   112
            (result @ ts, thy_consts, thy_nums)
clasohm@1262
   113
          else update_thys ts (thy :: result);
clasohm@1262
   114
clasohm@1262
   115
    val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
clasohm@1262
   116
clasohm@1272
   117
    (*Remove all theorems belonging to a theory*)
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@1272
   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@1272
   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
berghofe@1654
   202
      fun substsize(prop, tsig) =
berghofe@1654
   203
            let val Some pat = extract prop
berghofe@1654
   204
                val (_,subst) = Pattern.match tsig (pat,obj)
paulson@2150
   205
            in foldl op+
paulson@2150
   206
		(0, map (fn (_,t) => size_of_term t) subst)
paulson@2150
   207
            end
berghofe@1654
   208
berghofe@1654
   209
      fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
berghofe@1654
   210
            (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
berghofe@1654
   211
            orelse (p0=0 andalso p1<>0)
berghofe@1654
   212
clasohm@1262
   213
      fun select((p as (_,thm))::named_thms, sels) =
clasohm@1262
   214
            let val {prop, sign, ...} = rep_thm thm
nipkow@1221
   215
            in select(named_thms,
clasohm@1262
   216
                      if Sign.subsig(sign, signobj) andalso
nipkow@1230
   217
                         matches(prop,#tsig(Sign.rep_sg signobj))
berghofe@1654
   218
                      then
berghofe@1654
   219
			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
berghofe@1654
   220
                      else sels)
clasohm@1136
   221
            end
clasohm@1136
   222
        | select([],sels) = sels
nipkow@1221
   223
berghofe@1654
   224
  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
nipkow@1221
   225
nipkow@1221
   226
fun find_matching(prop,sign,index,extract) =
nipkow@1221
   227
  (case top_const prop of
nipkow@1221
   228
     Some c => select_match(prop,sign,index c,extract)
nipkow@1221
   229
   | _      => []);
nipkow@1221
   230
nipkow@1221
   231
fun find_intros(prop,sign) =
nipkow@1221
   232
  find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
clasohm@1136
   233
nipkow@1221
   234
fun find_elims sign prop =
nipkow@1221
   235
  let fun major prop = case Logic.strip_imp_prems prop of
nipkow@1221
   236
                         [] => None | p::_ => Some p
nipkow@1221
   237
  in find_matching(prop,sign,index_elims,major) end;
nipkow@1221
   238
nipkow@1221
   239
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
nipkow@1221
   240
nipkow@1221
   241
fun findEs i =
nipkow@1230
   242
  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
nipkow@1230
   243
      val sign = #sign(rep_thm(topthm()))
nipkow@1230
   244
      val thmss = map (find_elims sign) (prems_of_goal i)
nipkow@1230
   245
  in foldl (gen_union eq_nth) ([],thmss) end;
nipkow@1221
   246
nipkow@1221
   247
fun findE i j =
nipkow@1221
   248
  let val sign = #sign(rep_thm(topthm()))
nipkow@1221
   249
  in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
nipkow@1221
   250
clasohm@1132
   251
end;