25 instance erat :: times .. |
25 instance erat :: times .. |
26 instance erat :: inverse .. |
26 instance erat :: inverse .. |
27 instance erat :: ord .. |
27 instance erat :: ord .. |
28 |
28 |
29 definition |
29 definition |
30 norm :: "erat \<Rightarrow> erat" |
30 norm :: "erat \<Rightarrow> erat" where |
31 norm_def: "norm r = (case r of (Rat a p q) \<Rightarrow> |
31 "norm r = (case r of (Rat a p q) \<Rightarrow> |
32 if p = 0 then Rat True 0 1 |
32 if p = 0 then Rat True 0 1 |
33 else |
33 else |
34 let |
34 let |
35 absp = abs p |
35 absp = abs p |
36 in let |
36 in let |
37 m = zgcd (absp, q) |
37 m = zgcd (absp, q) |
38 in Rat (a = (0 <= p)) (absp div m) (q div m))" |
38 in Rat (a = (0 <= p)) (absp div m) (q div m))" |
39 common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" |
39 |
40 common_def: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
40 definition |
|
41 common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" where |
|
42 "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
41 let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
43 let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
42 in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
44 in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
43 of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" |
45 |
44 of_quotient_def: "of_quotient a b = |
46 definition |
45 norm (Rat True a b)" |
47 of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where |
46 of_rat :: "rat \<Rightarrow> erat" |
48 "of_quotient a b = norm (Rat True a b)" |
47 of_rat_def: "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)" |
49 |
48 to_rat :: "erat \<Rightarrow> rat" |
50 definition |
49 to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow> |
51 of_rat :: "rat \<Rightarrow> erat" where |
|
52 "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)" |
|
53 |
|
54 definition |
|
55 to_rat :: "erat \<Rightarrow> rat" where |
|
56 "to_rat r = (case r of (Rat a p q) \<Rightarrow> |
50 if a then Fract p q else Fract (uminus p) q)" |
57 if a then Fract p q else Fract (uminus p) q)" |
51 eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool" |
58 |
|
59 definition |
|
60 eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool" where |
52 "eq_erat r s = (norm r = norm s)" |
61 "eq_erat r s = (norm r = norm s)" |
53 |
62 |
54 axiomatization |
63 axiomatization |
55 div_zero :: erat |
64 div_zero :: erat |
56 |
65 |