The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
authornipkow
Sat Jun 16 15:01:54 2007 +0200 (2007-06-16)
changeset 23400a64b39e5809b
parent 23399 1766da98eaa9
child 23401 8c5532263ba9
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.
src/HOL/Ring_and_Field.thy
src/HOL/int_arith1.ML
src/HOL/int_factor_simprocs.ML
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jun 15 19:19:23 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jun 16 15:01:54 2007 +0200
     1.3 @@ -1042,13 +1042,14 @@
     1.4  
     1.5  subsubsection{*Special Cancellation Simprules for Division*}
     1.6  
     1.7 -lemma mult_divide_cancel_left_if [simp]:
     1.8 +(* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
     1.9 +lemma mult_divide_cancel_left_if[simp]:
    1.10    fixes c :: "'a :: {field,division_by_zero}"
    1.11    shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
    1.12  by (simp add: mult_divide_cancel_left)
    1.13 -(* also used at ML level *)
    1.14  
    1.15 -lemma mult_divide_cancel_right_if [simp]:
    1.16 +(* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
    1.17 +lemma mult_divide_cancel_right_if:
    1.18    fixes c :: "'a :: {field,division_by_zero}"
    1.19    shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
    1.20  by (simp add: mult_divide_cancel_right)
    1.21 @@ -1092,7 +1093,7 @@
    1.22    fixes a :: "'a :: {field,division_by_zero}"
    1.23    shows "(b/a) * a = (if a=0 then 0 else b)"
    1.24  by (simp add: times_divide_eq_left)
    1.25 -
    1.26 +*)
    1.27  
    1.28  subsection {* Division and Unary Minus *}
    1.29  
     2.1 --- a/src/HOL/int_arith1.ML	Fri Jun 15 19:19:23 2007 +0200
     2.2 +++ b/src/HOL/int_arith1.ML	Sat Jun 16 15:01:54 2007 +0200
     2.3 @@ -191,8 +191,7 @@
     2.4  
     2.5  fun mk_minus t = 
     2.6    let val T = Term.fastype_of t
     2.7 -  in Const (@{const_name HOL.uminus}, T --> T) $ t
     2.8 -  end;
     2.9 +  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
    2.10  
    2.11  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    2.12  fun mk_sum T []        = mk_number T 0
    2.13 @@ -220,22 +219,28 @@
    2.14  
    2.15  val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    2.16  
    2.17 +fun one_of T = Const(@{const_name HOL.one},T);
    2.18 +
    2.19 +(* build product with trailing 1 rather than Numeral 1 in order to avoid the
    2.20 +   unnecessary restriction to type class number_ring
    2.21 +   which is not required for cancellation of common factors in divisions.
    2.22 +*)
    2.23  fun mk_prod T = 
    2.24 -  let val one = mk_number T 1
    2.25 +  let val one = one_of T
    2.26    fun mk [] = one
    2.27      | mk [t] = t
    2.28      | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
    2.29    in mk end;
    2.30  
    2.31  (*This version ALWAYS includes a trailing one*)
    2.32 -fun long_mk_prod T []        = mk_number T 1
    2.33 +fun long_mk_prod T []        = one_of T
    2.34    | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
    2.35  
    2.36  val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
    2.37  
    2.38  fun dest_prod t =
    2.39        let val (t,u) = dest_times t
    2.40 -      in  dest_prod t @ dest_prod u  end
    2.41 +      in dest_prod t @ dest_prod u end
    2.42        handle TERM _ => [t];
    2.43  
    2.44  (*DON'T do the obvious simplifications; that would create special cases*)
    2.45 @@ -253,8 +258,8 @@
    2.46  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    2.47    | find_first_coeff past u (t::terms) =
    2.48          let val (n,u') = dest_coeff 1 t
    2.49 -        in  if u aconv u' then (n, rev past @ terms)
    2.50 -                          else find_first_coeff (t::past) u terms
    2.51 +        in if u aconv u' then (n, rev past @ terms)
    2.52 +                         else find_first_coeff (t::past) u terms
    2.53          end
    2.54          handle TERM _ => find_first_coeff (t::past) u terms;
    2.55  
    2.56 @@ -271,23 +276,23 @@
    2.57  (*Build term (p / q) * t*)
    2.58  fun mk_fcoeff ((p, q), t) =
    2.59    let val T = Term.fastype_of t
    2.60 -  in  mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
    2.61 +  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
    2.62  
    2.63  (*Express t as a product of a fraction with other sorted terms*)
    2.64  fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
    2.65    | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
    2.66      let val (p, t') = dest_coeff sign t
    2.67          val (q, u') = dest_coeff 1 u
    2.68 -    in  (mk_frac (p, q), mk_divide (t', u')) end
    2.69 +    in (mk_frac (p, q), mk_divide (t', u')) end
    2.70    | dest_fcoeff sign t =
    2.71      let val (p, t') = dest_coeff sign t
    2.72          val T = Term.fastype_of t
    2.73 -    in  (mk_frac (p, 1), mk_divide (t', mk_number T 1)) end;
    2.74 +    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
    2.75  
    2.76  
    2.77 -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
    2.78 +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    2.79  val add_0s =  thms "add_0s";
    2.80 -val mult_1s = thms "mult_1s";
    2.81 +val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
    2.82  
    2.83  (*Simplify inverse Numeral1, a/Numeral1*)
    2.84  val inverse_1s = [@{thm inverse_numeral_1}];
     3.1 --- a/src/HOL/int_factor_simprocs.ML	Fri Jun 15 19:19:23 2007 +0200
     3.2 +++ b/src/HOL/int_factor_simprocs.ML	Sat Jun 16 15:01:54 2007 +0200
     3.3 @@ -280,15 +280,15 @@
     3.4  val cancel_factors =
     3.5    map Int_Numeral_Base_Simprocs.prep_simproc
     3.6     [("ring_eq_cancel_factor",
     3.7 -     ["(l::'a::{idom,number_ring}) * m = n",
     3.8 -      "(l::'a::{idom,number_ring}) = m * n"],
     3.9 +     ["(l::'a::{idom}) * m = n",
    3.10 +      "(l::'a::{idom}) = m * n"],
    3.11      K EqCancelFactor.proc),
    3.12      ("int_div_cancel_factor",
    3.13       ["((l::int) * m) div n", "(l::int) div (m * n)"],
    3.14       K IntDivCancelFactor.proc),
    3.15      ("divide_cancel_factor",
    3.16 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
    3.17 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
    3.18 +     ["((l::'a::{division_by_zero,field}) * m) / n",
    3.19 +      "(l::'a::{division_by_zero,field}) / (m * n)"],
    3.20       K DivideCancelFactor.proc)];
    3.21  
    3.22  end;