--- a/src/HOL/Tools/record.ML Thu Dec 29 20:32:59 2011 +0100
+++ b/src/HOL/Tools/record.ML Fri Dec 30 12:00:10 2011 +0100
@@ -1331,11 +1331,6 @@
Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
- fun prove prop =
- Skip_Proof.prove_global thy [] [] prop
- (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
- addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
-
fun mkeq (lr, Teq, (sel, Tsel), x) i =
if is_selector thy sel then
let
@@ -1362,8 +1357,11 @@
list_all ([("r", T)],
Logic.mk_equals
(Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
- in SOME (prove prop) end
- handle TERM _ => NONE)
+ in
+ SOME (Skip_Proof.prove_global thy [] [] prop
+ (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
+ addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
+ end handle TERM _ => NONE)
| _ => NONE)
end);
@@ -1605,11 +1603,9 @@
(All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
end;
- val prove = Skip_Proof.prove_global defs_thy;
-
val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
simplify HOL_ss
- (prove [] [] inject_prop
+ (Skip_Proof.prove_global defs_thy [] [] inject_prop
(fn _ =>
simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
REPEAT_DETERM
@@ -1641,7 +1637,7 @@
val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
- prove [] [] split_meta_prop
+ Skip_Proof.prove_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
[rtac equal_intr_rule, Goal.norm_hhf_tac,
@@ -1651,7 +1647,7 @@
val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
- prove [] [assm] concl
+ Skip_Proof.prove_global defs_thy [] [assm] concl
(fn {prems, ...} =>
cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
resolve_tac prems 2 THEN
@@ -2126,17 +2122,17 @@
(* 3rd stage: thms_thy *)
- val prove = Skip_Proof.prove_global defs_thy;
-
val ss = get_simpset defs_thy;
val simp_defs_tac =
asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () =>
- map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
+ map (fn prop =>
+ Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () =>
- map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
+ map (fn prop =>
+ Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
let
@@ -2148,7 +2144,7 @@
val parent_induct = Option.map #induct_scheme (try List.last parents);
val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
- prove [] [] induct_scheme_prop
+ Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop
(fn _ =>
EVERY
[case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
@@ -2157,7 +2153,7 @@
val induct = timeit_msg ctxt "record induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
- prove [] [assm] concl (fn {prems, ...} =>
+ Skip_Proof.prove_global defs_thy [] [assm] concl (fn {prems, ...} =>
try_param_tac rN induct_scheme 1
THEN try_param_tac "more" @{thm unit.induct} 1
THEN resolve_tac prems 1)
@@ -2177,7 +2173,7 @@
future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop);
val cases = timeit_msg ctxt "record cases proof:" (fn () =>
- prove [] [] cases_prop
+ Skip_Proof.prove_global defs_thy [] [] cases_prop
(fn _ =>
try_param_tac rN cases_scheme 1 THEN
ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}]))));
@@ -2188,7 +2184,7 @@
get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
val init_ss = HOL_basic_ss addsimps ext_defs;
in
- prove [] [] surjective_prop
+ Skip_Proof.prove_global defs_thy [] [] surjective_prop
(fn _ =>
EVERY
[rtac surject_assist_idE 1,
@@ -2199,7 +2195,7 @@
end);
val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
- prove [] [] split_meta_prop
+ Skip_Proof.prove_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
[rtac equal_intr_rule, Goal.norm_hhf_tac,
@@ -2240,7 +2236,7 @@
val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
val so'' = simplify ss so';
- in prove [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
+ in Skip_Proof.prove_global defs_thy [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
fun equality_tac thms =
let
@@ -2250,7 +2246,7 @@
in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
val equality = timeit_msg ctxt "record equality proof:" (fn () =>
- prove [] [] equality_prop (fn {context, ...} =>
+ Skip_Proof.prove_global defs_thy [] [] equality_prop (fn {context, ...} =>
fn st =>
let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN