src/HOL/Divides.thy
changeset 60868 dd18c33c001e
parent 60867 86e7560e07d0
child 60930 dd8ab7252ba2
     1.1 --- a/src/HOL/Divides.thy	Thu Aug 06 23:56:48 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Aug 08 10:51:33 2015 +0200
     1.3 @@ -543,7 +543,7 @@
     1.4  lemma odd_two_times_div_two_succ [simp]:
     1.5    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
     1.6    using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
     1.7 -
     1.8 + 
     1.9  end
    1.10  
    1.11  
    1.12 @@ -1374,7 +1374,7 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 -theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
    1.17 +theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
    1.18    using mod_div_equality [of m n] by arith
    1.19  
    1.20  lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
    1.21 @@ -1520,6 +1520,11 @@
    1.22  
    1.23  declare Suc_times_mod_eq [of "numeral w", simp] for w
    1.24  
    1.25 +lemma mod_greater_zero_iff_not_dvd:
    1.26 +  fixes m n :: nat
    1.27 +  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
    1.28 +  by (simp add: dvd_eq_mod_eq_0)
    1.29 +
    1.30  lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
    1.31  by (simp add: div_le_mono)
    1.32  
    1.33 @@ -1595,111 +1600,25 @@
    1.34    qed
    1.35  qed
    1.36  
    1.37 +lemma Suc_0_div_numeral [simp]:
    1.38 +  fixes k l :: num
    1.39 +  shows "Suc 0 div numeral k = fst (divmod Num.One k)"
    1.40 +  by (simp_all add: fst_divmod)
    1.41 +
    1.42 +lemma Suc_0_mod_numeral [simp]:
    1.43 +  fixes k l :: num
    1.44 +  shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
    1.45 +  by (simp_all add: snd_divmod)
    1.46 +
    1.47  
    1.48  subsection \<open>Division on @{typ int}\<close>
    1.49  
    1.50 -definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
    1.51 -    --\<open>definition of quotient and remainder\<close>
    1.52 -  "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
    1.53 +definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" -- \<open>definition of quotient and remainder\<close>
    1.54 +  where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
    1.55      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
    1.56  
    1.57 -text \<open>
    1.58 -  The following algorithmic devlopment actually echos what has already
    1.59 -  been developed in class @{class semiring_numeral_div}.  In the long
    1.60 -  run it seems better to derive division on @{typ int} just from
    1.61 -  division on @{typ nat} and instantiate @{class semiring_numeral_div}
    1.62 -  accordingly.
    1.63 -\<close>
    1.64 -
    1.65 -definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
    1.66 -    --\<open>for the division algorithm\<close>
    1.67 -    "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
    1.68 -                         else (2 * q, r))"
    1.69 -
    1.70 -text\<open>algorithm for the case @{text "a\<ge>0, b>0"}\<close>
    1.71 -function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.72 -  "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
    1.73 -     else adjust b (posDivAlg a (2 * b)))"
    1.74 -by auto
    1.75 -termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")
    1.76 -  (auto simp add: mult_2)
    1.77 -
    1.78 -text\<open>algorithm for the case @{text "a<0, b>0"}\<close>
    1.79 -function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.80 -  "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
    1.81 -     else adjust b (negDivAlg a (2 * b)))"
    1.82 -by auto
    1.83 -termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")
    1.84 -  (auto simp add: mult_2)
    1.85 -
    1.86 -text\<open>algorithm for the general case @{term "b\<noteq>0"}\<close>
    1.87 -
    1.88 -definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.89 -    --\<open>The full division algorithm considers all possible signs for a, b
    1.90 -       including the special case @{text "a=0, b<0"} because
    1.91 -       @{term negDivAlg} requires @{term "a<0"}.\<close>
    1.92 -  "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
    1.93 -                  else if a = 0 then (0, 0)
    1.94 -                       else apsnd uminus (negDivAlg (-a) (-b))
    1.95 -               else
    1.96 -                  if 0 < b then negDivAlg a b
    1.97 -                  else apsnd uminus (posDivAlg (-a) (-b)))"
    1.98 -
    1.99 -instantiation int :: ring_div
   1.100 -begin
   1.101 -
   1.102 -definition divide_int where
   1.103 -  div_int_def: "a div b = fst (divmod_int a b)"
   1.104 -
   1.105 -definition mod_int where
   1.106 -  "a mod b = snd (divmod_int a b)"
   1.107 -
   1.108 -lemma fst_divmod_int [simp]:
   1.109 -  "fst (divmod_int a b) = a div b"
   1.110 -  by (simp add: div_int_def)
   1.111 -
   1.112 -lemma snd_divmod_int [simp]:
   1.113 -  "snd (divmod_int a b) = a mod b"
   1.114 -  by (simp add: mod_int_def)
   1.115 -
   1.116 -lemma divmod_int_mod_div:
   1.117 -  "divmod_int p q = (p div q, p mod q)"
   1.118 -  by (simp add: prod_eq_iff)
   1.119 -
   1.120 -text\<open>
   1.121 -Here is the division algorithm in ML:
   1.122 -
   1.123 -\begin{verbatim}
   1.124 -    fun posDivAlg (a,b) =
   1.125 -      if a<b then (0,a)
   1.126 -      else let val (q,r) = posDivAlg(a, 2*b)
   1.127 -               in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
   1.128 -           end
   1.129 -
   1.130 -    fun negDivAlg (a,b) =
   1.131 -      if 0\<le>a+b then (~1,a+b)
   1.132 -      else let val (q,r) = negDivAlg(a, 2*b)
   1.133 -               in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
   1.134 -           end;
   1.135 -
   1.136 -    fun negateSnd (q,r:int) = (q,~r);
   1.137 -
   1.138 -    fun divmod (a,b) = if 0\<le>a then
   1.139 -                          if b>0 then posDivAlg (a,b)
   1.140 -                           else if a=0 then (0,0)
   1.141 -                                else negateSnd (negDivAlg (~a,~b))
   1.142 -                       else
   1.143 -                          if 0<b then negDivAlg (a,b)
   1.144 -                          else        negateSnd (posDivAlg (~a,~b));
   1.145 -\end{verbatim}
   1.146 -\<close>
   1.147 -
   1.148 -
   1.149 -subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
   1.150 -
   1.151  lemma unique_quotient_lemma:
   1.152 -     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
   1.153 -      ==> q' \<le> (q::int)"
   1.154 +  "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
   1.155  apply (subgoal_tac "r' + b * (q'-q) \<le> r")
   1.156   prefer 2 apply (simp add: right_diff_distrib)
   1.157  apply (subgoal_tac "0 < b * (1 + q - q') ")
   1.158 @@ -1711,145 +1630,83 @@
   1.159  done
   1.160  
   1.161  lemma unique_quotient_lemma_neg:
   1.162 -     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]
   1.163 -      ==> q \<le> (q'::int)"
   1.164 -by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
   1.165 -    auto)
   1.166 +  "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   1.167 +  by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
   1.168  
   1.169  lemma unique_quotient:
   1.170 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   1.171 -      ==> q = q'"
   1.172 +  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
   1.173  apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
   1.174  apply (blast intro: order_antisym
   1.175               dest: order_eq_refl [THEN unique_quotient_lemma]
   1.176               order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.177  done
   1.178  
   1.179 -
   1.180  lemma unique_remainder:
   1.181 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   1.182 -      ==> r = r'"
   1.183 +  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
   1.184  apply (subgoal_tac "q = q'")
   1.185   apply (simp add: divmod_int_rel_def)
   1.186  apply (blast intro: unique_quotient)
   1.187  done
   1.188  
   1.189 -
   1.190 -subsubsection \<open>Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends\<close>
   1.191 -
   1.192 -text\<open>And positive divisors\<close>
   1.193 -
   1.194 -lemma adjust_eq [simp]:
   1.195 -     "adjust b (q, r) =
   1.196 -      (let diff = r - b in
   1.197 -        if 0 \<le> diff then (2 * q + 1, diff)
   1.198 -                     else (2*q, r))"
   1.199 -  by (simp add: Let_def adjust_def)
   1.200 -
   1.201 -declare posDivAlg.simps [simp del]
   1.202 -
   1.203 -text\<open>use with a simproc to avoid repeatedly proving the premise\<close>
   1.204 -lemma posDivAlg_eqn:
   1.205 -     "0 < b ==>
   1.206 -      posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
   1.207 -by (rule posDivAlg.simps [THEN trans], simp)
   1.208 -
   1.209 -text\<open>Correctness of @{term posDivAlg}: it computes quotients correctly\<close>
   1.210 -theorem posDivAlg_correct:
   1.211 -  assumes "0 \<le> a" and "0 < b"
   1.212 -  shows "divmod_int_rel a b (posDivAlg a b)"
   1.213 -  using assms
   1.214 -  apply (induct a b rule: posDivAlg.induct)
   1.215 -  apply auto
   1.216 -  apply (simp add: divmod_int_rel_def)
   1.217 -  apply (subst posDivAlg_eqn, simp add: distrib_left)
   1.218 -  apply (case_tac "a < b")
   1.219 -  apply simp_all
   1.220 -  apply (erule splitE)
   1.221 -  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
   1.222 +instantiation int :: Divides.div
   1.223 +begin
   1.224 +
   1.225 +definition divide_int
   1.226 +  where "k div l = (if l = 0 \<or> k = 0 then 0
   1.227 +    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   1.228 +      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   1.229 +      else
   1.230 +        if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   1.231 +        else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
   1.232 +
   1.233 +definition mod_int
   1.234 +  where "k mod l = (if l = 0 then k else if l dvd k then 0
   1.235 +    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   1.236 +      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   1.237 +      else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   1.238 +
   1.239 +instance ..      
   1.240 +
   1.241 +end
   1.242 +
   1.243 +lemma divmod_int_rel:
   1.244 +  "divmod_int_rel k l (k div l, k mod l)"
   1.245 +  apply (cases k rule: int_cases3)
   1.246 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
   1.247 +  apply (cases l rule: int_cases3)
   1.248 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
   1.249 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
   1.250 +  apply (simp add: of_nat_add [symmetric])
   1.251 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
   1.252 +  apply (simp add: of_nat_add [symmetric])
   1.253 +  apply (cases l rule: int_cases3)
   1.254 +  apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
   1.255 +  apply (simp_all add: of_nat_add [symmetric])
   1.256    done
   1.257  
   1.258 -
   1.259 -subsubsection \<open>Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends\<close>
   1.260 -
   1.261 -text\<open>And positive divisors\<close>
   1.262 -
   1.263 -declare negDivAlg.simps [simp del]
   1.264 -
   1.265 -text\<open>use with a simproc to avoid repeatedly proving the premise\<close>
   1.266 -lemma negDivAlg_eqn:
   1.267 -     "0 < b ==>
   1.268 -      negDivAlg a b =
   1.269 -       (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
   1.270 -by (rule negDivAlg.simps [THEN trans], simp)
   1.271 -
   1.272 -(*Correctness of negDivAlg: it computes quotients correctly
   1.273 -  It doesn't work if a=0 because the 0/b equals 0, not -1*)
   1.274 -lemma negDivAlg_correct:
   1.275 -  assumes "a < 0" and "b > 0"
   1.276 -  shows "divmod_int_rel a b (negDivAlg a b)"
   1.277 -  using assms
   1.278 -  apply (induct a b rule: negDivAlg.induct)
   1.279 -  apply (auto simp add: linorder_not_le)
   1.280 -  apply (simp add: divmod_int_rel_def)
   1.281 -  apply (subst negDivAlg_eqn, assumption)
   1.282 -  apply (case_tac "a + b < (0\<Colon>int)")
   1.283 -  apply simp_all
   1.284 -  apply (erule splitE)
   1.285 -  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
   1.286 -  done
   1.287 -
   1.288 -
   1.289 -subsubsection \<open>Existence Shown by Proving the Division Algorithm to be Correct\<close>
   1.290 -
   1.291 -(*the case a=0*)
   1.292 -lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
   1.293 -by (auto simp add: divmod_int_rel_def linorder_neq_iff)
   1.294 -
   1.295 -lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
   1.296 -by (subst posDivAlg.simps, auto)
   1.297 -
   1.298 -lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
   1.299 -by (subst posDivAlg.simps, auto)
   1.300 -
   1.301 -lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
   1.302 -by (subst negDivAlg.simps, auto)
   1.303 -
   1.304 -lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
   1.305 -by (auto simp add: divmod_int_rel_def)
   1.306 -
   1.307 -lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
   1.308 -apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
   1.309 -by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
   1.310 -                    posDivAlg_correct negDivAlg_correct)
   1.311 +instantiation int :: ring_div
   1.312 +begin
   1.313 +
   1.314 +subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
   1.315  
   1.316  lemma divmod_int_unique:
   1.317 -  assumes "divmod_int_rel a b qr"
   1.318 -  shows "divmod_int a b = qr"
   1.319 -  using assms divmod_int_correct [of a b]
   1.320 -  using unique_quotient [of a b] unique_remainder [of a b]
   1.321 -  by (metis pair_collapse)
   1.322 -
   1.323 -lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
   1.324 -  using divmod_int_correct by (simp add: divmod_int_mod_div)
   1.325 -
   1.326 -lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
   1.327 -  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
   1.328 -
   1.329 -lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   1.330 -  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   1.331 -
   1.332 +  assumes "divmod_int_rel k l (q, r)"
   1.333 +  shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   1.334 +  using assms divmod_int_rel [of k l]
   1.335 +  using unique_quotient [of k l] unique_remainder [of k l]
   1.336 +  by auto
   1.337 +  
   1.338  instance
   1.339  proof
   1.340    fix a b :: int
   1.341    show "a div b * b + a mod b = a"
   1.342 -    using divmod_int_rel_div_mod [of a b]
   1.343 +    using divmod_int_rel [of a b]
   1.344      unfolding divmod_int_rel_def by (simp add: mult.commute)
   1.345  next
   1.346    fix a b c :: int
   1.347    assume "b \<noteq> 0"
   1.348    hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
   1.349 -    using divmod_int_rel_div_mod [of a b]
   1.350 +    using divmod_int_rel [of a b]
   1.351      unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   1.352    thus "(a + c * b) div b = c + a div b"
   1.353      by (rule div_int_unique)
   1.354 @@ -1863,7 +1720,7 @@
   1.355        mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   1.356        mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
   1.357    hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
   1.358 -    using divmod_int_rel_div_mod [of a b] .
   1.359 +    using divmod_int_rel [of a b] .
   1.360    thus "(c * a) div (c * b) = a div b"
   1.361      by (rule div_int_unique)
   1.362  next
   1.363 @@ -1906,6 +1763,12 @@
   1.364  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
   1.365    by (fact mod_div_equality2 [symmetric])
   1.366  
   1.367 +lemma zdiv_int: "int (a div b) = int a div int b"
   1.368 +  by (simp add: divide_int_def)
   1.369 +
   1.370 +lemma zmod_int: "int (a mod b) = int a mod int b"
   1.371 +  by (simp add: mod_int_def int_dvd_iff)
   1.372 +  
   1.373  text \<open>Tool setup\<close>
   1.374  
   1.375  ML \<open>
   1.376 @@ -1927,14 +1790,14 @@
   1.377  simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
   1.378  
   1.379  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   1.380 -  using divmod_int_correct [of a b]
   1.381 +  using divmod_int_rel [of a b]
   1.382    by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.383  
   1.384  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   1.385     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   1.386  
   1.387  lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   1.388 -  using divmod_int_correct [of a b]
   1.389 +  using divmod_int_rel [of a b]
   1.390    by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.391  
   1.392  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   1.393 @@ -1991,12 +1854,12 @@
   1.394       "b \<noteq> (0::int)
   1.395        ==> (-a) div b =
   1.396            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.397 -by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
   1.398 +by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
   1.399  
   1.400  lemma zmod_zminus1_eq_if:
   1.401       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   1.402  apply (case_tac "b = 0", simp)
   1.403 -apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
   1.404 +apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
   1.405  done
   1.406  
   1.407  lemma zmod_zminus1_not_zero:
   1.408 @@ -2020,149 +1883,6 @@
   1.409    unfolding zmod_zminus2_eq_if by auto
   1.410  
   1.411  
   1.412 -subsubsection \<open>Computation of Division and Remainder\<close>
   1.413 -
   1.414 -lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
   1.415 -by (simp add: div_int_def divmod_int_def)
   1.416 -
   1.417 -lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   1.418 -by (simp add: mod_int_def divmod_int_def)
   1.419 -
   1.420 -text\<open>a positive, b positive\<close>
   1.421 -
   1.422 -lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
   1.423 -by (simp add: div_int_def divmod_int_def)
   1.424 -
   1.425 -lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
   1.426 -by (simp add: mod_int_def divmod_int_def)
   1.427 -
   1.428 -text\<open>a negative, b positive\<close>
   1.429 -
   1.430 -lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
   1.431 -by (simp add: div_int_def divmod_int_def)
   1.432 -
   1.433 -lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
   1.434 -by (simp add: mod_int_def divmod_int_def)
   1.435 -
   1.436 -text\<open>a positive, b negative\<close>
   1.437 -
   1.438 -lemma div_pos_neg:
   1.439 -     "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"
   1.440 -by (simp add: div_int_def divmod_int_def)
   1.441 -
   1.442 -lemma mod_pos_neg:
   1.443 -     "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"
   1.444 -by (simp add: mod_int_def divmod_int_def)
   1.445 -
   1.446 -text\<open>a negative, b negative\<close>
   1.447 -
   1.448 -lemma div_neg_neg:
   1.449 -     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"
   1.450 -by (simp add: div_int_def divmod_int_def)
   1.451 -
   1.452 -lemma mod_neg_neg:
   1.453 -     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"
   1.454 -by (simp add: mod_int_def divmod_int_def)
   1.455 -
   1.456 -text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
   1.457 -
   1.458 -lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   1.459 -  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
   1.460 -
   1.461 -lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   1.462 -  by (rule div_int_unique [of a b q r],
   1.463 -    simp add: divmod_int_rel_def)
   1.464 -
   1.465 -lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   1.466 -  by (rule mod_int_unique [of a b q r],
   1.467 -    simp add: divmod_int_rel_def)
   1.468 -
   1.469 -lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.470 -  by (rule mod_int_unique [of a b q r],
   1.471 -    simp add: divmod_int_rel_def)
   1.472 -
   1.473 -text \<open>
   1.474 -  numeral simprocs -- high chance that these can be replaced
   1.475 -  by divmod algorithm from @{class semiring_numeral_div}
   1.476 -\<close>
   1.477 -
   1.478 -ML \<open>
   1.479 -local
   1.480 -  val mk_number = HOLogic.mk_number HOLogic.intT
   1.481 -  val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
   1.482 -  val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
   1.483 -  val zero = @{term "0 :: int"}
   1.484 -  val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
   1.485 -  val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
   1.486 -  val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
   1.487 -  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
   1.488 -    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
   1.489 -  fun binary_proc proc ctxt ct =
   1.490 -    (case Thm.term_of ct of
   1.491 -      _ $ t $ u =>
   1.492 -      (case try (apply2 (`(snd o HOLogic.dest_number))) (t, u) of
   1.493 -        SOME args => proc ctxt args
   1.494 -      | NONE => NONE)
   1.495 -    | _ => NONE);
   1.496 -in
   1.497 -  fun divmod_proc posrule negrule =
   1.498 -    binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
   1.499 -      if b = 0 then NONE
   1.500 -      else
   1.501 -        let
   1.502 -          val (q, r) = apply2 mk_number (Integer.div_mod a b)
   1.503 -          val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
   1.504 -          val (goal2, goal3, rule) =
   1.505 -            if b > 0
   1.506 -            then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
   1.507 -            else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
   1.508 -        in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
   1.509 -end
   1.510 -\<close>
   1.511 -
   1.512 -simproc_setup binary_int_div
   1.513 -  ("numeral m div numeral n :: int" |
   1.514 -   "numeral m div - numeral n :: int" |
   1.515 -   "- numeral m div numeral n :: int" |
   1.516 -   "- numeral m div - numeral n :: int") =
   1.517 -  \<open>K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq})\<close>
   1.518 -
   1.519 -simproc_setup binary_int_mod
   1.520 -  ("numeral m mod numeral n :: int" |
   1.521 -   "numeral m mod - numeral n :: int" |
   1.522 -   "- numeral m mod numeral n :: int" |
   1.523 -   "- numeral m mod - numeral n :: int") =
   1.524 -  \<open>K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq})\<close>
   1.525 -
   1.526 -lemmas posDivAlg_eqn_numeral [simp] =
   1.527 -    posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
   1.528 -
   1.529 -lemmas negDivAlg_eqn_numeral [simp] =
   1.530 -    negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
   1.531 -
   1.532 -
   1.533 -text \<open>Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"}\<close>
   1.534 -
   1.535 -lemma [simp]:
   1.536 -  shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
   1.537 -    and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
   1.538 -    and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
   1.539 -    and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
   1.540 -    and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
   1.541 -    and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
   1.542 -  by (simp_all del: arith_special
   1.543 -    add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
   1.544 -
   1.545 -lemma [simp]:
   1.546 -  shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
   1.547 -    and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"
   1.548 -    and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"
   1.549 -    and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"
   1.550 -    and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"
   1.551 -    and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"
   1.552 -  by (simp_all add: div_eq_minus1 zmod_minus1)
   1.553 -
   1.554 -
   1.555  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   1.556  
   1.557  lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
   1.558 @@ -2255,7 +1975,7 @@
   1.559  
   1.560  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   1.561  apply (case_tac "c = 0", simp)
   1.562 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
   1.563 +apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
   1.564  done
   1.565  
   1.566  text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
   1.567 @@ -2269,43 +1989,16 @@
   1.568  lemma zdiv_zadd1_eq:
   1.569       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.570  apply (case_tac "c = 0", simp)
   1.571 -apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
   1.572 +apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
   1.573  done
   1.574  
   1.575 -lemma posDivAlg_div_mod:
   1.576 -  assumes "k \<ge> 0"
   1.577 -  and "l \<ge> 0"
   1.578 -  shows "posDivAlg k l = (k div l, k mod l)"
   1.579 -proof (cases "l = 0")
   1.580 -  case True then show ?thesis by (simp add: posDivAlg.simps)
   1.581 -next
   1.582 -  case False with assms posDivAlg_correct
   1.583 -    have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
   1.584 -    by simp
   1.585 -  from div_int_unique [OF this] mod_int_unique [OF this]
   1.586 -  show ?thesis by simp
   1.587 -qed
   1.588 -
   1.589 -lemma negDivAlg_div_mod:
   1.590 -  assumes "k < 0"
   1.591 -  and "l > 0"
   1.592 -  shows "negDivAlg k l = (k div l, k mod l)"
   1.593 -proof -
   1.594 -  from assms have "l \<noteq> 0" by simp
   1.595 -  from assms negDivAlg_correct
   1.596 -    have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
   1.597 -    by simp
   1.598 -  from div_int_unique [OF this] mod_int_unique [OF this]
   1.599 -  show ?thesis by simp
   1.600 -qed
   1.601 -
   1.602  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   1.603  by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.604  
   1.605  (* REVISIT: should this be generalized to all semiring_div types? *)
   1.606  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   1.607  
   1.608 -lemma zmod_zdiv_equality':
   1.609 +lemma zmod_zdiv_equality' [nitpick_unfold]:
   1.610    "(m\<Colon>int) mod n = m - (m div n) * n"
   1.611    using mod_div_equality [of m n] by arith
   1.612  
   1.613 @@ -2363,14 +2056,14 @@
   1.614    fixes a b c :: int
   1.615    shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   1.616  apply (case_tac "b = 0", simp)
   1.617 -apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
   1.618 +apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
   1.619  done
   1.620  
   1.621  lemma zmod_zmult2_eq:
   1.622    fixes a b c :: int
   1.623    shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   1.624  apply (case_tac "b = 0", simp)
   1.625 -apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
   1.626 +apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
   1.627  done
   1.628  
   1.629  lemma div_pos_geq:
   1.630 @@ -2474,12 +2167,12 @@
   1.631  text\<open>computing div by shifting\<close>
   1.632  
   1.633  lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
   1.634 -  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
   1.635 +  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
   1.636    by (rule div_int_unique)
   1.637  
   1.638  lemma neg_zdiv_mult_2:
   1.639    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   1.640 -  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
   1.641 +  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
   1.642    by (rule div_int_unique)
   1.643  
   1.644  (* FIXME: add rules for negative numerals *)
   1.645 @@ -2500,14 +2193,14 @@
   1.646    fixes a b :: int
   1.647    assumes "0 \<le> a"
   1.648    shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
   1.649 -  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
   1.650 +  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.651    by (rule mod_int_unique)
   1.652  
   1.653  lemma neg_zmod_mult_2:
   1.654    fixes a b :: int
   1.655    assumes "a \<le> 0"
   1.656    shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
   1.657 -  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
   1.658 +  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.659    by (rule mod_int_unique)
   1.660  
   1.661  (* FIXME: add rules for negative numerals *)
   1.662 @@ -2538,6 +2231,12 @@
   1.663  
   1.664  subsubsection \<open>Quotients of Signs\<close>
   1.665  
   1.666 +lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
   1.667 +by (simp add: divide_int_def)
   1.668 +
   1.669 +lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   1.670 +by (simp add: mod_int_def)
   1.671 +
   1.672  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
   1.673  apply (subgoal_tac "a div b \<le> -1", force)
   1.674  apply (rule order_trans)
   1.675 @@ -2563,6 +2262,11 @@
   1.676  apply (blast intro: div_neg_pos_less0)
   1.677  done
   1.678  
   1.679 +lemma pos_imp_zdiv_pos_iff:
   1.680 +  "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   1.681 +using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
   1.682 +by arith
   1.683 +
   1.684  lemma neg_imp_zdiv_nonneg_iff:
   1.685    "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
   1.686  apply (subst div_minus_minus [symmetric])
   1.687 @@ -2573,11 +2277,6 @@
   1.688  lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
   1.689  by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
   1.690  
   1.691 -lemma pos_imp_zdiv_pos_iff:
   1.692 -  "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   1.693 -using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
   1.694 -by arith
   1.695 -
   1.696  (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
   1.697  lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
   1.698  by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
   1.699 @@ -2597,40 +2296,104 @@
   1.700  apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
   1.701  done
   1.702  
   1.703 -
   1.704 -subsubsection \<open>The Divides Relation\<close>
   1.705 -
   1.706 -lemma dvd_eq_mod_eq_0_numeral:
   1.707 -  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   1.708 -  by (fact dvd_eq_mod_eq_0)
   1.709 -
   1.710 -
   1.711 -subsubsection \<open>Further properties\<close>
   1.712 -
   1.713 -lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   1.714 -  using zmod_zdiv_equality[where a="m" and b="n"]
   1.715 +lemma zmult_div_cancel:
   1.716 +  "(n::int) * (m div n) = m - (m mod n)"
   1.717 +  using zmod_zdiv_equality [where a="m" and b="n"]
   1.718    by (simp add: algebra_simps) (* FIXME: generalize *)
   1.719  
   1.720 +
   1.721 +subsubsection \<open>Computation of Division and Remainder\<close>
   1.722 +
   1.723  instance int :: semiring_numeral_div
   1.724    by intro_classes (auto intro: zmod_le_nonneg_dividend
   1.725 -    simp add: zmult_div_cancel
   1.726 +    simp add:
   1.727 +    zmult_div_cancel
   1.728      pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   1.729      zmod_zmult2_eq zdiv_zmult2_eq)
   1.730  
   1.731 -lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   1.732 -apply (subst split_div, auto)
   1.733 -apply (subst split_zdiv, auto)
   1.734 -apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)
   1.735 -apply (auto simp add: divmod_int_rel_def of_nat_mult)
   1.736 -done
   1.737 -
   1.738 -lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
   1.739 -apply (subst split_mod, auto)
   1.740 -apply (subst split_zmod, auto)
   1.741 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
   1.742 -       in unique_remainder)
   1.743 -apply (auto simp add: divmod_int_rel_def of_nat_mult)
   1.744 -done
   1.745 +definition adjust_div :: "int \<times> int \<Rightarrow> int"
   1.746 +where
   1.747 +  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
   1.748 +
   1.749 +lemma adjust_div_eq [simp, code]:
   1.750 +  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
   1.751 +  by (simp add: adjust_div_def)
   1.752 +
   1.753 +definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
   1.754 +where
   1.755 +  [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
   1.756 +
   1.757 +lemma minus_numeral_div_numeral [simp]:
   1.758 +  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
   1.759 +proof -
   1.760 +  have "int (fst (divmod m n)) = fst (divmod m n)"
   1.761 +    by (simp only: fst_divmod divide_int_def) auto
   1.762 +  then show ?thesis
   1.763 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
   1.764 +qed
   1.765 +
   1.766 +lemma minus_numeral_mod_numeral [simp]:
   1.767 +  "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
   1.768 +proof -
   1.769 +  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.770 +    using that by (simp only: snd_divmod mod_int_def) auto
   1.771 +  then show ?thesis
   1.772 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def)
   1.773 +qed
   1.774 +
   1.775 +lemma numeral_div_minus_numeral [simp]:
   1.776 +  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
   1.777 +proof -
   1.778 +  have "int (fst (divmod m n)) = fst (divmod m n)"
   1.779 +    by (simp only: fst_divmod divide_int_def) auto
   1.780 +  then show ?thesis
   1.781 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
   1.782 +qed
   1.783 +  
   1.784 +lemma numeral_mod_minus_numeral [simp]:
   1.785 +  "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
   1.786 +proof -
   1.787 +  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.788 +    using that by (simp only: snd_divmod mod_int_def) auto
   1.789 +  then show ?thesis
   1.790 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def)
   1.791 +qed
   1.792 +
   1.793 +lemma minus_one_div_numeral [simp]:
   1.794 +  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
   1.795 +  using minus_numeral_div_numeral [of Num.One n] by simp  
   1.796 +
   1.797 +lemma minus_one_mod_numeral [simp]:
   1.798 +  "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
   1.799 +  using minus_numeral_mod_numeral [of Num.One n] by simp
   1.800 +
   1.801 +lemma one_div_minus_numeral [simp]:
   1.802 +  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
   1.803 +  using numeral_div_minus_numeral [of Num.One n] by simp
   1.804 +  
   1.805 +lemma one_mod_minus_numeral [simp]:
   1.806 +  "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
   1.807 +  using numeral_mod_minus_numeral [of Num.One n] by simp
   1.808 +
   1.809 +
   1.810 +subsubsection \<open>Further properties\<close>
   1.811 +
   1.812 +text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
   1.813 +
   1.814 +lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   1.815 +  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
   1.816 +
   1.817 +lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   1.818 +  by (rule div_int_unique [of a b q r],
   1.819 +    simp add: divmod_int_rel_def)
   1.820 +
   1.821 +lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   1.822 +  by (rule mod_int_unique [of a b q r],
   1.823 +    simp add: divmod_int_rel_def)
   1.824 +
   1.825 +lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.826 +  by (rule mod_int_unique [of a b q r],
   1.827 +    simp add: divmod_int_rel_def)
   1.828  
   1.829  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
   1.830  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
   1.831 @@ -2766,88 +2529,92 @@
   1.832    thus  ?lhs by simp
   1.833  qed
   1.834  
   1.835 +subsubsection \<open>Dedicated simproc for calculation\<close>
   1.836 +
   1.837  text \<open>
   1.838 -  This re-embedding of natural division on integers goes back to the
   1.839 -  time when numerals had been signed numerals.  It should
   1.840 -  now be replaced by the algorithm developed in @{class semiring_numeral_div}.
   1.841 +  There is space for improvement here: the calculation itself
   1.842 +  could be carried outside the logic, and a generic simproc
   1.843 +  (simplifier setup) for generic calculation would be helpful. 
   1.844  \<close>
   1.845  
   1.846 -lemma div_nat_numeral [simp]:
   1.847 -  "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
   1.848 -  by (subst nat_div_distrib) simp_all
   1.849 -
   1.850 -lemma one_div_nat_numeral [simp]:
   1.851 -  "Suc 0 div numeral v' = nat (1 div numeral v')"
   1.852 -  by (subst nat_div_distrib) simp_all
   1.853 -
   1.854 -lemma mod_nat_numeral [simp]:
   1.855 -  "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
   1.856 -  by (subst nat_mod_distrib) simp_all
   1.857 -
   1.858 -lemma one_mod_nat_numeral [simp]:
   1.859 -  "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   1.860 -  by (subst nat_mod_distrib) simp_all
   1.861 -
   1.862 -
   1.863 -subsubsection \<open>Tools setup\<close>
   1.864 -
   1.865 -text \<open>Nitpick\<close>
   1.866 -
   1.867 -lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
   1.868 +simproc_setup numeral_divmod
   1.869 +  ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
   1.870 +   "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
   1.871 +   "0 div - 1 :: int" | "0 mod - 1 :: int" |
   1.872 +   "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
   1.873 +   "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
   1.874 +   "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
   1.875 +   "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
   1.876 +   "1 div - 1 :: int" | "1 mod - 1 :: int" |
   1.877 +   "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
   1.878 +   "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
   1.879 +   "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
   1.880 +   "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
   1.881 +   "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
   1.882 +   "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
   1.883 +   "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
   1.884 +   "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
   1.885 +   "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
   1.886 +   "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
   1.887 +   "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
   1.888 +   "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
   1.889 +   "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
   1.890 +   "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
   1.891 +   "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
   1.892 +\<open> let
   1.893 +    val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
   1.894 +    fun successful_rewrite ctxt ct =
   1.895 +      let
   1.896 +        val thm = Simplifier.rewrite ctxt ct
   1.897 +      in if Thm.is_reflexive thm then NONE else SOME thm end;
   1.898 +  in fn phi =>
   1.899 +    let
   1.900 +      val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
   1.901 +        one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
   1.902 +        one_div_minus_numeral one_mod_minus_numeral
   1.903 +        numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
   1.904 +        numeral_div_minus_numeral numeral_mod_minus_numeral
   1.905 +        div_minus_minus mod_minus_minus adjust_div_eq of_bool_eq one_neq_zero
   1.906 +        numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
   1.907 +        divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
   1.908 +        case_prod_beta rel_simps adjust_mod_def div_minus1_right mod_minus1_right
   1.909 +        minus_minus numeral_times_numeral mult_zero_right mult_1_right}
   1.910 +        @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
   1.911 +      fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
   1.912 +        (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
   1.913 +    in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
   1.914 +  end;
   1.915 +\<close>
   1.916  
   1.917  
   1.918  subsubsection \<open>Code generation\<close>
   1.919  
   1.920 -definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
   1.921 -where
   1.922 -  "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
   1.923 -
   1.924 -lemma fst_divmod_abs [simp]:
   1.925 -  "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
   1.926 -  by (simp add: divmod_abs_def)
   1.927 -
   1.928 -lemma snd_divmod_abs [simp]:
   1.929 -  "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
   1.930 -  by (simp add: divmod_abs_def)
   1.931 -
   1.932 -lemma divmod_abs_code [code]:
   1.933 -  "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
   1.934 -  "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
   1.935 -  "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
   1.936 -  "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
   1.937 -  "divmod_abs j 0 = (0, \<bar>j\<bar>)"
   1.938 -  "divmod_abs 0 j = (0, 0)"
   1.939 -  by (simp_all add: prod_eq_iff)
   1.940 -
   1.941 -lemma divmod_int_divmod_abs:
   1.942 -  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
   1.943 -  apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
   1.944 -    then divmod_abs k l
   1.945 -    else (let (r, s) = divmod_abs k l in
   1.946 -       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.947 -proof -
   1.948 -  have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
   1.949 -  show ?thesis
   1.950 -    by (simp add: prod_eq_iff split_def Let_def)
   1.951 -      (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
   1.952 -      zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
   1.953 -qed
   1.954 -
   1.955 -lemma divmod_int_code [code]:
   1.956 -  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
   1.957 -  apsnd ((op *) (sgn l)) (if sgn k = sgn l
   1.958 -    then divmod_abs k l
   1.959 -    else (let (r, s) = divmod_abs k l in
   1.960 -      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.961 -proof -
   1.962 -  have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
   1.963 -    by (auto simp add: not_less sgn_if)
   1.964 -  then show ?thesis by (simp add: divmod_int_divmod_abs)
   1.965 -qed
   1.966 -
   1.967 -hide_const (open) divmod_abs
   1.968 +lemma [code]:
   1.969 +  fixes k :: int
   1.970 +  shows 
   1.971 +    "k div 0 = 0"
   1.972 +    "k mod 0 = k"
   1.973 +    "0 div k = 0"
   1.974 +    "0 mod k = 0"
   1.975 +    "k div Int.Pos Num.One = k"
   1.976 +    "k mod Int.Pos Num.One = 0"
   1.977 +    "k div Int.Neg Num.One = - k"
   1.978 +    "k mod Int.Neg Num.One = 0"
   1.979 +    "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
   1.980 +    "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
   1.981 +    "Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
   1.982 +    "Int.Neg m mod Int.Pos n = adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
   1.983 +    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
   1.984 +    "Int.Pos m mod Int.Neg n = - adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
   1.985 +    "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
   1.986 +    "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
   1.987 +  by simp_all
   1.988  
   1.989  code_identifier
   1.990    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.991  
   1.992 +lemma dvd_eq_mod_eq_0_numeral:
   1.993 +  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   1.994 +  by (fact dvd_eq_mod_eq_0)
   1.995 +
   1.996  end