author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 76121 | f58ad163bb75 |
permissions | -rw-r--r-- |
65435 | 1 |
(* Title: HOL/Computational_Algebra/Normalized_Fraction.thy |
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64240
diff
changeset
|
2 |
Author: Manuel Eberl |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64240
diff
changeset
|
3 |
*) |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64240
diff
changeset
|
4 |
|
63500 | 5 |
theory Normalized_Fraction |
6 |
imports |
|
7 |
Main |
|
65417 | 8 |
Euclidean_Algorithm |
65366 | 9 |
Fraction_Field |
63500 | 10 |
begin |
11 |
||
76121 | 12 |
lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x" |
13 |
using unit_factor_mult_normalize [of x] by simp |
|
14 |
||
15 |
definition quot_to_fract :: "'a \<times> 'a \<Rightarrow> 'a :: idom fract" where |
|
63500 | 16 |
"quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)" |
17 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
67078
diff
changeset
|
18 |
definition normalize_quot :: "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} \<times> 'a \<Rightarrow> 'a \<times> 'a" where |
63500 | 19 |
"normalize_quot = |
20 |
(\<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))" |
|
21 |
||
67051 | 22 |
lemma normalize_quot_zero [simp]: |
23 |
"normalize_quot (a, 0) = (0, 1)" |
|
24 |
by (simp add: normalize_quot_def) |
|
25 |
||
67078
6a85b8a9c28c
removed overambitious simp rules from e7e54a0b9197
haftmann
parents:
67051
diff
changeset
|
26 |
lemma normalize_quot_proj: |
67051 | 27 |
"fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)" |
28 |
"snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0" |
|
29 |
using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff') |
|
30 |
||
63500 | 31 |
definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where |
32 |
"normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}" |
|
33 |
||
34 |
lemma not_normalized_fracts_0_denom [simp]: "(a, 0) \<notin> normalized_fracts" |
|
35 |
by (auto simp: normalized_fracts_def) |
|
36 |
||
37 |
lemma unit_factor_snd_normalize_quot [simp]: |
|
38 |
"unit_factor (snd (normalize_quot x)) = 1" |
|
39 |
by (simp add: normalize_quot_def case_prod_unfold Let_def dvd_unit_factor_div |
|
40 |
mult_unit_dvd_iff unit_factor_mult unit_factor_gcd) |
|
41 |
||
42 |
lemma snd_normalize_quot_nonzero [simp]: "snd (normalize_quot x) \<noteq> 0" |
|
43 |
using unit_factor_snd_normalize_quot[of x] |
|
44 |
by (auto simp del: unit_factor_snd_normalize_quot) |
|
45 |
||
46 |
lemma normalize_quot_aux: |
|
47 |
fixes a b |
|
48 |
assumes "b \<noteq> 0" |
|
49 |
defines "d \<equiv> gcd a b * unit_factor b" |
|
50 |
shows "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" |
|
51 |
"d dvd a" "d dvd b" "d \<noteq> 0" |
|
52 |
proof - |
|
53 |
from assms show "d dvd a" "d dvd b" |
|
54 |
by (simp_all add: d_def mult_unit_dvd_iff) |
|
55 |
thus "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" "d \<noteq> 0" |
|
56 |
by (auto simp: normalize_quot_def Let_def d_def \<open>b \<noteq> 0\<close>) |
|
57 |
qed |
|
58 |
||
59 |
lemma normalize_quotE: |
|
60 |
assumes "b \<noteq> 0" |
|
61 |
obtains d where "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" |
|
62 |
"d dvd a" "d dvd b" "d \<noteq> 0" |
|
63 |
using that[OF normalize_quot_aux[OF assms]] . |
|
64 |
||
65 |
lemma normalize_quotE': |
|
66 |
assumes "snd x \<noteq> 0" |
|
67 |
obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d" |
|
68 |
"d dvd fst x" "d dvd snd x" "d \<noteq> 0" |
|
69 |
proof - |
|
74362 | 70 |
from normalize_quotE[OF assms, of "fst x"] obtain d where |
71 |
"fst x = fst (normalize_quot (fst x, snd x)) * d" |
|
72 |
"snd x = snd (normalize_quot (fst x, snd x)) * d" |
|
73 |
"d dvd fst x" |
|
74 |
"d dvd snd x" |
|
75 |
"d \<noteq> 0" . |
|
76 |
then show ?thesis unfolding prod.collapse by (intro that[of d]) |
|
63500 | 77 |
qed |
78 |
||
79 |
lemma coprime_normalize_quot: |
|
80 |
"coprime (fst (normalize_quot x)) (snd (normalize_quot x))" |
|
67051 | 81 |
by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2) |
82 |
(metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit) |
|
63500 | 83 |
|
84 |
lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts" |
|
85 |
by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold) |
|
86 |
||
87 |
lemma normalize_quot_eq_iff: |
|
88 |
assumes "b \<noteq> 0" "d \<noteq> 0" |
|
89 |
shows "normalize_quot (a,b) = normalize_quot (c,d) \<longleftrightarrow> a * d = b * c" |
|
90 |
proof - |
|
91 |
define x y where "x = normalize_quot (a,b)" and "y = normalize_quot (c,d)" |
|
92 |
from normalize_quotE[OF assms(1), of a] normalize_quotE[OF assms(2), of c] |
|
93 |
obtain d1 d2 |
|
94 |
where "a = fst x * d1" "b = snd x * d1" "c = fst y * d2" "d = snd y * d2" "d1 \<noteq> 0" "d2 \<noteq> 0" |
|
95 |
unfolding x_def y_def by metis |
|
96 |
hence "a * d = b * c \<longleftrightarrow> fst x * snd y = snd x * fst y" by simp |
|
97 |
also have "\<dots> \<longleftrightarrow> fst x = fst y \<and> snd x = snd y" |
|
98 |
by (intro coprime_crossproduct') (simp_all add: x_def y_def coprime_normalize_quot) |
|
99 |
also have "\<dots> \<longleftrightarrow> x = y" using prod_eqI by blast |
|
100 |
finally show "x = y \<longleftrightarrow> a * d = b * c" .. |
|
101 |
qed |
|
102 |
||
103 |
lemma normalize_quot_eq_iff': |
|
104 |
assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
105 |
shows "normalize_quot x = normalize_quot y \<longleftrightarrow> fst x * snd y = snd x * fst y" |
|
106 |
using assms by (cases x, cases y, hypsubst) (subst normalize_quot_eq_iff, simp_all) |
|
107 |
||
108 |
lemma normalize_quot_id: "x \<in> normalized_fracts \<Longrightarrow> normalize_quot x = x" |
|
109 |
by (auto simp: normalized_fracts_def normalize_quot_def case_prod_unfold) |
|
110 |
||
111 |
lemma normalize_quot_idem [simp]: "normalize_quot (normalize_quot x) = normalize_quot x" |
|
112 |
by (rule normalize_quot_id) simp_all |
|
113 |
||
114 |
lemma fractrel_iff_normalize_quot_eq: |
|
115 |
"fractrel x y \<longleftrightarrow> normalize_quot x = normalize_quot y \<and> snd x \<noteq> 0 \<and> snd y \<noteq> 0" |
|
116 |
by (cases x, cases y) (auto simp: fractrel_def normalize_quot_eq_iff) |
|
117 |
||
118 |
lemma fractrel_normalize_quot_left: |
|
119 |
assumes "snd x \<noteq> 0" |
|
120 |
shows "fractrel (normalize_quot x) y \<longleftrightarrow> fractrel x y" |
|
121 |
using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
|
122 |
||
123 |
lemma fractrel_normalize_quot_right: |
|
124 |
assumes "snd x \<noteq> 0" |
|
125 |
shows "fractrel y (normalize_quot x) \<longleftrightarrow> fractrel y x" |
|
126 |
using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
|
127 |
||
128 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
67078
diff
changeset
|
129 |
lift_definition quot_of_fract :: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
67078
diff
changeset
|
130 |
"'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract \<Rightarrow> 'a \<times> 'a" |
63500 | 131 |
is normalize_quot |
132 |
by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all |
|
133 |
||
134 |
lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x" |
|
135 |
unfolding quot_to_fract_def |
|
136 |
proof transfer |
|
137 |
fix x :: "'a \<times> 'a" assume rel: "fractrel x x" |
|
138 |
define x' where "x' = normalize_quot x" |
|
139 |
obtain a b where [simp]: "x = (a, b)" by (cases x) |
|
140 |
from rel have "b \<noteq> 0" by simp |
|
74362 | 141 |
from normalize_quotE[OF this, of a] obtain d |
142 |
where |
|
143 |
"a = fst (normalize_quot (a, b)) * d" |
|
144 |
"b = snd (normalize_quot (a, b)) * d" |
|
145 |
"d dvd a" |
|
146 |
"d dvd b" |
|
147 |
"d \<noteq> 0" . |
|
63500 | 148 |
hence "a = fst x' * d" "b = snd x' * d" "d \<noteq> 0" "snd x' \<noteq> 0" by (simp_all add: x'_def) |
149 |
thus "fractrel (case x' of (a, b) \<Rightarrow> if b = 0 then (0, 1) else (a, b)) x" |
|
150 |
by (auto simp add: case_prod_unfold) |
|
151 |
qed |
|
152 |
||
153 |
lemma quot_of_fract_quot_to_fract: "quot_of_fract (quot_to_fract x) = normalize_quot x" |
|
154 |
proof (cases "snd x = 0") |
|
155 |
case True |
|
156 |
thus ?thesis unfolding quot_to_fract_def |
|
157 |
by transfer (simp add: case_prod_unfold normalize_quot_def) |
|
158 |
next |
|
159 |
case False |
|
160 |
thus ?thesis unfolding quot_to_fract_def by transfer (simp add: case_prod_unfold) |
|
161 |
qed |
|
162 |
||
163 |
lemma quot_of_fract_quot_to_fract': |
|
164 |
"x \<in> normalized_fracts \<Longrightarrow> quot_of_fract (quot_to_fract x) = x" |
|
165 |
unfolding quot_to_fract_def by transfer (auto simp: normalize_quot_id) |
|
166 |
||
167 |
lemma quot_of_fract_in_normalized_fracts [simp]: "quot_of_fract x \<in> normalized_fracts" |
|
168 |
by transfer simp |
|
169 |
||
170 |
lemma normalize_quotI: |
|
171 |
assumes "a * d = b * c" "b \<noteq> 0" "(c, d) \<in> normalized_fracts" |
|
172 |
shows "normalize_quot (a, b) = (c, d)" |
|
173 |
proof - |
|
174 |
from assms have "normalize_quot (a, b) = normalize_quot (c, d)" |
|
175 |
by (subst normalize_quot_eq_iff) auto |
|
176 |
also have "\<dots> = (c, d)" by (intro normalize_quot_id) fact |
|
177 |
finally show ?thesis . |
|
178 |
qed |
|
179 |
||
180 |
lemma td_normalized_fract: |
|
181 |
"type_definition quot_of_fract quot_to_fract normalized_fracts" |
|
182 |
by standard (simp_all add: quot_of_fract_quot_to_fract') |
|
183 |
||
184 |
lemma quot_of_fract_add_aux: |
|
185 |
assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
186 |
shows "(fst x * snd y + fst y * snd x) * (snd (normalize_quot x) * snd (normalize_quot y)) = |
|
187 |
snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) + |
|
188 |
snd (normalize_quot x) * fst (normalize_quot y))" |
|
189 |
proof - |
|
74362 | 190 |
from normalize_quotE'[OF assms(1)] obtain d |
191 |
where d: |
|
192 |
"fst x = fst (normalize_quot x) * d" |
|
193 |
"snd x = snd (normalize_quot x) * d" |
|
194 |
"d dvd fst x" |
|
195 |
"d dvd snd x" |
|
196 |
"d \<noteq> 0" . |
|
197 |
from normalize_quotE'[OF assms(2)] obtain e |
|
198 |
where e: |
|
199 |
"fst y = fst (normalize_quot y) * e" |
|
200 |
"snd y = snd (normalize_quot y) * e" |
|
201 |
"e dvd fst y" |
|
202 |
"e dvd snd y" |
|
203 |
"e \<noteq> 0" . |
|
63500 | 204 |
show ?thesis by (simp_all add: d e algebra_simps) |
205 |
qed |
|
206 |
||
207 |
||
208 |
locale fract_as_normalized_quot |
|
209 |
begin |
|
210 |
setup_lifting td_normalized_fract |
|
211 |
end |
|
212 |
||
213 |
||
214 |
lemma quot_of_fract_add: |
|
215 |
"quot_of_fract (x + y) = |
|
216 |
(let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y |
|
217 |
in normalize_quot (a * d + b * c, b * d))" |
|
218 |
by transfer (insert quot_of_fract_add_aux, |
|
219 |
simp_all add: Let_def case_prod_unfold normalize_quot_eq_iff) |
|
220 |
||
221 |
lemma quot_of_fract_uminus: |
|
222 |
"quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))" |
|
64592
7759f1766189
more fine-grained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset
|
223 |
by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff) |
63500 | 224 |
|
225 |
lemma quot_of_fract_diff: |
|
226 |
"quot_of_fract (x - y) = |
|
227 |
(let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y |
|
228 |
in normalize_quot (a * d - b * c, b * d))" (is "_ = ?rhs") |
|
229 |
proof - |
|
230 |
have "x - y = x + -y" by simp |
|
231 |
also have "quot_of_fract \<dots> = ?rhs" |
|
232 |
by (simp only: quot_of_fract_add quot_of_fract_uminus Let_def case_prod_unfold) simp_all |
|
233 |
finally show ?thesis . |
|
234 |
qed |
|
235 |
||
236 |
lemma normalize_quot_mult_coprime: |
|
237 |
assumes "coprime a b" "coprime c d" "unit_factor b = 1" "unit_factor d = 1" |
|
238 |
defines "e \<equiv> fst (normalize_quot (a, d))" and "f \<equiv> snd (normalize_quot (a, d))" |
|
239 |
and "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))" |
|
240 |
shows "normalize_quot (a * c, b * d) = (e * g, f * h)" |
|
241 |
proof (rule normalize_quotI) |
|
67051 | 242 |
from assms have "gcd a b = 1" "gcd c d = 1" |
243 |
by simp_all |
|
63500 | 244 |
from assms have "b \<noteq> 0" "d \<noteq> 0" by auto |
67051 | 245 |
with assms have "normalize b = b" "normalize d = d" |
246 |
by (auto intro: normalize_unit_factor_eqI) |
|
74362 | 247 |
from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] obtain k |
248 |
where |
|
249 |
"c = fst (normalize_quot (c, b)) * k" |
|
250 |
"b = snd (normalize_quot (c, b)) * k" |
|
251 |
"k dvd c" "k dvd b" "k \<noteq> 0" . |
|
67051 | 252 |
note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)] |
74362 | 253 |
from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] obtain l |
254 |
where "a = fst (normalize_quot (a, d)) * l" |
|
255 |
"d = snd (normalize_quot (a, d)) * l" |
|
256 |
"l dvd a" "l dvd d" "l \<noteq> 0" . |
|
67051 | 257 |
note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)] |
258 |
from k l show "a * c * (f * h) = b * d * (e * g)" |
|
259 |
by (metis e_def f_def g_def h_def mult.commute mult.left_commute) |
|
63500 | 260 |
from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1" |
261 |
by simp_all |
|
262 |
from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot) |
|
67051 | 263 |
with k l assms(1,2) \<open>b \<noteq> 0\<close> \<open>d \<noteq> 0\<close> \<open>unit_factor b = 1\<close> \<open>unit_factor d = 1\<close> |
264 |
\<open>normalize b = b\<close> \<open>normalize d = d\<close> |
|
265 |
show "(e * g, f * h) \<in> normalized_fracts" |
|
266 |
by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def |
|
267 |
coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd) |
|
268 |
(metis coprime_mult_left_iff coprime_mult_right_iff) |
|
63500 | 269 |
qed (insert assms(3,4), auto) |
270 |
||
271 |
lemma normalize_quot_mult: |
|
272 |
assumes "snd x \<noteq> 0" "snd y \<noteq> 0" |
|
273 |
shows "normalize_quot (fst x * fst y, snd x * snd y) = normalize_quot |
|
274 |
(fst (normalize_quot x) * fst (normalize_quot y), |
|
275 |
snd (normalize_quot x) * snd (normalize_quot y))" |
|
276 |
proof - |
|
74362 | 277 |
from normalize_quotE'[OF assms(1)] obtain d where d: |
278 |
"fst x = fst (normalize_quot x) * d" |
|
279 |
"snd x = snd (normalize_quot x) * d" |
|
280 |
"d dvd fst x" |
|
281 |
"d dvd snd x" |
|
282 |
"d \<noteq> 0" . |
|
283 |
from normalize_quotE'[OF assms(2)] obtain e where e: |
|
284 |
"fst y = fst (normalize_quot y) * e" |
|
285 |
"snd y = snd (normalize_quot y) * e" |
|
286 |
"e dvd fst y" |
|
287 |
"e dvd snd y" |
|
288 |
"e \<noteq> 0" . |
|
63500 | 289 |
show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff) |
290 |
qed |
|
291 |
||
292 |
lemma quot_of_fract_mult: |
|
293 |
"quot_of_fract (x * y) = |
|
294 |
(let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; |
|
295 |
(e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b) |
|
296 |
in (e*g, f*h))" |
|
67051 | 297 |
by transfer |
298 |
(simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime) |
|
63500 | 299 |
|
300 |
lemma normalize_quot_0 [simp]: |
|
301 |
"normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)" |
|
302 |
by (simp_all add: normalize_quot_def) |
|
303 |
||
304 |
lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0" |
|
305 |
by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff) |
|
306 |
||
307 |
lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1" |
|
308 |
by transfer auto |
|
309 |
||
310 |
lemma normalize_quot_swap: |
|
311 |
assumes "a \<noteq> 0" "b \<noteq> 0" |
|
312 |
defines "a' \<equiv> fst (normalize_quot (a, b))" and "b' \<equiv> snd (normalize_quot (a, b))" |
|
313 |
shows "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')" |
|
314 |
proof (rule normalize_quotI) |
|
74362 | 315 |
from normalize_quotE[OF assms(2), of a] obtain d where |
316 |
"a = fst (normalize_quot (a, b)) * d" |
|
317 |
"b = snd (normalize_quot (a, b)) * d" |
|
318 |
"d dvd a" "d dvd b" "d \<noteq> 0" . |
|
319 |
note d = this [folded assms(3,4)] |
|
63500 | 320 |
show "b * (a' div unit_factor a') = a * (b' div unit_factor a')" |
321 |
using assms(1,2) d |
|
322 |
by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor) |
|
323 |
have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot) |
|
324 |
thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts" |
|
67051 | 325 |
using assms(1,2) d |
67078
6a85b8a9c28c
removed overambitious simp rules from e7e54a0b9197
haftmann
parents:
67051
diff
changeset
|
326 |
by (auto simp add: normalized_fracts_def ac_simps dvd_div_unit_iff elim: coprime_imp_coprime) |
63500 | 327 |
qed fact+ |
328 |
||
329 |
lemma quot_of_fract_inverse: |
|
330 |
"quot_of_fract (inverse x) = |
|
331 |
(let (a,b) = quot_of_fract x; d = unit_factor a |
|
332 |
in if d = 0 then (0, 1) else (b div d, a div d))" |
|
333 |
proof (transfer, goal_cases) |
|
334 |
case (1 x) |
|
335 |
from normalize_quot_swap[of "fst x" "snd x"] show ?case |
|
336 |
by (auto simp: Let_def case_prod_unfold) |
|
337 |
qed |
|
338 |
||
339 |
lemma normalize_quot_div_unit_left: |
|
340 |
fixes x y u |
|
341 |
assumes "is_unit u" |
|
342 |
defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
343 |
shows "normalize_quot (x div u, y) = (x' div u, y')" |
|
344 |
proof (cases "y = 0") |
|
345 |
case False |
|
67051 | 346 |
define v where "v = 1 div u" |
347 |
with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v" |
|
348 |
by simp_all |
|
349 |
from \<open>is_unit v\<close> have "coprime v = top" |
|
350 |
by (simp add: fun_eq_iff is_unit_left_imp_coprime) |
|
74362 | 351 |
from normalize_quotE[OF False, of x] obtain d where |
352 |
"x = fst (normalize_quot (x, y)) * d" |
|
353 |
"y = snd (normalize_quot (x, y)) * d" |
|
354 |
"d dvd x" "d dvd y" "d \<noteq> 0" . |
|
67051 | 355 |
note d = this[folded assms(2,3)] |
356 |
from assms have "coprime x' y'" "unit_factor y' = 1" |
|
357 |
by (simp_all add: coprime_normalize_quot) |
|
358 |
with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')" |
|
359 |
by (auto simp: normalized_fracts_def intro: normalize_quotI) |
|
360 |
then show ?thesis |
|
361 |
by (simp add: u) |
|
63500 | 362 |
qed (simp_all add: assms) |
363 |
||
364 |
lemma normalize_quot_div_unit_right: |
|
365 |
fixes x y u |
|
366 |
assumes "is_unit u" |
|
367 |
defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
368 |
shows "normalize_quot (x, y div u) = (x' * u, y')" |
|
369 |
proof (cases "y = 0") |
|
370 |
case False |
|
74362 | 371 |
from normalize_quotE[OF this, of x] |
372 |
obtain d where d: |
|
373 |
"x = fst (normalize_quot (x, y)) * d" |
|
374 |
"y = snd (normalize_quot (x, y)) * d" |
|
375 |
"d dvd x" "d dvd y" "d \<noteq> 0" . |
|
376 |
note d = this[folded assms(2,3)] |
|
63500 | 377 |
from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot) |
67051 | 378 |
with d \<open>is_unit u\<close> show ?thesis |
379 |
by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI) |
|
63500 | 380 |
qed (simp_all add: assms) |
381 |
||
382 |
lemma normalize_quot_normalize_left: |
|
383 |
fixes x y u |
|
384 |
defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
385 |
shows "normalize_quot (normalize x, y) = (x' div unit_factor x, y')" |
|
386 |
using normalize_quot_div_unit_left[of "unit_factor x" x y] |
|
387 |
by (cases "x = 0") (simp_all add: assms) |
|
388 |
||
389 |
lemma normalize_quot_normalize_right: |
|
390 |
fixes x y u |
|
391 |
defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))" |
|
392 |
shows "normalize_quot (x, normalize y) = (x' * unit_factor y, y')" |
|
393 |
using normalize_quot_div_unit_right[of "unit_factor y" x y] |
|
394 |
by (cases "y = 0") (simp_all add: assms) |
|
395 |
||
396 |
lemma quot_of_fract_0 [simp]: "quot_of_fract 0 = (0, 1)" |
|
397 |
by transfer auto |
|
398 |
||
399 |
lemma quot_of_fract_1 [simp]: "quot_of_fract 1 = (1, 1)" |
|
400 |
by transfer (rule normalize_quotI, simp_all add: normalized_fracts_def) |
|
401 |
||
402 |
lemma quot_of_fract_divide: |
|
403 |
"quot_of_fract (x / y) = (if y = 0 then (0, 1) else |
|
404 |
(let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y; |
|
405 |
(e,f) = normalize_quot (a,c); (g,h) = normalize_quot (d,b) |
|
406 |
in (e * g, f * h)))" (is "_ = ?rhs") |
|
407 |
proof (cases "y = 0") |
|
408 |
case False |
|
409 |
hence A: "fst (quot_of_fract y) \<noteq> 0" by transfer auto |
|
410 |
have "x / y = x * inverse y" by (simp add: divide_inverse) |
|
411 |
also from False A have "quot_of_fract \<dots> = ?rhs" |
|
412 |
by (simp only: quot_of_fract_mult quot_of_fract_inverse) |
|
413 |
(simp_all add: Let_def case_prod_unfold fst_quot_of_fract_0_imp |
|
414 |
normalize_quot_div_unit_left normalize_quot_div_unit_right |
|
415 |
normalize_quot_normalize_right normalize_quot_normalize_left) |
|
416 |
finally show ?thesis . |
|
417 |
qed simp_all |
|
418 |
||
76121 | 419 |
lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0" |
420 |
by transfer simp |
|
421 |
||
422 |
lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x" |
|
423 |
by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp) |
|
424 |
||
425 |
lemma snd_quot_of_fract_Fract_whole: |
|
426 |
assumes "y dvd x" |
|
427 |
shows "snd (quot_of_fract (Fract x y)) = 1" |
|
428 |
using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd) |
|
429 |
||
430 |
lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0" |
|
431 |
by transfer simp |
|
432 |
||
433 |
lemma coprime_quot_of_fract: |
|
434 |
"coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))" |
|
435 |
by transfer (simp add: coprime_normalize_quot) |
|
436 |
||
437 |
lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1" |
|
438 |
using quot_of_fract_in_normalized_fracts[of x] |
|
439 |
by (simp add: normalized_fracts_def case_prod_unfold) |
|
440 |
||
441 |
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)" |
|
442 |
by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract) |
|
443 |
||
63500 | 444 |
end |