src/HOL/Euclidean_Division.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 64785 ae0bbc8e45ad child 66798 39bb2462e681 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
1 (*  Title:      HOL/Euclidean_Division.thy
2     Author:     Manuel Eberl, TU Muenchen
3     Author:     Florian Haftmann, TU Muenchen
4 *)
6 section \<open>Uniquely determined division in euclidean (semi)rings\<close>
8 theory Euclidean_Division
9   imports Nat_Transfer
10 begin
12 subsection \<open>Quotient and remainder in integral domains\<close>
14 class semidom_modulo = algebraic_semidom + semiring_modulo
15 begin
17 lemma mod_0 [simp]: "0 mod a = 0"
18   using div_mult_mod_eq [of 0 a] by simp
20 lemma mod_by_0 [simp]: "a mod 0 = a"
21   using div_mult_mod_eq [of a 0] by simp
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
31 lemma mod_self [simp]:
32   "a mod a = 0"
33   using div_mult_mod_eq [of a a] by simp
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
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
50 lemma mod_eq_0_iff_dvd:
51   "a mod b = 0 \<longleftrightarrow> b dvd a"
52   by (auto intro: mod_0_imp_dvd)
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)
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))"
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
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
74 end
76 class idom_modulo = idom + semidom_modulo
77 begin
79 subclass idom_divide ..
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)
85 end
88 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
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
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)
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
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
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
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
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)
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
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)
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
195 end
197 class euclidean_ring = idom_modulo + euclidean_semiring
200 subsection \<open>Uniquely determined division\<close>
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
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
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
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
283 end
285 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
287 end