(* Title: Pure/Thy/thm_database.ML
ID: $Id$
Author: Carsten Clasohm and Tobias Nipkow
Copyright 1995 TU Muenchen
*)
datatype thm_db =
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 THM_DATABASE =
sig
val thm_db: thm_db 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
val store_thm : string * thm -> thm
val bind_thm : string * thm -> unit
val qed : string -> unit
val qed_thm : thm ref
val qed_goal : string -> theory -> string
-> (thm list -> tactic list) -> unit
val qed_goalw : string -> theory -> thm list -> string
-> (thm list -> tactic list) -> unit
val get_thm : theory -> string -> thm
val thms_of : theory -> (string * thm) list
val delete_thms : string -> unit
val print_theory : theory -> unit
end;
structure ThmDatabase: THM_DATABASE =
struct
open ThyInfo BrowserInfo;
(*** 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;
(*** Store and retrieve theorems ***)
(** Store theorems **)
(*Store a theorem in the thy_info of its theory,
and in the theory's HTML file*)
fun store_thm (name, thm) =
let
val (thy_name, {path, children, parents, thy_time, ml_time,
theory, thms, methods, data}) =
thyinfo_of_sign (#sign (rep_thm thm))
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
handle Symtab.DUPLICATE s =>
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then
(warning ("Theory database already contains copy of\
\ theorem " ^ quote name);
(thms, true))
else error ("Duplicate theorem name " ^ quote s
^ " used in theory database"));
(*Label this theorem*)
val thm' = Thm.name_thm (name, thm)
in
loaded_thys := Symtab.update
((thy_name, {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms',
methods = methods, data = data}),
!loaded_thys);
thm_to_html thm name;
if duplicate then thm' else store_thm_db (name, thm')
end;
(*Store result of proof in loaded_thys and as ML value*)
val qed_thm = ref flexpair_def(*dummy*);
fun bind_thm (name, thm) =
(qed_thm := store_thm (name, (standard thm));
use_strings ["val " ^ name ^ " = !qed_thm;"]);
fun qed name =
(qed_thm := store_thm (name, result ());
use_strings ["val " ^ name ^ " = !qed_thm;"]);
fun qed_goal name thy agoal tacsf =
(qed_thm := store_thm (name, prove_goal thy agoal tacsf);
use_strings ["val " ^ name ^ " = !qed_thm;"]);
fun qed_goalw name thy rths agoal tacsf =
(qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
use_strings ["val " ^ name ^ " = !qed_thm;"]);
(** Retrieve theorems **)
(*Get all theorems belonging to a given theory*)
fun thmtab_of_thy thy =
let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy);
in thms end;
fun thmtab_of_name name =
let val {thms, ...} = the (get_thyinfo name);
in thms end;
(*Get a stored theorem specified by theory and name. *)
fun get_thm thy name =
let fun get [] [] searched =
raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
| get [] ng searched =
get (ng \\ searched) [] searched
| get (t::ts) ng searched =
(case Symtab.lookup (thmtab_of_name t, name) of
Some thm => thm
| None => get ts (ng union (parents_of_name t)) (t::searched));
val (tname, _) = thyinfo_of_sign (sign_of thy);
in get [tname] [] [] end;
(*Get stored theorems of a theory (original derivations) *)
val thms_of = Symtab.dest o thmtab_of_thy;
(*Remove theorems associated with a theory from theory and theorem database*)
fun delete_thms tname =
let
val tinfo = case get_thyinfo tname of
Some ({path, children, parents, thy_time, ml_time, theory,
methods, data, ...}) =>
{path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = Symtab.null,
methods = methods, data = data}
| None => error ("Theory " ^ tname ^ " not stored by loader");
val {theory, ...} = tinfo;
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
case theory of
Some t => delete_thm_db t
| None => ()
end;
(*** Print theory ***)
fun print_thms thy =
let
val thms = thms_of thy;
fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
Pretty.quote (pretty_thm th)];
in
Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
end;
fun print_theory thy = (Display.print_theory thy; print_thms thy);
end;