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