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.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.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.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.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.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.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.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.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.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.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.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.668 +
1.669 +lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
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.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.750 +  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
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.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.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.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.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.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.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.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.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
`