simprocs: static evaluation of simpset;
authorwenzelm
Thu Dec 01 22:04:27 2005 +0100 (2005-12-01)
changeset 18328841261f303a1
parent 18327 1ee4523c831f
child 18329 221d47d17a81
simprocs: static evaluation of simpset;
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/arith_data.ML
src/ZF/Integ/int_arith.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Dec 01 22:03:06 2005 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 01 22:04:27 2005 +0100
     1.3 @@ -308,9 +308,9 @@
     1.4  fun trans_tac NONE      = all_tac
     1.5    | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
     1.6  
     1.7 -fun simplify_meta_eq rules ss =
     1.8 -    simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     1.9 -    o mk_meta_eq;
    1.10 +fun simplify_meta_eq rules =
    1.11 +  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    1.12 +  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
    1.13  
    1.14  structure CancelNumeralsCommon =
    1.15    struct
    1.16 @@ -320,15 +320,18 @@
    1.17    val dest_coeff        = dest_coeff 1
    1.18    val find_first_coeff  = find_first_coeff []
    1.19    val trans_tac         = fn _ => trans_tac
    1.20 +
    1.21 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.22 +    diff_simps @ minus_simps @ add_ac
    1.23 +  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
    1.24 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
    1.25    fun norm_tac ss =
    1.26 -    let val num_ss' = Simplifier.inherit_context ss num_ss in
    1.27 -      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    1.28 -                                         diff_simps @ minus_simps @ add_ac))
    1.29 -      THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    1.30 -      THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    1.31 -    end
    1.32 -  fun numeral_simp_tac ss =
    1.33 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    1.34 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.35 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.36 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    1.37 +
    1.38 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
    1.39 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    1.40    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    1.41    end;
    1.42  
    1.43 @@ -398,15 +401,18 @@
    1.44    val left_distrib      = combine_common_factor RS trans
    1.45    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    1.46    val trans_tac         = fn _ => trans_tac
    1.47 +
    1.48 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.49 +    diff_simps @ minus_simps @ add_ac
    1.50 +  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
    1.51 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
    1.52    fun norm_tac ss =
    1.53 -    let val num_ss' = Simplifier.inherit_context ss num_ss in
    1.54 -      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    1.55 -                                          diff_simps @ minus_simps @ add_ac))
    1.56 -      THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    1.57 -      THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    1.58 -    end
    1.59 -  fun numeral_simp_tac ss =
    1.60 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    1.61 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.62 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.63 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    1.64 +
    1.65 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
    1.66 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    1.67    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    1.68    end;
    1.69  
     2.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:03:06 2005 +0100
     2.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:04:27 2005 +0100
     2.3 @@ -43,14 +43,17 @@
     2.4    val mk_coeff          = mk_coeff
     2.5    val dest_coeff        = dest_coeff 1
     2.6    val trans_tac         = fn _ => trans_tac
     2.7 +
     2.8 +  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
     2.9 +  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
    2.10 +  val norm_ss3 = HOL_ss addsimps mult_ac
    2.11    fun norm_tac ss =
    2.12 -    let val HOL_ss' = Simplifier.inherit_context ss HOL_ss in
    2.13 -      ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
    2.14 -      THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
    2.15 -      THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
    2.16 -    end
    2.17 -  fun numeral_simp_tac ss =
    2.18 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps))
    2.19 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.20 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    2.21 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    2.22 +
    2.23 +  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
    2.24 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    2.25    val simplify_meta_eq = 
    2.26  	Int_Numeral_Simprocs.simplify_meta_eq
    2.27  	     [add_0, add_0_right,
    2.28 @@ -250,8 +253,8 @@
    2.29    val dest_coeff        = dest_coeff
    2.30    val find_first        = find_first []
    2.31    val trans_tac         = fn _ => trans_tac
    2.32 -  fun norm_tac ss =
    2.33 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
    2.34 +  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
    2.35 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    2.36    end;
    2.37  
    2.38  (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Dec 01 22:03:06 2005 +0100
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Dec 01 22:04:27 2005 +0100
     3.3 @@ -169,14 +169,16 @@
     3.4    val dest_coeff        = dest_coeff
     3.5    val find_first_coeff  = find_first_coeff []
     3.6    val trans_tac         = fn _ => trans_tac
     3.7 -  fun norm_tac ss =
     3.8 -    let val num_ss' = Simplifier.inherit_context ss num_ss in
     3.9 -      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    3.10 -                                [Suc_eq_add_numeral_1_left] @ add_ac))
    3.11 -      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    3.12 -    end
    3.13 -  fun numeral_simp_tac ss =
    3.14 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    3.15 +
    3.16 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    3.17 +    [Suc_eq_add_numeral_1_left] @ add_ac
    3.18 +  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    3.19 +  fun norm_tac ss = 
    3.20 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    3.21 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    3.22 +
    3.23 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
    3.24 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
    3.25    val simplify_meta_eq  = simplify_meta_eq
    3.26    end;
    3.27  
    3.28 @@ -254,14 +256,15 @@
    3.29    val left_distrib      = left_add_mult_distrib RS trans
    3.30    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    3.31    val trans_tac         = fn _ => trans_tac
    3.32 +
    3.33 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
    3.34 +  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    3.35    fun norm_tac ss =
    3.36 -    let val num_ss' = Simplifier.inherit_context ss num_ss in
    3.37 -      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    3.38 -                              [Suc_eq_add_numeral_1] @ add_ac))
    3.39 -      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    3.40 -    end
    3.41 -  fun numeral_simp_tac ss =
    3.42 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    3.43 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    3.44 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    3.45 +
    3.46 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
    3.47 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    3.48    val simplify_meta_eq  = simplify_meta_eq
    3.49    end;
    3.50  
    3.51 @@ -278,14 +281,16 @@
    3.52    val mk_coeff          = mk_coeff
    3.53    val dest_coeff        = dest_coeff
    3.54    val trans_tac         = fn _ => trans_tac
    3.55 +
    3.56 +  val norm_ss1 = num_ss addsimps
    3.57 +    numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac
    3.58 +  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
    3.59    fun norm_tac ss =
    3.60 -    let val num_ss' = Simplifier.inherit_context ss num_ss in
    3.61 -      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    3.62 -                                [Suc_eq_add_numeral_1_left] @ add_ac))
    3.63 -      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    3.64 -    end
    3.65 -  fun numeral_simp_tac ss =
    3.66 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps bin_simps))
    3.67 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    3.68 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    3.69 +
    3.70 +  val numeral_simp_ss = HOL_ss addsimps bin_simps
    3.71 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    3.72    val simplify_meta_eq  = simplify_meta_eq
    3.73    end
    3.74  
    3.75 @@ -371,8 +376,8 @@
    3.76    val dest_coeff        = dest_coeff
    3.77    val find_first        = find_first []
    3.78    val trans_tac         = fn _ => trans_tac
    3.79 -  fun norm_tac ss =
    3.80 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
    3.81 +  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
    3.82 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    3.83    end;
    3.84  
    3.85  structure EqCancelFactor = ExtractCommonTermFun
     4.1 --- a/src/HOL/Product_Type.thy	Thu Dec 01 22:03:06 2005 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Thu Dec 01 22:04:27 2005 +0100
     4.3 @@ -401,7 +401,7 @@
     4.4  ML_setup {*
     4.5  
     4.6  local
     4.7 -  val cond_split_eta = thm "cond_split_eta";
     4.8 +  val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
     4.9    fun  Pair_pat k 0 (Bound m) = (m = k)
    4.10    |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
    4.11                          m = k+i andalso Pair_pat k (i-1) t
    4.12 @@ -415,7 +415,7 @@
    4.13    |   split_pat tp i _ = NONE;
    4.14    fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
    4.15          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    4.16 -        (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
    4.17 +        (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
    4.18  
    4.19    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    4.20    |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
     5.1 --- a/src/HOL/Set.thy	Thu Dec 01 22:03:06 2005 +0100
     5.2 +++ b/src/HOL/Set.thy	Thu Dec 01 22:04:27 2005 +0100
     5.3 @@ -426,24 +426,17 @@
     5.4  
     5.5  ML_setup {*
     5.6    local
     5.7 -    val Ball_def = thm "Ball_def";
     5.8 -    val Bex_def = thm "Bex_def";
     5.9 -
    5.10 -    val simpset = Simplifier.clear_ss HOL_basic_ss;
    5.11 -    fun unfold_tac ss th =
    5.12 -      ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th]));
    5.13 -
    5.14 -    fun prove_bex_tac ss =
    5.15 -      unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
    5.16 +    val unfold_bex_tac = unfold_tac [thm "Bex_def"];
    5.17 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    5.18      val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    5.19  
    5.20 -    fun prove_ball_tac ss =
    5.21 -      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
    5.22 +    val unfold_ball_tac = unfold_tac [thm "Ball_def"];
    5.23 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    5.24      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    5.25    in
    5.26 -    val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    5.27 +    val defBEX_regroup = Simplifier.simproc (the_context ())
    5.28        "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    5.29 -    val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    5.30 +    val defBALL_regroup = Simplifier.simproc (the_context ())
    5.31        "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    5.32    end;
    5.33  
     6.1 --- a/src/HOL/arith_data.ML	Thu Dec 01 22:03:06 2005 +0100
     6.2 +++ b/src/HOL/arith_data.ML	Thu Dec 01 22:04:27 2005 +0100
     6.3 @@ -59,8 +59,9 @@
     6.4  
     6.5  (* rewriting *)
     6.6  
     6.7 -fun simp_all_tac rules ss =
     6.8 -  ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
     6.9 +fun simp_all_tac rules =
    6.10 +  let val ss0 = HOL_ss addsimps rules
    6.11 +  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    6.12  
    6.13  val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    6.14  val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    6.15 @@ -89,7 +90,9 @@
    6.16    val mk_sum = mk_norm_sum;
    6.17    val dest_sum = dest_sum;
    6.18    val prove_conv = prove_conv;
    6.19 -  fun norm_tac ss = simp_all_tac add_rules ss THEN simp_all_tac add_ac ss;
    6.20 +  val norm_tac1 = simp_all_tac add_rules;
    6.21 +  val norm_tac2 = simp_all_tac add_ac;
    6.22 +  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    6.23  end;
    6.24  
    6.25  fun gen_uncancel_tac rule ct =
     7.1 --- a/src/ZF/Integ/int_arith.ML	Thu Dec 01 22:03:06 2005 +0100
     7.2 +++ b/src/ZF/Integ/int_arith.ML	Thu Dec 01 22:04:27 2005 +0100
     7.3 @@ -225,18 +225,18 @@
     7.4    val dest_coeff        = dest_coeff 1
     7.5    val find_first_coeff  = find_first_coeff []
     7.6    fun trans_tac _       = ArithData.gen_trans_tac iff_trans
     7.7 -  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
     7.8 -                                    zminus_simps@zadd_ac
     7.9 -  val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
    7.10 -  val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
    7.11 -                                    zadd_ac@zmult_ac@tc_rules@intifys
    7.12 +
    7.13 +  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac
    7.14 +  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
    7.15 +  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
    7.16    fun norm_tac ss =
    7.17 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
    7.18 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
    7.19 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
    7.20 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
    7.21 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
    7.22 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
    7.23 +
    7.24 +  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
    7.25    fun numeral_simp_tac ss =
    7.26 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
    7.27 -      add_0s @ bin_simps @ tc_rules @ intifys))
    7.28 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    7.29      THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
    7.30    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
    7.31    end;
    7.32 @@ -301,19 +301,19 @@
    7.33    val left_distrib      = left_zadd_zmult_distrib RS trans
    7.34    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
    7.35    fun trans_tac _       = ArithData.gen_trans_tac trans
    7.36 -  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
    7.37 -                                    zminus_simps@zadd_ac@intifys
    7.38 -  val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
    7.39 -  val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
    7.40 -                                    zadd_ac@zmult_ac@tc_rules@intifys
    7.41 +
    7.42 +  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys
    7.43 +  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
    7.44 +  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
    7.45    fun norm_tac ss =
    7.46 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
    7.47 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
    7.48 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
    7.49 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
    7.50 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
    7.51 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
    7.52 +
    7.53 +  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
    7.54    fun numeral_simp_tac ss =
    7.55 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
    7.56 -      add_0s @ bin_simps @ tc_rules @ intifys))
    7.57 -  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
    7.58 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    7.59 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
    7.60    end;
    7.61  
    7.62  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
    7.63 @@ -340,16 +340,18 @@
    7.64    val left_distrib      = zmult_assoc RS sym RS trans
    7.65    val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
    7.66    fun trans_tac _       = ArithData.gen_trans_tac trans
    7.67 -  val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
    7.68 -  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
    7.69 -                                    bin_simps@zmult_ac@tc_rules@intifys
    7.70 +
    7.71 +  val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
    7.72 +  val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
    7.73 +    bin_simps @ zmult_ac @ tc_rules @ intifys
    7.74    fun norm_tac ss =
    7.75 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
    7.76 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
    7.77 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
    7.78 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
    7.79 +
    7.80 +  val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
    7.81    fun numeral_simp_tac ss =
    7.82 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
    7.83 -      bin_simps @ tc_rules @ intifys))
    7.84 -  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
    7.85 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    7.86 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
    7.87    end;
    7.88  
    7.89  
     8.1 --- a/src/ZF/arith_data.ML	Thu Dec 01 22:03:06 2005 +0100
     8.2 +++ b/src/ZF/arith_data.ML	Thu Dec 01 22:04:27 2005 +0100
     8.3 @@ -128,11 +128,12 @@
     8.4                 diff_natify1, diff_natify2];
     8.5  
     8.6  (*Final simplification: cancel + and **)
     8.7 -fun simplify_meta_eq rules ss =
     8.8 -    mk_meta_eq o
     8.9 -    simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
    8.10 -                     delsimps iff_simps (*these could erase the whole rule!*)
    8.11 -                     addsimps rules);
    8.12 +fun simplify_meta_eq rules =
    8.13 +  let val ss0 =
    8.14 +    FOL_ss addeqcongs [eq_cong2, iff_cong2]
    8.15 +      delsimps iff_simps (*these could erase the whole rule!*)
    8.16 +      addsimps rules
    8.17 +  in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end;
    8.18  
    8.19  val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
    8.20  
    8.21 @@ -143,14 +144,15 @@
    8.22    val mk_coeff          = mk_coeff
    8.23    val dest_coeff        = dest_coeff
    8.24    val find_first_coeff  = find_first_coeff []
    8.25 -  val norm_tac_ss1      = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
    8.26 -  val norm_tac_ss2      = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
    8.27 +
    8.28 +  val norm_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
    8.29 +  val norm_ss2 = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
    8.30    fun norm_tac ss =
    8.31 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
    8.32 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
    8.33 -  val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
    8.34 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
    8.35 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
    8.36 +  val numeral_simp_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
    8.37    fun numeral_simp_tac ss =
    8.38 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss))
    8.39 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    8.40    val simplify_meta_eq  = simplify_meta_eq final_rules
    8.41    end;
    8.42