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