using only an relation predicate to construct div and mod
authorhaftmann
Wed Feb 20 14:52:34 2008 +0100 (2008-02-20)
changeset 26100fbc60cd02ae2
parent 26099 e0f3200e5b96
child 26101 a657683e902a
using only an relation predicate to construct div and mod
src/HOL/Divides.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 20 14:35:55 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 20 14:52:34 2008 +0100
     1.3 @@ -4,10 +4,10 @@
     1.4      Copyright   1999  University of Cambridge
     1.5  *)
     1.6  
     1.7 -header {* The division operators div, mod and the divides relation "dvd" *}
     1.8 +header {* The division operators div,  mod and the divides relation dvd *}
     1.9  
    1.10  theory Divides
    1.11 -imports Power Wellfounded_Recursion
    1.12 +imports Nat Power Product_Type Wellfounded_Recursion
    1.13  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.14  begin
    1.15  
    1.16 @@ -33,6 +33,8 @@
    1.17      and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.18  begin
    1.19  
    1.20 +text {* @{const div} and @{const mod} *}
    1.21 +
    1.22  lemma div_by_1: "a div 1 = a"
    1.23    using mult_div [of 1 a] zero_neq_one by simp
    1.24  
    1.25 @@ -83,6 +85,8 @@
    1.26  lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
    1.27    by (simp add: mod_div_equality2)
    1.28  
    1.29 +text {* The @{const dvd} relation *}
    1.30 +
    1.31  lemma dvdI [intro?]: "a = b * c \<Longrightarrow> b dvd a"
    1.32    unfolding dvd_def ..
    1.33  
    1.34 @@ -158,72 +162,200 @@
    1.35  end
    1.36  
    1.37  
    1.38 -subsection {* Division on the natural numbers *}
    1.39 +subsection {* Division on @{typ nat} *}
    1.40 +
    1.41 +text {*
    1.42 +  We define @{const div} and @{const mod} on @{typ nat} by means
    1.43 +  of a characteristic relation with two input arguments
    1.44 +  @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
    1.45 +  @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
    1.46 +*}
    1.47 +
    1.48 +definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.49 +  "divmod_rel m n q r \<longleftrightarrow> m = q * n + r \<and> (if n > 0 then 0 \<le> r \<and> r < n else q = 0)"
    1.50 +
    1.51 +text {* @{const divmod_rel} is total: *}
    1.52 +
    1.53 +lemma divmod_rel_ex:
    1.54 +  obtains q r where "divmod_rel m n q r"
    1.55 +proof (cases "n = 0")
    1.56 +  case True with that show thesis
    1.57 +    by (auto simp add: divmod_rel_def)
    1.58 +next
    1.59 +  case False
    1.60 +  have "\<exists>q r. m = q * n + r \<and> r < n"
    1.61 +  proof (induct m)
    1.62 +    case 0 with `n \<noteq> 0`
    1.63 +    have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp
    1.64 +    then show ?case by blast
    1.65 +  next
    1.66 +    case (Suc m) then obtain q' r'
    1.67 +      where m: "m = q' * n + r'" and n: "r' < n" by auto
    1.68 +    then show ?case proof (cases "Suc r' < n")
    1.69 +      case True
    1.70 +      from m n have "Suc m = q' * n + Suc r'" by simp
    1.71 +      with True show ?thesis by blast
    1.72 +    next
    1.73 +      case False then have "n \<le> Suc r'" by auto
    1.74 +      moreover from n have "Suc r' \<le> n" by auto
    1.75 +      ultimately have "n = Suc r'" by auto
    1.76 +      with m have "Suc m = Suc q' * n + 0" by simp
    1.77 +      with `n \<noteq> 0` show ?thesis by blast
    1.78 +    qed
    1.79 +  qed
    1.80 +  with that show thesis
    1.81 +    using `n \<noteq> 0` by (auto simp add: divmod_rel_def)
    1.82 +qed
    1.83 +
    1.84 +text {* @{const divmod_rel} is injective: *}
    1.85 +
    1.86 +lemma divmod_rel_unique_div:
    1.87 +  assumes "divmod_rel m n q r"
    1.88 +    and "divmod_rel m n q' r'"
    1.89 +  shows "q = q'"
    1.90 +proof (cases "n = 0")
    1.91 +  case True with assms show ?thesis
    1.92 +    by (simp add: divmod_rel_def)
    1.93 +next
    1.94 +  case False
    1.95 +  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
    1.96 +  apply (rule leI)
    1.97 +  apply (subst less_iff_Suc_add)
    1.98 +  apply (auto simp add: add_mult_distrib)
    1.99 +  done
   1.100 +  from `n \<noteq> 0` assms show ?thesis
   1.101 +    by (auto simp add: divmod_rel_def
   1.102 +      intro: order_antisym dest: aux sym)
   1.103 +qed
   1.104 +
   1.105 +lemma divmod_rel_unique_mod:
   1.106 +  assumes "divmod_rel m n q r"
   1.107 +    and "divmod_rel m n q' r'"
   1.108 +  shows "r = r'"
   1.109 +proof -
   1.110 +  from assms have "q = q'" by (rule divmod_rel_unique_div)
   1.111 +  with assms show ?thesis by (simp add: divmod_rel_def)
   1.112 +qed
   1.113 +
   1.114 +text {*
   1.115 +  We instantiate divisibility on the natural numbers by
   1.116 +  means of @{const divmod_rel}:
   1.117 +*}
   1.118  
   1.119  instantiation nat :: semiring_div
   1.120  begin
   1.121  
   1.122 -definition
   1.123 -  div_def: "m div n == wfrec (pred_nat^+)
   1.124 -                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
   1.125 +definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   1.126 +  [code func del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
   1.127 +
   1.128 +definition div_nat where
   1.129 +  "m div n = fst (divmod m n)"
   1.130 +
   1.131 +definition mod_nat where
   1.132 +  "m mod n = snd (divmod m n)"
   1.133  
   1.134 -lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
   1.135 -               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
   1.136 -by (simp add: div_def)
   1.137 +lemma divmod_div_mod:
   1.138 +  "divmod m n = (m div n, m mod n)"
   1.139 +  unfolding div_nat_def mod_nat_def by simp
   1.140 +
   1.141 +lemma divmod_eq:
   1.142 +  assumes "divmod_rel m n q r" 
   1.143 +  shows "divmod m n = (q, r)"
   1.144 +  using assms by (auto simp add: divmod_def
   1.145 +    dest: divmod_rel_unique_div divmod_rel_unique_mod)
   1.146  
   1.147 -definition
   1.148 -  mod_def: "m mod n == wfrec (pred_nat^+)
   1.149 -                          (%f j. if j<n | n=0 then j else f (j-n)) m"
   1.150 +lemma div_eq:
   1.151 +  assumes "divmod_rel m n q r" 
   1.152 +  shows "m div n = q"
   1.153 +  using assms by (auto dest: divmod_eq simp add: div_nat_def)
   1.154 +
   1.155 +lemma mod_eq:
   1.156 +  assumes "divmod_rel m n q r" 
   1.157 +  shows "m mod n = r"
   1.158 +  using assms by (auto dest: divmod_eq simp add: mod_nat_def)
   1.159  
   1.160 -lemma mod_eq: "(%m. m mod n) =
   1.161 -              wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
   1.162 -by (simp add: mod_def)
   1.163 +lemma divmod_rel: "divmod_rel m n (m div n) (m mod n)"
   1.164 +proof -
   1.165 +  from divmod_rel_ex
   1.166 +    obtain q r where rel: "divmod_rel m n q r" .
   1.167 +  moreover with div_eq mod_eq have "m div n = q" and "m mod n = r"
   1.168 +    by simp_all
   1.169 +  ultimately show ?thesis by simp
   1.170 +qed
   1.171  
   1.172 -lemmas wf_less_trans = def_wfrec [THEN trans,
   1.173 -  OF eq_reflection wf_pred_nat [THEN wf_trancl], standard]
   1.174 +lemma divmod_zero:
   1.175 +  "divmod m 0 = (0, m)"
   1.176 +proof -
   1.177 +  from divmod_rel [of m 0] show ?thesis
   1.178 +    unfolding divmod_div_mod divmod_rel_def by simp
   1.179 +qed
   1.180  
   1.181 -lemma div_less [simp]: "m < n \<Longrightarrow> m div n = (0\<Colon>nat)"
   1.182 -  by (rule div_eq [THEN wf_less_trans]) simp
   1.183 +lemma divmod_base:
   1.184 +  assumes "m < n"
   1.185 +  shows "divmod m n = (0, m)"
   1.186 +proof -
   1.187 +  from divmod_rel [of m n] show ?thesis
   1.188 +    unfolding divmod_div_mod divmod_rel_def
   1.189 +    using assms by (cases "m div n = 0")
   1.190 +      (auto simp add: gr0_conv_Suc [of "m div n"])
   1.191 +qed
   1.192  
   1.193 -lemma le_div_geq: "0 < n \<Longrightarrow> n \<le> m \<Longrightarrow> m div n = Suc ((m - n) div n)"
   1.194 -  by (rule div_eq [THEN wf_less_trans]) (simp add: cut_apply less_eq)
   1.195 -
   1.196 -lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a\<Colon>nat)"
   1.197 -  by (rule mod_eq [THEN wf_less_trans]) simp
   1.198 +lemma divmod_step:
   1.199 +  assumes "0 < n" and "n \<le> m"
   1.200 +  shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
   1.201 +proof -
   1.202 +  from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
   1.203 +  with assms have m_div_n: "m div n \<ge> 1"
   1.204 +    by (cases "m div n") (auto simp add: divmod_rel_def)
   1.205 +  from assms divmod_m_n have "divmod_rel (m - n) n (m div n - 1) (m mod n)"
   1.206 +    by (cases "m div n") (auto simp add: divmod_rel_def)
   1.207 +  with divmod_eq have "divmod (m - n) n = (m div n - 1, m mod n)" by simp
   1.208 +  moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
   1.209 +  ultimately have "m div n = Suc ((m - n) div n)"
   1.210 +    and "m mod n = (m - n) mod n" using m_div_n by simp_all
   1.211 +  then show ?thesis using divmod_div_mod by simp
   1.212 +qed
   1.213  
   1.214 -lemma mod_less [simp]: "m < n \<Longrightarrow> m mod n = (m\<Colon>nat)"
   1.215 -  by (rule mod_eq [THEN wf_less_trans]) simp
   1.216 +text {* The ''recursion┬┤┬┤ equations for @{const div} and @{const mod} *}
   1.217 +
   1.218 +lemma div_less [simp]:
   1.219 +  fixes m n :: nat
   1.220 +  assumes "m < n"
   1.221 +  shows "m div n = 0"
   1.222 +  using assms divmod_base divmod_div_mod by simp
   1.223  
   1.224 -lemma le_mod_geq: "(n\<Colon>nat) \<le> m \<Longrightarrow> m mod n = (m - n) mod n"
   1.225 -  by (cases "n = 0", simp, rule mod_eq [THEN wf_less_trans])
   1.226 -    (simp add: cut_apply less_eq)
   1.227 +lemma le_div_geq:
   1.228 +  fixes m n :: nat
   1.229 +  assumes "0 < n" and "n \<le> m"
   1.230 +  shows "m div n = Suc ((m - n) div n)"
   1.231 +  using assms divmod_step divmod_div_mod by simp
   1.232  
   1.233 -lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
   1.234 -  by (simp add: le_mod_geq)
   1.235 +lemma mod_less [simp]:
   1.236 +  fixes m n :: nat
   1.237 +  assumes "m < n"
   1.238 +  shows "m mod n = m"
   1.239 +  using assms divmod_base divmod_div_mod by simp
   1.240 +
   1.241 +lemma le_mod_geq:
   1.242 +  fixes m n :: nat
   1.243 +  assumes "n \<le> m"
   1.244 +  shows "m mod n = (m - n) mod n"
   1.245 +  using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
   1.246  
   1.247  instance proof
   1.248 -  fix n m :: nat
   1.249 -  show "(m div n) * n + m mod n = m"
   1.250 -    apply (cases "n = 0", simp)
   1.251 -    apply (induct m rule: less_induct)
   1.252 -    apply (subst mod_if)
   1.253 -    apply (simp add: add_assoc add_diff_inverse le_div_geq)
   1.254 -    done
   1.255 +  fix m n :: nat show "m div n * n + m mod n = m"
   1.256 +    using divmod_rel [of m n] by (simp add: divmod_rel_def)
   1.257  next
   1.258 -  fix n :: nat
   1.259 -  show "n div 0 = 0"
   1.260 -    by (rule div_eq [THEN wf_less_trans]) simp
   1.261 +  fix n :: nat show "n div 0 = 0"
   1.262 +    using divmod_zero divmod_div_mod [of n 0] by simp
   1.263  next
   1.264 -  fix n m :: nat
   1.265 -  assume "n \<noteq> 0"
   1.266 -  then show "m * n div n = m"
   1.267 +  fix m n :: nat assume "n \<noteq> 0" then show "m * n div n = m"
   1.268      by (induct m) (simp_all add: le_div_geq)
   1.269  qed
   1.270 -  
   1.271 +
   1.272  end
   1.273  
   1.274 -
   1.275 -subsubsection{*Simproc for Cancelling Div and Mod*}
   1.276 +text {* Simproc for cancelling @{const div} and @{const mod} *}
   1.277  
   1.278  lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
   1.279  lemmas mod_div_equality2 = mod_div_equality2 [of "n\<Colon>nat" m, standard]
   1.280 @@ -234,11 +366,11 @@
   1.281  structure CancelDivModData =
   1.282  struct
   1.283  
   1.284 -val div_name = @{const_name Divides.div};
   1.285 -val mod_name = @{const_name Divides.mod};
   1.286 +val div_name = @{const_name div};
   1.287 +val mod_name = @{const_name mod};
   1.288  val mk_binop = HOLogic.mk_binop;
   1.289 -val mk_sum = NatArithUtils.mk_sum;
   1.290 -val dest_sum = NatArithUtils.dest_sum;
   1.291 +val mk_sum = ArithData.mk_sum;
   1.292 +val dest_sum = ArithData.dest_sum;
   1.293  
   1.294  (*logic*)
   1.295  
   1.296 @@ -248,29 +380,78 @@
   1.297  
   1.298  val prove_eq_sums =
   1.299    let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   1.300 -  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   1.301 +  in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
   1.302  
   1.303  end;
   1.304  
   1.305  structure CancelDivMod = CancelDivModFun(CancelDivModData);
   1.306  
   1.307 -val cancel_div_mod_proc = NatArithUtils.prep_simproc
   1.308 -      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
   1.309 +val cancel_div_mod_proc = Simplifier.simproc @{theory}
   1.310 +  "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
   1.311  
   1.312  Addsimprocs[cancel_div_mod_proc];
   1.313  *}
   1.314  
   1.315 +text {* code generator setup *}
   1.316 +
   1.317 +lemma divmod_if [code]: "divmod m n = (if n = 0 \<or> m < n then (0, m) else
   1.318 +  let (q, r) = divmod (m - n) n in (Suc q, r))"
   1.319 +  by (simp add: divmod_zero divmod_base divmod_step)
   1.320 +    (simp add: divmod_div_mod)
   1.321 +
   1.322 +code_modulename SML
   1.323 +  Divides Nat
   1.324 +
   1.325 +code_modulename OCaml
   1.326 +  Divides Nat
   1.327 +
   1.328 +code_modulename Haskell
   1.329 +  Divides Nat
   1.330 +
   1.331 +
   1.332 +subsubsection {* Quotient *}
   1.333 +
   1.334 +lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
   1.335 +lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
   1.336 +
   1.337 +lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
   1.338 +  by (simp add: le_div_geq linorder_not_less)
   1.339 +
   1.340 +lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
   1.341 +  by (simp add: div_geq)
   1.342 +
   1.343 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.344 +  by (rule mult_div) simp
   1.345 +
   1.346 +lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.347 +  by (simp add: mult_commute)
   1.348 +
   1.349  
   1.350  subsubsection {* Remainder *}
   1.351  
   1.352  lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
   1.353 +lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
   1.354  
   1.355 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.356 -  by (induct m) (simp_all add: le_div_geq)
   1.357 +lemma mod_less_divisor [simp]:
   1.358 +  fixes m n :: nat
   1.359 +  assumes "n > 0"
   1.360 +  shows "m mod n < (n::nat)"
   1.361 +  using assms divmod_rel unfolding divmod_rel_def by auto
   1.362  
   1.363 -lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
   1.364 +lemma mod_less_eq_dividend [simp]:
   1.365 +  fixes m n :: nat
   1.366 +  shows "m mod n \<le> m"
   1.367 +proof (rule add_leD2)
   1.368 +  from mod_div_equality have "m div n * n + m mod n = m" .
   1.369 +  then show "m div n * n + m mod n \<le> m" by auto
   1.370 +qed
   1.371 +
   1.372 +lemma mod_geq: "\<not> m < (n\<Colon>nat) \<Longrightarrow> m mod n = (m - n) mod n"
   1.373    by (simp add: le_mod_geq linorder_not_less)
   1.374  
   1.375 +lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
   1.376 +  by (simp add: le_mod_geq)
   1.377 +
   1.378  lemma mod_1 [simp]: "m mod Suc 0 = 0"
   1.379    by (induct m) (simp_all add: mod_geq)
   1.380  
   1.381 @@ -291,7 +472,7 @@
   1.382  lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
   1.383    by (simp add: mult_commute mod_mult_self1)
   1.384  
   1.385 -lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
   1.386 +lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
   1.387    apply (cases "n = 0", simp)
   1.388    apply (cases "k = 0", simp)
   1.389    apply (induct m rule: nat_less_induct)
   1.390 @@ -313,106 +494,41 @@
   1.391  lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
   1.392    by (simp add: mult_commute mod_mult_self_is_0)
   1.393  
   1.394 -
   1.395 -subsubsection{*Quotient*}
   1.396 -
   1.397 -lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
   1.398 -
   1.399 -lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
   1.400 -  by (simp add: le_div_geq linorder_not_less)
   1.401 -
   1.402 -lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   1.403 -  by (simp add: div_geq)
   1.404 -
   1.405 -
   1.406 -
   1.407  (* a simple rearrangement of mod_div_equality: *)
   1.408  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   1.409    by (cut_tac m = m and n = n in mod_div_equality2, arith)
   1.410  
   1.411 -lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
   1.412 -  apply (induct m rule: nat_less_induct)
   1.413 -  apply (rename_tac m)
   1.414 -  apply (case_tac "m<n", simp)
   1.415 -  txt{*case @{term "n \<le> m"}*}
   1.416 -  apply (simp add: mod_geq)
   1.417 -  done
   1.418 -
   1.419  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   1.420    apply (drule mod_less_divisor [where m = m])
   1.421    apply simp
   1.422    done
   1.423  
   1.424 -lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.425 -  by (simp add: mult_commute div_mult_self_is_m)
   1.426 -
   1.427 -(*mod_mult_distrib2 above is the counterpart for remainder*)
   1.428 -
   1.429 -
   1.430 -subsubsection {* Proving advancedfacts about Quotient and Remainder *}
   1.431 -
   1.432 -definition
   1.433 -  quorem :: "(nat*nat) * (nat*nat) => bool" where
   1.434 -  (*This definition helps prove the harder properties of div and mod.
   1.435 -    It is copied from IntDiv.thy; should it be overloaded?*)
   1.436 -  "quorem = (%((a,b), (q,r)).
   1.437 -                    a = b*q + r &
   1.438 -                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
   1.439 -
   1.440 -lemma unique_quotient_lemma:
   1.441 -     "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
   1.442 -      ==> q' \<le> (q::nat)"
   1.443 -  apply (rule leI)
   1.444 -  apply (subst less_iff_Suc_add)
   1.445 -  apply (auto simp add: add_mult_distrib2)
   1.446 -  done
   1.447 +subsubsection {* Quotient and Remainder *}
   1.448  
   1.449 -lemma unique_quotient:
   1.450 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
   1.451 -      ==> q = q'"
   1.452 -  apply (simp add: split_ifs quorem_def)
   1.453 -  apply (blast intro: order_antisym
   1.454 -    dest: order_eq_refl [THEN unique_quotient_lemma] sym)
   1.455 -  done
   1.456 -
   1.457 -lemma unique_remainder:
   1.458 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
   1.459 -      ==> r = r'"
   1.460 -  apply (subgoal_tac "q = q'")
   1.461 -   prefer 2 apply (blast intro: unique_quotient)
   1.462 -  apply (simp add: quorem_def)
   1.463 -  done
   1.464 -
   1.465 -lemma quorem_div_mod: "b > 0 ==> quorem ((a, b), (a div b, a mod b))"
   1.466 -unfolding quorem_def by simp
   1.467 +lemma mod_div_decomp:
   1.468 +  fixes n k :: nat
   1.469 +  obtains m q where "m = n div k" and "q = n mod k"
   1.470 +    and "n = m * k + q"
   1.471 +proof -
   1.472 +  from mod_div_equality have "n = n div k * k + n mod k" by auto
   1.473 +  moreover have "n div k = n div k" ..
   1.474 +  moreover have "n mod k = n mod k" ..
   1.475 +  note that ultimately show thesis by blast
   1.476 +qed
   1.477  
   1.478 -lemma quorem_div: "[| quorem((a,b),(q,r));  b > 0 |] ==> a div b = q"
   1.479 -by (simp add: quorem_div_mod [THEN unique_quotient])
   1.480 -
   1.481 -lemma quorem_mod: "[| quorem((a,b),(q,r));  b > 0 |] ==> a mod b = r"
   1.482 -by (simp add: quorem_div_mod [THEN unique_remainder])
   1.483 -
   1.484 -(** A dividend of zero **)
   1.485 -
   1.486 -lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
   1.487 -
   1.488 -lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
   1.489 -
   1.490 -(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   1.491 -
   1.492 -lemma quorem_mult1_eq:
   1.493 -  "[| quorem((b,c),(q,r)); c > 0 |]
   1.494 -   ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
   1.495 -by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.496 +lemma divmod_rel_mult1_eq:
   1.497 +  "[| divmod_rel b c q r; c > 0 |]
   1.498 +   ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
   1.499 +by (auto simp add: split_ifs mult_ac divmod_rel_def add_mult_distrib2)
   1.500  
   1.501  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
   1.502  apply (cases "c = 0", simp)
   1.503 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   1.504 +apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
   1.505  done
   1.506  
   1.507  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
   1.508  apply (cases "c = 0", simp)
   1.509 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
   1.510 +apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
   1.511  done
   1.512  
   1.513  lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
   1.514 @@ -428,30 +544,23 @@
   1.515  apply (rule mod_mult1_eq)
   1.516  done
   1.517  
   1.518 -(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   1.519 -
   1.520 -lemma quorem_add1_eq:
   1.521 -  "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c > 0 |]
   1.522 -   ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
   1.523 -by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.524 +lemma divmod_rel_add1_eq:
   1.525 +  "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
   1.526 +   ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
   1.527 +by (auto simp add: split_ifs mult_ac divmod_rel_def add_mult_distrib2)
   1.528  
   1.529  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.530  lemma div_add1_eq:
   1.531    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.532  apply (cases "c = 0", simp)
   1.533 -apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod)
   1.534 +apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
   1.535  done
   1.536  
   1.537  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
   1.538  apply (cases "c = 0", simp)
   1.539 -apply (blast intro: quorem_div_mod quorem_add1_eq [THEN quorem_mod])
   1.540 +apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
   1.541  done
   1.542  
   1.543 -
   1.544 -subsubsection {* Proving @{prop "a div (b*c) = (a div b) div c"} *}
   1.545 -
   1.546 -(** first, a lemma to bound the remainder **)
   1.547 -
   1.548  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   1.549    apply (cut_tac m = q and n = c in mod_less_divisor)
   1.550    apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.551 @@ -459,20 +568,20 @@
   1.552    apply (simp add: add_mult_distrib2)
   1.553    done
   1.554  
   1.555 -lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
   1.556 -      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   1.557 -  by (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
   1.558 +lemma divmod_rel_mult2_eq: "[| divmod_rel a b q r;  0 < b;  0 < c |]
   1.559 +      ==> divmod_rel a (b*c) (q div c) (b*(q mod c) + r)"
   1.560 +  by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   1.561  
   1.562  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
   1.563    apply (cases "b = 0", simp)
   1.564    apply (cases "c = 0", simp)
   1.565 -  apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
   1.566 +  apply (force simp add: divmod_rel [THEN divmod_rel_mult2_eq, THEN div_eq])
   1.567    done
   1.568  
   1.569  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
   1.570    apply (cases "b = 0", simp)
   1.571    apply (cases "c = 0", simp)
   1.572 -  apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
   1.573 +  apply (auto simp add: mult_commute divmod_rel [THEN divmod_rel_mult2_eq, THEN mod_eq])
   1.574    done
   1.575  
   1.576  
   1.577 @@ -595,6 +704,61 @@
   1.578    by (cases "n = 0") auto
   1.579  
   1.580  
   1.581 +(* Antimonotonicity of div in second argument *)
   1.582 +lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   1.583 +apply (subgoal_tac "0<n")
   1.584 + prefer 2 apply simp
   1.585 +apply (induct_tac k rule: nat_less_induct)
   1.586 +apply (rename_tac "k")
   1.587 +apply (case_tac "k<n", simp)
   1.588 +apply (subgoal_tac "~ (k<m) ")
   1.589 + prefer 2 apply simp
   1.590 +apply (simp add: div_geq)
   1.591 +apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   1.592 + prefer 2
   1.593 + apply (blast intro: div_le_mono diff_le_mono2)
   1.594 +apply (rule le_trans, simp)
   1.595 +apply (simp)
   1.596 +done
   1.597 +
   1.598 +lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
   1.599 +apply (case_tac "n=0", simp)
   1.600 +apply (subgoal_tac "m div n \<le> m div 1", simp)
   1.601 +apply (rule div_le_mono2)
   1.602 +apply (simp_all (no_asm_simp))
   1.603 +done
   1.604 +
   1.605 +(* Similar for "less than" *)
   1.606 +lemma div_less_dividend [rule_format]:
   1.607 +     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   1.608 +apply (induct_tac m rule: nat_less_induct)
   1.609 +apply (rename_tac "m")
   1.610 +apply (case_tac "m<n", simp)
   1.611 +apply (subgoal_tac "0<n")
   1.612 + prefer 2 apply simp
   1.613 +apply (simp add: div_geq)
   1.614 +apply (case_tac "n<m")
   1.615 + apply (subgoal_tac "(m-n) div n < (m-n) ")
   1.616 +  apply (rule impI less_trans_Suc)+
   1.617 +apply assumption
   1.618 +  apply (simp_all)
   1.619 +done
   1.620 +
   1.621 +declare div_less_dividend [simp]
   1.622 +
   1.623 +text{*A fact for the mutilated chess board*}
   1.624 +lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   1.625 +apply (case_tac "n=0", simp)
   1.626 +apply (induct "m" rule: nat_less_induct)
   1.627 +apply (case_tac "Suc (na) <n")
   1.628 +(* case Suc(na) < n *)
   1.629 +apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   1.630 +(* case n \<le> Suc(na) *)
   1.631 +apply (simp add: linorder_not_less le_Suc_eq mod_geq)
   1.632 +apply (auto simp add: Suc_diff_le le_mod_geq)
   1.633 +done
   1.634 +
   1.635 +
   1.636  subsubsection{*The Divides Relation*}
   1.637  
   1.638  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   1.639 @@ -743,6 +907,18 @@
   1.640    apply (simp add: power_add)
   1.641    done
   1.642  
   1.643 +lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
   1.644 +  apply (rule trans [symmetric])
   1.645 +   apply (rule mod_add1_eq, simp)
   1.646 +  apply (rule mod_add1_eq [symmetric])
   1.647 +  done
   1.648 +
   1.649 +lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
   1.650 +  apply (rule trans [symmetric])
   1.651 +   apply (rule mod_add1_eq, simp)
   1.652 +  apply (rule mod_add1_eq [symmetric])
   1.653 +  done
   1.654 +
   1.655  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   1.656    by (induct n) auto
   1.657  
   1.658 @@ -769,7 +945,6 @@
   1.659    apply (blast intro: sym)
   1.660    done
   1.661  
   1.662 -
   1.663  lemma split_div:
   1.664   "P(n div k :: nat) =
   1.665   ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
   1.666 @@ -811,21 +986,24 @@
   1.667  qed
   1.668  
   1.669  lemma split_div_lemma:
   1.670 -  "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
   1.671 -apply (rule iffI)
   1.672 - apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
   1.673 -   prefer 3; apply assumption
   1.674 -  apply (simp_all add: quorem_def)
   1.675 - apply arith
   1.676 -apply (rule conjI)
   1.677 - apply (rule_tac P="%x. n * (m div n) \<le> x" in
   1.678 -    subst [OF mod_div_equality [of _ n]])
   1.679 - apply (simp only: add: mult_ac)
   1.680 - apply (rule_tac P="%x. x < n + n * (m div n)" in
   1.681 -    subst [OF mod_div_equality [of _ n]])
   1.682 -apply (simp only: add: mult_ac add_ac)
   1.683 -apply (rule add_less_mono1, simp)
   1.684 -done
   1.685 +  assumes "0 < n"
   1.686 +  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.687 +proof
   1.688 +  assume ?rhs
   1.689 +  with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
   1.690 +  then have A: "n * q \<le> m" by simp
   1.691 +  have "n - (m mod n) > 0" using mod_less_divisor assms by auto
   1.692 +  then have "m < m + (n - (m mod n))" by simp
   1.693 +  then have "m < n + (m - (m mod n))" by simp
   1.694 +  with nq have "m < n + n * q" by simp
   1.695 +  then have B: "m < n * Suc q" by simp
   1.696 +  from A B show ?lhs ..
   1.697 +next
   1.698 +  assume P: ?lhs
   1.699 +  then have "divmod_rel m n q (m - n * q)"
   1.700 +    unfolding divmod_rel_def by (auto simp add: mult_ac)
   1.701 +  then show ?rhs using divmod_rel by (rule divmod_rel_unique_div)
   1.702 +qed
   1.703  
   1.704  theorem split_div':
   1.705    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   1.706 @@ -976,62 +1154,4 @@
   1.707    with j show ?thesis by blast
   1.708  qed
   1.709  
   1.710 -
   1.711 -lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
   1.712 -  apply (rule trans [symmetric])
   1.713 -   apply (rule mod_add1_eq, simp)
   1.714 -  apply (rule mod_add1_eq [symmetric])
   1.715 -  done
   1.716 -
   1.717 -lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
   1.718 -  apply (rule trans [symmetric])
   1.719 -   apply (rule mod_add1_eq, simp)
   1.720 -  apply (rule mod_add1_eq [symmetric])
   1.721 -  done
   1.722 -
   1.723 -lemma mod_div_decomp:
   1.724 -  fixes n k :: nat
   1.725 -  obtains m q where "m = n div k" and "q = n mod k"
   1.726 -    and "n = m * k + q"
   1.727 -proof -
   1.728 -  from mod_div_equality have "n = n div k * k + n mod k" by auto
   1.729 -  moreover have "n div k = n div k" ..
   1.730 -  moreover have "n mod k = n mod k" ..
   1.731 -  note that ultimately show thesis by blast
   1.732 -qed
   1.733 -
   1.734 -
   1.735 -subsubsection {* Code generation for div, mod and dvd on nat *}
   1.736 -
   1.737 -definition [code func del]:
   1.738 -  "divmod (m\<Colon>nat) n = (m div n, m mod n)"
   1.739 -
   1.740 -lemma divmod_zero [code]: "divmod m 0 = (0, m)"
   1.741 -  unfolding divmod_def by simp
   1.742 -
   1.743 -lemma divmod_succ [code]:
   1.744 -  "divmod m (Suc k) = (if m < Suc k then (0, m) else
   1.745 -    let
   1.746 -      (p, q) = divmod (m - Suc k) (Suc k)
   1.747 -    in (Suc p, q))"
   1.748 -  unfolding divmod_def Let_def split_def
   1.749 -  by (auto intro: div_geq mod_geq)
   1.750 -
   1.751 -lemma div_divmod [code]: "m div n = fst (divmod m n)"
   1.752 -  unfolding divmod_def by simp
   1.753 -
   1.754 -lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
   1.755 -  unfolding divmod_def by simp
   1.756 -
   1.757 -code_modulename SML
   1.758 -  Divides Nat
   1.759 -
   1.760 -code_modulename OCaml
   1.761 -  Divides Nat
   1.762 -
   1.763 -code_modulename Haskell
   1.764 -  Divides Nat
   1.765 -
   1.766 -hide (open) const divmod
   1.767 -
   1.768  end
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Feb 20 14:35:55 2008 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Feb 20 14:52:34 2008 +0100
     2.3 @@ -57,17 +57,17 @@
     2.4    and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
     2.5  
     2.6  definition
     2.7 -  div_mod_nat_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
     2.8 +  divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
     2.9  where
    2.10 -  [code func del]: "div_mod_nat_aux = Divides.divmod"
    2.11 +  [code func del]: "divmod_aux = divmod"
    2.12  
    2.13  lemma [code func]:
    2.14 -  "Divides.divmod n m = (if m = 0 then (0, n) else div_mod_nat_aux n m)"
    2.15 -  unfolding div_mod_nat_aux_def divmod_def by simp
    2.16 +  "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
    2.17 +  unfolding divmod_aux_def divmod_div_mod by simp
    2.18  
    2.19 -lemma div_mod_aux_code [code]:
    2.20 -  "div_mod_nat_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
    2.21 -  unfolding div_mod_nat_aux_def divmod_def zdiv_int [symmetric] zmod_int [symmetric] by simp
    2.22 +lemma divmod_aux_code [code]:
    2.23 +  "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
    2.24 +  unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
    2.25  
    2.26  lemma eq_nat_code [code]:
    2.27    "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m"
    2.28 @@ -388,7 +388,7 @@
    2.29    (OCaml "Big'_int.mult'_big'_int")
    2.30    (Haskell infixl 7 "*")
    2.31  
    2.32 -code_const div_mod_nat_aux
    2.33 +code_const divmod_aux
    2.34    (SML "IntInf.divMod/ ((_),/ (_))")
    2.35    (OCaml "Big'_int.quomod'_big'_int")
    2.36    (Haskell "divMod")