moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
authorhaftmann
Fri Jul 18 18:25:53 2008 +0200 (2008-07-18)
changeset 2765116a26996c30e
parent 27650 7a4baad05495
child 27652 818666de6c24
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
NEWS
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Complex/ex/Sqrt_Script.thy
src/HOL/Divides.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/Import/HOL/divides.imp
src/HOL/IntDiv.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Primes.thy
src/HOL/NSA/StarDef.thy
src/HOL/NatBin.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Presburger.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Word/BinBoolList.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/ex/coopertac.ML
src/HOL/int_factor_simprocs.ML
src/HOL/nat_simprocs.ML
     1.1 --- a/NEWS	Fri Jul 18 17:09:48 2008 +0200
     1.2 +++ b/NEWS	Fri Jul 18 18:25:53 2008 +0200
     1.3 @@ -19,24 +19,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Command 'instance': attached definitions now longer accepted.
     1.8 +* Command 'instance': attached definitions no longer accepted.
     1.9  INCOMPATIBILITY, use proper 'instantiation' target.
    1.10  
    1.11  * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
    1.12  
    1.13 -* New ML antiquotation @{code}: takes constant as argument, generates
    1.14 -corresponding code in background and inserts name of the corresponding
    1.15 -resulting ML value/function/datatype constructor binding in place.
    1.16 -All occurrences of @{code} with a single ML block are generated
    1.17 -simultaneously.  Provides a generic and safe interface for
    1.18 -instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
    1.19 -example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
    1.20 -application.  In future you ought refrain from ad-hoc compiling
    1.21 -generated SML code on the ML toplevel.  Note that (for technical
    1.22 -reasons) @{code} cannot refer to constants for which user-defined
    1.23 -serializations are set.  Refer to the corresponding ML counterpart
    1.24 -directly in that cases.
    1.25 -
    1.26  
    1.27  *** Document preparation ***
    1.28  
    1.29 @@ -47,6 +34,19 @@
    1.30  
    1.31  *** HOL ***
    1.32  
    1.33 +* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
    1.34 +to separate class dvd in Ring_and_Field;  a couple of lemmas on dvd has been
    1.35 +generalized to class comm_semiring_1.  Likewise a bunch of lemmas from Divides
    1.36 +has been generalized from nat to class semiring_div.  INCOMPATIBILITY.
    1.37 +This involves the following theorem renames resulting from duplicate elimination:
    1.38 +
    1.39 +    dvd_def_mod ~>          dvd_eq_mod_eq_0
    1.40 +    zero_dvd_iff ~>         dvd_0_left_iff
    1.41 +    DIVISION_BY_ZERO_DIV ~> div_by_0
    1.42 +    DIVISION_BY_ZERO_MOD ~> mod_by_0
    1.43 +    mult_div ~>             div_mult_self2_is_id
    1.44 +    mult_mod ~>             mod_mult_self2_is_0
    1.45 +
    1.46  * HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
    1.47  zlcm (for int); carried together from various gcd/lcm developements in
    1.48  the HOL Distribution.  zgcd and zlcm replace former igcd and ilcm;
    1.49 @@ -63,6 +63,19 @@
    1.50  
    1.51  * HOL/Real/Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
    1.52  
    1.53 +* New ML antiquotation @{code}: takes constant as argument, generates
    1.54 +corresponding code in background and inserts name of the corresponding
    1.55 +resulting ML value/function/datatype constructor binding in place.
    1.56 +All occurrences of @{code} with a single ML block are generated
    1.57 +simultaneously.  Provides a generic and safe interface for
    1.58 +instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
    1.59 +example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
    1.60 +application.  In future you ought refrain from ad-hoc compiling
    1.61 +generated SML code on the ML toplevel.  Note that (for technical
    1.62 +reasons) @{code} cannot refer to constants for which user-defined
    1.63 +serializations are set.  Refer to the corresponding ML counterpart
    1.64 +directly in that cases.
    1.65 +
    1.66  * Integrated image HOL-Complex with HOL.  Entry points Main.thy and
    1.67  Complex_Main.thy remain as they are.
    1.68  
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Jul 18 17:09:48 2008 +0200
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Jul 18 18:25:53 2008 +0200
     2.3 @@ -49,8 +49,7 @@
     2.4  apply (erule disjE)
     2.5  apply (rule disjI1)
     2.6  apply (rule_tac [2] disjI2)
     2.7 -apply (erule_tac n = m in dvdE)
     2.8 -apply (erule_tac [2] n = n in dvdE, auto)
     2.9 +apply (auto elim!: dvdE)
    2.10  done
    2.11  
    2.12  
    2.13 @@ -202,7 +201,7 @@
    2.14  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
    2.15  apply (drule less_imp_le [of a])
    2.16  apply (drule le_imp_power_dvd)
    2.17 -apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
    2.18 +apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
    2.19  apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
    2.20  done
    2.21  
     3.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Jul 18 17:09:48 2008 +0200
     3.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Jul 18 18:25:53 2008 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  subsection {* Ring axioms *}
     3.6  
     3.7 -class ring = zero + one + plus + minus + uminus + times + inverse + power + Divides.dvd +
     3.8 +class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
     3.9    assumes a_assoc:      "(a + b) + c = a + (b + c)"
    3.10    and l_zero:           "0 + a = a"
    3.11    and l_neg:            "(-a) + a = 0"
     4.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 18 17:09:48 2008 +0200
     4.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 18 18:25:53 2008 +0200
     4.3 @@ -140,7 +140,7 @@
     4.4  
     4.5  end
     4.6  
     4.7 -instance up :: ("{times, comm_monoid_add}") Divides.dvd ..
     4.8 +instance up :: ("{times, comm_monoid_add}") Ring_and_Field.dvd ..
     4.9  
    4.10  instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
    4.11  begin
     5.1 --- a/src/HOL/Complex/ex/Sqrt_Script.thy	Fri Jul 18 17:09:48 2008 +0200
     5.2 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Fri Jul 18 18:25:53 2008 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  lemma prime_dvd_other_side:
     5.5      "n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
     5.6    apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
     5.7 -  apply (rule_tac j = "k * k" in dvd_mult_left, simp)
     5.8 +  apply auto
     5.9    done
    5.10  
    5.11  lemma reduction: "prime p \<Longrightarrow>
     6.1 --- a/src/HOL/Divides.thy	Fri Jul 18 17:09:48 2008 +0200
     6.2 +++ b/src/HOL/Divides.thy	Fri Jul 18 18:25:53 2008 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4      Copyright   1999  University of Cambridge
     6.5  *)
     6.6  
     6.7 -header {* The division operators div, mod and the divides relation dvd *}
     6.8 +header {* The division operators div and mod *}
     6.9  
    6.10  theory Divides
    6.11  imports Nat Power Product_Type
    6.12 @@ -13,71 +13,22 @@
    6.13  
    6.14  subsection {* Syntactic division operations *}
    6.15  
    6.16 -class dvd = times
    6.17 -begin
    6.18 -
    6.19 -definition
    6.20 -  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
    6.21 -where
    6.22 -  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
    6.23 -
    6.24 -end
    6.25 -
    6.26 -class div = times +
    6.27 +class div = dvd +
    6.28    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
    6.29 -  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
    6.30 +    and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
    6.31  
    6.32  
    6.33 -subsection {* Abstract divisibility in commutative semirings. *}
    6.34 +subsection {* Abstract division in commutative semirings. *}
    6.35  
    6.36 -class semiring_div = comm_semiring_1_cancel + dvd + div + 
    6.37 +class semiring_div = comm_semiring_1_cancel + div + 
    6.38    assumes mod_div_equality: "a div b * b + a mod b = a"
    6.39 -    and div_by_0: "a div 0 = 0"
    6.40 -    and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    6.41 +    and div_by_0 [simp]: "a div 0 = 0"
    6.42 +    and div_0 [simp]: "0 div a = 0"
    6.43 +    and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    6.44  begin
    6.45  
    6.46  text {* @{const div} and @{const mod} *}
    6.47  
    6.48 -lemma div_by_1: "a div 1 = a"
    6.49 -  using mult_div [of 1 a] zero_neq_one by simp
    6.50 -
    6.51 -lemma mod_by_1: "a mod 1 = 0"
    6.52 -proof -
    6.53 -  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
    6.54 -  then have "a + a mod 1 = a + 0" by simp
    6.55 -  then show ?thesis by (rule add_left_imp_eq)
    6.56 -qed
    6.57 -
    6.58 -lemma mod_by_0: "a mod 0 = a"
    6.59 -  using mod_div_equality [of a zero] by simp
    6.60 -
    6.61 -lemma mult_mod: "a * b mod b = 0"
    6.62 -proof (cases "b = 0")
    6.63 -  case True then show ?thesis by (simp add: mod_by_0)
    6.64 -next
    6.65 -  case False with mult_div have abb: "a * b div b = a" .
    6.66 -  from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
    6.67 -  with abb have "a * b + a * b mod b = a * b + 0" by simp
    6.68 -  then show ?thesis by (rule add_left_imp_eq)
    6.69 -qed
    6.70 -
    6.71 -lemma mod_self: "a mod a = 0"
    6.72 -  using mult_mod [of one] by simp
    6.73 -
    6.74 -lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
    6.75 -  using mult_div [of _ one] by simp
    6.76 -
    6.77 -lemma div_0: "0 div a = 0"
    6.78 -proof (cases "a = 0")
    6.79 -  case True then show ?thesis by (simp add: div_by_0)
    6.80 -next
    6.81 -  case False with mult_div have "0 * a div a = 0" .
    6.82 -  then show ?thesis by simp
    6.83 -qed
    6.84 -
    6.85 -lemma mod_0: "0 mod a = 0"
    6.86 -  using mod_div_equality [of zero a] div_0 by simp 
    6.87 -
    6.88  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    6.89    unfolding mult_commute [of b]
    6.90    by (rule mod_div_equality)
    6.91 @@ -88,15 +39,95 @@
    6.92  lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
    6.93    by (simp add: mod_div_equality2)
    6.94  
    6.95 -text {* The @{const dvd} relation *}
    6.96 +lemma mod_by_0 [simp]: "a mod 0 = a"
    6.97 +  using mod_div_equality [of a zero] by simp
    6.98 +
    6.99 +lemma mod_0 [simp]: "0 mod a = 0"
   6.100 +  using mod_div_equality [of zero a] div_0 by simp 
   6.101 +
   6.102 +lemma div_mult_self2 [simp]:
   6.103 +  assumes "b \<noteq> 0"
   6.104 +  shows "(a + b * c) div b = c + a div b"
   6.105 +  using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
   6.106  
   6.107 -lemma dvdI [intro?]: "a = b * c \<Longrightarrow> b dvd a"
   6.108 -  unfolding dvd_def ..
   6.109 +lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
   6.110 +proof (cases "b = 0")
   6.111 +  case True then show ?thesis by simp
   6.112 +next
   6.113 +  case False
   6.114 +  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
   6.115 +    by (simp add: mod_div_equality)
   6.116 +  also from False div_mult_self1 [of b a c] have
   6.117 +    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
   6.118 +      by (simp add: left_distrib add_ac)
   6.119 +  finally have "a = a div b * b + (a + c * b) mod b"
   6.120 +    by (simp add: add_commute [of a] add_assoc left_distrib)
   6.121 +  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   6.122 +    by (simp add: mod_div_equality)
   6.123 +  then show ?thesis by simp
   6.124 +qed
   6.125 +
   6.126 +lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
   6.127 +  by (simp add: mult_commute [of b])
   6.128 +
   6.129 +lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
   6.130 +  using div_mult_self2 [of b 0 a] by simp
   6.131 +
   6.132 +lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
   6.133 +  using div_mult_self1 [of b 0 a] by simp
   6.134 +
   6.135 +lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
   6.136 +  using mod_mult_self2 [of 0 b a] by simp
   6.137 +
   6.138 +lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
   6.139 +  using mod_mult_self1 [of 0 a b] by simp
   6.140  
   6.141 -lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>c. a = b * c \<Longrightarrow> P) \<Longrightarrow> P"
   6.142 -  unfolding dvd_def by blast 
   6.143 +lemma div_by_1 [simp]: "a div 1 = a"
   6.144 +  using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
   6.145 +
   6.146 +lemma mod_by_1 [simp]: "a mod 1 = 0"
   6.147 +proof -
   6.148 +  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
   6.149 +  then have "a + a mod 1 = a + 0" by simp
   6.150 +  then show ?thesis by (rule add_left_imp_eq)
   6.151 +qed
   6.152 +
   6.153 +lemma mod_self [simp]: "a mod a = 0"
   6.154 +  using mod_mult_self2_is_0 [of 1] by simp
   6.155 +
   6.156 +lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
   6.157 +  using div_mult_self2_is_id [of _ 1] by simp
   6.158 +
   6.159 +lemma div_add_self1:
   6.160 +  assumes "b \<noteq> 0"
   6.161 +  shows "(b + a) div b = a div b + 1"
   6.162 +  using assms div_mult_self1 [of b a 1] by (simp add: add_commute)
   6.163  
   6.164 -lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
   6.165 +lemma div_add_self2:
   6.166 +  assumes "b \<noteq> 0"
   6.167 +  shows "(a + b) div b = a div b + 1"
   6.168 +  using assms div_add_self1 [of b a] by (simp add: add_commute)
   6.169 +
   6.170 +lemma mod_add_self1:
   6.171 +  "(b + a) mod b = a mod b"
   6.172 +  using mod_mult_self1 [of a 1 b] by (simp add: add_commute)
   6.173 +
   6.174 +lemma mod_add_self2:
   6.175 +  "(a + b) mod b = a mod b"
   6.176 +  using mod_mult_self1 [of a 1 b] by simp
   6.177 +
   6.178 +lemma mod_div_decomp:
   6.179 +  fixes a b
   6.180 +  obtains q r where "q = a div b" and "r = a mod b"
   6.181 +    and "a = q * b + r"
   6.182 +proof -
   6.183 +  from mod_div_equality have "a = a div b * b + a mod b" by simp
   6.184 +  moreover have "a div b = a div b" ..
   6.185 +  moreover have "a mod b = a mod b" ..
   6.186 +  note that ultimately show thesis by blast
   6.187 +qed
   6.188 +
   6.189 +lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
   6.190  proof
   6.191    assume "b mod a = 0"
   6.192    with mod_div_equality [of b a] have "b div a * a = b" by simp
   6.193 @@ -109,59 +140,9 @@
   6.194    then obtain c where "b = a * c" ..
   6.195    then have "b mod a = a * c mod a" by simp
   6.196    then have "b mod a = c * a mod a" by (simp add: mult_commute)
   6.197 -  then show "b mod a = 0" by (simp add: mult_mod)
   6.198 -qed
   6.199 -
   6.200 -lemma dvd_refl: "a dvd a"
   6.201 -  unfolding dvd_def_mod mod_self ..
   6.202 -
   6.203 -lemma dvd_trans:
   6.204 -  assumes "a dvd b" and "b dvd c"
   6.205 -  shows "a dvd c"
   6.206 -proof -
   6.207 -  from assms obtain v where "b = a * v" unfolding dvd_def by auto
   6.208 -  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
   6.209 -  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   6.210 -  then show ?thesis unfolding dvd_def ..
   6.211 -qed
   6.212 -
   6.213 -lemma zero_dvd_iff [noatp]: "0 dvd a \<longleftrightarrow> a = 0"
   6.214 -  unfolding dvd_def by simp
   6.215 -
   6.216 -lemma dvd_0: "a dvd 0"
   6.217 -unfolding dvd_def proof
   6.218 -  show "0 = a * 0" by simp
   6.219 +  then show "b mod a = 0" by simp
   6.220  qed
   6.221  
   6.222 -lemma one_dvd: "1 dvd a"
   6.223 -  unfolding dvd_def by simp
   6.224 -
   6.225 -lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
   6.226 -  unfolding dvd_def by (blast intro: mult_left_commute)
   6.227 -
   6.228 -lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   6.229 -  apply (subst mult_commute)
   6.230 -  apply (erule dvd_mult)
   6.231 -  done
   6.232 -
   6.233 -lemma dvd_triv_right: "a dvd b * a"
   6.234 -  by (rule dvd_mult) (rule dvd_refl)
   6.235 -
   6.236 -lemma dvd_triv_left: "a dvd a * b"
   6.237 -  by (rule dvd_mult2) (rule dvd_refl)
   6.238 -
   6.239 -lemma mult_dvd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> a * b dvd c * d"
   6.240 -  apply (unfold dvd_def, clarify)
   6.241 -  apply (rule_tac x = "k * ka" in exI)
   6.242 -  apply (simp add: mult_ac)
   6.243 -  done
   6.244 -
   6.245 -lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   6.246 -  by (simp add: dvd_def mult_assoc, blast)
   6.247 -
   6.248 -lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   6.249 -  unfolding mult_ac [of a] by (rule dvd_mult_left)
   6.250 -
   6.251  end
   6.252  
   6.253  
   6.254 @@ -352,7 +333,10 @@
   6.255    fix n :: nat show "n div 0 = 0"
   6.256      using divmod_zero divmod_div_mod [of n 0] by simp
   6.257  next
   6.258 -  fix m n :: nat assume "n \<noteq> 0" then show "m * n div n = m"
   6.259 +  fix n :: nat show "0 div n = 0"
   6.260 +    using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
   6.261 +next
   6.262 +  fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
   6.263      by (induct m) (simp_all add: le_div_geq)
   6.264  qed
   6.265  
   6.266 @@ -360,10 +344,8 @@
   6.267  
   6.268  text {* Simproc for cancelling @{const div} and @{const mod} *}
   6.269  
   6.270 -lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
   6.271 -lemmas mod_div_equality2 = mod_div_equality2 [of "n\<Colon>nat" m, standard]
   6.272 -lemmas div_mod_equality = div_mod_equality [of "m\<Colon>nat" n k, standard]
   6.273 -lemmas div_mod_equality2 = div_mod_equality2 [of "m\<Colon>nat" n k, standard]
   6.274 +(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
   6.275 +lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\<Colon>nat" m, standard*)
   6.276  
   6.277  ML {*
   6.278  structure CancelDivModData =
   6.279 @@ -414,9 +396,6 @@
   6.280  
   6.281  subsubsection {* Quotient *}
   6.282  
   6.283 -lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
   6.284 -lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
   6.285 -
   6.286  lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
   6.287    by (simp add: le_div_geq linorder_not_less)
   6.288  
   6.289 @@ -424,17 +403,14 @@
   6.290    by (simp add: div_geq)
   6.291  
   6.292  lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   6.293 -  by (rule mult_div) simp
   6.294 +  by simp
   6.295  
   6.296  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   6.297 -  by (simp add: mult_commute)
   6.298 +  by simp
   6.299  
   6.300  
   6.301  subsubsection {* Remainder *}
   6.302  
   6.303 -lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
   6.304 -lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
   6.305 -
   6.306  lemma mod_less_divisor [simp]:
   6.307    fixes m n :: nat
   6.308    assumes "n > 0"
   6.309 @@ -458,23 +434,6 @@
   6.310  lemma mod_1 [simp]: "m mod Suc 0 = 0"
   6.311    by (induct m) (simp_all add: mod_geq)
   6.312  
   6.313 -lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
   6.314 -
   6.315 -lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
   6.316 -  apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
   6.317 -   apply (simp add: add_commute)
   6.318 -  apply (subst le_mod_geq [symmetric], simp_all)
   6.319 -  done
   6.320 -
   6.321 -lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
   6.322 -  by (simp add: add_commute mod_add_self2)
   6.323 -
   6.324 -lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
   6.325 -  by (induct k) (simp_all add: add_left_commute [of _ n])
   6.326 -
   6.327 -lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
   6.328 -  by (simp add: mult_commute mod_mult_self1)
   6.329 -
   6.330  lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
   6.331    apply (cases "n = 0", simp)
   6.332    apply (cases "k = 0", simp)
   6.333 @@ -486,20 +445,9 @@
   6.334  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
   6.335    by (simp add: mult_commute [of k] mod_mult_distrib)
   6.336  
   6.337 -lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
   6.338 -  apply (cases "n = 0", simp)
   6.339 -  apply (induct m, simp)
   6.340 -  apply (rename_tac k)
   6.341 -  apply (cut_tac m = "k * n" and n = n in mod_add_self2)
   6.342 -  apply (simp add: add_commute)
   6.343 -  done
   6.344 -
   6.345 -lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
   6.346 -  by (simp add: mult_commute mod_mult_self_is_0)
   6.347 -
   6.348  (* a simple rearrangement of mod_div_equality: *)
   6.349  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   6.350 -  by (cut_tac m = m and n = n in mod_div_equality2, arith)
   6.351 +  by (cut_tac a = m and b = n in mod_div_equality2, arith)
   6.352  
   6.353  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   6.354    apply (drule mod_less_divisor [where m = m])
   6.355 @@ -508,17 +456,6 @@
   6.356  
   6.357  subsubsection {* Quotient and Remainder *}
   6.358  
   6.359 -lemma mod_div_decomp:
   6.360 -  fixes n k :: nat
   6.361 -  obtains m q where "m = n div k" and "q = n mod k"
   6.362 -    and "n = m * k + q"
   6.363 -proof -
   6.364 -  from mod_div_equality have "n = n div k * k + n mod k" by auto
   6.365 -  moreover have "n div k = n div k" ..
   6.366 -  moreover have "n mod k = n mod k" ..
   6.367 -  note that ultimately show thesis by blast
   6.368 -qed
   6.369 -
   6.370  lemma divmod_rel_mult1_eq:
   6.371    "[| divmod_rel b c q r; c > 0 |]
   6.372     ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
   6.373 @@ -610,25 +547,6 @@
   6.374  lemma div_1 [simp]: "m div Suc 0 = m"
   6.375    by (induct m) (simp_all add: div_geq)
   6.376  
   6.377 -lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
   6.378 -
   6.379 -lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   6.380 -  apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
   6.381 -   apply (simp add: add_commute)
   6.382 -  apply (subst div_geq [symmetric], simp_all)
   6.383 -  done
   6.384 -
   6.385 -lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
   6.386 -  by (simp add: add_commute div_add_self2)
   6.387 -
   6.388 -lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
   6.389 -  apply (subst div_add1_eq)
   6.390 -  apply (subst div_mult1_eq, simp)
   6.391 -  done
   6.392 -
   6.393 -lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
   6.394 -  by (simp add: mult_commute div_mult_self1)
   6.395 -
   6.396  
   6.397  (* Monotonicity of div in first argument *)
   6.398  lemma div_le_mono [rule_format (no_asm)]:
   6.399 @@ -707,24 +625,7 @@
   6.400    by (cases "n = 0") auto
   6.401  
   6.402  
   6.403 -subsubsection{*The Divides Relation*}
   6.404 -
   6.405 -lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   6.406 -  unfolding dvd_def by blast
   6.407 -
   6.408 -lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
   6.409 -  unfolding dvd_def by blast
   6.410 -
   6.411 -lemma dvd_0_right [iff]: "m dvd (0::nat)"
   6.412 -  unfolding dvd_def by (blast intro: mult_0_right [symmetric])
   6.413 -
   6.414 -lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
   6.415 -  by (force simp add: dvd_def)
   6.416 -
   6.417 -lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
   6.418 -  by (blast intro: dvd_0_left)
   6.419 -
   6.420 -declare dvd_0_left_iff [noatp]
   6.421 +subsubsection {* The Divides Relation *}
   6.422  
   6.423  lemma dvd_1_left [iff]: "Suc 0 dvd k"
   6.424    unfolding dvd_def by simp
   6.425 @@ -732,9 +633,6 @@
   6.426  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   6.427    by (simp add: dvd_def)
   6.428  
   6.429 -lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
   6.430 -lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
   6.431 -
   6.432  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   6.433    unfolding dvd_def
   6.434    by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   6.435 @@ -742,11 +640,7 @@
   6.436  text {* @{term "op dvd"} is a partial order *}
   6.437  
   6.438  interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
   6.439 -  by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
   6.440 -
   6.441 -lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
   6.442 -  unfolding dvd_def
   6.443 -  by (blast intro: add_mult_distrib2 [symmetric])
   6.444 +  by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
   6.445  
   6.446  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   6.447    unfolding dvd_def
   6.448 @@ -760,20 +654,6 @@
   6.449  lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
   6.450    by (drule_tac m = m in dvd_diff, auto)
   6.451  
   6.452 -lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
   6.453 -  unfolding dvd_def by (blast intro: mult_left_commute)
   6.454 -
   6.455 -lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
   6.456 -  apply (subst mult_commute)
   6.457 -  apply (erule dvd_mult)
   6.458 -  done
   6.459 -
   6.460 -lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
   6.461 -  by (rule dvd_refl [THEN dvd_mult])
   6.462 -
   6.463 -lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
   6.464 -  by (rule dvd_refl [THEN dvd_mult2])
   6.465 -
   6.466  lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
   6.467    apply (rule iffI)
   6.468     apply (erule_tac [2] dvd_add)
   6.469 @@ -817,21 +697,6 @@
   6.470    apply (erule dvd_mult_cancel1)
   6.471    done
   6.472  
   6.473 -lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
   6.474 -  apply (unfold dvd_def, clarify)
   6.475 -  apply (rule_tac x = "k*ka" in exI)
   6.476 -  apply (simp add: mult_ac)
   6.477 -  done
   6.478 -
   6.479 -lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
   6.480 -  by (simp add: dvd_def mult_assoc, blast)
   6.481 -
   6.482 -lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
   6.483 -  apply (unfold dvd_def, clarify)
   6.484 -  apply (rule_tac x = "i*k" in exI)
   6.485 -  apply (simp add: mult_ac)
   6.486 -  done
   6.487 -
   6.488  lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
   6.489    apply (unfold dvd_def, clarify)
   6.490    apply (simp_all (no_asm_use) add: zero_less_mult_iff)
   6.491 @@ -841,8 +706,6 @@
   6.492     apply (erule_tac [2] Suc_leI, simp)
   6.493    done
   6.494  
   6.495 -lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
   6.496 -
   6.497  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   6.498    apply (subgoal_tac "m mod n = 0")
   6.499     apply (simp add: mult_div_cancel)
   6.500 @@ -888,7 +751,7 @@
   6.501  
   6.502  (*Loses information, namely we also have r<d provided d is nonzero*)
   6.503  lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
   6.504 -  apply (cut_tac m = m in mod_div_equality)
   6.505 +  apply (cut_tac a = m in mod_div_equality)
   6.506    apply (simp only: add_ac)
   6.507    apply (blast intro: sym)
   6.508    done
   6.509 @@ -902,7 +765,7 @@
   6.510    show ?Q
   6.511    proof (cases)
   6.512      assume "k = 0"
   6.513 -    with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
   6.514 +    with P show ?Q by simp
   6.515    next
   6.516      assume not0: "k \<noteq> 0"
   6.517      thus ?Q
   6.518 @@ -924,7 +787,7 @@
   6.519    show ?P
   6.520    proof (cases)
   6.521      assume "k = 0"
   6.522 -    with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
   6.523 +    with Q show ?P by simp
   6.524    next
   6.525      assume not0: "k \<noteq> 0"
   6.526      with Q have R: ?R by simp
   6.527 @@ -958,7 +821,7 @@
   6.528     (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   6.529    apply (case_tac "0 < n")
   6.530    apply (simp only: add: split_div_lemma)
   6.531 -  apply (simp_all add: DIVISION_BY_ZERO_DIV)
   6.532 +  apply simp_all
   6.533    done
   6.534  
   6.535  lemma split_mod:
   6.536 @@ -970,7 +833,7 @@
   6.537    show ?Q
   6.538    proof (cases)
   6.539      assume "k = 0"
   6.540 -    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
   6.541 +    with P show ?Q by simp
   6.542    next
   6.543      assume not0: "k \<noteq> 0"
   6.544      thus ?Q
   6.545 @@ -985,7 +848,7 @@
   6.546    show ?P
   6.547    proof (cases)
   6.548      assume "k = 0"
   6.549 -    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
   6.550 +    with Q show ?P by simp
   6.551    next
   6.552      assume not0: "k \<noteq> 0"
   6.553      with Q have R: ?R by simp
     7.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Fri Jul 18 17:09:48 2008 +0200
     7.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Fri Jul 18 18:25:53 2008 +0200
     7.3 @@ -1,6 +1,8 @@
     7.4  header {* \section{Examples} *}
     7.5  
     7.6 -theory RG_Examples imports RG_Syntax begin
     7.7 +theory RG_Examples
     7.8 +imports RG_Syntax
     7.9 +begin
    7.10  
    7.11  lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
    7.12  
    7.13 @@ -291,18 +293,14 @@
    7.14      apply force
    7.15     apply force
    7.16    apply(rule Basic)
    7.17 -     apply simp
    7.18 +     apply (simp add: mod_add_self2)
    7.19       apply clarify
    7.20       apply simp
    7.21 -     apply(case_tac "X x (j mod n)\<le> j")
    7.22 -      apply(drule le_imp_less_or_eq)
    7.23 -      apply(erule disjE)
    7.24 -       apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
    7.25 -        apply assumption+
    7.26 -       apply simp+
    7.27 -    apply clarsimp
    7.28 -    apply fastsimp
    7.29 -apply force+
    7.30 +     apply (case_tac "X x (j mod n) \<le> j")
    7.31 +     apply (drule le_imp_less_or_eq)
    7.32 +     apply (erule disjE)
    7.33 +     apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
    7.34 +     apply auto
    7.35  done
    7.36  
    7.37  text {* Same but with a list as auxiliary variable: *}
    7.38 @@ -348,16 +346,14 @@
    7.39    apply(rule Basic)
    7.40       apply simp
    7.41       apply clarify
    7.42 -     apply simp
    7.43 +     apply (simp add: mod_add_self2)
    7.44       apply(rule allI)
    7.45       apply(rule impI)+
    7.46       apply(case_tac "X x ! i\<le> j")
    7.47        apply(drule le_imp_less_or_eq)
    7.48        apply(erule disjE)
    7.49         apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
    7.50 -        apply assumption+
    7.51 -       apply simp
    7.52 -apply force+
    7.53 +     apply auto
    7.54  done
    7.55  
    7.56  end
     8.1 --- a/src/HOL/Import/HOL/divides.imp	Fri Jul 18 17:09:48 2008 +0200
     8.2 +++ b/src/HOL/Import/HOL/divides.imp	Fri Jul 18 18:25:53 2008 +0200
     8.3 @@ -9,16 +9,16 @@
     8.4    "divides_def" > "HOL4Compat.divides_def"
     8.5    "ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
     8.6    "NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
     8.7 -  "DIVIDES_TRANS" > "Divides.dvd_trans"
     8.8 -  "DIVIDES_SUB" > "Divides.dvd_diff"
     8.9 -  "DIVIDES_REFL" > "Divides.dvd_refl"
    8.10 +  "DIVIDES_TRANS" > "Ring_and_Field.dvd_trans"
    8.11 +  "DIVIDES_SUB" > "Ring_and_Field.dvd_diff"
    8.12 +  "DIVIDES_REFL" > "Ring_and_Field.dvd_refl"
    8.13    "DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
    8.14    "DIVIDES_MULT" > "Divides.dvd_mult2"
    8.15    "DIVIDES_LE" > "Divides.dvd_imp_le"
    8.16    "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
    8.17    "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
    8.18    "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
    8.19 -  "DIVIDES_ADD_1" > "Divides.dvd_add"
    8.20 +  "DIVIDES_ADD_1" > "Ring_and_Field.dvd_add"
    8.21    "ALL_DIVIDES_0" > "Divides.dvd_0_right"
    8.22  
    8.23  end
     9.1 --- a/src/HOL/IntDiv.thy	Fri Jul 18 17:09:48 2008 +0200
     9.2 +++ b/src/HOL/IntDiv.thy	Fri Jul 18 18:25:53 2008 +0200
     9.3 @@ -747,8 +747,49 @@
     9.4  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     9.5  by (simp add: zdiv_zmult1_eq)
     9.6  
     9.7 +lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
     9.8 +apply (case_tac "b = 0", simp)
     9.9 +apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    9.10 +done
    9.11 +
    9.12 +lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    9.13 +apply (case_tac "b = 0", simp)
    9.14 +apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    9.15 +done
    9.16 +
    9.17 +text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    9.18 +
    9.19 +lemma zadd1_lemma:
    9.20 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]  
    9.21 +      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    9.22 +by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
    9.23 +
    9.24 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    9.25 +lemma zdiv_zadd1_eq:
    9.26 +     "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
    9.27 +apply (case_tac "c = 0", simp)
    9.28 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
    9.29 +done
    9.30 +
    9.31 +lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    9.32 +apply (case_tac "c = 0", simp)
    9.33 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    9.34 +done
    9.35 +
    9.36 +lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    9.37 +by (simp add: zdiv_zadd1_eq)
    9.38 +
    9.39 +lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    9.40 +by (simp add: zdiv_zadd1_eq)
    9.41 +
    9.42  instance int :: semiring_div
    9.43 -  by intro_classes auto
    9.44 +proof
    9.45 +  fix a b c :: int
    9.46 +  assume not0: "b \<noteq> 0"
    9.47 +  show "(a + c * b) div b = c + a div b"
    9.48 +    unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    9.49 +      by (simp add: zmod_zmult1_eq)
    9.50 +qed auto
    9.51  
    9.52  lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    9.53  by (subst mult_commute, erule zdiv_zmult_self1)
    9.54 @@ -770,35 +811,6 @@
    9.55  
    9.56  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    9.57  
    9.58 -text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    9.59 -
    9.60 -lemma zadd1_lemma:
    9.61 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]  
    9.62 -      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    9.63 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
    9.64 -
    9.65 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    9.66 -lemma zdiv_zadd1_eq:
    9.67 -     "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
    9.68 -apply (case_tac "c = 0", simp)
    9.69 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
    9.70 -done
    9.71 -
    9.72 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    9.73 -apply (case_tac "c = 0", simp)
    9.74 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    9.75 -done
    9.76 -
    9.77 -lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
    9.78 -apply (case_tac "b = 0", simp)
    9.79 -apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    9.80 -done
    9.81 -
    9.82 -lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    9.83 -apply (case_tac "b = 0", simp)
    9.84 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    9.85 -done
    9.86 -
    9.87  lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    9.88  apply (rule trans [symmetric])
    9.89  apply (rule zmod_zadd1_eq, simp)
    9.90 @@ -811,12 +823,6 @@
    9.91  apply (rule zmod_zadd1_eq [symmetric])
    9.92  done
    9.93  
    9.94 -lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    9.95 -by (simp add: zdiv_zadd1_eq)
    9.96 -
    9.97 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    9.98 -by (simp add: zdiv_zadd1_eq)
    9.99 -
   9.100  lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
   9.101  apply (case_tac "a = 0", simp)
   9.102  apply (simp add: zmod_zadd1_eq)
   9.103 @@ -1183,33 +1189,36 @@
   9.104  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
   9.105    by (auto simp add: dvd_def intro: mult_assoc)
   9.106  
   9.107 -lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
   9.108 -  apply (simp add: dvd_def, auto)
   9.109 -   apply (rule_tac [!] x = "-k" in exI, auto)
   9.110 -  done
   9.111 +lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
   9.112 +proof
   9.113 +  assume "m dvd - n"
   9.114 +  then obtain k where "- n = m * k" ..
   9.115 +  then have "n = m * - k" by simp
   9.116 +  then show "m dvd n" ..
   9.117 +next
   9.118 +  assume "m dvd n"
   9.119 +  then have "m dvd n * -1" by (rule dvd_mult2)
   9.120 +  then show "m dvd - n" by simp
   9.121 +qed
   9.122  
   9.123 -lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
   9.124 -  apply (simp add: dvd_def, auto)
   9.125 -   apply (rule_tac [!] x = "-k" in exI, auto)
   9.126 -  done
   9.127 +lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
   9.128 +proof
   9.129 +  assume "- m dvd n"
   9.130 +  then obtain k where "n = - m * k" ..
   9.131 +  then have "n = m * - k" by simp
   9.132 +  then show "m dvd n" ..
   9.133 +next
   9.134 +  assume "m dvd n"
   9.135 +  then obtain k where "n = m * k" ..
   9.136 +  then have "n = - m * - k" by simp
   9.137 +  then show "- m dvd n" ..
   9.138 +qed
   9.139 +
   9.140  lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
   9.141 -  apply (cases "i > 0", simp)
   9.142 -  apply (simp add: dvd_def)
   9.143 -  apply (rule iffI)
   9.144 -  apply (erule exE)
   9.145 -  apply (rule_tac x="- k" in exI, simp)
   9.146 -  apply (erule exE)
   9.147 -  apply (rule_tac x="- k" in exI, simp)
   9.148 -  done
   9.149 +  by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
   9.150 +
   9.151  lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
   9.152 -  apply (cases "j > 0", simp)
   9.153 -  apply (simp add: dvd_def)
   9.154 -  apply (rule iffI)
   9.155 -  apply (erule exE)
   9.156 -  apply (rule_tac x="- k" in exI, simp)
   9.157 -  apply (erule exE)
   9.158 -  apply (rule_tac x="- k" in exI, simp)
   9.159 -  done
   9.160 +  by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
   9.161  
   9.162  lemma zdvd_anti_sym:
   9.163      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   9.164 @@ -1276,10 +1285,7 @@
   9.165    done
   9.166  
   9.167  lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   9.168 -  apply (simp add: dvd_def, clarify)
   9.169 -  apply (rule_tac x = "k * ka" in exI)
   9.170 -  apply (simp add: mult_ac)
   9.171 -  done
   9.172 +  by (rule mult_dvd_mono)
   9.173  
   9.174  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   9.175    apply (rule iffI)
   9.176 @@ -1301,7 +1307,7 @@
   9.177    done
   9.178  
   9.179  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   9.180 -  apply (simp add: dvd_def, auto)
   9.181 +  apply (auto elim!: dvdE)
   9.182    apply (subgoal_tac "0 < n")
   9.183     prefer 2
   9.184     apply (blast intro: order_less_trans)
   9.185 @@ -1309,6 +1315,7 @@
   9.186    apply (subgoal_tac "n * k < n * 1")
   9.187     apply (drule mult_less_cancel_left [THEN iffD1], auto)
   9.188    done
   9.189 +
   9.190  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   9.191    using zmod_zdiv_equality[where a="m" and b="n"]
   9.192    by (simp add: ring_simps)
   9.193 @@ -1348,21 +1355,24 @@
   9.194  done
   9.195  
   9.196  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   9.197 -apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   9.198 -    nat_0_le cong add: conj_cong)
   9.199 -apply (rule iffI)
   9.200 -apply iprover
   9.201 -apply (erule exE)
   9.202 -apply (case_tac "x=0")
   9.203 -apply (rule_tac x=0 in exI)
   9.204 -apply simp
   9.205 -apply (case_tac "0 \<le> k")
   9.206 -apply iprover
   9.207 -apply (simp add: neq0_conv linorder_not_le)
   9.208 -apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   9.209 -apply assumption
   9.210 -apply (simp add: mult_ac)
   9.211 -done
   9.212 +proof -
   9.213 +  have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
   9.214 +  proof -
   9.215 +    fix k
   9.216 +    assume A: "int y = int x * k"
   9.217 +    then show "x dvd y" proof (cases k)
   9.218 +      case (1 n) with A have "y = x * n" by (simp add: zmult_int)
   9.219 +      then show ?thesis ..
   9.220 +    next
   9.221 +      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
   9.222 +      also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
   9.223 +      also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
   9.224 +      finally have "- int (x * Suc n) = int y" ..
   9.225 +      then show ?thesis by (simp only: negative_eq_positive) auto
   9.226 +    qed
   9.227 +  qed
   9.228 +  then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
   9.229 +qed 
   9.230  
   9.231  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   9.232  proof
   9.233 @@ -1385,41 +1395,19 @@
   9.234  qed
   9.235  
   9.236  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   9.237 -  apply (auto simp add: dvd_def nat_abs_mult_distrib)
   9.238 -  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
   9.239 -   apply (rule_tac x = "-(int k)" in exI)
   9.240 -  apply (auto simp add: int_mult)
   9.241 -  done
   9.242 +  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
   9.243  
   9.244  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   9.245 -  apply (auto simp add: dvd_def abs_if int_mult)
   9.246 -    apply (rule_tac [3] x = "nat k" in exI)
   9.247 -    apply (rule_tac [2] x = "-(int k)" in exI)
   9.248 -    apply (rule_tac x = "nat (-k)" in exI)
   9.249 -    apply (cut_tac [3] k = m in int_less_0_conv)
   9.250 -    apply (cut_tac k = m in int_less_0_conv)
   9.251 -    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
   9.252 -      nat_mult_distrib [symmetric] nat_eq_iff2)
   9.253 -  done
   9.254 +  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
   9.255  
   9.256  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   9.257 -  apply (auto simp add: dvd_def int_mult)
   9.258 -  apply (rule_tac x = "nat k" in exI)
   9.259 -  apply (cut_tac k = m in int_less_0_conv)
   9.260 -  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
   9.261 -    nat_mult_distrib [symmetric] nat_eq_iff2)
   9.262 -  done
   9.263 +  by (auto simp add: dvd_int_iff)
   9.264  
   9.265  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   9.266 -  apply (auto simp add: dvd_def)
   9.267 -   apply (rule_tac [!] x = "-k" in exI, auto)
   9.268 -  done
   9.269 +  by (simp add: zdvd_zminus2_iff)
   9.270  
   9.271  lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   9.272 -  apply (auto simp add: dvd_def)
   9.273 -   apply (drule minus_equation_iff [THEN iffD1])
   9.274 -   apply (rule_tac [!] x = "-k" in exI, auto)
   9.275 -  done
   9.276 +  by (simp add: zdvd_zminus_iff)
   9.277  
   9.278  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   9.279    apply (rule_tac z=n in int_cases)
    10.1 --- a/src/HOL/Library/Char_nat.thy	Fri Jul 18 17:09:48 2008 +0200
    10.2 +++ b/src/HOL/Library/Char_nat.thy	Fri Jul 18 18:25:53 2008 +0200
    10.3 @@ -156,7 +156,7 @@
    10.4    have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
    10.5      using l by auto
    10.6    have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
    10.7 -    unfolding 256 mult_assoc [symmetric] mod_mult_self_is_0 by simp
    10.8 +    unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
    10.9    have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
   10.10      unfolding div_add1_eq [of "k * 256" l 16] aux2 256
   10.11        mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
    11.1 --- a/src/HOL/Library/GCD.thy	Fri Jul 18 17:09:48 2008 +0200
    11.2 +++ b/src/HOL/Library/GCD.thy	Fri Jul 18 18:25:53 2008 +0200
    11.3 @@ -148,8 +148,7 @@
    11.4    done
    11.5  
    11.6  lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
    11.7 -  apply (blast intro: relprime_dvd_mult dvd_trans)
    11.8 -  done
    11.9 +  by (auto intro: relprime_dvd_mult dvd_mult2)
   11.10  
   11.11  lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   11.12    apply (rule dvd_anti_sym)
   11.13 @@ -158,7 +157,7 @@
   11.14       apply (simp add: gcd_assoc)
   11.15       apply (simp add: gcd_commute)
   11.16      apply (simp_all add: mult_commute)
   11.17 -  apply (blast intro: dvd_trans)
   11.18 +  apply (blast intro: dvd_mult)
   11.19    done
   11.20  
   11.21  
   11.22 @@ -167,6 +166,7 @@
   11.23  lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   11.24    apply (case_tac "n = 0")
   11.25     apply (simp_all add: gcd_non_0)
   11.26 +  apply (simp add: mod_add_self2)
   11.27    done
   11.28  
   11.29  lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
   11.30 @@ -549,4 +549,8 @@
   11.31    thus ?thesis by (simp add: zlcm_def)
   11.32  qed
   11.33  
   11.34 +lemma zgcd_code [code func]:
   11.35 +  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   11.36 +  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
   11.37 +
   11.38  end
    12.1 --- a/src/HOL/Library/Parity.thy	Fri Jul 18 17:09:48 2008 +0200
    12.2 +++ b/src/HOL/Library/Parity.thy	Fri Jul 18 18:25:53 2008 +0200
    12.3 @@ -382,13 +382,14 @@
    12.4  done
    12.5  
    12.6  lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
    12.7 -apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
    12.8 +apply (rule mod_div_equality [of n 4, THEN subst])
    12.9  apply (simp add: even_num_iff)
   12.10  done
   12.11  
   12.12  lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   12.13 -by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
   12.14 -
   12.15 +apply (rule mod_div_equality [of n 4, THEN subst])
   12.16 +apply simp
   12.17 +done
   12.18  
   12.19  text {* Simplify, when the exponent is a numeral *}
   12.20  
    13.1 --- a/src/HOL/Library/Primes.thy	Fri Jul 18 17:09:48 2008 +0200
    13.2 +++ b/src/HOL/Library/Primes.thy	Fri Jul 18 18:25:53 2008 +0200
    13.3 @@ -789,21 +789,23 @@
    13.4      from coprime_prime_dvd_ex[OF c] obtain p 
    13.5        where p: "prime p" "p dvd x*y" "p dvd x^2 + y^2" by blast
    13.6      {assume px: "p dvd x"
    13.7 -      from dvd_mult[OF px, of x] p(3) have "p dvd y^2" 
    13.8 -	unfolding dvd_def 
    13.9 -	apply (auto simp add: power2_eq_square)
   13.10 -	apply (rule_tac x= "ka - k" in exI)
   13.11 -	by (simp add: diff_mult_distrib2)
   13.12 +      from dvd_mult[OF px, of x] p(3) 
   13.13 +        obtain r s where "x * x = p * r" and "x^2 + y^2 = p * s"
   13.14 +          by (auto elim!: dvdE)
   13.15 +        then have "y^2 = p * (s - r)" 
   13.16 +          by (auto simp add: power2_eq_square diff_mult_distrib2)
   13.17 +        then have "p dvd y^2" ..
   13.18        with prime_divexp[OF p(1), of y 2] have py: "p dvd y" .
   13.19        from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1  
   13.20        have False by simp }
   13.21      moreover
   13.22      {assume py: "p dvd y"
   13.23 -      from dvd_mult[OF py, of y] p(3) have "p dvd x^2" 
   13.24 -	unfolding dvd_def 
   13.25 -	apply (auto simp add: power2_eq_square)
   13.26 -	apply (rule_tac x= "ka - k" in exI)
   13.27 -	by (simp add: diff_mult_distrib2)
   13.28 +      from dvd_mult[OF py, of y] p(3)
   13.29 +        obtain r s where "y * y = p * r" and "x^2 + y^2 = p * s"
   13.30 +          by (auto elim!: dvdE)
   13.31 +        then have "x^2 = p * (s - r)" 
   13.32 +          by (auto simp add: power2_eq_square diff_mult_distrib2)
   13.33 +        then have "p dvd x^2" ..
   13.34        with prime_divexp[OF p(1), of x 2] have px: "p dvd x" .
   13.35        from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1  
   13.36        have False by simp }
   13.37 @@ -953,7 +955,18 @@
   13.38  
   13.39  text {* More useful lemmas. *}
   13.40  lemma prime_product: 
   13.41 -  "prime (p*q) \<Longrightarrow> p = 1 \<or> q  = 1" unfolding prime_def by auto
   13.42 +  assumes "prime (p * q)"
   13.43 +  shows "p = 1 \<or> q = 1"
   13.44 +proof -
   13.45 +  from assms have 
   13.46 +    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   13.47 +    unfolding prime_def by auto
   13.48 +  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
   13.49 +  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   13.50 +  have "p dvd p * q" by simp
   13.51 +  then have "p = 1 \<or> p = p * q" by (rule P)
   13.52 +  then show ?thesis by (simp add: Q)
   13.53 +qed
   13.54  
   13.55  lemma prime_exp: "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
   13.56  proof(induct n)
    14.1 --- a/src/HOL/NSA/StarDef.thy	Fri Jul 18 17:09:48 2008 +0200
    14.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Jul 18 18:25:53 2008 +0200
    14.3 @@ -531,6 +531,8 @@
    14.4  
    14.5  end
    14.6  
    14.7 +instance star :: (Ring_and_Field.dvd) Ring_and_Field.dvd ..
    14.8 +
    14.9  instantiation star :: (Divides.div) Divides.div
   14.10  begin
   14.11  
    15.1 --- a/src/HOL/NatBin.thy	Fri Jul 18 17:09:48 2008 +0200
    15.2 +++ b/src/HOL/NatBin.thy	Fri Jul 18 18:25:53 2008 +0200
    15.3 @@ -67,8 +67,8 @@
    15.4  
    15.5  lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
    15.6  apply (case_tac "0 <= z'")
    15.7 -apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
    15.8 -apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
    15.9 +apply (auto simp add: div_nonneg_neg_le0)
   15.10 +apply (case_tac "z' = 0", simp)
   15.11  apply (auto elim!: nonneg_eq_int)
   15.12  apply (rename_tac m m')
   15.13  apply (subgoal_tac "0 <= int m div int m'")
   15.14 @@ -145,9 +145,7 @@
   15.15           (if neg (number_of v :: int) then number_of v'  
   15.16            else if neg (number_of v' :: int) then number_of v  
   15.17            else number_of (v + v'))"
   15.18 -by (force dest!: neg_nat
   15.19 -          simp del: nat_number_of
   15.20 -          simp add: nat_number_of_def nat_add_distrib [symmetric]) 
   15.21 +by (simp add: neg_nat nat_number_of_def nat_add_distrib [symmetric] del: nat_number_of)
   15.22  
   15.23  
   15.24  subsubsection{*Subtraction *}
   15.25 @@ -157,8 +155,8 @@
   15.26          (if neg z' then nat z   
   15.27           else let d = z-z' in     
   15.28                if neg d then 0 else nat d)"
   15.29 -apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   15.30 -done
   15.31 +by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   15.32 +
   15.33  
   15.34  lemma diff_nat_number_of [simp]: 
   15.35       "(number_of v :: nat) - number_of v' =  
   15.36 @@ -174,10 +172,7 @@
   15.37  lemma mult_nat_number_of [simp]:
   15.38       "(number_of v :: nat) * number_of v' =  
   15.39         (if neg (number_of v :: int) then 0 else number_of (v * v'))"
   15.40 -by (force dest!: neg_nat
   15.41 -          simp del: nat_number_of
   15.42 -          simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
   15.43 -
   15.44 +by (simp add: neg_nat nat_number_of_def nat_mult_distrib [symmetric] del: nat_number_of)
   15.45  
   15.46  
   15.47  subsubsection{*Quotient *}
   15.48 @@ -186,12 +181,10 @@
   15.49       "(number_of v :: nat)  div  number_of v' =  
   15.50            (if neg (number_of v :: int) then 0  
   15.51             else nat (number_of v div number_of v'))"
   15.52 -by (force dest!: neg_nat
   15.53 -          simp del: nat_number_of
   15.54 -          simp add: nat_number_of_def nat_div_distrib [symmetric]) 
   15.55 +by (simp add: neg_nat nat_number_of_def nat_div_distrib [symmetric] del: nat_number_of)
   15.56  
   15.57  lemma one_div_nat_number_of [simp]:
   15.58 -     "(Suc 0)  div  number_of v' = (nat (1 div number_of v'))" 
   15.59 +     "Suc 0 div number_of v' = nat (1 div number_of v')" 
   15.60  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   15.61  
   15.62  
   15.63 @@ -202,12 +195,10 @@
   15.64          (if neg (number_of v :: int) then 0  
   15.65           else if neg (number_of v' :: int) then number_of v  
   15.66           else nat (number_of v mod number_of v'))"
   15.67 -by (force dest!: neg_nat
   15.68 -          simp del: nat_number_of
   15.69 -          simp add: nat_number_of_def nat_mod_distrib [symmetric]) 
   15.70 +by (simp add: neg_nat nat_number_of_def nat_mod_distrib [symmetric] del: nat_number_of)
   15.71  
   15.72  lemma one_mod_nat_number_of [simp]:
   15.73 -     "(Suc 0)  mod  number_of v' =  
   15.74 +     "Suc 0 mod number_of v' =  
   15.75          (if neg (number_of v' :: int) then Suc 0
   15.76           else nat (1 mod number_of v'))"
   15.77  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    16.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Jul 18 17:09:48 2008 +0200
    16.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Jul 18 18:25:53 2008 +0200
    16.3 @@ -5,7 +5,9 @@
    16.4  
    16.5  header {*Parity: Even and Odd Integers*}
    16.6  
    16.7 -theory EvenOdd imports Int2 begin
    16.8 +theory EvenOdd
    16.9 +imports Int2
   16.10 +begin
   16.11  
   16.12  definition
   16.13    zOdd    :: "int set" where
   16.14 @@ -224,7 +226,7 @@
   16.15  qed
   16.16  
   16.17  lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
   16.18 -  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
   16.19 +  by (auto simp add: zEven_def)
   16.20  
   16.21  lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
   16.22    by (auto simp add: zEven_def)
    17.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Jul 18 17:09:48 2008 +0200
    17.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Jul 18 18:25:53 2008 +0200
    17.3 @@ -127,9 +127,7 @@
    17.4    by (unfold zcong_def, auto)
    17.5  
    17.6  lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
    17.7 -  apply (unfold zcong_def dvd_def, auto)
    17.8 -   apply (rule_tac [!] x = "-k" in exI, auto)
    17.9 -  done
   17.10 +  unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
   17.11  
   17.12  lemma zcong_zadd:
   17.13      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
   17.14 @@ -147,9 +145,10 @@
   17.15  
   17.16  lemma zcong_trans:
   17.17      "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
   17.18 -  apply (unfold zcong_def dvd_def, auto)
   17.19 -  apply (rule_tac x = "k + ka" in exI)
   17.20 -  apply (simp add: zadd_ac zadd_zmult_distrib2)
   17.21 +  unfolding zcong_def
   17.22 +  apply (auto elim!: dvdE simp add: ring_simps)
   17.23 +  unfolding left_distrib [symmetric]
   17.24 +  apply (rule dvd_mult dvd_refl)+
   17.25    done
   17.26  
   17.27  lemma zcong_zmult:
   17.28 @@ -207,7 +206,7 @@
   17.29  lemma zcong_zgcd_zmult_zmod:
   17.30    "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
   17.31      ==> [a = b] (mod m * n)"
   17.32 -  apply (unfold zcong_def dvd_def, auto)
   17.33 +  apply (auto simp add: zcong_def dvd_def)
   17.34    apply (subgoal_tac "m dvd n * ka")
   17.35     apply (subgoal_tac "m dvd ka")
   17.36      apply (case_tac [2] "0 \<le> ka")
   17.37 @@ -255,8 +254,9 @@
   17.38    done
   17.39  
   17.40  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
   17.41 -  apply (unfold zcong_def dvd_def, auto)
   17.42 -   apply (rule_tac [!] x = "-k" in exI, auto)
   17.43 +  unfolding zcong_def
   17.44 +  apply (auto elim!: dvdE simp add: ring_simps)
   17.45 +  apply (rule_tac x = "-k" in exI) apply simp
   17.46    done
   17.47  
   17.48  lemma zgcd_zcong_zgcd:
   17.49 @@ -306,13 +306,7 @@
   17.50  
   17.51  lemma zmod_zdvd_zmod:
   17.52      "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   17.53 -  apply (unfold dvd_def, auto)
   17.54 -  apply (subst zcong_zmod_eq [symmetric])
   17.55 -   prefer 2
   17.56 -   apply (subst zcong_iff_lin)
   17.57 -   apply (rule_tac x = "k * (a div (m * k))" in exI)
   17.58 -   apply (simp add:zmult_assoc [symmetric], assumption)
   17.59 -  done
   17.60 +  by (rule zmod_zmod_cancel) 
   17.61  
   17.62  
   17.63  subsection {* Extended GCD *}
    18.1 --- a/src/HOL/Presburger.thy	Fri Jul 18 17:09:48 2008 +0200
    18.2 +++ b/src/HOL/Presburger.thy	Fri Jul 18 18:25:53 2008 +0200
    18.3 @@ -31,8 +31,8 @@
    18.4    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
    18.5    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
    18.6    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
    18.7 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (d dvd x + s) = (d dvd x + s)"
    18.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    18.9 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (d dvd x + s) = (d dvd x + s)"
   18.10 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   18.11    "\<exists>z.\<forall>x<z. F = F"
   18.12    by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
   18.13  
   18.14 @@ -47,8 +47,8 @@
   18.15    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
   18.16    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
   18.17    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
   18.18 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)"
   18.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   18.20 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (d dvd x + s) = (d dvd x + s)"
   18.21 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   18.22    "\<exists>z.\<forall>x>z. F = F"
   18.23    by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
   18.24  
   18.25 @@ -57,12 +57,12 @@
   18.26      \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
   18.27    "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
   18.28      \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
   18.29 -  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
   18.30 -  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
   18.31 +  "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
   18.32 +  "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
   18.33    "\<forall>x k. F = F"
   18.34 -by simp_all
   18.35 -  (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
   18.36 -    simp add: ring_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_simps)+
   18.37 +apply (auto elim!: dvdE simp add: ring_simps)
   18.38 +unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
   18.39 +unfolding dvd_def mult_commute [of d] by auto
   18.40  
   18.41  subsection{* The A and B sets *}
   18.42  lemma bset:
   18.43 @@ -114,11 +114,12 @@
   18.44  next
   18.45    assume d: "d dvd D"
   18.46    {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
   18.47 -      by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_simps)}
   18.48 +      by (auto elim!: dvdE simp add: ring_simps)
   18.49 +        (auto simp only: left_diff_distrib [symmetric] dvd_def mult_commute)}
   18.50    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
   18.51  next
   18.52    assume d: "d dvd D"
   18.53 -  {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t"
   18.54 +  {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not> d dvd (x - D) + t"
   18.55        by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)}
   18.56    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto
   18.57  qed blast
   18.58 @@ -360,16 +361,17 @@
   18.59  apply(fastsimp)
   18.60  done
   18.61  
   18.62 -theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   18.63 -  apply (rule eq_reflection[symmetric])
   18.64 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Ring_and_Field.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   18.65 +  apply (rule eq_reflection [symmetric])
   18.66    apply (rule iffI)
   18.67    defer
   18.68    apply (erule exE)
   18.69    apply (rule_tac x = "l * x" in exI)
   18.70    apply (simp add: dvd_def)
   18.71 -  apply (rule_tac x="x" in exI, simp)
   18.72 +  apply (rule_tac x = x in exI, simp)
   18.73    apply (erule exE)
   18.74    apply (erule conjE)
   18.75 +  apply simp
   18.76    apply (erule dvdE)
   18.77    apply (rule_tac x = k in exI)
   18.78    apply simp
   18.79 @@ -417,13 +419,13 @@
   18.80  
   18.81  lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
   18.82  unfolding zdvd_iff_zmod_eq_0[symmetric] ..
   18.83 -declare mod_1[presburger]
   18.84 +declare mod_1[presburger] 
   18.85  declare mod_0[presburger]
   18.86  declare zmod_1[presburger]
   18.87  declare zmod_zero[presburger]
   18.88  declare zmod_self[presburger]
   18.89  declare mod_self[presburger]
   18.90 -declare DIVISION_BY_ZERO_MOD[presburger]
   18.91 +declare mod_by_0[presburger]
   18.92  declare nat_mod_div_trivial[presburger]
   18.93  declare div_mod_equality2[presburger]
   18.94  declare div_mod_equality[presburger]
   18.95 @@ -435,7 +437,7 @@
   18.96  declare zdiv_zmod_equality[presburger]
   18.97  declare mod2_Suc_Suc[presburger]
   18.98  lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
   18.99 -using IntDiv.DIVISION_BY_ZERO by blast+
  18.100 +by simp_all
  18.101  
  18.102  use "Tools/Qelim/cooper.ML"
  18.103  oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
    19.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jul 18 17:09:48 2008 +0200
    19.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Jul 18 18:25:53 2008 +0200
    19.3 @@ -102,12 +102,108 @@
    19.4  
    19.5  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
    19.6  
    19.7 -class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
    19.8 +text {* Abstract divisibility *}
    19.9 +
   19.10 +class dvd = times
   19.11 +begin
   19.12 +
   19.13 +definition
   19.14 +  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
   19.15 +where
   19.16 +  [code func del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   19.17 +
   19.18 +lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   19.19 +  unfolding dvd_def ..
   19.20 +
   19.21 +lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   19.22 +  unfolding dvd_def by blast 
   19.23 +
   19.24 +end
   19.25 +
   19.26 +class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
   19.27    (*previously almost_semiring*)
   19.28  begin
   19.29  
   19.30  subclass semiring_1 ..
   19.31  
   19.32 +lemma dvd_refl: "a dvd a"
   19.33 +proof -
   19.34 +  have "a = a * 1" by simp
   19.35 +  then show ?thesis unfolding dvd_def ..
   19.36 +qed
   19.37 +
   19.38 +lemma dvd_trans:
   19.39 +  assumes "a dvd b" and "b dvd c"
   19.40 +  shows "a dvd c"
   19.41 +proof -
   19.42 +  from assms obtain v where "b = a * v" unfolding dvd_def by auto
   19.43 +  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
   19.44 +  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   19.45 +  then show ?thesis unfolding dvd_def ..
   19.46 +qed
   19.47 +
   19.48 +lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
   19.49 +  unfolding dvd_def by simp
   19.50 +
   19.51 +lemma dvd_0 [simp]: "a dvd 0"
   19.52 +unfolding dvd_def proof
   19.53 +  show "0 = a * 0" by simp
   19.54 +qed
   19.55 +
   19.56 +lemma one_dvd [simp]: "1 dvd a"
   19.57 +  unfolding dvd_def by simp
   19.58 +
   19.59 +lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
   19.60 +  unfolding dvd_def by (blast intro: mult_left_commute)
   19.61 +
   19.62 +lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   19.63 +  apply (subst mult_commute)
   19.64 +  apply (erule dvd_mult)
   19.65 +  done
   19.66 +
   19.67 +lemma dvd_triv_right [simp]: "a dvd b * a"
   19.68 +  by (rule dvd_mult) (rule dvd_refl)
   19.69 +
   19.70 +lemma dvd_triv_left [simp]: "a dvd a * b"
   19.71 +  by (rule dvd_mult2) (rule dvd_refl)
   19.72 +
   19.73 +lemma mult_dvd_mono:
   19.74 +  assumes ab: "a dvd b"
   19.75 +    and "cd": "c dvd d"
   19.76 +  shows "a * c dvd b * d"
   19.77 +proof -
   19.78 +  from ab obtain b' where "b = a * b'" ..
   19.79 +  moreover from "cd" obtain d' where "d = c * d'" ..
   19.80 +  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   19.81 +  then show ?thesis ..
   19.82 +qed
   19.83 +
   19.84 +lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   19.85 +  by (simp add: dvd_def mult_assoc, blast)
   19.86 +
   19.87 +lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   19.88 +  unfolding mult_ac [of a] by (rule dvd_mult_left)
   19.89 +
   19.90 +lemma dvd_0_right [iff]: "a dvd 0"
   19.91 +proof -
   19.92 +  have "0 = a * 0" by simp
   19.93 +  then show ?thesis unfolding dvd_def ..
   19.94 +qed
   19.95 +
   19.96 +lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   19.97 +  by simp
   19.98 +
   19.99 +lemma dvd_add:
  19.100 +  assumes ab: "a dvd b"
  19.101 +    and ac: "a dvd c"
  19.102 +    shows "a dvd (b + c)"
  19.103 +proof -
  19.104 +  from ab obtain b' where "b = a * b'" ..
  19.105 +  moreover from ac obtain c' where "c = a * c'" ..
  19.106 +  ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
  19.107 +  then show ?thesis ..
  19.108 +qed
  19.109 +
  19.110  end
  19.111  
  19.112  class no_zero_divisors = zero + times +
  19.113 @@ -973,6 +1069,26 @@
  19.114    "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  19.115    by (insert mult_less_cancel_left [of c a 1], simp)
  19.116  
  19.117 +lemma sgn_sgn [simp]:
  19.118 +  "sgn (sgn a) = sgn a"
  19.119 +  unfolding sgn_if by simp
  19.120 +
  19.121 +lemma sgn_0_0:
  19.122 +  "sgn a = 0 \<longleftrightarrow> a = 0"
  19.123 +  unfolding sgn_if by simp
  19.124 +
  19.125 +lemma sgn_1_pos:
  19.126 +  "sgn a = 1 \<longleftrightarrow> a > 0"
  19.127 +  unfolding sgn_if by (simp add: neg_equal_zero)
  19.128 +
  19.129 +lemma sgn_1_neg:
  19.130 +  "sgn a = - 1 \<longleftrightarrow> a < 0"
  19.131 +  unfolding sgn_if by (auto simp add: equal_neg_zero)
  19.132 +
  19.133 +lemma sgn_times:
  19.134 +  "sgn (a * b) = sgn a * sgn b"
  19.135 +  by (auto simp add: sgn_if zero_less_mult_iff)
  19.136 +
  19.137  end
  19.138  
  19.139  class ordered_field = field + ordered_idom
    20.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 18 17:09:48 2008 +0200
    20.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 18 18:25:53 2008 +0200
    20.3 @@ -80,9 +80,9 @@
    20.4  | Const (@{const_name HOL.less_eq}, _) $ y $ z => 
    20.5     if term_of x aconv y then Le (Thm.dest_arg ct) 
    20.6     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
    20.7 -| Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
    20.8 +| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
    20.9     if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox 
   20.10 -| Const (@{const_name Not},_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
   20.11 +| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
   20.12     if term_of x aconv y then 
   20.13     NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox 
   20.14  | _ => Nox)
   20.15 @@ -223,8 +223,8 @@
   20.16    | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
   20.17      lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
   20.18    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   20.19 -  | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = 
   20.20 -    HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
   20.21 +  | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) = 
   20.22 +    HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
   20.23    | lin (vs as x::_) ((b as Const("op =",_))$s$t) = 
   20.24       (case lint vs (subC$t$s) of 
   20.25        (t as a$(m$c$y)$r) => 
   20.26 @@ -252,7 +252,7 @@
   20.27    | is_intrel _ = false;
   20.28   
   20.29  fun linearize_conv ctxt vs ct = case term_of ct of
   20.30 -  Const(@{const_name Divides.dvd},_)$d$t => 
   20.31 +  Const(@{const_name Ring_and_Field.dvd},_)$d$t => 
   20.32    let 
   20.33      val th = binop_conv (lint_conv ctxt vs) ct
   20.34      val (d',t') = Thm.dest_binop (Thm.rhs_of th)
   20.35 @@ -277,7 +277,7 @@
   20.36        | _ => dth
   20.37       end
   20.38    end
   20.39 -| Const (@{const_name Not},_)$(Const(@{const_name Divides.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
   20.40 +| Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
   20.41  | t => if is_intrel t 
   20.42        then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
   20.43         RS eq_reflection
   20.44 @@ -300,7 +300,7 @@
   20.45      if x aconv y andalso member (op =)
   20.46         [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
   20.47      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   20.48 -  | Const(@{const_name Divides.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => 
   20.49 +  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => 
   20.50      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   20.51    | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   20.52    | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   20.53 @@ -340,7 +340,7 @@
   20.54      if x=y andalso member (op =)
   20.55        [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
   20.56      then cv (l div dest_numeral c) t else Thm.reflexive t
   20.57 -  | Const(@{const_name Divides.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => 
   20.58 +  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => 
   20.59      if x=y then 
   20.60        let 
   20.61         val k = l div dest_numeral c
   20.62 @@ -556,7 +556,7 @@
   20.63    | Const("False",_) => F
   20.64    | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   20.65    | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   20.66 -  | Const(@{const_name Divides.dvd},_)$t1$t2 => 
   20.67 +  | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => 
   20.68        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
   20.69    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
   20.70    | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    21.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Jul 18 17:09:48 2008 +0200
    21.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Jul 18 18:25:53 2008 +0200
    21.3 @@ -127,8 +127,8 @@
    21.4       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    21.5       @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
    21.6       @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
    21.7 -  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"}, 
    21.8 -     @{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
    21.9 +  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   21.10 +     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   21.11       @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   21.12       @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 
   21.13       @{thm "mod_1"}, @{thm "Suc_plus1"}]
    22.1 --- a/src/HOL/Word/BinBoolList.thy	Fri Jul 18 17:09:48 2008 +0200
    22.2 +++ b/src/HOL/Word/BinBoolList.thy	Fri Jul 18 18:25:53 2008 +0200
    22.3 @@ -1099,11 +1099,10 @@
    22.4    apply (subst bin_rsplit_aux.simps)
    22.5    apply (clarsimp simp: Let_def split: ls_splits)
    22.6    apply (erule thin_rl)
    22.7 +  apply (case_tac m)
    22.8 +  apply simp
    22.9    apply (case_tac "m <= n")
   22.10 -   prefer 2
   22.11 -   apply (simp add: div_add_self2 [symmetric])
   22.12 -  apply (case_tac m, clarsimp)
   22.13 -  apply (simp add: div_add_self2)
   22.14 +  apply (auto simp add: div_add_self2)
   22.15    done
   22.16  
   22.17  lemma bin_rsplit_len: 
    23.1 --- a/src/HOL/Word/Num_Lemmas.thy	Fri Jul 18 17:09:48 2008 +0200
    23.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Fri Jul 18 18:25:53 2008 +0200
    23.3 @@ -256,7 +256,6 @@
    23.4     prefer 2
    23.5     apply (erule asm_rl)
    23.6    apply (simp add: zmde ring_distribs)
    23.7 -  apply (simp add: push_mods)
    23.8    done
    23.9  
   23.10  (** Rep_Integ **)
    24.1 --- a/src/HOL/ex/coopertac.ML	Fri Jul 18 17:09:48 2008 +0200
    24.2 +++ b/src/HOL/ex/coopertac.ML	Fri Jul 18 18:25:53 2008 +0200
    24.3 @@ -10,33 +10,28 @@
    24.4  val binarith = @{thms normalize_bin_simps};
    24.5  val comp_arith = binarith @ simp_thms
    24.6  
    24.7 -val zdvd_int = thm "zdvd_int";
    24.8 -val zdiff_int_split = thm "zdiff_int_split";
    24.9 -val all_nat = thm "all_nat";
   24.10 -val ex_nat = thm "ex_nat";
   24.11 -val number_of1 = thm "number_of1";
   24.12 -val number_of2 = thm "number_of2";
   24.13 -val split_zdiv = thm "split_zdiv";
   24.14 -val split_zmod = thm "split_zmod";
   24.15 -val mod_div_equality' = thm "mod_div_equality'";
   24.16 -val split_div' = thm "split_div'";
   24.17 -val Suc_plus1 = thm "Suc_plus1";
   24.18 -val imp_le_cong = thm "imp_le_cong";
   24.19 -val conj_le_cong = thm "conj_le_cong";
   24.20 +val zdvd_int = @{thm zdvd_int};
   24.21 +val zdiff_int_split = @{thm zdiff_int_split};
   24.22 +val all_nat = @{thm all_nat};
   24.23 +val ex_nat = @{thm ex_nat};
   24.24 +val number_of1 = @{thm number_of1};
   24.25 +val number_of2 = @{thm number_of2};
   24.26 +val split_zdiv = @{thm split_zdiv};
   24.27 +val split_zmod = @{thm split_zmod};
   24.28 +val mod_div_equality' = @{thm mod_div_equality'};
   24.29 +val split_div' = @{thm split_div'};
   24.30 +val Suc_plus1 = @{thm Suc_plus1};
   24.31 +val imp_le_cong = @{thm imp_le_cong};
   24.32 +val conj_le_cong = @{thm conj_le_cong};
   24.33  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
   24.34  val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
   24.35  val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
   24.36 -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
   24.37 -val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
   24.38 -val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
   24.39 -val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
   24.40 -val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
   24.41 -val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
   24.42 -val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
   24.43 +val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
   24.44 +val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
   24.45 +val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
   24.46 +val nat_div_add_eq = @{thm div_add1_eq} RS sym;
   24.47 +val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
   24.48  
   24.49 -(*
   24.50 -val fn_rews = List.concat (map thms ["allpairs.simps","iupt.simps","decr.simps", "decrnum.simps","disjuncts.simps","simpnum.simps", "simpfm.simps","numadd.simps","nummul.simps","numneg_def","numsub","simp_num_pair_def","not.simps","prep.simps","qelim.simps","minusinf.simps","plusinf.simps","rsplit0.simps","rlfm.simps","\<Upsilon>.simps","\<upsilon>.simps","linrqe_def", "ferrack_def", "Let_def", "numsub_def", "numneg_def","DJ_def", "imp_def", "evaldjf_def", "djf_def", "split_def", "eq_def", "disj_def", "simp_num_pair_def", "conj_def", "lt_def", "neq_def","gt_def"]);
   24.51 -*)
   24.52  fun prepare_for_linz q fm = 
   24.53    let
   24.54      val ps = Logic.strip_params fm
   24.55 @@ -47,8 +42,7 @@
   24.56          (HOLogic.all_const T $ Abs (s, T, P), n)
   24.57        else (incr_boundvars ~1 P, n-1)
   24.58      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
   24.59 -      val rhs = hs
   24.60 -(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
   24.61 +    val rhs = hs
   24.62      val np = length ps
   24.63      val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   24.64        (foldr HOLogic.mk_imp c rhs, np) ps
   24.65 @@ -77,8 +71,7 @@
   24.66  				  int_mod_add_right_eq, int_mod_add_left_eq,
   24.67  				  nat_div_add_eq, int_div_add_eq,
   24.68  				  @{thm mod_self}, @{thm "zmod_self"},
   24.69 -				  @{thm DIVISION_BY_ZERO_MOD}, @{thm DIVISION_BY_ZERO_DIV},
   24.70 -				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
   24.71 +				  @{thm mod_by_0}, @{thm div_by_0},
   24.72  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
   24.73  				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
   24.74  				  Suc_plus1]
    25.1 --- a/src/HOL/int_factor_simprocs.ML	Fri Jul 18 17:09:48 2008 +0200
    25.2 +++ b/src/HOL/int_factor_simprocs.ML	Fri Jul 18 18:25:53 2008 +0200
    25.3 @@ -262,8 +262,8 @@
    25.4  structure IntDvdCancelFactor = ExtractCommonTermFun
    25.5   (open CancelFactorCommon
    25.6    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    25.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    25.8 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.intT
    25.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   25.10 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
   25.11    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
   25.12  );
   25.13  
    26.1 --- a/src/HOL/nat_simprocs.ML	Fri Jul 18 17:09:48 2008 +0200
    26.2 +++ b/src/HOL/nat_simprocs.ML	Fri Jul 18 18:25:53 2008 +0200
    26.3 @@ -294,8 +294,8 @@
    26.4  structure DvdCancelNumeralFactor = CancelNumeralFactorFun
    26.5   (open CancelNumeralFactorCommon
    26.6    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    26.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    26.8 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
    26.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   26.10 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   26.11    val cancel = @{thm nat_mult_dvd_cancel1} RS trans
   26.12    val neg_exchanges = false
   26.13  )
   26.14 @@ -414,8 +414,8 @@
   26.15  structure DvdCancelFactor = ExtractCommonTermFun
   26.16   (open CancelFactorCommon
   26.17    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   26.18 -  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
   26.19 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
   26.20 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   26.21 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   26.22    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
   26.23  );
   26.24