src/HOL/Euclidean_Division.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (21 months ago)
changeset 66810 cc2b490f9dc4
parent 66808 1907167b6038
child 66813 351142796345
permissions -rw-r--r--
generalized simproc
     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" and "r \<noteq> 0"
   535       and "uniqueness_constraint r b"
   536       and "euclidean_size r < euclidean_size b"
   537       and "a div b = q"
   538       and "a mod b = r"
   539       and "a = q * b + r"
   540   | (by0) "b = 0"
   541 proof (cases "b = 0")
   542   case True
   543   then show thesis
   544   by (rule by0)
   545 next
   546   case False
   547   show thesis
   548   proof (cases "b dvd a")
   549     case True
   550     then obtain q where "a = b * q" ..
   551     with \<open>b \<noteq> 0\<close> divides
   552     show thesis
   553       by (simp add: ac_simps)
   554   next
   555     case False
   556     then have "a mod b \<noteq> 0"
   557       by (simp add: mod_eq_0_iff_dvd)
   558     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   559       by (rule uniqueness_constraint_mod)
   560     moreover have "euclidean_size (a mod b) < euclidean_size b"
   561       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   562     moreover have "a = a div b * b + a mod b"
   563       by (simp add: div_mult_mod_eq)
   564     ultimately show thesis
   565       using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   566   qed
   567 qed
   568 
   569 lemma div_eqI:
   570   "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   571     "euclidean_size r < euclidean_size b" "q * b + r = a"
   572 proof -
   573   from that have "(q * b + r) div b = q"
   574     by (auto intro: div_bounded)
   575   with that show ?thesis
   576     by simp
   577 qed
   578 
   579 lemma mod_eqI:
   580   "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   581     "euclidean_size r < euclidean_size b" "q * b + r = a" 
   582 proof -
   583   from that have "a div b = q"
   584     by (rule div_eqI)
   585   moreover have "a div b * b + a mod b = a"
   586     by (fact div_mult_mod_eq)
   587   ultimately have "a div b * b + a mod b = a div b * b + r"
   588     using \<open>q * b + r = a\<close> by simp
   589   then show ?thesis
   590     by simp
   591 qed
   592 
   593 subclass euclidean_semiring_cancel
   594 proof
   595   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   596   proof (cases a b rule: divmod_cases)
   597     case by0
   598     with \<open>b \<noteq> 0\<close> show ?thesis
   599       by simp
   600   next
   601     case (divides q)
   602     then show ?thesis
   603       by (simp add: ac_simps)
   604   next
   605     case (remainder q r)
   606     then show ?thesis
   607       by (auto intro: div_eqI simp add: algebra_simps)
   608   qed
   609 next
   610   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   611   proof (cases a b rule: divmod_cases)
   612     case by0
   613     then show ?thesis
   614       by simp
   615   next
   616     case (divides q)
   617     with \<open>c \<noteq> 0\<close> show ?thesis
   618       by (simp add: mult.left_commute [of c])
   619   next
   620     case (remainder q r)
   621     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   622       by simp
   623     from remainder \<open>c \<noteq> 0\<close>
   624     have "uniqueness_constraint (r * c) (b * c)"
   625       and "euclidean_size (r * c) < euclidean_size (b * c)"
   626       by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   627     with remainder show ?thesis
   628       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   629         (use \<open>b * c \<noteq> 0\<close> in simp)
   630   qed
   631 qed
   632 
   633 end
   634 
   635 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   636 begin
   637   
   638 subclass euclidean_ring_cancel ..
   639 
   640 end
   641 
   642 
   643 subsection \<open>Euclidean division on @{typ nat}\<close>
   644 
   645 instantiation nat :: unique_euclidean_semiring
   646 begin
   647 
   648 definition normalize_nat :: "nat \<Rightarrow> nat"
   649   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   650 
   651 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   652   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   653 
   654 lemma unit_factor_simps [simp]:
   655   "unit_factor 0 = (0::nat)"
   656   "unit_factor (Suc n) = 1"
   657   by (simp_all add: unit_factor_nat_def)
   658 
   659 definition euclidean_size_nat :: "nat \<Rightarrow> nat"
   660   where [simp]: "euclidean_size_nat = id"
   661 
   662 definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   663   where [simp]: "uniqueness_constraint_nat = \<top>"
   664 
   665 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   666   where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
   667 
   668 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   669   where "m mod n = m - (m div n * (n::nat))"
   670 
   671 instance proof
   672   fix m n :: nat
   673   have ex: "\<exists>k. k * n \<le> l" for l :: nat
   674     by (rule exI [of _ 0]) simp
   675   have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
   676   proof -
   677     from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
   678       by (cases n) auto
   679     then show ?thesis
   680       by (rule finite_subset) simp
   681   qed
   682   have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
   683   proof (cases "n = 0")
   684     case True
   685     moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
   686       by auto
   687     ultimately show ?thesis
   688       by simp
   689   next
   690     case False
   691     with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
   692       by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
   693     also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
   694       by (auto simp add: ac_simps elim!: dvdE)
   695     finally show ?thesis
   696       using False by (simp add: divide_nat_def ac_simps)
   697   qed
   698   show "n div 0 = 0"
   699     by (simp add: divide_nat_def)
   700   have less_eq: "m div n * n \<le> m"
   701     by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
   702   then show "m div n * n + m mod n = m"
   703     by (simp add: modulo_nat_def)
   704   assume "n \<noteq> 0" 
   705   show "m * n div n = m"
   706     using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
   707   show "euclidean_size (m mod n) < euclidean_size n"
   708   proof -
   709     have "m < Suc (m div n) * n"
   710     proof (rule ccontr)
   711       assume "\<not> m < Suc (m div n) * n"
   712       then have "Suc (m div n) * n \<le> m"
   713         by (simp add: not_less)
   714       moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
   715         by (simp add: divide_nat_def)
   716       with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
   717         by auto
   718       ultimately have "Suc (m div n) < Suc (m div n)"
   719         by blast
   720       then show False
   721         by simp
   722     qed
   723     with \<open>n \<noteq> 0\<close> show ?thesis
   724       by (simp add: modulo_nat_def)
   725   qed
   726   show "euclidean_size m \<le> euclidean_size (m * n)"
   727     using \<open>n \<noteq> 0\<close> by (cases n) simp_all
   728   fix q r :: nat
   729   show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
   730   proof -
   731     from that have "r < n"
   732       by simp
   733     have "k \<le> q" if "k * n \<le> q * n + r" for k
   734     proof (rule ccontr)
   735       assume "\<not> k \<le> q"
   736       then have "q < k"
   737         by simp
   738       then obtain l where "k = Suc (q + l)"
   739         by (auto simp add: less_iff_Suc_add)
   740       with \<open>r < n\<close> that show False
   741         by (simp add: algebra_simps)
   742     qed
   743     with \<open>n \<noteq> 0\<close> ex fin show ?thesis
   744       by (auto simp add: divide_nat_def Max_eq_iff)
   745   qed
   746 qed (simp_all add: unit_factor_nat_def)
   747 
   748 end
   749 
   750 text \<open>Tool support\<close>
   751 
   752 ML \<open>
   753 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   754 (
   755   val div_name = @{const_name divide};
   756   val mod_name = @{const_name modulo};
   757   val mk_binop = HOLogic.mk_binop;
   758   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   759   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   760   fun mk_sum' [] = HOLogic.zero
   761     | mk_sum' [t] = t
   762     | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
   763   fun mk_sum _ = mk_sum';
   764   fun dest_sum tm =
   765     if HOLogic.is_zero tm then []
   766     else
   767       (case try HOLogic.dest_Suc tm of
   768         SOME t => HOLogic.Suc_zero :: dest_sum t
   769       | NONE =>
   770           (case try dest_plus tm of
   771             SOME (t, u) => dest_sum t @ dest_sum u
   772           | NONE => [tm]));
   773 
   774   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   775 
   776   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   777     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   778 )
   779 \<close>
   780 
   781 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   782   \<open>K Cancel_Div_Mod_Nat.proc\<close>
   783 
   784 lemma div_nat_eqI:
   785   "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
   786   by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   787 
   788 lemma mod_nat_eqI:
   789   "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
   790   by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   791 
   792 lemma div_mult_self_is_m [simp]:
   793   "m * n div n = m" if "n > 0" for m n :: nat
   794   using that by simp
   795 
   796 lemma div_mult_self1_is_m [simp]:
   797   "n * m div n = m" if "n > 0" for m n :: nat
   798   using that by simp
   799 
   800 lemma mod_less_divisor [simp]:
   801   "m mod n < n" if "n > 0" for m n :: nat
   802   using mod_size_less [of n m] that by simp
   803 
   804 lemma mod_le_divisor [simp]:
   805   "m mod n \<le> n" if "n > 0" for m n :: nat
   806   using that by (auto simp add: le_less)
   807 
   808 lemma div_times_less_eq_dividend [simp]:
   809   "m div n * n \<le> m" for m n :: nat
   810   by (simp add: minus_mod_eq_div_mult [symmetric])
   811 
   812 lemma times_div_less_eq_dividend [simp]:
   813   "n * (m div n) \<le> m" for m n :: nat
   814   using div_times_less_eq_dividend [of m n]
   815   by (simp add: ac_simps)
   816 
   817 lemma dividend_less_div_times:
   818   "m < n + (m div n) * n" if "0 < n" for m n :: nat
   819 proof -
   820   from that have "m mod n < n"
   821     by simp
   822   then show ?thesis
   823     by (simp add: minus_mod_eq_div_mult [symmetric])
   824 qed
   825 
   826 lemma dividend_less_times_div:
   827   "m < n + n * (m div n)" if "0 < n" for m n :: nat
   828   using dividend_less_div_times [of n m] that
   829   by (simp add: ac_simps)
   830 
   831 lemma mod_Suc_le_divisor [simp]:
   832   "m mod Suc n \<le> n"
   833   using mod_less_divisor [of "Suc n" m] by arith
   834 
   835 lemma mod_less_eq_dividend [simp]:
   836   "m mod n \<le> m" for m n :: nat
   837 proof (rule add_leD2)
   838   from div_mult_mod_eq have "m div n * n + m mod n = m" .
   839   then show "m div n * n + m mod n \<le> m" by auto
   840 qed
   841 
   842 lemma
   843   div_less [simp]: "m div n = 0"
   844   and mod_less [simp]: "m mod n = m"
   845   if "m < n" for m n :: nat
   846   using that by (auto intro: div_eqI mod_eqI) 
   847 
   848 lemma le_div_geq:
   849   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
   850 proof -
   851   from \<open>n \<le> m\<close> obtain q where "m = n + q"
   852     by (auto simp add: le_iff_add)
   853   with \<open>0 < n\<close> show ?thesis
   854     by (simp add: div_add_self1)
   855 qed
   856 
   857 lemma le_mod_geq:
   858   "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
   859 proof -
   860   from \<open>n \<le> m\<close> obtain q where "m = n + q"
   861     by (auto simp add: le_iff_add)
   862   then show ?thesis
   863     by simp
   864 qed
   865 
   866 lemma div_if:
   867   "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
   868   by (simp add: le_div_geq)
   869 
   870 lemma mod_if:
   871   "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
   872   by (simp add: le_mod_geq)
   873 
   874 lemma div_eq_0_iff:
   875   "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
   876   by (simp add: div_if)
   877 
   878 lemma div_greater_zero_iff:
   879   "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
   880   using div_eq_0_iff [of m n] by auto
   881 
   882 lemma mod_greater_zero_iff_not_dvd:
   883   "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
   884   by (simp add: dvd_eq_mod_eq_0)
   885 
   886 lemma div_by_Suc_0 [simp]:
   887   "m div Suc 0 = m"
   888   using div_by_1 [of m] by simp
   889 
   890 lemma mod_by_Suc_0 [simp]:
   891   "m mod Suc 0 = 0"
   892   using mod_by_1 [of m] by simp
   893 
   894 lemma div2_Suc_Suc [simp]:
   895   "Suc (Suc m) div 2 = Suc (m div 2)"
   896   by (simp add: numeral_2_eq_2 le_div_geq)
   897 
   898 lemma Suc_n_div_2_gt_zero [simp]:
   899   "0 < Suc n div 2" if "n > 0" for n :: nat
   900   using that by (cases n) simp_all
   901 
   902 lemma div_2_gt_zero [simp]:
   903   "0 < n div 2" if "Suc 0 < n" for n :: nat
   904   using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
   905 
   906 lemma mod2_Suc_Suc [simp]:
   907   "Suc (Suc m) mod 2 = m mod 2"
   908   by (simp add: numeral_2_eq_2 le_mod_geq)
   909 
   910 lemma add_self_div_2 [simp]:
   911   "(m + m) div 2 = m" for m :: nat
   912   by (simp add: mult_2 [symmetric])
   913 
   914 lemma add_self_mod_2 [simp]:
   915   "(m + m) mod 2 = 0" for m :: nat
   916   by (simp add: mult_2 [symmetric])
   917 
   918 lemma mod2_gr_0 [simp]:
   919   "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
   920 proof -
   921   have "m mod 2 < 2"
   922     by (rule mod_less_divisor) simp
   923   then have "m mod 2 = 0 \<or> m mod 2 = 1"
   924     by arith
   925   then show ?thesis
   926     by auto     
   927 qed
   928 
   929 lemma mod_Suc_eq [mod_simps]:
   930   "Suc (m mod n) mod n = Suc m mod n"
   931 proof -
   932   have "(m mod n + 1) mod n = (m + 1) mod n"
   933     by (simp only: mod_simps)
   934   then show ?thesis
   935     by simp
   936 qed
   937 
   938 lemma mod_Suc_Suc_eq [mod_simps]:
   939   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   940 proof -
   941   have "(m mod n + 2) mod n = (m + 2) mod n"
   942     by (simp only: mod_simps)
   943   then show ?thesis
   944     by simp
   945 qed
   946 
   947 lemma
   948   Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
   949   and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
   950   and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   951   and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
   952   by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
   953 
   954 lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
   955   "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
   956   apply (cases "c = 0")
   957    apply simp
   958   apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
   959      apply (auto simp add: algebra_simps distrib_left [symmetric])
   960   done
   961 
   962 lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
   963    -- \<open>TODO: Generalization candidate\<close>
   964   "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
   965   apply (cases "c = 0")
   966    apply simp
   967   apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
   968   apply (auto simp add: algebra_simps)
   969   done
   970 
   971 context
   972   fixes m n q :: nat
   973 begin
   974 
   975 private lemma eucl_rel_mult2:
   976   "m mod n + n * (m div n mod q) < n * q"
   977   if "n > 0" and "q > 0"
   978 proof -
   979   from \<open>n > 0\<close> have "m mod n < n"
   980     by (rule mod_less_divisor)
   981   from \<open>q > 0\<close> have "m div n mod q < q"
   982     by (rule mod_less_divisor)
   983   then obtain s where "q = Suc (m div n mod q + s)"
   984     by (blast dest: less_imp_Suc_add)
   985   moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
   986     using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
   987   ultimately show ?thesis
   988     by simp
   989 qed
   990 
   991 lemma div_mult2_eq:
   992   "m div (n * q) = (m div n) div q"
   993 proof (cases "n = 0 \<or> q = 0")
   994   case True
   995   then show ?thesis
   996     by auto
   997 next
   998   case False
   999   with eucl_rel_mult2 show ?thesis
  1000     by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
  1001       simp add: algebra_simps add_mult_distrib2 [symmetric])
  1002 qed
  1003 
  1004 lemma mod_mult2_eq:
  1005   "m mod (n * q) = n * (m div n mod q) + m mod n"
  1006 proof (cases "n = 0 \<or> q = 0")
  1007   case True
  1008   then show ?thesis
  1009     by auto
  1010 next
  1011   case False
  1012   with eucl_rel_mult2 show ?thesis
  1013     by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
  1014       simp add: algebra_simps add_mult_distrib2 [symmetric])
  1015 qed
  1016 
  1017 end
  1018 
  1019 lemma div_le_mono:
  1020   "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
  1021 proof -
  1022   from that obtain q where "n = m + q"
  1023     by (auto simp add: le_iff_add)
  1024   then show ?thesis
  1025     by (simp add: div_add1_eq [of m q k])
  1026 qed
  1027 
  1028 text \<open>Antimonotonicity of @{const divide} in second argument\<close>
  1029 
  1030 lemma div_le_mono2:
  1031   "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
  1032 using that proof (induct k arbitrary: m rule: less_induct)
  1033   case (less k)
  1034   show ?case
  1035   proof (cases "n \<le> k")
  1036     case False
  1037     then show ?thesis
  1038       by simp
  1039   next
  1040     case True
  1041     have "(k - n) div n \<le> (k - m) div n"
  1042       using less.prems
  1043       by (blast intro: div_le_mono diff_le_mono2)
  1044     also have "\<dots> \<le> (k - m) div m"
  1045       using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
  1046       by simp
  1047     finally show ?thesis
  1048       using \<open>n \<le> k\<close> less.prems
  1049       by (simp add: le_div_geq)
  1050   qed
  1051 qed
  1052 
  1053 lemma div_le_dividend [simp]:
  1054   "m div n \<le> m" for m n :: nat
  1055   using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
  1056 
  1057 lemma div_less_dividend [simp]:
  1058   "m div n < m" if "1 < n" and "0 < m" for m n :: nat
  1059 using that proof (induct m rule: less_induct)
  1060   case (less m)
  1061   show ?case
  1062   proof (cases "n < m")
  1063     case False
  1064     with less show ?thesis
  1065       by (cases "n = m") simp_all
  1066   next
  1067     case True
  1068     then show ?thesis
  1069       using less.hyps [of "m - n"] less.prems
  1070       by (simp add: le_div_geq)
  1071   qed
  1072 qed
  1073 
  1074 lemma div_eq_dividend_iff:
  1075   "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
  1076 proof
  1077   assume "n = 1"
  1078   then show "m div n = m"
  1079     by simp
  1080 next
  1081   assume P: "m div n = m"
  1082   show "n = 1"
  1083   proof (rule ccontr)
  1084     have "n \<noteq> 0"
  1085       by (rule ccontr) (use that P in auto)
  1086     moreover assume "n \<noteq> 1"
  1087     ultimately have "n > 1"
  1088       by simp
  1089     with that have "m div n < m"
  1090       by simp
  1091     with P show False
  1092       by simp
  1093   qed
  1094 qed
  1095 
  1096 lemma less_mult_imp_div_less:
  1097   "m div n < i" if "m < i * n" for m n i :: nat
  1098 proof -
  1099   from that have "i * n > 0"
  1100     by (cases "i * n = 0") simp_all
  1101   then have "i > 0" and "n > 0"
  1102     by simp_all
  1103   have "m div n * n \<le> m"
  1104     by simp
  1105   then have "m div n * n < i * n"
  1106     using that by (rule le_less_trans)
  1107   with \<open>n > 0\<close> show ?thesis
  1108     by simp
  1109 qed
  1110 
  1111 text \<open>A fact for the mutilated chess board\<close>
  1112 
  1113 lemma mod_Suc:
  1114   "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
  1115 proof (cases "n = 0")
  1116   case True
  1117   then show ?thesis
  1118     by simp
  1119 next
  1120   case False
  1121   have "Suc m mod n = Suc (m mod n) mod n"
  1122     by (simp add: mod_simps)
  1123   also have "\<dots> = ?rhs"
  1124     using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
  1125   finally show ?thesis .
  1126 qed
  1127 
  1128 lemma Suc_times_mod_eq:
  1129   "Suc (m * n) mod m = 1" if "Suc 0 < m"
  1130   using that by (simp add: mod_Suc)
  1131 
  1132 lemma Suc_times_numeral_mod_eq [simp]:
  1133   "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
  1134   by (rule Suc_times_mod_eq) (use that in simp)
  1135 
  1136 lemma Suc_div_le_mono [simp]:
  1137   "m div n \<le> Suc m div n"
  1138   by (simp add: div_le_mono)
  1139 
  1140 text \<open>These lemmas collapse some needless occurrences of Suc:
  1141   at least three Sucs, since two and fewer are rewritten back to Suc again!
  1142   We already have some rules to simplify operands smaller than 3.\<close>
  1143 
  1144 lemma div_Suc_eq_div_add3 [simp]:
  1145   "m div Suc (Suc (Suc n)) = m div (3 + n)"
  1146   by (simp add: Suc3_eq_add_3)
  1147 
  1148 lemma mod_Suc_eq_mod_add3 [simp]:
  1149   "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
  1150   by (simp add: Suc3_eq_add_3)
  1151 
  1152 lemma Suc_div_eq_add3_div:
  1153   "Suc (Suc (Suc m)) div n = (3 + m) div n"
  1154   by (simp add: Suc3_eq_add_3)
  1155 
  1156 lemma Suc_mod_eq_add3_mod:
  1157   "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
  1158   by (simp add: Suc3_eq_add_3)
  1159 
  1160 lemmas Suc_div_eq_add3_div_numeral [simp] =
  1161   Suc_div_eq_add3_div [of _ "numeral v"] for v
  1162 
  1163 lemmas Suc_mod_eq_add3_mod_numeral [simp] =
  1164   Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1165 
  1166 lemma (in field_char_0) of_nat_div:
  1167   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
  1168 proof -
  1169   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
  1170     unfolding of_nat_add by (cases "n = 0") simp_all
  1171   then show ?thesis
  1172     by simp
  1173 qed
  1174 
  1175 text \<open>An ``induction'' law for modulus arithmetic.\<close>
  1176 
  1177 lemma mod_induct [consumes 3, case_names step]:
  1178   "P m" if "P n" and "n < p" and "m < p"
  1179     and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
  1180 using \<open>m < p\<close> proof (induct m)
  1181   case 0
  1182   show ?case
  1183   proof (rule ccontr)
  1184     assume "\<not> P 0"
  1185     from \<open>n < p\<close> have "0 < p"
  1186       by simp
  1187     from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
  1188       by (blast dest: less_imp_add_positive)
  1189     with \<open>P n\<close> have "P (p - m)"
  1190       by simp
  1191     moreover have "\<not> P (p - m)"
  1192     using \<open>0 < m\<close> proof (induct m)
  1193       case 0
  1194       then show ?case
  1195         by simp
  1196     next
  1197       case (Suc m)
  1198       show ?case
  1199       proof
  1200         assume P: "P (p - Suc m)"
  1201         with \<open>\<not> P 0\<close> have "Suc m < p"
  1202           by (auto intro: ccontr) 
  1203         then have "Suc (p - Suc m) = p - m"
  1204           by arith
  1205         moreover from \<open>0 < p\<close> have "p - Suc m < p"
  1206           by arith
  1207         with P step have "P ((Suc (p - Suc m)) mod p)"
  1208           by blast
  1209         ultimately show False
  1210           using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
  1211       qed
  1212     qed
  1213     ultimately show False
  1214       by blast
  1215   qed
  1216 next
  1217   case (Suc m)
  1218   then have "m < p" and mod: "Suc m mod p = Suc m"
  1219     by simp_all
  1220   from \<open>m < p\<close> have "P m"
  1221     by (rule Suc.hyps)
  1222   with \<open>m < p\<close> have "P (Suc m mod p)"
  1223     by (rule step)
  1224   with mod show ?case
  1225     by simp
  1226 qed
  1227 
  1228 lemma split_div:
  1229   "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
  1230      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
  1231      (is "?P = ?Q") for m n :: nat
  1232 proof (cases "n = 0")
  1233   case True
  1234   then show ?thesis
  1235     by simp
  1236 next
  1237   case False
  1238   show ?thesis
  1239   proof
  1240     assume ?P
  1241     with False show ?Q
  1242       by auto
  1243   next
  1244     assume ?Q
  1245     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
  1246       by simp
  1247     with False show ?P
  1248       by (auto intro: * [of "m mod n"])
  1249   qed
  1250 qed
  1251 
  1252 lemma split_div':
  1253   "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)"
  1254 proof (cases "n = 0")
  1255   case True
  1256   then show ?thesis
  1257     by simp
  1258 next
  1259   case False
  1260   then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
  1261     by (auto intro: div_nat_eqI dividend_less_times_div)
  1262   then show ?thesis
  1263     by auto
  1264 qed
  1265 
  1266 lemma split_mod:
  1267   "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
  1268      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
  1269      (is "?P \<longleftrightarrow> ?Q") for m n :: nat
  1270 proof (cases "n = 0")
  1271   case True
  1272   then show ?thesis
  1273     by simp
  1274 next
  1275   case False
  1276   show ?thesis
  1277   proof
  1278     assume ?P
  1279     with False show ?Q
  1280       by auto
  1281   next
  1282     assume ?Q
  1283     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
  1284       by simp
  1285     with False show ?P
  1286       by (auto intro: * [of _ "m div n"])
  1287   qed
  1288 qed
  1289 
  1290 
  1291 subsection \<open>Code generation\<close>
  1292 
  1293 code_identifier
  1294   code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1295 
  1296 end