src/HOL/Euclidean_Division.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (21 months ago)
changeset 66806 a4e82b58d833
parent 66798 39bb2462e681
child 66807 c3631f32dfeb
permissions -rw-r--r--
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
     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
    10 begin
    11 
    12 subsection \<open>Quotient and remainder in integral domains\<close>
    13 
    14 class semidom_modulo = algebraic_semidom + semiring_modulo
    15 begin
    16 
    17 lemma mod_0 [simp]: "0 mod a = 0"
    18   using div_mult_mod_eq [of 0 a] by simp
    19 
    20 lemma mod_by_0 [simp]: "a mod 0 = a"
    21   using div_mult_mod_eq [of a 0] by simp
    22 
    23 lemma mod_by_1 [simp]:
    24   "a mod 1 = 0"
    25 proof -
    26   from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    27   then have "a + a mod 1 = a + 0" by simp
    28   then show ?thesis by (rule add_left_imp_eq)
    29 qed
    30 
    31 lemma mod_self [simp]:
    32   "a mod a = 0"
    33   using div_mult_mod_eq [of a a] by simp
    34 
    35 lemma dvd_imp_mod_0 [simp]:
    36   assumes "a dvd b"
    37   shows "b mod a = 0"
    38   using assms minus_div_mult_eq_mod [of b a] by simp
    39 
    40 lemma mod_0_imp_dvd: 
    41   assumes "a mod b = 0"
    42   shows   "b dvd a"
    43 proof -
    44   have "b dvd ((a div b) * b)" by simp
    45   also have "(a div b) * b = a"
    46     using div_mult_mod_eq [of a b] by (simp add: assms)
    47   finally show ?thesis .
    48 qed
    49 
    50 lemma mod_eq_0_iff_dvd:
    51   "a mod b = 0 \<longleftrightarrow> b dvd a"
    52   by (auto intro: mod_0_imp_dvd)
    53 
    54 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    55   "a dvd b \<longleftrightarrow> b mod a = 0"
    56   by (simp add: mod_eq_0_iff_dvd)
    57 
    58 lemma dvd_mod_iff: 
    59   assumes "c dvd b"
    60   shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    61 proof -
    62   from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    63     by (simp add: dvd_add_right_iff)
    64   also have "(a div b) * b + a mod b = a"
    65     using div_mult_mod_eq [of a b] by simp
    66   finally show ?thesis .
    67 qed
    68 
    69 lemma dvd_mod_imp_dvd:
    70   assumes "c dvd a mod b" and "c dvd b"
    71   shows "c dvd a"
    72   using assms dvd_mod_iff [of c b a] by simp
    73 
    74 end
    75 
    76 class idom_modulo = idom + semidom_modulo
    77 begin
    78 
    79 subclass idom_divide ..
    80 
    81 lemma div_diff [simp]:
    82   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    83   using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    84 
    85 end
    86 
    87   
    88 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    89   
    90 class euclidean_semiring = semidom_modulo + normalization_semidom + 
    91   fixes euclidean_size :: "'a \<Rightarrow> nat"
    92   assumes size_0 [simp]: "euclidean_size 0 = 0"
    93   assumes mod_size_less: 
    94     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    95   assumes size_mult_mono:
    96     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    97 begin
    98 
    99 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   100   by (subst mult.commute) (rule size_mult_mono)
   101 
   102 lemma euclidean_size_normalize [simp]:
   103   "euclidean_size (normalize a) = euclidean_size a"
   104 proof (cases "a = 0")
   105   case True
   106   then show ?thesis
   107     by simp
   108 next
   109   case [simp]: False
   110   have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
   111     by (rule size_mult_mono) simp
   112   moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
   113     by (rule size_mult_mono) simp
   114   ultimately show ?thesis
   115     by simp
   116 qed
   117 
   118 lemma dvd_euclidean_size_eq_imp_dvd:
   119   assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
   120     and "b dvd a" 
   121   shows "a dvd b"
   122 proof (rule ccontr)
   123   assume "\<not> a dvd b"
   124   hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
   125   then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   126   from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
   127   then obtain c where "b mod a = b * c" unfolding dvd_def by blast
   128     with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   129   with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
   130     using size_mult_mono by force
   131   moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
   132   have "euclidean_size (b mod a) < euclidean_size a"
   133     using mod_size_less by blast
   134   ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
   135     by simp
   136 qed
   137 
   138 lemma euclidean_size_times_unit:
   139   assumes "is_unit a"
   140   shows   "euclidean_size (a * b) = euclidean_size b"
   141 proof (rule antisym)
   142   from assms have [simp]: "a \<noteq> 0" by auto
   143   thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
   144   from assms have "is_unit (1 div a)" by simp
   145   hence "1 div a \<noteq> 0" by (intro notI) simp_all
   146   hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
   147     by (rule size_mult_mono')
   148   also from assms have "(1 div a) * (a * b) = b"
   149     by (simp add: algebra_simps unit_div_mult_swap)
   150   finally show "euclidean_size (a * b) \<le> euclidean_size b" .
   151 qed
   152 
   153 lemma euclidean_size_unit:
   154   "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
   155   using euclidean_size_times_unit [of a 1] by simp
   156 
   157 lemma unit_iff_euclidean_size: 
   158   "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
   159 proof safe
   160   assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
   161   show "is_unit a"
   162     by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
   163 qed (auto intro: euclidean_size_unit)
   164 
   165 lemma euclidean_size_times_nonunit:
   166   assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
   167   shows   "euclidean_size b < euclidean_size (a * b)"
   168 proof (rule ccontr)
   169   assume "\<not>euclidean_size b < euclidean_size (a * b)"
   170   with size_mult_mono'[OF assms(1), of b] 
   171     have eq: "euclidean_size (a * b) = euclidean_size b" by simp
   172   have "a * b dvd b"
   173     by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
   174   hence "a * b dvd 1 * b" by simp
   175   with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   176   with assms(3) show False by contradiction
   177 qed
   178 
   179 lemma dvd_imp_size_le:
   180   assumes "a dvd b" "b \<noteq> 0" 
   181   shows   "euclidean_size a \<le> euclidean_size b"
   182   using assms by (auto elim!: dvdE simp: size_mult_mono)
   183 
   184 lemma dvd_proper_imp_size_less:
   185   assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   186   shows   "euclidean_size a < euclidean_size b"
   187 proof -
   188   from assms(1) obtain c where "b = a * c" by (erule dvdE)
   189   hence z: "b = c * a" by (simp add: mult.commute)
   190   from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   191   with z assms show ?thesis
   192     by (auto intro!: euclidean_size_times_nonunit)
   193 qed
   194 
   195 lemma unit_imp_mod_eq_0:
   196   "a mod b = 0" if "is_unit b"
   197   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
   198 
   199 end
   200 
   201 class euclidean_ring = idom_modulo + euclidean_semiring
   202 
   203   
   204 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
   205 
   206 class euclidean_semiring_cancel = euclidean_semiring +
   207   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
   208   and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
   209 begin
   210 
   211 lemma div_mult_self2 [simp]:
   212   assumes "b \<noteq> 0"
   213   shows "(a + b * c) div b = c + a div b"
   214   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
   215 
   216 lemma div_mult_self3 [simp]:
   217   assumes "b \<noteq> 0"
   218   shows "(c * b + a) div b = c + a div b"
   219   using assms by (simp add: add.commute)
   220 
   221 lemma div_mult_self4 [simp]:
   222   assumes "b \<noteq> 0"
   223   shows "(b * c + a) div b = c + a div b"
   224   using assms by (simp add: add.commute)
   225 
   226 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
   227 proof (cases "b = 0")
   228   case True then show ?thesis by simp
   229 next
   230   case False
   231   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
   232     by (simp add: div_mult_mod_eq)
   233   also from False div_mult_self1 [of b a c] have
   234     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
   235       by (simp add: algebra_simps)
   236   finally have "a = a div b * b + (a + c * b) mod b"
   237     by (simp add: add.commute [of a] add.assoc distrib_right)
   238   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   239     by (simp add: div_mult_mod_eq)
   240   then show ?thesis by simp
   241 qed
   242 
   243 lemma mod_mult_self2 [simp]:
   244   "(a + b * c) mod b = a mod b"
   245   by (simp add: mult.commute [of b])
   246 
   247 lemma mod_mult_self3 [simp]:
   248   "(c * b + a) mod b = a mod b"
   249   by (simp add: add.commute)
   250 
   251 lemma mod_mult_self4 [simp]:
   252   "(b * c + a) mod b = a mod b"
   253   by (simp add: add.commute)
   254 
   255 lemma mod_mult_self1_is_0 [simp]:
   256   "b * a mod b = 0"
   257   using mod_mult_self2 [of 0 b a] by simp
   258 
   259 lemma mod_mult_self2_is_0 [simp]:
   260   "a * b mod b = 0"
   261   using mod_mult_self1 [of 0 a b] by simp
   262 
   263 lemma div_add_self1:
   264   assumes "b \<noteq> 0"
   265   shows "(b + a) div b = a div b + 1"
   266   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
   267 
   268 lemma div_add_self2:
   269   assumes "b \<noteq> 0"
   270   shows "(a + b) div b = a div b + 1"
   271   using assms div_add_self1 [of b a] by (simp add: add.commute)
   272 
   273 lemma mod_add_self1 [simp]:
   274   "(b + a) mod b = a mod b"
   275   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
   276 
   277 lemma mod_add_self2 [simp]:
   278   "(a + b) mod b = a mod b"
   279   using mod_mult_self1 [of a 1 b] by simp
   280 
   281 lemma mod_div_trivial [simp]:
   282   "a mod b div b = 0"
   283 proof (cases "b = 0")
   284   assume "b = 0"
   285   thus ?thesis by simp
   286 next
   287   assume "b \<noteq> 0"
   288   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
   289     by (rule div_mult_self1 [symmetric])
   290   also have "\<dots> = a div b"
   291     by (simp only: mod_div_mult_eq)
   292   also have "\<dots> = a div b + 0"
   293     by simp
   294   finally show ?thesis
   295     by (rule add_left_imp_eq)
   296 qed
   297 
   298 lemma mod_mod_trivial [simp]:
   299   "a mod b mod b = a mod b"
   300 proof -
   301   have "a mod b mod b = (a mod b + a div b * b) mod b"
   302     by (simp only: mod_mult_self1)
   303   also have "\<dots> = a mod b"
   304     by (simp only: mod_div_mult_eq)
   305   finally show ?thesis .
   306 qed
   307 
   308 lemma mod_mod_cancel:
   309   assumes "c dvd b"
   310   shows "a mod b mod c = a mod c"
   311 proof -
   312   from \<open>c dvd b\<close> obtain k where "b = c * k"
   313     by (rule dvdE)
   314   have "a mod b mod c = a mod (c * k) mod c"
   315     by (simp only: \<open>b = c * k\<close>)
   316   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   317     by (simp only: mod_mult_self1)
   318   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   319     by (simp only: ac_simps)
   320   also have "\<dots> = a mod c"
   321     by (simp only: div_mult_mod_eq)
   322   finally show ?thesis .
   323 qed
   324 
   325 lemma div_mult_mult2 [simp]:
   326   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   327   by (drule div_mult_mult1) (simp add: mult.commute)
   328 
   329 lemma div_mult_mult1_if [simp]:
   330   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   331   by simp_all
   332 
   333 lemma mod_mult_mult1:
   334   "(c * a) mod (c * b) = c * (a mod b)"
   335 proof (cases "c = 0")
   336   case True then show ?thesis by simp
   337 next
   338   case False
   339   from div_mult_mod_eq
   340   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   341   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   342     = c * a + c * (a mod b)" by (simp add: algebra_simps)
   343   with div_mult_mod_eq show ?thesis by simp
   344 qed
   345 
   346 lemma mod_mult_mult2:
   347   "(a * c) mod (b * c) = (a mod b) * c"
   348   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   349 
   350 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   351   by (fact mod_mult_mult2 [symmetric])
   352 
   353 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   354   by (fact mod_mult_mult1 [symmetric])
   355 
   356 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   357   unfolding dvd_def by (auto simp add: mod_mult_mult1)
   358 
   359 lemma div_plus_div_distrib_dvd_left:
   360   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   361   by (cases "c = 0") (auto elim: dvdE)
   362 
   363 lemma div_plus_div_distrib_dvd_right:
   364   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   365   using div_plus_div_distrib_dvd_left [of c b a]
   366   by (simp add: ac_simps)
   367 
   368 named_theorems mod_simps
   369 
   370 text \<open>Addition respects modular equivalence.\<close>
   371 
   372 lemma mod_add_left_eq [mod_simps]:
   373   "(a mod c + b) mod c = (a + b) mod c"
   374 proof -
   375   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   376     by (simp only: div_mult_mod_eq)
   377   also have "\<dots> = (a mod c + b + a div c * c) mod c"
   378     by (simp only: ac_simps)
   379   also have "\<dots> = (a mod c + b) mod c"
   380     by (rule mod_mult_self1)
   381   finally show ?thesis
   382     by (rule sym)
   383 qed
   384 
   385 lemma mod_add_right_eq [mod_simps]:
   386   "(a + b mod c) mod c = (a + b) mod c"
   387   using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   388 
   389 lemma mod_add_eq:
   390   "(a mod c + b mod c) mod c = (a + b) mod c"
   391   by (simp add: mod_add_left_eq mod_add_right_eq)
   392 
   393 lemma mod_sum_eq [mod_simps]:
   394   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   395 proof (induct A rule: infinite_finite_induct)
   396   case (insert i A)
   397   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   398     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   399     by simp
   400   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   401     by (simp add: mod_simps)
   402   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   403     by (simp add: insert.hyps)
   404   finally show ?case
   405     by (simp add: insert.hyps mod_simps)
   406 qed simp_all
   407 
   408 lemma mod_add_cong:
   409   assumes "a mod c = a' mod c"
   410   assumes "b mod c = b' mod c"
   411   shows "(a + b) mod c = (a' + b') mod c"
   412 proof -
   413   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   414     unfolding assms ..
   415   then show ?thesis
   416     by (simp add: mod_add_eq)
   417 qed
   418 
   419 text \<open>Multiplication respects modular equivalence.\<close>
   420 
   421 lemma mod_mult_left_eq [mod_simps]:
   422   "((a mod c) * b) mod c = (a * b) mod c"
   423 proof -
   424   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   425     by (simp only: div_mult_mod_eq)
   426   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   427     by (simp only: algebra_simps)
   428   also have "\<dots> = (a mod c * b) mod c"
   429     by (rule mod_mult_self1)
   430   finally show ?thesis
   431     by (rule sym)
   432 qed
   433 
   434 lemma mod_mult_right_eq [mod_simps]:
   435   "(a * (b mod c)) mod c = (a * b) mod c"
   436   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   437 
   438 lemma mod_mult_eq:
   439   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   440   by (simp add: mod_mult_left_eq mod_mult_right_eq)
   441 
   442 lemma mod_prod_eq [mod_simps]:
   443   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   444 proof (induct A rule: infinite_finite_induct)
   445   case (insert i A)
   446   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   447     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   448     by simp
   449   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   450     by (simp add: mod_simps)
   451   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   452     by (simp add: insert.hyps)
   453   finally show ?case
   454     by (simp add: insert.hyps mod_simps)
   455 qed simp_all
   456 
   457 lemma mod_mult_cong:
   458   assumes "a mod c = a' mod c"
   459   assumes "b mod c = b' mod c"
   460   shows "(a * b) mod c = (a' * b') mod c"
   461 proof -
   462   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   463     unfolding assms ..
   464   then show ?thesis
   465     by (simp add: mod_mult_eq)
   466 qed
   467 
   468 text \<open>Exponentiation respects modular equivalence.\<close>
   469 
   470 lemma power_mod [mod_simps]: 
   471   "((a mod b) ^ n) mod b = (a ^ n) mod b"
   472 proof (induct n)
   473   case 0
   474   then show ?case by simp
   475 next
   476   case (Suc n)
   477   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   478     by (simp add: mod_mult_right_eq)
   479   with Suc show ?case
   480     by (simp add: mod_mult_left_eq mod_mult_right_eq)
   481 qed
   482 
   483 end
   484 
   485 
   486 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
   487 begin
   488 
   489 subclass idom_divide ..
   490 
   491 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   492   using div_mult_mult1 [of "- 1" a b] by simp
   493 
   494 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   495   using mod_mult_mult1 [of "- 1" a b] by simp
   496 
   497 lemma div_minus_right: "a div (- b) = (- a) div b"
   498   using div_minus_minus [of "- a" b] by simp
   499 
   500 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   501   using mod_minus_minus [of "- a" b] by simp
   502 
   503 lemma div_minus1_right [simp]: "a div (- 1) = - a"
   504   using div_minus_right [of a 1] by simp
   505 
   506 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   507   using mod_minus_right [of a 1] by simp
   508 
   509 text \<open>Negation respects modular equivalence.\<close>
   510 
   511 lemma mod_minus_eq [mod_simps]:
   512   "(- (a mod b)) mod b = (- a) mod b"
   513 proof -
   514   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   515     by (simp only: div_mult_mod_eq)
   516   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   517     by (simp add: ac_simps)
   518   also have "\<dots> = (- (a mod b)) mod b"
   519     by (rule mod_mult_self1)
   520   finally show ?thesis
   521     by (rule sym)
   522 qed
   523 
   524 lemma mod_minus_cong:
   525   assumes "a mod b = a' mod b"
   526   shows "(- a) mod b = (- a') mod b"
   527 proof -
   528   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   529     unfolding assms ..
   530   then show ?thesis
   531     by (simp add: mod_minus_eq)
   532 qed
   533 
   534 text \<open>Subtraction respects modular equivalence.\<close>
   535 
   536 lemma mod_diff_left_eq [mod_simps]:
   537   "(a mod c - b) mod c = (a - b) mod c"
   538   using mod_add_cong [of a c "a mod c" "- b" "- b"]
   539   by simp
   540 
   541 lemma mod_diff_right_eq [mod_simps]:
   542   "(a - b mod c) mod c = (a - b) mod c"
   543   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   544   by simp
   545 
   546 lemma mod_diff_eq:
   547   "(a mod c - b mod c) mod c = (a - b) mod c"
   548   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   549   by simp
   550 
   551 lemma mod_diff_cong:
   552   assumes "a mod c = a' mod c"
   553   assumes "b mod c = b' mod c"
   554   shows "(a - b) mod c = (a' - b') mod c"
   555   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   556   by simp
   557 
   558 lemma minus_mod_self2 [simp]:
   559   "(a - b) mod b = a mod b"
   560   using mod_diff_right_eq [of a b b]
   561   by (simp add: mod_diff_right_eq)
   562 
   563 lemma minus_mod_self1 [simp]:
   564   "(b - a) mod b = - a mod b"
   565   using mod_add_self2 [of "- a" b] by simp
   566 
   567 lemma mod_eq_dvd_iff:
   568   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   569 proof
   570   assume ?P
   571   then have "(a mod c - b mod c) mod c = 0"
   572     by simp
   573   then show ?Q
   574     by (simp add: dvd_eq_mod_eq_0 mod_simps)
   575 next
   576   assume ?Q
   577   then obtain d where d: "a - b = c * d" ..
   578   then have "a = c * d + b"
   579     by (simp add: algebra_simps)
   580   then show ?P by simp
   581 qed
   582 
   583 end
   584 
   585   
   586 subsection \<open>Uniquely determined division\<close>
   587   
   588 class unique_euclidean_semiring = euclidean_semiring + 
   589   fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   590   assumes size_mono_mult:
   591     "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   592       \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   593     -- \<open>FIXME justify\<close>
   594   assumes uniqueness_constraint_mono_mult:
   595     "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   596   assumes uniqueness_constraint_mod:
   597     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   598   assumes div_bounded:
   599     "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   600     \<Longrightarrow> euclidean_size r < euclidean_size b
   601     \<Longrightarrow> (q * b + r) div b = q"
   602 begin
   603 
   604 lemma divmod_cases [case_names divides remainder by0]:
   605   obtains 
   606     (divides) q where "b \<noteq> 0"
   607       and "a div b = q"
   608       and "a mod b = 0"
   609       and "a = q * b"
   610   | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
   611       and "uniqueness_constraint r b"
   612       and "euclidean_size r < euclidean_size b"
   613       and "a div b = q"
   614       and "a mod b = r"
   615       and "a = q * b + r"
   616   | (by0) "b = 0"
   617 proof (cases "b = 0")
   618   case True
   619   then show thesis
   620   by (rule by0)
   621 next
   622   case False
   623   show thesis
   624   proof (cases "b dvd a")
   625     case True
   626     then obtain q where "a = b * q" ..
   627     with \<open>b \<noteq> 0\<close> divides
   628     show thesis
   629       by (simp add: ac_simps)
   630   next
   631     case False
   632     then have "a mod b \<noteq> 0"
   633       by (simp add: mod_eq_0_iff_dvd)
   634     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   635       by (rule uniqueness_constraint_mod)
   636     moreover have "euclidean_size (a mod b) < euclidean_size b"
   637       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   638     moreover have "a = a div b * b + a mod b"
   639       by (simp add: div_mult_mod_eq)
   640     ultimately show thesis
   641       using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   642   qed
   643 qed
   644 
   645 lemma div_eqI:
   646   "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   647     "euclidean_size r < euclidean_size b" "q * b + r = a"
   648 proof -
   649   from that have "(q * b + r) div b = q"
   650     by (auto intro: div_bounded)
   651   with that show ?thesis
   652     by simp
   653 qed
   654 
   655 lemma mod_eqI:
   656   "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   657     "euclidean_size r < euclidean_size b" "q * b + r = a" 
   658 proof -
   659   from that have "a div b = q"
   660     by (rule div_eqI)
   661   moreover have "a div b * b + a mod b = a"
   662     by (fact div_mult_mod_eq)
   663   ultimately have "a div b * b + a mod b = a div b * b + r"
   664     using \<open>q * b + r = a\<close> by simp
   665   then show ?thesis
   666     by simp
   667 qed
   668 
   669 subclass euclidean_semiring_cancel
   670 proof
   671   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   672   proof (cases a b rule: divmod_cases)
   673     case by0
   674     with \<open>b \<noteq> 0\<close> show ?thesis
   675       by simp
   676   next
   677     case (divides q)
   678     then show ?thesis
   679       by (simp add: ac_simps)
   680   next
   681     case (remainder q r)
   682     then show ?thesis
   683       by (auto intro: div_eqI simp add: algebra_simps)
   684   qed
   685 next
   686   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   687   proof (cases a b rule: divmod_cases)
   688     case by0
   689     then show ?thesis
   690       by simp
   691   next
   692     case (divides q)
   693     with \<open>c \<noteq> 0\<close> show ?thesis
   694       by (simp add: mult.left_commute [of c])
   695   next
   696     case (remainder q r)
   697     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   698       by simp
   699     from remainder \<open>c \<noteq> 0\<close>
   700     have "uniqueness_constraint (r * c) (b * c)"
   701       and "euclidean_size (r * c) < euclidean_size (b * c)"
   702       by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   703     with remainder show ?thesis
   704       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   705         (use \<open>b * c \<noteq> 0\<close> in simp)
   706   qed
   707 qed
   708 
   709 end
   710 
   711 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   712 begin
   713   
   714 subclass euclidean_ring_cancel ..
   715 
   716 end
   717 
   718 end