# HG changeset patch # User wenzelm # Date 1325242810 -3600 # Node ID 963af563a1328190a7768b99025b85878b701dbf # Parent 1e184c0d88be43f471c7598ab21011e18b4ac9fe tuned; diff -r 1e184c0d88be -r 963af563a132 src/HOL/Tools/record.ML --- 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