author | haftmann |
Mon, 25 Sep 2006 17:04:18 +0200 | |
changeset 20701 | 17a625996bb0 |
parent 20597 | 65fe827aa595 |
child 20713 | 823967ef47f1 |
permissions | -rw-r--r-- |
19039 | 1 |
(* Title: HOL/Library/ExecutableRat.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Executable implementation of rational numbers in HOL *} |
|
7 |
||
8 |
theory ExecutableRat |
|
9 |
imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes" |
|
10 |
begin |
|
11 |
||
12 |
text {* |
|
13 |
Actually nothing is proved about the implementation. |
|
14 |
*} |
|
15 |
||
19791 | 16 |
|
17 |
section {* HOL definitions *} |
|
18 |
||
19039 | 19 |
datatype erat = Rat bool int int |
20 |
||
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
21 |
instance erat :: zero .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
22 |
instance erat :: one .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
23 |
instance erat :: plus .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
24 |
instance erat :: minus .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
25 |
instance erat :: times .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
26 |
instance erat :: inverse .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
27 |
instance erat :: ord .. |
19039 | 28 |
|
19609 | 29 |
definition |
19039 | 30 |
norm :: "erat \<Rightarrow> erat" |
19791 | 31 |
norm_def: "norm r = (case r of (Rat a p q) \<Rightarrow> |
19039 | 32 |
if p = 0 then Rat True 0 1 |
33 |
else |
|
34 |
let |
|
35 |
absp = abs p |
|
36 |
in let |
|
37 |
m = zgcd (absp, q) |
|
19609 | 38 |
in Rat (a = (0 <= p)) (absp div m) (q div m))" |
39 |
common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" |
|
19791 | 40 |
common_def: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
19039 | 41 |
let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
19609 | 42 |
in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
20701 | 43 |
of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" |
44 |
of_quotient_def: "of_quotient a b = |
|
45 |
norm (Rat True a b)" |
|
19609 | 46 |
of_rat :: "rat \<Rightarrow> erat" |
20701 | 47 |
of_rat_def: "of_rat r = split of_quotient (SOME s. s : Rep_Rat r)" |
19609 | 48 |
to_rat :: "erat \<Rightarrow> rat" |
19791 | 49 |
to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow> |
19609 | 50 |
if a then Fract p q else Fract (uminus p) q)" |
20597 | 51 |
eq_erat :: "erat \<Rightarrow> erat \<Rightarrow> bool" |
52 |
"eq_erat r s = (norm r = norm s)" |
|
19039 | 53 |
|
20701 | 54 |
axiomatization |
55 |
div_zero :: erat |
|
56 |
||
19039 | 57 |
defs (overloaded) |
19791 | 58 |
zero_rat_def: "0 == Rat True 0 1" |
59 |
one_rat_def: "1 == Rat True 1 1" |
|
60 |
add_rat_def: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
19039 | 61 |
let |
62 |
((r1, r2), den) = common ((p1, q1), (p2, q2)) |
|
63 |
in let |
|
64 |
num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2) |
|
65 |
in norm (Rat True num den)" |
|
19791 | 66 |
uminus_rat_def: "- r == case r of Rat a p q \<Rightarrow> |
19039 | 67 |
if p = 0 then Rat a p q |
68 |
else Rat (\<not> a) p q" |
|
19791 | 69 |
times_rat_def: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
19039 | 70 |
norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))" |
19791 | 71 |
inverse_rat_def: "inverse r == case r of Rat a p q \<Rightarrow> |
20701 | 72 |
if p = 0 then div_zero |
19039 | 73 |
else Rat a q p" |
19791 | 74 |
le_rat_def: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
19039 | 75 |
(\<not> a1 \<and> a2) \<or> |
76 |
(\<not> (a1 \<and> \<not> a2) \<and> |
|
77 |
(let |
|
78 |
((r1, r2), dummy) = common ((p1, q1), (p2, q2)) |
|
79 |
in if a1 then r1 <= r2 else r2 <= r1))" |
|
80 |
||
19791 | 81 |
|
20701 | 82 |
section {* code lemmas *} |
83 |
||
84 |
lemma |
|
85 |
number_of_rat [code unfold]: "(number_of k \<Colon> rat) \<equiv> Fract k 1" |
|
86 |
unfolding Fract_of_int_eq rat_number_of_def by simp |
|
87 |
||
88 |
instance rat :: eq .. |
|
89 |
||
90 |
||
91 |
section {* code names *} |
|
92 |
||
93 |
code_typename |
|
94 |
erat "Rational.erat" |
|
95 |
||
96 |
code_constname |
|
97 |
Rat "Rational.rat" |
|
98 |
erat_case "Rational.erat_case" |
|
99 |
norm "Rational.norm" |
|
100 |
common "Rational.common" |
|
101 |
of_quotient "Rational.of_quotient" |
|
102 |
of_rat "Rational.of_rat" |
|
103 |
to_rat "Rational.to_rat" |
|
104 |
eq_erat "Rational.eq_erat" |
|
105 |
div_zero "Rational.div_zero" |
|
106 |
"0\<Colon>erat" "Rational.erat_zero" |
|
107 |
"1\<Colon>erat" "Rational.erat_one" |
|
108 |
"op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_plus" |
|
109 |
"uminus \<Colon> erat \<Rightarrow> erat" "Rational.erat_uminus" |
|
110 |
"op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_times" |
|
111 |
"inverse \<Colon> erat \<Rightarrow> erat" "Rational.erat_inverse" |
|
112 |
"op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_le" |
|
113 |
"OperationalEquality.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq" |
|
114 |
||
115 |
||
19791 | 116 |
section {* type serializations *} |
117 |
||
118 |
types_code |
|
119 |
rat ("{*erat*}") |
|
120 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
121 |
code_gen Rat |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
122 |
(SML) (Haskell) |
19889 | 123 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
124 |
code_type rat |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
125 |
(SML "{*erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
126 |
(Haskell "{*erat*}") |
19039 | 127 |
|
19791 | 128 |
|
129 |
section {* const serializations *} |
|
130 |
||
131 |
consts_code |
|
20701 | 132 |
div_zero ("raise/ (Fail/ \"non-defined rational number\")") |
19791 | 133 |
Fract ("{*of_quotient*}") |
134 |
0 :: rat ("{*0::erat*}") |
|
135 |
1 :: rat ("{*1::erat*}") |
|
136 |
HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
137 |
uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}") |
|
138 |
HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
139 |
inverse :: "rat \<Rightarrow> rat" ("{*inverse :: erat \<Rightarrow> erat*}") |
|
140 |
divide :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
|
141 |
Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
|
142 |
"op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}") |
|
143 |
||
20701 | 144 |
code_const div_zero |
145 |
(SML "raise/ (Fail/ \"Division by zero\")") |
|
146 |
(Haskell "error/ \"Division by zero\"") |
|
19889 | 147 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
148 |
code_gen |
19889 | 149 |
of_quotient |
150 |
"0::erat" |
|
151 |
"1::erat" |
|
152 |
"op + :: erat \<Rightarrow> erat \<Rightarrow> erat" |
|
153 |
"uminus :: erat \<Rightarrow> erat" |
|
154 |
"op * :: erat \<Rightarrow> erat \<Rightarrow> erat" |
|
155 |
"inverse :: erat \<Rightarrow> erat" |
|
156 |
"op <= :: erat \<Rightarrow> erat \<Rightarrow> bool" |
|
20597 | 157 |
eq_erat |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
158 |
(SML) (Haskell) |
19889 | 159 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
160 |
code_const Fract |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
161 |
(SML "{*of_quotient*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
162 |
(Haskell "{*of_quotient*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
163 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
164 |
code_const "0 :: rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
165 |
(SML "{*0::erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
166 |
(Haskell "{*1::erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
167 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
168 |
code_const "1 :: rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
169 |
(SML "{*1::erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
170 |
(Haskell "{*1::erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
171 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
172 |
code_const "op + :: rat \<Rightarrow> rat \<Rightarrow> rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
173 |
(SML "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
174 |
(Haskell "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
175 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
176 |
code_const "uminus :: rat \<Rightarrow> rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
177 |
(SML "{*uminus :: erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
178 |
(Haskell "{*uminus :: erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
179 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
180 |
code_const "op * :: rat \<Rightarrow> rat \<Rightarrow> rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
181 |
(SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
182 |
(Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
183 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
184 |
code_const "inverse :: rat \<Rightarrow> rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
185 |
(SML "{*inverse :: erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
186 |
(Haskell "{*inverse :: erat \<Rightarrow> erat*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
187 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
188 |
code_const "divide :: rat \<Rightarrow> rat \<Rightarrow> rat" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
189 |
(SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
190 |
(Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
191 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
192 |
code_const "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
193 |
(SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
194 |
(Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
19889
diff
changeset
|
195 |
|
20597 | 196 |
code_const "OperationalEquality.eq :: rat \<Rightarrow> rat \<Rightarrow> bool" |
197 |
(SML "{*eq_erat*}") |
|
198 |
(Haskell "{*eq_erat*}") |
|
199 |
||
200 |
code_gen (SML -) |
|
19039 | 201 |
|
202 |
end |