src/Pure/Thy/thm_database.ML
changeset 3601 43c7912aac8d
parent 2150 084218afaf4b
child 3627 3d0d5f2a2e33
     1.1 --- a/src/Pure/Thy/thm_database.ML	Wed Aug 06 00:15:14 1997 +0200
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Wed Aug 06 00:18:34 1997 +0200
     1.3 @@ -23,11 +23,27 @@
     1.4    val findI:         int -> (string * thm)list
     1.5    val findEs:        int -> (string * thm)list
     1.6    val findE:  int -> int -> (string * thm)list
     1.7 +
     1.8 +  val store_thm      : string * thm -> thm
     1.9 +  val bind_thm       : string * thm -> unit
    1.10 +  val qed            : string -> unit
    1.11 +  val qed_thm        : thm ref
    1.12 +  val qed_goal       : string -> theory -> string 
    1.13 +                       -> (thm list -> tactic list) -> unit
    1.14 +  val qed_goalw      : string -> theory -> thm list -> string 
    1.15 +                       -> (thm list -> tactic list) -> unit
    1.16 +  val get_thm        : theory -> string -> thm
    1.17 +  val thms_of        : theory -> (string * thm) list
    1.18 +  val delete_thms    : string -> unit
    1.19 +
    1.20 +  val print_theory   : theory -> unit
    1.21    end;
    1.22  
    1.23 -functor ThmDBFun(): THMDB =
    1.24 +structure ThmDB: THMDB =
    1.25  struct
    1.26  
    1.27 +open ThyInfo BrowserInfo;
    1.28 +
    1.29  (*** ignore and top_const could be turned into functor-parameters, but are
    1.30  currently identical for all object logics ***)
    1.31  
    1.32 @@ -248,4 +264,131 @@
    1.33    let val sign = #sign(rep_thm(topthm()))
    1.34    in find_elims sign (nth_elem(j-1, prems_of_goal i)) end;
    1.35  
    1.36 +
    1.37 +(*** Store and retrieve theorems ***)
    1.38 +
    1.39 +(** Store theorems **)
    1.40 +
    1.41 +(*Store a theorem in the thy_info of its theory,
    1.42 +  and in the theory's HTML file*)
    1.43 +fun store_thm (name, thm) =
    1.44 +  let
    1.45 +    val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
    1.46 +                            theory, thms, methods, data}) =
    1.47 +      thyinfo_of_sign (#sign (rep_thm thm))
    1.48 +
    1.49 +    val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
    1.50 +      handle Symtab.DUPLICATE s => 
    1.51 +        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
    1.52 +           (warning ("Theory database already contains copy of\
    1.53 +                     \ theorem " ^ quote name);
    1.54 +            (thms, true))
    1.55 +         else error ("Duplicate theorem name " ^ quote s
    1.56 +                     ^ " used in theory database"));
    1.57 +
    1.58 +    (*Label this theorem*)
    1.59 +    val thm' = Thm.name_thm (name, thm)
    1.60 +  in
    1.61 +    loaded_thys := Symtab.update
    1.62 +     ((thy_name, ThyInfo {path = path, children = children, parents = parents,
    1.63 +                          thy_time = thy_time, ml_time = ml_time,
    1.64 +                          theory = theory, thms = thms',
    1.65 +                          methods = methods, data = data}),
    1.66 +      !loaded_thys);
    1.67 +    thm_to_html thm name;
    1.68 +    if duplicate then thm' else store_thm_db (name, thm')
    1.69 +  end;
    1.70 +
    1.71 +
    1.72 +(*Store result of proof in loaded_thys and as ML value*)
    1.73 +
    1.74 +val qed_thm = ref flexpair_def(*dummy*);
    1.75 +
    1.76 +
    1.77 +fun bind_thm (name, thm) =
    1.78 + (qed_thm := store_thm (name, (standard thm));
    1.79 +  use_string ["val " ^ name ^ " = !qed_thm;"]);
    1.80 +
    1.81 +
    1.82 +fun qed name =
    1.83 + (qed_thm := store_thm (name, result ());
    1.84 +  use_string ["val " ^ name ^ " = !qed_thm;"]);
    1.85 +
    1.86 +
    1.87 +fun qed_goal name thy agoal tacsf =
    1.88 + (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
    1.89 +  use_string ["val " ^ name ^ " = !qed_thm;"]);
    1.90 +
    1.91 +
    1.92 +fun qed_goalw name thy rths agoal tacsf =
    1.93 + (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
    1.94 +  use_string ["val " ^ name ^ " = !qed_thm;"]);
    1.95 +
    1.96 +
    1.97 +(** Retrieve theorems **)
    1.98 +
    1.99 +(*Get all theorems belonging to a given theory*)
   1.100 +fun thmtab_of_thy thy =
   1.101 +  let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
   1.102 +  in thms end;
   1.103 +
   1.104 +
   1.105 +fun thmtab_of_name name =
   1.106 +  let val ThyInfo {thms, ...} = the (get_thyinfo name);
   1.107 +  in thms end;
   1.108 +
   1.109 +
   1.110 +(*Get a stored theorem specified by theory and name. *)
   1.111 +fun get_thm thy name =
   1.112 +  let fun get [] [] searched =
   1.113 +           raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
   1.114 +        | get [] ng searched =
   1.115 +            get (ng \\ searched) [] searched
   1.116 +        | get (t::ts) ng searched =
   1.117 +            (case Symtab.lookup (thmtab_of_name t, name) of
   1.118 +                 Some thm => thm
   1.119 +               | None => get ts (ng union (parents_of_name t)) (t::searched));
   1.120 +
   1.121 +      val (tname, _) = thyinfo_of_sign (sign_of thy);
   1.122 +  in get [tname] [] [] end;
   1.123 +
   1.124 +
   1.125 +(*Get stored theorems of a theory (original derivations) *)
   1.126 +val thms_of = Symtab.dest o thmtab_of_thy;
   1.127 +
   1.128 +
   1.129 +(*Remove theorems associated with a theory from theory and theorem database*)
   1.130 +fun delete_thms tname =
   1.131 +  let
   1.132 +    val tinfo = case get_thyinfo tname of
   1.133 +        Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
   1.134 +                       methods, data, ...}) =>
   1.135 +          ThyInfo {path = path, children = children, parents = parents,
   1.136 +                   thy_time = thy_time, ml_time = ml_time,
   1.137 +                   theory = theory, thms = Symtab.null,
   1.138 +                   methods = methods, data = data}
   1.139 +      | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.140 +
   1.141 +    val ThyInfo {theory, ...} = tinfo;
   1.142 +  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
   1.143 +     case theory of
   1.144 +         Some t => delete_thm_db t
   1.145 +       | None => ()
   1.146 +  end;
   1.147 +
   1.148 +
   1.149 +(*** Print theory ***)
   1.150 +
   1.151 +fun print_thms thy =
   1.152 +  let
   1.153 +    val thms = thms_of thy;
   1.154 +    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
   1.155 +      Pretty.quote (pretty_thm th)];
   1.156 +  in
   1.157 +    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
   1.158 +  end;
   1.159 +
   1.160 +
   1.161 +fun print_theory thy = (Display.print_theory thy; print_thms thy);
   1.162 +
   1.163  end;