src/HOL/Euclidean_Division.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (20 months ago)
changeset 66816 212a3334e7da
parent 66814 a24cde9588bb
child 66817 0b12755ccbb2
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/Euclidean_Division.thy
     2     Author:     Manuel Eberl, TU Muenchen
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 section \<open>Uniquely determined division in euclidean (semi)rings\<close>
     7 
     8 theory Euclidean_Division
     9   imports Nat_Transfer Lattices_Big
    10 begin
    11 
    12 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    13   
    14 class euclidean_semiring = semidom_modulo + normalization_semidom + 
    15   fixes euclidean_size :: "'a \<Rightarrow> nat"
    16   assumes size_0 [simp]: "euclidean_size 0 = 0"
    17   assumes mod_size_less: 
    18     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    19   assumes size_mult_mono:
    20     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    21 begin
    22 
    23 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
    24   by (subst mult.commute) (rule size_mult_mono)
    25 
    26 lemma euclidean_size_normalize [simp]:
    27   "euclidean_size (normalize a) = euclidean_size a"
    28 proof (cases "a = 0")
    29   case True
    30   then show ?thesis
    31     by simp
    32 next
    33   case [simp]: False
    34   have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    35     by (rule size_mult_mono) simp
    36   moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    37     by (rule size_mult_mono) simp
    38   ultimately show ?thesis
    39     by simp
    40 qed
    41 
    42 lemma dvd_euclidean_size_eq_imp_dvd:
    43   assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
    44     and "b dvd a" 
    45   shows "a dvd b"
    46 proof (rule ccontr)
    47   assume "\<not> a dvd b"
    48   hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
    49   then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
    50   from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
    51   then obtain c where "b mod a = b * c" unfolding dvd_def by blast
    52     with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
    53   with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
    54     using size_mult_mono by force
    55   moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
    56   have "euclidean_size (b mod a) < euclidean_size a"
    57     using mod_size_less by blast
    58   ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
    59     by simp
    60 qed
    61 
    62 lemma euclidean_size_times_unit:
    63   assumes "is_unit a"
    64   shows   "euclidean_size (a * b) = euclidean_size b"
    65 proof (rule antisym)
    66   from assms have [simp]: "a \<noteq> 0" by auto
    67   thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
    68   from assms have "is_unit (1 div a)" by simp
    69   hence "1 div a \<noteq> 0" by (intro notI) simp_all
    70   hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
    71     by (rule size_mult_mono')
    72   also from assms have "(1 div a) * (a * b) = b"
    73     by (simp add: algebra_simps unit_div_mult_swap)
    74   finally show "euclidean_size (a * b) \<le> euclidean_size b" .
    75 qed
    76 
    77 lemma euclidean_size_unit:
    78   "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
    79   using euclidean_size_times_unit [of a 1] by simp
    80 
    81 lemma unit_iff_euclidean_size: 
    82   "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
    83 proof safe
    84   assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
    85   show "is_unit a"
    86     by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
    87 qed (auto intro: euclidean_size_unit)
    88 
    89 lemma euclidean_size_times_nonunit:
    90   assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
    91   shows   "euclidean_size b < euclidean_size (a * b)"
    92 proof (rule ccontr)
    93   assume "\<not>euclidean_size b < euclidean_size (a * b)"
    94   with size_mult_mono'[OF assms(1), of b] 
    95     have eq: "euclidean_size (a * b) = euclidean_size b" by simp
    96   have "a * b dvd b"
    97     by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
    98   hence "a * b dvd 1 * b" by simp
    99   with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   100   with assms(3) show False by contradiction
   101 qed
   102 
   103 lemma dvd_imp_size_le:
   104   assumes "a dvd b" "b \<noteq> 0" 
   105   shows   "euclidean_size a \<le> euclidean_size b"
   106   using assms by (auto elim!: dvdE simp: size_mult_mono)
   107 
   108 lemma dvd_proper_imp_size_less:
   109   assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   110   shows   "euclidean_size a < euclidean_size b"
   111 proof -
   112   from assms(1) obtain c where "b = a * c" by (erule dvdE)
   113   hence z: "b = c * a" by (simp add: mult.commute)
   114   from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   115   with z assms show ?thesis
   116     by (auto intro!: euclidean_size_times_nonunit)
   117 qed
   118 
   119 lemma unit_imp_mod_eq_0:
   120   "a mod b = 0" if "is_unit b"
   121   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
   122 
   123 end
   124 
   125 class euclidean_ring = idom_modulo + euclidean_semiring
   126 
   127   
   128 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
   129 
   130 class euclidean_semiring_cancel = euclidean_semiring +
   131   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
   132   and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
   133 begin
   134 
   135 lemma div_mult_self2 [simp]:
   136   assumes "b \<noteq> 0"
   137   shows "(a + b * c) div b = c + a div b"
   138   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
   139 
   140 lemma div_mult_self3 [simp]:
   141   assumes "b \<noteq> 0"
   142   shows "(c * b + a) div b = c + a div b"
   143   using assms by (simp add: add.commute)
   144 
   145 lemma div_mult_self4 [simp]:
   146   assumes "b \<noteq> 0"
   147   shows "(b * c + a) div b = c + a div b"
   148   using assms by (simp add: add.commute)
   149 
   150 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
   151 proof (cases "b = 0")
   152   case True then show ?thesis by simp
   153 next
   154   case False
   155   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
   156     by (simp add: div_mult_mod_eq)
   157   also from False div_mult_self1 [of b a c] have
   158     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
   159       by (simp add: algebra_simps)
   160   finally have "a = a div b * b + (a + c * b) mod b"
   161     by (simp add: add.commute [of a] add.assoc distrib_right)
   162   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   163     by (simp add: div_mult_mod_eq)
   164   then show ?thesis by simp
   165 qed
   166 
   167 lemma mod_mult_self2 [simp]:
   168   "(a + b * c) mod b = a mod b"
   169   by (simp add: mult.commute [of b])
   170 
   171 lemma mod_mult_self3 [simp]:
   172   "(c * b + a) mod b = a mod b"
   173   by (simp add: add.commute)
   174 
   175 lemma mod_mult_self4 [simp]:
   176   "(b * c + a) mod b = a mod b"
   177   by (simp add: add.commute)
   178 
   179 lemma mod_mult_self1_is_0 [simp]:
   180   "b * a mod b = 0"
   181   using mod_mult_self2 [of 0 b a] by simp
   182 
   183 lemma mod_mult_self2_is_0 [simp]:
   184   "a * b mod b = 0"
   185   using mod_mult_self1 [of 0 a b] by simp
   186 
   187 lemma div_add_self1:
   188   assumes "b \<noteq> 0"
   189   shows "(b + a) div b = a div b + 1"
   190   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
   191 
   192 lemma div_add_self2:
   193   assumes "b \<noteq> 0"
   194   shows "(a + b) div b = a div b + 1"
   195   using assms div_add_self1 [of b a] by (simp add: add.commute)
   196 
   197 lemma mod_add_self1 [simp]:
   198   "(b + a) mod b = a mod b"
   199   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
   200 
   201 lemma mod_add_self2 [simp]:
   202   "(a + b) mod b = a mod b"
   203   using mod_mult_self1 [of a 1 b] by simp
   204 
   205 lemma mod_div_trivial [simp]:
   206   "a mod b div b = 0"
   207 proof (cases "b = 0")
   208   assume "b = 0"
   209   thus ?thesis by simp
   210 next
   211   assume "b \<noteq> 0"
   212   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
   213     by (rule div_mult_self1 [symmetric])
   214   also have "\<dots> = a div b"
   215     by (simp only: mod_div_mult_eq)
   216   also have "\<dots> = a div b + 0"
   217     by simp
   218   finally show ?thesis
   219     by (rule add_left_imp_eq)
   220 qed
   221 
   222 lemma mod_mod_trivial [simp]:
   223   "a mod b mod b = a mod b"
   224 proof -
   225   have "a mod b mod b = (a mod b + a div b * b) mod b"
   226     by (simp only: mod_mult_self1)
   227   also have "\<dots> = a mod b"
   228     by (simp only: mod_div_mult_eq)
   229   finally show ?thesis .
   230 qed
   231 
   232 lemma mod_mod_cancel:
   233   assumes "c dvd b"
   234   shows "a mod b mod c = a mod c"
   235 proof -
   236   from \<open>c dvd b\<close> obtain k where "b = c * k"
   237     by (rule dvdE)
   238   have "a mod b mod c = a mod (c * k) mod c"
   239     by (simp only: \<open>b = c * k\<close>)
   240   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   241     by (simp only: mod_mult_self1)
   242   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   243     by (simp only: ac_simps)
   244   also have "\<dots> = a mod c"
   245     by (simp only: div_mult_mod_eq)
   246   finally show ?thesis .
   247 qed
   248 
   249 lemma div_mult_mult2 [simp]:
   250   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   251   by (drule div_mult_mult1) (simp add: mult.commute)
   252 
   253 lemma div_mult_mult1_if [simp]:
   254   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   255   by simp_all
   256 
   257 lemma mod_mult_mult1:
   258   "(c * a) mod (c * b) = c * (a mod b)"
   259 proof (cases "c = 0")
   260   case True then show ?thesis by simp
   261 next
   262   case False
   263   from div_mult_mod_eq
   264   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   265   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   266     = c * a + c * (a mod b)" by (simp add: algebra_simps)
   267   with div_mult_mod_eq show ?thesis by simp
   268 qed
   269 
   270 lemma mod_mult_mult2:
   271   "(a * c) mod (b * c) = (a mod b) * c"
   272   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   273 
   274 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   275   by (fact mod_mult_mult2 [symmetric])
   276 
   277 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   278   by (fact mod_mult_mult1 [symmetric])
   279 
   280 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   281   unfolding dvd_def by (auto simp add: mod_mult_mult1)
   282 
   283 lemma div_plus_div_distrib_dvd_left:
   284   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   285   by (cases "c = 0") (auto elim: dvdE)
   286 
   287 lemma div_plus_div_distrib_dvd_right:
   288   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   289   using div_plus_div_distrib_dvd_left [of c b a]
   290   by (simp add: ac_simps)
   291 
   292 named_theorems mod_simps
   293 
   294 text \<open>Addition respects modular equivalence.\<close>
   295 
   296 lemma mod_add_left_eq [mod_simps]:
   297   "(a mod c + b) mod c = (a + b) mod c"
   298 proof -
   299   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   300     by (simp only: div_mult_mod_eq)
   301   also have "\<dots> = (a mod c + b + a div c * c) mod c"
   302     by (simp only: ac_simps)
   303   also have "\<dots> = (a mod c + b) mod c"
   304     by (rule mod_mult_self1)
   305   finally show ?thesis
   306     by (rule sym)
   307 qed
   308 
   309 lemma mod_add_right_eq [mod_simps]:
   310   "(a + b mod c) mod c = (a + b) mod c"
   311   using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   312 
   313 lemma mod_add_eq:
   314   "(a mod c + b mod c) mod c = (a + b) mod c"
   315   by (simp add: mod_add_left_eq mod_add_right_eq)
   316 
   317 lemma mod_sum_eq [mod_simps]:
   318   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   319 proof (induct A rule: infinite_finite_induct)
   320   case (insert i A)
   321   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   322     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   323     by simp
   324   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   325     by (simp add: mod_simps)
   326   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   327     by (simp add: insert.hyps)
   328   finally show ?case
   329     by (simp add: insert.hyps mod_simps)
   330 qed simp_all
   331 
   332 lemma mod_add_cong:
   333   assumes "a mod c = a' mod c"
   334   assumes "b mod c = b' mod c"
   335   shows "(a + b) mod c = (a' + b') mod c"
   336 proof -
   337   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   338     unfolding assms ..
   339   then show ?thesis
   340     by (simp add: mod_add_eq)
   341 qed
   342 
   343 text \<open>Multiplication respects modular equivalence.\<close>
   344 
   345 lemma mod_mult_left_eq [mod_simps]:
   346   "((a mod c) * b) mod c = (a * b) mod c"
   347 proof -
   348   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   349     by (simp only: div_mult_mod_eq)
   350   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   351     by (simp only: algebra_simps)
   352   also have "\<dots> = (a mod c * b) mod c"
   353     by (rule mod_mult_self1)
   354   finally show ?thesis
   355     by (rule sym)
   356 qed
   357 
   358 lemma mod_mult_right_eq [mod_simps]:
   359   "(a * (b mod c)) mod c = (a * b) mod c"
   360   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   361 
   362 lemma mod_mult_eq:
   363   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   364   by (simp add: mod_mult_left_eq mod_mult_right_eq)
   365 
   366 lemma mod_prod_eq [mod_simps]:
   367   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   368 proof (induct A rule: infinite_finite_induct)
   369   case (insert i A)
   370   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   371     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   372     by simp
   373   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   374     by (simp add: mod_simps)
   375   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   376     by (simp add: insert.hyps)
   377   finally show ?case
   378     by (simp add: insert.hyps mod_simps)
   379 qed simp_all
   380 
   381 lemma mod_mult_cong:
   382   assumes "a mod c = a' mod c"
   383   assumes "b mod c = b' mod c"
   384   shows "(a * b) mod c = (a' * b') mod c"
   385 proof -
   386   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   387     unfolding assms ..
   388   then show ?thesis
   389     by (simp add: mod_mult_eq)
   390 qed
   391 
   392 text \<open>Exponentiation respects modular equivalence.\<close>
   393 
   394 lemma power_mod [mod_simps]: 
   395   "((a mod b) ^ n) mod b = (a ^ n) mod b"
   396 proof (induct n)
   397   case 0
   398   then show ?case by simp
   399 next
   400   case (Suc n)
   401   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   402     by (simp add: mod_mult_right_eq)
   403   with Suc show ?case
   404     by (simp add: mod_mult_left_eq mod_mult_right_eq)
   405 qed
   406 
   407 end
   408 
   409 
   410 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
   411 begin
   412 
   413 subclass idom_divide ..
   414 
   415 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   416   using div_mult_mult1 [of "- 1" a b] by simp
   417 
   418 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   419   using mod_mult_mult1 [of "- 1" a b] by simp
   420 
   421 lemma div_minus_right: "a div (- b) = (- a) div b"
   422   using div_minus_minus [of "- a" b] by simp
   423 
   424 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   425   using mod_minus_minus [of "- a" b] by simp
   426 
   427 lemma div_minus1_right [simp]: "a div (- 1) = - a"
   428   using div_minus_right [of a 1] by simp
   429 
   430 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   431   using mod_minus_right [of a 1] by simp
   432 
   433 text \<open>Negation respects modular equivalence.\<close>
   434 
   435 lemma mod_minus_eq [mod_simps]:
   436   "(- (a mod b)) mod b = (- a) mod b"
   437 proof -
   438   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   439     by (simp only: div_mult_mod_eq)
   440   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   441     by (simp add: ac_simps)
   442   also have "\<dots> = (- (a mod b)) mod b"
   443     by (rule mod_mult_self1)
   444   finally show ?thesis
   445     by (rule sym)
   446 qed
   447 
   448 lemma mod_minus_cong:
   449   assumes "a mod b = a' mod b"
   450   shows "(- a) mod b = (- a') mod b"
   451 proof -
   452   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   453     unfolding assms ..
   454   then show ?thesis
   455     by (simp add: mod_minus_eq)
   456 qed
   457 
   458 text \<open>Subtraction respects modular equivalence.\<close>
   459 
   460 lemma mod_diff_left_eq [mod_simps]:
   461   "(a mod c - b) mod c = (a - b) mod c"
   462   using mod_add_cong [of a c "a mod c" "- b" "- b"]
   463   by simp
   464 
   465 lemma mod_diff_right_eq [mod_simps]:
   466   "(a - b mod c) mod c = (a - b) mod c"
   467   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   468   by simp
   469 
   470 lemma mod_diff_eq:
   471   "(a mod c - b mod c) mod c = (a - b) mod c"
   472   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   473   by simp
   474 
   475 lemma mod_diff_cong:
   476   assumes "a mod c = a' mod c"
   477   assumes "b mod c = b' mod c"
   478   shows "(a - b) mod c = (a' - b') mod c"
   479   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   480   by simp
   481 
   482 lemma minus_mod_self2 [simp]:
   483   "(a - b) mod b = a mod b"
   484   using mod_diff_right_eq [of a b b]
   485   by (simp add: mod_diff_right_eq)
   486 
   487 lemma minus_mod_self1 [simp]:
   488   "(b - a) mod b = - a mod b"
   489   using mod_add_self2 [of "- a" b] by simp
   490 
   491 lemma mod_eq_dvd_iff:
   492   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   493 proof
   494   assume ?P
   495   then have "(a mod c - b mod c) mod c = 0"
   496     by simp
   497   then show ?Q
   498     by (simp add: dvd_eq_mod_eq_0 mod_simps)
   499 next
   500   assume ?Q
   501   then obtain d where d: "a - b = c * d" ..
   502   then have "a = c * d + b"
   503     by (simp add: algebra_simps)
   504   then show ?P by simp
   505 qed
   506 
   507 end
   508 
   509   
   510 subsection \<open>Uniquely determined division\<close>
   511   
   512 class unique_euclidean_semiring = euclidean_semiring + 
   513   fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   514   assumes size_mono_mult:
   515     "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   516       \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   517     -- \<open>FIXME justify\<close>
   518   assumes uniqueness_constraint_mono_mult:
   519     "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   520   assumes uniqueness_constraint_mod:
   521     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   522   assumes div_bounded:
   523     "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   524     \<Longrightarrow> euclidean_size r < euclidean_size b
   525     \<Longrightarrow> (q * b + r) div b = q"
   526 begin
   527 
   528 lemma divmod_cases [case_names divides remainder by0]:
   529   obtains 
   530     (divides) q where "b \<noteq> 0"
   531       and "a div b = q"
   532       and "a mod b = 0"
   533       and "a = q * b"
   534   | (remainder) q r where "b \<noteq> 0"
   535       and "uniqueness_constraint r b"
   536       and "euclidean_size r < euclidean_size b"
   537       and "r \<noteq> 0"
   538       and "a div b = q"
   539       and "a mod b = r"
   540       and "a = q * b + r"
   541   | (by0) "b = 0"
   542 proof (cases "b = 0")
   543   case True
   544   then show thesis
   545   by (rule by0)
   546 next
   547   case False
   548   show thesis
   549   proof (cases "b dvd a")
   550     case True
   551     then obtain q where "a = b * q" ..
   552     with \<open>b \<noteq> 0\<close> divides
   553     show thesis
   554       by (simp add: ac_simps)
   555   next
   556     case False
   557     then have "a mod b \<noteq> 0"
   558       by (simp add: mod_eq_0_iff_dvd)
   559     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   560       by (rule uniqueness_constraint_mod)
   561     moreover have "euclidean_size (a mod b) < euclidean_size b"
   562       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   563     moreover have "a = a div b * b + a mod b"
   564       by (simp add: div_mult_mod_eq)
   565     ultimately show thesis
   566       using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   567   qed
   568 qed
   569 
   570 lemma div_eqI:
   571   "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   572     "euclidean_size r < euclidean_size b" "q * b + r = a"
   573 proof -
   574   from that have "(q * b + r) div b = q"
   575     by (auto intro: div_bounded)
   576   with that show ?thesis
   577     by simp
   578 qed
   579 
   580 lemma mod_eqI:
   581   "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   582     "euclidean_size r < euclidean_size b" "q * b + r = a" 
   583 proof -
   584   from that have "a div b = q"
   585     by (rule div_eqI)
   586   moreover have "a div b * b + a mod b = a"
   587     by (fact div_mult_mod_eq)
   588   ultimately have "a div b * b + a mod b = a div b * b + r"
   589     using \<open>q * b + r = a\<close> by simp
   590   then show ?thesis
   591     by simp
   592 qed
   593 
   594 subclass euclidean_semiring_cancel
   595 proof
   596   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   597   proof (cases a b rule: divmod_cases)
   598     case by0
   599     with \<open>b \<noteq> 0\<close> show ?thesis
   600       by simp
   601   next
   602     case (divides q)
   603     then show ?thesis
   604       by (simp add: ac_simps)
   605   next
   606     case (remainder q r)
   607     then show ?thesis
   608       by (auto intro: div_eqI simp add: algebra_simps)
   609   qed
   610 next
   611   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   612   proof (cases a b rule: divmod_cases)
   613     case by0
   614     then show ?thesis
   615       by simp
   616   next
   617     case (divides q)
   618     with \<open>c \<noteq> 0\<close> show ?thesis
   619       by (simp add: mult.left_commute [of c])
   620   next
   621     case (remainder q r)
   622     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   623       by simp
   624     from remainder \<open>c \<noteq> 0\<close>
   625     have "uniqueness_constraint (r * c) (b * c)"
   626       and "euclidean_size (r * c) < euclidean_size (b * c)"
   627       by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   628     with remainder show ?thesis
   629       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   630         (use \<open>b * c \<noteq> 0\<close> in simp)
   631   qed
   632 qed
   633 
   634 lemma div_mult1_eq:
   635   "(a * b) div c = a * (b div c) + a * (b mod c) div c"
   636 proof (cases "a * (b mod c)" c rule: divmod_cases)
   637   case (divides q)
   638   have "a * b = a * (b div c * c + b mod c)"
   639     by (simp add: div_mult_mod_eq)
   640   also have "\<dots> = (a * (b div c) + q) * c"
   641     using divides by (simp add: algebra_simps)
   642   finally have "(a * b) div c = \<dots> div c"
   643     by simp
   644   with divides show ?thesis
   645     by simp
   646 next
   647   case (remainder q r)
   648   from remainder(1-3) show ?thesis
   649   proof (rule div_eqI)
   650     have "a * b = a * (b div c * c + b mod c)"
   651       by (simp add: div_mult_mod_eq)
   652     also have "\<dots> = a * c * (b div c) + q * c + r"
   653       using remainder by (simp add: algebra_simps)
   654     finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
   655       using remainder(5-7) by (simp add: algebra_simps)
   656   qed
   657 next
   658   case by0
   659   then show ?thesis
   660     by simp
   661 qed
   662 
   663 lemma div_add1_eq:
   664   "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
   665 proof (cases "a mod c + b mod c" c rule: divmod_cases)
   666   case (divides q)
   667   have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
   668     using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
   669   also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
   670     by (simp add: algebra_simps)
   671   also have "\<dots> = (a div c + b div c + q) * c"
   672     using divides by (simp add: algebra_simps)
   673   finally have "(a + b) div c = (a div c + b div c + q) * c div c"
   674     by simp
   675   with divides show ?thesis
   676     by simp
   677 next
   678   case (remainder q r)
   679   from remainder(1-3) show ?thesis
   680   proof (rule div_eqI)
   681     have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
   682         (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
   683       by (simp add: algebra_simps)
   684     also have "\<dots> = a + b + (a mod c + b mod c)"
   685       by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
   686     finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
   687       using remainder by simp
   688   qed
   689 next
   690   case by0
   691   then show ?thesis
   692     by simp
   693 qed
   694 
   695 end
   696 
   697 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   698 begin
   699   
   700 subclass euclidean_ring_cancel ..
   701 
   702 end
   703 
   704 
   705 subsection \<open>Euclidean division on @{typ nat}\<close>
   706 
   707 instantiation nat :: normalization_semidom
   708 begin
   709 
   710 definition normalize_nat :: "nat \<Rightarrow> nat"
   711   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   712 
   713 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   714   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   715 
   716 lemma unit_factor_simps [simp]:
   717   "unit_factor 0 = (0::nat)"
   718   "unit_factor (Suc n) = 1"
   719   by (simp_all add: unit_factor_nat_def)
   720 
   721 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   722   where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
   723 
   724 instance
   725   by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
   726 
   727 end
   728 
   729 instantiation nat :: unique_euclidean_semiring
   730 begin
   731 
   732 definition euclidean_size_nat :: "nat \<Rightarrow> nat"
   733   where [simp]: "euclidean_size_nat = id"
   734 
   735 definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   736   where [simp]: "uniqueness_constraint_nat = \<top>"
   737 
   738 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   739   where "m mod n = m - (m div n * (n::nat))"
   740 
   741 instance proof
   742   fix m n :: nat
   743   have ex: "\<exists>k. k * n \<le> l" for l :: nat
   744     by (rule exI [of _ 0]) simp
   745   have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
   746   proof -
   747     from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
   748       by (cases n) auto
   749     then show ?thesis
   750       by (rule finite_subset) simp
   751   qed
   752   have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
   753   proof (cases "n = 0")
   754     case True
   755     moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
   756       by auto
   757     ultimately show ?thesis
   758       by simp
   759   next
   760     case False
   761     with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
   762       by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
   763     also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
   764       by (auto simp add: ac_simps elim!: dvdE)
   765     finally show ?thesis
   766       using False by (simp add: divide_nat_def ac_simps)
   767   qed
   768   have less_eq: "m div n * n \<le> m"
   769     by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
   770   then show "m div n * n + m mod n = m"
   771     by (simp add: modulo_nat_def)
   772   assume "n \<noteq> 0" 
   773   show "euclidean_size (m mod n) < euclidean_size n"
   774   proof -
   775     have "m < Suc (m div n) * n"
   776     proof (rule ccontr)
   777       assume "\<not> m < Suc (m div n) * n"
   778       then have "Suc (m div n) * n \<le> m"
   779         by (simp add: not_less)
   780       moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
   781         by (simp add: divide_nat_def)
   782       with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
   783         by auto
   784       ultimately have "Suc (m div n) < Suc (m div n)"
   785         by blast
   786       then show False
   787         by simp
   788     qed
   789     with \<open>n \<noteq> 0\<close> show ?thesis
   790       by (simp add: modulo_nat_def)
   791   qed
   792   show "euclidean_size m \<le> euclidean_size (m * n)"
   793     using \<open>n \<noteq> 0\<close> by (cases n) simp_all
   794   fix q r :: nat
   795   show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
   796   proof -
   797     from that have "r < n"
   798       by simp
   799     have "k \<le> q" if "k * n \<le> q * n + r" for k
   800     proof (rule ccontr)
   801       assume "\<not> k \<le> q"
   802       then have "q < k"
   803         by simp
   804       then obtain l where "k = Suc (q + l)"
   805         by (auto simp add: less_iff_Suc_add)
   806       with \<open>r < n\<close> that show False
   807         by (simp add: algebra_simps)
   808     qed
   809     with \<open>n \<noteq> 0\<close> ex fin show ?thesis
   810       by (auto simp add: divide_nat_def Max_eq_iff)
   811   qed
   812 qed simp_all
   813 
   814 end
   815 
   816 text \<open>Tool support\<close>
   817 
   818 ML \<open>
   819 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   820 (
   821   val div_name = @{const_name divide};
   822   val mod_name = @{const_name modulo};
   823   val mk_binop = HOLogic.mk_binop;
   824   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   825   val mk_sum = Arith_Data.mk_sum;
   826   fun dest_sum tm =
   827     if HOLogic.is_zero tm then []
   828     else
   829       (case try HOLogic.dest_Suc tm of
   830         SOME t => HOLogic.Suc_zero :: dest_sum t
   831       | NONE =>
   832           (case try dest_plus tm of
   833             SOME (t, u) => dest_sum t @ dest_sum u
   834           | NONE => [tm]));
   835 
   836   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   837 
   838   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   839     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   840 )
   841 \<close>
   842 
   843 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   844   \<open>K Cancel_Div_Mod_Nat.proc\<close>
   845 
   846 lemma div_nat_eqI:
   847   "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
   848   by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   849 
   850 lemma mod_nat_eqI:
   851   "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
   852   by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   853 
   854 lemma div_mult_self_is_m [simp]:
   855   "m * n div n = m" if "n > 0" for m n :: nat
   856   using that by simp
   857 
   858 lemma div_mult_self1_is_m [simp]:
   859   "n * m div n = m" if "n > 0" for m n :: nat
   860   using that by simp
   861 
   862 lemma mod_less_divisor [simp]:
   863   "m mod n < n" if "n > 0" for m n :: nat
   864   using mod_size_less [of n m] that by simp
   865 
   866 lemma mod_le_divisor [simp]:
   867   "m mod n \<le> n" if "n > 0" for m n :: nat
   868   using that by (auto simp add: le_less)
   869 
   870 lemma div_times_less_eq_dividend [simp]:
   871   "m div n * n \<le> m" for m n :: nat
   872   by (simp add: minus_mod_eq_div_mult [symmetric])
   873 
   874 lemma times_div_less_eq_dividend [simp]:
   875   "n * (m div n) \<le> m" for m n :: nat
   876   using div_times_less_eq_dividend [of m n]
   877   by (simp add: ac_simps)
   878 
   879 lemma dividend_less_div_times:
   880   "m < n + (m div n) * n" if "0 < n" for m n :: nat
   881 proof -
   882   from that have "m mod n < n"
   883     by simp
   884   then show ?thesis
   885     by (simp add: minus_mod_eq_div_mult [symmetric])
   886 qed
   887 
   888 lemma dividend_less_times_div:
   889   "m < n + n * (m div n)" if "0 < n" for m n :: nat
   890   using dividend_less_div_times [of n m] that
   891   by (simp add: ac_simps)
   892 
   893 lemma mod_Suc_le_divisor [simp]:
   894   "m mod Suc n \<le> n"
   895   using mod_less_divisor [of "Suc n" m] by arith
   896 
   897 lemma mod_less_eq_dividend [simp]:
   898   "m mod n \<le> m" for m n :: nat
   899 proof (rule add_leD2)
   900   from div_mult_mod_eq have "m div n * n + m mod n = m" .
   901   then show "m div n * n + m mod n \<le> m" by auto
   902 qed
   903 
   904 lemma
   905   div_less [simp]: "m div n = 0"
   906   and mod_less [simp]: "m mod n = m"
   907   if "m < n" for m n :: nat
   908   using that by (auto intro: div_eqI mod_eqI) 
   909 
   910 lemma le_div_geq:
   911   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
   912 proof -
   913   from \<open>n \<le> m\<close> obtain q where "m = n + q"
   914     by (auto simp add: le_iff_add)
   915   with \<open>0 < n\<close> show ?thesis
   916     by (simp add: div_add_self1)
   917 qed
   918 
   919 lemma le_mod_geq:
   920   "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
   921 proof -
   922   from \<open>n \<le> m\<close> obtain q where "m = n + q"
   923     by (auto simp add: le_iff_add)
   924   then show ?thesis
   925     by simp
   926 qed
   927 
   928 lemma div_if:
   929   "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
   930   by (simp add: le_div_geq)
   931 
   932 lemma mod_if:
   933   "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
   934   by (simp add: le_mod_geq)
   935 
   936 lemma div_eq_0_iff:
   937   "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
   938   by (simp add: div_if)
   939 
   940 lemma div_greater_zero_iff:
   941   "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
   942   using div_eq_0_iff [of m n] by auto
   943 
   944 lemma mod_greater_zero_iff_not_dvd:
   945   "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
   946   by (simp add: dvd_eq_mod_eq_0)
   947 
   948 lemma div_by_Suc_0 [simp]:
   949   "m div Suc 0 = m"
   950   using div_by_1 [of m] by simp
   951 
   952 lemma mod_by_Suc_0 [simp]:
   953   "m mod Suc 0 = 0"
   954   using mod_by_1 [of m] by simp
   955 
   956 lemma div2_Suc_Suc [simp]:
   957   "Suc (Suc m) div 2 = Suc (m div 2)"
   958   by (simp add: numeral_2_eq_2 le_div_geq)
   959 
   960 lemma Suc_n_div_2_gt_zero [simp]:
   961   "0 < Suc n div 2" if "n > 0" for n :: nat
   962   using that by (cases n) simp_all
   963 
   964 lemma div_2_gt_zero [simp]:
   965   "0 < n div 2" if "Suc 0 < n" for n :: nat
   966   using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
   967 
   968 lemma mod2_Suc_Suc [simp]:
   969   "Suc (Suc m) mod 2 = m mod 2"
   970   by (simp add: numeral_2_eq_2 le_mod_geq)
   971 
   972 lemma add_self_div_2 [simp]:
   973   "(m + m) div 2 = m" for m :: nat
   974   by (simp add: mult_2 [symmetric])
   975 
   976 lemma add_self_mod_2 [simp]:
   977   "(m + m) mod 2 = 0" for m :: nat
   978   by (simp add: mult_2 [symmetric])
   979 
   980 lemma mod2_gr_0 [simp]:
   981   "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
   982 proof -
   983   have "m mod 2 < 2"
   984     by (rule mod_less_divisor) simp
   985   then have "m mod 2 = 0 \<or> m mod 2 = 1"
   986     by arith
   987   then show ?thesis
   988     by auto     
   989 qed
   990 
   991 lemma mod_Suc_eq [mod_simps]:
   992   "Suc (m mod n) mod n = Suc m mod n"
   993 proof -
   994   have "(m mod n + 1) mod n = (m + 1) mod n"
   995     by (simp only: mod_simps)
   996   then show ?thesis
   997     by simp
   998 qed
   999 
  1000 lemma mod_Suc_Suc_eq [mod_simps]:
  1001   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
  1002 proof -
  1003   have "(m mod n + 2) mod n = (m + 2) mod n"
  1004     by (simp only: mod_simps)
  1005   then show ?thesis
  1006     by simp
  1007 qed
  1008 
  1009 lemma
  1010   Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
  1011   and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
  1012   and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
  1013   and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
  1014   by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
  1015 
  1016 context
  1017   fixes m n q :: nat
  1018 begin
  1019 
  1020 private lemma eucl_rel_mult2:
  1021   "m mod n + n * (m div n mod q) < n * q"
  1022   if "n > 0" and "q > 0"
  1023 proof -
  1024   from \<open>n > 0\<close> have "m mod n < n"
  1025     by (rule mod_less_divisor)
  1026   from \<open>q > 0\<close> have "m div n mod q < q"
  1027     by (rule mod_less_divisor)
  1028   then obtain s where "q = Suc (m div n mod q + s)"
  1029     by (blast dest: less_imp_Suc_add)
  1030   moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
  1031     using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
  1032   ultimately show ?thesis
  1033     by simp
  1034 qed
  1035 
  1036 lemma div_mult2_eq:
  1037   "m div (n * q) = (m div n) div q"
  1038 proof (cases "n = 0 \<or> q = 0")
  1039   case True
  1040   then show ?thesis
  1041     by auto
  1042 next
  1043   case False
  1044   with eucl_rel_mult2 show ?thesis
  1045     by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
  1046       simp add: algebra_simps add_mult_distrib2 [symmetric])
  1047 qed
  1048 
  1049 lemma mod_mult2_eq:
  1050   "m mod (n * q) = n * (m div n mod q) + m mod n"
  1051 proof (cases "n = 0 \<or> q = 0")
  1052   case True
  1053   then show ?thesis
  1054     by auto
  1055 next
  1056   case False
  1057   with eucl_rel_mult2 show ?thesis
  1058     by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
  1059       simp add: algebra_simps add_mult_distrib2 [symmetric])
  1060 qed
  1061 
  1062 end
  1063 
  1064 lemma div_le_mono:
  1065   "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
  1066 proof -
  1067   from that obtain q where "n = m + q"
  1068     by (auto simp add: le_iff_add)
  1069   then show ?thesis
  1070     by (simp add: div_add1_eq [of m q k])
  1071 qed
  1072 
  1073 text \<open>Antimonotonicity of @{const divide} in second argument\<close>
  1074 
  1075 lemma div_le_mono2:
  1076   "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
  1077 using that proof (induct k arbitrary: m rule: less_induct)
  1078   case (less k)
  1079   show ?case
  1080   proof (cases "n \<le> k")
  1081     case False
  1082     then show ?thesis
  1083       by simp
  1084   next
  1085     case True
  1086     have "(k - n) div n \<le> (k - m) div n"
  1087       using less.prems
  1088       by (blast intro: div_le_mono diff_le_mono2)
  1089     also have "\<dots> \<le> (k - m) div m"
  1090       using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
  1091       by simp
  1092     finally show ?thesis
  1093       using \<open>n \<le> k\<close> less.prems
  1094       by (simp add: le_div_geq)
  1095   qed
  1096 qed
  1097 
  1098 lemma div_le_dividend [simp]:
  1099   "m div n \<le> m" for m n :: nat
  1100   using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
  1101 
  1102 lemma div_less_dividend [simp]:
  1103   "m div n < m" if "1 < n" and "0 < m" for m n :: nat
  1104 using that proof (induct m rule: less_induct)
  1105   case (less m)
  1106   show ?case
  1107   proof (cases "n < m")
  1108     case False
  1109     with less show ?thesis
  1110       by (cases "n = m") simp_all
  1111   next
  1112     case True
  1113     then show ?thesis
  1114       using less.hyps [of "m - n"] less.prems
  1115       by (simp add: le_div_geq)
  1116   qed
  1117 qed
  1118 
  1119 lemma div_eq_dividend_iff:
  1120   "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
  1121 proof
  1122   assume "n = 1"
  1123   then show "m div n = m"
  1124     by simp
  1125 next
  1126   assume P: "m div n = m"
  1127   show "n = 1"
  1128   proof (rule ccontr)
  1129     have "n \<noteq> 0"
  1130       by (rule ccontr) (use that P in auto)
  1131     moreover assume "n \<noteq> 1"
  1132     ultimately have "n > 1"
  1133       by simp
  1134     with that have "m div n < m"
  1135       by simp
  1136     with P show False
  1137       by simp
  1138   qed
  1139 qed
  1140 
  1141 lemma less_mult_imp_div_less:
  1142   "m div n < i" if "m < i * n" for m n i :: nat
  1143 proof -
  1144   from that have "i * n > 0"
  1145     by (cases "i * n = 0") simp_all
  1146   then have "i > 0" and "n > 0"
  1147     by simp_all
  1148   have "m div n * n \<le> m"
  1149     by simp
  1150   then have "m div n * n < i * n"
  1151     using that by (rule le_less_trans)
  1152   with \<open>n > 0\<close> show ?thesis
  1153     by simp
  1154 qed
  1155 
  1156 text \<open>A fact for the mutilated chess board\<close>
  1157 
  1158 lemma mod_Suc:
  1159   "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
  1160 proof (cases "n = 0")
  1161   case True
  1162   then show ?thesis
  1163     by simp
  1164 next
  1165   case False
  1166   have "Suc m mod n = Suc (m mod n) mod n"
  1167     by (simp add: mod_simps)
  1168   also have "\<dots> = ?rhs"
  1169     using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
  1170   finally show ?thesis .
  1171 qed
  1172 
  1173 lemma Suc_times_mod_eq:
  1174   "Suc (m * n) mod m = 1" if "Suc 0 < m"
  1175   using that by (simp add: mod_Suc)
  1176 
  1177 lemma Suc_times_numeral_mod_eq [simp]:
  1178   "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
  1179   by (rule Suc_times_mod_eq) (use that in simp)
  1180 
  1181 lemma Suc_div_le_mono [simp]:
  1182   "m div n \<le> Suc m div n"
  1183   by (simp add: div_le_mono)
  1184 
  1185 text \<open>These lemmas collapse some needless occurrences of Suc:
  1186   at least three Sucs, since two and fewer are rewritten back to Suc again!
  1187   We already have some rules to simplify operands smaller than 3.\<close>
  1188 
  1189 lemma div_Suc_eq_div_add3 [simp]:
  1190   "m div Suc (Suc (Suc n)) = m div (3 + n)"
  1191   by (simp add: Suc3_eq_add_3)
  1192 
  1193 lemma mod_Suc_eq_mod_add3 [simp]:
  1194   "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
  1195   by (simp add: Suc3_eq_add_3)
  1196 
  1197 lemma Suc_div_eq_add3_div:
  1198   "Suc (Suc (Suc m)) div n = (3 + m) div n"
  1199   by (simp add: Suc3_eq_add_3)
  1200 
  1201 lemma Suc_mod_eq_add3_mod:
  1202   "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
  1203   by (simp add: Suc3_eq_add_3)
  1204 
  1205 lemmas Suc_div_eq_add3_div_numeral [simp] =
  1206   Suc_div_eq_add3_div [of _ "numeral v"] for v
  1207 
  1208 lemmas Suc_mod_eq_add3_mod_numeral [simp] =
  1209   Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1210 
  1211 lemma (in field_char_0) of_nat_div:
  1212   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
  1213 proof -
  1214   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
  1215     unfolding of_nat_add by (cases "n = 0") simp_all
  1216   then show ?thesis
  1217     by simp
  1218 qed
  1219 
  1220 text \<open>An ``induction'' law for modulus arithmetic.\<close>
  1221 
  1222 lemma mod_induct [consumes 3, case_names step]:
  1223   "P m" if "P n" and "n < p" and "m < p"
  1224     and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
  1225 using \<open>m < p\<close> proof (induct m)
  1226   case 0
  1227   show ?case
  1228   proof (rule ccontr)
  1229     assume "\<not> P 0"
  1230     from \<open>n < p\<close> have "0 < p"
  1231       by simp
  1232     from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
  1233       by (blast dest: less_imp_add_positive)
  1234     with \<open>P n\<close> have "P (p - m)"
  1235       by simp
  1236     moreover have "\<not> P (p - m)"
  1237     using \<open>0 < m\<close> proof (induct m)
  1238       case 0
  1239       then show ?case
  1240         by simp
  1241     next
  1242       case (Suc m)
  1243       show ?case
  1244       proof
  1245         assume P: "P (p - Suc m)"
  1246         with \<open>\<not> P 0\<close> have "Suc m < p"
  1247           by (auto intro: ccontr) 
  1248         then have "Suc (p - Suc m) = p - m"
  1249           by arith
  1250         moreover from \<open>0 < p\<close> have "p - Suc m < p"
  1251           by arith
  1252         with P step have "P ((Suc (p - Suc m)) mod p)"
  1253           by blast
  1254         ultimately show False
  1255           using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
  1256       qed
  1257     qed
  1258     ultimately show False
  1259       by blast
  1260   qed
  1261 next
  1262   case (Suc m)
  1263   then have "m < p" and mod: "Suc m mod p = Suc m"
  1264     by simp_all
  1265   from \<open>m < p\<close> have "P m"
  1266     by (rule Suc.hyps)
  1267   with \<open>m < p\<close> have "P (Suc m mod p)"
  1268     by (rule step)
  1269   with mod show ?case
  1270     by simp
  1271 qed
  1272 
  1273 lemma split_div:
  1274   "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
  1275      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
  1276      (is "?P = ?Q") for m n :: nat
  1277 proof (cases "n = 0")
  1278   case True
  1279   then show ?thesis
  1280     by simp
  1281 next
  1282   case False
  1283   show ?thesis
  1284   proof
  1285     assume ?P
  1286     with False show ?Q
  1287       by auto
  1288   next
  1289     assume ?Q
  1290     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
  1291       by simp
  1292     with False show ?P
  1293       by (auto intro: * [of "m mod n"])
  1294   qed
  1295 qed
  1296 
  1297 lemma split_div':
  1298   "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
  1299 proof (cases "n = 0")
  1300   case True
  1301   then show ?thesis
  1302     by simp
  1303 next
  1304   case False
  1305   then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
  1306     by (auto intro: div_nat_eqI dividend_less_times_div)
  1307   then show ?thesis
  1308     by auto
  1309 qed
  1310 
  1311 lemma split_mod:
  1312   "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
  1313      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
  1314      (is "?P \<longleftrightarrow> ?Q") for m n :: nat
  1315 proof (cases "n = 0")
  1316   case True
  1317   then show ?thesis
  1318     by simp
  1319 next
  1320   case False
  1321   show ?thesis
  1322   proof
  1323     assume ?P
  1324     with False show ?Q
  1325       by auto
  1326   next
  1327     assume ?Q
  1328     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
  1329       by simp
  1330     with False show ?P
  1331       by (auto intro: * [of _ "m div n"])
  1332   qed
  1333 qed
  1334 
  1335 
  1336 subsection \<open>Euclidean division on @{typ int}\<close>
  1337 
  1338 instantiation int :: normalization_semidom
  1339 begin
  1340 
  1341 definition normalize_int :: "int \<Rightarrow> int"
  1342   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
  1343 
  1344 definition unit_factor_int :: "int \<Rightarrow> int"
  1345   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
  1346 
  1347 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1348   where "k div l = (if l = 0 then 0
  1349     else if sgn k = sgn l
  1350       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
  1351       else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
  1352 
  1353 lemma divide_int_unfold:
  1354   "(sgn k * int m) div (sgn l * int n) =
  1355    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
  1356     else if sgn k = sgn l
  1357       then int (m div n)
  1358       else - int (m div n + of_bool (\<not> n dvd m)))"
  1359   by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
  1360     nat_mult_distrib dvd_int_iff)
  1361 
  1362 instance proof
  1363   fix k :: int show "k div 0 = 0"
  1364   by (simp add: divide_int_def)
  1365 next
  1366   fix k l :: int
  1367   assume "l \<noteq> 0"
  1368   obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 
  1369     by (blast intro: int_sgnE elim: that)
  1370   then have "k * l = sgn (s * t) * int (n * m)"
  1371     by (simp add: ac_simps sgn_mult)
  1372   with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
  1373     by (simp only: divide_int_unfold)
  1374       (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
  1375 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
  1376 
  1377 end
  1378 
  1379 instantiation int :: unique_euclidean_ring
  1380 begin
  1381 
  1382 definition euclidean_size_int :: "int \<Rightarrow> nat"
  1383   where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
  1384 
  1385 definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
  1386   where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
  1387 
  1388 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1389   where "k mod l = (if l = 0 then k
  1390     else if sgn k = sgn l
  1391       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
  1392       else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
  1393 
  1394 lemma modulo_int_unfold:
  1395   "(sgn k * int m) mod (sgn l * int n) =
  1396    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
  1397     else if sgn k = sgn l
  1398       then sgn l * int (m mod n)
  1399       else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
  1400   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
  1401     nat_mult_distrib dvd_int_iff)
  1402 
  1403 lemma abs_mod_less:
  1404   "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
  1405 proof -
  1406   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
  1407     by (blast intro: int_sgnE elim: that)
  1408   with that show ?thesis
  1409     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
  1410       abs_mult mod_greater_zero_iff_not_dvd)
  1411 qed
  1412 
  1413 lemma sgn_mod:
  1414   "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
  1415 proof -
  1416   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
  1417     by (blast intro: int_sgnE elim: that)
  1418   with that show ?thesis
  1419     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
  1420       sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
  1421 qed
  1422 
  1423 instance proof
  1424   fix k l :: int
  1425   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
  1426     by (blast intro: int_sgnE elim: that)
  1427   then show "k div l * l + k mod l = k"
  1428     by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
  1429        (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
  1430          distrib_left [symmetric] minus_mult_right
  1431          del: of_nat_mult minus_mult_right [symmetric])
  1432 next
  1433   fix l q r :: int
  1434   obtain n m and s t
  1435      where l: "l = sgn s * int n" and q: "q = sgn t * int m"
  1436     by (blast intro: int_sgnE elim: that)
  1437   assume \<open>l \<noteq> 0\<close>
  1438   with l have "s \<noteq> 0" and "n > 0"
  1439     by (simp_all add: sgn_0_0)
  1440   assume "uniqueness_constraint r l"
  1441   moreover have "r = sgn r * \<bar>r\<bar>"
  1442     by (simp add: sgn_mult_abs)
  1443   moreover define u where "u = nat \<bar>r\<bar>"
  1444   ultimately have "r = sgn l * int u"
  1445     by simp
  1446   with l \<open>n > 0\<close> have r: "r = sgn s * int u"
  1447     by (simp add: sgn_mult)
  1448   assume "euclidean_size r < euclidean_size l"
  1449   with l r \<open>s \<noteq> 0\<close> have "u < n"
  1450     by (simp add: abs_mult)
  1451   show "(q * l + r) div l = q"
  1452   proof (cases "q = 0 \<or> r = 0")
  1453     case True
  1454     then show ?thesis
  1455     proof
  1456       assume "q = 0"
  1457       then show ?thesis
  1458         using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
  1459     next
  1460       assume "r = 0"
  1461       from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
  1462         using q l by (simp add: ac_simps sgn_mult)
  1463       from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
  1464         by (simp only: *, simp only: q l divide_int_unfold)
  1465           (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
  1466     qed
  1467   next
  1468     case False
  1469     with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
  1470       by (simp_all add: sgn_0_0)
  1471     moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
  1472       using mult_le_less_imp_less [of 1 m u n] by simp
  1473     ultimately have *: "q * l + r = sgn (s * t)
  1474       * int (if t < 0 then m * n - u else m * n + u)"
  1475       using l q r
  1476       by (simp add: sgn_mult algebra_simps of_nat_diff)
  1477     have "(m * n - u) div n = m - 1" if "u > 0"
  1478       using \<open>0 < m\<close> \<open>u < n\<close> that
  1479       by (auto intro: div_nat_eqI simp add: algebra_simps)
  1480     moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
  1481       using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
  1482       by auto
  1483     ultimately show ?thesis
  1484       using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
  1485       by (simp only: *, simp only: l q divide_int_unfold)
  1486         (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
  1487   qed
  1488 qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
  1489 
  1490 end
  1491 
  1492 lemma pos_mod_bound [simp]:
  1493   "k mod l < l" if "l > 0" for k l :: int
  1494 proof -
  1495   obtain m and s where "k = sgn s * int m"
  1496     by (blast intro: int_sgnE elim: that)
  1497   moreover from that obtain n where "l = sgn 1 * int n"
  1498     by (cases l) auto
  1499   ultimately show ?thesis
  1500     using that by (simp only: modulo_int_unfold)
  1501       (simp add: mod_greater_zero_iff_not_dvd)
  1502 qed
  1503 
  1504 lemma pos_mod_sign [simp]:
  1505   "0 \<le> k mod l" if "l > 0" for k l :: int
  1506 proof -
  1507   obtain m and s where "k = sgn s * int m"
  1508     by (blast intro: int_sgnE elim: that)
  1509   moreover from that obtain n where "l = sgn 1 * int n"
  1510     by (cases l) auto
  1511   ultimately show ?thesis
  1512     using that by (simp only: modulo_int_unfold) simp
  1513 qed
  1514 
  1515 
  1516 subsection \<open>Code generation\<close>
  1517 
  1518 code_identifier
  1519   code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1520 
  1521 end