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