1 (* Title: HOL/Library/Normalized_Fraction.thy |
|
2 Author: Manuel Eberl |
|
3 *) |
|
4 |
|
5 theory Normalized_Fraction |
|
6 imports |
|
7 Main |
|
8 "~~/src/HOL/Number_Theory/Euclidean_Algorithm" |
|
9 Fraction_Field |
|
10 begin |
|
11 |
|
12 definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where |
|
13 "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)" |
|
14 |
|
15 definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \<times> 'a \<Rightarrow> 'a \<times> 'a" where |
|
16 "normalize_quot = |
|
17 (\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))" |
|
18 |
|
19 definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where |
|
20 "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}" |
|
21 |
|
22 lemma not_normalized_fracts_0_denom [simp]: "(a, 0) \<notin> normalized_fracts" |
|
23 by (auto simp: normalized_fracts_def) |
|
24 |
|
25 lemma unit_factor_snd_normalize_quot [simp]: |
|
26 "unit_factor (snd (normalize_quot x)) = 1" |
|
27 by (simp add: normalize_quot_def case_prod_unfold Let_def dvd_unit_factor_div |
|
28 mult_unit_dvd_iff unit_factor_mult unit_factor_gcd) |
|
29 |
|
30 lemma snd_normalize_quot_nonzero [simp]: "snd (normalize_quot x) \<noteq> 0" |
|
31 using unit_factor_snd_normalize_quot[of x] |
|
32 by (auto simp del: unit_factor_snd_normalize_quot) |
|
33 |
|
34 lemma normalize_quot_aux: |
|
35 fixes a b |
|
36 assumes "b \<noteq> 0" |
|
37 defines "d \<equiv> gcd a b * unit_factor b" |
|
38 shows "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" |
|
39 "d dvd a" "d dvd b" "d \<noteq> 0" |
|
40 proof - |
|
41 from assms show "d dvd a" "d dvd b" |
|
42 by (simp_all add: d_def mult_unit_dvd_iff) |
|
43 thus "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" "d \<noteq> 0" |
|
44 by (auto simp: normalize_quot_def Let_def d_def \<open>b \<noteq> 0\<close>) |
|
45 qed |
|
46 |
|
47 lemma normalize_quotE: |
|
48 assumes "b \<noteq> 0" |
|
49 obtains d where "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" |
|
50 "d dvd a" "d dvd b" "d \<noteq> 0" |
|
51 using that[OF normalize_quot_aux[OF assms]] . |
|
52 |
|
53 lemma normalize_quotE': |
|
54 assumes "snd x \<noteq> 0" |
|
55 obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d" |
|
56 "d dvd fst x" "d dvd snd x" "d \<noteq> 0" |
|
57 proof - |
|
58 from normalize_quotE[OF assms, of "fst x"] guess d . |
|
59 from this show ?thesis unfolding prod.collapse by (intro that[of d]) |
|
60 qed |
|
61 |
|
62 lemma coprime_normalize_quot: |
|
63 "coprime (fst (normalize_quot x)) (snd (normalize_quot x))" |
|
64 by (simp add: normalize_quot_def case_prod_unfold Let_def |
|
65 div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime) |
|
66 |
|
67 lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts" |
|
68 by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold) |
|
69 |
|
70 lemma normalize_quot_eq_iff: |
|
71 assumes "b \<noteq> 0" "d \<noteq> 0" |
|
72 shows "normalize_quot (a,b) = normalize_quot (c,d) \<longleftrightarrow> a * d = b * c" |
|
73 proof - |
|
74 define x y where "x = normalize_quot (a,b)" and "y = normalize_quot (c,d)" |
|
75 from normalize_quotE[OF assms(1), of a] normalize_quotE[OF assms(2), of c] |
|
76 obtain d1 d2 |
|
77 where "a = fst x * d1" "b = snd x * d1" "c = fst y * d2" "d = snd y * d2" "d1 \<noteq> 0" "d2 \<noteq> 0" |
|
78 unfolding x_def y_def by metis |
|
79 hence "a * d = b * c \<longleftrightarrow> fst x * snd y = snd x * fst y" by simp |
|
80 also have "\<dots> \<longleftrightarrow> fst x = fst y \<and> snd x = snd y" |
|
81 by (intro coprime_crossproduct') (simp_all add: x_def y_def coprime_normalize_quot) |
|
82 also have "\<dots> \<longleftrightarrow> x = y" using prod_eqI by blast |
|
83 finally show "x = y \<longleftrightarrow> a * d = b * c" .. |
|
84 qed |
|
85 |
|
86 lemma normalize_quot_eq_iff': |
|
87 assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
88 shows "normalize_quot x = normalize_quot y \<longleftrightarrow> fst x * snd y = snd x * fst y" |
|
89 using assms by (cases x, cases y, hypsubst) (subst normalize_quot_eq_iff, simp_all) |
|
90 |
|
91 lemma normalize_quot_id: "x \<in> normalized_fracts \<Longrightarrow> normalize_quot x = x" |
|
92 by (auto simp: normalized_fracts_def normalize_quot_def case_prod_unfold) |
|
93 |
|
94 lemma normalize_quot_idem [simp]: "normalize_quot (normalize_quot x) = normalize_quot x" |
|
95 by (rule normalize_quot_id) simp_all |
|
96 |
|
97 lemma fractrel_iff_normalize_quot_eq: |
|
98 "fractrel x y \<longleftrightarrow> normalize_quot x = normalize_quot y \<and> snd x \<noteq> 0 \<and> snd y \<noteq> 0" |
|
99 by (cases x, cases y) (auto simp: fractrel_def normalize_quot_eq_iff) |
|
100 |
|
101 lemma fractrel_normalize_quot_left: |
|
102 assumes "snd x \<noteq> 0" |
|
103 shows "fractrel (normalize_quot x) y \<longleftrightarrow> fractrel x y" |
|
104 using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
|
105 |
|
106 lemma fractrel_normalize_quot_right: |
|
107 assumes "snd x \<noteq> 0" |
|
108 shows "fractrel y (normalize_quot x) \<longleftrightarrow> fractrel y x" |
|
109 using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
|
110 |
|
111 |
|
112 lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \<Rightarrow> 'a \<times> 'a" |
|
113 is normalize_quot |
|
114 by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all |
|
115 |
|
116 lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x" |
|
117 unfolding quot_to_fract_def |
|
118 proof transfer |
|
119 fix x :: "'a \<times> 'a" assume rel: "fractrel x x" |
|
120 define x' where "x' = normalize_quot x" |
|
121 obtain a b where [simp]: "x = (a, b)" by (cases x) |
|
122 from rel have "b \<noteq> 0" by simp |
|
123 from normalize_quotE[OF this, of a] guess d . |
|
124 hence "a = fst x' * d" "b = snd x' * d" "d \<noteq> 0" "snd x' \<noteq> 0" by (simp_all add: x'_def) |
|
125 thus "fractrel (case x' of (a, b) \<Rightarrow> if b = 0 then (0, 1) else (a, b)) x" |
|
126 by (auto simp add: case_prod_unfold) |
|
127 qed |
|
128 |
|
129 lemma quot_of_fract_quot_to_fract: "quot_of_fract (quot_to_fract x) = normalize_quot x" |
|
130 proof (cases "snd x = 0") |
|
131 case True |
|
132 thus ?thesis unfolding quot_to_fract_def |
|
133 by transfer (simp add: case_prod_unfold normalize_quot_def) |
|
134 next |
|
135 case False |
|
136 thus ?thesis unfolding quot_to_fract_def by transfer (simp add: case_prod_unfold) |
|
137 qed |
|
138 |
|
139 lemma quot_of_fract_quot_to_fract': |
|
140 "x \<in> normalized_fracts \<Longrightarrow> quot_of_fract (quot_to_fract x) = x" |
|
141 unfolding quot_to_fract_def by transfer (auto simp: normalize_quot_id) |
|
142 |
|
143 lemma quot_of_fract_in_normalized_fracts [simp]: "quot_of_fract x \<in> normalized_fracts" |
|
144 by transfer simp |
|
145 |
|
146 lemma normalize_quotI: |
|
147 assumes "a * d = b * c" "b \<noteq> 0" "(c, d) \<in> normalized_fracts" |
|
148 shows "normalize_quot (a, b) = (c, d)" |
|
149 proof - |
|
150 from assms have "normalize_quot (a, b) = normalize_quot (c, d)" |
|
151 by (subst normalize_quot_eq_iff) auto |
|
152 also have "\<dots> = (c, d)" by (intro normalize_quot_id) fact |
|
153 finally show ?thesis . |
|
154 qed |
|
155 |
|
156 lemma td_normalized_fract: |
|
157 "type_definition quot_of_fract quot_to_fract normalized_fracts" |
|
158 by standard (simp_all add: quot_of_fract_quot_to_fract') |
|
159 |
|
160 lemma quot_of_fract_add_aux: |
|
161 assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
162 shows "(fst x * snd y + fst y * snd x) * (snd (normalize_quot x) * snd (normalize_quot y)) = |
|
163 snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) + |
|
164 snd (normalize_quot x) * fst (normalize_quot y))" |
|
165 proof - |
|
166 from normalize_quotE'[OF assms(1)] guess d . note d = this |
|
167 from normalize_quotE'[OF assms(2)] guess e . note e = this |
|
168 show ?thesis by (simp_all add: d e algebra_simps) |
|
169 qed |
|
170 |
|
171 |
|
172 locale fract_as_normalized_quot |
|
173 begin |
|
174 setup_lifting td_normalized_fract |
|
175 end |
|
176 |
|
177 |
|
178 lemma quot_of_fract_add: |
|
179 "quot_of_fract (x + y) = |
|
180 (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y |
|
181 in normalize_quot (a * d + b * c, b * d))" |
|
182 by transfer (insert quot_of_fract_add_aux, |
|
183 simp_all add: Let_def case_prod_unfold normalize_quot_eq_iff) |
|
184 |
|
185 lemma quot_of_fract_uminus: |
|
186 "quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))" |
|
187 by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff) |
|
188 |
|
189 lemma quot_of_fract_diff: |
|
190 "quot_of_fract (x - y) = |
|
191 (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y |
|
192 in normalize_quot (a * d - b * c, b * d))" (is "_ = ?rhs") |
|
193 proof - |
|
194 have "x - y = x + -y" by simp |
|
195 also have "quot_of_fract \<dots> = ?rhs" |
|
196 by (simp only: quot_of_fract_add quot_of_fract_uminus Let_def case_prod_unfold) simp_all |
|
197 finally show ?thesis . |
|
198 qed |
|
199 |
|
200 lemma normalize_quot_mult_coprime: |
|
201 assumes "coprime a b" "coprime c d" "unit_factor b = 1" "unit_factor d = 1" |
|
202 defines "e \<equiv> fst (normalize_quot (a, d))" and "f \<equiv> snd (normalize_quot (a, d))" |
|
203 and "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))" |
|
204 shows "normalize_quot (a * c, b * d) = (e * g, f * h)" |
|
205 proof (rule normalize_quotI) |
|
206 from assms have "b \<noteq> 0" "d \<noteq> 0" by auto |
|
207 from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms] |
|
208 from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms] |
|
209 from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all) |
|
210 from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1" |
|
211 by simp_all |
|
212 from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot) |
|
213 with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts" |
|
214 by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq') |
|
215 qed (insert assms(3,4), auto) |
|
216 |
|
217 lemma normalize_quot_mult: |
|
218 assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
219 shows "normalize_quot (fst x * fst y, snd x * snd y) = normalize_quot |
|
220 (fst (normalize_quot x) * fst (normalize_quot y), |
|
221 snd (normalize_quot x) * snd (normalize_quot y))" |
|
222 proof - |
|
223 from normalize_quotE'[OF assms(1)] guess d . note d = this |
|
224 from normalize_quotE'[OF assms(2)] guess e . note e = this |
|
225 show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff) |
|
226 qed |
|
227 |
|
228 lemma quot_of_fract_mult: |
|
229 "quot_of_fract (x * y) = |
|
230 (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; |
|
231 (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b) |
|
232 in (e*g, f*h))" |
|
233 by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric] |
|
234 coprime_normalize_quot normalize_quot_mult [symmetric]) |
|
235 |
|
236 lemma normalize_quot_0 [simp]: |
|
237 "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)" |
|
238 by (simp_all add: normalize_quot_def) |
|
239 |
|
240 lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0" |
|
241 by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff) |
|
242 find_theorems "_ div _ = 0" |
|
243 |
|
244 lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1" |
|
245 by transfer auto |
|
246 |
|
247 lemma normalize_quot_swap: |
|
248 assumes "a \<noteq> 0" "b \<noteq> 0" |
|
249 defines "a' \<equiv> fst (normalize_quot (a, b))" and "b' \<equiv> snd (normalize_quot (a, b))" |
|
250 shows "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')" |
|
251 proof (rule normalize_quotI) |
|
252 from normalize_quotE[OF assms(2), of a] guess d . note d = this [folded assms(3,4)] |
|
253 show "b * (a' div unit_factor a') = a * (b' div unit_factor a')" |
|
254 using assms(1,2) d |
|
255 by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor) |
|
256 have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot) |
|
257 thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts" |
|
258 using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute) |
|
259 qed fact+ |
|
260 |
|
261 lemma quot_of_fract_inverse: |
|
262 "quot_of_fract (inverse x) = |
|
263 (let (a,b) = quot_of_fract x; d = unit_factor a |
|
264 in if d = 0 then (0, 1) else (b div d, a div d))" |
|
265 proof (transfer, goal_cases) |
|
266 case (1 x) |
|
267 from normalize_quot_swap[of "fst x" "snd x"] show ?case |
|
268 by (auto simp: Let_def case_prod_unfold) |
|
269 qed |
|
270 |
|
271 lemma normalize_quot_div_unit_left: |
|
272 fixes x y u |
|
273 assumes "is_unit u" |
|
274 defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
275 shows "normalize_quot (x div u, y) = (x' div u, y')" |
|
276 proof (cases "y = 0") |
|
277 case False |
|
278 from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)] |
|
279 from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot) |
|
280 with False d \<open>is_unit u\<close> show ?thesis |
|
281 by (intro normalize_quotI) |
|
282 (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel |
|
283 gcd_div_unit1) |
|
284 qed (simp_all add: assms) |
|
285 |
|
286 lemma normalize_quot_div_unit_right: |
|
287 fixes x y u |
|
288 assumes "is_unit u" |
|
289 defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
290 shows "normalize_quot (x, y div u) = (x' * u, y')" |
|
291 proof (cases "y = 0") |
|
292 case False |
|
293 from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)] |
|
294 from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot) |
|
295 with False d \<open>is_unit u\<close> show ?thesis |
|
296 by (intro normalize_quotI) |
|
297 (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel |
|
298 gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric]) |
|
299 qed (simp_all add: assms) |
|
300 |
|
301 lemma normalize_quot_normalize_left: |
|
302 fixes x y u |
|
303 defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
304 shows "normalize_quot (normalize x, y) = (x' div unit_factor x, y')" |
|
305 using normalize_quot_div_unit_left[of "unit_factor x" x y] |
|
306 by (cases "x = 0") (simp_all add: assms) |
|
307 |
|
308 lemma normalize_quot_normalize_right: |
|
309 fixes x y u |
|
310 defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
311 shows "normalize_quot (x, normalize y) = (x' * unit_factor y, y')" |
|
312 using normalize_quot_div_unit_right[of "unit_factor y" x y] |
|
313 by (cases "y = 0") (simp_all add: assms) |
|
314 |
|
315 lemma quot_of_fract_0 [simp]: "quot_of_fract 0 = (0, 1)" |
|
316 by transfer auto |
|
317 |
|
318 lemma quot_of_fract_1 [simp]: "quot_of_fract 1 = (1, 1)" |
|
319 by transfer (rule normalize_quotI, simp_all add: normalized_fracts_def) |
|
320 |
|
321 lemma quot_of_fract_divide: |
|
322 "quot_of_fract (x / y) = (if y = 0 then (0, 1) else |
|
323 (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; |
|
324 (e,f) = normalize_quot (a,c); (g,h) = normalize_quot (d,b) |
|
325 in (e * g, f * h)))" (is "_ = ?rhs") |
|
326 proof (cases "y = 0") |
|
327 case False |
|
328 hence A: "fst (quot_of_fract y) \<noteq> 0" by transfer auto |
|
329 have "x / y = x * inverse y" by (simp add: divide_inverse) |
|
330 also from False A have "quot_of_fract \<dots> = ?rhs" |
|
331 by (simp only: quot_of_fract_mult quot_of_fract_inverse) |
|
332 (simp_all add: Let_def case_prod_unfold fst_quot_of_fract_0_imp |
|
333 normalize_quot_div_unit_left normalize_quot_div_unit_right |
|
334 normalize_quot_normalize_right normalize_quot_normalize_left) |
|
335 finally show ?thesis . |
|
336 qed simp_all |
|
337 |
|
338 end |
|