Extra sml procedures for ProofPower

The available proof context facilities are a bit cumbersome if you want to build up a proof context incrementatlly as you work your way through a theory. Here are some hacks to make that easier.

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).

xl-sml

fun force_new_theory name =
let
val _ = force_delete_theory name handle _ => ();
in
new_theory name
end;

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.

xl-sml

fun force_new_pc name =
let
val _ = delete_pc name handle _ => ();
in
new_pc name
end;

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

xl-sml

fun add_pc_thms pc thms =

(add_rw_thms thms pc;

add_sc_thms thms pc;

add_st_thms thms pc);

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.

xl-sml

open_theory "basic_hol";
val xl_consistency_result = ref t_thm;
fun xl_cs_∃_conv x =

if x =$ (concl(!xl_consistency_result))

then ≡_t_intro (!xl_consistency_result)

else eq_sym_conv x;
force_new_pc "xl_cs_∃_conv";
set_cs_∃_convs [xl_cs_∃_conv] "xl_cs_∃_conv";
set_pr_conv basic_prove_conv "xl_cs_∃_conv";
set_pr_tac basic_prove_tac "xl_cs_∃_conv";
commit_pc "xl_cs_∃_conv";
fun xl_set_cs_∃_thm thm = (xl_consistency_result := thm);

To make it easier to find things relevant to the current goal.

xl-sml

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 =

let

val 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 =

let

val 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 =

let

val consts = term_consts t

in map (get_spec o mk_const) consts

end;