author | haftmann |
Mon, 06 Nov 2006 16:28:31 +0100 | |
changeset 21191 | c00161fbf990 |
parent 21125 | 9b7d35ca1eef |
child 21404 | eb85850d3eb7 |
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 |
||
20934 | 84 |
lemma number_of_rat [code unfold]: |
85 |
"(number_of k \<Colon> rat) \<equiv> Fract k 1" |
|
20701 | 86 |
unfolding Fract_of_int_eq rat_number_of_def by simp |
87 |
||
20934 | 88 |
declare divide_inverse [where ?'a = rat, code func] |
89 |
||
20701 | 90 |
instance rat :: eq .. |
20934 | 91 |
instance erat :: eq .. |
20701 | 92 |
|
93 |
||
94 |
section {* code names *} |
|
95 |
||
21191 | 96 |
code_modulename SML |
97 |
ExecutableRat Rational |
|
20701 | 98 |
|
99 |
||
20934 | 100 |
section {* rat as abstype *} |
101 |
||
21191 | 102 |
lemma [code func]: -- {* prevents eq constraint *} |
103 |
shows "All = All" |
|
104 |
and "contents = contents" by rule+ |
|
105 |
||
20934 | 106 |
code_abstype rat erat where |
107 |
Fract \<equiv> of_quotient |
|
108 |
"0 \<Colon> rat" \<equiv> "0 \<Colon> erat" |
|
109 |
"1 \<Colon> rat" \<equiv> "1 \<Colon> erat" |
|
110 |
"op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" |
|
111 |
"uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat" |
|
112 |
"op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" |
|
113 |
"inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat" |
|
114 |
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" |
|
21191 | 115 |
"Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat |
20934 | 116 |
|
117 |
code_const div_zero |
|
118 |
(SML "raise/ (Fail/ \"Division by zero\")") |
|
119 |
(Haskell "error/ \"Division by zero\"") |
|
120 |
||
121 |
code_gen |
|
122 |
Fract |
|
123 |
"0 \<Colon> rat" |
|
124 |
"1 \<Colon> rat" |
|
125 |
"op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" |
|
126 |
"uminus \<Colon> rat \<Rightarrow> rat" |
|
127 |
"op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" |
|
128 |
"inverse \<Colon> rat \<Rightarrow> rat" |
|
129 |
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" |
|
21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20934
diff
changeset
|
130 |
"Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" |
21125 | 131 |
(SML *) |
20934 | 132 |
|
133 |
||
19791 | 134 |
section {* type serializations *} |
135 |
||
136 |
types_code |
|
137 |
rat ("{*erat*}") |
|
138 |
||
139 |
||
140 |
section {* const serializations *} |
|
141 |
||
142 |
consts_code |
|
20701 | 143 |
div_zero ("raise/ (Fail/ \"non-defined rational number\")") |
19791 | 144 |
Fract ("{*of_quotient*}") |
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20701
diff
changeset
|
145 |
HOL.zero :: rat ("{*0::erat*}") |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20701
diff
changeset
|
146 |
HOL.one :: rat ("{*1::erat*}") |
19791 | 147 |
HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
148 |
uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}") |
|
149 |
HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
150 |
inverse :: "rat \<Rightarrow> rat" ("{*inverse :: erat \<Rightarrow> erat*}") |
|
151 |
divide :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
|
152 |
Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
|
20934 | 153 |
"op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_erat*}") |
19889 | 154 |
|
19039 | 155 |
end |