simplify theorem references
authorhuffman
Mon Mar 30 12:07:59 2009 -0700 (2009-03-30)
changeset 30802f9e9e800d27e
parent 30796 126701134811
child 30803 d9f4e7a59392
child 30807 a167ed35ec0d
simplify theorem references
src/HOL/Int.thy
src/HOL/Tools/int_arith.ML
     1.1 --- a/src/HOL/Int.thy	Mon Mar 30 10:47:41 2009 -0700
     1.2 +++ b/src/HOL/Int.thy	Mon Mar 30 12:07:59 2009 -0700
     1.3 @@ -1525,6 +1525,17 @@
     1.4  lemmas zle_int = of_nat_le_iff [where 'a=int]
     1.5  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
     1.6  
     1.7 +subsection {* Setting up simplification procedures *}
     1.8 +
     1.9 +lemmas int_arith_rules =
    1.10 +  neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
    1.11 +  minus_zero diff_minus left_minus right_minus
    1.12 +  mult_zero_left mult_zero_right mult_Bit1 mult_1_right
    1.13 +  mult_minus_left mult_minus_right
    1.14 +  minus_add_distrib minus_minus mult_assoc
    1.15 +  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.16 +  of_int_0 of_int_1 of_int_add of_int_mult
    1.17 +
    1.18  use "Tools/int_arith.ML"
    1.19  declaration {* K Int_Arith.setup *}
    1.20  
     2.1 --- a/src/HOL/Tools/int_arith.ML	Mon Mar 30 10:47:41 2009 -0700
     2.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Mar 30 12:07:59 2009 -0700
     2.3 @@ -26,9 +26,6 @@
     2.4  val reorient_simproc = 
     2.5    Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
     2.6  
     2.7 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
     2.8 -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
     2.9 -
    2.10  
    2.11  (** Utilities **)
    2.12  
    2.13 @@ -176,10 +173,12 @@
    2.14  
    2.15  val num_ss = HOL_ss settermless numtermless;
    2.16  
    2.17 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
    2.18 +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    2.19  
    2.20  (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    2.21 -val add_0s =  thms "add_0s";
    2.22 -val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
    2.23 +val add_0s =  @{thms add_0s};
    2.24 +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
    2.25  
    2.26  (*Simplify inverse Numeral1, a/Numeral1*)
    2.27  val inverse_1s = [@{thm inverse_numeral_1}];
    2.28 @@ -208,16 +207,21 @@
    2.29  
    2.30  (*push the unary minus down: - x * y = x * - y *)
    2.31  val minus_mult_eq_1_to_2 =
    2.32 -    [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
    2.33 +    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
    2.34  
    2.35  (*to extract again any uncancelled minuses*)
    2.36  val minus_from_mult_simps =
    2.37 -    [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
    2.38 +    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
    2.39  
    2.40  (*combine unary minus with numeric literals, however nested within a product*)
    2.41  val mult_minus_simps =
    2.42      [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
    2.43  
    2.44 +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    2.45 +  diff_simps @ minus_simps @ @{thms add_ac}
    2.46 +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    2.47 +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    2.48 +
    2.49  structure CancelNumeralsCommon =
    2.50    struct
    2.51    val mk_sum            = mk_sum
    2.52 @@ -227,10 +231,6 @@
    2.53    val find_first_coeff  = find_first_coeff []
    2.54    val trans_tac         = K Arith_Data.trans_tac
    2.55  
    2.56 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    2.57 -    diff_simps @ minus_simps @ @{thms add_ac}
    2.58 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    2.59 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    2.60    fun norm_tac ss =
    2.61      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.62      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    2.63 @@ -310,10 +310,6 @@
    2.64    val prove_conv        = Arith_Data.prove_conv_nohyps
    2.65    val trans_tac         = K Arith_Data.trans_tac
    2.66  
    2.67 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    2.68 -    diff_simps @ minus_simps @ @{thms add_ac}
    2.69 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    2.70 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    2.71    fun norm_tac ss =
    2.72      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.73      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    2.74 @@ -340,12 +336,9 @@
    2.75    val prove_conv        = Arith_Data.prove_conv_nohyps
    2.76    val trans_tac         = K Arith_Data.trans_tac
    2.77  
    2.78 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    2.79 -    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
    2.80 -  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    2.81 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    2.82 +  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
    2.83    fun norm_tac ss =
    2.84 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.85 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
    2.86      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    2.87      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    2.88  
    2.89 @@ -516,14 +509,7 @@
    2.90  
    2.91  val add_rules =
    2.92      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
    2.93 -    [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
    2.94 -     @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
    2.95 -     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
    2.96 -     @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
    2.97 -     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
    2.98 -     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
    2.99 -     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   2.100 -     @{thm of_int_mult}]
   2.101 +    @{thms int_arith_rules}
   2.102  
   2.103  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   2.104