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