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