67 |
67 |
68 subsubsection {* Representation and basic operations *} |
68 subsubsection {* Representation and basic operations *} |
69 |
69 |
70 definition |
70 definition |
71 Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where |
71 Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where |
72 [code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" |
72 "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" |
73 |
|
74 code_datatype Fract |
|
75 |
|
76 lemma Rat_cases [case_names Fract, cases type: rat]: |
|
77 assumes "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> C" |
|
78 shows C |
|
79 using assms by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) |
|
80 |
|
81 lemma Rat_induct [case_names Fract, induct type: rat]: |
|
82 assumes "\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)" |
|
83 shows "P q" |
|
84 using assms by (cases q) simp |
|
85 |
73 |
86 lemma eq_rat: |
74 lemma eq_rat: |
87 shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
75 shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
88 and "\<And>a. Fract a 0 = Fract 0 1" |
76 and "\<And>a. Fract a 0 = Fract 0 1" |
89 and "\<And>a c. Fract 0 a = Fract 0 c" |
77 and "\<And>a c. Fract 0 a = Fract 0 c" |
90 by (simp_all add: Fract_def) |
78 by (simp_all add: Fract_def) |
91 |
79 |
|
80 lemma Rat_cases [case_names Fract, cases type: rat]: |
|
81 assumes "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" |
|
82 shows C |
|
83 proof - |
|
84 obtain a b :: int where "q = Fract a b" and "b \<noteq> 0" |
|
85 by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) |
|
86 let ?a = "a div gcd a b" |
|
87 let ?b = "b div gcd a b" |
|
88 from `b \<noteq> 0` have "?b * gcd a b = b" |
|
89 by (simp add: dvd_div_mult_self) |
|
90 with `b \<noteq> 0` have "?b \<noteq> 0" by auto |
|
91 from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b" |
|
92 by (simp add: eq_rat dvd_div_mult mult_commute [of a]) |
|
93 from `b \<noteq> 0` have coprime: "coprime ?a ?b" |
|
94 by (auto intro: div_gcd_coprime_int) |
|
95 show C proof (cases "b > 0") |
|
96 case True |
|
97 note assms |
|
98 moreover note q |
|
99 moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) |
|
100 moreover note coprime |
|
101 ultimately show C . |
|
102 next |
|
103 case False |
|
104 note assms |
|
105 moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def) |
|
106 moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) |
|
107 moreover from coprime have "coprime (- ?a) (- ?b)" by simp |
|
108 ultimately show C . |
|
109 qed |
|
110 qed |
|
111 |
|
112 lemma Rat_induct [case_names Fract, induct type: rat]: |
|
113 assumes "\<And>a b. b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> P (Fract a b)" |
|
114 shows "P q" |
|
115 using assms by (cases q) simp |
|
116 |
92 instantiation rat :: comm_ring_1 |
117 instantiation rat :: comm_ring_1 |
93 begin |
118 begin |
94 |
119 |
95 definition |
120 definition |
96 Zero_rat_def [code, code_unfold]: "0 = Fract 0 1" |
121 Zero_rat_def: "0 = Fract 0 1" |
97 |
122 |
98 definition |
123 definition |
99 One_rat_def [code, code_unfold]: "1 = Fract 1 1" |
124 One_rat_def: "1 = Fract 1 1" |
100 |
125 |
101 definition |
126 definition |
102 add_rat_def [code del]: |
127 add_rat_def: |
103 "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
128 "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
104 ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" |
129 ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" |
105 |
130 |
106 lemma add_rat [simp]: |
131 lemma add_rat [simp]: |
107 assumes "b \<noteq> 0" and "d \<noteq> 0" |
132 assumes "b \<noteq> 0" and "d \<noteq> 0" |
228 lemma iszero_rat [simp]: |
253 lemma iszero_rat [simp]: |
229 "iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)" |
254 "iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)" |
230 by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) |
255 by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) |
231 |
256 |
232 lemma Rat_cases_nonzero [case_names Fract 0]: |
257 lemma Rat_cases_nonzero [case_names Fract 0]: |
233 assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> C" |
258 assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" |
234 assumes 0: "q = 0 \<Longrightarrow> C" |
259 assumes 0: "q = 0 \<Longrightarrow> C" |
235 shows C |
260 shows C |
236 proof (cases "q = 0") |
261 proof (cases "q = 0") |
237 case True then show C using 0 by auto |
262 case True then show C using 0 by auto |
238 next |
263 next |
239 case False |
264 case False |
240 then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto |
265 then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto |
241 moreover with False have "0 \<noteq> Fract a b" by simp |
266 moreover with False have "0 \<noteq> Fract a b" by simp |
242 with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) |
267 with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) |
243 with Fract `q = Fract a b` `b \<noteq> 0` show C by auto |
268 with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast |
244 qed |
269 qed |
245 |
270 |
246 subsubsection {* Function @{text normalize} *} |
271 subsubsection {* Function @{text normalize} *} |
247 |
272 |
|
273 lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" |
|
274 proof (cases "b = 0") |
|
275 case True then show ?thesis by (simp add: eq_rat) |
|
276 next |
|
277 case False |
|
278 moreover have "b div gcd a b * gcd a b = b" |
|
279 by (rule dvd_div_mult_self) simp |
|
280 ultimately have "b div gcd a b \<noteq> 0" by auto |
|
281 with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a]) |
|
282 qed |
|
283 |
|
284 definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" where |
|
285 "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) |
|
286 else if snd p = 0 then (0, 1) |
|
287 else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))" |
|
288 |
|
289 lemma normalize_crossproduct: |
|
290 assumes "q \<noteq> 0" "s \<noteq> 0" |
|
291 assumes "normalize (p, q) = normalize (r, s)" |
|
292 shows "p * s = r * q" |
|
293 proof - |
|
294 have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \<Longrightarrow> q * gcd r s = sgn (q * s) * s * gcd p q \<Longrightarrow> p * s = q * r" |
|
295 proof - |
|
296 assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" |
|
297 then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp |
|
298 with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0) |
|
299 qed |
|
300 from assms show ?thesis |
|
301 by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) |
|
302 qed |
|
303 |
|
304 lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" |
|
305 by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse |
|
306 split:split_if_asm) |
|
307 |
|
308 lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0" |
|
309 by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff |
|
310 split:split_if_asm) |
|
311 |
|
312 lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q" |
|
313 by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int |
|
314 split:split_if_asm) |
|
315 |
|
316 lemma normalize_stable [simp]: |
|
317 "q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)" |
|
318 by (simp add: normalize_def) |
|
319 |
|
320 lemma normalize_denom_zero [simp]: |
|
321 "normalize (p, 0) = (0, 1)" |
|
322 by (simp add: normalize_def) |
|
323 |
|
324 lemma normalize_negative [simp]: |
|
325 "q < 0 \<Longrightarrow> normalize (p, q) = normalize (- p, - q)" |
|
326 by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) |
|
327 |
248 text{* |
328 text{* |
249 Decompose a fraction into normalized, i.e. coprime numerator and denominator: |
329 Decompose a fraction into normalized, i.e. coprime numerator and denominator: |
250 *} |
330 *} |
251 |
331 |
252 definition normalize :: "rat \<Rightarrow> int \<times> int" where |
332 definition quotient_of :: "rat \<Rightarrow> int \<times> int" where |
253 "normalize x \<equiv> THE pair. x = Fract (fst pair) (snd pair) & |
333 "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & |
254 snd pair > 0 & gcd (fst pair) (snd pair) = 1" |
334 snd pair > 0 & coprime (fst pair) (snd pair))" |
255 |
335 |
256 declare normalize_def[code del] |
336 lemma quotient_of_unique: |
257 |
337 "\<exists>!p. r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" |
258 lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" |
338 proof (cases r) |
259 proof (cases "a = 0 | b = 0") |
339 case (Fract a b) |
260 case True then show ?thesis by (auto simp add: eq_rat) |
340 then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" by auto |
261 next |
341 then show ?thesis proof (rule ex1I) |
262 let ?c = "gcd a b" |
342 fix p |
263 case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto |
343 obtain c d :: int where p: "p = (c, d)" by (cases p) |
264 then have "?c \<noteq> 0" by simp |
344 assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" |
265 then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat) |
345 with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all |
266 moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" |
346 have "c = a \<and> d = b" |
267 by (simp add: semiring_div_class.mod_div_equality) |
347 proof (cases "a = 0") |
268 moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
348 case True with Fract Fract' show ?thesis by (simp add: eq_rat) |
269 moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
349 next |
270 ultimately show ?thesis |
350 case False |
271 by (simp add: mult_rat [symmetric]) |
351 with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat) |
272 qed |
352 then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto |
273 |
353 with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff) |
274 text{* Proof by Ren\'e Thiemann: *} |
354 with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less) |
275 lemma normalize_code[code]: |
355 from `coprime a b` `coprime c d` have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>" |
276 "normalize (Fract a b) = |
356 by (simp add: coprime_crossproduct_int) |
277 (if b > 0 then (let g = gcd a b in (a div g, b div g)) |
357 with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp |
278 else if b = 0 then (0,1) |
358 then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn) |
279 else (let g = - gcd a b in (a div g, b div g)))" |
359 with sgn * show ?thesis by (auto simp add: sgn_0_0) |
|
360 qed |
|
361 with p show "p = (a, b)" by simp |
|
362 qed |
|
363 qed |
|
364 |
|
365 lemma quotient_of_Fract [code]: |
|
366 "quotient_of (Fract a b) = normalize (a, b)" |
280 proof - |
367 proof - |
281 let ?cond = "% r p. r = Fract (fst p) (snd p) & snd p > 0 & |
368 have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) |
282 gcd (fst p) (snd p) = 1" |
369 by (rule sym) (auto intro: normalize_eq) |
283 show ?thesis |
370 moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) |
284 proof (cases "b = 0") |
371 by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) |
285 case True |
372 moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) |
286 thus ?thesis |
373 by (rule normalize_coprime) simp |
287 proof (simp add: normalize_def) |
374 ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast |
288 show "(THE pair. ?cond (Fract a 0) pair) = (0,1)" |
375 with quotient_of_unique have |
289 proof |
376 "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> coprime (fst p) (snd p)) = normalize (a, b)" |
290 show "?cond (Fract a 0) (0,1)" |
377 by (rule the1_equality) |
291 by (simp add: rat_number_collapse) |
378 then show ?thesis by (simp add: quotient_of_def) |
292 next |
379 qed |
293 fix pair |
380 |
294 assume cond: "?cond (Fract a 0) pair" |
381 lemma quotient_of_number [simp]: |
295 show "pair = (0,1)" |
382 "quotient_of 0 = (0, 1)" |
296 proof (cases pair) |
383 "quotient_of 1 = (1, 1)" |
297 case (Pair den num) |
384 "quotient_of (number_of k) = (number_of k, 1)" |
298 with cond have num: "num > 0" by auto |
385 by (simp_all add: rat_number_expand quotient_of_Fract) |
299 with Pair cond have den: "den = 0" by (simp add: eq_rat) |
386 |
300 show ?thesis |
387 lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" |
301 proof (cases "num = 1", simp add: Pair den) |
388 by (simp add: quotient_of_Fract normalize_eq) |
302 case False |
389 |
303 with num have gr: "num > 1" by auto |
390 lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0" |
304 with den have "gcd den num = num" by auto |
391 by (cases r) (simp add: quotient_of_Fract normalize_denom_pos) |
305 with Pair cond False gr show ?thesis by auto |
392 |
306 qed |
393 lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q" |
307 qed |
394 by (cases r) (simp add: quotient_of_Fract normalize_coprime) |
308 qed |
395 |
309 qed |
396 lemma quotient_of_inject: |
310 next |
397 assumes "quotient_of a = quotient_of b" |
311 { fix a b :: int assume b: "b > 0" |
398 shows "a = b" |
312 hence b0: "b \<noteq> 0" and "b >= 0" by auto |
399 proof - |
313 let ?g = "gcd a b" |
400 obtain p q r s where a: "a = Fract p q" |
314 from b0 have g0: "?g \<noteq> 0" by auto |
401 and b: "b = Fract r s" |
315 then have gp: "?g > 0" by simp |
402 and "q > 0" and "s > 0" by (cases a, cases b) |
316 then have gs: "?g <= b" by (metis b gcd_le2_int) |
403 with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) |
317 from gcd_dvd1_int[of a b] obtain a' where a': "a = ?g * a'" |
404 qed |
318 unfolding dvd_def by auto |
405 |
319 from gcd_dvd2_int[of a b] obtain b' where b': "b = ?g * b'" |
406 lemma quotient_of_inject_eq: |
320 unfolding dvd_def by auto |
407 "quotient_of a = quotient_of b \<longleftrightarrow> a = b" |
321 hence b'2: "b' * ?g = b" by (simp add: ring_simps) |
408 by (auto simp add: quotient_of_inject) |
322 with b0 have b'0: "b' \<noteq> 0" by auto |
|
323 from b b' zero_less_mult_iff[of ?g b'] gp have b'p: "b' > 0" by arith |
|
324 have "normalize (Fract a b) = (a div ?g, b div ?g)" |
|
325 proof (simp add: normalize_def) |
|
326 show "(THE pair. ?cond (Fract a b) pair) = (a div ?g, b div ?g)" |
|
327 proof |
|
328 have "1 = b div b" using b0 by auto |
|
329 also have "\<dots> <= b div ?g" by (rule zdiv_mono2[OF `b >= 0` gp gs]) |
|
330 finally have div0: "b div ?g > 0" by simp |
|
331 show "?cond (Fract a b) (a div ?g, b div ?g)" |
|
332 by (simp add: b0 Fract_norm div_gcd_coprime_int div0) |
|
333 next |
|
334 fix pair assume cond: "?cond (Fract a b) pair" |
|
335 show "pair = (a div ?g, b div ?g)" |
|
336 proof (cases pair) |
|
337 case (Pair den num) |
|
338 with cond |
|
339 have num: "num > 0" and num0: "num \<noteq> 0" and gcd: "gcd den num = 1" |
|
340 by auto |
|
341 obtain g where g: "g = ?g" by auto |
|
342 with gp have gg0: "g > 0" by auto |
|
343 from cond Pair eq_rat(1)[OF b0 num0] |
|
344 have eq: "a * num = den * b" by auto |
|
345 hence "a' * g * num = den * g * b'" |
|
346 using a'[simplified g[symmetric]] b'[simplified g[symmetric]] |
|
347 by simp |
|
348 hence "a' * num * g = b' * den * g" by (simp add: algebra_simps) |
|
349 hence eq2: "a' * num = b' * den" using gg0 by auto |
|
350 have "a div ?g = ?g * a' div ?g" using a' by force |
|
351 hence adiv: "a div ?g = a'" using g0 by auto |
|
352 have "b div ?g = ?g * b' div ?g" using b' by force |
|
353 hence bdiv: "b div ?g = b'" using g0 by auto |
|
354 from div_gcd_coprime_int[of a b] b0 |
|
355 have "gcd (a div ?g) (b div ?g) = 1" by auto |
|
356 with adiv bdiv have gcd2: "gcd a' b' = 1" by auto |
|
357 from gcd have gcd3: "gcd num den = 1" |
|
358 by (simp add: gcd_commute_int[of den num]) |
|
359 from gcd2 have gcd4: "gcd b' a' = 1" |
|
360 by (simp add: gcd_commute_int[of a' b']) |
|
361 have one: "num dvd b'" |
|
362 by (metis coprime_dvd_mult_int[OF gcd3] dvd_triv_right eq2) |
|
363 have two: "b' dvd num" |
|
364 by (metis coprime_dvd_mult_int[OF gcd4] dvd_triv_left eq2 zmult_commute) |
|
365 from zdvd_antisym_abs[OF one two] b'p num |
|
366 have numb': "num = b'" by auto |
|
367 with eq2 b'0 have "a' = den" by auto |
|
368 with numb' adiv bdiv Pair show ?thesis by simp |
|
369 qed |
|
370 qed |
|
371 qed |
|
372 } |
|
373 note main = this |
|
374 assume "b \<noteq> 0" |
|
375 hence "b > 0 | b < 0" by arith |
|
376 thus ?thesis |
|
377 proof |
|
378 assume b: "b > 0" thus ?thesis by (simp add: Let_def main[OF b]) |
|
379 next |
|
380 assume b: "b < 0" |
|
381 thus ?thesis |
|
382 by(simp add:main Let_def minus_rat_cancel[of a b, symmetric] |
|
383 zdiv_zminus2 del:minus_rat_cancel) |
|
384 qed |
|
385 qed |
|
386 qed |
|
387 |
|
388 lemma normalize_id: "normalize (Fract a b) = (p,q) \<Longrightarrow> Fract p q = Fract a b" |
|
389 by(auto simp add: normalize_code Let_def Fract_norm dvd_div_neg rat_number_collapse |
|
390 split:split_if_asm) |
|
391 |
|
392 lemma normalize_denom_pos: "normalize (Fract a b) = (p,q) \<Longrightarrow> q > 0" |
|
393 by(auto simp add: normalize_code Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff |
|
394 split:split_if_asm) |
|
395 |
|
396 lemma normalize_coprime: "normalize (Fract a b) = (p,q) \<Longrightarrow> coprime p q" |
|
397 by(auto simp add: normalize_code Let_def dvd_div_neg div_gcd_coprime_int |
|
398 split:split_if_asm) |
|
399 |
409 |
400 |
410 |
401 subsubsection {* The field of rational numbers *} |
411 subsubsection {* The field of rational numbers *} |
402 |
412 |
403 instantiation rat :: "{field, division_by_zero}" |
413 instantiation rat :: "{field, division_by_zero}" |
404 begin |
414 begin |
405 |
415 |
406 definition |
416 definition |
407 inverse_rat_def [code del]: |
417 inverse_rat_def: |
408 "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. |
418 "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. |
409 ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" |
419 ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" |
410 |
420 |
411 lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" |
421 lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" |
412 proof - |
422 proof - |
1003 by (rule Rats_cases) auto |
1013 by (rule Rats_cases) auto |
1004 |
1014 |
1005 |
1015 |
1006 subsection {* Implementation of rational numbers as pairs of integers *} |
1016 subsection {* Implementation of rational numbers as pairs of integers *} |
1007 |
1017 |
1008 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where |
1018 definition Frct :: "int \<times> int \<Rightarrow> rat" where |
1009 [simp, code del]: "Fract_norm a b = Fract a b" |
1019 [simp]: "Frct p = Fract (fst p) (snd p)" |
1010 |
1020 |
1011 lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = gcd a b in |
1021 code_abstype Frct quotient_of |
1012 if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))" |
1022 proof (rule eq_reflection) |
1013 by (simp add: eq_rat Zero_rat_def Let_def Fract_norm) |
1023 show "Frct (quotient_of x) = x" by (cases x) (auto intro: quotient_of_eq) |
1014 |
1024 qed |
1015 lemma [code]: |
1025 |
1016 "of_rat (Fract a b) = (if b \<noteq> 0 then of_int a / of_int b else 0)" |
1026 lemma Frct_code_post [code_post]: |
1017 by (cases "b = 0") (simp_all add: rat_number_collapse of_rat_rat) |
1027 "Frct (0, k) = 0" |
|
1028 "Frct (k, 0) = 0" |
|
1029 "Frct (1, 1) = 1" |
|
1030 "Frct (number_of k, 1) = number_of k" |
|
1031 "Frct (1, number_of k) = 1 / number_of k" |
|
1032 "Frct (number_of k, number_of l) = number_of k / number_of l" |
|
1033 by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of) |
|
1034 |
|
1035 declare quotient_of_Fract [code abstract] |
|
1036 |
|
1037 lemma rat_zero_code [code abstract]: |
|
1038 "quotient_of 0 = (0, 1)" |
|
1039 by (simp add: Zero_rat_def quotient_of_Fract normalize_def) |
|
1040 |
|
1041 lemma rat_one_code [code abstract]: |
|
1042 "quotient_of 1 = (1, 1)" |
|
1043 by (simp add: One_rat_def quotient_of_Fract normalize_def) |
|
1044 |
|
1045 lemma rat_plus_code [code abstract]: |
|
1046 "quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
|
1047 in normalize (a * d + b * c, c * d))" |
|
1048 by (cases p, cases q) (simp add: quotient_of_Fract) |
|
1049 |
|
1050 lemma rat_uminus_code [code abstract]: |
|
1051 "quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))" |
|
1052 by (cases p) (simp add: quotient_of_Fract) |
|
1053 |
|
1054 lemma rat_minus_code [code abstract]: |
|
1055 "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
|
1056 in normalize (a * d - b * c, c * d))" |
|
1057 by (cases p, cases q) (simp add: quotient_of_Fract) |
|
1058 |
|
1059 lemma rat_times_code [code abstract]: |
|
1060 "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
|
1061 in normalize (a * b, c * d))" |
|
1062 by (cases p, cases q) (simp add: quotient_of_Fract) |
|
1063 |
|
1064 lemma rat_inverse_code [code abstract]: |
|
1065 "quotient_of (inverse p) = (let (a, b) = quotient_of p |
|
1066 in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))" |
|
1067 proof (cases p) |
|
1068 case (Fract a b) then show ?thesis |
|
1069 by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute) |
|
1070 qed |
|
1071 |
|
1072 lemma rat_divide_code [code abstract]: |
|
1073 "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
|
1074 in normalize (a * d, c * b))" |
|
1075 by (cases p, cases q) (simp add: quotient_of_Fract) |
|
1076 |
|
1077 lemma rat_abs_code [code abstract]: |
|
1078 "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))" |
|
1079 by (cases p) (simp add: quotient_of_Fract) |
|
1080 |
|
1081 lemma rat_sgn_code [code abstract]: |
|
1082 "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" |
|
1083 proof (cases p) |
|
1084 case (Fract a b) then show ?thesis |
|
1085 by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) |
|
1086 qed |
1018 |
1087 |
1019 instantiation rat :: eq |
1088 instantiation rat :: eq |
1020 begin |
1089 begin |
1021 |
1090 |
1022 definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0" |
1091 definition [code]: |
1023 |
1092 "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b" |
1024 instance by default (simp add: eq_rat_def) |
1093 |
1025 |
1094 instance proof |
1026 lemma rat_eq_code [code]: |
1095 qed (simp add: eq_rat_def quotient_of_inject_eq) |
1027 "eq_class.eq (Fract a b) (Fract c d) \<longleftrightarrow> (if b = 0 |
|
1028 then c = 0 \<or> d = 0 |
|
1029 else if d = 0 |
|
1030 then a = 0 \<or> b = 0 |
|
1031 else a * d = b * c)" |
|
1032 by (auto simp add: eq eq_rat) |
|
1033 |
1096 |
1034 lemma rat_eq_refl [code nbe]: |
1097 lemma rat_eq_refl [code nbe]: |
1035 "eq_class.eq (r::rat) r \<longleftrightarrow> True" |
1098 "eq_class.eq (r::rat) r \<longleftrightarrow> True" |
1036 by (rule HOL.eq_refl) |
1099 by (rule HOL.eq_refl) |
1037 |
1100 |
1038 end |
1101 end |
1039 |
1102 |
1040 lemma le_rat': |
|
1041 assumes "b \<noteq> 0" |
|
1042 and "d \<noteq> 0" |
|
1043 shows "Fract a b \<le> Fract c d \<longleftrightarrow> a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d" |
|
1044 proof - |
|
1045 have abs_sgn: "\<And>k::int. \<bar>k\<bar> = k * sgn k" unfolding abs_if sgn_if by simp |
|
1046 have "a * d * (b * d) \<le> c * b * (b * d) \<longleftrightarrow> a * d * (sgn b * sgn d) \<le> c * b * (sgn b * sgn d)" |
|
1047 proof (cases "b * d > 0") |
|
1048 case True |
|
1049 moreover from True have "sgn b * sgn d = 1" |
|
1050 by (simp add: sgn_times [symmetric] sgn_1_pos) |
|
1051 ultimately show ?thesis by (simp add: mult_le_cancel_right) |
|
1052 next |
|
1053 case False with assms have "b * d < 0" by (simp add: less_le) |
|
1054 moreover from this have "sgn b * sgn d = - 1" |
|
1055 by (simp only: sgn_times [symmetric] sgn_1_neg) |
|
1056 ultimately show ?thesis by (simp add: mult_le_cancel_right) |
|
1057 qed |
|
1058 also have "\<dots> \<longleftrightarrow> a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d" |
|
1059 by (simp add: abs_sgn mult_ac) |
|
1060 finally show ?thesis using assms by simp |
|
1061 qed |
|
1062 |
|
1063 lemma less_rat': |
|
1064 assumes "b \<noteq> 0" |
|
1065 and "d \<noteq> 0" |
|
1066 shows "Fract a b < Fract c d \<longleftrightarrow> a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d" |
|
1067 proof - |
|
1068 have abs_sgn: "\<And>k::int. \<bar>k\<bar> = k * sgn k" unfolding abs_if sgn_if by simp |
|
1069 have "a * d * (b * d) < c * b * (b * d) \<longleftrightarrow> a * d * (sgn b * sgn d) < c * b * (sgn b * sgn d)" |
|
1070 proof (cases "b * d > 0") |
|
1071 case True |
|
1072 moreover from True have "sgn b * sgn d = 1" |
|
1073 by (simp add: sgn_times [symmetric] sgn_1_pos) |
|
1074 ultimately show ?thesis by (simp add: mult_less_cancel_right) |
|
1075 next |
|
1076 case False with assms have "b * d < 0" by (simp add: less_le) |
|
1077 moreover from this have "sgn b * sgn d = - 1" |
|
1078 by (simp only: sgn_times [symmetric] sgn_1_neg) |
|
1079 ultimately show ?thesis by (simp add: mult_less_cancel_right) |
|
1080 qed |
|
1081 also have "\<dots> \<longleftrightarrow> a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d" |
|
1082 by (simp add: abs_sgn mult_ac) |
|
1083 finally show ?thesis using assms by simp |
|
1084 qed |
|
1085 |
|
1086 lemma rat_le_eq_code [code]: |
|
1087 "Fract a b < Fract c d \<longleftrightarrow> (if b = 0 |
|
1088 then sgn c * sgn d > 0 |
|
1089 else if d = 0 |
|
1090 then sgn a * sgn b < 0 |
|
1091 else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)" |
|
1092 by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat) |
|
1093 |
|
1094 lemma rat_less_eq_code [code]: |
1103 lemma rat_less_eq_code [code]: |
1095 "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0 |
1104 "p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)" |
1096 then sgn c * sgn d \<ge> 0 |
1105 by (cases p, cases q) (simp add: quotient_of_Fract times.commute) |
1097 else if d = 0 |
1106 |
1098 then sgn a * sgn b \<le> 0 |
1107 lemma rat_less_code [code]: |
1099 else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)" |
1108 "p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" |
1100 by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat) |
1109 by (cases p, cases q) (simp add: quotient_of_Fract times.commute) |
1101 (auto simp add: le_less not_less sgn_0_0) |
1110 |
1102 |
1111 lemma [code]: |
1103 |
1112 "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" |
1104 lemma rat_plus_code [code]: |
1113 by (cases p) (simp add: quotient_of_Fract of_rat_rat) |
1105 "Fract a b + Fract c d = (if b = 0 |
|
1106 then Fract c d |
|
1107 else if d = 0 |
|
1108 then Fract a b |
|
1109 else Fract_norm (a * d + c * b) (b * d))" |
|
1110 by (simp add: eq_rat, simp add: Zero_rat_def) |
|
1111 |
|
1112 lemma rat_times_code [code]: |
|
1113 "Fract a b * Fract c d = Fract_norm (a * c) (b * d)" |
|
1114 by simp |
|
1115 |
|
1116 lemma rat_minus_code [code]: |
|
1117 "Fract a b - Fract c d = (if b = 0 |
|
1118 then Fract (- c) d |
|
1119 else if d = 0 |
|
1120 then Fract a b |
|
1121 else Fract_norm (a * d - c * b) (b * d))" |
|
1122 by (simp add: eq_rat, simp add: Zero_rat_def) |
|
1123 |
|
1124 lemma rat_inverse_code [code]: |
|
1125 "inverse (Fract a b) = (if b = 0 then Fract 1 0 |
|
1126 else if a < 0 then Fract (- b) (- a) |
|
1127 else Fract b a)" |
|
1128 by (simp add: eq_rat) |
|
1129 |
|
1130 lemma rat_divide_code [code]: |
|
1131 "Fract a b / Fract c d = Fract_norm (a * d) (b * c)" |
|
1132 by simp |
|
1133 |
1114 |
1134 definition (in term_syntax) |
1115 definition (in term_syntax) |
1135 valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1116 valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1136 [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l" |
1117 [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l" |
1137 |
1118 |