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
```