# HG changeset patch
# User haftmann
# Date 1236968277 -3600
# Node ID 07b45c1aa78882d538fa916af88eb1297e4fe2d8
# Parent  51a39ed24c0fc887453d19a41577ecbf4a6c32b4
moved some generic nonsense to arith_data.ML

diff -r 51a39ed24c0f -r 07b45c1aa788 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Fri Mar 13 19:17:57 2009 +0100
@@ -10,6 +10,8 @@
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   val simp_all_tac: thm list -> simpset -> tactic
+  val simplify_meta_eq: thm list -> simpset -> thm -> thm
+  val trans_tac: thm option -> tactic
   val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
 end;
@@ -33,6 +35,13 @@
   let val ss0 = HOL_ss addsimps rules
   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
 
+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
+
+fun trans_tac NONE  = all_tac
+  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+
 fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
   Simplifier.simproc (the_context ()) name pats proc;
 
diff -r 51a39ed24c0f -r 07b45c1aa788 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
@@ -29,41 +29,6 @@
 (*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];
 
-(** New term ordering so that AC-rewriting brings numerals to the front **)
-
-(*Order integers by absolute value and then by sign. The standard integer
-  ordering is not well-founded.*)
-fun num_ord (i,j) =
-  (case int_ord (abs i, abs j) of
-    EQUAL => int_ord (Int.sign i, Int.sign j) 
-  | ord => ord);
-
-(*This resembles TermOrd.term_ord, but it puts binary numerals before other
-  non-atomic terms.*)
-local open Term 
-in 
-fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
-      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
-  | numterm_ord
-     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
-     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
-  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
-  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
-  | numterm_ord (t, u) =
-      (case int_ord (size_of_term t, size_of_term u) of
-        EQUAL =>
-          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
-            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
-          end
-      | ord => ord)
-and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
-end;
-
-fun numtermless tu = (numterm_ord tu = LESS);
-
-(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
-val num_ss = HOL_ss settermless numtermless;
-
 
 (** Utilities **)
 
@@ -177,6 +142,41 @@
     in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
 
 
+(** New term ordering so that AC-rewriting brings numerals to the front **)
+
+(*Order integers by absolute value and then by sign. The standard integer
+  ordering is not well-founded.*)
+fun num_ord (i,j) =
+  (case int_ord (abs i, abs j) of
+    EQUAL => int_ord (Int.sign i, Int.sign j) 
+  | ord => ord);
+
+(*This resembles TermOrd.term_ord, but it puts binary numerals before other
+  non-atomic terms.*)
+local open Term 
+in 
+fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
+      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
+  | numterm_ord
+     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
+     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
+  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
+  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
+  | numterm_ord (t, u) =
+      (case int_ord (size_of_term t, size_of_term u) of
+        EQUAL =>
+          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
+            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
+          end
+      | ord => ord)
+and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
+end;
+
+fun numtermless tu = (numterm_ord tu = LESS);
+
+val num_ss = HOL_ss settermless numtermless;
+
+
 (*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"];
@@ -218,14 +218,6 @@
 val mult_minus_simps =
     [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
 
-(*Apply the given rewrite (if present) just once*)
-fun trans_tac NONE      = all_tac
-  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
-
-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
   val mk_sum            = mk_sum
@@ -233,7 +225,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = fn _ => trans_tac
+  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}
@@ -246,7 +238,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ 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)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 
@@ -316,7 +308,7 @@
   val dest_coeff        = dest_coeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  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}
@@ -329,7 +321,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ 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)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
@@ -346,7 +338,7 @@
   val dest_coeff        = dest_fcoeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  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}
@@ -359,7 +351,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   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 @ divide_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   end;
 
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
diff -r 51a39ed24c0f -r 07b45c1aa788 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
@@ -29,7 +29,7 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
 
   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -41,7 +41,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps rel_number_of @ 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
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq
     [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
       @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
   end
@@ -215,7 +215,7 @@
         handle TERM _ => find_first_t (t::past) u terms;
 
 (** Final simplification for the CancelFactor simprocs **)
-val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
+val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
 
 fun cancel_simplify_meta_eq cancel_th ss th =
@@ -228,7 +228,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;
diff -r 51a39ed24c0f -r 07b45c1aa788 src/HOL/Tools/nat_simprocs.ML
--- a/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
@@ -41,8 +41,6 @@
 
 (** Other simproc items **)
 
-val trans_tac = Int_Numeral_Simprocs.trans_tac;
-
 val bin_simps =
      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
@@ -130,15 +128,11 @@
   @{thm Suc_not_Zero}, @{thm le_0_eq}];
 
 val simplify_meta_eq =
-    Int_Numeral_Simprocs.simplify_meta_eq
+    Arith_Data.simplify_meta_eq
         ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
           @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
 
 
-(*Like HOL_ss but with an ordering that brings numerals to the front
-  under AC-rewriting.*)
-val num_ss = Int_Numeral_Simprocs.num_ss;
-
 (*** Applying CancelNumeralsFun ***)
 
 structure CancelNumeralsCommon =
@@ -148,11 +142,11 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_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))
@@ -237,10 +231,10 @@
   val dest_coeff        = dest_coeff
   val left_distrib      = @{thm left_add_mult_distrib} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_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))
@@ -262,11 +256,11 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
 
-  val norm_ss1 = num_ss addsimps
+  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps
     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_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))
@@ -355,7 +349,7 @@
         handle TERM _ => find_first_t (t::past) u terms;
 
 (** Final simplification for the CancelFactor simprocs **)
-val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
+val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
 
 fun cancel_simplify_meta_eq cancel_th ss th =
@@ -368,7 +362,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;