src/Pure/Thy/thm_database.ML

tuned;

(*  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;