21 instance erat :: minus .. |
21 instance erat :: minus .. |
22 instance erat :: times .. |
22 instance erat :: times .. |
23 instance erat :: inverse .. |
23 instance erat :: inverse .. |
24 instance erat :: ord .. |
24 instance erat :: ord .. |
25 |
25 |
26 consts |
26 definition |
27 norm :: "erat \<Rightarrow> erat" |
27 norm :: "erat \<Rightarrow> erat" |
28 common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" |
28 norm_def [simp]: "norm r = (case r of (Rat a p q) \<Rightarrow> |
29 of_quotient :: "int * int \<Rightarrow> erat" |
|
30 of_rat :: "rat \<Rightarrow> erat" |
|
31 to_rat :: "erat \<Rightarrow> rat" |
|
32 |
|
33 defs |
|
34 norm_def [simp]: "norm r == case r of (Rat a p q) \<Rightarrow> |
|
35 if p = 0 then Rat True 0 1 |
29 if p = 0 then Rat True 0 1 |
36 else |
30 else |
37 let |
31 let |
38 absp = abs p |
32 absp = abs p |
39 in let |
33 in let |
40 m = zgcd (absp, q) |
34 m = zgcd (absp, q) |
41 in Rat (a = (0 <= p)) (absp div m) (q div m)" |
35 in Rat (a = (0 <= p)) (absp div m) (q div m))" |
42 common_def [simp]: "common r == case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
36 common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" |
|
37 common_def [simp]: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
43 let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
38 let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
44 in ((p1 * (q' div q1), p2 * (q' div q2)), q')" |
39 in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
45 of_quotient_def [simp]: "of_quotient r == case r of (a, b) \<Rightarrow> |
40 of_quotient :: "int * int \<Rightarrow> erat" |
46 norm (Rat True a b)" |
41 of_quotient_def [simp]: "of_quotient r = (case r of (a, b) \<Rightarrow> |
47 of_rat_def [simp]: "of_rat r == of_quotient (THE s. s : Rep_Rat r)" |
42 norm (Rat True a b))" |
48 to_rat_def [simp]: "to_rat r == case r of (Rat a p q) \<Rightarrow> |
43 of_rat :: "rat \<Rightarrow> erat" |
49 if a then Fract p q else Fract (uminus p) q" |
44 of_rat_def [simp]: "of_rat r = of_quotient (THE s. s : Rep_Rat r)" |
50 |
45 to_rat :: "erat \<Rightarrow> rat" |
51 consts |
46 to_rat_def [simp]: "to_rat r = (case r of (Rat a p q) \<Rightarrow> |
52 zero :: erat |
47 if a then Fract p q else Fract (uminus p) q)" |
53 one :: erat |
|
54 add :: "erat \<Rightarrow> erat \<Rightarrow> erat" |
|
55 neg :: "erat \<Rightarrow> erat" |
|
56 mult :: "erat \<Rightarrow> erat \<Rightarrow> erat" |
|
57 inv :: "erat \<Rightarrow> erat" |
|
58 le :: "erat \<Rightarrow> erat \<Rightarrow> bool" |
|
59 |
48 |
60 defs (overloaded) |
49 defs (overloaded) |
61 zero_rat_def [simp]: "0 == Rat False 0 1" |
50 zero_rat_def [simp]: "0 == Rat False 0 1" |
62 one_rat_def [simp]: "1 == Rat False 1 1" |
51 one_rat_def [simp]: "1 == Rat False 1 1" |
63 add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
52 add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |