# HG changeset patch # User wenzelm # Date 1133471067 -3600 # Node ID 841261f303a19c9b85609efb0219e1c6fd7b544b # Parent 1ee4523c831f19e17596dfe94bb6f6a6357d451a simprocs: static evaluation of simpset; diff -r 1ee4523c831f -r 841261f303a1 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/Integ/int_arith1.ML Thu Dec 01 22:04:27 2005 +0100 @@ -308,9 +308,9 @@ fun trans_tac NONE = all_tac | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); -fun simplify_meta_eq rules ss = - simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) - o mk_meta_eq; +fun simplify_meta_eq rules = + let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules + in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end structure CancelNumeralsCommon = struct @@ -320,15 +320,18 @@ val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] val trans_tac = fn _ => trans_tac + + val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + diff_simps @ minus_simps @ add_ac + val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps + val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac fun norm_tac ss = - let val num_ss' = Simplifier.inherit_context ss num_ss in - ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ add_ac)) - THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps)) - THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s) end; @@ -398,15 +401,18 @@ val left_distrib = combine_common_factor RS trans val prove_conv = Bin_Simprocs.prove_conv_nohyps val trans_tac = fn _ => trans_tac + + val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + diff_simps @ minus_simps @ add_ac + val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps + val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac fun norm_tac ss = - let val num_ss' = Simplifier.inherit_context ss num_ss in - ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ add_ac)) - THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps)) - THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s) end; diff -r 1ee4523c831f -r 841261f303a1 src/HOL/Integ/int_factor_simprocs.ML --- a/src/HOL/Integ/int_factor_simprocs.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/Integ/int_factor_simprocs.ML Thu Dec 01 22:04:27 2005 +0100 @@ -43,14 +43,17 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val trans_tac = fn _ => trans_tac + + val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s + val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps + val norm_ss3 = HOL_ss addsimps mult_ac fun norm_tac ss = - let val HOL_ss' = Simplifier.inherit_context ss HOL_ss in - ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s)) - THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq [add_0, add_0_right, @@ -250,8 +253,8 @@ val dest_coeff = dest_coeff val find_first = find_first [] val trans_tac = fn _ => trans_tac - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac)) + val norm_ss = HOL_ss addsimps mult_1s @ mult_ac + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) end; (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in diff -r 1ee4523c831f -r 841261f303a1 src/HOL/Integ/nat_simprocs.ML --- a/src/HOL/Integ/nat_simprocs.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/Integ/nat_simprocs.ML Thu Dec 01 22:04:27 2005 +0100 @@ -169,14 +169,16 @@ val dest_coeff = dest_coeff val find_first_coeff = find_first_coeff [] val trans_tac = fn _ => trans_tac - fun norm_tac ss = - let val num_ss' = Simplifier.inherit_context ss num_ss in - ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @ - [Suc_eq_add_numeral_1_left] @ add_ac)) - THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps)) + + val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + [Suc_eq_add_numeral_1_left] @ add_ac + val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); val simplify_meta_eq = simplify_meta_eq end; @@ -254,14 +256,15 @@ val left_distrib = left_add_mult_distrib RS trans val prove_conv = Bin_Simprocs.prove_conv_nohyps val trans_tac = fn _ => trans_tac + + val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac + val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac fun norm_tac ss = - let val num_ss' = Simplifier.inherit_context ss num_ss in - ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @ - [Suc_eq_add_numeral_1] @ add_ac)) - THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = simplify_meta_eq end; @@ -278,14 +281,16 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff val trans_tac = fn _ => trans_tac + + val norm_ss1 = num_ss addsimps + numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac + val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac fun norm_tac ss = - let val num_ss' = Simplifier.inherit_context ss num_ss in - ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @ - [Suc_eq_add_numeral_1_left] @ add_ac)) - THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac)) - end - fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps bin_simps)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = simplify_meta_eq end @@ -371,8 +376,8 @@ val dest_coeff = dest_coeff val find_first = find_first [] val trans_tac = fn _ => trans_tac - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac)) + val norm_ss = HOL_ss addsimps mult_1s @ mult_ac + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) end; structure EqCancelFactor = ExtractCommonTermFun diff -r 1ee4523c831f -r 841261f303a1 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/Product_Type.thy Thu Dec 01 22:04:27 2005 +0100 @@ -401,7 +401,7 @@ ML_setup {* local - val cond_split_eta = thm "cond_split_eta"; + val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"] fun Pair_pat k 0 (Bound m) = (m = k) | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso m = k+i andalso Pair_pat k (i-1) t @@ -415,7 +415,7 @@ | split_pat tp i _ = NONE; fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))) - (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1))); + (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1))); fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse diff -r 1ee4523c831f -r 841261f303a1 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/Set.thy Thu Dec 01 22:04:27 2005 +0100 @@ -426,24 +426,17 @@ ML_setup {* local - val Ball_def = thm "Ball_def"; - val Bex_def = thm "Bex_def"; - - val simpset = Simplifier.clear_ss HOL_basic_ss; - fun unfold_tac ss th = - ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th])); - - fun prove_bex_tac ss = - unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac; + val unfold_bex_tac = unfold_tac [thm "Bex_def"]; + fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; - fun prove_ball_tac ss = - unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac; + val unfold_ball_tac = unfold_tac [thm "Ball_def"]; + fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; in - val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) + val defBEX_regroup = Simplifier.simproc (the_context ()) "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; - val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) + val defBALL_regroup = Simplifier.simproc (the_context ()) "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; end; diff -r 1ee4523c831f -r 841261f303a1 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/HOL/arith_data.ML Thu Dec 01 22:04:27 2005 +0100 @@ -59,8 +59,9 @@ (* rewriting *) -fun simp_all_tac rules ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules)); +fun simp_all_tac rules = + let val ss0 = HOL_ss addsimps rules + in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; @@ -89,7 +90,9 @@ val mk_sum = mk_norm_sum; val dest_sum = dest_sum; val prove_conv = prove_conv; - fun norm_tac ss = simp_all_tac add_rules ss THEN simp_all_tac add_ac ss; + val norm_tac1 = simp_all_tac add_rules; + val norm_tac2 = simp_all_tac add_ac; + fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; end; fun gen_uncancel_tac rule ct = diff -r 1ee4523c831f -r 841261f303a1 src/ZF/Integ/int_arith.ML --- a/src/ZF/Integ/int_arith.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/ZF/Integ/int_arith.ML Thu Dec 01 22:04:27 2005 +0100 @@ -225,18 +225,18 @@ val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] fun trans_tac _ = ArithData.gen_trans_tac iff_trans - val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac - val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys - val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@ - zadd_ac@zmult_ac@tc_rules@intifys + + val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac + val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys + val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys fun norm_tac ss = - ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3)) + ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps - add_0s @ bin_simps @ tc_rules @ intifys)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset))) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end; @@ -301,19 +301,19 @@ val left_distrib = left_zadd_zmult_distrib RS trans val prove_conv = prove_conv_nohyps "int_combine_numerals" fun trans_tac _ = ArithData.gen_trans_tac trans - val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac@intifys - val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys - val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@ - zadd_ac@zmult_ac@tc_rules@intifys + + val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys + val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys + val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys fun norm_tac ss = - ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3)) + ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps - add_0s @ bin_simps @ tc_rules @ intifys)) - val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s) + ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); @@ -340,16 +340,18 @@ val left_distrib = zmult_assoc RS sym RS trans val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" fun trans_tac _ = ArithData.gen_trans_tac trans - val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps - val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@ - bin_simps@zmult_ac@tc_rules@intifys + + val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps + val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @ + bin_simps @ zmult_ac @ tc_rules @ intifys fun norm_tac ss = - ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2)) + ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys fun numeral_simp_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps - bin_simps @ tc_rules @ intifys)) - val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s) + ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); end; diff -r 1ee4523c831f -r 841261f303a1 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Dec 01 22:03:06 2005 +0100 +++ b/src/ZF/arith_data.ML Thu Dec 01 22:04:27 2005 +0100 @@ -128,11 +128,12 @@ diff_natify1, diff_natify2]; (*Final simplification: cancel + and **) -fun simplify_meta_eq rules ss = - mk_meta_eq o - simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2] - delsimps iff_simps (*these could erase the whole rule!*) - addsimps rules); +fun simplify_meta_eq rules = + let val ss0 = + FOL_ss addeqcongs [eq_cong2, iff_cong2] + delsimps iff_simps (*these could erase the whole rule!*) + addsimps rules + in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end; val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right]; @@ -143,14 +144,15 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff val find_first_coeff = find_first_coeff [] - val norm_tac_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac - val norm_tac_ss2 = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys + + val norm_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac + val norm_ss2 = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys fun norm_tac ss = - ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1)) - THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2)) - val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys + ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) + val numeral_simp_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys fun numeral_simp_tac ss = - ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss)) + ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = simplify_meta_eq final_rules end;