Simplification of the development of Integers
authorpaulson
Wed Dec 03 10:49:34 2003 +0100 (2003-12-03)
changeset 142718ed6989228bb
parent 14270 342451d763f9
child 14272 5efbb548107d
Simplification of the development of Integers
src/HOL/Integ/Bin.ML
src/HOL/Integ/Int.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/Presburger.thy
src/HOL/Integ/int_arith1.ML
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/IntFact.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/ROOT.ML
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/Presburger.thy
src/HOL/Real/RealOrd.thy
     1.1 --- a/src/HOL/Integ/Bin.ML	Tue Dec 02 11:48:15 2003 +0100
     1.2 +++ b/src/HOL/Integ/Bin.ML	Wed Dec 03 10:49:34 2003 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4  (** Special-case simplification for small constants **)
     1.5  
     1.6  Goal "-1 * z = -(z::int)";
     1.7 -by (simp_tac (simpset() addsimps zcompare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
     1.8 +by (simp_tac (simpset() addsimps compare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
     1.9  qed "zmult_minus1";
    1.10  
    1.11  Goal "z * -1 = -(z::int)";
    1.12 @@ -243,7 +243,7 @@
    1.13    "((number_of x::int) = number_of y) = \
    1.14  \  iszero (number_of (bin_add x (bin_minus y)))"; 
    1.15  by (simp_tac (simpset()
    1.16 -                 addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1); 
    1.17 +                 addsimps compare_rls @ [number_of_add, number_of_minus]) 1); 
    1.18  qed "eq_number_of_eq"; 
    1.19  
    1.20  Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)"; 
    1.21 @@ -261,7 +261,7 @@
    1.22  by (int_case_tac "number_of w" 1); 
    1.23  by (ALLGOALS 
    1.24      (asm_simp_tac 
    1.25 -     (simpset() addsimps zcompare_rls @ 
    1.26 +     (simpset() addsimps compare_rls @ 
    1.27    	                 [zero_reorient, zminus_zadd_distrib RS sym, 
    1.28                            int_Suc0_eq_1 RS sym, zadd_int]))); 
    1.29  qed "iszero_number_of_BIT"; 
    1.30 @@ -299,7 +299,7 @@
    1.31  by (int_case_tac "number_of w" 1); 
    1.32  by (ALLGOALS (asm_simp_tac 
    1.33  	      (simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int, 
    1.34 -                         neg_eq_less_0, symmetric zdiff_def] @ zcompare_rls)));
    1.35 +                         neg_eq_less_0, symmetric zdiff_def] @ compare_rls)));
    1.36  qed "neg_number_of_BIT"; 
    1.37  
    1.38  
     2.1 --- a/src/HOL/Integ/Int.thy	Tue Dec 02 11:48:15 2003 +0100
     2.2 +++ b/src/HOL/Integ/Int.thy	Wed Dec 03 10:49:34 2003 +0100
     2.3 @@ -4,19 +4,10 @@
     2.4      Copyright   1998  University of Cambridge
     2.5  *)
     2.6  
     2.7 -header {*Type "int" is a Linear Order and Other Lemmas*}
     2.8 +header {*Type "int" is an Ordered Ring and Other Lemmas*}
     2.9  
    2.10  theory Int = IntDef:
    2.11  
    2.12 -instance int :: order
    2.13 -proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
    2.14 -
    2.15 -instance int :: plus_ac0
    2.16 -proof qed (rule zadd_commute zadd_assoc zadd_0)+
    2.17 -
    2.18 -instance int :: linorder
    2.19 -proof qed (rule zle_linear)
    2.20 -
    2.21  constdefs
    2.22     nat  :: "int => nat"
    2.23      "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
    2.24 @@ -63,152 +54,9 @@
    2.25  by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    2.26  
    2.27  
    2.28 -
    2.29 -subsection{*@{text Abel_Cancel} simproc on the integers*}
    2.30 -
    2.31 -(* Lemmas needed for the simprocs *)
    2.32 -
    2.33 -(*Deletion of other terms in the formula, seeking the -x at the front of z*)
    2.34 -lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
    2.35 -apply (subst zadd_left_commute)
    2.36 -apply (rule zadd_left_cancel)
    2.37 -done
    2.38 -
    2.39 -(*A further rule to deal with the case that
    2.40 -  everything gets cancelled on the right.*)
    2.41 -lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
    2.42 -apply (subst zadd_left_commute)
    2.43 -apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
    2.44 -apply (simp add: eq_zdiff_eq [symmetric])
    2.45 -done
    2.46 -
    2.47 -(*Legacy ML bindings, but no longer the structure Int.*)
    2.48 -ML
    2.49 -{*
    2.50 -val Int_thy = the_context ()
    2.51 -val zabs_def = thm "zabs_def"
    2.52 -val nat_def  = thm "nat_def"
    2.53 -
    2.54 -val int_0 = thm "int_0";
    2.55 -val int_1 = thm "int_1";
    2.56 -val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
    2.57 -val neg_eq_less_0 = thm "neg_eq_less_0";
    2.58 -val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
    2.59 -val not_neg_0 = thm "not_neg_0";
    2.60 -val not_neg_1 = thm "not_neg_1";
    2.61 -val iszero_0 = thm "iszero_0";
    2.62 -val not_iszero_1 = thm "not_iszero_1";
    2.63 -val int_0_less_1 = thm "int_0_less_1";
    2.64 -val int_0_neq_1 = thm "int_0_neq_1";
    2.65 -val zadd_cancel_21 = thm "zadd_cancel_21";
    2.66 -val zadd_cancel_end = thm "zadd_cancel_end";
    2.67 -
    2.68 -structure Int_Cancel_Data =
    2.69 -struct
    2.70 -  val ss		= HOL_ss
    2.71 -  val eq_reflection	= eq_reflection
    2.72 -
    2.73 -  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context()))
    2.74 -  val T		= HOLogic.intT
    2.75 -  val zero		= Const ("0", HOLogic.intT)
    2.76 -  val restrict_to_left  = restrict_to_left
    2.77 -  val add_cancel_21	= zadd_cancel_21
    2.78 -  val add_cancel_end	= zadd_cancel_end
    2.79 -  val add_left_cancel	= zadd_left_cancel
    2.80 -  val add_assoc		= zadd_assoc
    2.81 -  val add_commute	= zadd_commute
    2.82 -  val add_left_commute	= zadd_left_commute
    2.83 -  val add_0		= zadd_0
    2.84 -  val add_0_right	= zadd_0_right
    2.85 -
    2.86 -  val eq_diff_eq	= eq_zdiff_eq
    2.87 -  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
    2.88 -  fun dest_eqI th = 
    2.89 -      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
    2.90 -	      (HOLogic.dest_Trueprop (concl_of th)))
    2.91 -
    2.92 -  val diff_def		= zdiff_def
    2.93 -  val minus_add_distrib	= zminus_zadd_distrib
    2.94 -  val minus_minus	= zminus_zminus
    2.95 -  val minus_0		= zminus_0
    2.96 -  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2]
    2.97 -  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
    2.98 -end;
    2.99 +subsection{*Comparison laws*}
   2.100  
   2.101 -structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
   2.102 -
   2.103 -Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   2.104 -*}
   2.105 -
   2.106 -
   2.107 -subsection{*Misc Results*}
   2.108 -
   2.109 -lemma zminus_zdiff_eq [simp]: "- (z - y) = y - (z::int)"
   2.110 -by simp
   2.111 -
   2.112 -lemma zless_eq_neg: "(w<z) = neg(w-z)"
   2.113 -by (simp add: zless_def)
   2.114 -
   2.115 -lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
   2.116 -by (simp add: iszero_def zdiff_eq_eq)
   2.117 -
   2.118 -lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
   2.119 -by (simp add: zle_def zless_def)
   2.120 -
   2.121 -subsection{*Inequality reasoning*}
   2.122 -
   2.123 -lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   2.124 -apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
   2.125 -apply (rule_tac x = "Suc n" in exI)
   2.126 -apply (simp add: int_Suc)
   2.127 -done
   2.128 -
   2.129 -lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
   2.130 -apply (simp add: zle_def zless_add1_eq)
   2.131 -apply (auto intro: zless_asym zle_anti_sym
   2.132 -            simp add: order_less_imp_le symmetric zle_def)
   2.133 -done
   2.134 -
   2.135 -lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
   2.136 -apply (subst zadd_commute)
   2.137 -apply (rule add1_zle_eq)
   2.138 -done
   2.139 -
   2.140 -
   2.141 -subsection{*Monotonicity results*}
   2.142 -
   2.143 -lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
   2.144 -by simp
   2.145 -
   2.146 -lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
   2.147 -by simp
   2.148 -
   2.149 -lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
   2.150 -by simp
   2.151 -
   2.152 -lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
   2.153 -by simp
   2.154 -
   2.155 -(*"v\<le>w ==> v+z \<le> w+z"*)
   2.156 -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
   2.157 -
   2.158 -(*"v\<le>w ==> z+v \<le> z+w"*)
   2.159 -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
   2.160 -
   2.161 -(*"v\<le>w ==> v+z \<le> w+z"*)
   2.162 -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
   2.163 -
   2.164 -(*"v\<le>w ==> z+v \<le> z+w"*)
   2.165 -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
   2.166 -
   2.167 -lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
   2.168 -by (erule zadd_zle_mono1 [THEN zle_trans], simp)
   2.169 -
   2.170 -lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
   2.171 -by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
   2.172 -
   2.173 -
   2.174 -subsection{*Comparison laws*}
   2.175 +(*ring and field?*)
   2.176  
   2.177  lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
   2.178  by (simp add: zless_def zdiff_def zadd_ac)
   2.179 @@ -237,7 +85,132 @@
   2.180  by auto
   2.181  
   2.182  
   2.183 -subsection{*Instances of the equations above, for zero*}
   2.184 +subsection{*nat: magnitide of an integer, as a natural number*}
   2.185 +
   2.186 +lemma nat_int [simp]: "nat(int n) = n"
   2.187 +by (unfold nat_def, auto)
   2.188 +
   2.189 +lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
   2.190 +apply (unfold nat_def)
   2.191 +apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
   2.192 +done
   2.193 +
   2.194 +lemma nat_zero [simp]: "nat 0 = 0"
   2.195 +apply (unfold Zero_int_def)
   2.196 +apply (rule nat_int)
   2.197 +done
   2.198 +
   2.199 +lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   2.200 +apply (drule not_neg_eq_ge_0 [THEN iffD1])
   2.201 +apply (drule zle_imp_zless_or_eq)
   2.202 +apply (auto simp add: zless_iff_Suc_zadd)
   2.203 +done
   2.204 +
   2.205 +lemma neg_nat: "neg z ==> nat z = 0"
   2.206 +by (unfold nat_def, auto)
   2.207 +
   2.208 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   2.209 +apply (case_tac "neg z")
   2.210 +apply (erule_tac [2] not_neg_nat [THEN subst])
   2.211 +apply (auto simp add: neg_nat)
   2.212 +apply (auto dest: order_less_trans simp add: neg_eq_less_0)
   2.213 +done
   2.214 +
   2.215 +lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
   2.216 +by (simp add: neg_eq_less_0 zle_def not_neg_nat)
   2.217 +
   2.218 +lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   2.219 +by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
   2.220 +
   2.221 +(*An alternative condition is  0 \<le> w  *)
   2.222 +lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   2.223 +apply (subst zless_int [symmetric])
   2.224 +apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
   2.225 +apply (case_tac "neg w")
   2.226 + apply (simp add: neg_eq_less_0 neg_nat)
   2.227 + apply (blast intro: order_less_trans)
   2.228 +apply (simp add: not_neg_nat)
   2.229 +done
   2.230 +
   2.231 +lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
   2.232 +apply (case_tac "0 < z")
   2.233 +apply (auto simp add: nat_mono_iff linorder_not_less)
   2.234 +done
   2.235 +
   2.236 +
   2.237 +subsection{*Monotonicity results*}
   2.238 +
   2.239 +(*RING AND FIELD?*)
   2.240 +
   2.241 +lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
   2.242 +by (simp add: zless_def zdiff_def zadd_ac) 
   2.243 +
   2.244 +lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
   2.245 +by (simp add: zless_def zdiff_def zadd_ac) 
   2.246 +
   2.247 +lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
   2.248 +by (simp add: linorder_not_less [symmetric]) 
   2.249 +
   2.250 +lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
   2.251 +by (simp add: linorder_not_less [symmetric]) 
   2.252 +
   2.253 +(*"v\<le>w ==> v+z \<le> w+z"*)
   2.254 +lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
   2.255 +
   2.256 +(*"v\<le>w ==> z+v \<le> z+w"*)
   2.257 +lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
   2.258 +
   2.259 +(*"v\<le>w ==> v+z \<le> w+z"*)
   2.260 +lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
   2.261 +
   2.262 +(*"v\<le>w ==> z+v \<le> z+w"*)
   2.263 +lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
   2.264 +
   2.265 +lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
   2.266 +by (erule zadd_zle_mono1 [THEN zle_trans], simp)
   2.267 +
   2.268 +lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
   2.269 +by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
   2.270 +
   2.271 +
   2.272 +subsection{*Strict Monotonicity of Multiplication*}
   2.273 +
   2.274 +text{*strict, in 1st argument; proof is by induction on k>0*}
   2.275 +lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
   2.276 +apply (induct_tac "k", simp) 
   2.277 +apply (simp add: int_Suc)
   2.278 +apply (case_tac "n=0")
   2.279 +apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
   2.280 +apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
   2.281 +done
   2.282 +
   2.283 +lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   2.284 +apply (rule_tac t = k in not_neg_nat [THEN subst])
   2.285 +apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
   2.286 +apply (simp add: not_neg_eq_ge_0 order_le_less)
   2.287 +apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
   2.288 +done
   2.289 +
   2.290 +text{*The Integers Form an Ordered Ring*}
   2.291 +instance int :: ordered_ring
   2.292 +proof
   2.293 +  fix i j k :: int
   2.294 +  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
   2.295 +  show "i + j = j + i" by (simp add: zadd_commute)
   2.296 +  show "0 + i = i" by simp
   2.297 +  show "- i + i = 0" by simp
   2.298 +  show "i - j = i + (-j)" by (simp add: zdiff_def)
   2.299 +  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
   2.300 +  show "i * j = j * i" by (rule zmult_commute)
   2.301 +  show "1 * i = i" by simp
   2.302 +  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   2.303 +  show "0 \<noteq> (1::int)" by simp
   2.304 +  show "i \<le> j ==> k + i \<le> k + j" by simp
   2.305 +  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
   2.306 +  show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
   2.307 +qed
   2.308 +
   2.309 +subsection{*Lemmas about the Function @{term int} and Orderings*}
   2.310  
   2.311  lemma negative_zless_0: "- (int (Suc n)) < 0"
   2.312  by (simp add: zless_def)
   2.313 @@ -279,116 +252,36 @@
   2.314  by (simp add: zabs_def)
   2.315  
   2.316  
   2.317 -subsection{*nat: magnitide of an integer, as a natural number*}
   2.318 -
   2.319 -lemma nat_int [simp]: "nat(int n) = n"
   2.320 -by (unfold nat_def, auto)
   2.321 -
   2.322 -lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
   2.323 -apply (unfold nat_def)
   2.324 -apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
   2.325 -done
   2.326 -
   2.327 -lemma nat_zero [simp]: "nat 0 = 0"
   2.328 -apply (unfold Zero_int_def)
   2.329 -apply (rule nat_int)
   2.330 -done
   2.331 +subsection{*Misc Results*}
   2.332  
   2.333 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   2.334 -apply (drule not_neg_eq_ge_0 [THEN iffD1])
   2.335 -apply (drule zle_imp_zless_or_eq)
   2.336 -apply (auto simp add: zless_iff_Suc_zadd)
   2.337 -done
   2.338 -
   2.339 -lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
   2.340 -by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd zdiff_eq_eq [symmetric] zdiff_def)
   2.341 -
   2.342 -lemma neg_nat: "neg z ==> nat z = 0"
   2.343 -by (unfold nat_def, auto)
   2.344 -
   2.345 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   2.346 -apply (case_tac "neg z")
   2.347 -apply (erule_tac [2] not_neg_nat [THEN subst])
   2.348 -apply (auto simp add: neg_nat)
   2.349 -apply (auto dest: order_less_trans simp add: neg_eq_less_0)
   2.350 -done
   2.351 -
   2.352 -lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
   2.353 -by (simp add: neg_eq_less_0 zle_def not_neg_nat)
   2.354 -
   2.355 -lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   2.356 -by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
   2.357 +lemma zless_eq_neg: "(w<z) = neg(w-z)"
   2.358 +by (simp add: zless_def)
   2.359  
   2.360 -(*An alternative condition is  0 \<le> w  *)
   2.361 -lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   2.362 -apply (subst zless_int [symmetric])
   2.363 -apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
   2.364 -apply (case_tac "neg w")
   2.365 - apply (simp add: neg_eq_less_0 neg_nat)
   2.366 - apply (blast intro: order_less_trans)
   2.367 -apply (simp add: not_neg_nat)
   2.368 -done
   2.369 -
   2.370 -lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
   2.371 -apply (case_tac "0 < z")
   2.372 -apply (auto simp add: nat_mono_iff linorder_not_less)
   2.373 -done
   2.374 -
   2.375 -
   2.376 -subsection{*Strict Monotonicity of Multiplication*}
   2.377 -
   2.378 -text{*strict, in 1st argument; proof is by induction on k>0*}
   2.379 -lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
   2.380 -apply (induct_tac "k", simp) 
   2.381 -apply (simp add: int_Suc)
   2.382 -apply (case_tac "n=0")
   2.383 -apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
   2.384 -done
   2.385 +lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
   2.386 +by (simp add: iszero_def diff_eq_eq)
   2.387  
   2.388 -lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   2.389 -apply (rule_tac t = k in not_neg_nat [THEN subst])
   2.390 -apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
   2.391 -apply (simp add: not_neg_eq_ge_0 order_le_less)
   2.392 -apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
   2.393 -done
   2.394 +lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
   2.395 +by (simp add: zle_def zless_def)
   2.396  
   2.397 -text{*The Integers Form an Ordered Ring*}
   2.398 -instance int :: ordered_ring
   2.399 -proof
   2.400 -  fix i j k :: int
   2.401 -  show "(i + j) + k = i + (j + k)" by simp
   2.402 -  show "i + j = j + i" by simp
   2.403 -  show "0 + i = i" by simp
   2.404 -  show "- i + i = 0" by simp
   2.405 -  show "i - j = i + (-j)" by simp
   2.406 -  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
   2.407 -  show "i * j = j * i" by (rule zmult_commute)
   2.408 -  show "1 * i = i" by simp
   2.409 -  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   2.410 -  show "0 \<noteq> (1::int)" by simp
   2.411 -  show "i \<le> j ==> k + i \<le> k + j" by simp
   2.412 -  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
   2.413 -  show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
   2.414 -qed
   2.415  
   2.416  subsection{*Monotonicity of Multiplication*}
   2.417  
   2.418  lemma zmult_zle_mono1: "[| i \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*k"
   2.419 -  by (rule mult_right_mono)
   2.420 +  by (rule Ring_and_Field.mult_right_mono)
   2.421  
   2.422  lemma zmult_zle_mono1_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> j*k \<le> i*k"
   2.423 -  by (rule mult_right_mono_neg)
   2.424 +  by (rule Ring_and_Field.mult_right_mono_neg)
   2.425  
   2.426  lemma zmult_zle_mono2: "[| i \<le> j;  (0::int) \<le> k |] ==> k*i \<le> k*j"
   2.427 -  by (rule mult_left_mono)
   2.428 +  by (rule Ring_and_Field.mult_left_mono)
   2.429  
   2.430  lemma zmult_zle_mono2_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> k*j \<le> k*i"
   2.431 -  by (rule mult_left_mono_neg)
   2.432 +  by (rule Ring_and_Field.mult_left_mono_neg)
   2.433  
   2.434  (* \<le> monotonicity, BOTH arguments*)
   2.435  lemma zmult_zle_mono:
   2.436       "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
   2.437 -  by (rule mult_mono)
   2.438 +  by (rule Ring_and_Field.mult_mono)
   2.439  
   2.440  lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
   2.441    by (rule Ring_and_Field.mult_strict_right_mono)
   2.442 @@ -423,13 +316,108 @@
   2.443  lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
   2.444   by (rule Ring_and_Field.mult_cancel_left)
   2.445  
   2.446 -(*Analogous to zadd_int*)
   2.447 -lemma zdiff_int [rule_format]: "n\<le>m --> int m - int n = int (m-n)"
   2.448 -apply (induct_tac m n rule: diff_induct)
   2.449 -apply (auto simp add: int_Suc symmetric zdiff_def)
   2.450 +
   2.451 +subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
   2.452 +
   2.453 +(* Lemmas needed for the simprocs *)
   2.454 +
   2.455 +(** The idea is to cancel like terms on opposite sides by subtraction **)
   2.456 +
   2.457 +lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
   2.458 +by (simp add: zless_def)
   2.459 +
   2.460 +lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
   2.461 +apply (drule zless_eqI)
   2.462 +apply (simp (no_asm_simp) add: zle_def)
   2.463 +done
   2.464 +
   2.465 +lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
   2.466 +apply safe
   2.467 +apply (simp_all add: eq_diff_eq diff_eq_eq)
   2.468 +done
   2.469 +
   2.470 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
   2.471 +lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
   2.472 +apply (subst zadd_left_commute)
   2.473 +apply (rule zadd_left_cancel)
   2.474 +done
   2.475 +
   2.476 +(*A further rule to deal with the case that
   2.477 +  everything gets cancelled on the right.*)
   2.478 +lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
   2.479 +apply (subst zadd_left_commute)
   2.480 +apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
   2.481 +apply (simp add: eq_diff_eq [symmetric])
   2.482  done
   2.483  
   2.484 -(* a case theorem distinguishing non-negative and negative int *)  
   2.485 +(*Legacy ML bindings, but no longer the structure Int.*)
   2.486 +ML
   2.487 +{*
   2.488 +val Int_thy = the_context ()
   2.489 +val zabs_def = thm "zabs_def"
   2.490 +val nat_def  = thm "nat_def"
   2.491 +
   2.492 +val zless_eqI = thm "zless_eqI";
   2.493 +val zle_eqI = thm "zle_eqI";
   2.494 +val zeq_eqI = thm "zeq_eqI";
   2.495 +
   2.496 +val int_0 = thm "int_0";
   2.497 +val int_1 = thm "int_1";
   2.498 +val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
   2.499 +val neg_eq_less_0 = thm "neg_eq_less_0";
   2.500 +val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
   2.501 +val not_neg_0 = thm "not_neg_0";
   2.502 +val not_neg_1 = thm "not_neg_1";
   2.503 +val iszero_0 = thm "iszero_0";
   2.504 +val not_iszero_1 = thm "not_iszero_1";
   2.505 +val int_0_less_1 = thm "int_0_less_1";
   2.506 +val int_0_neq_1 = thm "int_0_neq_1";
   2.507 +val zadd_cancel_21 = thm "zadd_cancel_21";
   2.508 +val zadd_cancel_end = thm "zadd_cancel_end";
   2.509 +
   2.510 +structure Int_Cancel_Data =
   2.511 +struct
   2.512 +  val ss		= HOL_ss
   2.513 +  val eq_reflection	= eq_reflection
   2.514 +
   2.515 +  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context()))
   2.516 +  val T		= HOLogic.intT
   2.517 +  val zero		= Const ("0", HOLogic.intT)
   2.518 +  val restrict_to_left  = restrict_to_left
   2.519 +  val add_cancel_21	= zadd_cancel_21
   2.520 +  val add_cancel_end	= zadd_cancel_end
   2.521 +  val add_left_cancel	= zadd_left_cancel
   2.522 +  val add_assoc		= zadd_assoc
   2.523 +  val add_commute	= zadd_commute
   2.524 +  val add_left_commute	= zadd_left_commute
   2.525 +  val add_0		= zadd_0
   2.526 +  val add_0_right	= zadd_0_right
   2.527 +
   2.528 +  val eq_diff_eq	= eq_diff_eq
   2.529 +  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
   2.530 +  fun dest_eqI th = 
   2.531 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
   2.532 +	      (HOLogic.dest_Trueprop (concl_of th)))
   2.533 +
   2.534 +  val diff_def		= zdiff_def
   2.535 +  val minus_add_distrib	= zminus_zadd_distrib
   2.536 +  val minus_minus	= zminus_zminus
   2.537 +  val minus_0		= zminus_0
   2.538 +  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2]
   2.539 +  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
   2.540 +end;
   2.541 +
   2.542 +structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
   2.543 +
   2.544 +Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   2.545 +*}
   2.546 +
   2.547 +
   2.548 +text{*A case theorem distinguishing non-negative and negative int*}
   2.549 +
   2.550 +lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
   2.551 +by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd 
   2.552 +                   diff_eq_eq [symmetric] zdiff_def)
   2.553  
   2.554  lemma int_cases: 
   2.555       "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   2.556 @@ -439,11 +427,31 @@
   2.557  done
   2.558  
   2.559  
   2.560 +subsection{*Inequality reasoning*}
   2.561 +
   2.562 +text{*Are they needed????*}
   2.563 +lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   2.564 +apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
   2.565 +apply (rule_tac x = "Suc n" in exI)
   2.566 +apply (simp add: int_Suc)
   2.567 +done
   2.568 +
   2.569 +lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
   2.570 +apply (simp add: zle_def zless_add1_eq)
   2.571 +apply (auto intro: zless_asym zle_anti_sym
   2.572 +            simp add: order_less_imp_le symmetric zle_def)
   2.573 +done
   2.574 +
   2.575 +lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
   2.576 +apply (subst zadd_commute)
   2.577 +apply (rule add1_zle_eq)
   2.578 +done
   2.579 +
   2.580 +
   2.581  
   2.582  
   2.583  ML
   2.584  {*
   2.585 -val zminus_zdiff_eq = thm "zminus_zdiff_eq";
   2.586  val zless_eq_neg = thm "zless_eq_neg";
   2.587  val eq_eq_iszero = thm "eq_eq_iszero";
   2.588  val zle_eq_not_neg = thm "zle_eq_not_neg";
   2.589 @@ -468,12 +476,9 @@
   2.590  val zminus_zle = thm "zminus_zle";
   2.591  val equation_zminus = thm "equation_zminus";
   2.592  val zminus_equation = thm "zminus_equation";
   2.593 -val negative_zless_0 = thm "negative_zless_0";
   2.594  val negative_zless = thm "negative_zless";
   2.595 -val negative_zle_0 = thm "negative_zle_0";
   2.596  val negative_zle = thm "negative_zle";
   2.597  val not_zle_0_negative = thm "not_zle_0_negative";
   2.598 -val int_zle_neg = thm "int_zle_neg";
   2.599  val not_int_zless_negative = thm "not_int_zless_negative";
   2.600  val negative_eq_positive = thm "negative_eq_positive";
   2.601  val zle_iff_zadd = thm "zle_iff_zadd";
   2.602 @@ -482,7 +487,6 @@
   2.603  val nat_zminus_int = thm "nat_zminus_int";
   2.604  val nat_zero = thm "nat_zero";
   2.605  val not_neg_nat = thm "not_neg_nat";
   2.606 -val negD = thm "negD";
   2.607  val neg_nat = thm "neg_nat";
   2.608  val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
   2.609  val nat_0_le = thm "nat_0_le";
   2.610 @@ -505,7 +509,6 @@
   2.611  val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
   2.612  val zmult_cancel2 = thm "zmult_cancel2";
   2.613  val zmult_cancel1 = thm "zmult_cancel1";
   2.614 -val zdiff_int = thm "zdiff_int";
   2.615  *}
   2.616  
   2.617  end
     3.1 --- a/src/HOL/Integ/IntArith.thy	Tue Dec 02 11:48:15 2003 +0100
     3.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Dec 03 10:49:34 2003 +0100
     3.3 @@ -202,8 +202,7 @@
     3.4  lemma int_val_lemma:
     3.5       "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
     3.6        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
     3.7 -apply (induct_tac "n")
     3.8 - apply (simp (no_asm_simp))
     3.9 +apply (induct_tac "n", simp)
    3.10  apply (intro strip)
    3.11  apply (erule impE, simp)
    3.12  apply (erule_tac x = n in allE, simp)
    3.13 @@ -293,9 +292,9 @@
    3.14  
    3.15  lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
    3.16  apply (case_tac "0<m")
    3.17 -apply (simp (no_asm_simp) add: pos_zmult_eq_1_iff)
    3.18 +apply (simp add: pos_zmult_eq_1_iff)
    3.19  apply (case_tac "m=0")
    3.20 -apply (simp (no_asm_simp) del: number_of_reorient)
    3.21 +apply (simp del: number_of_reorient)
    3.22  apply (subgoal_tac "0 < -m")
    3.23  apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
    3.24  done
    3.25 @@ -303,22 +302,26 @@
    3.26  
    3.27  subsection{*More about nat*}
    3.28  
    3.29 +(*Analogous to zadd_int*)
    3.30 +lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
    3.31 +by (induct m n rule: diff_induct, simp_all)
    3.32 +
    3.33  lemma nat_add_distrib:
    3.34       "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
    3.35  apply (rule inj_int [THEN injD])
    3.36 -apply (simp (no_asm_simp) add: zadd_int [symmetric])
    3.37 +apply (simp add: zadd_int [symmetric])
    3.38  done
    3.39  
    3.40  lemma nat_diff_distrib:
    3.41       "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
    3.42  apply (rule inj_int [THEN injD])
    3.43 -apply (simp (no_asm_simp) add: zdiff_int [symmetric] nat_le_eq_zle)
    3.44 +apply (simp add: zdiff_int [symmetric] nat_le_eq_zle)
    3.45  done
    3.46  
    3.47  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
    3.48  apply (case_tac "0 \<le> z'")
    3.49  apply (rule inj_int [THEN injD])
    3.50 -apply (simp (no_asm_simp) add: zmult_int [symmetric] int_0_le_mult_iff)
    3.51 +apply (simp add: zmult_int [symmetric] int_0_le_mult_iff)
    3.52  apply (simp add: zmult_le_0_iff)
    3.53  done
    3.54  
     4.1 --- a/src/HOL/Integ/IntDef.thy	Tue Dec 02 11:48:15 2003 +0100
     4.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Dec 03 10:49:34 2003 +0100
     4.3 @@ -3,13 +3,14 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1996  University of Cambridge
     4.6  
     4.7 -The integers as equivalence classes over nat*nat.
     4.8  *)
     4.9  
    4.10 +header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
    4.11 +
    4.12  theory IntDef = Equiv + NatArith:
    4.13  constdefs
    4.14 -  intrel      :: "((nat * nat) * (nat * nat)) set"
    4.15 -  "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
    4.16 +  intrel :: "((nat * nat) * (nat * nat)) set"
    4.17 +    "intrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    4.18  
    4.19  typedef (Integ)
    4.20    int = "UNIV//intrel"
    4.21 @@ -22,17 +23,13 @@
    4.22  instance int :: times ..
    4.23  instance int :: minus ..
    4.24  
    4.25 -defs
    4.26 -  zminus_def:
    4.27 -    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
    4.28 -
    4.29  constdefs
    4.30  
    4.31    int :: "nat => int"
    4.32    "int m == Abs_Integ(intrel `` {(m,0)})"
    4.33  
    4.34    neg   :: "int => bool"
    4.35 -  "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
    4.36 +  "neg(Z) == \<exists>x y. x<y & (x,y::nat):Rep_Integ(Z)"
    4.37  
    4.38    (*For simplifying equalities*)
    4.39    iszero :: "int => bool"
    4.40 @@ -40,12 +37,14 @@
    4.41    
    4.42  defs (overloaded)
    4.43    
    4.44 +  zminus_def:    "- Z == Abs_Integ(\<Union>(x,y) \<in> Rep_Integ(Z). intrel``{(y,x)})"
    4.45 +
    4.46    Zero_int_def:  "0 == int 0"
    4.47 -  One_int_def:  "1 == int 1"
    4.48 +  One_int_def:   "1 == int 1"
    4.49  
    4.50    zadd_def:
    4.51     "z + w == 
    4.52 -       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
    4.53 +       Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).   
    4.54  		 intrel``{(x1+x2, y1+y2)})"
    4.55  
    4.56    zdiff_def:  "z - (w::int) == z + (-w)"
    4.57 @@ -56,10 +55,10 @@
    4.58  
    4.59    zmult_def:
    4.60     "z * w == 
    4.61 -       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
    4.62 +       Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).   
    4.63  		 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
    4.64  
    4.65 -lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)"
    4.66 +lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in>  intrel) = (x1+y2 = x2+y1)"
    4.67  by (unfold intrel_def, blast)
    4.68  
    4.69  lemma equiv_intrel: "equiv UNIV intrel"
    4.70 @@ -171,7 +170,7 @@
    4.71  done
    4.72  
    4.73  (*For AC rewriting*)
    4.74 -lemma zadd_left_commute: "x + (y + z) = y + ((x + z)::int)"
    4.75 +lemma zadd_left_commute: "x + (y + z) = y + ((x + z)  ::int)"
    4.76    apply (rule mk_left_commute [of "op +"])
    4.77    apply (rule zadd_assoc)
    4.78    apply (rule zadd_commute)
    4.79 @@ -180,6 +179,8 @@
    4.80  (*Integer addition is an AC operator*)
    4.81  lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
    4.82  
    4.83 +lemmas zmult_ac = Ring_and_Field.mult_ac
    4.84 +
    4.85  lemma zadd_int: "(int m) + (int n) = int (m + n)"
    4.86  by (simp add: int_def zadd)
    4.87  
    4.88 @@ -278,16 +279,6 @@
    4.89  apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
    4.90  done
    4.91  
    4.92 -(*For AC rewriting*)
    4.93 -lemma zmult_left_commute: "x * (y * z) = y * ((x * z)::int)"
    4.94 -  apply (rule mk_left_commute [of "op *"])
    4.95 -  apply (rule zmult_assoc)
    4.96 -  apply (rule zmult_commute)
    4.97 -  done
    4.98 -
    4.99 -(*Integer multiplication is an AC operator*)
   4.100 -lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
   4.101 -
   4.102  lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
   4.103  apply (rule_tac z = z1 in eq_Abs_Integ)
   4.104  apply (rule_tac z = z2 in eq_Abs_Integ)
   4.105 @@ -340,7 +331,7 @@
   4.106  
   4.107  (*This lemma allows direct proofs of other <-properties*)
   4.108  lemma zless_iff_Suc_zadd: 
   4.109 -    "(w < z) = (EX n. z = w + int(Suc n))"
   4.110 +    "(w < z) = (\<exists>n. z = w + int(Suc n))"
   4.111  apply (unfold zless_def neg_def zdiff_def int_def)
   4.112  apply (rule_tac z = z in eq_Abs_Integ)
   4.113  apply (rule_tac z = w in eq_Abs_Integ, clarify)
   4.114 @@ -465,84 +456,21 @@
   4.115  apply (blast elim!: zless_asym)
   4.116  done
   4.117  
   4.118 -
   4.119 -(*** Subtraction laws ***)
   4.120 -
   4.121 -lemma zadd_zdiff_eq: "x + (y - z) = (x + y) - (z::int)"
   4.122 -by (simp add: zdiff_def zadd_ac)
   4.123 -
   4.124 -lemma zdiff_zadd_eq: "(x - y) + z = (x + z) - (y::int)"
   4.125 -by (simp add: zdiff_def zadd_ac)
   4.126 -
   4.127 -lemma zdiff_zdiff_eq: "(x - y) - z = x - (y + (z::int))"
   4.128 -by (simp add: zdiff_def zadd_ac)
   4.129 -
   4.130 -lemma zdiff_zdiff_eq2: "x - (y - z) = (x + z) - (y::int)"
   4.131 -by (simp add: zdiff_def zadd_ac)
   4.132 -
   4.133 -lemma zdiff_zless_eq: "(x-y < z) = (x < z + (y::int))"
   4.134 -apply (unfold zless_def zdiff_def)
   4.135 -apply (simp add: zadd_ac)
   4.136 -done
   4.137 -
   4.138 -lemma zless_zdiff_eq: "(x < z-y) = (x + (y::int) < z)"
   4.139 -apply (unfold zless_def zdiff_def)
   4.140 -apply (simp add: zadd_ac)
   4.141 -done
   4.142 -
   4.143 -lemma zdiff_zle_eq: "(x-y <= z) = (x <= z + (y::int))"
   4.144 -apply (unfold zle_def)
   4.145 -apply (simp add: zless_zdiff_eq)
   4.146 -done
   4.147 -
   4.148 -lemma zle_zdiff_eq: "(x <= z-y) = (x + (y::int) <= z)"
   4.149 -apply (unfold zle_def)
   4.150 -apply (simp add: zdiff_zless_eq)
   4.151 -done
   4.152 -
   4.153 -lemma zdiff_eq_eq: "(x-y = z) = (x = z + (y::int))"
   4.154 -by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
   4.155 -
   4.156 -lemma eq_zdiff_eq: "(x = z-y) = (x + (y::int) = z)"
   4.157 -by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
   4.158 -
   4.159 -(*This list of rewrites simplifies (in)equalities by bringing subtractions
   4.160 -  to the top and then moving negative terms to the other side.  
   4.161 -  Use with zadd_ac*)
   4.162 -lemmas zcompare_rls =
   4.163 -     zdiff_def [symmetric]
   4.164 -     zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 
   4.165 -     zdiff_zless_eq zless_zdiff_eq zdiff_zle_eq zle_zdiff_eq 
   4.166 -     zdiff_eq_eq eq_zdiff_eq
   4.167 -
   4.168 -
   4.169 -(** Cancellation laws **)
   4.170 -
   4.171  lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
   4.172  apply safe
   4.173  apply (drule_tac f = "%x. x + (-z) " in arg_cong)
   4.174  apply (simp add: Zero_int_def [symmetric] zadd_ac)
   4.175  done
   4.176  
   4.177 -lemma zadd_right_cancel [simp]: "!!z::int. (w' + z = w + z) = (w' = w)"
   4.178 -by (simp add: zadd_ac)
   4.179 -
   4.180 -
   4.181 -(** For the cancellation simproc.
   4.182 -    The idea is to cancel like terms on opposite sides by subtraction **)
   4.183 -
   4.184 -lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
   4.185 -by (simp add: zless_def)
   4.186 +instance int :: order
   4.187 +proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
   4.188  
   4.189 -lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
   4.190 -apply (drule zless_eqI)
   4.191 -apply (simp (no_asm_simp) add: zle_def)
   4.192 -done
   4.193 +instance int :: plus_ac0
   4.194 +proof qed (rule zadd_commute zadd_assoc zadd_0)+
   4.195  
   4.196 -lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
   4.197 -apply safe
   4.198 -apply (simp_all add: eq_zdiff_eq zdiff_eq_eq)
   4.199 -done
   4.200 +instance int :: linorder
   4.201 +proof qed (rule zle_linear)
   4.202 +
   4.203  
   4.204  ML
   4.205  {*
   4.206 @@ -578,6 +506,7 @@
   4.207  val zadd_assoc = thm "zadd_assoc";
   4.208  val zadd_left_commute = thm "zadd_left_commute";
   4.209  val zadd_ac = thms "zadd_ac";
   4.210 +val zmult_ac = thms "zmult_ac";
   4.211  val zadd_int = thm "zadd_int";
   4.212  val zadd_int_left = thm "zadd_int_left";
   4.213  val int_Suc = thm "int_Suc";
   4.214 @@ -597,8 +526,6 @@
   4.215  val zmult_zminus = thm "zmult_zminus";
   4.216  val zmult_commute = thm "zmult_commute";
   4.217  val zmult_assoc = thm "zmult_assoc";
   4.218 -val zmult_left_commute = thm "zmult_left_commute";
   4.219 -val zmult_ac = thms "zmult_ac";
   4.220  val zadd_zmult_distrib = thm "zadd_zmult_distrib";
   4.221  val zmult_zminus_right = thm "zmult_zminus_right";
   4.222  val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
   4.223 @@ -636,22 +563,15 @@
   4.224  val zle_trans = thm "zle_trans";
   4.225  val zle_anti_sym = thm "zle_anti_sym";
   4.226  val int_less_le = thm "int_less_le";
   4.227 -val zadd_zdiff_eq = thm "zadd_zdiff_eq";
   4.228 -val zdiff_zadd_eq = thm "zdiff_zadd_eq";
   4.229 -val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
   4.230 -val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
   4.231 -val zdiff_zless_eq = thm "zdiff_zless_eq";
   4.232 -val zless_zdiff_eq = thm "zless_zdiff_eq";
   4.233 -val zdiff_zle_eq = thm "zdiff_zle_eq";
   4.234 -val zle_zdiff_eq = thm "zle_zdiff_eq";
   4.235 -val zdiff_eq_eq = thm "zdiff_eq_eq";
   4.236 -val eq_zdiff_eq = thm "eq_zdiff_eq";
   4.237 -val zcompare_rls = thms "zcompare_rls";
   4.238  val zadd_left_cancel = thm "zadd_left_cancel";
   4.239 -val zadd_right_cancel = thm "zadd_right_cancel";
   4.240 -val zless_eqI = thm "zless_eqI";
   4.241 -val zle_eqI = thm "zle_eqI";
   4.242 -val zeq_eqI = thm "zeq_eqI";
   4.243 +
   4.244 +val diff_less_eq = thm"diff_less_eq";
   4.245 +val less_diff_eq = thm"less_diff_eq";
   4.246 +val eq_diff_eq = thm"eq_diff_eq";
   4.247 +val diff_eq_eq = thm"diff_eq_eq";
   4.248 +val diff_le_eq = thm"diff_le_eq";
   4.249 +val le_diff_eq = thm"le_diff_eq";
   4.250 +val compare_rls = thms "compare_rls";
   4.251  *}
   4.252  
   4.253  end
     5.1 --- a/src/HOL/Integ/IntDiv.thy	Tue Dec 02 11:48:15 2003 +0100
     5.2 +++ b/src/HOL/Integ/IntDiv.thy	Wed Dec 03 10:49:34 2003 +0100
     5.3 @@ -89,7 +89,7 @@
     5.4  
     5.5  
     5.6  
     5.7 -(*** Uniqueness and monotonicity of quotients and remainders ***)
     5.8 +subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
     5.9  
    5.10  lemma unique_quotient_lemma:
    5.11       "[| b*q' + r'  <= b*q + r;  0 <= r';  0 < b;  r < b |]  
    5.12 @@ -129,7 +129,9 @@
    5.13  done
    5.14  
    5.15  
    5.16 -(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
    5.17 +subsection{*Correctness of posDivAlg, the Algorithm for Non-Negative Dividends*}
    5.18 +
    5.19 +text{*And positive divisors*}
    5.20  
    5.21  lemma adjust_eq [simp]:
    5.22       "adjust b (q,r) = 
    5.23 @@ -160,7 +162,9 @@
    5.24  done
    5.25  
    5.26  
    5.27 -(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
    5.28 +subsection{*Correctness of negDivAlg, the Algorithm for Negative Dividends*}
    5.29 +
    5.30 +text{*And positive divisors*}
    5.31  
    5.32  declare negDivAlg.simps [simp del]
    5.33  
    5.34 @@ -186,7 +190,7 @@
    5.35  done
    5.36  
    5.37  
    5.38 -(*** Existence shown by proving the division algorithm to be correct ***)
    5.39 +subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
    5.40  
    5.41  (*the case a=0*)
    5.42  lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))"
    5.43 @@ -211,8 +215,8 @@
    5.44  (** Arbitrary definitions for division by zero.  Useful to simplify 
    5.45      certain equations **)
    5.46  
    5.47 -lemma DIVISION_BY_ZERO: "a div (0::int) = 0 & a mod (0::int) = a"
    5.48 -by (simp add: div_def mod_def divAlg_def posDivAlg.simps)  (*NOT for adding to default simpset*)
    5.49 +lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
    5.50 +by (simp add: div_def mod_def divAlg_def posDivAlg.simps)  
    5.51  
    5.52  (** Basic laws about division and remainder **)
    5.53  
    5.54 @@ -311,7 +315,7 @@
    5.55         auto)
    5.56  done
    5.57  
    5.58 -(*** div, mod and unary minus ***)
    5.59 +subsection{*div, mod and unary minus*}
    5.60  
    5.61  lemma zminus1_lemma:
    5.62       "quorem((a,b),(q,r))  
    5.63 @@ -349,7 +353,7 @@
    5.64  by (simp add: zmod_zminus1_eq_if zmod_zminus2)
    5.65  
    5.66  
    5.67 -(*** division of a number by itself ***)
    5.68 +subsection{*Division of a Number by Itself*}
    5.69  
    5.70  lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
    5.71  apply (subgoal_tac "0 < a*q")
    5.72 @@ -385,7 +389,7 @@
    5.73  done
    5.74  
    5.75  
    5.76 -(*** Computation of division and remainder ***)
    5.77 +subsection{*Computation of Division and Remainder*}
    5.78  
    5.79  lemma zdiv_zero [simp]: "(0::int) div b = 0"
    5.80  by (simp add: div_def divAlg_def)
    5.81 @@ -486,7 +490,7 @@
    5.82  declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp]
    5.83  
    5.84  
    5.85 -(*** Monotonicity in the first argument (divisor) ***)
    5.86 +subsection{*Monotonicity in the First Argument (Dividend)*}
    5.87  
    5.88  lemma zdiv_mono1: "[| a <= a';  0 < (b::int) |] ==> a div b <= a' div b"
    5.89  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
    5.90 @@ -507,7 +511,7 @@
    5.91  done
    5.92  
    5.93  
    5.94 -(*** Monotonicity in the second argument (dividend) ***)
    5.95 +subsection{*Monotonicity in the Second Argument (Divisor)*}
    5.96  
    5.97  lemma q_pos_lemma:
    5.98       "[| 0 <= b'*q' + r'; r' < b';  0 < b' |] ==> 0 <= (q'::int)"
    5.99 @@ -574,7 +578,7 @@
   5.100  done
   5.101  
   5.102  
   5.103 -(*** More algebraic laws for div and mod ***)
   5.104 +subsection{*More Algebraic Laws for div and mod*}
   5.105  
   5.106  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   5.107  
   5.108 @@ -686,7 +690,7 @@
   5.109  done
   5.110  
   5.111  
   5.112 -(*** proving  a div (b*c) = (a div b) div c ***)
   5.113 +subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
   5.114  
   5.115  (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   5.116    7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   5.117 @@ -700,7 +704,7 @@
   5.118  apply (rule order_le_less_trans)
   5.119  apply (erule_tac [2] zmult_zless_mono1)
   5.120  apply (rule zmult_zle_mono2_neg)
   5.121 -apply (auto simp add: zcompare_rls zadd_commute [of 1]
   5.122 +apply (auto simp add: compare_rls zadd_commute [of 1]
   5.123                        add1_zle_eq pos_mod_bound)
   5.124  done
   5.125  
   5.126 @@ -722,13 +726,13 @@
   5.127  apply (rule order_less_le_trans)
   5.128  apply (erule zmult_zless_mono1)
   5.129  apply (rule_tac [2] zmult_zle_mono2)
   5.130 -apply (auto simp add: zcompare_rls zadd_commute [of 1]
   5.131 +apply (auto simp add: compare_rls zadd_commute [of 1]
   5.132                        add1_zle_eq pos_mod_bound)
   5.133  done
   5.134  
   5.135  lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b ~= 0;  0 < c |]  
   5.136        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   5.137 -by (auto simp add: zmult_ac quorem_def linorder_neq_iff
   5.138 +by (auto simp add: mult_ac quorem_def linorder_neq_iff
   5.139                     int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
   5.140                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
   5.141  
   5.142 @@ -744,7 +748,7 @@
   5.143  done
   5.144  
   5.145  
   5.146 -(*** Cancellation of common factors in div ***)
   5.147 +subsection{*Cancellation of Common Factors in div*}
   5.148  
   5.149  lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
   5.150  by (subst zdiv_zmult2_eq, auto)
   5.151 @@ -766,7 +770,7 @@
   5.152  
   5.153  
   5.154  
   5.155 -(*** Distribution of factors over mod ***)
   5.156 +subsection{*Distribution of Factors over mod*}
   5.157  
   5.158  lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
   5.159  by (subst zmod_zmult2_eq, auto)
   5.160 @@ -788,7 +792,7 @@
   5.161  done
   5.162  
   5.163  
   5.164 -subsection {*splitting rules for div and mod*}
   5.165 +subsection {*Splitting Rules for div and mod*}
   5.166  
   5.167  text{*The proofs of the two lemmas below are essentially identical*}
   5.168  
   5.169 @@ -853,7 +857,7 @@
   5.170  declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
   5.171  
   5.172  
   5.173 -subsection{*Speeding up the division algorithm with shifting*}
   5.174 +subsection{*Speeding up the Division Algorithm with Shifting*}
   5.175  
   5.176  (** computing div by shifting **)
   5.177  
   5.178 @@ -986,7 +990,7 @@
   5.179  by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
   5.180  
   5.181  
   5.182 -subsection {* Divides relation *}
   5.183 +subsection {* The Divides Relation *}
   5.184  
   5.185  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   5.186  by(simp add:dvd_def zmod_eq_0_iff)
   5.187 @@ -1046,7 +1050,7 @@
   5.188  
   5.189  lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   5.190    apply (unfold dvd_def)
   5.191 -  apply (blast intro: zmult_left_commute)
   5.192 +  apply (blast intro: mult_left_commute)
   5.193    done
   5.194  
   5.195  lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
   5.196 @@ -1077,7 +1081,7 @@
   5.197  lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   5.198    apply (unfold dvd_def, clarify)
   5.199    apply (rule_tac x = "k * ka" in exI)
   5.200 -  apply (simp add: zmult_ac)
   5.201 +  apply (simp add: mult_ac)
   5.202    done
   5.203  
   5.204  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
     6.1 --- a/src/HOL/Integ/Presburger.thy	Tue Dec 02 11:48:15 2003 +0100
     6.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Dec 03 10:49:34 2003 +0100
     6.3 @@ -395,7 +395,7 @@
     6.4    apply(clarsimp)
     6.5    apply(rename_tac n m)
     6.6    apply(rule_tac x = "m - n*k" in exI)
     6.7 -  apply(simp add:int_distrib zmult_ac)
     6.8 +  apply(simp add:int_distrib mult_ac)
     6.9    done
    6.10  
    6.11  lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
    6.12 @@ -405,11 +405,11 @@
    6.13    apply(clarsimp)
    6.14    apply(rename_tac n m)
    6.15    apply(erule_tac x = "m - n*k" in allE)
    6.16 -  apply(simp add:int_distrib zmult_ac)
    6.17 +  apply(simp add:int_distrib mult_ac)
    6.18    apply(clarsimp)
    6.19    apply(rename_tac n m)
    6.20    apply(erule_tac x = "m + n*k" in allE)
    6.21 -  apply(simp add:int_distrib zmult_ac)
    6.22 +  apply(simp add:int_distrib mult_ac)
    6.23    done
    6.24  
    6.25  (*=============================================================================*)
    6.26 @@ -462,7 +462,7 @@
    6.27  apply(clarsimp)
    6.28  apply(rename_tac n m)
    6.29  apply(rule_tac x = "m + n*k" in exI)
    6.30 -apply(simp add:int_distrib zmult_ac)
    6.31 +apply(simp add:int_distrib mult_ac)
    6.32  done
    6.33  
    6.34  
    6.35 @@ -473,11 +473,11 @@
    6.36  apply(clarsimp)
    6.37  apply(rename_tac n m)
    6.38  apply(erule_tac x = "m + n*k" in allE)
    6.39 -apply(simp add:int_distrib zmult_ac)
    6.40 +apply(simp add:int_distrib mult_ac)
    6.41  apply(clarsimp)
    6.42  apply(rename_tac n m)
    6.43  apply(erule_tac x = "m - n*k" in allE)
    6.44 -apply(simp add:int_distrib zmult_ac)
    6.45 +apply(simp add:int_distrib mult_ac)
    6.46  done
    6.47  
    6.48  
    6.49 @@ -626,7 +626,7 @@
    6.50    assume ?LHS
    6.51    then obtain x where P: "P x" ..
    6.52    have "x mod d = x - (x div d)*d"
    6.53 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
    6.54 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
    6.55    hence Pmod: "P x = P(x mod d)" using modd by simp
    6.56    show ?RHS
    6.57    proof (cases)
    6.58 @@ -661,7 +661,7 @@
    6.59    assume ?LHS
    6.60    then obtain x where P: "P x" ..
    6.61    have "x mod d = x + (-(x div d))*d"
    6.62 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
    6.63 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
    6.64    hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
    6.65    show ?RHS
    6.66    proof (cases)
    6.67 @@ -702,7 +702,7 @@
    6.68      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
    6.69      also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
    6.70        using minus[THEN spec, of "x - i * d"]
    6.71 -      by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
    6.72 +      by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
    6.73      ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
    6.74    qed
    6.75  qed
    6.76 @@ -864,12 +864,12 @@
    6.77      apply(drule_tac f = "op * k" in arg_cong)
    6.78      apply(simp only:int_distrib)
    6.79      apply(rule_tac x = "d" in exI)
    6.80 -    apply(simp only:zmult_ac)
    6.81 +    apply(simp only:mult_ac)
    6.82      done
    6.83  next
    6.84    assume ?Q
    6.85    then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
    6.86 -  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
    6.87 +  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
    6.88    hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
    6.89    hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
    6.90    thus ?P by(simp add:dvd_def)
    6.91 @@ -879,10 +879,10 @@
    6.92  shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
    6.93  proof
    6.94    assume P: ?P
    6.95 -  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
    6.96 +  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
    6.97  next
    6.98    assume ?Q
    6.99 -  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
   6.100 +  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
   6.101    with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
   6.102    thus ?P by(simp)
   6.103  qed
   6.104 @@ -896,7 +896,7 @@
   6.105      done
   6.106  next
   6.107    assume ?Q
   6.108 -  hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
   6.109 +  hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
   6.110    hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   6.111    thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   6.112  qed
   6.113 @@ -904,9 +904,9 @@
   6.114  lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
   6.115  proof -
   6.116    have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
   6.117 -  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
   6.118 +  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
   6.119    also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified])
   6.120 -  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
   6.121 +  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
   6.122    finally show ?thesis .
   6.123  qed
   6.124  
   6.125 @@ -963,7 +963,7 @@
   6.126    apply (simp add: linorder_not_le)
   6.127    apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
   6.128    apply assumption
   6.129 -  apply (simp add: zmult_ac)
   6.130 +  apply (simp add: mult_ac)
   6.131    done
   6.132  
   6.133  theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
     7.1 --- a/src/HOL/Integ/int_arith1.ML	Tue Dec 02 11:48:15 2003 +0100
     7.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed Dec 03 10:49:34 2003 +0100
     7.3 @@ -5,6 +5,10 @@
     7.4  Simprocs and decision procedure for linear arithmetic.
     7.5  *)
     7.6  
     7.7 +val zadd_ac = thms "Ring_and_Field.add_ac";
     7.8 +val zmult_ac = thms "Ring_and_Field.mult_ac";
     7.9 +
    7.10 +
    7.11  Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
    7.12  
    7.13  (*** Simprocs for numeric literals ***)
    7.14 @@ -12,15 +16,15 @@
    7.15  (** Combining of literal coefficients in sums of products **)
    7.16  
    7.17  Goal "(x < y) = (x-y < (0::int))";
    7.18 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.19 +by (simp_tac (simpset() addsimps compare_rls) 1);
    7.20  qed "zless_iff_zdiff_zless_0";
    7.21  
    7.22  Goal "(x = y) = (x-y = (0::int))";
    7.23 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.24 +by (simp_tac (simpset() addsimps compare_rls) 1);
    7.25  qed "eq_iff_zdiff_eq_0";
    7.26  
    7.27  Goal "(x <= y) = (x-y <= (0::int))";
    7.28 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.29 +by (simp_tac (simpset() addsimps compare_rls) 1);
    7.30  qed "zle_iff_zdiff_zle_0";
    7.31  
    7.32  
     8.1 --- a/src/HOL/NumberTheory/Gauss.thy	Tue Dec 02 11:48:15 2003 +0100
     8.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Wed Dec 03 10:49:34 2003 +0100
     8.3 @@ -479,7 +479,7 @@
     8.4      then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
     8.5          (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
     8.6        apply (rule zcong_trans)
     8.7 -      by (simp add: a zmult_commute zmult_left_commute)
     8.8 +      by (simp add: a mult_commute mult_left_commute)
     8.9      then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
    8.10          a^(card A)](mod p)";
    8.11        apply (rule zcong_trans)
     9.1 --- a/src/HOL/NumberTheory/IntFact.thy	Tue Dec 02 11:48:15 2003 +0100
     9.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Wed Dec 03 10:49:34 2003 +0100
     9.3 @@ -39,7 +39,7 @@
     9.4  
     9.5  lemma setprod_insert [simp]:
     9.6      "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
     9.7 -  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
     9.8 +  by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
     9.9  
    9.10  text {*
    9.11    \medskip @{term d22set} --- recursively defined set including all
    10.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Dec 02 11:48:15 2003 +0100
    10.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed Dec 03 10:49:34 2003 +0100
    10.3 @@ -305,7 +305,7 @@
    10.4     apply (rule_tac [!] zrelprime_zdvd_zmult)
    10.5       apply (simp_all add: zdiff_zmult_distrib)
    10.6    apply (subgoal_tac "m dvd (-(a * k - b * k))")
    10.7 -   apply (simp add: zminus_zdiff_eq)
    10.8 +   apply simp
    10.9    apply (subst zdvd_zminus_iff, assumption)
   10.10    done
   10.11  
   10.12 @@ -380,7 +380,7 @@
   10.13    apply (unfold zcong_def dvd_def)
   10.14    apply (rule_tac x = "a mod m" in exI, auto)
   10.15    apply (rule_tac x = "-(a div m)" in exI)
   10.16 -  apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
   10.17 +  apply (simp add: diff_eq_eq eq_diff_eq add_commute)
   10.18    done
   10.19  
   10.20  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
   10.21 @@ -395,7 +395,7 @@
   10.22  
   10.23  lemma zcong_zmod_aux:
   10.24       "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   10.25 -  by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
   10.26 +  by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac)
   10.27  
   10.28  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   10.29    apply (unfold zcong_def)
   10.30 @@ -505,7 +505,7 @@
   10.31      ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
   10.32    apply (rule trans)
   10.33     apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
   10.34 -  apply (simp add: eq_zdiff_eq zmult_commute)
   10.35 +  apply (simp add: eq_diff_eq mult_commute)
   10.36    done
   10.37  
   10.38  lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
    11.1 --- a/src/HOL/NumberTheory/ROOT.ML	Tue Dec 02 11:48:15 2003 +0100
    11.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Wed Dec 03 10:49:34 2003 +0100
    11.3 @@ -19,7 +19,6 @@
    11.4  use_thy "Fib";
    11.5  use_thy "Factorization";
    11.6  use_thy "Chinese";
    11.7 -use_thy "EulerFermat";
    11.8  use_thy "WilsonRuss";
    11.9  use_thy "WilsonBij";
   11.10  use_thy "Quadratic_Reciprocity";
    12.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Tue Dec 02 11:48:15 2003 +0100
    12.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Wed Dec 03 10:49:34 2003 +0100
    12.3 @@ -75,9 +75,9 @@
    12.4  lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    12.5    -- {* same as @{text WilsonRuss} *}
    12.6    apply (unfold zcong_def)
    12.7 -  apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
    12.8 +  apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    12.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   12.10 -   apply (simp add: zmult_commute zminus_zdiff_eq)
   12.11 +   apply (simp add: mult_commute)
   12.12    apply (subst zdvd_zminus_iff)
   12.13    apply (subst zdvd_reduce)
   12.14    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
    13.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Dec 02 11:48:15 2003 +0100
    13.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Wed Dec 03 10:49:34 2003 +0100
    13.3 @@ -86,9 +86,9 @@
    13.4  
    13.5  lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    13.6    apply (unfold zcong_def)
    13.7 -  apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
    13.8 +  apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    13.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   13.10 -   apply (simp add: zmult_commute zminus_zdiff_eq)
   13.11 +   apply (simp add: mult_commute)
   13.12    apply (subst zdvd_zminus_iff)
   13.13    apply (subst zdvd_reduce)
   13.14    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
    14.1 --- a/src/HOL/Presburger.thy	Tue Dec 02 11:48:15 2003 +0100
    14.2 +++ b/src/HOL/Presburger.thy	Wed Dec 03 10:49:34 2003 +0100
    14.3 @@ -395,7 +395,7 @@
    14.4    apply(clarsimp)
    14.5    apply(rename_tac n m)
    14.6    apply(rule_tac x = "m - n*k" in exI)
    14.7 -  apply(simp add:int_distrib zmult_ac)
    14.8 +  apply(simp add:int_distrib mult_ac)
    14.9    done
   14.10  
   14.11  lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
   14.12 @@ -405,11 +405,11 @@
   14.13    apply(clarsimp)
   14.14    apply(rename_tac n m)
   14.15    apply(erule_tac x = "m - n*k" in allE)
   14.16 -  apply(simp add:int_distrib zmult_ac)
   14.17 +  apply(simp add:int_distrib mult_ac)
   14.18    apply(clarsimp)
   14.19    apply(rename_tac n m)
   14.20    apply(erule_tac x = "m + n*k" in allE)
   14.21 -  apply(simp add:int_distrib zmult_ac)
   14.22 +  apply(simp add:int_distrib mult_ac)
   14.23    done
   14.24  
   14.25  (*=============================================================================*)
   14.26 @@ -462,7 +462,7 @@
   14.27  apply(clarsimp)
   14.28  apply(rename_tac n m)
   14.29  apply(rule_tac x = "m + n*k" in exI)
   14.30 -apply(simp add:int_distrib zmult_ac)
   14.31 +apply(simp add:int_distrib mult_ac)
   14.32  done
   14.33  
   14.34  
   14.35 @@ -473,11 +473,11 @@
   14.36  apply(clarsimp)
   14.37  apply(rename_tac n m)
   14.38  apply(erule_tac x = "m + n*k" in allE)
   14.39 -apply(simp add:int_distrib zmult_ac)
   14.40 +apply(simp add:int_distrib mult_ac)
   14.41  apply(clarsimp)
   14.42  apply(rename_tac n m)
   14.43  apply(erule_tac x = "m - n*k" in allE)
   14.44 -apply(simp add:int_distrib zmult_ac)
   14.45 +apply(simp add:int_distrib mult_ac)
   14.46  done
   14.47  
   14.48  
   14.49 @@ -626,7 +626,7 @@
   14.50    assume ?LHS
   14.51    then obtain x where P: "P x" ..
   14.52    have "x mod d = x - (x div d)*d"
   14.53 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
   14.54 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   14.55    hence Pmod: "P x = P(x mod d)" using modd by simp
   14.56    show ?RHS
   14.57    proof (cases)
   14.58 @@ -661,7 +661,7 @@
   14.59    assume ?LHS
   14.60    then obtain x where P: "P x" ..
   14.61    have "x mod d = x + (-(x div d))*d"
   14.62 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
   14.63 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   14.64    hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
   14.65    show ?RHS
   14.66    proof (cases)
   14.67 @@ -702,7 +702,7 @@
   14.68      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   14.69      also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
   14.70        using minus[THEN spec, of "x - i * d"]
   14.71 -      by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
   14.72 +      by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
   14.73      ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
   14.74    qed
   14.75  qed
   14.76 @@ -864,12 +864,12 @@
   14.77      apply(drule_tac f = "op * k" in arg_cong)
   14.78      apply(simp only:int_distrib)
   14.79      apply(rule_tac x = "d" in exI)
   14.80 -    apply(simp only:zmult_ac)
   14.81 +    apply(simp only:mult_ac)
   14.82      done
   14.83  next
   14.84    assume ?Q
   14.85    then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
   14.86 -  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
   14.87 +  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
   14.88    hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   14.89    hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   14.90    thus ?P by(simp add:dvd_def)
   14.91 @@ -879,10 +879,10 @@
   14.92  shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
   14.93  proof
   14.94    assume P: ?P
   14.95 -  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
   14.96 +  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
   14.97  next
   14.98    assume ?Q
   14.99 -  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
  14.100 +  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
  14.101    with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
  14.102    thus ?P by(simp)
  14.103  qed
  14.104 @@ -896,7 +896,7 @@
  14.105      done
  14.106  next
  14.107    assume ?Q
  14.108 -  hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
  14.109 +  hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
  14.110    hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
  14.111    thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
  14.112  qed
  14.113 @@ -904,9 +904,9 @@
  14.114  lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
  14.115  proof -
  14.116    have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
  14.117 -  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
  14.118 +  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
  14.119    also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified])
  14.120 -  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
  14.121 +  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
  14.122    finally show ?thesis .
  14.123  qed
  14.124  
  14.125 @@ -963,7 +963,7 @@
  14.126    apply (simp add: linorder_not_le)
  14.127    apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
  14.128    apply assumption
  14.129 -  apply (simp add: zmult_ac)
  14.130 +  apply (simp add: mult_ac)
  14.131    done
  14.132  
  14.133  theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
    15.1 --- a/src/HOL/Real/RealOrd.thy	Tue Dec 02 11:48:15 2003 +0100
    15.2 +++ b/src/HOL/Real/RealOrd.thy	Wed Dec 03 10:49:34 2003 +0100
    15.3 @@ -1027,13 +1027,6 @@
    15.4  val real_minus_divide_eq = thm"real_minus_divide_eq";
    15.5  val real_divide_minus_eq = thm"real_divide_minus_eq";
    15.6  val real_add_divide_distrib = thm"real_add_divide_distrib";
    15.7 -
    15.8 -val diff_less_eq = thm"diff_less_eq";
    15.9 -val less_diff_eq = thm"less_diff_eq";
   15.10 -val diff_eq_eq = thm"diff_eq_eq";
   15.11 -val diff_le_eq = thm"diff_le_eq";
   15.12 -val le_diff_eq = thm"le_diff_eq";
   15.13 -val compare_rls = thms "compare_rls";
   15.14  *}
   15.15  
   15.16  end