(* Title: Pure/Thy/thm_database.ML
ID: $Id$
Author: Carsten Clasohm and Tobias Nipkow
Copyright 1995 TU Muenchen
*)
datatype thm_db_type =
ThmDB of {count: int,
thy_idx: (Sign.sg * (string list * int list)) list,
const_idx: ((int * (string * thm)) list) Symtab.table};
(*count: number of theorems in database (used as unique ID for next thm)
thy_idx: constants and IDs of theorems
indexed by the theory's signature they belong to
const_idx: named theorems tagged by numbers and
indexed by the constants they contain*)
signature THMDB =
sig
val thm_db: thm_db_type ref
val store_thm_db: string * thm -> thm
val delete_thm_db: theory -> unit
val thms_containing: string list -> (string * thm) list
val findI: int -> (string * thm)list
val findEs: int -> (string * thm)list
val findE: int -> int -> (string * thm)list
end;
functor ThmDBFun(): THMDB =
struct
(*** ignore and top_const could be turned into functor-parameters, but are
currently identical for all object logics ***)
(* Constants not to be used for theorem indexing *)
val ignore = ["Trueprop", "all", "==>", "=="];
(* top_const: main constant, ignoring Trueprop *)
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
| _ => None)
| top_const _ = None;
(*Symtab which associates a constant with a list of theorems that contain the
constant (theorems are tagged with numbers)*)
val thm_db = ref (ThmDB
{count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
(*List all relevant constants a term contains*)
fun list_consts t =
let fun consts (Const (c, _)) = if c mem ignore then [] else [c]
| consts (Free _) = []
| consts (Var _) = []
| consts (Bound _) = []
| consts (Abs (_, _, t)) = consts t
| consts (t1$t2) = (consts t1) union (consts t2);
in distinct (consts t) end;
(*Store a theorem in database*)
fun store_thm_db (named_thm as (name, thm)) =
let val {prop, hyps, sign, ...} = rep_thm thm;
val consts = distinct (flat (map list_consts (prop :: hyps)));
val ThmDB {count, thy_idx, const_idx} = !thm_db;
fun update_thys [] = [(sign, (consts, [count]))]
| update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
if Sign.eq_sg (sign, thy_sign) then
(thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
else thy :: update_thys ts;
val tagged_thm = (count, named_thm);
fun update_db _ [] result = Some result
| update_db checked (c :: cs) result =
let
val old_thms = Symtab.lookup_multi (result, c);
val duplicate =
if checked then false
else case find_first (fn (_, (n, _)) => n = name) old_thms of
Some (_, (_, t)) => eq_thm (t, thm)
| None => false
in if duplicate then None
else update_db true
cs (Symtab.update ((c, tagged_thm :: old_thms), result))
end;
val const_idx' = update_db false consts const_idx;
in if consts = [] then warning ("Theorem " ^ name ^
" cannot be stored in ThmDB\n\t because it \
\contains no or only ignored constants.")
else if is_some const_idx' then
thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
const_idx = the const_idx'}
else ();
thm
end;
(*Remove all theorems with given signature from database*)
fun delete_thm_db thy =
let
val sign = sign_of thy;
val ThmDB {count, thy_idx, const_idx} = !thm_db;
(*Remove theory from thy_idx and get the data associated with it*)
fun update_thys [] result = (result, [], [])
| update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
result =
if Sign.eq_sg (sign, thy_sign) then
(result @ ts, thy_consts, thy_nums)
else update_thys ts (thy :: result);
val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
(*Remove all theorems belonging to a theory*)
fun update_db [] result = result
| update_db (c :: cs) result =
let val thms' = filter_out (fn (num, _) => num mem thy_nums)
(Symtab.lookup_multi (result, c));
in update_db cs (Symtab.update ((c, thms'), result)) end;
in thm_db := ThmDB {count = count, thy_idx = thy_idx',
const_idx = update_db thy_consts const_idx}
end;
(*Intersection of two theorem lists with descending tags*)
infix desc_inter;
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
| xs desc_inter [] = []
| (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
if xi = yi then x :: (xs desc_inter ys)
else if xi > yi then xs desc_inter yss
else xss desc_inter ys;
(*Get all theorems from database that contain a list of constants*)
fun thms_containing constants =
let fun collect [] _ result = map snd result
| collect (c :: cs) first result =
let val ThmDB {const_idx, ...} = !thm_db;
val new_thms = Symtab.lookup_multi (const_idx, c);
in collect cs false (if first then new_thms
else (result desc_inter new_thms))
end;
val look_for = constants \\ ignore;
in if null look_for then
error ("No or only ignored constants were specified for theorem \
\database search:\n " ^ commas (map quote ignore))
else ();
collect look_for true [] end;
val intro_const = top_const o concl_of;
fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p);
(* In case faster access is necessary, the thm db should provide special
functions
index_intros, index_elims: string -> (string * thm) list
where thm [| A1 ; ...; An |] ==> B is returned by
- index_intros c if B is of the form c t1 ... tn
- index_elims c if A1 is of the form c t1 ... tn
*)
(* could be provided by thm db *)
fun index_intros c =
let fun topc(_,thm) = intro_const thm = Some(c);
val named_thms = thms_containing [c]
in filter topc named_thms end;
(* could be provided by thm db *)
fun index_elims c =
let fun topc(_,thm) = elim_const thm = Some(c);
val named_thms = thms_containing [c]
in filter topc named_thms end;
(*assume that parameters have unique names*)
fun goal_params i =
let val gi = getgoal i
val frees = map Free (Logic.strip_params gi)
in (gi,frees) end;
fun concl_of_goal i =
let val (gi,frees) = goal_params i
val B = Logic.strip_assums_concl gi
in subst_bounds(frees,B) end;
fun prems_of_goal i =
let val (gi,frees) = goal_params i
val As = Logic.strip_assums_hyp gi
in map (fn A => subst_bounds(frees,A)) As end;
fun select_match(obj, signobj, named_thms, extract) =
let fun matches(prop, tsig) =
case extract prop of
None => false
| Some pat => Pattern.matches tsig (pat, obj);
fun substsize(prop, tsig) =
let val Some pat = extract prop
val (_,subst) = Pattern.match tsig (pat,obj)
in foldl op+
(0, map (fn (_,t) => size_of_term t) subst)
end
fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
(((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
orelse (p0=0 andalso p1<>0)
fun select((p as (_,thm))::named_thms, sels) =
let val {prop, sign, ...} = rep_thm thm
in select(named_thms,
if Sign.subsig(sign, signobj) andalso
matches(prop,#tsig(Sign.rep_sg signobj))
then
(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
else sels)
end
| select([],sels) = sels
in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end;
fun find_matching(prop,sign,index,extract) =
(case top_const prop of
Some c => select_match(prop,sign,index c,extract)
| _ => []);
fun find_intros(prop,sign) =
find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl);
fun find_elims sign prop =
let fun major prop = case Logic.strip_imp_prems prop of
[] => None | p::_ => Some p
in find_matching(prop,sign,index_elims,major) end;
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
fun findEs i =
let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
val sign = #sign(rep_thm(topthm()))
val thmss = map (find_elims sign) (prems_of_goal i)
in foldl (gen_union eq_nth) ([],thmss) end;
fun findE i j =
let val sign = #sign(rep_thm(topthm()))
in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
end;