author | haftmann |
Thu, 11 May 2006 10:25:55 +0200 | |
changeset 19609 | a677ac8c9b10 |
parent 19233 | 77ca20b0ed77 |
child 19791 | ab326de16ad5 |
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 |
||
16 |
datatype erat = Rat bool int int |
|
17 |
||
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
18 |
instance erat :: zero .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
19 |
instance erat :: one .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
20 |
instance erat :: plus .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
21 |
instance erat :: minus .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
22 |
instance erat :: times .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
23 |
instance erat :: inverse .. |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
24 |
instance erat :: ord .. |
19039 | 25 |
|
19609 | 26 |
definition |
19039 | 27 |
norm :: "erat \<Rightarrow> erat" |
19609 | 28 |
norm_def [simp]: "norm r = (case r of (Rat a p q) \<Rightarrow> |
19039 | 29 |
if p = 0 then Rat True 0 1 |
30 |
else |
|
31 |
let |
|
32 |
absp = abs p |
|
33 |
in let |
|
34 |
m = zgcd (absp, q) |
|
19609 | 35 |
in Rat (a = (0 <= p)) (absp div m) (q div m))" |
36 |
common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int" |
|
37 |
common_def [simp]: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow> |
|
19039 | 38 |
let q' = q1 * q2 div int (gcd (nat q1, nat q2)) |
19609 | 39 |
in ((p1 * (q' div q1), p2 * (q' div q2)), q'))" |
40 |
of_quotient :: "int * int \<Rightarrow> erat" |
|
41 |
of_quotient_def [simp]: "of_quotient r = (case r of (a, b) \<Rightarrow> |
|
42 |
norm (Rat True a b))" |
|
43 |
of_rat :: "rat \<Rightarrow> erat" |
|
44 |
of_rat_def [simp]: "of_rat r = of_quotient (THE s. s : Rep_Rat r)" |
|
45 |
to_rat :: "erat \<Rightarrow> rat" |
|
46 |
to_rat_def [simp]: "to_rat r = (case r of (Rat a p q) \<Rightarrow> |
|
47 |
if a then Fract p q else Fract (uminus p) q)" |
|
19039 | 48 |
|
49 |
defs (overloaded) |
|
50 |
zero_rat_def [simp]: "0 == Rat False 0 1" |
|
51 |
one_rat_def [simp]: "1 == Rat False 1 1" |
|
52 |
add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
53 |
let |
|
54 |
((r1, r2), den) = common ((p1, q1), (p2, q2)) |
|
55 |
in let |
|
56 |
num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2) |
|
57 |
in norm (Rat True num den)" |
|
58 |
uminus_rat_def [simp]: "- r == case r of Rat a p q \<Rightarrow> |
|
59 |
if p = 0 then Rat a p q |
|
60 |
else Rat (\<not> a) p q" |
|
61 |
times_rat_def [simp]: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
62 |
norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))" |
|
63 |
inverse_rat_def [simp]: "inverse r == case r of Rat a p q \<Rightarrow> |
|
64 |
if p = 0 then arbitrary |
|
65 |
else Rat a q p" |
|
66 |
le_rat_def [simp]: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow> |
|
67 |
(\<not> a1 \<and> a2) \<or> |
|
68 |
(\<not> (a1 \<and> \<not> a2) \<and> |
|
69 |
(let |
|
70 |
((r1, r2), dummy) = common ((p1, q1), (p2, q2)) |
|
71 |
in if a1 then r1 <= r2 else r2 <= r1))" |
|
72 |
||
73 |
code_syntax_tyco rat |
|
74 |
ml (target_atom "{*erat*}") |
|
75 |
haskell (target_atom "{*erat*}") |
|
76 |
||
77 |
code_syntax_const |
|
19609 | 78 |
"arbitrary :: erat" |
79 |
ml ("raise/ (Fail/ \"non-defined rational number\")") |
|
80 |
haskell ("error/ \"non-defined rational number\"") |
|
19039 | 81 |
Fract |
82 |
ml ("{*of_quotient*}") |
|
83 |
haskell ("{*of_quotient*}") |
|
19137 | 84 |
"0 :: rat" |
19039 | 85 |
ml ("{*0::erat*}") |
86 |
haskell ("{*1::erat*}") |
|
19137 | 87 |
"1 :: rat" |
19039 | 88 |
ml ("{*1::erat*}") |
89 |
haskell ("{*1::erat*}") |
|
19137 | 90 |
"op + :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 91 |
ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19137
diff
changeset
|
92 |
haskell ("{*HOL.plus :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
19137 | 93 |
"uminus :: rat \<Rightarrow> rat" |
19039 | 94 |
ml ("{*uminus :: erat \<Rightarrow> erat*}") |
95 |
haskell ("{*uminus :: erat \<Rightarrow> erat*}") |
|
19137 | 96 |
"op * :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 97 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
98 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}") |
|
19137 | 99 |
"inverse :: rat \<Rightarrow> rat" |
19039 | 100 |
ml ("{*inverse :: erat \<Rightarrow> erat*}") |
101 |
haskell ("{*inverse :: erat \<Rightarrow> erat*}") |
|
19137 | 102 |
"divide :: rat \<Rightarrow> rat \<Rightarrow> rat" |
19039 | 103 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
104 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)") |
|
19137 | 105 |
"op <= :: rat \<Rightarrow> rat \<Rightarrow> bool" |
19039 | 106 |
ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
107 |
haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}") |
|
108 |
||
109 |
end |
|
110 |