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);
     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   | top_const _ = None;
    41 
    42 (*Symtab which associates a constant with a list of theorems that contain the
    43   constant (theorems are tagged with numbers)*)
    44 val thm_db = ref (ThmDB
    45  {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
    46   const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
    47 
    48 (*List all relevant constants a term contains*)
    49 fun list_consts t =
    50   let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
    51         | consts (Free _) = []
    52         | consts (Var _) = []
    53         | consts (Bound _) = []
    54         | consts (Abs (_, _, t)) = consts t
    55         | consts (t1$t2) = (consts t1) union (consts t2);
    56   in distinct (consts t) end;
    57 
    58 (*Store a theorem in database*)
    59 fun store_thm_db (named_thm as (name, thm)) =
    60   let val {prop, hyps, sign, ...} = rep_thm thm;
    61 
    62       val consts = distinct (flat (map list_consts (prop :: hyps)));
    63 
    64       val ThmDB {count, thy_idx, const_idx} = !thm_db;
    65 
    66       fun update_thys [] = [(sign, (consts, [count]))]
    67         | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
    68             if Sign.eq_sg (sign, thy_sign) then
    69               (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
    70             else thy :: update_thys ts;
    71 
    72       val tagged_thm = (count, named_thm);
    73 
    74       fun update_db _ [] result = Some result
    75         | update_db checked (c :: cs) result =
    76             let
    77               val old_thms = Symtab.lookup_multi (result, c);
    78 
    79               val duplicate =
    80                 if checked then false
    81                 else case find_first (fn (_, (n, _)) => n = name) old_thms of
    82                        Some (_, (_, t)) => eq_thm (t, thm)
    83                      | None => false
    84             in if duplicate then None
    85                else update_db true
    86                       cs (Symtab.update ((c, tagged_thm :: old_thms), result))
    87             end;
    88 
    89       val const_idx' = update_db false consts const_idx;
    90   in if consts = [] then warning ("Theorem " ^ name ^
    91                                   " cannot be stored in ThmDB\n\t because it \
    92                                   \contains no or only ignored constants.")
    93      else if is_some const_idx' then
    94        thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
    95                         const_idx = the const_idx'}
    96      else ();
    97      thm
    98   end;
    99 
   100 (*Remove all theorems with given signature from database*)
   101 fun delete_thm_db thy =
   102   let
   103     val sign = sign_of thy;
   104 
   105     val ThmDB {count, thy_idx, const_idx} = !thm_db;
   106 
   107     (*Remove theory from thy_idx and get the data associated with it*)
   108     fun update_thys [] result = (result, [], [])
   109       | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
   110                     result =
   111           if Sign.eq_sg (sign, thy_sign) then
   112             (result @ ts, thy_consts, thy_nums)
   113           else update_thys ts (thy :: result);
   114 
   115     val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
   116 
   117     (*Remove all theorems belonging to a theory*)
   118     fun update_db [] result = result
   119       | update_db (c :: cs) result =
   120         let val thms' = filter_out (fn (num, _) => num mem thy_nums)
   121                                    (Symtab.lookup_multi (result, c));
   122         in update_db cs (Symtab.update ((c, thms'), result)) end;
   123   in thm_db := ThmDB {count = count, thy_idx = thy_idx',
   124                       const_idx = update_db thy_consts const_idx}
   125   end;
   126 
   127 (*Intersection of two theorem lists with descending tags*)
   128 infix desc_inter;
   129 fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
   130   | xs desc_inter [] = []
   131   | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
   132       if xi = yi then x :: (xs desc_inter ys)
   133       else if xi > yi then xs desc_inter yss
   134       else xss desc_inter ys;
   135 
   136 (*Get all theorems from database that contain a list of constants*)
   137 fun thms_containing constants =
   138   let fun collect [] _ result = map snd result
   139         | collect (c :: cs) first result =
   140             let val ThmDB {const_idx, ...} = !thm_db;
   141 
   142                 val new_thms = Symtab.lookup_multi (const_idx, c);
   143             in collect cs false (if first then new_thms
   144                                           else (result desc_inter new_thms))
   145             end;
   146 
   147       val look_for = constants \\ ignore;
   148   in if null look_for then
   149        error ("No or only ignored constants were specified for theorem \
   150               \database search:\n  " ^ commas (map quote ignore))
   151      else ();
   152      collect look_for true [] end;
   153 
   154 val intro_const = top_const o concl_of;
   155 
   156 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
   157 
   158 (* In case faster access is necessary, the thm db should provide special
   159 functions
   160 
   161 index_intros, index_elims: string -> (string * thm) list
   162 
   163 where thm [| A1 ; ...; An |] ==> B is returned by
   164 - index_intros c if B  is of the form c t1 ... tn
   165 - index_elims c  if A1 is of the form c t1 ... tn
   166 *)
   167 
   168 (* could be provided by thm db *)
   169 fun index_intros c =
   170   let fun topc(_,thm) = intro_const thm = Some(c);
   171       val named_thms = thms_containing [c]
   172   in filter topc named_thms end;
   173 
   174 (* could be provided by thm db *)
   175 fun index_elims c =
   176   let fun topc(_,thm) = elim_const thm = Some(c);
   177       val named_thms = thms_containing [c]
   178   in filter topc named_thms end;
   179 
   180 (*assume that parameters have unique names*)
   181 fun goal_params i =
   182   let val gi = getgoal i
   183       val frees = map Free (Logic.strip_params gi)
   184   in (gi,frees) end;
   185 
   186 fun concl_of_goal i =
   187   let val (gi,frees) = goal_params i
   188       val B = Logic.strip_assums_concl gi
   189   in subst_bounds(frees,B) end;
   190 
   191 fun prems_of_goal i =
   192   let val (gi,frees) = goal_params i
   193       val As = Logic.strip_assums_hyp gi
   194   in map (fn A => subst_bounds(frees,A)) As end;
   195 
   196 fun select_match(obj, signobj, named_thms, extract) =
   197   let fun matches(prop, tsig) =
   198             case extract prop of
   199               None => false
   200             | Some pat => Pattern.matches tsig (pat, obj);
   201 
   202       fun substsize(prop, tsig) =
   203             let val Some pat = extract prop
   204                 val (_,subst) = Pattern.match tsig (pat,obj)
   205             in foldl op+
   206 		(0, map (fn (_,t) => size_of_term t) subst)
   207             end
   208 
   209       fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
   210             (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
   211             orelse (p0=0 andalso p1<>0)
   212 
   213       fun select((p as (_,thm))::named_thms, sels) =
   214             let val {prop, sign, ...} = rep_thm thm
   215             in select(named_thms,
   216                       if Sign.subsig(sign, signobj) andalso
   217                          matches(prop,#tsig(Sign.rep_sg signobj))
   218                       then
   219 			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
   220                       else sels)
   221             end
   222         | select([],sels) = sels
   223 
   224   in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
   225 
   226 fun find_matching(prop,sign,index,extract) =
   227   (case top_const prop of
   228      Some c => select_match(prop,sign,index c,extract)
   229    | _      => []);
   230 
   231 fun find_intros(prop,sign) =
   232   find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
   233 
   234 fun find_elims sign prop =
   235   let fun major prop = case Logic.strip_imp_prems prop of
   236                          [] => None | p::_ => Some p
   237   in find_matching(prop,sign,index_elims,major) end;
   238 
   239 fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
   240 
   241 fun findEs i =
   242   let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
   243       val sign = #sign(rep_thm(topthm()))
   244       val thmss = map (find_elims sign) (prems_of_goal i)
   245   in foldl (gen_union eq_nth) ([],thmss) end;
   246 
   247 fun findE i j =
   248   let val sign = #sign(rep_thm(topthm()))
   249   in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
   250 
   251 end;