further tweaks to the numeric theories
authorpaulson
Tue Feb 17 10:41:59 2004 +0100 (2004-02-17)
changeset 1439055fe71faadda
parent 14389 57c2d90936ba
child 14391 bb726050650d
further tweaks to the numeric theories
src/HOL/Hyperreal/IntFloor.ML
src/HOL/Integ/IntArith.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Real/rat_arith.ML
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Hyperreal/IntFloor.ML	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/IntFloor.ML	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -4,8 +4,6 @@
     1.4      Description: Floor and ceiling operations over reals
     1.5  *)
     1.6  
     1.7 -val real_number_of = thm"real_number_of";
     1.8 -
     1.9  Goal "((number_of n) < real (m::int)) = (number_of n < m)";
    1.10  by Auto_tac;
    1.11  by (rtac (real_of_int_less_iff RS iffD1) 1);
     2.1 --- a/src/HOL/Integ/IntArith.thy	Mon Feb 16 15:24:03 2004 +0100
     2.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Feb 17 10:41:59 2004 +0100
     2.3 @@ -429,6 +429,7 @@
     2.4  val zle_add1_eq_le = thm "zle_add1_eq_le";
     2.5  val nonneg_eq_int = thm "nonneg_eq_int";
     2.6  val abs_minus_one = thm "abs_minus_one";
     2.7 +val of_int_number_of_eq = thm"of_int_number_of_eq";
     2.8  val nat_eq_iff = thm "nat_eq_iff";
     2.9  val nat_eq_iff2 = thm "nat_eq_iff2";
    2.10  val nat_less_iff = thm "nat_less_iff";
     3.1 --- a/src/HOL/Integ/NatBin.thy	Mon Feb 16 15:24:03 2004 +0100
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Feb 17 10:41:59 2004 +0100
     3.3 @@ -86,7 +86,7 @@
     3.4  	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
     3.5  
     3.6  
     3.7 -(** Successor **)
     3.8 +subsubsection{*Successor *}
     3.9  
    3.10  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    3.11  apply (rule sym)
    3.12 @@ -108,7 +108,7 @@
    3.13  done
    3.14  
    3.15  
    3.16 -(** Addition **)
    3.17 +subsubsection{*Addition *}
    3.18  
    3.19  (*"neg" is used in rewrite rules for binary comparisons*)
    3.20  lemma add_nat_number_of [simp]:
    3.21 @@ -121,7 +121,7 @@
    3.22            simp add: nat_number_of_def nat_add_distrib [symmetric]) 
    3.23  
    3.24  
    3.25 -(** Subtraction **)
    3.26 +subsubsection{*Subtraction *}
    3.27  
    3.28  lemma diff_nat_eq_if:
    3.29       "nat z - nat z' =  
    3.30 @@ -141,7 +141,7 @@
    3.31  
    3.32  
    3.33  
    3.34 -(** Multiplication **)
    3.35 +subsubsection{*Multiplication *}
    3.36  
    3.37  lemma mult_nat_number_of [simp]:
    3.38       "(number_of v :: nat) * number_of v' =  
    3.39 @@ -152,7 +152,7 @@
    3.40  
    3.41  
    3.42  
    3.43 -(** Quotient **)
    3.44 +subsubsection{*Quotient *}
    3.45  
    3.46  lemma div_nat_number_of [simp]:
    3.47       "(number_of v :: nat)  div  number_of v' =  
    3.48 @@ -167,7 +167,7 @@
    3.49  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    3.50  
    3.51  
    3.52 -(** Remainder **)
    3.53 +subsubsection{*Remainder *}
    3.54  
    3.55  lemma mod_nat_number_of [simp]:
    3.56       "(number_of v :: nat)  mod  number_of v' =  
    3.57 @@ -210,16 +210,16 @@
    3.58  *}
    3.59  
    3.60  
    3.61 -(*** Comparisons ***)
    3.62 +subsection{*Comparisons*}
    3.63  
    3.64 -(** Equals (=) **)
    3.65 +subsubsection{*Equals (=) *}
    3.66  
    3.67  lemma eq_nat_nat_iff:
    3.68       "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
    3.69  by (auto elim!: nonneg_eq_int)
    3.70  
    3.71  (*"neg" is used in rewrite rules for binary comparisons*)
    3.72 -lemma eq_nat_number_of:
    3.73 +lemma eq_nat_number_of [simp]:
    3.74       "((number_of v :: nat) = number_of v') =  
    3.75        (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
    3.76         else if neg (number_of v' :: int) then iszero (number_of v :: int)  
    3.77 @@ -231,21 +231,19 @@
    3.78  apply (simp add: not_neg_eq_ge_0 [symmetric])
    3.79  done
    3.80  
    3.81 -declare eq_nat_number_of [simp]
    3.82  
    3.83 -(** Less-than (<) **)
    3.84 +subsubsection{*Less-than (<) *}
    3.85  
    3.86  (*"neg" is used in rewrite rules for binary comparisons*)
    3.87 -lemma less_nat_number_of:
    3.88 +lemma less_nat_number_of [simp]:
    3.89       "((number_of v :: nat) < number_of v') =  
    3.90           (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
    3.91            else neg (number_of (bin_add v (bin_minus v')) :: int))"
    3.92 -apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
    3.93 +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
    3.94                  nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
    3.95 -            cong add: imp_cong, simp) 
    3.96 -done
    3.97 +         cong add: imp_cong, simp) 
    3.98  
    3.99 -declare less_nat_number_of [simp]
   3.100 +
   3.101  
   3.102  
   3.103  (*Maps #n to n for n = 0, 1, 2*)
   3.104 @@ -335,7 +333,7 @@
   3.105  done
   3.106  
   3.107  
   3.108 -(** Nat **)
   3.109 +subsubsection{*Nat *}
   3.110  
   3.111  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   3.112  by (simp add: numerals)
   3.113 @@ -344,7 +342,7 @@
   3.114    NOT suitable for rewriting because n recurs in the condition.*)
   3.115  lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   3.116  
   3.117 -(** Arith **)
   3.118 +subsubsection{*Arith *}
   3.119  
   3.120  lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   3.121  by (simp add: numerals)
   3.122 @@ -372,33 +370,31 @@
   3.123  declare diff_less' [of "number_of v", standard, simp]
   3.124  
   3.125  
   3.126 -(*** Comparisons involving (0::nat) ***)
   3.127 +subsection{*Comparisons involving (0::nat) *}
   3.128  
   3.129 -lemma eq_number_of_0:
   3.130 +text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   3.131 +
   3.132 +lemma eq_number_of_0 [simp]:
   3.133       "(number_of v = (0::nat)) =  
   3.134        (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   3.135 -apply (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   3.136 -done
   3.137 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   3.138  
   3.139 -lemma eq_0_number_of:
   3.140 +lemma eq_0_number_of [simp]:
   3.141       "((0::nat) = number_of v) =  
   3.142        (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   3.143 -apply (rule trans [OF eq_sym_conv eq_number_of_0])
   3.144 -done
   3.145 +by (rule trans [OF eq_sym_conv eq_number_of_0])
   3.146  
   3.147 -lemma less_0_number_of:
   3.148 +lemma less_0_number_of [simp]:
   3.149       "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
   3.150  by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   3.151  
   3.152 -(*Simplification already handles n<0, n<=0 and 0<=n.*)
   3.153 -declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
   3.154  
   3.155  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   3.156  by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   3.157  
   3.158  
   3.159  
   3.160 -(*** Comparisons involving Suc ***)
   3.161 +subsection{*Comparisons involving Suc *}
   3.162  
   3.163  lemma eq_number_of_Suc [simp]:
   3.164       "(number_of v = Suc n) =  
   3.165 @@ -415,8 +411,7 @@
   3.166       "(Suc n = number_of v) =  
   3.167          (let pv = number_of (bin_pred v) in  
   3.168           if neg pv then False else nat pv = n)"
   3.169 -apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
   3.170 -done
   3.171 +by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   3.172  
   3.173  lemma less_number_of_Suc [simp]:
   3.174       "(number_of v < Suc n) =  
   3.175 @@ -444,15 +439,13 @@
   3.176       "(number_of v <= Suc n) =  
   3.177          (let pv = number_of (bin_pred v) in  
   3.178           if neg pv then True else nat pv <= n)"
   3.179 -apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   3.180 -done
   3.181 +by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   3.182  
   3.183  lemma le_Suc_number_of [simp]:
   3.184       "(Suc n <= number_of v) =  
   3.185          (let pv = number_of (bin_pred v) in  
   3.186           if neg pv then False else n <= nat pv)"
   3.187 -apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   3.188 -done
   3.189 +by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   3.190  
   3.191  
   3.192  (* Push int(.) inwards: *)
   3.193 @@ -500,7 +493,7 @@
   3.194  
   3.195  
   3.196  
   3.197 -(*** Literal arithmetic involving powers, type nat ***)
   3.198 +subsection{*Literal arithmetic involving powers*}
   3.199  
   3.200  lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   3.201  apply (induct_tac "n")
   3.202 @@ -518,7 +511,7 @@
   3.203  
   3.204  
   3.205  
   3.206 -(*** Literal arithmetic involving powers, type int ***)
   3.207 +text{*For the integers*}
   3.208  
   3.209  lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
   3.210  by (simp add: zpower_zpower mult_commute)
   3.211 @@ -612,6 +605,40 @@
   3.212    by (simp add: Let_def)
   3.213  
   3.214  
   3.215 +subsection{*Literal arithmetic and @{term of_nat}*}
   3.216 +
   3.217 +lemma of_nat_double:
   3.218 +     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   3.219 +by (simp only: mult_2 nat_add_distrib of_nat_add) 
   3.220 +
   3.221 +lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   3.222 +by (simp only:  nat_number_of_def, simp)
   3.223 +
   3.224 +lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
   3.225 +by arith
   3.226 +
   3.227 +lemma of_nat_number_of_lemma:
   3.228 +     "of_nat (number_of v :: nat) =  
   3.229 +         (if 0 \<le> (number_of v :: int) 
   3.230 +          then (number_of v :: 'a :: number_ring)
   3.231 +          else 0)"
   3.232 +apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
   3.233 +apply (simp only: number_of nat_number_of_def)
   3.234 +txt{*Generalize in order to eliminate the function @{term number_of} and
   3.235 +its annoying simprules*}
   3.236 +apply (erule rev_mp)
   3.237 +apply (rule_tac x="number_of bin :: int" in spec) 
   3.238 +apply (rule_tac x="number_of bin :: 'a" in spec) 
   3.239 +apply (simp add: nat_add_distrib of_nat_double int_double_iff)
   3.240 +done
   3.241 +
   3.242 +lemma of_nat_number_of_eq [simp]:
   3.243 +     "of_nat (number_of v :: nat) =  
   3.244 +         (if neg (number_of v :: int) then 0  
   3.245 +          else (number_of v :: 'a :: number_ring))"
   3.246 +by (simp only: of_nat_number_of_lemma neg_def, simp) 
   3.247 +
   3.248 +
   3.249  subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   3.250  
   3.251  lemma nat_number_of_add_left:
   3.252 @@ -619,17 +646,16 @@
   3.253           (if neg (number_of v :: int) then number_of v' + k  
   3.254            else if neg (number_of v' :: int) then number_of v + k  
   3.255            else number_of (bin_add v v') + k)"
   3.256 -apply simp
   3.257 -done
   3.258 +by simp
   3.259  
   3.260  
   3.261 -(** For combine_numerals **)
   3.262 +subsubsection{*For @{text combine_numerals}*}
   3.263  
   3.264  lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   3.265  by (simp add: add_mult_distrib)
   3.266  
   3.267  
   3.268 -(** For cancel_numerals **)
   3.269 +subsubsection{*For @{text cancel_numerals}*}
   3.270  
   3.271  lemma nat_diff_add_eq1:
   3.272       "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   3.273 @@ -664,7 +690,7 @@
   3.274  by (auto split add: nat_diff_split simp add: add_mult_distrib)
   3.275  
   3.276  
   3.277 -(** For cancel_numeral_factors **)
   3.278 +subsubsection{*For @{text cancel_numeral_factors} *}
   3.279  
   3.280  lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   3.281  by auto
   3.282 @@ -679,7 +705,7 @@
   3.283  by auto
   3.284  
   3.285  
   3.286 -(** For cancel_factor **)
   3.287 +subsubsection{*For @{text cancel_factor} *}
   3.288  
   3.289  lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   3.290  by auto
   3.291 @@ -734,6 +760,7 @@
   3.292  val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
   3.293  val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
   3.294  val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
   3.295 +val of_nat_number_of_eq = thm"of_nat_number_of_eq";
   3.296  val nat_power_eq = thm"nat_power_eq";
   3.297  val power_nat_number_of = thm"power_nat_number_of";
   3.298  val zpower_even = thm"zpower_even";
     4.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Feb 16 15:24:03 2004 +0100
     4.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Feb 17 10:41:59 2004 +0100
     4.3 @@ -476,7 +476,7 @@
     4.4  (* reduce contradictory <= to False *)
     4.5  val add_rules =
     4.6      simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
     4.7 -    [numeral_0_eq_0, numeral_1_eq_1,
     4.8 +    [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
     4.9       minus_zero, diff_minus, left_minus, right_minus,
    4.10       mult_zero_left, mult_zero_right, mult_1, mult_1_right,
    4.11       minus_mult_left RS sym, minus_mult_right RS sym,
     5.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Feb 16 15:24:03 2004 +0100
     5.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Feb 17 10:41:59 2004 +0100
     5.3 @@ -3,12 +3,25 @@
     5.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5      Copyright   2000  University of Cambridge
     5.6  
     5.7 -Factor cancellation simprocs for the integers.
     5.8 +Factor cancellation simprocs for the integers (and for fields).
     5.9  
    5.10  This file can't be combined with int_arith1 because it requires IntDiv.thy.
    5.11  *)
    5.12  
    5.13 -(** Factor cancellation theorems for "int" **)
    5.14 +
    5.15 +(*To quote from Provers/Arith/cancel_numeral_factor.ML:
    5.16 +
    5.17 +Cancels common coefficients in balanced expressions:
    5.18 +
    5.19 +     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    5.20 +
    5.21 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    5.22 +and d = gcd(m,m') and n=m/d and n'=m'/d.
    5.23 +*)
    5.24 +
    5.25 +val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
    5.26 +
    5.27 +(** Factor cancellation theorems for integer division (div, not /) **)
    5.28  
    5.29  Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    5.30  by (stac zdiv_zmult_zmult1 1);
    5.31 @@ -31,13 +44,18 @@
    5.32    val dest_coeff        = dest_coeff 1
    5.33    val trans_tac         = trans_tac
    5.34    val norm_tac =
    5.35 -     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@mult_1s))
    5.36 +     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
    5.37       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    5.38       THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    5.39 -  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    5.40 -  val simplify_meta_eq  = simplify_meta_eq mult_1s
    5.41 +  val numeral_simp_tac  =
    5.42 +         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    5.43 +  val simplify_meta_eq  = 
    5.44 +	Int_Numeral_Simprocs.simplify_meta_eq
    5.45 +	     [add_0, add_0_right,
    5.46 +	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    5.47    end
    5.48  
    5.49 +(*Version for integer division*)
    5.50  structure DivCancelNumeralFactor = CancelNumeralFactorFun
    5.51   (open CancelNumeralFactorCommon
    5.52    val prove_conv = Bin_Simprocs.prove_conv
    5.53 @@ -47,20 +65,41 @@
    5.54    val neg_exchanges = false
    5.55  )
    5.56  
    5.57 +(*Version for fields*)
    5.58 +structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
    5.59 + (open CancelNumeralFactorCommon
    5.60 +  val prove_conv = Bin_Simprocs.prove_conv
    5.61 +  val mk_bal   = HOLogic.mk_binop "HOL.divide"
    5.62 +  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    5.63 +  val cancel = mult_divide_cancel_left RS trans
    5.64 +  val neg_exchanges = false
    5.65 +)
    5.66 +
    5.67 +(*Version for ordered rings: mult_cancel_left requires an ordering*)
    5.68  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    5.69   (open CancelNumeralFactorCommon
    5.70    val prove_conv = Bin_Simprocs.prove_conv
    5.71    val mk_bal   = HOLogic.mk_eq
    5.72 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    5.73 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    5.74    val cancel = mult_cancel_left RS trans
    5.75    val neg_exchanges = false
    5.76  )
    5.77  
    5.78 +(*Version for (unordered) fields*)
    5.79 +structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
    5.80 + (open CancelNumeralFactorCommon
    5.81 +  val prove_conv = Bin_Simprocs.prove_conv
    5.82 +  val mk_bal   = HOLogic.mk_eq
    5.83 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    5.84 +  val cancel = field_mult_cancel_left RS trans
    5.85 +  val neg_exchanges = false
    5.86 +)
    5.87 +
    5.88  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    5.89   (open CancelNumeralFactorCommon
    5.90    val prove_conv = Bin_Simprocs.prove_conv
    5.91    val mk_bal   = HOLogic.mk_binrel "op <"
    5.92 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    5.93 +  val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
    5.94    val cancel = mult_less_cancel_left RS trans
    5.95    val neg_exchanges = true
    5.96  )
    5.97 @@ -69,26 +108,46 @@
    5.98   (open CancelNumeralFactorCommon
    5.99    val prove_conv = Bin_Simprocs.prove_conv
   5.100    val mk_bal   = HOLogic.mk_binrel "op <="
   5.101 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   5.102 +  val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
   5.103    val cancel = mult_le_cancel_left RS trans
   5.104    val neg_exchanges = true
   5.105  )
   5.106  
   5.107 -val int_cancel_numeral_factors =
   5.108 +val ring_cancel_numeral_factors =
   5.109    map Bin_Simprocs.prep_simproc
   5.110 -   [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
   5.111 +   [("ring_eq_cancel_numeral_factor",
   5.112 +     ["(l::'a::{ordered_ring,number_ring}) * m = n",
   5.113 +      "(l::'a::{ordered_ring,number_ring}) = m * n"],
   5.114       EqCancelNumeralFactor.proc),
   5.115 -    ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
   5.116 +    ("ring_less_cancel_numeral_factor",
   5.117 +     ["(l::'a::{ordered_ring,number_ring}) * m < n",
   5.118 +      "(l::'a::{ordered_ring,number_ring}) < m * n"],
   5.119       LessCancelNumeralFactor.proc),
   5.120 -    ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
   5.121 +    ("ring_le_cancel_numeral_factor",
   5.122 +     ["(l::'a::{ordered_ring,number_ring}) * m <= n",
   5.123 +      "(l::'a::{ordered_ring,number_ring}) <= m * n"],
   5.124       LeCancelNumeralFactor.proc),
   5.125 -    ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   5.126 +    ("int_div_cancel_numeral_factors",
   5.127 +     ["((l::int) * m) div n", "(l::int) div (m * n)"],
   5.128       DivCancelNumeralFactor.proc)];
   5.129  
   5.130 +
   5.131 +val field_cancel_numeral_factors =
   5.132 +  map Bin_Simprocs.prep_simproc
   5.133 +   [("field_eq_cancel_numeral_factor",
   5.134 +     ["(l::'a::{field,number_ring}) * m = n",
   5.135 +      "(l::'a::{field,number_ring}) = m * n"],
   5.136 +     FieldEqCancelNumeralFactor.proc),
   5.137 +    ("field_cancel_numeral_factor",
   5.138 +     ["((l::'a::{field,number_ring}) * m) / n",
   5.139 +      "(l::'a::{field,number_ring}) / (m * n)",
   5.140 +      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
   5.141 +     FieldDivCancelNumeralFactor.proc)]
   5.142 +
   5.143  end;
   5.144  
   5.145 -Addsimprocs int_cancel_numeral_factors;
   5.146 -
   5.147 +Addsimprocs ring_cancel_numeral_factors;
   5.148 +Addsimprocs field_cancel_numeral_factors;
   5.149  
   5.150  (*examples:
   5.151  print_depth 22;
   5.152 @@ -125,6 +184,38 @@
   5.153  test "-x <= -23 * (y::int)";
   5.154  *)
   5.155  
   5.156 +(*And the same examples for fields such as rat or real:
   5.157 +test "0 <= (y::rat) * -2";
   5.158 +test "9*x = 12 * (y::rat)";
   5.159 +test "(9*x) / (12 * (y::rat)) = z";
   5.160 +test "9*x < 12 * (y::rat)";
   5.161 +test "9*x <= 12 * (y::rat)";
   5.162 +
   5.163 +test "-99*x = 132 * (y::rat)";
   5.164 +test "(-99*x) / (132 * (y::rat)) = z";
   5.165 +test "-99*x < 132 * (y::rat)";
   5.166 +test "-99*x <= 132 * (y::rat)";
   5.167 +
   5.168 +test "999*x = -396 * (y::rat)";
   5.169 +test "(999*x) / (-396 * (y::rat)) = z";
   5.170 +test "999*x < -396 * (y::rat)";
   5.171 +test "999*x <= -396 * (y::rat)";
   5.172 +
   5.173 +test  "(- ((2::rat) * x) <= 2 * y)";
   5.174 +test "-99*x = -81 * (y::rat)";
   5.175 +test "(-99*x) / (-81 * (y::rat)) = z";
   5.176 +test "-99*x <= -81 * (y::rat)";
   5.177 +test "-99*x < -81 * (y::rat)";
   5.178 +
   5.179 +test "-2 * x = -1 * (y::rat)";
   5.180 +test "-2 * x = -(y::rat)";
   5.181 +test "(-2 * x) / (-1 * (y::rat)) = z";
   5.182 +test "-2 * x < -(y::rat)";
   5.183 +test "-2 * x <= -1 * (y::rat)";
   5.184 +test "-x < -23 * (y::rat)";
   5.185 +test "-x <= -23 * (y::rat)";
   5.186 +*)
   5.187 +
   5.188  
   5.189  (** Declarations for ExtractCommonTerm **)
   5.190  
   5.191 @@ -178,13 +269,42 @@
   5.192  
   5.193  val int_cancel_factor =
   5.194    map Bin_Simprocs.prep_simproc
   5.195 -   [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
   5.196 -    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   5.197 +   [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], 
   5.198 +    EqCancelFactor.proc),
   5.199 +    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
   5.200       DivideCancelFactor.proc)];
   5.201  
   5.202 +(** Versions for all fields, including unordered ones (type complex).*)
   5.203 +
   5.204 +structure FieldEqCancelFactor = ExtractCommonTermFun
   5.205 + (open CancelFactorCommon
   5.206 +  val prove_conv = Bin_Simprocs.prove_conv
   5.207 +  val mk_bal   = HOLogic.mk_eq
   5.208 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   5.209 +  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
   5.210 +);
   5.211 +
   5.212 +structure FieldDivideCancelFactor = ExtractCommonTermFun
   5.213 + (open CancelFactorCommon
   5.214 +  val prove_conv = Bin_Simprocs.prove_conv
   5.215 +  val mk_bal   = HOLogic.mk_binop "HOL.divide"
   5.216 +  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   5.217 +  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
   5.218 +);
   5.219 +
   5.220 +val field_cancel_factor =
   5.221 +  map Bin_Simprocs.prep_simproc
   5.222 +   [("field_eq_cancel_factor",
   5.223 +     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
   5.224 +     FieldEqCancelFactor.proc),
   5.225 +    ("field_divide_cancel_factor",
   5.226 +     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
   5.227 +     FieldDivideCancelFactor.proc)];
   5.228 +
   5.229  end;
   5.230  
   5.231  Addsimprocs int_cancel_factor;
   5.232 +Addsimprocs field_cancel_factor;
   5.233  
   5.234  
   5.235  (*examples:
   5.236 @@ -204,3 +324,23 @@
   5.237  test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   5.238  *)
   5.239  
   5.240 +(*And the same examples for fields such as rat or real:
   5.241 +print_depth 22;
   5.242 +set timing;
   5.243 +set trace_simp;
   5.244 +fun test s = (Goal s; by (Asm_simp_tac 1));
   5.245 +
   5.246 +test "x*k = k*(y::rat)";
   5.247 +test "k = k*(y::rat)";
   5.248 +test "a*(b*c) = (b::rat)";
   5.249 +test "a*(b*c) = d*(b::rat)*(x*a)";
   5.250 +
   5.251 +
   5.252 +test "(x*k) / (k*(y::rat)) = (uu::rat)";
   5.253 +test "(k) / (k*(y::rat)) = (uu::rat)";
   5.254 +test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   5.255 +test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   5.256 +
   5.257 +(*FIXME: what do we do about this?*)
   5.258 +test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   5.259 +*)
     6.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon Feb 16 15:24:03 2004 +0100
     6.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Feb 17 10:41:59 2004 +0100
     6.3 @@ -512,7 +512,7 @@
     6.4     Suc_eq_number_of,eq_number_of_Suc,
     6.5     mult_Suc, mult_Suc_right,
     6.6     eq_number_of_0, eq_0_number_of, less_0_number_of,
     6.7 -   nat_number_of, if_True, if_False];
     6.8 +   of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
     6.9  
    6.10  val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@
    6.11                  Nat_Numeral_Simprocs.cancel_numerals;
     7.1 --- a/src/HOL/Real/rat_arith.ML	Mon Feb 16 15:24:03 2004 +0100
     7.2 +++ b/src/HOL/Real/rat_arith.ML	Tue Feb 17 10:41:59 2004 +0100
     7.3 @@ -8,236 +8,20 @@
     7.4  Instantiation of the generic linear arithmetic package for type rat.
     7.5  *)
     7.6  
     7.7 -(*FIXME DELETE*)
     7.8 +(*FIXME: these monomorphic versions are necessary because of a bug in the arith
     7.9 +  procedure*)
    7.10  val rat_mult_strict_left_mono =
    7.11      read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
    7.12  
    7.13  val rat_mult_left_mono =
    7.14   read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
    7.15  
    7.16 -	val le_number_of_eq = thm"le_number_of_eq";
    7.17 -
    7.18 -
    7.19 -(****Common factor cancellation****)
    7.20 -
    7.21 -(*To quote from Provers/Arith/cancel_numeral_factor.ML:
    7.22 -
    7.23 -This simproc Cancels common coefficients in balanced expressions:
    7.24 -
    7.25 -     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    7.26 -
    7.27 -where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    7.28 -and d = gcd(m,m') and n=m/d and n'=m'/d.
    7.29 -*)
    7.30 -
    7.31 -val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq]
    7.32 -
    7.33 -local open Int_Numeral_Simprocs
    7.34 -in
    7.35 -
    7.36 -structure CancelNumeralFactorCommon =
    7.37 -  struct
    7.38 -  val mk_coeff          = mk_coeff
    7.39 -  val dest_coeff        = dest_coeff 1
    7.40 -  val trans_tac         = trans_tac
    7.41 -  val norm_tac =
    7.42 -     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
    7.43 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    7.44 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    7.45 -  val numeral_simp_tac  =
    7.46 -         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    7.47 -  val simplify_meta_eq  = 
    7.48 -	Int_Numeral_Simprocs.simplify_meta_eq
    7.49 -	     [add_0, add_0_right,
    7.50 -	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    7.51 -  end
    7.52 -
    7.53 -structure DivCancelNumeralFactor = CancelNumeralFactorFun
    7.54 - (open CancelNumeralFactorCommon
    7.55 -  val prove_conv = Bin_Simprocs.prove_conv
    7.56 -  val mk_bal   = HOLogic.mk_binop "HOL.divide"
    7.57 -  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    7.58 -  val cancel = mult_divide_cancel_left RS trans
    7.59 -  val neg_exchanges = false
    7.60 -)
    7.61 -
    7.62 -structure EqCancelNumeralFactor = CancelNumeralFactorFun
    7.63 - (open CancelNumeralFactorCommon
    7.64 -  val prove_conv = Bin_Simprocs.prove_conv
    7.65 -  val mk_bal   = HOLogic.mk_eq
    7.66 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    7.67 -  val cancel = field_mult_cancel_left RS trans
    7.68 -  val neg_exchanges = false
    7.69 -)
    7.70 -
    7.71 -structure LessCancelNumeralFactor = CancelNumeralFactorFun
    7.72 - (open CancelNumeralFactorCommon
    7.73 -  val prove_conv = Bin_Simprocs.prove_conv
    7.74 -  val mk_bal   = HOLogic.mk_binrel "op <"
    7.75 -  val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
    7.76 -  val cancel = mult_less_cancel_left RS trans
    7.77 -  val neg_exchanges = true
    7.78 -)
    7.79 -
    7.80 -structure LeCancelNumeralFactor = CancelNumeralFactorFun
    7.81 - (open CancelNumeralFactorCommon
    7.82 -  val prove_conv = Bin_Simprocs.prove_conv
    7.83 -  val mk_bal   = HOLogic.mk_binrel "op <="
    7.84 -  val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
    7.85 -  val cancel = mult_le_cancel_left RS trans
    7.86 -  val neg_exchanges = true
    7.87 -)
    7.88 -
    7.89 -val field_cancel_numeral_factors_relations =
    7.90 -  map Bin_Simprocs.prep_simproc
    7.91 -   [("field_eq_cancel_numeral_factor",
    7.92 -     ["(l::'a::{field,number_ring}) * m = n",
    7.93 -      "(l::'a::{field,number_ring}) = m * n"],
    7.94 -     EqCancelNumeralFactor.proc),
    7.95 -    ("field_less_cancel_numeral_factor",
    7.96 -     ["(l::'a::{ordered_field,number_ring}) * m < n",
    7.97 -      "(l::'a::{ordered_field,number_ring}) < m * n"],
    7.98 -     LessCancelNumeralFactor.proc),
    7.99 -    ("field_le_cancel_numeral_factor",
   7.100 -     ["(l::'a::{ordered_field,number_ring}) * m <= n",
   7.101 -      "(l::'a::{ordered_field,number_ring}) <= m * n"],
   7.102 -     LeCancelNumeralFactor.proc)]
   7.103 -
   7.104 -val field_cancel_numeral_factors_divide = 
   7.105 -    Bin_Simprocs.prep_simproc
   7.106 -        ("field_cancel_numeral_factor",
   7.107 -         ["((l::'a::{field,number_ring}) * m) / n",
   7.108 -          "(l::'a::{field,number_ring}) / (m * n)",
   7.109 -          "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
   7.110 -         DivCancelNumeralFactor.proc)
   7.111 -
   7.112 -val field_cancel_numeral_factors =
   7.113 -    field_cancel_numeral_factors_relations @
   7.114 -    [field_cancel_numeral_factors_divide]
   7.115 -
   7.116 -end;
   7.117 -
   7.118 -Addsimprocs field_cancel_numeral_factors;
   7.119 -
   7.120 -
   7.121 -(*examples:
   7.122 -print_depth 22;
   7.123 -set timing;
   7.124 -set trace_simp;
   7.125 -fun test s = (Goal s; by (Simp_tac 1));
   7.126 -
   7.127 -test "0 <= (y::rat) * -2";
   7.128 -test "9*x = 12 * (y::rat)";
   7.129 -test "(9*x) / (12 * (y::rat)) = z";
   7.130 -test "9*x < 12 * (y::rat)";
   7.131 -test "9*x <= 12 * (y::rat)";
   7.132 -
   7.133 -test "-99*x = 132 * (y::rat)";
   7.134 -test "(-99*x) / (132 * (y::rat)) = z";
   7.135 -test "-99*x < 132 * (y::rat)";
   7.136 -test "-99*x <= 132 * (y::rat)";
   7.137 -
   7.138 -test "999*x = -396 * (y::rat)";
   7.139 -test "(999*x) / (-396 * (y::rat)) = z";
   7.140 -test "999*x < -396 * (y::rat)";
   7.141 -test "999*x <= -396 * (y::rat)";
   7.142 -
   7.143 -test  "(- ((2::rat) * x) <= 2 * y)";
   7.144 -test "-99*x = -81 * (y::rat)";
   7.145 -test "(-99*x) / (-81 * (y::rat)) = z";
   7.146 -test "-99*x <= -81 * (y::rat)";
   7.147 -test "-99*x < -81 * (y::rat)";
   7.148 -
   7.149 -test "-2 * x = -1 * (y::rat)";
   7.150 -test "-2 * x = -(y::rat)";
   7.151 -test "(-2 * x) / (-1 * (y::rat)) = z";
   7.152 -test "-2 * x < -(y::rat)";
   7.153 -test "-2 * x <= -1 * (y::rat)";
   7.154 -test "-x < -23 * (y::rat)";
   7.155 -test "-x <= -23 * (y::rat)";
   7.156 -*)
   7.157 -
   7.158 -
   7.159 -(** Declarations for ExtractCommonTerm **)
   7.160 -
   7.161 -local open Int_Numeral_Simprocs
   7.162 -in
   7.163 -
   7.164 -structure CancelFactorCommon =
   7.165 -  struct
   7.166 -  val mk_sum            = long_mk_prod
   7.167 -  val dest_sum          = dest_prod
   7.168 -  val mk_coeff          = mk_coeff
   7.169 -  val dest_coeff        = dest_coeff
   7.170 -  val find_first        = find_first []
   7.171 -  val trans_tac         = trans_tac
   7.172 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
   7.173 -  end;
   7.174 -
   7.175 -(*This version works for all fields, including unordered ones (complex).
   7.176 -  The version declared in int_factor_simprocs.ML is for integers.*)
   7.177 -structure EqCancelFactor = ExtractCommonTermFun
   7.178 - (open CancelFactorCommon
   7.179 -  val prove_conv = Bin_Simprocs.prove_conv
   7.180 -  val mk_bal   = HOLogic.mk_eq
   7.181 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   7.182 -  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
   7.183 -);
   7.184 -
   7.185 -
   7.186 -(*This version works for fields, with the generic divides operator (/).
   7.187 -  The version declared in int_factor_simprocs.ML for integers with div.*)
   7.188 -structure DivideCancelFactor = ExtractCommonTermFun
   7.189 - (open CancelFactorCommon
   7.190 -  val prove_conv = Bin_Simprocs.prove_conv
   7.191 -  val mk_bal   = HOLogic.mk_binop "HOL.divide"
   7.192 -  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   7.193 -  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
   7.194 -);
   7.195 -
   7.196 -val field_cancel_factor =
   7.197 -  map Bin_Simprocs.prep_simproc
   7.198 -   [("field_eq_cancel_factor",
   7.199 -     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
   7.200 -     EqCancelFactor.proc),
   7.201 -    ("field_divide_cancel_factor",
   7.202 -     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
   7.203 -     DivideCancelFactor.proc)];
   7.204 -
   7.205 -end;
   7.206 -
   7.207 -Addsimprocs field_cancel_factor;
   7.208 -
   7.209 -
   7.210 -(*examples:
   7.211 -print_depth 22;
   7.212 -set timing;
   7.213 -set trace_simp;
   7.214 -fun test s = (Goal s; by (Asm_simp_tac 1));
   7.215 -
   7.216 -test "x*k = k*(y::rat)";
   7.217 -test "k = k*(y::rat)";
   7.218 -test "a*(b*c) = (b::rat)";
   7.219 -test "a*(b*c) = d*(b::rat)*(x*a)";
   7.220 -
   7.221 -
   7.222 -test "(x*k) / (k*(y::rat)) = (uu::rat)";
   7.223 -test "(k) / (k*(y::rat)) = (uu::rat)";
   7.224 -test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   7.225 -test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   7.226 -
   7.227 -(*FIXME: what do we do about this?*)
   7.228 -test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   7.229 -*)
   7.230 -
   7.231 -
   7.232  
   7.233  (****Instantiation of the generic linear arithmetic package for fields****)
   7.234  
   7.235 -
   7.236  local
   7.237  
   7.238 -val simprocs = [field_cancel_numeral_factors_divide]
   7.239 +val simprocs = field_cancel_numeral_factors
   7.240  
   7.241  val mono_ss = simpset() addsimps
   7.242                  [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
   7.243 @@ -259,10 +43,11 @@
   7.244    (rat_mult_left_mono,
   7.245     cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
   7.246  
   7.247 -val simps = [order_less_irrefl, True_implies_equals,
   7.248 +val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
   7.249               inst "a" "(number_of ?v)" right_distrib,
   7.250               divide_1, divide_zero_left,
   7.251               times_divide_eq_right, times_divide_eq_left,
   7.252 +             minus_divide_left RS sym, minus_divide_right RS sym,
   7.253  	     of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
   7.254  	     of_int_mult, of_int_of_nat_eq];
   7.255  
     8.1 --- a/src/HOL/Real/real_arith.ML	Mon Feb 16 15:24:03 2004 +0100
     8.2 +++ b/src/HOL/Real/real_arith.ML	Tue Feb 17 10:41:59 2004 +0100
     8.3 @@ -111,6 +111,8 @@
     8.4  val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
     8.5  val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
     8.6  val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
     8.7 +val real_number_of = thm"real_number_of";
     8.8 +val real_of_nat_number_of = thm"real_of_nat_number_of";
     8.9  
    8.10  
    8.11  (****Instantiation of the generic linear arithmetic package****)
    8.12 @@ -128,7 +130,8 @@
    8.13  val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
    8.14         real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
    8.15         real_of_int_minus RS sym, real_of_int_diff RS sym,
    8.16 -       real_of_int_mult RS sym];
    8.17 +       real_of_int_mult RS sym,
    8.18 +       real_of_nat_number_of, real_number_of];
    8.19  
    8.20  val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
    8.21                      real_of_int_inject RS iffD2];