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