1(* Title: HOL/Divides.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1999 University of Cambridge 4*) 5 6section \<open>More on quotient and remainder\<close> 7 8theory Divides 9imports Parity 10begin 11 12subsection \<open>More on division\<close> 13 14inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" 15 where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)" 16 | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)" 17 | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar> 18 \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)" 19 20lemma eucl_rel_int_iff: 21 "eucl_rel_int k l (q, r) \<longleftrightarrow> 22 k = l * q + r \<and> 23 (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)" 24 by (cases "r = 0") 25 (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI 26 simp add: ac_simps sgn_1_pos sgn_1_neg) 27 28lemma unique_quotient_lemma: 29 assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)" 30proof - 31 have "r' + b * (q'-q) \<le> r" 32 using assms by (simp add: right_diff_distrib) 33 moreover have "0 < b * (1 + q - q') " 34 using assms by (simp add: right_diff_distrib distrib_left) 35 moreover have "b * q' < b * (1 + q)" 36 using assms by (simp add: right_diff_distrib distrib_left) 37 ultimately show ?thesis 38 using assms by (simp add: mult_less_cancel_left) 39qed 40 41lemma unique_quotient_lemma_neg: 42 "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)" 43 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto 44 45lemma unique_quotient: 46 "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'" 47 apply (rule order_antisym) 48 apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm) 49 apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+ 50 done 51 52lemma unique_remainder: 53 "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'" 54apply (subgoal_tac "q = q'") 55 apply (simp add: eucl_rel_int_iff) 56apply (blast intro: unique_quotient) 57done 58 59lemma eucl_rel_int: 60 "eucl_rel_int k l (k div l, k mod l)" 61proof (cases k rule: int_cases3) 62 case zero 63 then show ?thesis 64 by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def) 65next 66 case (pos n) 67 then show ?thesis 68 using div_mult_mod_eq [of n] 69 by (cases l rule: int_cases3) 70 (auto simp del: of_nat_mult of_nat_add 71 simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps 72 eucl_rel_int_iff divide_int_def modulo_int_def) 73next 74 case (neg n) 75 then show ?thesis 76 using div_mult_mod_eq [of n] 77 by (cases l rule: int_cases3) 78 (auto simp del: of_nat_mult of_nat_add 79 simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps 80 eucl_rel_int_iff divide_int_def modulo_int_def) 81qed 82 83lemma divmod_int_unique: 84 assumes "eucl_rel_int k l (q, r)" 85 shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r" 86 using assms eucl_rel_int [of k l] 87 using unique_quotient [of k l] unique_remainder [of k l] 88 by auto 89 90lemma div_abs_eq_div_nat: 91 "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)" 92 by (simp add: divide_int_def) 93 94lemma mod_abs_eq_div_nat: 95 "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)" 96 by (simp add: modulo_int_def) 97 98lemma zdiv_int: 99 "int (a div b) = int a div int b" 100 by (simp add: divide_int_def) 101 102lemma zmod_int: 103 "int (a mod b) = int a mod int b" 104 by (simp add: modulo_int_def) 105 106lemma div_sgn_abs_cancel: 107 fixes k l v :: int 108 assumes "v \<noteq> 0" 109 shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>" 110proof - 111 from assms have "sgn v = - 1 \<or> sgn v = 1" 112 by (cases "v \<ge> 0") auto 113 then show ?thesis 114 using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"] 115 by (fastforce simp add: not_less div_abs_eq_div_nat) 116qed 117 118lemma div_eq_sgn_abs: 119 fixes k l v :: int 120 assumes "sgn k = sgn l" 121 shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>" 122proof (cases "l = 0") 123 case True 124 then show ?thesis 125 by simp 126next 127 case False 128 with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>" 129 using div_sgn_abs_cancel [of l k l] by simp 130 then show ?thesis 131 by (simp add: sgn_mult_abs) 132qed 133 134lemma div_dvd_sgn_abs: 135 fixes k l :: int 136 assumes "l dvd k" 137 shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)" 138proof (cases "k = 0 \<or> l = 0") 139 case True 140 then show ?thesis 141 by auto 142next 143 case False 144 then have "k \<noteq> 0" and "l \<noteq> 0" 145 by auto 146 show ?thesis 147 proof (cases "sgn l = sgn k") 148 case True 149 then show ?thesis 150 by (simp add: div_eq_sgn_abs) 151 next 152 case False 153 with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close> 154 have "sgn l * sgn k = - 1" 155 by (simp add: sgn_if split: if_splits) 156 with assms show ?thesis 157 unfolding divide_int_def [of k l] 158 by (auto simp add: zdiv_int ac_simps) 159 qed 160qed 161 162lemma div_noneq_sgn_abs: 163 fixes k l :: int 164 assumes "l \<noteq> 0" 165 assumes "sgn k \<noteq> sgn l" 166 shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)" 167 using assms 168 by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int) 169 170 171subsubsection \<open>General Properties of div and mod\<close> 172 173lemma div_pos_pos_trivial [simp]: 174 "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int 175 using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) 176 177lemma mod_pos_pos_trivial [simp]: 178 "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int 179 using that by (simp add: mod_eq_self_iff_div_eq_0) 180 181lemma div_neg_neg_trivial [simp]: 182 "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int 183 using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) 184 185lemma mod_neg_neg_trivial [simp]: 186 "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int 187 using that by (simp add: mod_eq_self_iff_div_eq_0) 188 189lemma div_pos_neg_trivial: 190 "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int 191 apply (rule div_int_unique [of _ _ _ "k + l"]) 192 apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>) 193 done 194 195lemma mod_pos_neg_trivial: 196 "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int 197 apply (rule mod_int_unique [of _ _ "- 1"]) 198 apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>) 199 done 200 201text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close> 202 because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close> 203 204 205 206subsubsection \<open>Laws for div and mod with Unary Minus\<close> 207 208lemma zminus1_lemma: 209 "eucl_rel_int a b (q, r) ==> b \<noteq> 0 210 ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1, 211 if r=0 then 0 else b-r)" 212by (force simp add: eucl_rel_int_iff right_diff_distrib) 213 214 215lemma zdiv_zminus1_eq_if: 216 "b \<noteq> (0::int) 217 \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)" 218by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique]) 219 220lemma zmod_zminus1_eq_if: 221 "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" 222proof (cases "b = 0") 223 case False 224 then show ?thesis 225 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique]) 226qed auto 227 228lemma zmod_zminus1_not_zero: 229 fixes k l :: int 230 shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" 231 by (simp add: mod_eq_0_iff_dvd) 232 233lemma zmod_zminus2_not_zero: 234 fixes k l :: int 235 shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" 236 by (simp add: mod_eq_0_iff_dvd) 237 238lemma zdiv_zminus2_eq_if: 239 "b \<noteq> (0::int) 240 ==> a div (-b) = 241 (if a mod b = 0 then - (a div b) else - (a div b) - 1)" 242 by (auto simp add: zdiv_zminus1_eq_if div_minus_right) 243 244lemma zmod_zminus2_eq_if: 245 "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" 246 by (auto simp add: zmod_zminus1_eq_if mod_minus_right) 247 248 249subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close> 250 251lemma zdiv_mono1: 252 fixes b::int 253 assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b" 254proof (rule unique_quotient_lemma) 255 show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b" 256 using assms(1) by auto 257qed (use assms in auto) 258 259lemma zdiv_mono1_neg: 260 fixes b::int 261 assumes "a \<le> a'" "b < 0" shows "a' div b \<le> a div b" 262proof (rule unique_quotient_lemma_neg) 263 show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b" 264 using assms(1) by auto 265qed (use assms in auto) 266 267 268subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close> 269 270lemma q_pos_lemma: 271 fixes q'::int 272 assumes "0 \<le> b'*q' + r'" "r' < b'" "0 < b'" 273 shows "0 \<le> q'" 274proof - 275 have "0 < b'* (q' + 1)" 276 using assms by (simp add: distrib_left) 277 with assms show ?thesis 278 by (simp add: zero_less_mult_iff) 279qed 280 281lemma zdiv_mono2_lemma: 282 fixes q'::int 283 assumes eq: "b*q + r = b'*q' + r'" and le: "0 \<le> b'*q' + r'" and "r' < b'" "0 \<le> r" "0 < b'" "b' \<le> b" 284 shows "q \<le> q'" 285proof - 286 have "0 \<le> q'" 287 using q_pos_lemma le \<open>r' < b'\<close> \<open>0 < b'\<close> by blast 288 moreover have "b*q = r' - r + b'*q'" 289 using eq by linarith 290 ultimately have "b*q < b* (q' + 1)" 291 using mult_right_mono assms unfolding distrib_left by fastforce 292 with assms show ?thesis 293 by (simp add: mult_less_cancel_left_pos) 294qed 295 296lemma zdiv_mono2: 297 fixes a::int 298 assumes "0 \<le> a" "0 < b'" "b' \<le> b" shows "a div b \<le> a div b'" 299proof (rule zdiv_mono2_lemma) 300 have "b \<noteq> 0" 301 using assms by linarith 302 show "b * (a div b) + a mod b = b' * (a div b') + a mod b'" 303 by simp 304qed (use assms in auto) 305 306lemma zdiv_mono2_neg_lemma: 307 fixes q'::int 308 assumes "b*q + r = b'*q' + r'" "b'*q' + r' < 0" "r < b" "0 \<le> r'" "0 < b'" "b' \<le> b" 309 shows "q' \<le> q" 310proof - 311 have "b'*q' < 0" 312 using assms by linarith 313 with assms have "q' \<le> 0" 314 by (simp add: mult_less_0_iff) 315 have "b*q' \<le> b'*q'" 316 by (simp add: \<open>q' \<le> 0\<close> assms(6) mult_right_mono_neg) 317 then have "b*q' < b* (q + 1)" 318 using assms by (simp add: distrib_left) 319 then show ?thesis 320 using assms by (simp add: mult_less_cancel_left) 321qed 322 323lemma zdiv_mono2_neg: 324 fixes a::int 325 assumes "a < 0" "0 < b'" "b' \<le> b" shows "a div b' \<le> a div b" 326proof (rule zdiv_mono2_neg_lemma) 327 have "b \<noteq> 0" 328 using assms by linarith 329 show "b * (a div b) + a mod b = b' * (a div b') + a mod b'" 330 by simp 331qed (use assms in auto) 332 333lemma div_pos_geq: 334 fixes k l :: int 335 assumes "0 < l" and "l \<le> k" 336 shows "k div l = (k - l) div l + 1" 337proof - 338 have "k = (k - l) + l" by simp 339 then obtain j where k: "k = j + l" .. 340 with assms show ?thesis by (simp add: div_add_self2) 341qed 342 343lemma mod_pos_geq: 344 fixes k l :: int 345 assumes "0 < l" and "l \<le> k" 346 shows "k mod l = (k - l) mod l" 347proof - 348 have "k = (k - l) + l" by simp 349 then obtain j where k: "k = j + l" .. 350 with assms show ?thesis by simp 351qed 352 353 354subsubsection \<open>Splitting Rules for div and mod\<close> 355 356text\<open>The proofs of the two lemmas below are essentially identical\<close> 357 358lemma split_pos_lemma: 359 "0<k \<Longrightarrow> 360 P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i j)" 361 by auto 362 363lemma split_neg_lemma: 364 "k<0 \<Longrightarrow> 365 P(n div k :: int)(n mod k) = (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i j)" 366 by auto 367 368lemma split_zdiv: 369 "P(n div k :: int) = 370 ((k = 0 \<longrightarrow> P 0) \<and> 371 (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i)) \<and> 372 (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i)))" 373proof (cases "k = 0") 374 case False 375 then show ?thesis 376 unfolding linorder_neq_iff 377 by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P x"] split_neg_lemma [of concl: "\<lambda>x y. P x"]) 378qed auto 379 380lemma split_zmod: 381 "P(n mod k :: int) = 382 ((k = 0 \<longrightarrow> P n) \<and> 383 (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P j)) \<and> 384 (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P j)))" 385proof (cases "k = 0") 386 case False 387 then show ?thesis 388 unfolding linorder_neq_iff 389 by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P y"] split_neg_lemma [of concl: "\<lambda>x y. P y"]) 390qed auto 391 392text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close> 393 when these are applied to some constant that is of the form 394 \<^term>\<open>numeral k\<close>:\<close> 395declare split_zdiv [of _ _ "numeral k", arith_split] for k 396declare split_zmod [of _ _ "numeral k", arith_split] for k 397 398 399subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close> 400 401lemma pos_eucl_rel_int_mult_2: 402 assumes "0 \<le> b" 403 assumes "eucl_rel_int a b (q, r)" 404 shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)" 405 using assms unfolding eucl_rel_int_iff by auto 406 407lemma neg_eucl_rel_int_mult_2: 408 assumes "b \<le> 0" 409 assumes "eucl_rel_int (a + 1) b (q, r)" 410 shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)" 411 using assms unfolding eucl_rel_int_iff by auto 412 413text\<open>computing div by shifting\<close> 414 415lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a" 416 using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int] 417 by (rule div_int_unique) 418 419lemma neg_zdiv_mult_2: 420 assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a" 421 using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int] 422 by (rule div_int_unique) 423 424lemma zdiv_numeral_Bit0 [simp]: 425 "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) = 426 numeral v div (numeral w :: int)" 427 unfolding numeral.simps unfolding mult_2 [symmetric] 428 by (rule div_mult_mult1, simp) 429 430lemma zdiv_numeral_Bit1 [simp]: 431 "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) = 432 (numeral v div (numeral w :: int))" 433 unfolding numeral.simps 434 unfolding mult_2 [symmetric] add.commute [of _ 1] 435 by (rule pos_zdiv_mult_2, simp) 436 437lemma pos_zmod_mult_2: 438 fixes a b :: int 439 assumes "0 \<le> a" 440 shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)" 441 using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int] 442 by (rule mod_int_unique) 443 444lemma neg_zmod_mult_2: 445 fixes a b :: int 446 assumes "a \<le> 0" 447 shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1" 448 using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int] 449 by (rule mod_int_unique) 450 451lemma zmod_numeral_Bit0 [simp]: 452 "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) = 453 (2::int) * (numeral v mod numeral w)" 454 unfolding numeral_Bit0 [of v] numeral_Bit0 [of w] 455 unfolding mult_2 [symmetric] by (rule mod_mult_mult1) 456 457lemma zmod_numeral_Bit1 [simp]: 458 "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) = 459 2 * (numeral v mod numeral w) + (1::int)" 460 unfolding numeral_Bit1 [of v] numeral_Bit0 [of w] 461 unfolding mult_2 [symmetric] add.commute [of _ 1] 462 by (rule pos_zmod_mult_2, simp) 463 464lemma zdiv_eq_0_iff: 465 "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R") 466 for i k :: int 467proof 468 assume ?L 469 moreover have "?L \<longrightarrow> ?R" 470 by (rule split_zdiv [THEN iffD2]) simp 471 ultimately show ?R 472 by blast 473next 474 assume ?R then show ?L 475 by auto 476qed 477 478lemma zmod_trival_iff: 479 fixes i k :: int 480 shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" 481proof - 482 have "i mod k = i \<longleftrightarrow> i div k = 0" 483 by safe (insert div_mult_mod_eq [of i k], auto) 484 with zdiv_eq_0_iff 485 show ?thesis 486 by simp 487qed 488 489 490subsubsection \<open>Quotients of Signs\<close> 491 492lemma div_eq_minus1: "0 < b \<Longrightarrow> - 1 div b = - 1" for b :: int 493 by (simp add: divide_int_def) 494 495lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int 496 by (auto simp add: modulo_int_def) 497 498lemma div_neg_pos_less0: 499 fixes a::int 500 assumes "a < 0" "0 < b" 501 shows "a div b < 0" 502proof - 503 have "a div b \<le> - 1 div b" 504 using zdiv_mono1 assms by auto 505 also have "... \<le> -1" 506 by (simp add: assms(2) div_eq_minus1) 507 finally show ?thesis 508 by force 509qed 510 511lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0" 512 by (drule zdiv_mono1_neg, auto) 513 514lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0" 515 by (drule zdiv_mono1, auto) 516 517text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close> 518conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more. 519They should all be simp rules unless that causes too much search.\<close> 520 521lemma pos_imp_zdiv_nonneg_iff: 522 fixes a::int 523 assumes "0 < b" 524 shows "(0 \<le> a div b) = (0 \<le> a)" 525proof 526 show "0 \<le> a div b \<Longrightarrow> 0 \<le> a" 527 using assms 528 by (simp add: linorder_not_less [symmetric]) (blast intro: div_neg_pos_less0) 529next 530 assume "0 \<le> a" 531 then have "0 div b \<le> a div b" 532 using zdiv_mono1 assms by blast 533 then show "0 \<le> a div b" 534 by auto 535qed 536 537lemma pos_imp_zdiv_pos_iff: 538 "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i" 539 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith 540 541 542lemma neg_imp_zdiv_nonneg_iff: 543 fixes a::int 544 assumes "b < 0" 545 shows "(0 \<le> a div b) = (a \<le> 0)" 546 using assms by (simp add: div_minus_minus [of a, symmetric] pos_imp_zdiv_nonneg_iff del: div_minus_minus) 547 548(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*) 549lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)" 550 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff) 551 552(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*) 553lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)" 554 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff) 555 556lemma nonneg1_imp_zdiv_pos_iff: 557 fixes a::int 558 assumes "0 \<le> a" 559 shows "a div b > 0 \<longleftrightarrow> a \<ge> b \<and> b>0" 560proof - 561 have "0 < a div b \<Longrightarrow> b \<le> a" 562 using div_pos_pos_trivial[of a b] assms by arith 563 moreover have "0 < a div b \<Longrightarrow> b > 0" 564 using assms div_nonneg_neg_le0[of a b] by(cases "b=0"; force) 565 moreover have "b \<le> a \<and> 0 < b \<Longrightarrow> 0 < a div b" 566 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b] by simp 567 ultimately show ?thesis 568 by blast 569qed 570 571lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 \<Longrightarrow> m mod k \<le> m" 572 by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le) 573 574 575subsubsection \<open>Further properties\<close> 576 577lemma div_int_pos_iff: 578 "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0 579 \<or> k < 0 \<and> l < 0" 580 for k l :: int 581proof (cases "k = 0 \<or> l = 0") 582 case False 583 then show ?thesis 584 apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff) 585 by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq) 586qed auto 587 588lemma mod_int_pos_iff: 589 "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0" 590 for k l :: int 591proof (cases "l > 0") 592 case False 593 then show ?thesis 594 by (simp add: dvd_eq_mod_eq_0) (use neg_mod_sign [of l k] in \<open>auto simp add: le_less not_less\<close>) 595qed auto 596 597text \<open>Simplify expressions in which div and mod combine numerical constants\<close> 598 599lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q" 600 by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff) 601 602lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q" 603 by (rule div_int_unique [of a b q r], 604 simp add: eucl_rel_int_iff) 605 606lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r" 607 by (rule mod_int_unique [of a b q r], 608 simp add: eucl_rel_int_iff) 609 610lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r" 611 by (rule mod_int_unique [of a b q r], 612 simp add: eucl_rel_int_iff) 613 614lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>" 615 unfolding dvd_def by (cases "y=0") (auto simp add: abs_mult) 616 617text\<open>Suggested by Matthias Daum\<close> 618lemma int_power_div_base: 619 fixes k :: int 620 assumes "0 < m" "0 < k" 621 shows "k ^ m div k = (k::int) ^ (m - Suc 0)" 622proof - 623 have eq: "k ^ m = k ^ ((m - Suc 0) + Suc 0)" 624 by (simp add: assms) 625 show ?thesis 626 using assms by (simp only: power_add eq) auto 627qed 628 629text \<open>Distributive laws for function \<open>nat\<close>.\<close> 630 631lemma nat_div_distrib: 632 assumes "0 \<le> x" 633 shows "nat (x div y) = nat x div nat y" 634proof (cases y "0::int" rule: linorder_cases) 635 case less 636 with assms show ?thesis 637 using div_nonneg_neg_le0 by auto 638next 639 case greater 640 then show ?thesis 641 by (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int) 642qed auto 643 644(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*) 645lemma nat_mod_distrib: 646 assumes "0 \<le> x" "0 \<le> y" 647 shows "nat (x mod y) = nat x mod nat y" 648proof (cases "y = 0") 649 case False 650 with assms show ?thesis 651 by (simp add: nat_eq_iff zmod_int) 652qed auto 653 654text\<open>Suggested by Matthias Daum\<close> 655lemma int_div_less_self: 656 fixes x::int 657 assumes "0 < x" "1 < k" 658 shows "x div k < x" 659proof - 660 have "nat x div nat k < nat x" 661 by (simp add: assms) 662 with assms show ?thesis 663 by (simp add: nat_div_distrib [symmetric]) 664qed 665 666lemma mod_eq_dvd_iff_nat: 667 "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat 668proof - 669 have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n" 670 by (simp add: mod_eq_dvd_iff) 671 with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)" 672 by (simp only: of_nat_mod of_nat_diff) 673 then show ?thesis 674 by simp 675qed 676 677lemma mod_eq_nat1E: 678 fixes m n q :: nat 679 assumes "m mod q = n mod q" and "m \<ge> n" 680 obtains s where "m = n + q * s" 681proof - 682 from assms have "q dvd m - n" 683 by (simp add: mod_eq_dvd_iff_nat) 684 then obtain s where "m - n = q * s" .. 685 with \<open>m \<ge> n\<close> have "m = n + q * s" 686 by simp 687 with that show thesis . 688qed 689 690lemma mod_eq_nat2E: 691 fixes m n q :: nat 692 assumes "m mod q = n mod q" and "n \<ge> m" 693 obtains s where "n = m + q * s" 694 using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps) 695 696lemma nat_mod_eq_lemma: 697 assumes "(x::nat) mod n = y mod n" and "y \<le> x" 698 shows "\<exists>q. x = y + n * q" 699 using assms by (rule mod_eq_nat1E) rule 700 701lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 702 (is "?lhs = ?rhs") 703proof 704 assume H: "x mod n = y mod n" 705 {assume xy: "x \<le> y" 706 from H have th: "y mod n = x mod n" by simp 707 from nat_mod_eq_lemma[OF th xy] have ?rhs 708 apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)} 709 moreover 710 {assume xy: "y \<le> x" 711 from nat_mod_eq_lemma[OF H xy] have ?rhs 712 apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)} 713 ultimately show ?rhs using linear[of x y] by blast 714next 715 assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast 716 hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp 717 thus ?lhs by simp 718qed 719 720 721subsection \<open>Numeral division with a pragmatic type class\<close> 722 723text \<open> 724 The following type class contains everything necessary to formulate 725 a division algorithm in ring structures with numerals, restricted 726 to its positive segments. This is its primary motivation, and it 727 could surely be formulated using a more fine-grained, more algebraic 728 and less technical class hierarchy. 729\<close> 730 731class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom + 732 assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0" 733 and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a" 734 and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0" 735 and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a" 736 and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b" 737 and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b" 738 and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b" 739 and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c" 740 assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b" 741 fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a" 742 and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a" 743 assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)" 744 and divmod_step_def: "divmod_step l qr = (let (q, r) = qr 745 in if r \<ge> numeral l then (2 * q + 1, r - numeral l) 746 else (2 * q, r))" 747 \<comment> \<open>These are conceptually definitions but force generated code 748 to be monomorphic wrt. particular instances of this class which 749 yields a significant speedup.\<close> 750begin 751 752lemma divmod_digit_1: 753 assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)" 754 shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P") 755 and "a mod (2 * b) - b = a mod b" (is "?Q") 756proof - 757 from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a" 758 by (auto intro: trans) 759 with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive) 760 then have [simp]: "1 \<le> a div b" by (simp add: discrete) 761 with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound) 762 define w where "w = a div b mod 2" 763 then have w_exhaust: "w = 0 \<or> w = 1" by auto 764 have mod_w: "a mod (2 * b) = a mod b + b * w" 765 by (simp add: w_def mod_mult2_eq ac_simps) 766 from assms w_exhaust have "w = 1" 767 by (auto simp add: mod_w) (insert mod_less, auto) 768 with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp 769 have "2 * (a div (2 * b)) = a div b - w" 770 by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps) 771 with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp 772 then show ?P and ?Q 773 by (simp_all add: div mod add_implies_diff [symmetric]) 774qed 775 776lemma divmod_digit_0: 777 assumes "0 < b" and "a mod (2 * b) < b" 778 shows "2 * (a div (2 * b)) = a div b" (is "?P") 779 and "a mod (2 * b) = a mod b" (is "?Q") 780proof - 781 define w where "w = a div b mod 2" 782 then have w_exhaust: "w = 0 \<or> w = 1" by auto 783 have mod_w: "a mod (2 * b) = a mod b + b * w" 784 by (simp add: w_def mod_mult2_eq ac_simps) 785 moreover have "b \<le> a mod b + b" 786 proof - 787 from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast 788 then have "0 + b \<le> a mod b + b" by (rule add_right_mono) 789 then show ?thesis by simp 790 qed 791 moreover note assms w_exhaust 792 ultimately have "w = 0" by auto 793 with mod_w have mod: "a mod (2 * b) = a mod b" by simp 794 have "2 * (a div (2 * b)) = a div b - w" 795 by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps) 796 with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp 797 then show ?P and ?Q 798 by (simp_all add: div mod) 799qed 800 801lemma mod_double_modulus: 802 assumes "m > 0" "x \<ge> 0" 803 shows "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m" 804proof (cases "x mod (2 * m) < m") 805 case True 806 thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto 807next 808 case False 809 hence *: "x mod (2 * m) - m = x mod m" 810 using assms by (intro divmod_digit_1) auto 811 hence "x mod (2 * m) = x mod m + m" 812 by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto) 813 thus ?thesis by simp 814qed 815 816lemma fst_divmod: 817 "fst (divmod m n) = numeral m div numeral n" 818 by (simp add: divmod_def) 819 820lemma snd_divmod: 821 "snd (divmod m n) = numeral m mod numeral n" 822 by (simp add: divmod_def) 823 824text \<open> 825 This is a formulation of one step (referring to one digit position) 826 in school-method division: compare the dividend at the current 827 digit position with the remainder from previous division steps 828 and evaluate accordingly. 829\<close> 830 831lemma divmod_step_eq [simp]: 832 "divmod_step l (q, r) = (if numeral l \<le> r 833 then (2 * q + 1, r - numeral l) else (2 * q, r))" 834 by (simp add: divmod_step_def) 835 836text \<open> 837 This is a formulation of school-method division. 838 If the divisor is smaller than the dividend, terminate. 839 If not, shift the dividend to the right until termination 840 occurs and then reiterate single division steps in the 841 opposite direction. 842\<close> 843 844lemma divmod_divmod_step: 845 "divmod m n = (if m < n then (0, numeral m) 846 else divmod_step n (divmod m (Num.Bit0 n)))" 847proof (cases "m < n") 848 case True then have "numeral m < numeral n" by simp 849 then show ?thesis 850 by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod) 851next 852 case False 853 have "divmod m n = 854 divmod_step n (numeral m div (2 * numeral n), 855 numeral m mod (2 * numeral n))" 856 proof (cases "numeral n \<le> numeral m mod (2 * numeral n)") 857 case True 858 with divmod_step_eq 859 have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = 860 (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)" 861 by simp 862 moreover from True divmod_digit_1 [of "numeral m" "numeral n"] 863 have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n" 864 and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n" 865 by simp_all 866 ultimately show ?thesis by (simp only: divmod_def) 867 next 868 case False then have *: "numeral m mod (2 * numeral n) < numeral n" 869 by (simp add: not_le) 870 with divmod_step_eq 871 have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) = 872 (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))" 873 by auto 874 moreover from * divmod_digit_0 [of "numeral n" "numeral m"] 875 have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n" 876 and "numeral m mod (2 * numeral n) = numeral m mod numeral n" 877 by (simp_all only: zero_less_numeral) 878 ultimately show ?thesis by (simp only: divmod_def) 879 qed 880 then have "divmod m n = 881 divmod_step n (numeral m div numeral (Num.Bit0 n), 882 numeral m mod numeral (Num.Bit0 n))" 883 by (simp only: numeral.simps distrib mult_1) 884 then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))" 885 by (simp add: divmod_def) 886 with False show ?thesis by simp 887qed 888 889text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close> 890 891lemma divmod_trivial [simp]: 892 "divmod Num.One Num.One = (numeral Num.One, 0)" 893 "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)" 894 "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)" 895 "divmod num.One (num.Bit0 n) = (0, Numeral1)" 896 "divmod num.One (num.Bit1 n) = (0, Numeral1)" 897 using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def) 898 899text \<open>Division by an even number is a right-shift\<close> 900 901lemma divmod_cancel [simp]: 902 "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P) 903 "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q) 904proof - 905 have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q" 906 "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1" 907 by (simp_all only: numeral_mult numeral.simps distrib) simp_all 908 have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less) 909 then show ?P and ?Q 910 by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1 911 div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] 912 add.commute del: numeral_times_numeral) 913qed 914 915text \<open>The really hard work\<close> 916 917lemma divmod_steps [simp]: 918 "divmod (num.Bit0 m) (num.Bit1 n) = 919 (if m \<le> n then (0, numeral (num.Bit0 m)) 920 else divmod_step (num.Bit1 n) 921 (divmod (num.Bit0 m) 922 (num.Bit0 (num.Bit1 n))))" 923 "divmod (num.Bit1 m) (num.Bit1 n) = 924 (if m < n then (0, numeral (num.Bit1 m)) 925 else divmod_step (num.Bit1 n) 926 (divmod (num.Bit1 m) 927 (num.Bit0 (num.Bit1 n))))" 928 by (simp_all add: divmod_divmod_step) 929 930lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps 931 932text \<open>Special case: divisibility\<close> 933 934definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool" 935where 936 "divides_aux qr \<longleftrightarrow> snd qr = 0" 937 938lemma divides_aux_eq [simp]: 939 "divides_aux (q, r) \<longleftrightarrow> r = 0" 940 by (simp add: divides_aux_def) 941 942lemma dvd_numeral_simp [simp]: 943 "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)" 944 by (simp add: divmod_def mod_eq_0_iff_dvd) 945 946text \<open>Generic computation of quotient and remainder\<close> 947 948lemma numeral_div_numeral [simp]: 949 "numeral k div numeral l = fst (divmod k l)" 950 by (simp add: fst_divmod) 951 952lemma numeral_mod_numeral [simp]: 953 "numeral k mod numeral l = snd (divmod k l)" 954 by (simp add: snd_divmod) 955 956lemma one_div_numeral [simp]: 957 "1 div numeral n = fst (divmod num.One n)" 958 by (simp add: fst_divmod) 959 960lemma one_mod_numeral [simp]: 961 "1 mod numeral n = snd (divmod num.One n)" 962 by (simp add: snd_divmod) 963 964text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close> 965 966lemma cong_exp_iff_simps: 967 "numeral n mod numeral Num.One = 0 968 \<longleftrightarrow> True" 969 "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0 970 \<longleftrightarrow> numeral n mod numeral q = 0" 971 "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0 972 \<longleftrightarrow> False" 973 "numeral m mod numeral Num.One = (numeral n mod numeral Num.One) 974 \<longleftrightarrow> True" 975 "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) 976 \<longleftrightarrow> True" 977 "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) 978 \<longleftrightarrow> False" 979 "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) 980 \<longleftrightarrow> (numeral n mod numeral q) = 0" 981 "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) 982 \<longleftrightarrow> False" 983 "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) 984 \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)" 985 "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) 986 \<longleftrightarrow> False" 987 "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) 988 \<longleftrightarrow> (numeral m mod numeral q) = 0" 989 "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) 990 \<longleftrightarrow> False" 991 "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) 992 \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)" 993 by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even]) 994 995end 996 997hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq 998 999instantiation nat :: unique_euclidean_semiring_numeral 1000begin 1001 1002definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat" 1003where 1004 divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)" 1005 1006definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" 1007where 1008 "divmod_step_nat l qr = (let (q, r) = qr 1009 in if r \<ge> numeral l then (2 * q + 1, r - numeral l) 1010 else (2 * q, r))" 1011 1012instance by standard 1013 (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq) 1014 1015end 1016 1017declare divmod_algorithm_code [where ?'a = nat, code] 1018 1019lemma Suc_0_div_numeral [simp]: 1020 fixes k l :: num 1021 shows "Suc 0 div numeral k = fst (divmod Num.One k)" 1022 by (simp_all add: fst_divmod) 1023 1024lemma Suc_0_mod_numeral [simp]: 1025 fixes k l :: num 1026 shows "Suc 0 mod numeral k = snd (divmod Num.One k)" 1027 by (simp_all add: snd_divmod) 1028 1029instantiation int :: unique_euclidean_semiring_numeral 1030begin 1031 1032definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int" 1033where 1034 "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)" 1035 1036definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" 1037where 1038 "divmod_step_int l qr = (let (q, r) = qr 1039 in if r \<ge> numeral l then (2 * q + 1, r - numeral l) 1040 else (2 * q, r))" 1041 1042instance 1043 by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def 1044 pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq) 1045 1046end 1047 1048declare divmod_algorithm_code [where ?'a = int, code] 1049 1050context 1051begin 1052 1053qualified definition adjust_div :: "int \<times> int \<Rightarrow> int" 1054where 1055 "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))" 1056 1057qualified lemma adjust_div_eq [simp, code]: 1058 "adjust_div (q, r) = q + of_bool (r \<noteq> 0)" 1059 by (simp add: adjust_div_def) 1060 1061qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int" 1062where 1063 [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)" 1064 1065lemma minus_numeral_div_numeral [simp]: 1066 "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)" 1067proof - 1068 have "int (fst (divmod m n)) = fst (divmod m n)" 1069 by (simp only: fst_divmod divide_int_def) auto 1070 then show ?thesis 1071 by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def) 1072qed 1073 1074lemma minus_numeral_mod_numeral [simp]: 1075 "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)" 1076proof (cases "snd (divmod m n) = (0::int)") 1077 case True 1078 then show ?thesis 1079 by (simp add: mod_eq_0_iff_dvd divides_aux_def) 1080next 1081 case False 1082 then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)" 1083 by (simp only: snd_divmod modulo_int_def) auto 1084 then show ?thesis 1085 by (simp add: divides_aux_def adjust_div_def) 1086 (simp add: divides_aux_def modulo_int_def) 1087qed 1088 1089lemma numeral_div_minus_numeral [simp]: 1090 "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)" 1091proof - 1092 have "int (fst (divmod m n)) = fst (divmod m n)" 1093 by (simp only: fst_divmod divide_int_def) auto 1094 then show ?thesis 1095 by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def) 1096qed 1097 1098lemma numeral_mod_minus_numeral [simp]: 1099 "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)" 1100proof (cases "snd (divmod m n) = (0::int)") 1101 case True 1102 then show ?thesis 1103 by (simp add: mod_eq_0_iff_dvd divides_aux_def) 1104next 1105 case False 1106 then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)" 1107 by (simp only: snd_divmod modulo_int_def) auto 1108 then show ?thesis 1109 by (simp add: divides_aux_def adjust_div_def) 1110 (simp add: divides_aux_def modulo_int_def) 1111qed 1112 1113lemma minus_one_div_numeral [simp]: 1114 "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)" 1115 using minus_numeral_div_numeral [of Num.One n] by simp 1116 1117lemma minus_one_mod_numeral [simp]: 1118 "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)" 1119 using minus_numeral_mod_numeral [of Num.One n] by simp 1120 1121lemma one_div_minus_numeral [simp]: 1122 "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)" 1123 using numeral_div_minus_numeral [of Num.One n] by simp 1124 1125lemma one_mod_minus_numeral [simp]: 1126 "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)" 1127 using numeral_mod_minus_numeral [of Num.One n] by simp 1128 1129end 1130 1131lemma div_positive_int: 1132 "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int 1133 using that div_positive [of l k] by blast 1134 1135 1136subsubsection \<open>Dedicated simproc for calculation\<close> 1137 1138text \<open> 1139 There is space for improvement here: the calculation itself 1140 could be carried out outside the logic, and a generic simproc 1141 (simplifier setup) for generic calculation would be helpful. 1142\<close> 1143 1144simproc_setup numeral_divmod 1145 ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" | 1146 "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" | 1147 "0 div - 1 :: int" | "0 mod - 1 :: int" | 1148 "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" | 1149 "0 div - numeral b :: int" | "0 mod - numeral b :: int" | 1150 "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" | 1151 "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" | 1152 "1 div - 1 :: int" | "1 mod - 1 :: int" | 1153 "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" | 1154 "1 div - numeral b :: int" |"1 mod - numeral b :: int" | 1155 "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" | 1156 "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" | 1157 "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" | 1158 "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" | 1159 "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" | 1160 "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" | 1161 "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" | 1162 "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" | 1163 "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" | 1164 "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" | 1165 "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" | 1166 "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" | 1167 "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = 1168\<open> let 1169 val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>); 1170 fun successful_rewrite ctxt ct = 1171 let 1172 val thm = Simplifier.rewrite ctxt ct 1173 in if Thm.is_reflexive thm then NONE else SOME thm end; 1174 in fn phi => 1175 let 1176 val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1 1177 one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral 1178 one_div_minus_numeral one_mod_minus_numeral 1179 numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral 1180 numeral_div_minus_numeral numeral_mod_minus_numeral 1181 div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero 1182 numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial 1183 divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One 1184 case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right 1185 minus_minus numeral_times_numeral mult_zero_right mult_1_right} 1186 @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]); 1187 fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt 1188 (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps) 1189 in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end 1190 end 1191\<close> 1192 1193 1194subsubsection \<open>Code generation\<close> 1195 1196definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" 1197 where "divmod_nat m n = (m div n, m mod n)" 1198 1199lemma fst_divmod_nat [simp]: 1200 "fst (divmod_nat m n) = m div n" 1201 by (simp add: divmod_nat_def) 1202 1203lemma snd_divmod_nat [simp]: 1204 "snd (divmod_nat m n) = m mod n" 1205 by (simp add: divmod_nat_def) 1206 1207lemma divmod_nat_if [code]: 1208 "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else 1209 let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))" 1210 by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) 1211 1212lemma [code]: 1213 "m div n = fst (divmod_nat m n)" 1214 "m mod n = snd (divmod_nat m n)" 1215 by simp_all 1216 1217lemma [code]: 1218 fixes k :: int 1219 shows 1220 "k div 0 = 0" 1221 "k mod 0 = k" 1222 "0 div k = 0" 1223 "0 mod k = 0" 1224 "k div Int.Pos Num.One = k" 1225 "k mod Int.Pos Num.One = 0" 1226 "k div Int.Neg Num.One = - k" 1227 "k mod Int.Neg Num.One = 0" 1228 "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)" 1229 "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)" 1230 "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)" 1231 "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)" 1232 "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)" 1233 "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)" 1234 "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)" 1235 "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)" 1236 by simp_all 1237 1238code_identifier 1239 code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 1240 1241 1242subsection \<open>Lemmas of doubtful value\<close> 1243 1244lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat 1245 by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>) 1246 1247lemma mod_geq: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat 1248 by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>) 1249 1250lemma mod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat 1251 using that by (auto simp add: mod_eq_0_iff_dvd) 1252 1253lemma pos_mod_conj: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int 1254 by simp 1255 1256lemma neg_mod_conj: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int 1257 by simp 1258 1259lemma zmod_eq_0_iff: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int 1260 by (auto simp add: mod_eq_0_iff_dvd) 1261 1262(* REVISIT: should this be generalized to all semiring_div types? *) 1263lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int 1264 using that by auto 1265 1266end 1267