src/HOL/Divides.thy
author haftmann
Mon Jun 01 18:59:22 2015 +0200 (2015-06-01)
changeset 60353 838025c6e278
parent 60352 d46de31a50c4
child 60429 d3d1e185cd63
permissions -rw-r--r--
implicit partial divison operation in integral domains
     1 (*  Title:      HOL/Divides.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 section {* The division operators div and mod *}
     7 
     8 theory Divides
     9 imports Parity
    10 begin
    11 
    12 subsection {* Syntactic division operations *}
    13 
    14 class div = dvd + divide +
    15   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    16 begin
    17 
    18 abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    19 where
    20   "op div \<equiv> divide"
    21 
    22 end
    23 
    24 subsection {* Abstract division in commutative semirings. *}
    25 
    26 class semiring_div = semidom + div +
    27   assumes mod_div_equality: "a div b * b + a mod b = a"
    28     and div_by_0 [simp]: "a div 0 = 0"
    29     and div_0 [simp]: "0 div a = 0"
    30     and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    31     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    32 begin
    33 
    34 subclass semidom_divide
    35 proof
    36   fix b a
    37   assume "b \<noteq> 0"
    38   then show "a * b div b = a"
    39     using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
    40 qed simp
    41 
    42 lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
    43   "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
    44   by (induct n) (simp_all add: no_zero_divisors)
    45 
    46 lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>
    47   "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
    48   using power_not_zero [of a n] by (auto simp add: zero_power)
    49 
    50 text {* @{const div} and @{const mod} *}
    51 
    52 lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    53   unfolding mult.commute [of b]
    54   by (rule mod_div_equality)
    55 
    56 lemma mod_div_equality': "a mod b + a div b * b = a"
    57   using mod_div_equality [of a b]
    58   by (simp only: ac_simps)
    59 
    60 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
    61   by (simp add: mod_div_equality)
    62 
    63 lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
    64   by (simp add: mod_div_equality2)
    65 
    66 lemma mod_by_0 [simp]: "a mod 0 = a"
    67   using mod_div_equality [of a zero] by simp
    68 
    69 lemma mod_0 [simp]: "0 mod a = 0"
    70   using mod_div_equality [of zero a] div_0 by simp
    71 
    72 lemma div_mult_self2 [simp]:
    73   assumes "b \<noteq> 0"
    74   shows "(a + b * c) div b = c + a div b"
    75   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
    76 
    77 lemma div_mult_self3 [simp]:
    78   assumes "b \<noteq> 0"
    79   shows "(c * b + a) div b = c + a div b"
    80   using assms by (simp add: add.commute)
    81 
    82 lemma div_mult_self4 [simp]:
    83   assumes "b \<noteq> 0"
    84   shows "(b * c + a) div b = c + a div b"
    85   using assms by (simp add: add.commute)
    86 
    87 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
    88 proof (cases "b = 0")
    89   case True then show ?thesis by simp
    90 next
    91   case False
    92   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
    93     by (simp add: mod_div_equality)
    94   also from False div_mult_self1 [of b a c] have
    95     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
    96       by (simp add: algebra_simps)
    97   finally have "a = a div b * b + (a + c * b) mod b"
    98     by (simp add: add.commute [of a] add.assoc distrib_right)
    99   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   100     by (simp add: mod_div_equality)
   101   then show ?thesis by simp
   102 qed
   103 
   104 lemma mod_mult_self2 [simp]: 
   105   "(a + b * c) mod b = a mod b"
   106   by (simp add: mult.commute [of b])
   107 
   108 lemma mod_mult_self3 [simp]:
   109   "(c * b + a) mod b = a mod b"
   110   by (simp add: add.commute)
   111 
   112 lemma mod_mult_self4 [simp]:
   113   "(b * c + a) mod b = a mod b"
   114   by (simp add: add.commute)
   115 
   116 lemma div_mult_self1_is_id:
   117   "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
   118   by (fact nonzero_mult_divide_cancel_left)
   119 
   120 lemma div_mult_self2_is_id:
   121   "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
   122   by (fact nonzero_mult_divide_cancel_right)
   123 
   124 lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
   125   using mod_mult_self2 [of 0 b a] by simp
   126 
   127 lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
   128   using mod_mult_self1 [of 0 a b] by simp
   129 
   130 lemma div_by_1 [simp]: "a div 1 = a"
   131   using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
   132 
   133 lemma mod_by_1 [simp]: "a mod 1 = 0"
   134 proof -
   135   from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
   136   then have "a + a mod 1 = a + 0" by simp
   137   then show ?thesis by (rule add_left_imp_eq)
   138 qed
   139 
   140 lemma mod_self [simp]: "a mod a = 0"
   141   using mod_mult_self2_is_0 [of 1] by simp
   142 
   143 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
   144   using div_mult_self2_is_id [of _ 1] by simp
   145 
   146 lemma div_add_self1 [simp]:
   147   assumes "b \<noteq> 0"
   148   shows "(b + a) div b = a div b + 1"
   149   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
   150 
   151 lemma div_add_self2 [simp]:
   152   assumes "b \<noteq> 0"
   153   shows "(a + b) div b = a div b + 1"
   154   using assms div_add_self1 [of b a] by (simp add: add.commute)
   155 
   156 lemma mod_add_self1 [simp]:
   157   "(b + a) mod b = a mod b"
   158   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
   159 
   160 lemma mod_add_self2 [simp]:
   161   "(a + b) mod b = a mod b"
   162   using mod_mult_self1 [of a 1 b] by simp
   163 
   164 lemma mod_div_decomp:
   165   fixes a b
   166   obtains q r where "q = a div b" and "r = a mod b"
   167     and "a = q * b + r"
   168 proof -
   169   from mod_div_equality have "a = a div b * b + a mod b" by simp
   170   moreover have "a div b = a div b" ..
   171   moreover have "a mod b = a mod b" ..
   172   note that ultimately show thesis by blast
   173 qed
   174 
   175 lemma dvd_imp_mod_0 [simp]:
   176   assumes "a dvd b"
   177   shows "b mod a = 0"
   178 proof -
   179   from assms obtain c where "b = a * c" ..
   180   then have "b mod a = a * c mod a" by simp
   181   then show "b mod a = 0" by simp
   182 qed
   183 
   184 lemma mod_eq_0_iff_dvd:
   185   "a mod b = 0 \<longleftrightarrow> b dvd a"
   186 proof
   187   assume "b dvd a"
   188   then show "a mod b = 0" by simp
   189 next
   190   assume "a mod b = 0"
   191   with mod_div_equality [of a b] have "a div b * b = a" by simp
   192   then have "a = b * (a div b)" by (simp add: ac_simps)
   193   then show "b dvd a" ..
   194 qed
   195 
   196 lemma dvd_eq_mod_eq_0 [code]:
   197   "a dvd b \<longleftrightarrow> b mod a = 0"
   198   by (simp add: mod_eq_0_iff_dvd)
   199 
   200 lemma mod_div_trivial [simp]:
   201   "a mod b div b = 0"
   202 proof (cases "b = 0")
   203   assume "b = 0"
   204   thus ?thesis by simp
   205 next
   206   assume "b \<noteq> 0"
   207   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
   208     by (rule div_mult_self1 [symmetric])
   209   also have "\<dots> = a div b"
   210     by (simp only: mod_div_equality')
   211   also have "\<dots> = a div b + 0"
   212     by simp
   213   finally show ?thesis
   214     by (rule add_left_imp_eq)
   215 qed
   216 
   217 lemma mod_mod_trivial [simp]:
   218   "a mod b mod b = a mod b"
   219 proof -
   220   have "a mod b mod b = (a mod b + a div b * b) mod b"
   221     by (simp only: mod_mult_self1)
   222   also have "\<dots> = a mod b"
   223     by (simp only: mod_div_equality')
   224   finally show ?thesis .
   225 qed
   226 
   227 lemma dvd_div_mult_self [simp]:
   228   "a dvd b \<Longrightarrow> (b div a) * a = b"
   229   using mod_div_equality [of b a, symmetric] by simp
   230 
   231 lemma dvd_mult_div_cancel [simp]:
   232   "a dvd b \<Longrightarrow> a * (b div a) = b"
   233   using dvd_div_mult_self by (simp add: ac_simps)
   234 
   235 lemma dvd_div_mult:
   236   "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
   237   by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
   238 
   239 lemma div_dvd_div [simp]:
   240   assumes "a dvd b" and "a dvd c"
   241   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
   242 using assms apply (cases "a = 0")
   243 apply auto
   244 apply (unfold dvd_def)
   245 apply auto
   246  apply(blast intro:mult.assoc[symmetric])
   247 apply(fastforce simp add: mult.assoc)
   248 done
   249 
   250 lemma dvd_mod_imp_dvd:
   251   assumes "k dvd m mod n" and "k dvd n"
   252   shows "k dvd m"
   253 proof -
   254   from assms have "k dvd (m div n) * n + m mod n"
   255     by (simp only: dvd_add dvd_mult)
   256   then show ?thesis by (simp add: mod_div_equality)
   257 qed
   258 
   259 text {* Addition respects modular equivalence. *}
   260 
   261 lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
   262 proof -
   263   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   264     by (simp only: mod_div_equality)
   265   also have "\<dots> = (a mod c + b + a div c * c) mod c"
   266     by (simp only: ac_simps)
   267   also have "\<dots> = (a mod c + b) mod c"
   268     by (rule mod_mult_self1)
   269   finally show ?thesis .
   270 qed
   271 
   272 lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
   273 proof -
   274   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
   275     by (simp only: mod_div_equality)
   276   also have "\<dots> = (a + b mod c + b div c * c) mod c"
   277     by (simp only: ac_simps)
   278   also have "\<dots> = (a + b mod c) mod c"
   279     by (rule mod_mult_self1)
   280   finally show ?thesis .
   281 qed
   282 
   283 lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
   284 by (rule trans [OF mod_add_left_eq mod_add_right_eq])
   285 
   286 lemma mod_add_cong:
   287   assumes "a mod c = a' mod c"
   288   assumes "b mod c = b' mod c"
   289   shows "(a + b) mod c = (a' + b') mod c"
   290 proof -
   291   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   292     unfolding assms ..
   293   thus ?thesis
   294     by (simp only: mod_add_eq [symmetric])
   295 qed
   296 
   297 lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
   298   \<Longrightarrow> (x + y) div z = x div z + y div z"
   299 by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
   300 
   301 text {* Multiplication respects modular equivalence. *}
   302 
   303 lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
   304 proof -
   305   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   306     by (simp only: mod_div_equality)
   307   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   308     by (simp only: algebra_simps)
   309   also have "\<dots> = (a mod c * b) mod c"
   310     by (rule mod_mult_self1)
   311   finally show ?thesis .
   312 qed
   313 
   314 lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
   315 proof -
   316   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
   317     by (simp only: mod_div_equality)
   318   also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
   319     by (simp only: algebra_simps)
   320   also have "\<dots> = (a * (b mod c)) mod c"
   321     by (rule mod_mult_self1)
   322   finally show ?thesis .
   323 qed
   324 
   325 lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
   326 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
   327 
   328 lemma mod_mult_cong:
   329   assumes "a mod c = a' mod c"
   330   assumes "b mod c = b' mod c"
   331   shows "(a * b) mod c = (a' * b') mod c"
   332 proof -
   333   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   334     unfolding assms ..
   335   thus ?thesis
   336     by (simp only: mod_mult_eq [symmetric])
   337 qed
   338 
   339 text {* Exponentiation respects modular equivalence. *}
   340 
   341 lemma power_mod: "(a mod b)^n mod b = a^n mod b"
   342 apply (induct n, simp_all)
   343 apply (rule mod_mult_right_eq [THEN trans])
   344 apply (simp (no_asm_simp))
   345 apply (rule mod_mult_eq [symmetric])
   346 done
   347 
   348 lemma mod_mod_cancel:
   349   assumes "c dvd b"
   350   shows "a mod b mod c = a mod c"
   351 proof -
   352   from `c dvd b` obtain k where "b = c * k"
   353     by (rule dvdE)
   354   have "a mod b mod c = a mod (c * k) mod c"
   355     by (simp only: `b = c * k`)
   356   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   357     by (simp only: mod_mult_self1)
   358   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   359     by (simp only: ac_simps)
   360   also have "\<dots> = a mod c"
   361     by (simp only: mod_div_equality)
   362   finally show ?thesis .
   363 qed
   364 
   365 lemma div_mult_div_if_dvd:
   366   "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
   367   apply (cases "y = 0", simp)
   368   apply (cases "z = 0", simp)
   369   apply (auto elim!: dvdE simp add: algebra_simps)
   370   apply (subst mult.assoc [symmetric])
   371   apply (simp add: no_zero_divisors)
   372   done
   373 
   374 lemma div_mult_swap:
   375   assumes "c dvd b"
   376   shows "a * (b div c) = (a * b) div c"
   377 proof -
   378   from assms have "b div c * (a div 1) = b * a div (c * 1)"
   379     by (simp only: div_mult_div_if_dvd one_dvd)
   380   then show ?thesis by (simp add: mult.commute)
   381 qed
   382    
   383 lemma div_mult_mult2 [simp]:
   384   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   385   by (drule div_mult_mult1) (simp add: mult.commute)
   386 
   387 lemma div_mult_mult1_if [simp]:
   388   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   389   by simp_all
   390 
   391 lemma mod_mult_mult1:
   392   "(c * a) mod (c * b) = c * (a mod b)"
   393 proof (cases "c = 0")
   394   case True then show ?thesis by simp
   395 next
   396   case False
   397   from mod_div_equality
   398   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   399   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   400     = c * a + c * (a mod b)" by (simp add: algebra_simps)
   401   with mod_div_equality show ?thesis by simp 
   402 qed
   403   
   404 lemma mod_mult_mult2:
   405   "(a * c) mod (b * c) = (a mod b) * c"
   406   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   407 
   408 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   409   by (fact mod_mult_mult2 [symmetric])
   410 
   411 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   412   by (fact mod_mult_mult1 [symmetric])
   413 
   414 lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
   415   assumes "c \<noteq> 0"
   416   shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
   417 proof -
   418   have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
   419     using assms by (simp add: mod_mult_mult1)
   420   then show ?thesis by (simp add: mod_eq_0_iff_dvd)
   421 qed
   422 
   423 lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
   424   assumes "c \<noteq> 0"
   425   shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
   426   using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
   427 
   428 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   429   unfolding dvd_def by (auto simp add: mod_mult_mult1)
   430 
   431 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
   432 by (blast intro: dvd_mod_imp_dvd dvd_mod)
   433 
   434 lemma div_power:
   435   "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
   436 apply (induct n)
   437  apply simp
   438 apply(simp add: div_mult_div_if_dvd dvd_power_same)
   439 done
   440 
   441 lemma dvd_div_eq_mult:
   442   assumes "a \<noteq> 0" and "a dvd b"  
   443   shows "b div a = c \<longleftrightarrow> b = c * a"
   444 proof
   445   assume "b = c * a"
   446   then show "b div a = c" by (simp add: assms)
   447 next
   448   assume "b div a = c"
   449   then have "b div a * a = c * a" by simp
   450   moreover from `a dvd b` have "b div a * a = b" by simp
   451   ultimately show "b = c * a" by simp
   452 qed
   453    
   454 lemma dvd_div_div_eq_mult:
   455   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   456   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
   457   using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
   458 
   459 end
   460 
   461 class ring_div = comm_ring_1 + semiring_div
   462 begin
   463 
   464 subclass idom_divide ..
   465 
   466 text {* Negation respects modular equivalence. *}
   467 
   468 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
   469 proof -
   470   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   471     by (simp only: mod_div_equality)
   472   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   473     by (simp add: ac_simps)
   474   also have "\<dots> = (- (a mod b)) mod b"
   475     by (rule mod_mult_self1)
   476   finally show ?thesis .
   477 qed
   478 
   479 lemma mod_minus_cong:
   480   assumes "a mod b = a' mod b"
   481   shows "(- a) mod b = (- a') mod b"
   482 proof -
   483   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   484     unfolding assms ..
   485   thus ?thesis
   486     by (simp only: mod_minus_eq [symmetric])
   487 qed
   488 
   489 text {* Subtraction respects modular equivalence. *}
   490 
   491 lemma mod_diff_left_eq:
   492   "(a - b) mod c = (a mod c - b) mod c"
   493   using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
   494 
   495 lemma mod_diff_right_eq:
   496   "(a - b) mod c = (a - b mod c) mod c"
   497   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   498 
   499 lemma mod_diff_eq:
   500   "(a - b) mod c = (a mod c - b mod c) mod c"
   501   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   502 
   503 lemma mod_diff_cong:
   504   assumes "a mod c = a' mod c"
   505   assumes "b mod c = b' mod c"
   506   shows "(a - b) mod c = (a' - b') mod c"
   507   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
   508 
   509 lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
   510 apply (case_tac "y = 0") apply simp
   511 apply (auto simp add: dvd_def)
   512 apply (subgoal_tac "-(y * k) = y * - k")
   513  apply (simp only:)
   514  apply (erule div_mult_self1_is_id)
   515 apply simp
   516 done
   517 
   518 lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
   519 apply (case_tac "y = 0") apply simp
   520 apply (auto simp add: dvd_def)
   521 apply (subgoal_tac "y * k = -y * -k")
   522  apply (erule ssubst, rule div_mult_self1_is_id)
   523  apply simp
   524 apply simp
   525 done
   526 
   527 lemma div_diff[simp]:
   528   "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"
   529 using div_add[where y = "- z" for z]
   530 by (simp add: dvd_neg_div)
   531 
   532 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   533   using div_mult_mult1 [of "- 1" a b]
   534   unfolding neg_equal_0_iff_equal by simp
   535 
   536 lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
   537   using mod_mult_mult1 [of "- 1" a b] by simp
   538 
   539 lemma div_minus_right: "a div (-b) = (-a) div b"
   540   using div_minus_minus [of "-a" b] by simp
   541 
   542 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
   543   using mod_minus_minus [of "-a" b] by simp
   544 
   545 lemma div_minus1_right [simp]: "a div (-1) = -a"
   546   using div_minus_right [of a 1] by simp
   547 
   548 lemma mod_minus1_right [simp]: "a mod (-1) = 0"
   549   using mod_minus_right [of a 1] by simp
   550 
   551 lemma minus_mod_self2 [simp]: 
   552   "(a - b) mod b = a mod b"
   553   by (simp add: mod_diff_right_eq)
   554 
   555 lemma minus_mod_self1 [simp]: 
   556   "(b - a) mod b = - a mod b"
   557   using mod_add_self2 [of "- a" b] by simp
   558 
   559 end
   560 
   561 
   562 subsubsection {* Parity and division *}
   563 
   564 class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
   565   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   566   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   567   assumes zero_not_eq_two: "0 \<noteq> 2"
   568 begin
   569 
   570 lemma parity_cases [case_names even odd]:
   571   assumes "a mod 2 = 0 \<Longrightarrow> P"
   572   assumes "a mod 2 = 1 \<Longrightarrow> P"
   573   shows P
   574   using assms parity by blast
   575 
   576 lemma one_div_two_eq_zero [simp]:
   577   "1 div 2 = 0"
   578 proof (cases "2 = 0")
   579   case True then show ?thesis by simp
   580 next
   581   case False
   582   from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
   583   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
   584   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
   585   then have "1 div 2 = 0 \<or> 2 = 0" by simp
   586   with False show ?thesis by auto
   587 qed
   588 
   589 lemma not_mod_2_eq_0_eq_1 [simp]:
   590   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   591   by (cases a rule: parity_cases) simp_all
   592 
   593 lemma not_mod_2_eq_1_eq_0 [simp]:
   594   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   595   by (cases a rule: parity_cases) simp_all
   596 
   597 subclass semiring_parity
   598 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   599   show "1 mod 2 = 1"
   600     by (fact one_mod_two_eq_one)
   601 next
   602   fix a b
   603   assume "a mod 2 = 1"
   604   moreover assume "b mod 2 = 1"
   605   ultimately show "(a + b) mod 2 = 0"
   606     using mod_add_eq [of a b 2] by simp
   607 next
   608   fix a b
   609   assume "(a * b) mod 2 = 0"
   610   then have "(a mod 2) * (b mod 2) = 0"
   611     by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
   612   then show "a mod 2 = 0 \<or> b mod 2 = 0"
   613     by (rule divisors_zero)
   614 next
   615   fix a
   616   assume "a mod 2 = 1"
   617   then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
   618   then show "\<exists>b. a = b + 1" ..
   619 qed
   620 
   621 lemma even_iff_mod_2_eq_zero:
   622   "even a \<longleftrightarrow> a mod 2 = 0"
   623   by (fact dvd_eq_mod_eq_0)
   624 
   625 lemma even_succ_div_two [simp]:
   626   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   627   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
   628 
   629 lemma odd_succ_div_two [simp]:
   630   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
   631   by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
   632 
   633 lemma even_two_times_div_two:
   634   "even a \<Longrightarrow> 2 * (a div 2) = a"
   635   by (fact dvd_mult_div_cancel)
   636 
   637 lemma odd_two_times_div_two_succ [simp]:
   638   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   639   using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
   640 
   641 end
   642 
   643 
   644 subsection {* Generic numeral division with a pragmatic type class *}
   645 
   646 text {*
   647   The following type class contains everything necessary to formulate
   648   a division algorithm in ring structures with numerals, restricted
   649   to its positive segments.  This is its primary motiviation, and it
   650   could surely be formulated using a more fine-grained, more algebraic
   651   and less technical class hierarchy.
   652 *}
   653 
   654 class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
   655   assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
   656   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
   657     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
   658     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
   659     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
   660     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
   661     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
   662     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   663     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
   664   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
   665 begin
   666 
   667 lemma mult_div_cancel:
   668   "b * (a div b) = a - a mod b"
   669 proof -
   670   have "b * (a div b) + a mod b = a"
   671     using mod_div_equality [of a b] by (simp add: ac_simps)
   672   then have "b * (a div b) + a mod b - a mod b = a - a mod b"
   673     by simp
   674   then show ?thesis
   675     by simp
   676 qed
   677 
   678 subclass semiring_div_parity
   679 proof
   680   fix a
   681   show "a mod 2 = 0 \<or> a mod 2 = 1"
   682   proof (rule ccontr)
   683     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
   684     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
   685     have "0 < 2" by simp
   686     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
   687     with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
   688     with discrete have "1 \<le> a mod 2" by simp
   689     with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
   690     with discrete have "2 \<le> a mod 2" by simp
   691     with `a mod 2 < 2` show False by simp
   692   qed
   693 next
   694   show "1 mod 2 = 1"
   695     by (rule mod_less) simp_all
   696 next
   697   show "0 \<noteq> 2"
   698     by simp
   699 qed
   700 
   701 lemma divmod_digit_1:
   702   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   703   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
   704     and "a mod (2 * b) - b = a mod b" (is "?Q")
   705 proof -
   706   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
   707     by (auto intro: trans)
   708   with `0 < b` have "0 < a div b" by (auto intro: div_positive)
   709   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
   710   with `0 < b` have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
   711   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   712   have mod_w: "a mod (2 * b) = a mod b + b * w"
   713     by (simp add: w_def mod_mult2_eq ac_simps)
   714   from assms w_exhaust have "w = 1"
   715     by (auto simp add: mod_w) (insert mod_less, auto)
   716   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
   717   have "2 * (a div (2 * b)) = a div b - w"
   718     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
   719   with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   720   then show ?P and ?Q
   721     by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
   722 qed
   723 
   724 lemma divmod_digit_0:
   725   assumes "0 < b" and "a mod (2 * b) < b"
   726   shows "2 * (a div (2 * b)) = a div b" (is "?P")
   727     and "a mod (2 * b) = a mod b" (is "?Q")
   728 proof -
   729   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   730   have mod_w: "a mod (2 * b) = a mod b + b * w"
   731     by (simp add: w_def mod_mult2_eq ac_simps)
   732   moreover have "b \<le> a mod b + b"
   733   proof -
   734     from `0 < b` pos_mod_sign have "0 \<le> a mod b" by blast
   735     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
   736     then show ?thesis by simp
   737   qed
   738   moreover note assms w_exhaust
   739   ultimately have "w = 0" by auto
   740   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   741   have "2 * (a div (2 * b)) = a div b - w"
   742     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
   743   with `w = 0` have div: "2 * (a div (2 * b)) = a div b" by simp
   744   then show ?P and ?Q
   745     by (simp_all add: div mod)
   746 qed
   747 
   748 definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
   749 where
   750   "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
   751 
   752 lemma fst_divmod [simp]:
   753   "fst (divmod m n) = numeral m div numeral n"
   754   by (simp add: divmod_def)
   755 
   756 lemma snd_divmod [simp]:
   757   "snd (divmod m n) = numeral m mod numeral n"
   758   by (simp add: divmod_def)
   759 
   760 definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   761 where
   762   "divmod_step l qr = (let (q, r) = qr
   763     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   764     else (2 * q, r))"
   765 
   766 text {*
   767   This is a formulation of one step (referring to one digit position)
   768   in school-method division: compare the dividend at the current
   769   digit position with the remainder from previous division steps
   770   and evaluate accordingly.
   771 *}
   772 
   773 lemma divmod_step_eq [code]:
   774   "divmod_step l (q, r) = (if numeral l \<le> r
   775     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   776   by (simp add: divmod_step_def)
   777 
   778 lemma divmod_step_simps [simp]:
   779   "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
   780   "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
   781   by (auto simp add: divmod_step_eq not_le)
   782 
   783 text {*
   784   This is a formulation of school-method division.
   785   If the divisor is smaller than the dividend, terminate.
   786   If not, shift the dividend to the right until termination
   787   occurs and then reiterate single division steps in the
   788   opposite direction.
   789 *}
   790 
   791 lemma divmod_divmod_step [code]:
   792   "divmod m n = (if m < n then (0, numeral m)
   793     else divmod_step n (divmod m (Num.Bit0 n)))"
   794 proof (cases "m < n")
   795   case True then have "numeral m < numeral n" by simp
   796   then show ?thesis
   797     by (simp add: prod_eq_iff div_less mod_less)
   798 next
   799   case False
   800   have "divmod m n =
   801     divmod_step n (numeral m div (2 * numeral n),
   802       numeral m mod (2 * numeral n))"
   803   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   804     case True
   805     with divmod_step_simps
   806       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   807         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   808         by blast
   809     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   810       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   811       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   812       by simp_all
   813     ultimately show ?thesis by (simp only: divmod_def)
   814   next
   815     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   816       by (simp add: not_le)
   817     with divmod_step_simps
   818       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   819         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   820         by blast
   821     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   822       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   823       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   824       by (simp_all only: zero_less_numeral)
   825     ultimately show ?thesis by (simp only: divmod_def)
   826   qed
   827   then have "divmod m n =
   828     divmod_step n (numeral m div numeral (Num.Bit0 n),
   829       numeral m mod numeral (Num.Bit0 n))"
   830     by (simp only: numeral.simps distrib mult_1) 
   831   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   832     by (simp add: divmod_def)
   833   with False show ?thesis by simp
   834 qed
   835 
   836 lemma divmod_eq [simp]:
   837   "m < n \<Longrightarrow> divmod m n = (0, numeral m)"
   838   "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   839   by (auto simp add: divmod_divmod_step [of m n])
   840 
   841 lemma divmod_cancel [simp, code]:
   842   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   843   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
   844 proof -
   845   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
   846     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
   847     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   848   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   849   then show ?P and ?Q
   850     by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   851       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
   852 qed
   853 
   854 text {* Special case: divisibility *}
   855 
   856 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   857 where
   858   "divides_aux qr \<longleftrightarrow> snd qr = 0"
   859 
   860 lemma divides_aux_eq [simp]:
   861   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   862   by (simp add: divides_aux_def)
   863 
   864 lemma dvd_numeral_simp [simp]:
   865   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   866   by (simp add: divmod_def mod_eq_0_iff_dvd)
   867 
   868 end
   869 
   870 hide_fact (open) le_add_diff_inverse2
   871   -- {* restore simple accesses for more general variants of theorems *}
   872 
   873   
   874 subsection {* Division on @{typ nat} *}
   875 
   876 text {*
   877   We define @{const div} and @{const mod} on @{typ nat} by means
   878   of a characteristic relation with two input arguments
   879   @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
   880   @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
   881 *}
   882 
   883 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
   884   "divmod_nat_rel m n qr \<longleftrightarrow>
   885     m = fst qr * n + snd qr \<and>
   886       (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
   887 
   888 text {* @{const divmod_nat_rel} is total: *}
   889 
   890 lemma divmod_nat_rel_ex:
   891   obtains q r where "divmod_nat_rel m n (q, r)"
   892 proof (cases "n = 0")
   893   case True  with that show thesis
   894     by (auto simp add: divmod_nat_rel_def)
   895 next
   896   case False
   897   have "\<exists>q r. m = q * n + r \<and> r < n"
   898   proof (induct m)
   899     case 0 with `n \<noteq> 0`
   900     have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp
   901     then show ?case by blast
   902   next
   903     case (Suc m) then obtain q' r'
   904       where m: "m = q' * n + r'" and n: "r' < n" by auto
   905     then show ?case proof (cases "Suc r' < n")
   906       case True
   907       from m n have "Suc m = q' * n + Suc r'" by simp
   908       with True show ?thesis by blast
   909     next
   910       case False then have "n \<le> Suc r'" by auto
   911       moreover from n have "Suc r' \<le> n" by auto
   912       ultimately have "n = Suc r'" by auto
   913       with m have "Suc m = Suc q' * n + 0" by simp
   914       with `n \<noteq> 0` show ?thesis by blast
   915     qed
   916   qed
   917   with that show thesis
   918     using `n \<noteq> 0` by (auto simp add: divmod_nat_rel_def)
   919 qed
   920 
   921 text {* @{const divmod_nat_rel} is injective: *}
   922 
   923 lemma divmod_nat_rel_unique:
   924   assumes "divmod_nat_rel m n qr"
   925     and "divmod_nat_rel m n qr'"
   926   shows "qr = qr'"
   927 proof (cases "n = 0")
   928   case True with assms show ?thesis
   929     by (cases qr, cases qr')
   930       (simp add: divmod_nat_rel_def)
   931 next
   932   case False
   933   have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
   934   apply (rule leI)
   935   apply (subst less_iff_Suc_add)
   936   apply (auto simp add: add_mult_distrib)
   937   done
   938   from `n \<noteq> 0` assms have *: "fst qr = fst qr'"
   939     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
   940   with assms have "snd qr = snd qr'"
   941     by (simp add: divmod_nat_rel_def)
   942   with * show ?thesis by (cases qr, cases qr') simp
   943 qed
   944 
   945 text {*
   946   We instantiate divisibility on the natural numbers by
   947   means of @{const divmod_nat_rel}:
   948 *}
   949 
   950 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   951   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
   952 
   953 lemma divmod_nat_rel_divmod_nat:
   954   "divmod_nat_rel m n (divmod_nat m n)"
   955 proof -
   956   from divmod_nat_rel_ex
   957     obtain qr where rel: "divmod_nat_rel m n qr" .
   958   then show ?thesis
   959   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   960 qed
   961 
   962 lemma divmod_nat_unique:
   963   assumes "divmod_nat_rel m n qr" 
   964   shows "divmod_nat m n = qr"
   965   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   966 
   967 instantiation nat :: "Divides.div"
   968 begin
   969 
   970 definition divide_nat where
   971   div_nat_def: "divide m n = fst (divmod_nat m n)"
   972 
   973 definition mod_nat where
   974   "m mod n = snd (divmod_nat m n)"
   975   
   976 instance ..
   977 
   978 end
   979 
   980 instantiation nat :: semiring_div
   981 begin
   982 
   983 lemma fst_divmod_nat [simp]:
   984   "fst (divmod_nat m n) = m div n"
   985   by (simp add: div_nat_def)
   986 
   987 lemma snd_divmod_nat [simp]:
   988   "snd (divmod_nat m n) = m mod n"
   989   by (simp add: mod_nat_def)
   990 
   991 lemma divmod_nat_div_mod:
   992   "divmod_nat m n = (m div n, m mod n)"
   993   by (simp add: prod_eq_iff)
   994 
   995 lemma div_nat_unique:
   996   assumes "divmod_nat_rel m n (q, r)" 
   997   shows "m div n = q"
   998   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   999 
  1000 lemma mod_nat_unique:
  1001   assumes "divmod_nat_rel m n (q, r)" 
  1002   shows "m mod n = r"
  1003   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
  1004 
  1005 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
  1006   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
  1007 
  1008 lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
  1009   by (simp add: divmod_nat_unique divmod_nat_rel_def)
  1010 
  1011 lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
  1012   by (simp add: divmod_nat_unique divmod_nat_rel_def)
  1013 
  1014 lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
  1015   by (simp add: divmod_nat_unique divmod_nat_rel_def)
  1016 
  1017 lemma divmod_nat_step:
  1018   assumes "0 < n" and "n \<le> m"
  1019   shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
  1020 proof (rule divmod_nat_unique)
  1021   have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
  1022     by (rule divmod_nat_rel)
  1023   thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
  1024     unfolding divmod_nat_rel_def using assms by auto
  1025 qed
  1026 
  1027 text {* The ''recursion'' equations for @{const div} and @{const mod} *}
  1028 
  1029 lemma div_less [simp]:
  1030   fixes m n :: nat
  1031   assumes "m < n"
  1032   shows "m div n = 0"
  1033   using assms divmod_nat_base by (simp add: prod_eq_iff)
  1034 
  1035 lemma le_div_geq:
  1036   fixes m n :: nat
  1037   assumes "0 < n" and "n \<le> m"
  1038   shows "m div n = Suc ((m - n) div n)"
  1039   using assms divmod_nat_step by (simp add: prod_eq_iff)
  1040 
  1041 lemma mod_less [simp]:
  1042   fixes m n :: nat
  1043   assumes "m < n"
  1044   shows "m mod n = m"
  1045   using assms divmod_nat_base by (simp add: prod_eq_iff)
  1046 
  1047 lemma le_mod_geq:
  1048   fixes m n :: nat
  1049   assumes "n \<le> m"
  1050   shows "m mod n = (m - n) mod n"
  1051   using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
  1052 
  1053 instance proof
  1054   fix m n :: nat
  1055   show "m div n * n + m mod n = m"
  1056     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
  1057 next
  1058   fix m n q :: nat
  1059   assume "n \<noteq> 0"
  1060   then show "(q + m * n) div n = m + q div n"
  1061     by (induct m) (simp_all add: le_div_geq)
  1062 next
  1063   fix m n q :: nat
  1064   assume "m \<noteq> 0"
  1065   hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
  1066     unfolding divmod_nat_rel_def
  1067     by (auto split: split_if_asm, simp_all add: algebra_simps)
  1068   moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
  1069   ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
  1070   thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
  1071 next
  1072   fix n :: nat show "n div 0 = 0"
  1073     by (simp add: div_nat_def divmod_nat_zero)
  1074 next
  1075   fix n :: nat show "0 div n = 0"
  1076     by (simp add: div_nat_def divmod_nat_zero_left)
  1077 qed
  1078 
  1079 end
  1080 
  1081 lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
  1082   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
  1083   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
  1084 
  1085 text {* Simproc for cancelling @{const div} and @{const mod} *}
  1086 
  1087 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
  1088 
  1089 ML {*
  1090 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
  1091 (
  1092   val div_name = @{const_name divide};
  1093   val mod_name = @{const_name mod};
  1094   val mk_binop = HOLogic.mk_binop;
  1095   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
  1096   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
  1097   fun mk_sum [] = HOLogic.zero
  1098     | mk_sum [t] = t
  1099     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
  1100   fun dest_sum tm =
  1101     if HOLogic.is_zero tm then []
  1102     else
  1103       (case try HOLogic.dest_Suc tm of
  1104         SOME t => HOLogic.Suc_zero :: dest_sum t
  1105       | NONE =>
  1106           (case try dest_plus tm of
  1107             SOME (t, u) => dest_sum t @ dest_sum u
  1108           | NONE => [tm]));
  1109 
  1110   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
  1111 
  1112   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
  1113     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
  1114 )
  1115 *}
  1116 
  1117 simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
  1118 
  1119 
  1120 subsubsection {* Quotient *}
  1121 
  1122 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
  1123 by (simp add: le_div_geq linorder_not_less)
  1124 
  1125 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
  1126 by (simp add: div_geq)
  1127 
  1128 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
  1129 by simp
  1130 
  1131 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
  1132 by simp
  1133 
  1134 lemma div_positive:
  1135   fixes m n :: nat
  1136   assumes "n > 0"
  1137   assumes "m \<ge> n"
  1138   shows "m div n > 0"
  1139 proof -
  1140   from `m \<ge> n` obtain q where "m = n + q"
  1141     by (auto simp add: le_iff_add)
  1142   with `n > 0` show ?thesis by simp
  1143 qed
  1144 
  1145 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
  1146   by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
  1147 
  1148 subsubsection {* Remainder *}
  1149 
  1150 lemma mod_less_divisor [simp]:
  1151   fixes m n :: nat
  1152   assumes "n > 0"
  1153   shows "m mod n < (n::nat)"
  1154   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
  1155 
  1156 lemma mod_Suc_le_divisor [simp]:
  1157   "m mod Suc n \<le> n"
  1158   using mod_less_divisor [of "Suc n" m] by arith
  1159 
  1160 lemma mod_less_eq_dividend [simp]:
  1161   fixes m n :: nat
  1162   shows "m mod n \<le> m"
  1163 proof (rule add_leD2)
  1164   from mod_div_equality have "m div n * n + m mod n = m" .
  1165   then show "m div n * n + m mod n \<le> m" by auto
  1166 qed
  1167 
  1168 lemma mod_geq: "\<not> m < (n\<Colon>nat) \<Longrightarrow> m mod n = (m - n) mod n"
  1169 by (simp add: le_mod_geq linorder_not_less)
  1170 
  1171 lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
  1172 by (simp add: le_mod_geq)
  1173 
  1174 lemma mod_1 [simp]: "m mod Suc 0 = 0"
  1175 by (induct m) (simp_all add: mod_geq)
  1176 
  1177 (* a simple rearrangement of mod_div_equality: *)
  1178 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
  1179   using mod_div_equality2 [of n m] by arith
  1180 
  1181 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
  1182   apply (drule mod_less_divisor [where m = m])
  1183   apply simp
  1184   done
  1185 
  1186 subsubsection {* Quotient and Remainder *}
  1187 
  1188 lemma divmod_nat_rel_mult1_eq:
  1189   "divmod_nat_rel b c (q, r)
  1190    \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
  1191 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1192 
  1193 lemma div_mult1_eq:
  1194   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
  1195 by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
  1196 
  1197 lemma divmod_nat_rel_add1_eq:
  1198   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
  1199    \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
  1200 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1201 
  1202 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  1203 lemma div_add1_eq:
  1204   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
  1205 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
  1206 
  1207 lemma divmod_nat_rel_mult2_eq:
  1208   assumes "divmod_nat_rel a b (q, r)"
  1209   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
  1210 proof -
  1211   { assume "r < b" and "0 < c" 
  1212     then have "b * (q mod c) + r < b * c"
  1213       apply (cut_tac m = q and n = c in mod_less_divisor)
  1214       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
  1215       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
  1216       apply (simp add: add_mult_distrib2)
  1217       done
  1218     then have "r + b * (q mod c) < b * c"
  1219       by (simp add: ac_simps)
  1220   } with assms show ?thesis
  1221     by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
  1222 qed
  1223     
  1224 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
  1225 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
  1226 
  1227 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
  1228 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
  1229 
  1230 instance nat :: semiring_numeral_div
  1231   by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
  1232 
  1233 
  1234 subsubsection {* Further Facts about Quotient and Remainder *}
  1235 
  1236 lemma div_1 [simp]:
  1237   "m div Suc 0 = m"
  1238   using div_by_1 [of m] by simp
  1239 
  1240 (* Monotonicity of div in first argument *)
  1241 lemma div_le_mono [rule_format (no_asm)]:
  1242     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
  1243 apply (case_tac "k=0", simp)
  1244 apply (induct "n" rule: nat_less_induct, clarify)
  1245 apply (case_tac "n<k")
  1246 (* 1  case n<k *)
  1247 apply simp
  1248 (* 2  case n >= k *)
  1249 apply (case_tac "m<k")
  1250 (* 2.1  case m<k *)
  1251 apply simp
  1252 (* 2.2  case m>=k *)
  1253 apply (simp add: div_geq diff_le_mono)
  1254 done
  1255 
  1256 (* Antimonotonicity of div in second argument *)
  1257 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
  1258 apply (subgoal_tac "0<n")
  1259  prefer 2 apply simp
  1260 apply (induct_tac k rule: nat_less_induct)
  1261 apply (rename_tac "k")
  1262 apply (case_tac "k<n", simp)
  1263 apply (subgoal_tac "~ (k<m) ")
  1264  prefer 2 apply simp
  1265 apply (simp add: div_geq)
  1266 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
  1267  prefer 2
  1268  apply (blast intro: div_le_mono diff_le_mono2)
  1269 apply (rule le_trans, simp)
  1270 apply (simp)
  1271 done
  1272 
  1273 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
  1274 apply (case_tac "n=0", simp)
  1275 apply (subgoal_tac "m div n \<le> m div 1", simp)
  1276 apply (rule div_le_mono2)
  1277 apply (simp_all (no_asm_simp))
  1278 done
  1279 
  1280 (* Similar for "less than" *)
  1281 lemma div_less_dividend [simp]:
  1282   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
  1283 apply (induct m rule: nat_less_induct)
  1284 apply (rename_tac "m")
  1285 apply (case_tac "m<n", simp)
  1286 apply (subgoal_tac "0<n")
  1287  prefer 2 apply simp
  1288 apply (simp add: div_geq)
  1289 apply (case_tac "n<m")
  1290  apply (subgoal_tac "(m-n) div n < (m-n) ")
  1291   apply (rule impI less_trans_Suc)+
  1292 apply assumption
  1293   apply (simp_all)
  1294 done
  1295 
  1296 text{*A fact for the mutilated chess board*}
  1297 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
  1298 apply (case_tac "n=0", simp)
  1299 apply (induct "m" rule: nat_less_induct)
  1300 apply (case_tac "Suc (na) <n")
  1301 (* case Suc(na) < n *)
  1302 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
  1303 (* case n \<le> Suc(na) *)
  1304 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
  1305 apply (auto simp add: Suc_diff_le le_mod_geq)
  1306 done
  1307 
  1308 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1309 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1310 
  1311 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1312 
  1313 (*Loses information, namely we also have r<d provided d is nonzero*)
  1314 lemma mod_eqD:
  1315   fixes m d r q :: nat
  1316   assumes "m mod d = r"
  1317   shows "\<exists>q. m = r + q * d"
  1318 proof -
  1319   from mod_div_equality obtain q where "q * d + m mod d = m" by blast
  1320   with assms have "m = r + q * d" by simp
  1321   then show ?thesis ..
  1322 qed
  1323 
  1324 lemma split_div:
  1325  "P(n div k :: nat) =
  1326  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
  1327  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1328 proof
  1329   assume P: ?P
  1330   show ?Q
  1331   proof (cases)
  1332     assume "k = 0"
  1333     with P show ?Q by simp
  1334   next
  1335     assume not0: "k \<noteq> 0"
  1336     thus ?Q
  1337     proof (simp, intro allI impI)
  1338       fix i j
  1339       assume n: "n = k*i + j" and j: "j < k"
  1340       show "P i"
  1341       proof (cases)
  1342         assume "i = 0"
  1343         with n j P show "P i" by simp
  1344       next
  1345         assume "i \<noteq> 0"
  1346         with not0 n j P show "P i" by(simp add:ac_simps)
  1347       qed
  1348     qed
  1349   qed
  1350 next
  1351   assume Q: ?Q
  1352   show ?P
  1353   proof (cases)
  1354     assume "k = 0"
  1355     with Q show ?P by simp
  1356   next
  1357     assume not0: "k \<noteq> 0"
  1358     with Q have R: ?R by simp
  1359     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1360     show ?P by simp
  1361   qed
  1362 qed
  1363 
  1364 lemma split_div_lemma:
  1365   assumes "0 < n"
  1366   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
  1367 proof
  1368   assume ?rhs
  1369   with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
  1370   then have A: "n * q \<le> m" by simp
  1371   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
  1372   then have "m < m + (n - (m mod n))" by simp
  1373   then have "m < n + (m - (m mod n))" by simp
  1374   with nq have "m < n + n * q" by simp
  1375   then have B: "m < n * Suc q" by simp
  1376   from A B show ?lhs ..
  1377 next
  1378   assume P: ?lhs
  1379   then have "divmod_nat_rel m n (q, m - n * q)"
  1380     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
  1381   with divmod_nat_rel_unique divmod_nat_rel [of m n]
  1382   have "(q, m - n * q) = (m div n, m mod n)" by auto
  1383   then show ?rhs by simp
  1384 qed
  1385 
  1386 theorem split_div':
  1387   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
  1388    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
  1389   apply (case_tac "0 < n")
  1390   apply (simp only: add: split_div_lemma)
  1391   apply simp_all
  1392   done
  1393 
  1394 lemma split_mod:
  1395  "P(n mod k :: nat) =
  1396  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
  1397  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1398 proof
  1399   assume P: ?P
  1400   show ?Q
  1401   proof (cases)
  1402     assume "k = 0"
  1403     with P show ?Q by simp
  1404   next
  1405     assume not0: "k \<noteq> 0"
  1406     thus ?Q
  1407     proof (simp, intro allI impI)
  1408       fix i j
  1409       assume "n = k*i + j" "j < k"
  1410       thus "P j" using not0 P by (simp add: ac_simps)
  1411     qed
  1412   qed
  1413 next
  1414   assume Q: ?Q
  1415   show ?P
  1416   proof (cases)
  1417     assume "k = 0"
  1418     with Q show ?P by simp
  1419   next
  1420     assume not0: "k \<noteq> 0"
  1421     with Q have R: ?R by simp
  1422     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1423     show ?P by simp
  1424   qed
  1425 qed
  1426 
  1427 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
  1428   using mod_div_equality [of m n] by arith
  1429 
  1430 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
  1431   using mod_div_equality [of m n] by arith
  1432 (* FIXME: very similar to mult_div_cancel *)
  1433 
  1434 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  1435   apply rule
  1436   apply (cases "b = 0")
  1437   apply simp_all
  1438   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
  1439   done
  1440 
  1441 
  1442 subsubsection {* An ``induction'' law for modulus arithmetic. *}
  1443 
  1444 lemma mod_induct_0:
  1445   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1446   and base: "P i" and i: "i<p"
  1447   shows "P 0"
  1448 proof (rule ccontr)
  1449   assume contra: "\<not>(P 0)"
  1450   from i have p: "0<p" by simp
  1451   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
  1452   proof
  1453     fix k
  1454     show "?A k"
  1455     proof (induct k)
  1456       show "?A 0" by simp  -- "by contradiction"
  1457     next
  1458       fix n
  1459       assume ih: "?A n"
  1460       show "?A (Suc n)"
  1461       proof (clarsimp)
  1462         assume y: "P (p - Suc n)"
  1463         have n: "Suc n < p"
  1464         proof (rule ccontr)
  1465           assume "\<not>(Suc n < p)"
  1466           hence "p - Suc n = 0"
  1467             by simp
  1468           with y contra show "False"
  1469             by simp
  1470         qed
  1471         hence n2: "Suc (p - Suc n) = p-n" by arith
  1472         from p have "p - Suc n < p" by arith
  1473         with y step have z: "P ((Suc (p - Suc n)) mod p)"
  1474           by blast
  1475         show "False"
  1476         proof (cases "n=0")
  1477           case True
  1478           with z n2 contra show ?thesis by simp
  1479         next
  1480           case False
  1481           with p have "p-n < p" by arith
  1482           with z n2 False ih show ?thesis by simp
  1483         qed
  1484       qed
  1485     qed
  1486   qed
  1487   moreover
  1488   from i obtain k where "0<k \<and> i+k=p"
  1489     by (blast dest: less_imp_add_positive)
  1490   hence "0<k \<and> i=p-k" by auto
  1491   moreover
  1492   note base
  1493   ultimately
  1494   show "False" by blast
  1495 qed
  1496 
  1497 lemma mod_induct:
  1498   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1499   and base: "P i" and i: "i<p" and j: "j<p"
  1500   shows "P j"
  1501 proof -
  1502   have "\<forall>j<p. P j"
  1503   proof
  1504     fix j
  1505     show "j<p \<longrightarrow> P j" (is "?A j")
  1506     proof (induct j)
  1507       from step base i show "?A 0"
  1508         by (auto elim: mod_induct_0)
  1509     next
  1510       fix k
  1511       assume ih: "?A k"
  1512       show "?A (Suc k)"
  1513       proof
  1514         assume suc: "Suc k < p"
  1515         hence k: "k<p" by simp
  1516         with ih have "P k" ..
  1517         with step k have "P (Suc k mod p)"
  1518           by blast
  1519         moreover
  1520         from suc have "Suc k mod p = Suc k"
  1521           by simp
  1522         ultimately
  1523         show "P (Suc k)" by simp
  1524       qed
  1525     qed
  1526   qed
  1527   with j show ?thesis by blast
  1528 qed
  1529 
  1530 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
  1531   by (simp add: numeral_2_eq_2 le_div_geq)
  1532 
  1533 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
  1534   by (simp add: numeral_2_eq_2 le_mod_geq)
  1535 
  1536 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
  1537 by (simp add: mult_2 [symmetric])
  1538 
  1539 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
  1540 proof -
  1541   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
  1542   moreover have "m mod 2 < 2" by simp
  1543   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
  1544   then show ?thesis by auto
  1545 qed
  1546 
  1547 text{*These lemmas collapse some needless occurrences of Suc:
  1548     at least three Sucs, since two and fewer are rewritten back to Suc again!
  1549     We already have some rules to simplify operands smaller than 3.*}
  1550 
  1551 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
  1552 by (simp add: Suc3_eq_add_3)
  1553 
  1554 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
  1555 by (simp add: Suc3_eq_add_3)
  1556 
  1557 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
  1558 by (simp add: Suc3_eq_add_3)
  1559 
  1560 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
  1561 by (simp add: Suc3_eq_add_3)
  1562 
  1563 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
  1564 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1565 
  1566 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
  1567 apply (induct "m")
  1568 apply (simp_all add: mod_Suc)
  1569 done
  1570 
  1571 declare Suc_times_mod_eq [of "numeral w", simp] for w
  1572 
  1573 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
  1574 by (simp add: div_le_mono)
  1575 
  1576 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
  1577 by (cases n) simp_all
  1578 
  1579 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
  1580 proof -
  1581   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
  1582   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
  1583 qed
  1584 
  1585 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
  1586 proof -
  1587   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
  1588   also have "... = Suc m mod n" by (rule mod_mult_self3) 
  1589   finally show ?thesis .
  1590 qed
  1591 
  1592 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
  1593 apply (subst mod_Suc [of m]) 
  1594 apply (subst mod_Suc [of "m mod n"], simp) 
  1595 done
  1596 
  1597 lemma mod_2_not_eq_zero_eq_one_nat:
  1598   fixes n :: nat
  1599   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1600   by (fact not_mod_2_eq_0_eq_1)
  1601   
  1602 lemma even_Suc_div_two [simp]:
  1603   "even n \<Longrightarrow> Suc n div 2 = n div 2"
  1604   using even_succ_div_two [of n] by simp
  1605   
  1606 lemma odd_Suc_div_two [simp]:
  1607   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
  1608   using odd_succ_div_two [of n] by simp
  1609 
  1610 lemma odd_two_times_div_two_nat [simp]:
  1611   assumes "odd n"
  1612   shows "2 * (n div 2) = n - (1 :: nat)"
  1613 proof -
  1614   from assms have "2 * (n div 2) + 1 = n"
  1615     by (rule odd_two_times_div_two_succ)
  1616   then have "Suc (2 * (n div 2)) - 1 = n - 1"
  1617     by simp
  1618   then show ?thesis
  1619     by simp
  1620 qed
  1621 
  1622 lemma odd_Suc_minus_one [simp]:
  1623   "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
  1624   by (auto elim: oddE)
  1625 
  1626 lemma parity_induct [case_names zero even odd]:
  1627   assumes zero: "P 0"
  1628   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
  1629   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
  1630   shows "P n"
  1631 proof (induct n rule: less_induct)
  1632   case (less n)
  1633   show "P n"
  1634   proof (cases "n = 0")
  1635     case True with zero show ?thesis by simp
  1636   next
  1637     case False
  1638     with less have hyp: "P (n div 2)" by simp
  1639     show ?thesis
  1640     proof (cases "even n")
  1641       case True
  1642       with hyp even [of "n div 2"] show ?thesis
  1643         by simp
  1644     next
  1645       case False
  1646       with hyp odd [of "n div 2"] show ?thesis 
  1647         by simp
  1648     qed
  1649   qed
  1650 qed
  1651 
  1652 
  1653 subsection {* Division on @{typ int} *}
  1654 
  1655 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
  1656     --{*definition of quotient and remainder*}
  1657   "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
  1658     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
  1659 
  1660 text {*
  1661   The following algorithmic devlopment actually echos what has already
  1662   been developed in class @{class semiring_numeral_div}.  In the long
  1663   run it seems better to derive division on @{typ int} just from
  1664   division on @{typ nat} and instantiate @{class semiring_numeral_div}
  1665   accordingly.
  1666 *}
  1667 
  1668 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
  1669     --{*for the division algorithm*}
  1670     "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
  1671                          else (2 * q, r))"
  1672 
  1673 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
  1674 function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1675   "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
  1676      else adjust b (posDivAlg a (2 * b)))"
  1677 by auto
  1678 termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")
  1679   (auto simp add: mult_2)
  1680 
  1681 text{*algorithm for the case @{text "a<0, b>0"}*}
  1682 function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1683   "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
  1684      else adjust b (negDivAlg a (2 * b)))"
  1685 by auto
  1686 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")
  1687   (auto simp add: mult_2)
  1688 
  1689 text{*algorithm for the general case @{term "b\<noteq>0"}*}
  1690 
  1691 definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1692     --{*The full division algorithm considers all possible signs for a, b
  1693        including the special case @{text "a=0, b<0"} because 
  1694        @{term negDivAlg} requires @{term "a<0"}.*}
  1695   "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
  1696                   else if a = 0 then (0, 0)
  1697                        else apsnd uminus (negDivAlg (-a) (-b))
  1698                else 
  1699                   if 0 < b then negDivAlg a b
  1700                   else apsnd uminus (posDivAlg (-a) (-b)))"
  1701 
  1702 instantiation int :: Divides.div
  1703 begin
  1704 
  1705 definition divide_int where
  1706   div_int_def: "divide a b = fst (divmod_int a b)"
  1707 
  1708 definition mod_int where
  1709   "a mod b = snd (divmod_int a b)"
  1710 
  1711 instance ..
  1712 
  1713 end
  1714 
  1715 lemma fst_divmod_int [simp]:
  1716   "fst (divmod_int a b) = a div b"
  1717   by (simp add: div_int_def)
  1718 
  1719 lemma snd_divmod_int [simp]:
  1720   "snd (divmod_int a b) = a mod b"
  1721   by (simp add: mod_int_def)
  1722 
  1723 lemma divmod_int_mod_div:
  1724   "divmod_int p q = (p div q, p mod q)"
  1725   by (simp add: prod_eq_iff)
  1726 
  1727 text{*
  1728 Here is the division algorithm in ML:
  1729 
  1730 \begin{verbatim}
  1731     fun posDivAlg (a,b) =
  1732       if a<b then (0,a)
  1733       else let val (q,r) = posDivAlg(a, 2*b)
  1734                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
  1735            end
  1736 
  1737     fun negDivAlg (a,b) =
  1738       if 0\<le>a+b then (~1,a+b)
  1739       else let val (q,r) = negDivAlg(a, 2*b)
  1740                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
  1741            end;
  1742 
  1743     fun negateSnd (q,r:int) = (q,~r);
  1744 
  1745     fun divmod (a,b) = if 0\<le>a then 
  1746                           if b>0 then posDivAlg (a,b) 
  1747                            else if a=0 then (0,0)
  1748                                 else negateSnd (negDivAlg (~a,~b))
  1749                        else 
  1750                           if 0<b then negDivAlg (a,b)
  1751                           else        negateSnd (posDivAlg (~a,~b));
  1752 \end{verbatim}
  1753 *}
  1754 
  1755 
  1756 subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
  1757 
  1758 lemma unique_quotient_lemma:
  1759      "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
  1760       ==> q' \<le> (q::int)"
  1761 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  1762  prefer 2 apply (simp add: right_diff_distrib)
  1763 apply (subgoal_tac "0 < b * (1 + q - q') ")
  1764 apply (erule_tac [2] order_le_less_trans)
  1765  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1766 apply (subgoal_tac "b * q' < b * (1 + q) ")
  1767  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1768 apply (simp add: mult_less_cancel_left)
  1769 done
  1770 
  1771 lemma unique_quotient_lemma_neg:
  1772      "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]  
  1773       ==> q \<le> (q'::int)"
  1774 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
  1775     auto)
  1776 
  1777 lemma unique_quotient:
  1778      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
  1779       ==> q = q'"
  1780 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
  1781 apply (blast intro: order_antisym
  1782              dest: order_eq_refl [THEN unique_quotient_lemma] 
  1783              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
  1784 done
  1785 
  1786 
  1787 lemma unique_remainder:
  1788      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
  1789       ==> r = r'"
  1790 apply (subgoal_tac "q = q'")
  1791  apply (simp add: divmod_int_rel_def)
  1792 apply (blast intro: unique_quotient)
  1793 done
  1794 
  1795 
  1796 subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
  1797 
  1798 text{*And positive divisors*}
  1799 
  1800 lemma adjust_eq [simp]:
  1801      "adjust b (q, r) = 
  1802       (let diff = r - b in  
  1803         if 0 \<le> diff then (2 * q + 1, diff)   
  1804                      else (2*q, r))"
  1805   by (simp add: Let_def adjust_def)
  1806 
  1807 declare posDivAlg.simps [simp del]
  1808 
  1809 text{*use with a simproc to avoid repeatedly proving the premise*}
  1810 lemma posDivAlg_eqn:
  1811      "0 < b ==>  
  1812       posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
  1813 by (rule posDivAlg.simps [THEN trans], simp)
  1814 
  1815 text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
  1816 theorem posDivAlg_correct:
  1817   assumes "0 \<le> a" and "0 < b"
  1818   shows "divmod_int_rel a b (posDivAlg a b)"
  1819   using assms
  1820   apply (induct a b rule: posDivAlg.induct)
  1821   apply auto
  1822   apply (simp add: divmod_int_rel_def)
  1823   apply (subst posDivAlg_eqn, simp add: distrib_left)
  1824   apply (case_tac "a < b")
  1825   apply simp_all
  1826   apply (erule splitE)
  1827   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  1828   done
  1829 
  1830 
  1831 subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
  1832 
  1833 text{*And positive divisors*}
  1834 
  1835 declare negDivAlg.simps [simp del]
  1836 
  1837 text{*use with a simproc to avoid repeatedly proving the premise*}
  1838 lemma negDivAlg_eqn:
  1839      "0 < b ==>  
  1840       negDivAlg a b =       
  1841        (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
  1842 by (rule negDivAlg.simps [THEN trans], simp)
  1843 
  1844 (*Correctness of negDivAlg: it computes quotients correctly
  1845   It doesn't work if a=0 because the 0/b equals 0, not -1*)
  1846 lemma negDivAlg_correct:
  1847   assumes "a < 0" and "b > 0"
  1848   shows "divmod_int_rel a b (negDivAlg a b)"
  1849   using assms
  1850   apply (induct a b rule: negDivAlg.induct)
  1851   apply (auto simp add: linorder_not_le)
  1852   apply (simp add: divmod_int_rel_def)
  1853   apply (subst negDivAlg_eqn, assumption)
  1854   apply (case_tac "a + b < (0\<Colon>int)")
  1855   apply simp_all
  1856   apply (erule splitE)
  1857   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  1858   done
  1859 
  1860 
  1861 subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
  1862 
  1863 (*the case a=0*)
  1864 lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
  1865 by (auto simp add: divmod_int_rel_def linorder_neq_iff)
  1866 
  1867 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
  1868 by (subst posDivAlg.simps, auto)
  1869 
  1870 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
  1871 by (subst posDivAlg.simps, auto)
  1872 
  1873 lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
  1874 by (subst negDivAlg.simps, auto)
  1875 
  1876 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
  1877 by (auto simp add: divmod_int_rel_def)
  1878 
  1879 lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
  1880 apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
  1881 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
  1882                     posDivAlg_correct negDivAlg_correct)
  1883 
  1884 lemma divmod_int_unique:
  1885   assumes "divmod_int_rel a b qr" 
  1886   shows "divmod_int a b = qr"
  1887   using assms divmod_int_correct [of a b]
  1888   using unique_quotient [of a b] unique_remainder [of a b]
  1889   by (metis pair_collapse)
  1890 
  1891 lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
  1892   using divmod_int_correct by (simp add: divmod_int_mod_div)
  1893 
  1894 lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
  1895   by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
  1896 
  1897 lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
  1898   by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
  1899 
  1900 instance int :: ring_div
  1901 proof
  1902   fix a b :: int
  1903   show "a div b * b + a mod b = a"
  1904     using divmod_int_rel_div_mod [of a b]
  1905     unfolding divmod_int_rel_def by (simp add: mult.commute)
  1906 next
  1907   fix a b c :: int
  1908   assume "b \<noteq> 0"
  1909   hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
  1910     using divmod_int_rel_div_mod [of a b]
  1911     unfolding divmod_int_rel_def by (auto simp: algebra_simps)
  1912   thus "(a + c * b) div b = c + a div b"
  1913     by (rule div_int_unique)
  1914 next
  1915   fix a b c :: int
  1916   assume "c \<noteq> 0"
  1917   hence "\<And>q r. divmod_int_rel a b (q, r)
  1918     \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
  1919     unfolding divmod_int_rel_def
  1920     by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
  1921       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
  1922       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
  1923   hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
  1924     using divmod_int_rel_div_mod [of a b] .
  1925   thus "(c * a) div (c * b) = a div b"
  1926     by (rule div_int_unique)
  1927 next
  1928   fix a :: int show "a div 0 = 0"
  1929     by (rule div_int_unique, simp add: divmod_int_rel_def)
  1930 next
  1931   fix a :: int show "0 div a = 0"
  1932     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
  1933 qed
  1934 
  1935 text{*Basic laws about division and remainder*}
  1936 
  1937 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
  1938   by (fact mod_div_equality2 [symmetric])
  1939 
  1940 text {* Tool setup *}
  1941 
  1942 ML {*
  1943 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
  1944 (
  1945   val div_name = @{const_name Rings.divide};
  1946   val mod_name = @{const_name mod};
  1947   val mk_binop = HOLogic.mk_binop;
  1948   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
  1949   val dest_sum = Arith_Data.dest_sum;
  1950 
  1951   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
  1952 
  1953   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
  1954     (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
  1955 )
  1956 *}
  1957 
  1958 simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
  1959 
  1960 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
  1961   using divmod_int_correct [of a b]
  1962   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1963 
  1964 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
  1965    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
  1966 
  1967 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
  1968   using divmod_int_correct [of a b]
  1969   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1970 
  1971 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
  1972    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
  1973 
  1974 
  1975 subsubsection {* General Properties of div and mod *}
  1976 
  1977 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
  1978 apply (rule div_int_unique)
  1979 apply (auto simp add: divmod_int_rel_def)
  1980 done
  1981 
  1982 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
  1983 apply (rule div_int_unique)
  1984 apply (auto simp add: divmod_int_rel_def)
  1985 done
  1986 
  1987 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
  1988 apply (rule div_int_unique)
  1989 apply (auto simp add: divmod_int_rel_def)
  1990 done
  1991 
  1992 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
  1993 
  1994 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
  1995 apply (rule_tac q = 0 in mod_int_unique)
  1996 apply (auto simp add: divmod_int_rel_def)
  1997 done
  1998 
  1999 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
  2000 apply (rule_tac q = 0 in mod_int_unique)
  2001 apply (auto simp add: divmod_int_rel_def)
  2002 done
  2003 
  2004 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
  2005 apply (rule_tac q = "-1" in mod_int_unique)
  2006 apply (auto simp add: divmod_int_rel_def)
  2007 done
  2008 
  2009 text{*There is no @{text mod_neg_pos_trivial}.*}
  2010 
  2011 
  2012 subsubsection {* Laws for div and mod with Unary Minus *}
  2013 
  2014 lemma zminus1_lemma:
  2015      "divmod_int_rel a b (q, r) ==> b \<noteq> 0
  2016       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
  2017                           if r=0 then 0 else b-r)"
  2018 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
  2019 
  2020 
  2021 lemma zdiv_zminus1_eq_if:
  2022      "b \<noteq> (0::int)  
  2023       ==> (-a) div b =  
  2024           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  2025 by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
  2026 
  2027 lemma zmod_zminus1_eq_if:
  2028      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
  2029 apply (case_tac "b = 0", simp)
  2030 apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
  2031 done
  2032 
  2033 lemma zmod_zminus1_not_zero:
  2034   fixes k l :: int
  2035   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  2036   unfolding zmod_zminus1_eq_if by auto
  2037 
  2038 lemma zdiv_zminus2_eq_if:
  2039      "b \<noteq> (0::int)  
  2040       ==> a div (-b) =  
  2041           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  2042 by (simp add: zdiv_zminus1_eq_if div_minus_right)
  2043 
  2044 lemma zmod_zminus2_eq_if:
  2045      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
  2046 by (simp add: zmod_zminus1_eq_if mod_minus_right)
  2047 
  2048 lemma zmod_zminus2_not_zero:
  2049   fixes k l :: int
  2050   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  2051   unfolding zmod_zminus2_eq_if by auto 
  2052 
  2053 
  2054 subsubsection {* Computation of Division and Remainder *}
  2055 
  2056 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  2057 by (simp add: div_int_def divmod_int_def)
  2058 
  2059 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  2060 by (simp add: mod_int_def divmod_int_def)
  2061 
  2062 text{*a positive, b positive *}
  2063 
  2064 lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
  2065 by (simp add: div_int_def divmod_int_def)
  2066 
  2067 lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
  2068 by (simp add: mod_int_def divmod_int_def)
  2069 
  2070 text{*a negative, b positive *}
  2071 
  2072 lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
  2073 by (simp add: div_int_def divmod_int_def)
  2074 
  2075 lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
  2076 by (simp add: mod_int_def divmod_int_def)
  2077 
  2078 text{*a positive, b negative *}
  2079 
  2080 lemma div_pos_neg:
  2081      "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"
  2082 by (simp add: div_int_def divmod_int_def)
  2083 
  2084 lemma mod_pos_neg:
  2085      "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"
  2086 by (simp add: mod_int_def divmod_int_def)
  2087 
  2088 text{*a negative, b negative *}
  2089 
  2090 lemma div_neg_neg:
  2091      "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"
  2092 by (simp add: div_int_def divmod_int_def)
  2093 
  2094 lemma mod_neg_neg:
  2095      "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"
  2096 by (simp add: mod_int_def divmod_int_def)
  2097 
  2098 text {*Simplify expresions in which div and mod combine numerical constants*}
  2099 
  2100 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  2101   by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
  2102 
  2103 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  2104   by (rule div_int_unique [of a b q r],
  2105     simp add: divmod_int_rel_def)
  2106 
  2107 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  2108   by (rule mod_int_unique [of a b q r],
  2109     simp add: divmod_int_rel_def)
  2110 
  2111 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  2112   by (rule mod_int_unique [of a b q r],
  2113     simp add: divmod_int_rel_def)
  2114 
  2115 text {*
  2116   numeral simprocs -- high chance that these can be replaced
  2117   by divmod algorithm from @{class semiring_numeral_div}
  2118 *}
  2119 
  2120 ML {*
  2121 local
  2122   val mk_number = HOLogic.mk_number HOLogic.intT
  2123   val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
  2124   val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
  2125   val zero = @{term "0 :: int"}
  2126   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
  2127   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
  2128   val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
  2129   fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
  2130     (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
  2131   fun binary_proc proc ctxt ct =
  2132     (case Thm.term_of ct of
  2133       _ $ t $ u =>
  2134       (case try (apply2 (`(snd o HOLogic.dest_number))) (t, u) of
  2135         SOME args => proc ctxt args
  2136       | NONE => NONE)
  2137     | _ => NONE);
  2138 in
  2139   fun divmod_proc posrule negrule =
  2140     binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
  2141       if b = 0 then NONE
  2142       else
  2143         let
  2144           val (q, r) = apply2 mk_number (Integer.div_mod a b)
  2145           val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
  2146           val (goal2, goal3, rule) =
  2147             if b > 0
  2148             then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
  2149             else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
  2150         in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
  2151 end
  2152 *}
  2153 
  2154 simproc_setup binary_int_div
  2155   ("numeral m div numeral n :: int" |
  2156    "numeral m div - numeral n :: int" |
  2157    "- numeral m div numeral n :: int" |
  2158    "- numeral m div - numeral n :: int") =
  2159   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
  2160 
  2161 simproc_setup binary_int_mod
  2162   ("numeral m mod numeral n :: int" |
  2163    "numeral m mod - numeral n :: int" |
  2164    "- numeral m mod numeral n :: int" |
  2165    "- numeral m mod - numeral n :: int") =
  2166   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
  2167 
  2168 lemmas posDivAlg_eqn_numeral [simp] =
  2169     posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
  2170 
  2171 lemmas negDivAlg_eqn_numeral [simp] =
  2172     negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
  2173 
  2174 
  2175 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}
  2176 
  2177 lemma [simp]:
  2178   shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
  2179     and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
  2180     and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
  2181     and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
  2182     and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
  2183     and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
  2184   by (simp_all del: arith_special
  2185     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
  2186 
  2187 lemma [simp]:
  2188   shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
  2189     and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"
  2190     and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"
  2191     and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"
  2192     and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"
  2193     and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"
  2194   by (simp_all add: div_eq_minus1 zmod_minus1)
  2195 
  2196 
  2197 subsubsection {* Monotonicity in the First Argument (Dividend) *}
  2198 
  2199 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
  2200 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2201 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
  2202 apply (rule unique_quotient_lemma)
  2203 apply (erule subst)
  2204 apply (erule subst, simp_all)
  2205 done
  2206 
  2207 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
  2208 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2209 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
  2210 apply (rule unique_quotient_lemma_neg)
  2211 apply (erule subst)
  2212 apply (erule subst, simp_all)
  2213 done
  2214 
  2215 
  2216 subsubsection {* Monotonicity in the Second Argument (Divisor) *}
  2217 
  2218 lemma q_pos_lemma:
  2219      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
  2220 apply (subgoal_tac "0 < b'* (q' + 1) ")
  2221  apply (simp add: zero_less_mult_iff)
  2222 apply (simp add: distrib_left)
  2223 done
  2224 
  2225 lemma zdiv_mono2_lemma:
  2226      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';   
  2227          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]   
  2228       ==> q \<le> (q'::int)"
  2229 apply (frule q_pos_lemma, assumption+) 
  2230 apply (subgoal_tac "b*q < b* (q' + 1) ")
  2231  apply (simp add: mult_less_cancel_left)
  2232 apply (subgoal_tac "b*q = r' - r + b'*q'")
  2233  prefer 2 apply simp
  2234 apply (simp (no_asm_simp) add: distrib_left)
  2235 apply (subst add.commute, rule add_less_le_mono, arith)
  2236 apply (rule mult_right_mono, auto)
  2237 done
  2238 
  2239 lemma zdiv_mono2:
  2240      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
  2241 apply (subgoal_tac "b \<noteq> 0")
  2242  prefer 2 apply arith
  2243 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2244 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
  2245 apply (rule zdiv_mono2_lemma)
  2246 apply (erule subst)
  2247 apply (erule subst, simp_all)
  2248 done
  2249 
  2250 lemma q_neg_lemma:
  2251      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
  2252 apply (subgoal_tac "b'*q' < 0")
  2253  apply (simp add: mult_less_0_iff, arith)
  2254 done
  2255 
  2256 lemma zdiv_mono2_neg_lemma:
  2257      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
  2258          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
  2259       ==> q' \<le> (q::int)"
  2260 apply (frule q_neg_lemma, assumption+) 
  2261 apply (subgoal_tac "b*q' < b* (q + 1) ")
  2262  apply (simp add: mult_less_cancel_left)
  2263 apply (simp add: distrib_left)
  2264 apply (subgoal_tac "b*q' \<le> b'*q'")
  2265  prefer 2 apply (simp add: mult_right_mono_neg, arith)
  2266 done
  2267 
  2268 lemma zdiv_mono2_neg:
  2269      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
  2270 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2271 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
  2272 apply (rule zdiv_mono2_neg_lemma)
  2273 apply (erule subst)
  2274 apply (erule subst, simp_all)
  2275 done
  2276 
  2277 
  2278 subsubsection {* More Algebraic Laws for div and mod *}
  2279 
  2280 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
  2281 
  2282 lemma zmult1_lemma:
  2283      "[| divmod_int_rel b c (q, r) |]  
  2284       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
  2285 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
  2286 
  2287 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
  2288 apply (case_tac "c = 0", simp)
  2289 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
  2290 done
  2291 
  2292 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
  2293 
  2294 lemma zadd1_lemma:
  2295      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
  2296       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
  2297 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
  2298 
  2299 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  2300 lemma zdiv_zadd1_eq:
  2301      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
  2302 apply (case_tac "c = 0", simp)
  2303 apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
  2304 done
  2305 
  2306 lemma posDivAlg_div_mod:
  2307   assumes "k \<ge> 0"
  2308   and "l \<ge> 0"
  2309   shows "posDivAlg k l = (k div l, k mod l)"
  2310 proof (cases "l = 0")
  2311   case True then show ?thesis by (simp add: posDivAlg.simps)
  2312 next
  2313   case False with assms posDivAlg_correct
  2314     have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
  2315     by simp
  2316   from div_int_unique [OF this] mod_int_unique [OF this]
  2317   show ?thesis by simp
  2318 qed
  2319 
  2320 lemma negDivAlg_div_mod:
  2321   assumes "k < 0"
  2322   and "l > 0"
  2323   shows "negDivAlg k l = (k div l, k mod l)"
  2324 proof -
  2325   from assms have "l \<noteq> 0" by simp
  2326   from assms negDivAlg_correct
  2327     have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
  2328     by simp
  2329   from div_int_unique [OF this] mod_int_unique [OF this]
  2330   show ?thesis by simp
  2331 qed
  2332 
  2333 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
  2334 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  2335 
  2336 (* REVISIT: should this be generalized to all semiring_div types? *)
  2337 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
  2338 
  2339 lemma zmod_zdiv_equality':
  2340   "(m\<Colon>int) mod n = m - (m div n) * n"
  2341   using mod_div_equality [of m n] by arith
  2342 
  2343 
  2344 subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}
  2345 
  2346 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
  2347   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
  2348   to cause particular problems.*)
  2349 
  2350 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}
  2351 
  2352 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
  2353 apply (subgoal_tac "b * (c - q mod c) < r * 1")
  2354  apply (simp add: algebra_simps)
  2355 apply (rule order_le_less_trans)
  2356  apply (erule_tac [2] mult_strict_right_mono)
  2357  apply (rule mult_left_mono_neg)
  2358   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
  2359  apply (simp)
  2360 apply (simp)
  2361 done
  2362 
  2363 lemma zmult2_lemma_aux2:
  2364      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
  2365 apply (subgoal_tac "b * (q mod c) \<le> 0")
  2366  apply arith
  2367 apply (simp add: mult_le_0_iff)
  2368 done
  2369 
  2370 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
  2371 apply (subgoal_tac "0 \<le> b * (q mod c) ")
  2372 apply arith
  2373 apply (simp add: zero_le_mult_iff)
  2374 done
  2375 
  2376 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
  2377 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
  2378  apply (simp add: right_diff_distrib)
  2379 apply (rule order_less_le_trans)
  2380  apply (erule mult_strict_right_mono)
  2381  apply (rule_tac [2] mult_left_mono)
  2382   apply simp
  2383  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
  2384 apply simp
  2385 done
  2386 
  2387 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
  2388       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
  2389 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
  2390                    zero_less_mult_iff distrib_left [symmetric] 
  2391                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
  2392 
  2393 lemma zdiv_zmult2_eq:
  2394   fixes a b c :: int
  2395   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
  2396 apply (case_tac "b = 0", simp)
  2397 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
  2398 done
  2399 
  2400 lemma zmod_zmult2_eq:
  2401   fixes a b c :: int
  2402   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
  2403 apply (case_tac "b = 0", simp)
  2404 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
  2405 done
  2406 
  2407 lemma div_pos_geq:
  2408   fixes k l :: int
  2409   assumes "0 < l" and "l \<le> k"
  2410   shows "k div l = (k - l) div l + 1"
  2411 proof -
  2412   have "k = (k - l) + l" by simp
  2413   then obtain j where k: "k = j + l" ..
  2414   with assms show ?thesis by simp
  2415 qed
  2416 
  2417 lemma mod_pos_geq:
  2418   fixes k l :: int
  2419   assumes "0 < l" and "l \<le> k"
  2420   shows "k mod l = (k - l) mod l"
  2421 proof -
  2422   have "k = (k - l) + l" by simp
  2423   then obtain j where k: "k = j + l" ..
  2424   with assms show ?thesis by simp
  2425 qed
  2426 
  2427 
  2428 subsubsection {* Splitting Rules for div and mod *}
  2429 
  2430 text{*The proofs of the two lemmas below are essentially identical*}
  2431 
  2432 lemma split_pos_lemma:
  2433  "0<k ==> 
  2434     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
  2435 apply (rule iffI, clarify)
  2436  apply (erule_tac P="P x y" for x y in rev_mp)  
  2437  apply (subst mod_add_eq) 
  2438  apply (subst zdiv_zadd1_eq) 
  2439  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
  2440 txt{*converse direction*}
  2441 apply (drule_tac x = "n div k" in spec) 
  2442 apply (drule_tac x = "n mod k" in spec, simp)
  2443 done
  2444 
  2445 lemma split_neg_lemma:
  2446  "k<0 ==>
  2447     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
  2448 apply (rule iffI, clarify)
  2449  apply (erule_tac P="P x y" for x y in rev_mp)  
  2450  apply (subst mod_add_eq) 
  2451  apply (subst zdiv_zadd1_eq) 
  2452  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
  2453 txt{*converse direction*}
  2454 apply (drule_tac x = "n div k" in spec) 
  2455 apply (drule_tac x = "n mod k" in spec, simp)
  2456 done
  2457 
  2458 lemma split_zdiv:
  2459  "P(n div k :: int) =
  2460   ((k = 0 --> P 0) & 
  2461    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
  2462    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
  2463 apply (case_tac "k=0", simp)
  2464 apply (simp only: linorder_neq_iff)
  2465 apply (erule disjE) 
  2466  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
  2467                       split_neg_lemma [of concl: "%x y. P x"])
  2468 done
  2469 
  2470 lemma split_zmod:
  2471  "P(n mod k :: int) =
  2472   ((k = 0 --> P n) & 
  2473    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
  2474    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  2475 apply (case_tac "k=0", simp)
  2476 apply (simp only: linorder_neq_iff)
  2477 apply (erule disjE) 
  2478  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
  2479                       split_neg_lemma [of concl: "%x y. P y"])
  2480 done
  2481 
  2482 text {* Enable (lin)arith to deal with @{const div} and @{const mod}
  2483   when these are applied to some constant that is of the form
  2484   @{term "numeral k"}: *}
  2485 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  2486 declare split_zmod [of _ _ "numeral k", arith_split] for k
  2487 
  2488 
  2489 subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}
  2490 
  2491 lemma pos_divmod_int_rel_mult_2:
  2492   assumes "0 \<le> b"
  2493   assumes "divmod_int_rel a b (q, r)"
  2494   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
  2495   using assms unfolding divmod_int_rel_def by auto
  2496 
  2497 declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
  2498 
  2499 lemma neg_divmod_int_rel_mult_2:
  2500   assumes "b \<le> 0"
  2501   assumes "divmod_int_rel (a + 1) b (q, r)"
  2502   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
  2503   using assms unfolding divmod_int_rel_def by auto
  2504 
  2505 text{*computing div by shifting *}
  2506 
  2507 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  2508   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
  2509   by (rule div_int_unique)
  2510 
  2511 lemma neg_zdiv_mult_2: 
  2512   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  2513   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
  2514   by (rule div_int_unique)
  2515 
  2516 (* FIXME: add rules for negative numerals *)
  2517 lemma zdiv_numeral_Bit0 [simp]:
  2518   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  2519     numeral v div (numeral w :: int)"
  2520   unfolding numeral.simps unfolding mult_2 [symmetric]
  2521   by (rule div_mult_mult1, simp)
  2522 
  2523 lemma zdiv_numeral_Bit1 [simp]:
  2524   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
  2525     (numeral v div (numeral w :: int))"
  2526   unfolding numeral.simps
  2527   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2528   by (rule pos_zdiv_mult_2, simp)
  2529 
  2530 lemma pos_zmod_mult_2:
  2531   fixes a b :: int
  2532   assumes "0 \<le> a"
  2533   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  2534   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
  2535   by (rule mod_int_unique)
  2536 
  2537 lemma neg_zmod_mult_2:
  2538   fixes a b :: int
  2539   assumes "a \<le> 0"
  2540   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  2541   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
  2542   by (rule mod_int_unique)
  2543 
  2544 (* FIXME: add rules for negative numerals *)
  2545 lemma zmod_numeral_Bit0 [simp]:
  2546   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
  2547     (2::int) * (numeral v mod numeral w)"
  2548   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  2549   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  2550 
  2551 lemma zmod_numeral_Bit1 [simp]:
  2552   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  2553     2 * (numeral v mod numeral w) + (1::int)"
  2554   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  2555   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2556   by (rule pos_zmod_mult_2, simp)
  2557 
  2558 lemma zdiv_eq_0_iff:
  2559  "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
  2560 proof
  2561   assume ?L
  2562   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  2563   with `?L` show ?R by blast
  2564 next
  2565   assume ?R thus ?L
  2566     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  2567 qed
  2568 
  2569 
  2570 subsubsection {* Quotients of Signs *}
  2571 
  2572 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  2573 apply (subgoal_tac "a div b \<le> -1", force)
  2574 apply (rule order_trans)
  2575 apply (rule_tac a' = "-1" in zdiv_mono1)
  2576 apply (auto simp add: div_eq_minus1)
  2577 done
  2578 
  2579 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  2580 by (drule zdiv_mono1_neg, auto)
  2581 
  2582 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  2583 by (drule zdiv_mono1, auto)
  2584 
  2585 text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
  2586 conditional upon the sign of @{text a} or @{text b}. There are many more.
  2587 They should all be simp rules unless that causes too much search. *}
  2588 
  2589 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  2590 apply auto
  2591 apply (drule_tac [2] zdiv_mono1)
  2592 apply (auto simp add: linorder_neq_iff)
  2593 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  2594 apply (blast intro: div_neg_pos_less0)
  2595 done
  2596 
  2597 lemma neg_imp_zdiv_nonneg_iff:
  2598   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  2599 apply (subst div_minus_minus [symmetric])
  2600 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  2601 done
  2602 
  2603 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  2604 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  2605 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  2606 
  2607 lemma pos_imp_zdiv_pos_iff:
  2608   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  2609 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  2610 by arith
  2611 
  2612 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  2613 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  2614 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  2615 
  2616 lemma nonneg1_imp_zdiv_pos_iff:
  2617   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  2618 apply rule
  2619  apply rule
  2620   using div_pos_pos_trivial[of a b]apply arith
  2621  apply(cases "b=0")apply simp
  2622  using div_nonneg_neg_le0[of a b]apply arith
  2623 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  2624 done
  2625 
  2626 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  2627 apply (rule split_zmod[THEN iffD2])
  2628 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  2629 done
  2630 
  2631 
  2632 subsubsection {* The Divides Relation *}
  2633 
  2634 lemma dvd_eq_mod_eq_0_numeral:
  2635   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
  2636   by (fact dvd_eq_mod_eq_0)
  2637 
  2638 
  2639 subsubsection {* Further properties *}
  2640 
  2641 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
  2642   using zmod_zdiv_equality[where a="m" and b="n"]
  2643   by (simp add: algebra_simps) (* FIXME: generalize *)
  2644 
  2645 instance int :: semiring_numeral_div
  2646   by intro_classes (auto intro: zmod_le_nonneg_dividend
  2647     simp add: zmult_div_cancel
  2648     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
  2649     zmod_zmult2_eq zdiv_zmult2_eq)
  2650   
  2651 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
  2652 apply (subst split_div, auto)
  2653 apply (subst split_zdiv, auto)
  2654 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)
  2655 apply (auto simp add: divmod_int_rel_def of_nat_mult)
  2656 done
  2657 
  2658 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
  2659 apply (subst split_mod, auto)
  2660 apply (subst split_zmod, auto)
  2661 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
  2662        in unique_remainder)
  2663 apply (auto simp add: divmod_int_rel_def of_nat_mult)
  2664 done
  2665 
  2666 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
  2667 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  2668 
  2669 text{*Suggested by Matthias Daum*}
  2670 lemma int_power_div_base:
  2671      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  2672 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  2673  apply (erule ssubst)
  2674  apply (simp only: power_add)
  2675  apply simp_all
  2676 done
  2677 
  2678 text {* by Brian Huffman *}
  2679 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
  2680 by (rule mod_minus_eq [symmetric])
  2681 
  2682 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
  2683 by (rule mod_diff_left_eq [symmetric])
  2684 
  2685 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
  2686 by (rule mod_diff_right_eq [symmetric])
  2687 
  2688 lemmas zmod_simps =
  2689   mod_add_left_eq  [symmetric]
  2690   mod_add_right_eq [symmetric]
  2691   mod_mult_right_eq[symmetric]
  2692   mod_mult_left_eq [symmetric]
  2693   power_mod
  2694   zminus_zmod zdiff_zmod_left zdiff_zmod_right
  2695 
  2696 text {* Distributive laws for function @{text nat}. *}
  2697 
  2698 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  2699 apply (rule linorder_cases [of y 0])
  2700 apply (simp add: div_nonneg_neg_le0)
  2701 apply simp
  2702 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  2703 done
  2704 
  2705 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  2706 lemma nat_mod_distrib:
  2707   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  2708 apply (case_tac "y = 0", simp)
  2709 apply (simp add: nat_eq_iff zmod_int)
  2710 done
  2711 
  2712 text  {* transfer setup *}
  2713 
  2714 lemma transfer_nat_int_functions:
  2715     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  2716     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  2717   by (auto simp add: nat_div_distrib nat_mod_distrib)
  2718 
  2719 lemma transfer_nat_int_function_closures:
  2720     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  2721     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  2722   apply (cases "y = 0")
  2723   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  2724   apply (cases "y = 0")
  2725   apply auto
  2726 done
  2727 
  2728 declare transfer_morphism_nat_int [transfer add return:
  2729   transfer_nat_int_functions
  2730   transfer_nat_int_function_closures
  2731 ]
  2732 
  2733 lemma transfer_int_nat_functions:
  2734     "(int x) div (int y) = int (x div y)"
  2735     "(int x) mod (int y) = int (x mod y)"
  2736   by (auto simp add: zdiv_int zmod_int)
  2737 
  2738 lemma transfer_int_nat_function_closures:
  2739     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  2740     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  2741   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  2742 
  2743 declare transfer_morphism_int_nat [transfer add return:
  2744   transfer_int_nat_functions
  2745   transfer_int_nat_function_closures
  2746 ]
  2747 
  2748 text{*Suggested by Matthias Daum*}
  2749 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  2750 apply (subgoal_tac "nat x div nat k < nat x")
  2751  apply (simp add: nat_div_distrib [symmetric])
  2752 apply (rule Divides.div_less_dividend, simp_all)
  2753 done
  2754 
  2755 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
  2756 proof
  2757   assume H: "x mod n = y mod n"
  2758   hence "x mod n - y mod n = 0" by simp
  2759   hence "(x mod n - y mod n) mod n = 0" by simp 
  2760   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
  2761   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
  2762 next
  2763   assume H: "n dvd x - y"
  2764   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
  2765   hence "x = n*k + y" by simp
  2766   hence "x mod n = (n*k + y) mod n" by simp
  2767   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
  2768 qed
  2769 
  2770 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
  2771   shows "\<exists>q. x = y + n * q"
  2772 proof-
  2773   from xy have th: "int x - int y = int (x - y)" by simp 
  2774   from xyn have "int x mod int n = int y mod int n" 
  2775     by (simp add: zmod_int [symmetric])
  2776   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
  2777   hence "n dvd x - y" by (simp add: th zdvd_int)
  2778   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  2779 qed
  2780 
  2781 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
  2782   (is "?lhs = ?rhs")
  2783 proof
  2784   assume H: "x mod n = y mod n"
  2785   {assume xy: "x \<le> y"
  2786     from H have th: "y mod n = x mod n" by simp
  2787     from nat_mod_eq_lemma[OF th xy] have ?rhs 
  2788       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  2789   moreover
  2790   {assume xy: "y \<le> x"
  2791     from nat_mod_eq_lemma[OF H xy] have ?rhs 
  2792       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  2793   ultimately  show ?rhs using linear[of x y] by blast  
  2794 next
  2795   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  2796   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  2797   thus  ?lhs by simp
  2798 qed
  2799 
  2800 text {*
  2801   This re-embedding of natural division on integers goes back to the
  2802   time when numerals had been signed numerals.  It should
  2803   now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
  2804 *}
  2805 
  2806 lemma div_nat_numeral [simp]:
  2807   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
  2808   by (simp add: nat_div_distrib)
  2809 
  2810 lemma one_div_nat_numeral [simp]:
  2811   "Suc 0 div numeral v' = nat (1 div numeral v')"
  2812   by (subst nat_div_distrib, simp_all)
  2813 
  2814 lemma mod_nat_numeral [simp]:
  2815   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
  2816   by (simp add: nat_mod_distrib)
  2817 
  2818 lemma one_mod_nat_numeral [simp]:
  2819   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
  2820   by (subst nat_mod_distrib) simp_all
  2821 
  2822 
  2823 subsubsection {* Tools setup *}
  2824 
  2825 text {* Nitpick *}
  2826 
  2827 lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
  2828 
  2829 
  2830 subsubsection {* Code generation *}
  2831 
  2832 definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
  2833 where
  2834   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
  2835 
  2836 lemma fst_divmod_abs [simp]:
  2837   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
  2838   by (simp add: divmod_abs_def)
  2839 
  2840 lemma snd_divmod_abs [simp]:
  2841   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
  2842   by (simp add: divmod_abs_def)
  2843 
  2844 lemma divmod_abs_code [code]:
  2845   "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
  2846   "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
  2847   "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
  2848   "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
  2849   "divmod_abs j 0 = (0, \<bar>j\<bar>)"
  2850   "divmod_abs 0 j = (0, 0)"
  2851   by (simp_all add: prod_eq_iff)
  2852 
  2853 lemma divmod_int_divmod_abs:
  2854   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
  2855   apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
  2856     then divmod_abs k l
  2857     else (let (r, s) = divmod_abs k l in
  2858        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
  2859 proof -
  2860   have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
  2861   show ?thesis
  2862     by (simp add: prod_eq_iff split_def Let_def)
  2863       (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
  2864       zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
  2865 qed
  2866 
  2867 lemma divmod_int_code [code]:
  2868   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
  2869   apsnd ((op *) (sgn l)) (if sgn k = sgn l
  2870     then divmod_abs k l
  2871     else (let (r, s) = divmod_abs k l in
  2872       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
  2873 proof -
  2874   have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
  2875     by (auto simp add: not_less sgn_if)
  2876   then show ?thesis by (simp add: divmod_int_divmod_abs)
  2877 qed
  2878 
  2879 hide_const (open) divmod_abs
  2880 
  2881 code_identifier
  2882   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2883 
  2884 end