simplify theorem references

--- a/src/HOL/Int.thy	Mon Mar 30 10:47:41 2009 -0700
+++ b/src/HOL/Int.thy	Mon Mar 30 12:07:59 2009 -0700
@@ -1525,6 +1525,17 @@
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
 
+subsection {* Setting up simplification procedures *}
+
+lemmas int_arith_rules =
+  neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
+  minus_zero diff_minus left_minus right_minus
+  mult_zero_left mult_zero_right mult_Bit1 mult_1_right
+  mult_minus_left mult_minus_right
+  minus_add_distrib minus_minus mult_assoc
+  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
+  of_int_0 of_int_1 of_int_add of_int_mult
+
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 

--- a/src/HOL/Tools/int_arith.ML	Mon Mar 30 10:47:41 2009 -0700
+++ b/src/HOL/Tools/int_arith.ML	Mon Mar 30 12:07:59 2009 -0700
@@ -26,9 +26,6 @@
 val reorient_simproc = 
   Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
 
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
-val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
-
 
 (** Utilities **)
 
@@ -176,10 +173,12 @@
 
 val num_ss = HOL_ss settermless numtermless;
 
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
+val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
 
 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
-val add_0s =  thms "add_0s";
-val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
+val add_0s =  @{thms add_0s};
+val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
 
 (*Simplify inverse Numeral1, a/Numeral1*)
 val inverse_1s = [@{thm inverse_numeral_1}];
@@ -208,16 +207,21 @@
 
 (*push the unary minus down: - x * y = x * - y *)
 val minus_mult_eq_1_to_2 =
-    [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
+    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
 
 (*to extract again any uncancelled minuses*)
 val minus_from_mult_simps =
-    [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
+    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val mult_minus_simps =
     [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
 
+val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+  diff_simps @ minus_simps @ @{thms add_ac}
+val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
+val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
+
 structure CancelNumeralsCommon =
   struct
   val mk_sum            = mk_sum
@@ -227,10 +231,6 @@
   val find_first_coeff  = find_first_coeff []
   val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms 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))
@@ -310,10 +310,6 @@
   val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms 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))
@@ -340,12 +336,9 @@
   val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   fun norm_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
@@ -516,14 +509,7 @@
 
 val add_rules =
     simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
-    [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
-     @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
-     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
-     @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
-     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
-     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
-     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
-     @{thm of_int_mult}]
+    @{thms int_arith_rules}
 
 val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]