elementary definition of division on natural numbers
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 668081907167b6038
parent 66807 c3631f32dfeb
child 66809 f6a30d48aab0
elementary definition of division on natural numbers
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Parity.thy
src/HOL/Rings.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
     1.6    where "to_fract x = Fract x 1"
     1.7 -  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
     1.8 +  \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
     1.9  
    1.10  lemma to_fract_0 [simp]: "to_fract 0 = 0"
    1.11    by (simp add: to_fract_def eq_fract Zero_fract_def)
    1.12 @@ -438,8 +438,8 @@
    1.13      by (simp add: irreducible_dict)
    1.14    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
    1.15      by (simp add: prime_elem_dict)
    1.16 -  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
    1.17 -    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
    1.18 +  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
    1.19 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
    1.20      (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
    1.21    proof (standard, fold dvd_dict)
    1.22      fix p :: "'a poly"
     2.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -9,95 +9,6 @@
     2.4  imports Parity
     2.5  begin
     2.6  
     2.7 -subsection \<open>Parity\<close>
     2.8 -
     2.9 -class unique_euclidean_semiring_parity = unique_euclidean_semiring +
    2.10 -  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    2.11 -  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    2.12 -  assumes zero_not_eq_two: "0 \<noteq> 2"
    2.13 -begin
    2.14 -
    2.15 -lemma parity_cases [case_names even odd]:
    2.16 -  assumes "a mod 2 = 0 \<Longrightarrow> P"
    2.17 -  assumes "a mod 2 = 1 \<Longrightarrow> P"
    2.18 -  shows P
    2.19 -  using assms parity by blast
    2.20 -
    2.21 -lemma one_div_two_eq_zero [simp]:
    2.22 -  "1 div 2 = 0"
    2.23 -proof (cases "2 = 0")
    2.24 -  case True then show ?thesis by simp
    2.25 -next
    2.26 -  case False
    2.27 -  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
    2.28 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    2.29 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
    2.30 -  then have "1 div 2 = 0 \<or> 2 = 0" by simp
    2.31 -  with False show ?thesis by auto
    2.32 -qed
    2.33 -
    2.34 -lemma not_mod_2_eq_0_eq_1 [simp]:
    2.35 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    2.36 -  by (cases a rule: parity_cases) simp_all
    2.37 -
    2.38 -lemma not_mod_2_eq_1_eq_0 [simp]:
    2.39 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    2.40 -  by (cases a rule: parity_cases) simp_all
    2.41 -
    2.42 -subclass semiring_parity
    2.43 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    2.44 -  show "1 mod 2 = 1"
    2.45 -    by (fact one_mod_two_eq_one)
    2.46 -next
    2.47 -  fix a b
    2.48 -  assume "a mod 2 = 1"
    2.49 -  moreover assume "b mod 2 = 1"
    2.50 -  ultimately show "(a + b) mod 2 = 0"
    2.51 -    using mod_add_eq [of a 2 b] by simp
    2.52 -next
    2.53 -  fix a b
    2.54 -  assume "(a * b) mod 2 = 0"
    2.55 -  then have "(a mod 2) * (b mod 2) mod 2 = 0"
    2.56 -    by (simp add: mod_mult_eq)
    2.57 -  then have "(a mod 2) * (b mod 2) = 0"
    2.58 -    by (cases "a mod 2 = 0") simp_all
    2.59 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
    2.60 -    by (rule divisors_zero)
    2.61 -next
    2.62 -  fix a
    2.63 -  assume "a mod 2 = 1"
    2.64 -  then have "a = a div 2 * 2 + 1"
    2.65 -    using div_mult_mod_eq [of a 2] by simp
    2.66 -  then show "\<exists>b. a = b + 1" ..
    2.67 -qed
    2.68 -
    2.69 -lemma even_iff_mod_2_eq_zero:
    2.70 -  "even a \<longleftrightarrow> a mod 2 = 0"
    2.71 -  by (fact dvd_eq_mod_eq_0)
    2.72 -
    2.73 -lemma odd_iff_mod_2_eq_one:
    2.74 -  "odd a \<longleftrightarrow> a mod 2 = 1"
    2.75 -  by (simp add: even_iff_mod_2_eq_zero)
    2.76 -
    2.77 -lemma even_succ_div_two [simp]:
    2.78 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    2.79 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    2.80 -
    2.81 -lemma odd_succ_div_two [simp]:
    2.82 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    2.83 -  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    2.84 -
    2.85 -lemma even_two_times_div_two:
    2.86 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
    2.87 -  by (fact dvd_mult_div_cancel)
    2.88 -
    2.89 -lemma odd_two_times_div_two_succ [simp]:
    2.90 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    2.91 -  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    2.92 - 
    2.93 -end
    2.94 -
    2.95 -
    2.96  subsection \<open>Numeral division with a pragmatic type class\<close>
    2.97  
    2.98  text \<open>
    2.99 @@ -382,445 +293,11 @@
   2.100  
   2.101  end
   2.102  
   2.103 +hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
   2.104 +
   2.105  
   2.106  subsection \<open>Division on @{typ nat}\<close>
   2.107  
   2.108 -context
   2.109 -begin
   2.110 -
   2.111 -text \<open>
   2.112 -  We define @{const divide} and @{const modulo} on @{typ nat} by means
   2.113 -  of a characteristic relation with two input arguments
   2.114 -  @{term "m::nat"}, @{term "n::nat"} and two output arguments
   2.115 -  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
   2.116 -\<close>
   2.117 -
   2.118 -inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
   2.119 -  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
   2.120 -  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
   2.121 -
   2.122 -text \<open>@{const eucl_rel_nat} is total:\<close>
   2.123 -
   2.124 -qualified lemma eucl_rel_nat_ex:
   2.125 -  obtains q r where "eucl_rel_nat m n (q, r)"
   2.126 -proof (cases "n = 0")
   2.127 -  case True
   2.128 -  with that eucl_rel_nat_by0 show thesis
   2.129 -    by blast
   2.130 -next
   2.131 -  case False
   2.132 -  have "\<exists>q r. m = q * n + r \<and> r < n"
   2.133 -  proof (induct m)
   2.134 -    case 0 with \<open>n \<noteq> 0\<close>
   2.135 -    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
   2.136 -    then show ?case by blast
   2.137 -  next
   2.138 -    case (Suc m) then obtain q' r'
   2.139 -      where m: "m = q' * n + r'" and n: "r' < n" by auto
   2.140 -    then show ?case proof (cases "Suc r' < n")
   2.141 -      case True
   2.142 -      from m n have "Suc m = q' * n + Suc r'" by simp
   2.143 -      with True show ?thesis by blast
   2.144 -    next
   2.145 -      case False then have "n \<le> Suc r'"
   2.146 -        by (simp add: not_less)
   2.147 -      moreover from n have "Suc r' \<le> n"
   2.148 -        by (simp add: Suc_le_eq)
   2.149 -      ultimately have "n = Suc r'" by auto
   2.150 -      with m have "Suc m = Suc q' * n + 0" by simp
   2.151 -      with \<open>n \<noteq> 0\<close> show ?thesis by blast
   2.152 -    qed
   2.153 -  qed
   2.154 -  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
   2.155 -    by blast
   2.156 -qed
   2.157 -
   2.158 -text \<open>@{const eucl_rel_nat} is injective:\<close>
   2.159 -
   2.160 -qualified lemma eucl_rel_nat_unique_div:
   2.161 -  assumes "eucl_rel_nat m n (q, r)"
   2.162 -    and "eucl_rel_nat m n (q', r')"
   2.163 -  shows "q = q'"
   2.164 -proof (cases "n = 0")
   2.165 -  case True with assms show ?thesis
   2.166 -    by (auto elim: eucl_rel_nat.cases)
   2.167 -next
   2.168 -  case False
   2.169 -  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
   2.170 -  proof (rule ccontr)
   2.171 -    assume "\<not> q' \<le> q"
   2.172 -    then have "q < q'"
   2.173 -      by (simp add: not_le)
   2.174 -    with that show False
   2.175 -      by (auto simp add: less_iff_Suc_add algebra_simps)
   2.176 -  qed
   2.177 -  from \<open>n \<noteq> 0\<close> assms show ?thesis
   2.178 -    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
   2.179 -qed
   2.180 -
   2.181 -qualified lemma eucl_rel_nat_unique_mod:
   2.182 -  assumes "eucl_rel_nat m n (q, r)"
   2.183 -    and "eucl_rel_nat m n (q', r')"
   2.184 -  shows "r = r'"
   2.185 -proof -
   2.186 -  from assms have "q' = q"
   2.187 -    by (auto intro: eucl_rel_nat_unique_div)
   2.188 -  with assms show ?thesis
   2.189 -    by (auto elim!: eucl_rel_nat.cases)
   2.190 -qed
   2.191 -
   2.192 -text \<open>
   2.193 -  We instantiate divisibility on the natural numbers by
   2.194 -  means of @{const eucl_rel_nat}:
   2.195 -\<close>
   2.196 -
   2.197 -qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   2.198 -  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
   2.199 -
   2.200 -qualified lemma eucl_rel_nat_divmod_nat:
   2.201 -  "eucl_rel_nat m n (divmod_nat m n)"
   2.202 -proof -
   2.203 -  from eucl_rel_nat_ex
   2.204 -    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   2.205 -  then show ?thesis
   2.206 -    by (auto simp add: divmod_nat_def intro: theI
   2.207 -      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   2.208 -qed
   2.209 -
   2.210 -qualified lemma divmod_nat_unique:
   2.211 -  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
   2.212 -  using that
   2.213 -  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   2.214 -
   2.215 -qualified lemma divmod_nat_zero:
   2.216 -  "divmod_nat m 0 = (0, m)"
   2.217 -  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
   2.218 -
   2.219 -qualified lemma divmod_nat_zero_left:
   2.220 -  "divmod_nat 0 n = (0, 0)"
   2.221 -  by (rule divmod_nat_unique) 
   2.222 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   2.223 -
   2.224 -qualified lemma divmod_nat_base:
   2.225 -  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   2.226 -  by (rule divmod_nat_unique) 
   2.227 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   2.228 -
   2.229 -qualified lemma divmod_nat_step:
   2.230 -  assumes "0 < n" and "n \<le> m"
   2.231 -  shows "divmod_nat m n =
   2.232 -    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   2.233 -proof (rule divmod_nat_unique)
   2.234 -  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
   2.235 -    by (fact eucl_rel_nat_divmod_nat)
   2.236 -  then show "eucl_rel_nat m n (Suc
   2.237 -    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   2.238 -    using assms
   2.239 -      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
   2.240 -qed
   2.241 -
   2.242 -end
   2.243 -
   2.244 -instantiation nat :: "{semidom_modulo, normalization_semidom}"
   2.245 -begin
   2.246 -
   2.247 -definition normalize_nat :: "nat \<Rightarrow> nat"
   2.248 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   2.249 -
   2.250 -definition unit_factor_nat :: "nat \<Rightarrow> nat"
   2.251 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   2.252 -
   2.253 -lemma unit_factor_simps [simp]:
   2.254 -  "unit_factor 0 = (0::nat)"
   2.255 -  "unit_factor (Suc n) = 1"
   2.256 -  by (simp_all add: unit_factor_nat_def)
   2.257 -
   2.258 -definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.259 -  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   2.260 -
   2.261 -definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.262 -  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   2.263 -
   2.264 -lemma fst_divmod_nat [simp]:
   2.265 -  "fst (Divides.divmod_nat m n) = m div n"
   2.266 -  by (simp add: div_nat_def)
   2.267 -
   2.268 -lemma snd_divmod_nat [simp]:
   2.269 -  "snd (Divides.divmod_nat m n) = m mod n"
   2.270 -  by (simp add: mod_nat_def)
   2.271 -
   2.272 -lemma divmod_nat_div_mod:
   2.273 -  "Divides.divmod_nat m n = (m div n, m mod n)"
   2.274 -  by (simp add: prod_eq_iff)
   2.275 -
   2.276 -lemma div_nat_unique:
   2.277 -  assumes "eucl_rel_nat m n (q, r)"
   2.278 -  shows "m div n = q"
   2.279 -  using assms
   2.280 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.281 -
   2.282 -lemma mod_nat_unique:
   2.283 -  assumes "eucl_rel_nat m n (q, r)"
   2.284 -  shows "m mod n = r"
   2.285 -  using assms
   2.286 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.287 -
   2.288 -lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
   2.289 -  using Divides.eucl_rel_nat_divmod_nat
   2.290 -  by (simp add: divmod_nat_div_mod)
   2.291 -
   2.292 -text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   2.293 -
   2.294 -lemma div_less [simp]:
   2.295 -  fixes m n :: nat
   2.296 -  assumes "m < n"
   2.297 -  shows "m div n = 0"
   2.298 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   2.299 -
   2.300 -lemma le_div_geq:
   2.301 -  fixes m n :: nat
   2.302 -  assumes "0 < n" and "n \<le> m"
   2.303 -  shows "m div n = Suc ((m - n) div n)"
   2.304 -  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
   2.305 -
   2.306 -lemma mod_less [simp]:
   2.307 -  fixes m n :: nat
   2.308 -  assumes "m < n"
   2.309 -  shows "m mod n = m"
   2.310 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   2.311 -
   2.312 -lemma le_mod_geq:
   2.313 -  fixes m n :: nat
   2.314 -  assumes "n \<le> m"
   2.315 -  shows "m mod n = (m - n) mod n"
   2.316 -  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   2.317 -
   2.318 -lemma mod_less_divisor [simp]:
   2.319 -  fixes m n :: nat
   2.320 -  assumes "n > 0"
   2.321 -  shows "m mod n < n"
   2.322 -  using assms eucl_rel_nat [of m n]
   2.323 -    by (auto elim: eucl_rel_nat.cases)
   2.324 -
   2.325 -lemma mod_le_divisor [simp]:
   2.326 -  fixes m n :: nat
   2.327 -  assumes "n > 0"
   2.328 -  shows "m mod n \<le> n"
   2.329 -  using assms eucl_rel_nat [of m n]
   2.330 -    by (auto elim: eucl_rel_nat.cases)
   2.331 -
   2.332 -instance proof
   2.333 -  fix m n :: nat
   2.334 -  show "m div n * n + m mod n = m"
   2.335 -    using eucl_rel_nat [of m n]
   2.336 -    by (auto elim: eucl_rel_nat.cases)
   2.337 -next
   2.338 -  fix n :: nat show "n div 0 = 0"
   2.339 -    by (simp add: div_nat_def Divides.divmod_nat_zero)
   2.340 -next
   2.341 -  fix m n :: nat
   2.342 -  assume "n \<noteq> 0"
   2.343 -  then show "m * n div n = m"
   2.344 -    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
   2.345 -qed (simp_all add: unit_factor_nat_def)
   2.346 -
   2.347 -end
   2.348 -
   2.349 -text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   2.350 -
   2.351 -lemma (in semiring_modulo) cancel_div_mod_rules:
   2.352 -  "((a div b) * b + a mod b) + c = a + c"
   2.353 -  "(b * (a div b) + a mod b) + c = a + c"
   2.354 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
   2.355 -
   2.356 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
   2.357 -
   2.358 -ML \<open>
   2.359 -structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   2.360 -(
   2.361 -  val div_name = @{const_name divide};
   2.362 -  val mod_name = @{const_name modulo};
   2.363 -  val mk_binop = HOLogic.mk_binop;
   2.364 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   2.365 -  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   2.366 -  fun mk_sum [] = HOLogic.zero
   2.367 -    | mk_sum [t] = t
   2.368 -    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   2.369 -  fun dest_sum tm =
   2.370 -    if HOLogic.is_zero tm then []
   2.371 -    else
   2.372 -      (case try HOLogic.dest_Suc tm of
   2.373 -        SOME t => HOLogic.Suc_zero :: dest_sum t
   2.374 -      | NONE =>
   2.375 -          (case try dest_plus tm of
   2.376 -            SOME (t, u) => dest_sum t @ dest_sum u
   2.377 -          | NONE => [tm]));
   2.378 -
   2.379 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   2.380 -
   2.381 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   2.382 -    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   2.383 -)
   2.384 -\<close>
   2.385 -
   2.386 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   2.387 -  \<open>K Cancel_Div_Mod_Nat.proc\<close>
   2.388 -
   2.389 -lemma div_by_Suc_0 [simp]:
   2.390 -  "m div Suc 0 = m"
   2.391 -  using div_by_1 [of m] by simp
   2.392 -
   2.393 -lemma mod_by_Suc_0 [simp]:
   2.394 -  "m mod Suc 0 = 0"
   2.395 -  using mod_by_1 [of m] by simp
   2.396 -
   2.397 -lemma mod_greater_zero_iff_not_dvd:
   2.398 -  fixes m n :: nat
   2.399 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   2.400 -  by (simp add: dvd_eq_mod_eq_0)
   2.401 -
   2.402 -instantiation nat :: unique_euclidean_semiring
   2.403 -begin
   2.404 -
   2.405 -definition [simp]:
   2.406 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   2.407 -
   2.408 -definition [simp]:
   2.409 -  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   2.410 -
   2.411 -instance proof
   2.412 -  fix n q r :: nat
   2.413 -  assume "euclidean_size r < euclidean_size n"
   2.414 -  then have "n > r"
   2.415 -    by simp_all
   2.416 -  then have "eucl_rel_nat (q * n + r) n (q, r)"
   2.417 -    by (rule eucl_rel_natI) rule
   2.418 -  then show "(q * n + r) div n = q"
   2.419 -    by (rule div_nat_unique)
   2.420 -qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
   2.421 -
   2.422 -end
   2.423 -  
   2.424 -lemma divmod_nat_if [code]:
   2.425 -  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   2.426 -    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   2.427 -  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   2.428 -
   2.429 -lemma mod_Suc_eq [mod_simps]:
   2.430 -  "Suc (m mod n) mod n = Suc m mod n"
   2.431 -proof -
   2.432 -  have "(m mod n + 1) mod n = (m + 1) mod n"
   2.433 -    by (simp only: mod_simps)
   2.434 -  then show ?thesis
   2.435 -    by simp
   2.436 -qed
   2.437 -
   2.438 -lemma mod_Suc_Suc_eq [mod_simps]:
   2.439 -  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   2.440 -proof -
   2.441 -  have "(m mod n + 2) mod n = (m + 2) mod n"
   2.442 -    by (simp only: mod_simps)
   2.443 -  then show ?thesis
   2.444 -    by simp
   2.445 -qed
   2.446 -
   2.447 -
   2.448 -subsubsection \<open>Quotient\<close>
   2.449 -
   2.450 -lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
   2.451 -by (simp add: le_div_geq linorder_not_less)
   2.452 -
   2.453 -lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
   2.454 -by (simp add: div_geq)
   2.455 -
   2.456 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   2.457 -by simp
   2.458 -
   2.459 -lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   2.460 -by simp
   2.461 -
   2.462 -lemma div_positive:
   2.463 -  fixes m n :: nat
   2.464 -  assumes "n > 0"
   2.465 -  assumes "m \<ge> n"
   2.466 -  shows "m div n > 0"
   2.467 -proof -
   2.468 -  from \<open>m \<ge> n\<close> obtain q where "m = n + q"
   2.469 -    by (auto simp add: le_iff_add)
   2.470 -  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
   2.471 -qed
   2.472 -
   2.473 -lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
   2.474 -  by auto (metis div_positive less_numeral_extra(3) not_less)
   2.475 -
   2.476 -
   2.477 -subsubsection \<open>Remainder\<close>
   2.478 -
   2.479 -lemma mod_Suc_le_divisor [simp]:
   2.480 -  "m mod Suc n \<le> n"
   2.481 -  using mod_less_divisor [of "Suc n" m] by arith
   2.482 -
   2.483 -lemma mod_less_eq_dividend [simp]:
   2.484 -  fixes m n :: nat
   2.485 -  shows "m mod n \<le> m"
   2.486 -proof (rule add_leD2)
   2.487 -  from div_mult_mod_eq have "m div n * n + m mod n = m" .
   2.488 -  then show "m div n * n + m mod n \<le> m" by auto
   2.489 -qed
   2.490 -
   2.491 -lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
   2.492 -by (simp add: le_mod_geq linorder_not_less)
   2.493 -
   2.494 -lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
   2.495 -by (simp add: le_mod_geq)
   2.496 -
   2.497 -
   2.498 -subsubsection \<open>Quotient and Remainder\<close>
   2.499 -
   2.500 -lemma div_mult1_eq:
   2.501 -  "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   2.502 -  by (cases "c = 0")
   2.503 -     (auto simp add: algebra_simps distrib_left [symmetric]
   2.504 -     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
   2.505 -
   2.506 -lemma eucl_rel_nat_add1_eq:
   2.507 -  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
   2.508 -   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   2.509 -  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
   2.510 -
   2.511 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   2.512 -lemma div_add1_eq:
   2.513 -  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   2.514 -by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
   2.515 -
   2.516 -lemma eucl_rel_nat_mult2_eq:
   2.517 -  assumes "eucl_rel_nat a b (q, r)"
   2.518 -  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
   2.519 -proof (cases "c = 0")
   2.520 -  case True
   2.521 -  with assms show ?thesis
   2.522 -    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
   2.523 -next
   2.524 -  case False
   2.525 -  { assume "r < b"
   2.526 -    with False have "b * (q mod c) + r < b * c"
   2.527 -      apply (cut_tac m = q and n = c in mod_less_divisor)
   2.528 -      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   2.529 -      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
   2.530 -      apply (simp add: add_mult_distrib2)
   2.531 -      done
   2.532 -    then have "r + b * (q mod c) < b * c"
   2.533 -      by (simp add: ac_simps)
   2.534 -  } with assms False show ?thesis
   2.535 -    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
   2.536 -qed
   2.537 -
   2.538 -lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   2.539 -by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
   2.540 -
   2.541 -lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   2.542 -by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   2.543 -
   2.544  instantiation nat :: unique_euclidean_semiring_numeral
   2.545  begin
   2.546  
   2.547 @@ -834,370 +311,15 @@
   2.548      in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   2.549      else (2 * q, r))"
   2.550  
   2.551 -instance
   2.552 -  by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
   2.553 +instance by standard
   2.554 +  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
   2.555  
   2.556  end
   2.557  
   2.558  declare divmod_algorithm_code [where ?'a = nat, code]
   2.559 -  
   2.560  
   2.561 -subsubsection \<open>Further Facts about Quotient and Remainder\<close>
   2.562 -
   2.563 -lemma div_le_mono:
   2.564 -  fixes m n k :: nat
   2.565 -  assumes "m \<le> n"
   2.566 -  shows "m div k \<le> n div k"
   2.567 -proof -
   2.568 -  from assms obtain q where "n = m + q"
   2.569 -    by (auto simp add: le_iff_add)
   2.570 -  then show ?thesis
   2.571 -    by (simp add: div_add1_eq [of m q k])
   2.572 -qed
   2.573 -
   2.574 -(* Antimonotonicity of div in second argument *)
   2.575 -lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   2.576 -apply (subgoal_tac "0<n")
   2.577 - prefer 2 apply simp
   2.578 -apply (induct_tac k rule: nat_less_induct)
   2.579 -apply (rename_tac "k")
   2.580 -apply (case_tac "k<n", simp)
   2.581 -apply (subgoal_tac "~ (k<m) ")
   2.582 - prefer 2 apply simp
   2.583 -apply (simp add: div_geq)
   2.584 -apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   2.585 - prefer 2
   2.586 - apply (blast intro: div_le_mono diff_le_mono2)
   2.587 -apply (rule le_trans, simp)
   2.588 -apply (simp)
   2.589 -done
   2.590 -
   2.591 -lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
   2.592 -apply (case_tac "n=0", simp)
   2.593 -apply (subgoal_tac "m div n \<le> m div 1", simp)
   2.594 -apply (rule div_le_mono2)
   2.595 -apply (simp_all (no_asm_simp))
   2.596 -done
   2.597 -
   2.598 -(* Similar for "less than" *)
   2.599 -lemma div_less_dividend [simp]:
   2.600 -  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
   2.601 -apply (induct m rule: nat_less_induct)
   2.602 -apply (rename_tac "m")
   2.603 -apply (case_tac "m<n", simp)
   2.604 -apply (subgoal_tac "0<n")
   2.605 - prefer 2 apply simp
   2.606 -apply (simp add: div_geq)
   2.607 -apply (case_tac "n<m")
   2.608 - apply (subgoal_tac "(m-n) div n < (m-n) ")
   2.609 -  apply (rule impI less_trans_Suc)+
   2.610 -apply assumption
   2.611 -  apply (simp_all)
   2.612 -done
   2.613 -
   2.614 -text\<open>A fact for the mutilated chess board\<close>
   2.615 -lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   2.616 -apply (case_tac "n=0", simp)
   2.617 -apply (induct "m" rule: nat_less_induct)
   2.618 -apply (case_tac "Suc (na) <n")
   2.619 -(* case Suc(na) < n *)
   2.620 -apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   2.621 -(* case n \<le> Suc(na) *)
   2.622 -apply (simp add: linorder_not_less le_Suc_eq mod_geq)
   2.623 -apply (auto simp add: Suc_diff_le le_mod_geq)
   2.624 -done
   2.625 -
   2.626 -lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   2.627 -by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   2.628 -
   2.629 -lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
   2.630 -
   2.631 -(*Loses information, namely we also have r<d provided d is nonzero*)
   2.632 -lemma mod_eqD:
   2.633 -  fixes m d r q :: nat
   2.634 -  assumes "m mod d = r"
   2.635 -  shows "\<exists>q. m = r + q * d"
   2.636 -proof -
   2.637 -  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
   2.638 -  with assms have "m = r + q * d" by simp
   2.639 -  then show ?thesis ..
   2.640 -qed
   2.641 -
   2.642 -lemma split_div:
   2.643 - "P(n div k :: nat) =
   2.644 - ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
   2.645 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
   2.646 -proof
   2.647 -  assume P: ?P
   2.648 -  show ?Q
   2.649 -  proof (cases)
   2.650 -    assume "k = 0"
   2.651 -    with P show ?Q by simp
   2.652 -  next
   2.653 -    assume not0: "k \<noteq> 0"
   2.654 -    thus ?Q
   2.655 -    proof (simp, intro allI impI)
   2.656 -      fix i j
   2.657 -      assume n: "n = k*i + j" and j: "j < k"
   2.658 -      show "P i"
   2.659 -      proof (cases)
   2.660 -        assume "i = 0"
   2.661 -        with n j P show "P i" by simp
   2.662 -      next
   2.663 -        assume "i \<noteq> 0"
   2.664 -        with not0 n j P show "P i" by(simp add:ac_simps)
   2.665 -      qed
   2.666 -    qed
   2.667 -  qed
   2.668 -next
   2.669 -  assume Q: ?Q
   2.670 -  show ?P
   2.671 -  proof (cases)
   2.672 -    assume "k = 0"
   2.673 -    with Q show ?P by simp
   2.674 -  next
   2.675 -    assume not0: "k \<noteq> 0"
   2.676 -    with Q have R: ?R by simp
   2.677 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   2.678 -    show ?P by simp
   2.679 -  qed
   2.680 -qed
   2.681 -
   2.682 -lemma split_div_lemma:
   2.683 -  assumes "0 < n"
   2.684 -  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
   2.685 -proof
   2.686 -  assume ?rhs
   2.687 -  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
   2.688 -  then have A: "n * q \<le> m" by simp
   2.689 -  have "n - (m mod n) > 0" using mod_less_divisor assms by auto
   2.690 -  then have "m < m + (n - (m mod n))" by simp
   2.691 -  then have "m < n + (m - (m mod n))" by simp
   2.692 -  with nq have "m < n + n * q" by simp
   2.693 -  then have B: "m < n * Suc q" by simp
   2.694 -  from A B show ?lhs ..
   2.695 -next
   2.696 -  assume P: ?lhs
   2.697 -  then have "eucl_rel_nat m n (q, m - n * q)"
   2.698 -    by (auto intro: eucl_rel_natI simp add: ac_simps)
   2.699 -  then have "m div n = q"
   2.700 -    by (rule div_nat_unique)
   2.701 -  then show ?rhs by simp
   2.702 -qed
   2.703 -
   2.704 -theorem split_div':
   2.705 -  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   2.706 -   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   2.707 -  apply (cases "0 < n")
   2.708 -  apply (simp only: add: split_div_lemma)
   2.709 -  apply simp_all
   2.710 -  done
   2.711 -
   2.712 -lemma split_mod:
   2.713 - "P(n mod k :: nat) =
   2.714 - ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
   2.715 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
   2.716 -proof
   2.717 -  assume P: ?P
   2.718 -  show ?Q
   2.719 -  proof (cases)
   2.720 -    assume "k = 0"
   2.721 -    with P show ?Q by simp
   2.722 -  next
   2.723 -    assume not0: "k \<noteq> 0"
   2.724 -    thus ?Q
   2.725 -    proof (simp, intro allI impI)
   2.726 -      fix i j
   2.727 -      assume "n = k*i + j" "j < k"
   2.728 -      thus "P j" using not0 P by (simp add: ac_simps)
   2.729 -    qed
   2.730 -  qed
   2.731 -next
   2.732 -  assume Q: ?Q
   2.733 -  show ?P
   2.734 -  proof (cases)
   2.735 -    assume "k = 0"
   2.736 -    with Q show ?P by simp
   2.737 -  next
   2.738 -    assume not0: "k \<noteq> 0"
   2.739 -    with Q have R: ?R by simp
   2.740 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   2.741 -    show ?P by simp
   2.742 -  qed
   2.743 -qed
   2.744 -
   2.745 -lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
   2.746 -  apply rule
   2.747 -  apply (cases "b = 0")
   2.748 -  apply simp_all
   2.749 -  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
   2.750 -  done
   2.751 -
   2.752 -lemma (in field_char_0) of_nat_div:
   2.753 -  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
   2.754 -proof -
   2.755 -  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
   2.756 -    unfolding of_nat_add by (cases "n = 0") simp_all
   2.757 -  then show ?thesis
   2.758 -    by simp
   2.759 -qed
   2.760 -
   2.761 -
   2.762 -subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
   2.763 -
   2.764 -lemma mod_induct_0:
   2.765 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   2.766 -  and base: "P i" and i: "i<p"
   2.767 -  shows "P 0"
   2.768 -proof (rule ccontr)
   2.769 -  assume contra: "\<not>(P 0)"
   2.770 -  from i have p: "0<p" by simp
   2.771 -  have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
   2.772 -  proof
   2.773 -    fix k
   2.774 -    show "?A k"
   2.775 -    proof (induct k)
   2.776 -      show "?A 0" by simp  \<comment> "by contradiction"
   2.777 -    next
   2.778 -      fix n
   2.779 -      assume ih: "?A n"
   2.780 -      show "?A (Suc n)"
   2.781 -      proof (clarsimp)
   2.782 -        assume y: "P (p - Suc n)"
   2.783 -        have n: "Suc n < p"
   2.784 -        proof (rule ccontr)
   2.785 -          assume "\<not>(Suc n < p)"
   2.786 -          hence "p - Suc n = 0"
   2.787 -            by simp
   2.788 -          with y contra show "False"
   2.789 -            by simp
   2.790 -        qed
   2.791 -        hence n2: "Suc (p - Suc n) = p-n" by arith
   2.792 -        from p have "p - Suc n < p" by arith
   2.793 -        with y step have z: "P ((Suc (p - Suc n)) mod p)"
   2.794 -          by blast
   2.795 -        show "False"
   2.796 -        proof (cases "n=0")
   2.797 -          case True
   2.798 -          with z n2 contra show ?thesis by simp
   2.799 -        next
   2.800 -          case False
   2.801 -          with p have "p-n < p" by arith
   2.802 -          with z n2 False ih show ?thesis by simp
   2.803 -        qed
   2.804 -      qed
   2.805 -    qed
   2.806 -  qed
   2.807 -  moreover
   2.808 -  from i obtain k where "0<k \<and> i+k=p"
   2.809 -    by (blast dest: less_imp_add_positive)
   2.810 -  hence "0<k \<and> i=p-k" by auto
   2.811 -  moreover
   2.812 -  note base
   2.813 -  ultimately
   2.814 -  show "False" by blast
   2.815 -qed
   2.816 -
   2.817 -lemma mod_induct:
   2.818 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   2.819 -  and base: "P i" and i: "i<p" and j: "j<p"
   2.820 -  shows "P j"
   2.821 -proof -
   2.822 -  have "\<forall>j<p. P j"
   2.823 -  proof
   2.824 -    fix j
   2.825 -    show "j<p \<longrightarrow> P j" (is "?A j")
   2.826 -    proof (induct j)
   2.827 -      from step base i show "?A 0"
   2.828 -        by (auto elim: mod_induct_0)
   2.829 -    next
   2.830 -      fix k
   2.831 -      assume ih: "?A k"
   2.832 -      show "?A (Suc k)"
   2.833 -      proof
   2.834 -        assume suc: "Suc k < p"
   2.835 -        hence k: "k<p" by simp
   2.836 -        with ih have "P k" ..
   2.837 -        with step k have "P (Suc k mod p)"
   2.838 -          by blast
   2.839 -        moreover
   2.840 -        from suc have "Suc k mod p = Suc k"
   2.841 -          by simp
   2.842 -        ultimately
   2.843 -        show "P (Suc k)" by simp
   2.844 -      qed
   2.845 -    qed
   2.846 -  qed
   2.847 -  with j show ?thesis by blast
   2.848 -qed
   2.849 -
   2.850 -lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
   2.851 -  by (simp add: numeral_2_eq_2 le_div_geq)
   2.852 -
   2.853 -lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
   2.854 -  by (simp add: numeral_2_eq_2 le_mod_geq)
   2.855 -
   2.856 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   2.857 -by (simp add: mult_2 [symmetric])
   2.858 -
   2.859 -lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
   2.860 -proof -
   2.861 -  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
   2.862 -  moreover have "m mod 2 < 2" by simp
   2.863 -  ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
   2.864 -  then show ?thesis by auto
   2.865 -qed
   2.866 -
   2.867 -text\<open>These lemmas collapse some needless occurrences of Suc:
   2.868 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   2.869 -    We already have some rules to simplify operands smaller than 3.\<close>
   2.870 -
   2.871 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   2.872 -by (simp add: Suc3_eq_add_3)
   2.873 -
   2.874 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   2.875 -by (simp add: Suc3_eq_add_3)
   2.876 -
   2.877 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   2.878 -by (simp add: Suc3_eq_add_3)
   2.879 -
   2.880 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   2.881 -by (simp add: Suc3_eq_add_3)
   2.882 -
   2.883 -lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
   2.884 -lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   2.885 -
   2.886 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
   2.887 -apply (induct "m")
   2.888 -apply (simp_all add: mod_Suc)
   2.889 -done
   2.890 -
   2.891 -declare Suc_times_mod_eq [of "numeral w", simp] for w
   2.892 -
   2.893 -lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
   2.894 -by (simp add: div_le_mono)
   2.895 -
   2.896 -lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
   2.897 -by (cases n) simp_all
   2.898 -
   2.899 -lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
   2.900 -proof -
   2.901 -  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
   2.902 -  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
   2.903 -qed
   2.904 -
   2.905 -lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   2.906 -  using mod_mult_self3 [of k n "Suc m"] by simp
   2.907 -
   2.908 -lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
   2.909 -apply (subst mod_Suc [of m])
   2.910 -apply (subst mod_Suc [of "m mod n"], simp)
   2.911 -done
   2.912 -
   2.913 -lemma mod_2_not_eq_zero_eq_one_nat:
   2.914 -  fixes n :: nat
   2.915 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   2.916 -  by (fact not_mod_2_eq_0_eq_1)
   2.917 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   2.918 +  by (auto elim: oddE)
   2.919  
   2.920  lemma even_Suc_div_two [simp]:
   2.921    "even n \<Longrightarrow> Suc n div 2 = n div 2"
   2.922 @@ -1245,6 +367,11 @@
   2.923    qed
   2.924  qed
   2.925  
   2.926 +lemma mod_2_not_eq_zero_eq_one_nat:
   2.927 +  fixes n :: nat
   2.928 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   2.929 +  by (fact not_mod_2_eq_0_eq_1)
   2.930 +
   2.931  lemma Suc_0_div_numeral [simp]:
   2.932    fixes k l :: num
   2.933    shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   2.934 @@ -1255,6 +382,27 @@
   2.935    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   2.936    by (simp_all add: snd_divmod)
   2.937  
   2.938 +definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
   2.939 +  where "divmod_nat m n = (m div n, m mod n)"
   2.940 +
   2.941 +lemma fst_divmod_nat [simp]:
   2.942 +  "fst (divmod_nat m n) = m div n"
   2.943 +  by (simp add: divmod_nat_def)
   2.944 +
   2.945 +lemma snd_divmod_nat [simp]:
   2.946 +  "snd (divmod_nat m n) = m mod n"
   2.947 +  by (simp add: divmod_nat_def)
   2.948 +
   2.949 +lemma divmod_nat_if [code]:
   2.950 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   2.951 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   2.952 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   2.953 +
   2.954 +lemma [code]:
   2.955 +  "m div n = fst (divmod_nat m n)"
   2.956 +  "m mod n = snd (divmod_nat m n)"
   2.957 +  by simp_all
   2.958 +
   2.959  
   2.960  subsection \<open>Division on @{typ int}\<close>
   2.961  
   2.962 @@ -2225,7 +1373,7 @@
   2.963  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
   2.964  apply (subgoal_tac "nat x div nat k < nat x")
   2.965   apply (simp add: nat_div_distrib [symmetric])
   2.966 -apply (rule Divides.div_less_dividend, simp_all)
   2.967 +apply (rule div_less_dividend, simp_all)
   2.968  done
   2.969  
   2.970  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   2.971 @@ -2258,11 +1406,12 @@
   2.972    thus  ?lhs by simp
   2.973  qed
   2.974  
   2.975 +
   2.976  subsubsection \<open>Dedicated simproc for calculation\<close>
   2.977  
   2.978  text \<open>
   2.979    There is space for improvement here: the calculation itself
   2.980 -  could be carried outside the logic, and a generic simproc
   2.981 +  could be carried out outside the logic, and a generic simproc
   2.982    (simplifier setup) for generic calculation would be helpful. 
   2.983  \<close>
   2.984  
   2.985 @@ -2348,4 +1497,39 @@
   2.986  
   2.987  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
   2.988  
   2.989 +
   2.990 +subsubsection \<open>Lemmas of doubtful value\<close>
   2.991 +
   2.992 +lemma mod_mult_self3':
   2.993 +  "Suc (k * n + m) mod n = Suc m mod n"
   2.994 +  by (fact Suc_mod_mult_self3)
   2.995 +
   2.996 +lemma mod_Suc_eq_Suc_mod:
   2.997 +  "Suc m mod n = Suc (m mod n) mod n"
   2.998 +  by (simp add: mod_simps)
   2.999 +
  2.1000 +lemma div_geq:
  2.1001 +  "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
  2.1002 +  by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
  2.1003 +
  2.1004 +lemma mod_geq:
  2.1005 +  "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
  2.1006 +  by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
  2.1007 +
  2.1008 +lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  2.1009 +  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  2.1010 +
  2.1011 +lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  2.1012 +
  2.1013 +(*Loses information, namely we also have r<d provided d is nonzero*)
  2.1014 +lemma mod_eqD:
  2.1015 +  fixes m d r q :: nat
  2.1016 +  assumes "m mod d = r"
  2.1017 +  shows "\<exists>q. m = r + q * d"
  2.1018 +proof -
  2.1019 +  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  2.1020 +  with assms have "m = r + q * d" by simp
  2.1021 +  then show ?thesis ..
  2.1022 +qed
  2.1023 +
  2.1024  end
     3.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     3.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     3.3 @@ -6,9 +6,19 @@
     3.4  section \<open>Uniquely determined division in euclidean (semi)rings\<close>
     3.5  
     3.6  theory Euclidean_Division
     3.7 -  imports Nat_Transfer
     3.8 +  imports Nat_Transfer Lattices_Big
     3.9  begin
    3.10  
    3.11 +subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
    3.12 +
    3.13 +lemma (in semiring_modulo) cancel_div_mod_rules:
    3.14 +  "((a div b) * b + a mod b) + c = a + c"
    3.15 +  "(b * (a div b) + a mod b) + c = a + c"
    3.16 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    3.17 +
    3.18 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    3.19 +
    3.20 +
    3.21  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    3.22    
    3.23  class euclidean_semiring = semidom_modulo + normalization_semidom + 
    3.24 @@ -639,4 +649,657 @@
    3.25  
    3.26  end
    3.27  
    3.28 +
    3.29 +subsection \<open>Euclidean division on @{typ nat}\<close>
    3.30 +
    3.31 +instantiation nat :: unique_euclidean_semiring
    3.32 +begin
    3.33 +
    3.34 +definition normalize_nat :: "nat \<Rightarrow> nat"
    3.35 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
    3.36 +
    3.37 +definition unit_factor_nat :: "nat \<Rightarrow> nat"
    3.38 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
    3.39 +
    3.40 +lemma unit_factor_simps [simp]:
    3.41 +  "unit_factor 0 = (0::nat)"
    3.42 +  "unit_factor (Suc n) = 1"
    3.43 +  by (simp_all add: unit_factor_nat_def)
    3.44 +
    3.45 +definition euclidean_size_nat :: "nat \<Rightarrow> nat"
    3.46 +  where [simp]: "euclidean_size_nat = id"
    3.47 +
    3.48 +definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    3.49 +  where [simp]: "uniqueness_constraint_nat = \<top>"
    3.50 +
    3.51 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    3.52 +  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
    3.53 +
    3.54 +definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    3.55 +  where "m mod n = m - (m div n * (n::nat))"
    3.56 +
    3.57 +instance proof
    3.58 +  fix m n :: nat
    3.59 +  have ex: "\<exists>k. k * n \<le> l" for l :: nat
    3.60 +    by (rule exI [of _ 0]) simp
    3.61 +  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
    3.62 +  proof -
    3.63 +    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
    3.64 +      by (cases n) auto
    3.65 +    then show ?thesis
    3.66 +      by (rule finite_subset) simp
    3.67 +  qed
    3.68 +  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
    3.69 +  proof (cases "n = 0")
    3.70 +    case True
    3.71 +    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
    3.72 +      by auto
    3.73 +    ultimately show ?thesis
    3.74 +      by simp
    3.75 +  next
    3.76 +    case False
    3.77 +    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
    3.78 +      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
    3.79 +    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
    3.80 +      by (auto simp add: ac_simps elim!: dvdE)
    3.81 +    finally show ?thesis
    3.82 +      using False by (simp add: divide_nat_def ac_simps)
    3.83 +  qed
    3.84 +  show "n div 0 = 0"
    3.85 +    by (simp add: divide_nat_def)
    3.86 +  have less_eq: "m div n * n \<le> m"
    3.87 +    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
    3.88 +  then show "m div n * n + m mod n = m"
    3.89 +    by (simp add: modulo_nat_def)
    3.90 +  assume "n \<noteq> 0" 
    3.91 +  show "m * n div n = m"
    3.92 +    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
    3.93 +  show "euclidean_size (m mod n) < euclidean_size n"
    3.94 +  proof -
    3.95 +    have "m < Suc (m div n) * n"
    3.96 +    proof (rule ccontr)
    3.97 +      assume "\<not> m < Suc (m div n) * n"
    3.98 +      then have "Suc (m div n) * n \<le> m"
    3.99 +        by (simp add: not_less)
   3.100 +      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
   3.101 +        by (simp add: divide_nat_def)
   3.102 +      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
   3.103 +        by auto
   3.104 +      ultimately have "Suc (m div n) < Suc (m div n)"
   3.105 +        by blast
   3.106 +      then show False
   3.107 +        by simp
   3.108 +    qed
   3.109 +    with \<open>n \<noteq> 0\<close> show ?thesis
   3.110 +      by (simp add: modulo_nat_def)
   3.111 +  qed
   3.112 +  show "euclidean_size m \<le> euclidean_size (m * n)"
   3.113 +    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
   3.114 +  fix q r :: nat
   3.115 +  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
   3.116 +  proof -
   3.117 +    from that have "r < n"
   3.118 +      by simp
   3.119 +    have "k \<le> q" if "k * n \<le> q * n + r" for k
   3.120 +    proof (rule ccontr)
   3.121 +      assume "\<not> k \<le> q"
   3.122 +      then have "q < k"
   3.123 +        by simp
   3.124 +      then obtain l where "k = Suc (q + l)"
   3.125 +        by (auto simp add: less_iff_Suc_add)
   3.126 +      with \<open>r < n\<close> that show False
   3.127 +        by (simp add: algebra_simps)
   3.128 +    qed
   3.129 +    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
   3.130 +      by (auto simp add: divide_nat_def Max_eq_iff)
   3.131 +  qed
   3.132 +qed (simp_all add: unit_factor_nat_def)
   3.133 +
   3.134  end
   3.135 +
   3.136 +text \<open>Tool support\<close>
   3.137 +
   3.138 +ML \<open>
   3.139 +structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   3.140 +(
   3.141 +  val div_name = @{const_name divide};
   3.142 +  val mod_name = @{const_name modulo};
   3.143 +  val mk_binop = HOLogic.mk_binop;
   3.144 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   3.145 +  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   3.146 +  fun mk_sum [] = HOLogic.zero
   3.147 +    | mk_sum [t] = t
   3.148 +    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   3.149 +  fun dest_sum tm =
   3.150 +    if HOLogic.is_zero tm then []
   3.151 +    else
   3.152 +      (case try HOLogic.dest_Suc tm of
   3.153 +        SOME t => HOLogic.Suc_zero :: dest_sum t
   3.154 +      | NONE =>
   3.155 +          (case try dest_plus tm of
   3.156 +            SOME (t, u) => dest_sum t @ dest_sum u
   3.157 +          | NONE => [tm]));
   3.158 +
   3.159 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   3.160 +
   3.161 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   3.162 +    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   3.163 +)
   3.164 +\<close>
   3.165 +
   3.166 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   3.167 +  \<open>K Cancel_Div_Mod_Nat.proc\<close>
   3.168 +
   3.169 +lemma div_nat_eqI:
   3.170 +  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
   3.171 +  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   3.172 +
   3.173 +lemma mod_nat_eqI:
   3.174 +  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
   3.175 +  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   3.176 +
   3.177 +lemma div_mult_self_is_m [simp]:
   3.178 +  "m * n div n = m" if "n > 0" for m n :: nat
   3.179 +  using that by simp
   3.180 +
   3.181 +lemma div_mult_self1_is_m [simp]:
   3.182 +  "n * m div n = m" if "n > 0" for m n :: nat
   3.183 +  using that by simp
   3.184 +
   3.185 +lemma mod_less_divisor [simp]:
   3.186 +  "m mod n < n" if "n > 0" for m n :: nat
   3.187 +  using mod_size_less [of n m] that by simp
   3.188 +
   3.189 +lemma mod_le_divisor [simp]:
   3.190 +  "m mod n \<le> n" if "n > 0" for m n :: nat
   3.191 +  using that by (auto simp add: le_less)
   3.192 +
   3.193 +lemma div_times_less_eq_dividend [simp]:
   3.194 +  "m div n * n \<le> m" for m n :: nat
   3.195 +  by (simp add: minus_mod_eq_div_mult [symmetric])
   3.196 +
   3.197 +lemma times_div_less_eq_dividend [simp]:
   3.198 +  "n * (m div n) \<le> m" for m n :: nat
   3.199 +  using div_times_less_eq_dividend [of m n]
   3.200 +  by (simp add: ac_simps)
   3.201 +
   3.202 +lemma dividend_less_div_times:
   3.203 +  "m < n + (m div n) * n" if "0 < n" for m n :: nat
   3.204 +proof -
   3.205 +  from that have "m mod n < n"
   3.206 +    by simp
   3.207 +  then show ?thesis
   3.208 +    by (simp add: minus_mod_eq_div_mult [symmetric])
   3.209 +qed
   3.210 +
   3.211 +lemma dividend_less_times_div:
   3.212 +  "m < n + n * (m div n)" if "0 < n" for m n :: nat
   3.213 +  using dividend_less_div_times [of n m] that
   3.214 +  by (simp add: ac_simps)
   3.215 +
   3.216 +lemma mod_Suc_le_divisor [simp]:
   3.217 +  "m mod Suc n \<le> n"
   3.218 +  using mod_less_divisor [of "Suc n" m] by arith
   3.219 +
   3.220 +lemma mod_less_eq_dividend [simp]:
   3.221 +  "m mod n \<le> m" for m n :: nat
   3.222 +proof (rule add_leD2)
   3.223 +  from div_mult_mod_eq have "m div n * n + m mod n = m" .
   3.224 +  then show "m div n * n + m mod n \<le> m" by auto
   3.225 +qed
   3.226 +
   3.227 +lemma
   3.228 +  div_less [simp]: "m div n = 0"
   3.229 +  and mod_less [simp]: "m mod n = m"
   3.230 +  if "m < n" for m n :: nat
   3.231 +  using that by (auto intro: div_eqI mod_eqI) 
   3.232 +
   3.233 +lemma le_div_geq:
   3.234 +  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
   3.235 +proof -
   3.236 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
   3.237 +    by (auto simp add: le_iff_add)
   3.238 +  with \<open>0 < n\<close> show ?thesis
   3.239 +    by (simp add: div_add_self1)
   3.240 +qed
   3.241 +
   3.242 +lemma le_mod_geq:
   3.243 +  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
   3.244 +proof -
   3.245 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
   3.246 +    by (auto simp add: le_iff_add)
   3.247 +  then show ?thesis
   3.248 +    by simp
   3.249 +qed
   3.250 +
   3.251 +lemma div_if:
   3.252 +  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
   3.253 +  by (simp add: le_div_geq)
   3.254 +
   3.255 +lemma mod_if:
   3.256 +  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
   3.257 +  by (simp add: le_mod_geq)
   3.258 +
   3.259 +lemma div_eq_0_iff:
   3.260 +  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
   3.261 +  by (simp add: div_if)
   3.262 +
   3.263 +lemma div_greater_zero_iff:
   3.264 +  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
   3.265 +  using div_eq_0_iff [of m n] by auto
   3.266 +
   3.267 +lemma mod_greater_zero_iff_not_dvd:
   3.268 +  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
   3.269 +  by (simp add: dvd_eq_mod_eq_0)
   3.270 +
   3.271 +lemma div_by_Suc_0 [simp]:
   3.272 +  "m div Suc 0 = m"
   3.273 +  using div_by_1 [of m] by simp
   3.274 +
   3.275 +lemma mod_by_Suc_0 [simp]:
   3.276 +  "m mod Suc 0 = 0"
   3.277 +  using mod_by_1 [of m] by simp
   3.278 +
   3.279 +lemma div2_Suc_Suc [simp]:
   3.280 +  "Suc (Suc m) div 2 = Suc (m div 2)"
   3.281 +  by (simp add: numeral_2_eq_2 le_div_geq)
   3.282 +
   3.283 +lemma Suc_n_div_2_gt_zero [simp]:
   3.284 +  "0 < Suc n div 2" if "n > 0" for n :: nat
   3.285 +  using that by (cases n) simp_all
   3.286 +
   3.287 +lemma div_2_gt_zero [simp]:
   3.288 +  "0 < n div 2" if "Suc 0 < n" for n :: nat
   3.289 +  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
   3.290 +
   3.291 +lemma mod2_Suc_Suc [simp]:
   3.292 +  "Suc (Suc m) mod 2 = m mod 2"
   3.293 +  by (simp add: numeral_2_eq_2 le_mod_geq)
   3.294 +
   3.295 +lemma add_self_div_2 [simp]:
   3.296 +  "(m + m) div 2 = m" for m :: nat
   3.297 +  by (simp add: mult_2 [symmetric])
   3.298 +
   3.299 +lemma add_self_mod_2 [simp]:
   3.300 +  "(m + m) mod 2 = 0" for m :: nat
   3.301 +  by (simp add: mult_2 [symmetric])
   3.302 +
   3.303 +lemma mod2_gr_0 [simp]:
   3.304 +  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
   3.305 +proof -
   3.306 +  have "m mod 2 < 2"
   3.307 +    by (rule mod_less_divisor) simp
   3.308 +  then have "m mod 2 = 0 \<or> m mod 2 = 1"
   3.309 +    by arith
   3.310 +  then show ?thesis
   3.311 +    by auto     
   3.312 +qed
   3.313 +
   3.314 +lemma mod_Suc_eq [mod_simps]:
   3.315 +  "Suc (m mod n) mod n = Suc m mod n"
   3.316 +proof -
   3.317 +  have "(m mod n + 1) mod n = (m + 1) mod n"
   3.318 +    by (simp only: mod_simps)
   3.319 +  then show ?thesis
   3.320 +    by simp
   3.321 +qed
   3.322 +
   3.323 +lemma mod_Suc_Suc_eq [mod_simps]:
   3.324 +  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   3.325 +proof -
   3.326 +  have "(m mod n + 2) mod n = (m + 2) mod n"
   3.327 +    by (simp only: mod_simps)
   3.328 +  then show ?thesis
   3.329 +    by simp
   3.330 +qed
   3.331 +
   3.332 +lemma
   3.333 +  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
   3.334 +  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
   3.335 +  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   3.336 +  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
   3.337 +  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
   3.338 +
   3.339 +lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
   3.340 +  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
   3.341 +  apply (cases "c = 0")
   3.342 +   apply simp
   3.343 +  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
   3.344 +     apply (auto simp add: algebra_simps distrib_left [symmetric])
   3.345 +  done
   3.346 +
   3.347 +lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
   3.348 +   -- \<open>TODO: Generalization candidate\<close>
   3.349 +  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
   3.350 +  apply (cases "c = 0")
   3.351 +   apply simp
   3.352 +  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
   3.353 +  apply (auto simp add: algebra_simps)
   3.354 +  done
   3.355 +
   3.356 +context
   3.357 +  fixes m n q :: nat
   3.358 +begin
   3.359 +
   3.360 +private lemma eucl_rel_mult2:
   3.361 +  "m mod n + n * (m div n mod q) < n * q"
   3.362 +  if "n > 0" and "q > 0"
   3.363 +proof -
   3.364 +  from \<open>n > 0\<close> have "m mod n < n"
   3.365 +    by (rule mod_less_divisor)
   3.366 +  from \<open>q > 0\<close> have "m div n mod q < q"
   3.367 +    by (rule mod_less_divisor)
   3.368 +  then obtain s where "q = Suc (m div n mod q + s)"
   3.369 +    by (blast dest: less_imp_Suc_add)
   3.370 +  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
   3.371 +    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
   3.372 +  ultimately show ?thesis
   3.373 +    by simp
   3.374 +qed
   3.375 +
   3.376 +lemma div_mult2_eq:
   3.377 +  "m div (n * q) = (m div n) div q"
   3.378 +proof (cases "n = 0 \<or> q = 0")
   3.379 +  case True
   3.380 +  then show ?thesis
   3.381 +    by auto
   3.382 +next
   3.383 +  case False
   3.384 +  with eucl_rel_mult2 show ?thesis
   3.385 +    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
   3.386 +      simp add: algebra_simps add_mult_distrib2 [symmetric])
   3.387 +qed
   3.388 +
   3.389 +lemma mod_mult2_eq:
   3.390 +  "m mod (n * q) = n * (m div n mod q) + m mod n"
   3.391 +proof (cases "n = 0 \<or> q = 0")
   3.392 +  case True
   3.393 +  then show ?thesis
   3.394 +    by auto
   3.395 +next
   3.396 +  case False
   3.397 +  with eucl_rel_mult2 show ?thesis
   3.398 +    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
   3.399 +      simp add: algebra_simps add_mult_distrib2 [symmetric])
   3.400 +qed
   3.401 +
   3.402 +end
   3.403 +
   3.404 +lemma div_le_mono:
   3.405 +  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
   3.406 +proof -
   3.407 +  from that obtain q where "n = m + q"
   3.408 +    by (auto simp add: le_iff_add)
   3.409 +  then show ?thesis
   3.410 +    by (simp add: div_add1_eq [of m q k])
   3.411 +qed
   3.412 +
   3.413 +text \<open>Antimonotonicity of @{const divide} in second argument\<close>
   3.414 +
   3.415 +lemma div_le_mono2:
   3.416 +  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
   3.417 +using that proof (induct k arbitrary: m rule: less_induct)
   3.418 +  case (less k)
   3.419 +  show ?case
   3.420 +  proof (cases "n \<le> k")
   3.421 +    case False
   3.422 +    then show ?thesis
   3.423 +      by simp
   3.424 +  next
   3.425 +    case True
   3.426 +    have "(k - n) div n \<le> (k - m) div n"
   3.427 +      using less.prems
   3.428 +      by (blast intro: div_le_mono diff_le_mono2)
   3.429 +    also have "\<dots> \<le> (k - m) div m"
   3.430 +      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
   3.431 +      by simp
   3.432 +    finally show ?thesis
   3.433 +      using \<open>n \<le> k\<close> less.prems
   3.434 +      by (simp add: le_div_geq)
   3.435 +  qed
   3.436 +qed
   3.437 +
   3.438 +lemma div_le_dividend [simp]:
   3.439 +  "m div n \<le> m" for m n :: nat
   3.440 +  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
   3.441 +
   3.442 +lemma div_less_dividend [simp]:
   3.443 +  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
   3.444 +using that proof (induct m rule: less_induct)
   3.445 +  case (less m)
   3.446 +  show ?case
   3.447 +  proof (cases "n < m")
   3.448 +    case False
   3.449 +    with less show ?thesis
   3.450 +      by (cases "n = m") simp_all
   3.451 +  next
   3.452 +    case True
   3.453 +    then show ?thesis
   3.454 +      using less.hyps [of "m - n"] less.prems
   3.455 +      by (simp add: le_div_geq)
   3.456 +  qed
   3.457 +qed
   3.458 +
   3.459 +lemma div_eq_dividend_iff:
   3.460 +  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
   3.461 +proof
   3.462 +  assume "n = 1"
   3.463 +  then show "m div n = m"
   3.464 +    by simp
   3.465 +next
   3.466 +  assume P: "m div n = m"
   3.467 +  show "n = 1"
   3.468 +  proof (rule ccontr)
   3.469 +    have "n \<noteq> 0"
   3.470 +      by (rule ccontr) (use that P in auto)
   3.471 +    moreover assume "n \<noteq> 1"
   3.472 +    ultimately have "n > 1"
   3.473 +      by simp
   3.474 +    with that have "m div n < m"
   3.475 +      by simp
   3.476 +    with P show False
   3.477 +      by simp
   3.478 +  qed
   3.479 +qed
   3.480 +
   3.481 +lemma less_mult_imp_div_less:
   3.482 +  "m div n < i" if "m < i * n" for m n i :: nat
   3.483 +proof -
   3.484 +  from that have "i * n > 0"
   3.485 +    by (cases "i * n = 0") simp_all
   3.486 +  then have "i > 0" and "n > 0"
   3.487 +    by simp_all
   3.488 +  have "m div n * n \<le> m"
   3.489 +    by simp
   3.490 +  then have "m div n * n < i * n"
   3.491 +    using that by (rule le_less_trans)
   3.492 +  with \<open>n > 0\<close> show ?thesis
   3.493 +    by simp
   3.494 +qed
   3.495 +
   3.496 +text \<open>A fact for the mutilated chess board\<close>
   3.497 +
   3.498 +lemma mod_Suc:
   3.499 +  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
   3.500 +proof (cases "n = 0")
   3.501 +  case True
   3.502 +  then show ?thesis
   3.503 +    by simp
   3.504 +next
   3.505 +  case False
   3.506 +  have "Suc m mod n = Suc (m mod n) mod n"
   3.507 +    by (simp add: mod_simps)
   3.508 +  also have "\<dots> = ?rhs"
   3.509 +    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
   3.510 +  finally show ?thesis .
   3.511 +qed
   3.512 +
   3.513 +lemma Suc_times_mod_eq:
   3.514 +  "Suc (m * n) mod m = 1" if "Suc 0 < m"
   3.515 +  using that by (simp add: mod_Suc)
   3.516 +
   3.517 +lemma Suc_times_numeral_mod_eq [simp]:
   3.518 +  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
   3.519 +  by (rule Suc_times_mod_eq) (use that in simp)
   3.520 +
   3.521 +lemma Suc_div_le_mono [simp]:
   3.522 +  "m div n \<le> Suc m div n"
   3.523 +  by (simp add: div_le_mono)
   3.524 +
   3.525 +text \<open>These lemmas collapse some needless occurrences of Suc:
   3.526 +  at least three Sucs, since two and fewer are rewritten back to Suc again!
   3.527 +  We already have some rules to simplify operands smaller than 3.\<close>
   3.528 +
   3.529 +lemma div_Suc_eq_div_add3 [simp]:
   3.530 +  "m div Suc (Suc (Suc n)) = m div (3 + n)"
   3.531 +  by (simp add: Suc3_eq_add_3)
   3.532 +
   3.533 +lemma mod_Suc_eq_mod_add3 [simp]:
   3.534 +  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
   3.535 +  by (simp add: Suc3_eq_add_3)
   3.536 +
   3.537 +lemma Suc_div_eq_add3_div:
   3.538 +  "Suc (Suc (Suc m)) div n = (3 + m) div n"
   3.539 +  by (simp add: Suc3_eq_add_3)
   3.540 +
   3.541 +lemma Suc_mod_eq_add3_mod:
   3.542 +  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
   3.543 +  by (simp add: Suc3_eq_add_3)
   3.544 +
   3.545 +lemmas Suc_div_eq_add3_div_numeral [simp] =
   3.546 +  Suc_div_eq_add3_div [of _ "numeral v"] for v
   3.547 +
   3.548 +lemmas Suc_mod_eq_add3_mod_numeral [simp] =
   3.549 +  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   3.550 +
   3.551 +lemma (in field_char_0) of_nat_div:
   3.552 +  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
   3.553 +proof -
   3.554 +  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
   3.555 +    unfolding of_nat_add by (cases "n = 0") simp_all
   3.556 +  then show ?thesis
   3.557 +    by simp
   3.558 +qed
   3.559 +
   3.560 +text \<open>An ``induction'' law for modulus arithmetic.\<close>
   3.561 +
   3.562 +lemma mod_induct [consumes 3, case_names step]:
   3.563 +  "P m" if "P n" and "n < p" and "m < p"
   3.564 +    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
   3.565 +using \<open>m < p\<close> proof (induct m)
   3.566 +  case 0
   3.567 +  show ?case
   3.568 +  proof (rule ccontr)
   3.569 +    assume "\<not> P 0"
   3.570 +    from \<open>n < p\<close> have "0 < p"
   3.571 +      by simp
   3.572 +    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
   3.573 +      by (blast dest: less_imp_add_positive)
   3.574 +    with \<open>P n\<close> have "P (p - m)"
   3.575 +      by simp
   3.576 +    moreover have "\<not> P (p - m)"
   3.577 +    using \<open>0 < m\<close> proof (induct m)
   3.578 +      case 0
   3.579 +      then show ?case
   3.580 +        by simp
   3.581 +    next
   3.582 +      case (Suc m)
   3.583 +      show ?case
   3.584 +      proof
   3.585 +        assume P: "P (p - Suc m)"
   3.586 +        with \<open>\<not> P 0\<close> have "Suc m < p"
   3.587 +          by (auto intro: ccontr) 
   3.588 +        then have "Suc (p - Suc m) = p - m"
   3.589 +          by arith
   3.590 +        moreover from \<open>0 < p\<close> have "p - Suc m < p"
   3.591 +          by arith
   3.592 +        with P step have "P ((Suc (p - Suc m)) mod p)"
   3.593 +          by blast
   3.594 +        ultimately show False
   3.595 +          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
   3.596 +      qed
   3.597 +    qed
   3.598 +    ultimately show False
   3.599 +      by blast
   3.600 +  qed
   3.601 +next
   3.602 +  case (Suc m)
   3.603 +  then have "m < p" and mod: "Suc m mod p = Suc m"
   3.604 +    by simp_all
   3.605 +  from \<open>m < p\<close> have "P m"
   3.606 +    by (rule Suc.hyps)
   3.607 +  with \<open>m < p\<close> have "P (Suc m mod p)"
   3.608 +    by (rule step)
   3.609 +  with mod show ?case
   3.610 +    by simp
   3.611 +qed
   3.612 +
   3.613 +lemma split_div:
   3.614 +  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
   3.615 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
   3.616 +     (is "?P = ?Q") for m n :: nat
   3.617 +proof (cases "n = 0")
   3.618 +  case True
   3.619 +  then show ?thesis
   3.620 +    by simp
   3.621 +next
   3.622 +  case False
   3.623 +  show ?thesis
   3.624 +  proof
   3.625 +    assume ?P
   3.626 +    with False show ?Q
   3.627 +      by auto
   3.628 +  next
   3.629 +    assume ?Q
   3.630 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
   3.631 +      by simp
   3.632 +    with False show ?P
   3.633 +      by (auto intro: * [of "m mod n"])
   3.634 +  qed
   3.635 +qed
   3.636 +
   3.637 +lemma split_div':
   3.638 +  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
   3.639 +proof (cases "n = 0")
   3.640 +  case True
   3.641 +  then show ?thesis
   3.642 +    by simp
   3.643 +next
   3.644 +  case False
   3.645 +  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
   3.646 +    by (auto intro: div_nat_eqI dividend_less_times_div)
   3.647 +  then show ?thesis
   3.648 +    by auto
   3.649 +qed
   3.650 +
   3.651 +lemma split_mod:
   3.652 +  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
   3.653 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
   3.654 +     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
   3.655 +proof (cases "n = 0")
   3.656 +  case True
   3.657 +  then show ?thesis
   3.658 +    by simp
   3.659 +next
   3.660 +  case False
   3.661 +  show ?thesis
   3.662 +  proof
   3.663 +    assume ?P
   3.664 +    with False show ?Q
   3.665 +      by auto
   3.666 +  next
   3.667 +    assume ?Q
   3.668 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
   3.669 +      by simp
   3.670 +    with False show ?P
   3.671 +      by (auto intro: * [of _ "m div n"])
   3.672 +  qed
   3.673 +qed
   3.674 +
   3.675 +
   3.676 +subsection \<open>Code generation\<close>
   3.677 +
   3.678 +code_identifier
   3.679 +  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   3.680 +
   3.681 +end
     4.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     4.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     4.3 @@ -95,7 +95,7 @@
     4.4  
     4.5  lemma [code]:
     4.6    "Divides.divmod_nat m n = (m div n, m mod n)"
     4.7 -  by (fact divmod_nat_div_mod)
     4.8 +  by (fact divmod_nat_def)
     4.9  
    4.10  lemma [code]:
    4.11    "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
    4.12 @@ -130,7 +130,7 @@
    4.13  proof -
    4.14    from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
    4.15    show ?thesis
    4.16 -    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
    4.17 +    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
    4.18        (simp add: * mult.commute of_nat_mult add.commute)
    4.19  qed
    4.20  
     5.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
     5.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
     5.3 @@ -1169,7 +1169,7 @@
     5.4            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
     5.5        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
     5.6            apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
     5.7 -by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
     5.8 +by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
     5.9  
    5.10  lemma rbtreeify_g_code [code]:
    5.11    "rbtreeify_g n kvs =
    5.12 @@ -1180,7 +1180,7 @@
    5.13            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
    5.14        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    5.15            apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
    5.16 -by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
    5.17 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
    5.18  
    5.19  lemma Suc_double_half: "Suc (2 * n) div 2 = n"
    5.20  by simp
     6.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
     6.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
     6.3 @@ -101,6 +101,92 @@
     6.4  
     6.5  end
     6.6  
     6.7 +class unique_euclidean_semiring_parity = unique_euclidean_semiring +
     6.8 +  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     6.9 +  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    6.10 +  assumes zero_not_eq_two: "0 \<noteq> 2"
    6.11 +begin
    6.12 +
    6.13 +lemma parity_cases [case_names even odd]:
    6.14 +  assumes "a mod 2 = 0 \<Longrightarrow> P"
    6.15 +  assumes "a mod 2 = 1 \<Longrightarrow> P"
    6.16 +  shows P
    6.17 +  using assms parity by blast
    6.18 +
    6.19 +lemma one_div_two_eq_zero [simp]:
    6.20 +  "1 div 2 = 0"
    6.21 +proof (cases "2 = 0")
    6.22 +  case True then show ?thesis by simp
    6.23 +next
    6.24 +  case False
    6.25 +  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
    6.26 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    6.27 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
    6.28 +  then have "1 div 2 = 0 \<or> 2 = 0" by simp
    6.29 +  with False show ?thesis by auto
    6.30 +qed
    6.31 +
    6.32 +lemma not_mod_2_eq_0_eq_1 [simp]:
    6.33 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    6.34 +  by (cases a rule: parity_cases) simp_all
    6.35 +
    6.36 +lemma not_mod_2_eq_1_eq_0 [simp]:
    6.37 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    6.38 +  by (cases a rule: parity_cases) simp_all
    6.39 +
    6.40 +subclass semiring_parity
    6.41 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    6.42 +  show "1 mod 2 = 1"
    6.43 +    by (fact one_mod_two_eq_one)
    6.44 +next
    6.45 +  fix a b
    6.46 +  assume "a mod 2 = 1"
    6.47 +  moreover assume "b mod 2 = 1"
    6.48 +  ultimately show "(a + b) mod 2 = 0"
    6.49 +    using mod_add_eq [of a 2 b] by simp
    6.50 +next
    6.51 +  fix a b
    6.52 +  assume "(a * b) mod 2 = 0"
    6.53 +  then have "(a mod 2) * (b mod 2) mod 2 = 0"
    6.54 +    by (simp add: mod_mult_eq)
    6.55 +  then have "(a mod 2) * (b mod 2) = 0"
    6.56 +    by (cases "a mod 2 = 0") simp_all
    6.57 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
    6.58 +    by (rule divisors_zero)
    6.59 +next
    6.60 +  fix a
    6.61 +  assume "a mod 2 = 1"
    6.62 +  then have "a = a div 2 * 2 + 1"
    6.63 +    using div_mult_mod_eq [of a 2] by simp
    6.64 +  then show "\<exists>b. a = b + 1" ..
    6.65 +qed
    6.66 +
    6.67 +lemma even_iff_mod_2_eq_zero:
    6.68 +  "even a \<longleftrightarrow> a mod 2 = 0"
    6.69 +  by (fact dvd_eq_mod_eq_0)
    6.70 +
    6.71 +lemma odd_iff_mod_2_eq_one:
    6.72 +  "odd a \<longleftrightarrow> a mod 2 = 1"
    6.73 +  by (simp add: even_iff_mod_2_eq_zero)
    6.74 +
    6.75 +lemma even_succ_div_two [simp]:
    6.76 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    6.77 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    6.78 +
    6.79 +lemma odd_succ_div_two [simp]:
    6.80 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    6.81 +  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    6.82 +
    6.83 +lemma even_two_times_div_two:
    6.84 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
    6.85 +  by (fact dvd_mult_div_cancel)
    6.86 +
    6.87 +lemma odd_two_times_div_two_succ [simp]:
    6.88 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    6.89 +  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    6.90 + 
    6.91 +end
    6.92 +
    6.93  
    6.94  subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
    6.95  
    6.96 @@ -190,9 +276,6 @@
    6.97    for k l :: int
    6.98    using even_abs_add_iff [of l k] by (simp add: ac_simps)
    6.99  
   6.100 -lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   6.101 -  by (auto elim: oddE)
   6.102 -
   6.103  instance int :: ring_parity
   6.104  proof
   6.105    show "\<not> 2 dvd (1 :: int)"
     7.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     7.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     7.3 @@ -1620,6 +1620,10 @@
     7.4    shows "c dvd a"
     7.5    using assms dvd_mod_iff [of c b a] by simp
     7.6  
     7.7 +lemma dvd_minus_mod [simp]:
     7.8 +  "b dvd a - a mod b"
     7.9 +  by (simp add: minus_mod_eq_div_mult)
    7.10 +
    7.11  end
    7.12  
    7.13  class idom_modulo = idom + semidom_modulo
     8.1 --- a/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
     8.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
     8.3 @@ -2024,7 +2024,7 @@
     8.4  
     8.5  lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
     8.6  
     8.7 -lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
     8.8 +lemmas thd = times_div_less_eq_dividend
     8.9  
    8.10  lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
    8.11  
    8.12 @@ -3724,7 +3724,7 @@
    8.13  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
    8.14  
    8.15  (* alternative proof of word_rcat_rsplit *)
    8.16 -lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
    8.17 +lemmas tdle = times_div_less_eq_dividend
    8.18  lemmas dtle = xtr4 [OF tdle mult.commute]
    8.19  
    8.20  lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
    8.21 @@ -3734,7 +3734,7 @@
    8.22      apply (simp_all add: word_size
    8.23        refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
    8.24     apply safe
    8.25 -   apply (erule xtr7, rule len_gt_0 [THEN dtle])+
    8.26 +   apply (erule xtr7, rule dtle)+
    8.27    done
    8.28  
    8.29  lemma size_word_rsplit_rcat_size:
     9.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
     9.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
     9.3 @@ -304,8 +304,8 @@
     9.4  lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
     9.5  
     9.6  lemmas dme = div_mult_mod_eq
     9.7 -lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
     9.8 -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
     9.9 +lemmas dtle = div_times_less_eq_dividend
    9.10 +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
    9.11  
    9.12  lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
    9.13    for a b c :: nat
    9.14 @@ -316,15 +316,13 @@
    9.15  
    9.16  lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
    9.17  
    9.18 -lemma div_mult_le: "a div b * b \<le> a"
    9.19 -  for a b :: nat
    9.20 -  by (fact dtle)
    9.21 +lemmas div_mult_le = div_times_less_eq_dividend 
    9.22  
    9.23 -lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
    9.24 +lemmas sdl = div_nat_eqI
    9.25  
    9.26  lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
    9.27    for f l :: nat
    9.28 -  by (rule sdl, assumption) (simp (no_asm))
    9.29 +  by (rule div_nat_eqI) (simp_all)
    9.30  
    9.31  lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
    9.32    for f l :: nat