src/HOL/Integ/int_factor_simprocs.ML

--- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Aug 06 11:22:05 2002 +0200
@@ -12,26 +12,26 @@
 
 Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
 by (stac zmult_zle_cancel1 1);
-by Auto_tac;  
+by Auto_tac;
 qed "int_mult_le_cancel1";
 
 Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
 by (stac zmult_zless_cancel1 1);
-by Auto_tac;  
+by Auto_tac;
 qed "int_mult_less_cancel1";
 
 Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
-by Auto_tac;  
+by Auto_tac;
 qed "int_mult_eq_cancel1";
 
 Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
-by (stac zdiv_zmult_zmult1 1); 
-by Auto_tac;  
+by (stac zdiv_zmult_zmult1 1);
+by Auto_tac;
 qed "int_mult_div_cancel1";
 
 (*For ExtractCommonTermFun, cancelling common factors*)
 Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
-by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); 
+by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
 qed "int_mult_div_cancel_disj";
 
 local
@@ -40,15 +40,15 @@
 
 structure CancelNumeralFactorCommon =
   struct
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff 1
+  val mk_coeff          = mk_coeff
+  val dest_coeff        = dest_coeff 1
   val trans_tac         = trans_tac
-  val norm_tac = 
+  val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
      THEN ALLGOALS
             (simp_tac (HOL_ss addsimps zmult_ac))
-  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq mult_1s
   end
 
@@ -88,19 +88,15 @@
   val neg_exchanges = true
 )
 
-val int_cancel_numeral_factors = 
+val int_cancel_numeral_factors =
   map Bin_Simprocs.prep_simproc
-   [("inteq_cancel_numeral_factors",
-     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
+   [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
      EqCancelNumeralFactor.proc),
-    ("intless_cancel_numeral_factors", 
-     Bin_Simprocs.prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
+    ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
      LessCancelNumeralFactor.proc),
-    ("intle_cancel_numeral_factors", 
-     Bin_Simprocs.prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
+    ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
      LeCancelNumeralFactor.proc),
-    ("intdiv_cancel_numeral_factors", 
-     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
+    ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
      DivCancelNumeralFactor.proc)];
 
 end;
@@ -112,7 +108,7 @@
 print_depth 22;
 set timing;
 set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1)); 
+fun test s = (Goal s; by (Simp_tac 1));
 
 test "9*x = 12 * (y::int)";
 test "(9*x) div (12 * (y::int)) = z";
@@ -156,25 +152,25 @@
   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
 
 (*Find first term that matches u*)
-fun find_first past u []         = raise TERM("find_first", []) 
+fun find_first past u []         = raise TERM("find_first", [])
   | find_first past u (t::terms) =
-	if u aconv t then (rev past @ terms)
+        if u aconv t then (rev past @ terms)
         else find_first (t::past) u terms
-	handle TERM _ => find_first (t::past) u terms;
+        handle TERM _ => find_first (t::past) u terms;
 
 (*Final simplification: cancel + and *  *)
-fun cancel_simplify_meta_eq cancel_th th = 
-    Int_Numeral_Simprocs.simplify_meta_eq 
-        [zmult_1, zmult_1_right] 
+fun cancel_simplify_meta_eq cancel_th th =
+    Int_Numeral_Simprocs.simplify_meta_eq
+        [zmult_1, zmult_1_right]
         (([th, cancel_th]) MRS trans);
 
 structure CancelFactorCommon =
   struct
-  val mk_sum    	= long_mk_prod
-  val dest_sum		= dest_prod
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff
-  val find_first	= find_first []
+  val mk_sum            = long_mk_prod
+  val dest_sum          = dest_prod
+  val mk_coeff          = mk_coeff
+  val dest_coeff        = dest_coeff
+  val find_first        = find_first []
   val trans_tac         = trans_tac
   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
   end;
@@ -195,13 +191,10 @@
   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
 );
 
-val int_cancel_factor = 
+val int_cancel_factor =
   map Bin_Simprocs.prep_simproc
-   [("int_eq_cancel_factor",
-     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
-     EqCancelFactor.proc),
-    ("int_divide_cancel_factor", 
-     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
+   [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
+    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
      DivideCancelFactor.proc)];
 
 end;
@@ -213,15 +206,15 @@
 print_depth 22;
 set timing;
 set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1)); 
+fun test s = (Goal s; by (Asm_simp_tac 1));
 
 test "x*k = k*(y::int)";
-test "k = k*(y::int)"; 
+test "k = k*(y::int)";
 test "a*(b*c) = (b::int)";
 test "a*(b*c) = d*(b::int)*(x*a)";
 
 test "(x*k) div (k*(y::int)) = (uu::int)";
-test "(k) div (k*(y::int)) = (uu::int)"; 
+test "(k) div (k*(y::int)) = (uu::int)";
 test "(a*(b*c)) div ((b::int)) = (uu::int)";
 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
 *)