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