|
1 (* Title: HOL/Library/Executable_Rat.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Executable implementation of rational numbers in HOL *} |
|
7 |
|
8 theory Executable_Rat |
|
9 imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes" |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Actually \emph{nothing} is proved about this implementation. |
|
14 *} |
|
15 |
|
16 subsection {* Representation and operations of executable rationals *} |
|
17 |
|
18 datatype erat = Rat bool nat nat |
|
19 |
|
20 axiomatization |
|
21 div_zero :: erat |
|
22 |
|
23 fun |
|
24 common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where |
|
25 "common (p1, q1) (p2, q2) = ( |
|
26 let |
|
27 q' = q1 * q2 div gcd (q1, q2) |
|
28 in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
|
29 |
|
30 definition |
|
31 minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where |
|
32 "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))" |
|
33 |
|
34 fun |
|
35 add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where |
|
36 "add_sign (True, n) (True, m) = (True, n + m)" |
|
37 | "add_sign (False, n) (False, m) = (False, n + m)" |
|
38 | "add_sign (True, n) (False, m) = minus_sign n m" |
|
39 | "add_sign (False, n) (True, m) = minus_sign m n" |
|
40 |
|
41 definition |
|
42 erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where |
|
43 "erat_of_quotient k1 k2 = ( |
|
44 let |
|
45 l1 = nat (abs k1); |
|
46 l2 = nat (abs k2); |
|
47 m = gcd (l1, l2) |
|
48 in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))" |
|
49 |
|
50 instance erat :: zero |
|
51 zero_rat_def: "0 \<equiv> Rat True 0 1" .. |
|
52 |
|
53 instance erat :: one |
|
54 one_rat_def: "1 \<equiv> Rat True 1 1" .. |
|
55 |
|
56 instance erat :: plus |
|
57 add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
58 let |
|
59 ((r1, r2), den) = common (p1, q1) (p2, q2); |
|
60 (sign, num) = add_sign (a1, r1) (a2, r2) |
|
61 in Rat sign num den" .. |
|
62 |
|
63 instance erat :: minus |
|
64 uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow> |
|
65 if p = 0 then Rat True 0 1 |
|
66 else Rat (\<not> a) p q" .. |
|
67 |
|
68 instance erat :: times |
|
69 times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
70 let |
|
71 p = p1 * p2; |
|
72 q = q1 * q2; |
|
73 m = gcd (p, q) |
|
74 in Rat (a1 = a2) (p div m) (q div m)" .. |
|
75 |
|
76 instance erat :: inverse |
|
77 inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow> |
|
78 if p = 0 then div_zero |
|
79 else Rat a q p" .. |
|
80 |
|
81 instance erat :: ord |
|
82 le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow> |
|
83 (\<not> a1 \<and> a2) \<or> |
|
84 (\<not> (a1 \<and> \<not> a2) \<and> |
|
85 (let |
|
86 ((r1, r2), dummy) = common (p1, q1) (p2, q2) |
|
87 in if a1 then r1 \<le> r2 else r2 \<le> r1))" .. |
|
88 |
|
89 |
|
90 subsection {* Code generator setup *} |
|
91 |
|
92 subsubsection {* code lemmas *} |
|
93 |
|
94 lemma number_of_rat [code unfold]: |
|
95 "(number_of k \<Colon> rat) = Fract k 1" |
|
96 unfolding Fract_of_int_eq rat_number_of_def by simp |
|
97 |
|
98 lemma rat_minus [code func]: |
|
99 "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus .. |
|
100 |
|
101 lemma rat_divide [code func]: |
|
102 "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse .. |
|
103 |
|
104 instance rat :: eq .. |
|
105 |
|
106 subsubsection {* names *} |
|
107 |
|
108 code_modulename SML |
|
109 Executable_Rat Rational |
|
110 |
|
111 code_modulename OCaml |
|
112 Executable_Rat Rational |
|
113 |
|
114 code_modulename Haskell |
|
115 Executable_Rat Rational |
|
116 |
|
117 subsubsection {* rat as abstype *} |
|
118 |
|
119 code_const div_zero |
|
120 (SML "raise/ Fail/ \"Division by zero\"") |
|
121 (OCaml "failwith \"Division by zero\"") |
|
122 (Haskell "error/ \"Division by zero\"") |
|
123 |
|
124 code_abstype rat erat where |
|
125 Fract \<equiv> erat_of_quotient |
|
126 "0 \<Colon> rat" \<equiv> "0 \<Colon> erat" |
|
127 "1 \<Colon> rat" \<equiv> "1 \<Colon> erat" |
|
128 "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" |
|
129 "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat" |
|
130 "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" |
|
131 "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat" |
|
132 "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" |
|
133 "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" |
|
134 |
|
135 types_code |
|
136 rat ("{*erat*}") |
|
137 |
|
138 consts_code |
|
139 div_zero ("(raise/ (Fail/ \"Division by zero\"))") |
|
140 Fract ("({*erat_of_quotient*} (_) (_))") |
|
141 "0 \<Colon> rat" ("({*Rat True 0 1*})") |
|
142 "1 \<Colon> rat" ("({*Rat True 1 1*})") |
|
143 "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))") |
|
144 "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))") |
|
145 "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))") |
|
146 "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))") |
|
147 "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))") |
|
148 "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))") |
|
149 |
|
150 end |