# HG changeset patch
# User nipkow
# Date 1181998914 -7200
# Node ID a64b39e5809bbcab48d7f8630f9cdb6587351c90
# Parent  1766da98eaa9a7f0b89d84e31917bd09510e06c0
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
longer need class numeral_ring. This made a number of special
simp-thms redundant.

diff -r 1766da98eaa9 -r a64b39e5809b src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Jun 15 19:19:23 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sat Jun 16 15:01:54 2007 +0200
@@ -1042,13 +1042,14 @@
 
 subsubsection{*Special Cancellation Simprules for Division*}
 
-lemma mult_divide_cancel_left_if [simp]:
+(* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
+lemma mult_divide_cancel_left_if[simp]:
   fixes c :: "'a :: {field,division_by_zero}"
   shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
 by (simp add: mult_divide_cancel_left)
-(* also used at ML level *)
 
-lemma mult_divide_cancel_right_if [simp]:
+(* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
+lemma mult_divide_cancel_right_if:
   fixes c :: "'a :: {field,division_by_zero}"
   shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
 by (simp add: mult_divide_cancel_right)
@@ -1092,7 +1093,7 @@
   fixes a :: "'a :: {field,division_by_zero}"
   shows "(b/a) * a = (if a=0 then 0 else b)"
 by (simp add: times_divide_eq_left)
-
+*)
 
 subsection {* Division and Unary Minus *}
 
diff -r 1766da98eaa9 -r a64b39e5809b src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Fri Jun 15 19:19:23 2007 +0200
+++ b/src/HOL/int_arith1.ML	Sat Jun 16 15:01:54 2007 +0200
@@ -191,8 +191,7 @@
 
 fun mk_minus t = 
   let val T = Term.fastype_of t
-  in Const (@{const_name HOL.uminus}, T --> T) $ t
-  end;
+  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
 fun mk_sum T []        = mk_number T 0
@@ -220,22 +219,28 @@
 
 val mk_times = HOLogic.mk_binop @{const_name HOL.times};
 
+fun one_of T = Const(@{const_name HOL.one},T);
+
+(* build product with trailing 1 rather than Numeral 1 in order to avoid the
+   unnecessary restriction to type class number_ring
+   which is not required for cancellation of common factors in divisions.
+*)
 fun mk_prod T = 
-  let val one = mk_number T 1
+  let val one = one_of T
   fun mk [] = one
     | mk [t] = t
     | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
   in mk end;
 
 (*This version ALWAYS includes a trailing one*)
-fun long_mk_prod T []        = mk_number T 1
+fun long_mk_prod T []        = one_of T
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
 val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
-      in  dest_prod t @ dest_prod u  end
+      in dest_prod t @ dest_prod u end
       handle TERM _ => [t];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
@@ -253,8 +258,8 @@
 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   | find_first_coeff past u (t::terms) =
         let val (n,u') = dest_coeff 1 t
-        in  if u aconv u' then (n, rev past @ terms)
-                          else find_first_coeff (t::past) u terms
+        in if u aconv u' then (n, rev past @ terms)
+                         else find_first_coeff (t::past) u terms
         end
         handle TERM _ => find_first_coeff (t::past) u terms;
 
@@ -271,23 +276,23 @@
 (*Build term (p / q) * t*)
 fun mk_fcoeff ((p, q), t) =
   let val T = Term.fastype_of t
-  in  mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
+  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
 
 (*Express t as a product of a fraction with other sorted terms*)
 fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
   | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
     let val (p, t') = dest_coeff sign t
         val (q, u') = dest_coeff 1 u
-    in  (mk_frac (p, q), mk_divide (t', u')) end
+    in (mk_frac (p, q), mk_divide (t', u')) end
   | dest_fcoeff sign t =
     let val (p, t') = dest_coeff sign t
         val T = Term.fastype_of t
-    in  (mk_frac (p, 1), mk_divide (t', mk_number T 1)) end;
+    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
 
 
-(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
+(*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";
+val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
 
 (*Simplify inverse Numeral1, a/Numeral1*)
 val inverse_1s = [@{thm inverse_numeral_1}];
diff -r 1766da98eaa9 -r a64b39e5809b src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Fri Jun 15 19:19:23 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML	Sat Jun 16 15:01:54 2007 +0200
@@ -280,15 +280,15 @@
 val cancel_factors =
   map Int_Numeral_Base_Simprocs.prep_simproc
    [("ring_eq_cancel_factor",
-     ["(l::'a::{idom,number_ring}) * m = n",
-      "(l::'a::{idom,number_ring}) = m * n"],
+     ["(l::'a::{idom}) * m = n",
+      "(l::'a::{idom}) = m * n"],
     K EqCancelFactor.proc),
     ("int_div_cancel_factor",
      ["((l::int) * m) div n", "(l::int) div (m * n)"],
      K IntDivCancelFactor.proc),
     ("divide_cancel_factor",
-     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
-      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
+     ["((l::'a::{division_by_zero,field}) * m) / n",
+      "(l::'a::{division_by_zero,field}) / (m * n)"],
      K DivideCancelFactor.proc)];
 
 end;