force new theory
This procedure is for making a new theory in a context where a previous version of the same theory could be present and if
so should be deleted (even if it has children).
xlsml
fun force_new_theory name =
let
val _ = force_delete_theory name handle _ => ();
in
new_theory name
end;


force new proof context
This procedure is for making a new pc in a context where a previous version of the pc could be present and if so should be
deleted.
xlsml
fun force_new_pc name =
let
val _ = delete_pc name handle _ => ();
in
new_pc name
end;


Adding new theorems
The following procedure just abbreviates the process of adding one or more theorems for rewriting and for stripping.

Consistency Proofs
To permit hand consistency proofs to be completed before a HOLCONST specification we provide a consistency prover which just
looks up a standard location for the consistency proof and put this in a proof context.

Trawling for helpful theorems and definitions
To make it easier to find things relevant to the current goal.
xlsml
set_goal([], ⌜0=1 ∧ F⌝);
val avoid_theories = ref ["min", "log"];
val avoid_constants = ref ["=", "∧"];
val avoid_specs = ref ["=", "∧"];
fun defined_consts t = let val consts = term_consts t in filter (fn x => (fst x) mem ["=", "ε", "⇒"]) consts end;
fun on_goal_conc f = f (snd (top_goal()));
fun term_const_defns t =
letval consts = defined_consts t; fun cd c = get_defn (get_const_theory c) c
in map (cd o fst) consts
end;
fun goal_defns void =
term_const_defns(snd(top_goal()));
fun term_const_specs t =
letval consts = defined_consts t
in map (get_spec o mk_const) consts
end;
fun goal_specs void =
term_const_specs(snd(top_goal()));
fun const_thms c =
let val allthms = get_thms (get_const_theory c)
in allthms
end;
fun goal_const_thms void =
let val consts = term_consts (snd(top_goal()))
in map (const_thms o fst) consts
end;
fun get_thml th kl = map (get_thm th) kl;
fun get_thml2 thkl =
foldl (op @) [] (map (fn (th, kl) => get_thml th kl) thkl);
fun get_keys th l =
let val thms = get_thms th
in map (fn chose => (hd o fst o chose) thms) (map nth l)
end;
fun no_map f l =
let fun g n f [] = []
 g n f (h::t) = f n h :: (g (n+1) f t)
in g 0 f l
end;
fun get_num_thms th =
no_map (fn x => fn t => (x,t)) (get_thms th);
(* get_thml "" ["tc_mono_thm", "tran_tc_thm2"];
get_thml2 [("", ["tc_mono_thm", "tran_tc_thm2"])];
*)
fun term_const_thms t =
letval consts = term_consts t
in map (get_spec o mk_const) consts
end;

