23854
|
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
|