author | haftmann |
Tue, 06 Jun 2006 15:02:55 +0200 | |
changeset 19791 | ab326de16ad5 |
parent 19609 | a677ac8c9b10 |
child 19889 | 2202a5648897 |
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'))" |
43 |
of_quotient :: "int * int \<Rightarrow> erat" |
|
19791 | 44 |
of_quotient_def: "of_quotient r = (case r of (a, b) \<Rightarrow> |
19609 | 45 |
norm (Rat True a b))" |
46 |
of_rat :: "rat \<Rightarrow> erat" |
|
19791 | 47 |
of_rat_def: "of_rat r = 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)" |
19791 | 51 |
eq_rat :: "erat \<Rightarrow> erat \<Rightarrow> bool" |
52 |
"eq_rat r s = (norm r = norm s)" |
|
19039 | 53 |
|
54 |
defs (overloaded) |
|
19791 | 55 |
zero_rat_def: "0 == Rat True 0 1" |
56 |
one_rat_def: "1 == Rat True 1 1" |
|
57 |
add_rat_def: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
19039 | 58 |
let |
59 |
((r1, r2), den) = common ((p1, q1), (p2, q2)) |
|
60 |
in let |
|
61 |
num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2) |
|
62 |
in norm (Rat True num den)" |
|
19791 | 63 |
uminus_rat_def: "- r == case r of Rat a p q \<Rightarrow> |
19039 | 64 |
if p = 0 then Rat a p q |
65 |
else Rat (\<not> a) p q" |
|
19791 | 66 |
times_rat_def: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
19039 | 67 |
norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))" |
19791 | 68 |
inverse_rat_def: "inverse r == case r of Rat a p q \<Rightarrow> |
19039 | 69 |
if p = 0 then arbitrary |
70 |
else Rat a q p" |
|
19791 | 71 |
le_rat_def: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
19039 | 72 |
(\<not> a1 \<and> a2) \<or> |
73 |
(\<not> (a1 \<and> \<not> a2) \<and> |
|
74 |
(let |
|
75 |
((r1, r2), dummy) = common ((p1, q1), (p2, q2)) |
|
76 |
in if a1 then r1 <= r2 else r2 <= r1))" |
|
77 |
||
19791 | 78 |
|
79 |
section {* type serializations *} |
|
80 |
||
81 |
types_code |
|
82 |
rat ("{*erat*}") |
|
83 |
||
19039 | 84 |
code_syntax_tyco rat |
85 |
ml (target_atom "{*erat*}") |
|
86 |
haskell (target_atom "{*erat*}") |
|
87 |
||
19791 | 88 |
|
89 |
section {* const serializations *} |
|
90 |
||
91 |
consts_code |
|
92 |
arbitrary :: erat ("raise/ (Fail/ \"non-defined rational number\")") |
|
93 |
Fract ("{*of_quotient*}") |
|
94 |
0 :: rat ("{*0::erat*}") |
|
95 |
1 :: rat ("{*1::erat*}") |
|
96 |
HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
97 |
uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}") |
|
98 |
HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
99 |
inverse :: "rat \<Rightarrow> rat" ("{*inverse :: erat \<Rightarrow> erat*}") |
|
100 |
divide :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
|
101 |
Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
|
102 |
"op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}") |
|
103 |
||
19039 | 104 |
code_syntax_const |
19609 | 105 |
"arbitrary :: erat" |
106 |
ml ("raise/ (Fail/ \"non-defined rational number\")") |
|
107 |
haskell ("error/ \"non-defined rational number\"") |
|
19039 | 108 |
Fract |
109 |
ml ("{*of_quotient*}") |
|
110 |
haskell ("{*of_quotient*}") |
|
19137 | 111 |
"0 :: rat" |
19039 | 112 |
ml ("{*0::erat*}") |
113 |
haskell ("{*1::erat*}") |
|
19137 | 114 |
"1 :: rat" |
19039 | 115 |
ml ("{*1::erat*}") |
116 |
haskell ("{*1::erat*}") |
|
19137 | 117 |
"op + :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 118 |
ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
19791 | 119 |
haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
19137 | 120 |
"uminus :: rat \<Rightarrow> rat" |
19039 | 121 |
ml ("{*uminus :: erat \<Rightarrow> erat*}") |
122 |
haskell ("{*uminus :: erat \<Rightarrow> erat*}") |
|
19137 | 123 |
"op * :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 124 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
125 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
19137 | 126 |
"inverse :: rat \<Rightarrow> rat" |
19039 | 127 |
ml ("{*inverse :: erat \<Rightarrow> erat*}") |
128 |
haskell ("{*inverse :: erat \<Rightarrow> erat*}") |
|
19137 | 129 |
"divide :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 130 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
131 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
|
19137 | 132 |
"op <= :: rat \<Rightarrow> rat \<Rightarrow> bool" |
19039 | 133 |
ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
134 |
haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
|
19791 | 135 |
"op = :: rat \<Rightarrow> rat \<Rightarrow> bool" |
136 |
ml ("{*eq_rat*}") |
|
137 |
haskell ("{*eq_rat*}") |
|
19039 | 138 |
|
139 |
end |
|
140 |