1.1 --- a/src/HOL/Tools/record.ML Thu Dec 29 20:32:59 2011 +0100
1.2 +++ b/src/HOL/Tools/record.ML Fri Dec 30 12:00:10 2011 +0100
1.3 @@ -1331,11 +1331,6 @@
1.4 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1.5 (fn thy => fn ss => fn t =>
1.6 let
1.7 - fun prove prop =
1.8 - Skip_Proof.prove_global thy [] [] prop
1.9 - (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1.10 - addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
1.11 -
1.12 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1.13 if is_selector thy sel then
1.14 let
1.15 @@ -1362,8 +1357,11 @@
1.16 list_all ([("r", T)],
1.17 Logic.mk_equals
1.18 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
1.19 - in SOME (prove prop) end
1.20 - handle TERM _ => NONE)
1.21 + in
1.22 + SOME (Skip_Proof.prove_global thy [] [] prop
1.23 + (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1.24 + addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
1.25 + end handle TERM _ => NONE)
1.26 | _ => NONE)
1.27 end);
1.28
1.29 @@ -1605,11 +1603,9 @@
1.30 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1.31 end;
1.32
1.33 - val prove = Skip_Proof.prove_global defs_thy;
1.34 -
1.35 val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
1.36 simplify HOL_ss
1.37 - (prove [] [] inject_prop
1.38 + (Skip_Proof.prove_global defs_thy [] [] inject_prop
1.39 (fn _ =>
1.40 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1.41 REPEAT_DETERM
1.42 @@ -1641,7 +1637,7 @@
1.43
1.44
1.45 val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
1.46 - prove [] [] split_meta_prop
1.47 + Skip_Proof.prove_global defs_thy [] [] split_meta_prop
1.48 (fn _ =>
1.49 EVERY1
1.50 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1.51 @@ -1651,7 +1647,7 @@
1.52
1.53 val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
1.54 let val (assm, concl) = induct_prop in
1.55 - prove [] [assm] concl
1.56 + Skip_Proof.prove_global defs_thy [] [assm] concl
1.57 (fn {prems, ...} =>
1.58 cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
1.59 resolve_tac prems 2 THEN
1.60 @@ -2126,17 +2122,17 @@
1.61
1.62 (* 3rd stage: thms_thy *)
1.63
1.64 - val prove = Skip_Proof.prove_global defs_thy;
1.65 -
1.66 val ss = get_simpset defs_thy;
1.67 val simp_defs_tac =
1.68 asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
1.69
1.70 val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () =>
1.71 - map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
1.72 + map (fn prop =>
1.73 + Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
1.74
1.75 val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () =>
1.76 - map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
1.77 + map (fn prop =>
1.78 + Skip_Proof.prove_global defs_thy [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
1.79
1.80 val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
1.81 let
1.82 @@ -2148,7 +2144,7 @@
1.83 val parent_induct = Option.map #induct_scheme (try List.last parents);
1.84
1.85 val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
1.86 - prove [] [] induct_scheme_prop
1.87 + Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop
1.88 (fn _ =>
1.89 EVERY
1.90 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
1.91 @@ -2157,7 +2153,7 @@
1.92
1.93 val induct = timeit_msg ctxt "record induct proof:" (fn () =>
1.94 let val (assm, concl) = induct_prop in
1.95 - prove [] [assm] concl (fn {prems, ...} =>
1.96 + Skip_Proof.prove_global defs_thy [] [assm] concl (fn {prems, ...} =>
1.97 try_param_tac rN induct_scheme 1
1.98 THEN try_param_tac "more" @{thm unit.induct} 1
1.99 THEN resolve_tac prems 1)
1.100 @@ -2177,7 +2173,7 @@
1.101 future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop);
1.102
1.103 val cases = timeit_msg ctxt "record cases proof:" (fn () =>
1.104 - prove [] [] cases_prop
1.105 + Skip_Proof.prove_global defs_thy [] [] cases_prop
1.106 (fn _ =>
1.107 try_param_tac rN cases_scheme 1 THEN
1.108 ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}]))));
1.109 @@ -2188,7 +2184,7 @@
1.110 get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
1.111 val init_ss = HOL_basic_ss addsimps ext_defs;
1.112 in
1.113 - prove [] [] surjective_prop
1.114 + Skip_Proof.prove_global defs_thy [] [] surjective_prop
1.115 (fn _ =>
1.116 EVERY
1.117 [rtac surject_assist_idE 1,
1.118 @@ -2199,7 +2195,7 @@
1.119 end);
1.120
1.121 val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
1.122 - prove [] [] split_meta_prop
1.123 + Skip_Proof.prove_global defs_thy [] [] split_meta_prop
1.124 (fn _ =>
1.125 EVERY1
1.126 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1.127 @@ -2240,7 +2236,7 @@
1.128 val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
1.129 val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
1.130 val so'' = simplify ss so';
1.131 - in prove [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
1.132 + in Skip_Proof.prove_global defs_thy [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
1.133
1.134 fun equality_tac thms =
1.135 let
1.136 @@ -2250,7 +2246,7 @@
1.137 in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
1.138
1.139 val equality = timeit_msg ctxt "record equality proof:" (fn () =>
1.140 - prove [] [] equality_prop (fn {context, ...} =>
1.141 + Skip_Proof.prove_global defs_thy [] [] equality_prop (fn {context, ...} =>
1.142 fn st =>
1.143 let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
1.144 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN