src/HOL/Euclidean_Division.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (21 months ago) changeset 66695 91500c024c7f parent 64785 ae0bbc8e45ad child 66798 39bb2462e681 permissions -rw-r--r--
tuned;
```     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 end
```
```   196
```
```   197 class euclidean_ring = idom_modulo + euclidean_semiring
```
```   198
```
```   199
```
```   200 subsection \<open>Uniquely determined division\<close>
```
```   201
```
```   202 class unique_euclidean_semiring = euclidean_semiring +
```
```   203   fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   204   assumes size_mono_mult:
```
```   205     "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
```
```   206       \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
```
```   207     -- \<open>FIXME justify\<close>
```
```   208   assumes uniqueness_constraint_mono_mult:
```
```   209     "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
```
```   210   assumes uniqueness_constraint_mod:
```
```   211     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
```
```   212   assumes div_bounded:
```
```   213     "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
```
```   214     \<Longrightarrow> euclidean_size r < euclidean_size b
```
```   215     \<Longrightarrow> (q * b + r) div b = q"
```
```   216 begin
```
```   217
```
```   218 lemma divmod_cases [case_names divides remainder by0]:
```
```   219   obtains
```
```   220     (divides) q where "b \<noteq> 0"
```
```   221       and "a div b = q"
```
```   222       and "a mod b = 0"
```
```   223       and "a = q * b"
```
```   224   | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
```
```   225       and "uniqueness_constraint r b"
```
```   226       and "euclidean_size r < euclidean_size b"
```
```   227       and "a div b = q"
```
```   228       and "a mod b = r"
```
```   229       and "a = q * b + r"
```
```   230   | (by0) "b = 0"
```
```   231 proof (cases "b = 0")
```
```   232   case True
```
```   233   then show thesis
```
```   234   by (rule by0)
```
```   235 next
```
```   236   case False
```
```   237   show thesis
```
```   238   proof (cases "b dvd a")
```
```   239     case True
```
```   240     then obtain q where "a = b * q" ..
```
```   241     with \<open>b \<noteq> 0\<close> divides
```
```   242     show thesis
```
```   243       by (simp add: ac_simps)
```
```   244   next
```
```   245     case False
```
```   246     then have "a mod b \<noteq> 0"
```
```   247       by (simp add: mod_eq_0_iff_dvd)
```
```   248     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
```
```   249       by (rule uniqueness_constraint_mod)
```
```   250     moreover have "euclidean_size (a mod b) < euclidean_size b"
```
```   251       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
```
```   252     moreover have "a = a div b * b + a mod b"
```
```   253       by (simp add: div_mult_mod_eq)
```
```   254     ultimately show thesis
```
```   255       using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
```
```   256   qed
```
```   257 qed
```
```   258
```
```   259 lemma div_eqI:
```
```   260   "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
```
```   261     "euclidean_size r < euclidean_size b" "q * b + r = a"
```
```   262 proof -
```
```   263   from that have "(q * b + r) div b = q"
```
```   264     by (auto intro: div_bounded)
```
```   265   with that show ?thesis
```
```   266     by simp
```
```   267 qed
```
```   268
```
```   269 lemma mod_eqI:
```
```   270   "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
```
```   271     "euclidean_size r < euclidean_size b" "q * b + r = a"
```
```   272 proof -
```
```   273   from that have "a div b = q"
```
```   274     by (rule div_eqI)
```
```   275   moreover have "a div b * b + a mod b = a"
```
```   276     by (fact div_mult_mod_eq)
```
```   277   ultimately have "a div b * b + a mod b = a div b * b + r"
```
```   278     using \<open>q * b + r = a\<close> by simp
```
```   279   then show ?thesis
```
```   280     by simp
```
```   281 qed
```
```   282
```
```   283 end
```
```   284
```
```   285 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
```
```   286
```
```   287 end
```