src/HOL/Tools/int_arith.ML
changeset 30802 f9e9e800d27e
parent 30732 afca5be252d6
child 31024 0fdf666e08bf
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon Mar 30 10:47:41 2009 -0700
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Mar 30 12:07:59 2009 -0700
     1.3 @@ -26,9 +26,6 @@
     1.4  val reorient_simproc = 
     1.5    Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
     1.6  
     1.7 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
     1.8 -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
     1.9 -
    1.10  
    1.11  (** Utilities **)
    1.12  
    1.13 @@ -176,10 +173,12 @@
    1.14  
    1.15  val num_ss = HOL_ss settermless numtermless;
    1.16  
    1.17 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
    1.18 +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    1.19  
    1.20  (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    1.21 -val add_0s =  thms "add_0s";
    1.22 -val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
    1.23 +val add_0s =  @{thms add_0s};
    1.24 +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
    1.25  
    1.26  (*Simplify inverse Numeral1, a/Numeral1*)
    1.27  val inverse_1s = [@{thm inverse_numeral_1}];
    1.28 @@ -208,16 +207,21 @@
    1.29  
    1.30  (*push the unary minus down: - x * y = x * - y *)
    1.31  val minus_mult_eq_1_to_2 =
    1.32 -    [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
    1.33 +    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
    1.34  
    1.35  (*to extract again any uncancelled minuses*)
    1.36  val minus_from_mult_simps =
    1.37 -    [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
    1.38 +    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
    1.39  
    1.40  (*combine unary minus with numeric literals, however nested within a product*)
    1.41  val mult_minus_simps =
    1.42      [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
    1.43  
    1.44 +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.45 +  diff_simps @ minus_simps @ @{thms add_ac}
    1.46 +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.47 +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.48 +
    1.49  structure CancelNumeralsCommon =
    1.50    struct
    1.51    val mk_sum            = mk_sum
    1.52 @@ -227,10 +231,6 @@
    1.53    val find_first_coeff  = find_first_coeff []
    1.54    val trans_tac         = K Arith_Data.trans_tac
    1.55  
    1.56 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.57 -    diff_simps @ minus_simps @ @{thms add_ac}
    1.58 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.59 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.60    fun norm_tac ss =
    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 @@ -310,10 +310,6 @@
    1.64    val prove_conv        = Arith_Data.prove_conv_nohyps
    1.65    val trans_tac         = K Arith_Data.trans_tac
    1.66  
    1.67 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.68 -    diff_simps @ minus_simps @ @{thms add_ac}
    1.69 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.70 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.71    fun norm_tac ss =
    1.72      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.73      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.74 @@ -340,12 +336,9 @@
    1.75    val prove_conv        = Arith_Data.prove_conv_nohyps
    1.76    val trans_tac         = K Arith_Data.trans_tac
    1.77  
    1.78 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.79 -    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
    1.80 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.81 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.82 +  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
    1.83    fun norm_tac ss =
    1.84 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.85 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
    1.86      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.87      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    1.88  
    1.89 @@ -516,14 +509,7 @@
    1.90  
    1.91  val add_rules =
    1.92      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
    1.93 -    [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
    1.94 -     @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
    1.95 -     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
    1.96 -     @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
    1.97 -     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
    1.98 -     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
    1.99 -     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   1.100 -     @{thm of_int_mult}]
   1.101 +    @{thms int_arith_rules}
   1.102  
   1.103  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   1.104