author | haftmann |
Wed, 25 Nov 2009 11:16:57 +0100 | |
changeset 33959 | 2afc55e8ed27 |
parent 33814 | 984fb2171607 |
child 35028 | 108662d50512 |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset
|
1 |
(* Title: HOL/Rational.thy |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
3 |
*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
4 |
|
14691 | 5 |
header {* Rational numbers *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
6 |
|
15131 | 7 |
theory Rational |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
8 |
imports GCD Archimedean_Field |
15131 | 9 |
begin |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
10 |
|
27551 | 11 |
subsection {* Rational numbers as quotient *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
12 |
|
27551 | 13 |
subsubsection {* Construction of the type of rational numbers *} |
18913 | 14 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20522
diff
changeset
|
15 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20522
diff
changeset
|
16 |
ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where |
27551 | 17 |
"ratrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
18 |
|
18913 | 19 |
lemma ratrel_iff [simp]: |
27551 | 20 |
"(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x" |
21 |
by (simp add: ratrel_def) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
22 |
|
30198 | 23 |
lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel" |
24 |
by (auto simp add: refl_on_def ratrel_def) |
|
18913 | 25 |
|
26 |
lemma sym_ratrel: "sym ratrel" |
|
27551 | 27 |
by (simp add: ratrel_def sym_def) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
28 |
|
18913 | 29 |
lemma trans_ratrel: "trans ratrel" |
27551 | 30 |
proof (rule transI, unfold split_paired_all) |
31 |
fix a b a' b' a'' b'' :: int |
|
32 |
assume A: "((a, b), (a', b')) \<in> ratrel" |
|
33 |
assume B: "((a', b'), (a'', b'')) \<in> ratrel" |
|
34 |
have "b' * (a * b'') = b'' * (a * b')" by simp |
|
35 |
also from A have "a * b' = a' * b" by auto |
|
36 |
also have "b'' * (a' * b) = b * (a' * b'')" by simp |
|
37 |
also from B have "a' * b'' = a'' * b'" by auto |
|
38 |
also have "b * (a'' * b') = b' * (a'' * b)" by simp |
|
39 |
finally have "b' * (a * b'') = b' * (a'' * b)" . |
|
40 |
moreover from B have "b' \<noteq> 0" by auto |
|
41 |
ultimately have "a * b'' = a'' * b" by simp |
|
42 |
with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
43 |
qed |
27551 | 44 |
|
45 |
lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel" |
|
30198 | 46 |
by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel]) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
47 |
|
18913 | 48 |
lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] |
49 |
lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
50 |
|
27551 | 51 |
lemma equiv_ratrel_iff [iff]: |
52 |
assumes "snd x \<noteq> 0" and "snd y \<noteq> 0" |
|
53 |
shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel" |
|
54 |
by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
55 |
|
27551 | 56 |
typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel" |
57 |
proof |
|
58 |
have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp |
|
59 |
then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI) |
|
60 |
qed |
|
61 |
||
62 |
lemma ratrel_in_Rat [simp]: "snd x \<noteq> 0 \<Longrightarrow> ratrel `` {x} \<in> Rat" |
|
63 |
by (simp add: Rat_def quotientI) |
|
64 |
||
65 |
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] |
|
66 |
||
67 |
||
68 |
subsubsection {* Representation and basic operations *} |
|
69 |
||
70 |
definition |
|
71 |
Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where |
|
28562 | 72 |
[code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
73 |
|
27551 | 74 |
code_datatype Fract |
75 |
||
76 |
lemma Rat_cases [case_names Fract, cases type: rat]: |
|
77 |
assumes "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> C" |
|
78 |
shows C |
|
79 |
using assms by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) |
|
80 |
||
81 |
lemma Rat_induct [case_names Fract, induct type: rat]: |
|
82 |
assumes "\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)" |
|
83 |
shows "P q" |
|
84 |
using assms by (cases q) simp |
|
85 |
||
86 |
lemma eq_rat: |
|
87 |
shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
88 |
and "\<And>a. Fract a 0 = Fract 0 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
89 |
and "\<And>a c. Fract 0 a = Fract 0 c" |
27551 | 90 |
by (simp_all add: Fract_def) |
91 |
||
31017 | 92 |
instantiation rat :: comm_ring_1 |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
93 |
begin |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
94 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
95 |
definition |
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
96 |
Zero_rat_def [code, code_unfold]: "0 = Fract 0 1" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
97 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
98 |
definition |
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
99 |
One_rat_def [code, code_unfold]: "1 = Fract 1 1" |
18913 | 100 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
101 |
definition |
28562 | 102 |
add_rat_def [code del]: |
27551 | 103 |
"q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
104 |
ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" |
|
105 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
106 |
lemma add_rat [simp]: |
27551 | 107 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
108 |
shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
|
109 |
proof - |
|
110 |
have "(\<lambda>x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)}) |
|
111 |
respects2 ratrel" |
|
112 |
by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib) |
|
113 |
with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2) |
|
114 |
qed |
|
18913 | 115 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
116 |
definition |
28562 | 117 |
minus_rat_def [code del]: |
27551 | 118 |
"- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})" |
119 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
120 |
lemma minus_rat [simp, code]: "- Fract a b = Fract (- a) b" |
27551 | 121 |
proof - |
122 |
have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel" |
|
123 |
by (simp add: congruent_def) |
|
124 |
then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel) |
|
125 |
qed |
|
126 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
127 |
lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b" |
27551 | 128 |
by (cases "b = 0") (simp_all add: eq_rat) |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
129 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
130 |
definition |
28562 | 131 |
diff_rat_def [code del]: "q - r = q + - (r::rat)" |
18913 | 132 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
133 |
lemma diff_rat [simp]: |
27551 | 134 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
135 |
shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
136 |
using assms by (simp add: diff_rat_def) |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
137 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
138 |
definition |
28562 | 139 |
mult_rat_def [code del]: |
27551 | 140 |
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
141 |
ratrel``{(fst x * fst y, snd x * snd y)})" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
142 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
143 |
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" |
27551 | 144 |
proof - |
145 |
have "(\<lambda>x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel" |
|
146 |
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all |
|
147 |
then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
148 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
149 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
150 |
lemma mult_rat_cancel: |
27551 | 151 |
assumes "c \<noteq> 0" |
152 |
shows "Fract (c * a) (c * b) = Fract a b" |
|
153 |
proof - |
|
154 |
from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
155 |
then show ?thesis by (simp add: mult_rat [symmetric]) |
27551 | 156 |
qed |
27509 | 157 |
|
158 |
instance proof |
|
27668 | 159 |
fix q r s :: rat show "(q * r) * s = q * (r * s)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
160 |
by (cases q, cases r, cases s) (simp add: eq_rat) |
27551 | 161 |
next |
162 |
fix q r :: rat show "q * r = r * q" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
163 |
by (cases q, cases r) (simp add: eq_rat) |
27551 | 164 |
next |
165 |
fix q :: rat show "1 * q = q" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
166 |
by (cases q) (simp add: One_rat_def eq_rat) |
27551 | 167 |
next |
168 |
fix q r s :: rat show "(q + r) + s = q + (r + s)" |
|
29667 | 169 |
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) |
27551 | 170 |
next |
171 |
fix q r :: rat show "q + r = r + q" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
172 |
by (cases q, cases r) (simp add: eq_rat) |
27551 | 173 |
next |
174 |
fix q :: rat show "0 + q = q" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
175 |
by (cases q) (simp add: Zero_rat_def eq_rat) |
27551 | 176 |
next |
177 |
fix q :: rat show "- q + q = 0" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
178 |
by (cases q) (simp add: Zero_rat_def eq_rat) |
27551 | 179 |
next |
180 |
fix q r :: rat show "q - r = q + - r" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
181 |
by (cases q, cases r) (simp add: eq_rat) |
27551 | 182 |
next |
183 |
fix q r s :: rat show "(q + r) * s = q * s + r * s" |
|
29667 | 184 |
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) |
27551 | 185 |
next |
186 |
show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat) |
|
27509 | 187 |
qed |
188 |
||
189 |
end |
|
190 |
||
27551 | 191 |
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
192 |
by (induct k) (simp_all add: Zero_rat_def One_rat_def) |
27551 | 193 |
|
194 |
lemma of_int_rat: "of_int k = Fract k 1" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
195 |
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) |
27551 | 196 |
|
197 |
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" |
|
198 |
by (rule of_nat_rat [symmetric]) |
|
199 |
||
200 |
lemma Fract_of_int_eq: "Fract k 1 = of_int k" |
|
201 |
by (rule of_int_rat [symmetric]) |
|
202 |
||
203 |
instantiation rat :: number_ring |
|
204 |
begin |
|
205 |
||
206 |
definition |
|
28562 | 207 |
rat_number_of_def [code del]: "number_of w = Fract w 1" |
27551 | 208 |
|
30960 | 209 |
instance proof |
210 |
qed (simp add: rat_number_of_def of_int_rat) |
|
27551 | 211 |
|
212 |
end |
|
213 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
214 |
lemma rat_number_collapse [code_post]: |
27551 | 215 |
"Fract 0 k = 0" |
216 |
"Fract 1 1 = 1" |
|
217 |
"Fract (number_of k) 1 = number_of k" |
|
218 |
"Fract k 0 = 0" |
|
219 |
by (cases "k = 0") |
|
220 |
(simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def) |
|
221 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
222 |
lemma rat_number_expand [code_unfold]: |
27551 | 223 |
"0 = Fract 0 1" |
224 |
"1 = Fract 1 1" |
|
225 |
"number_of k = Fract (number_of k) 1" |
|
226 |
by (simp_all add: rat_number_collapse) |
|
227 |
||
228 |
lemma iszero_rat [simp]: |
|
229 |
"iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)" |
|
230 |
by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) |
|
231 |
||
232 |
lemma Rat_cases_nonzero [case_names Fract 0]: |
|
233 |
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> C" |
|
234 |
assumes 0: "q = 0 \<Longrightarrow> C" |
|
235 |
shows C |
|
236 |
proof (cases "q = 0") |
|
237 |
case True then show C using 0 by auto |
|
238 |
next |
|
239 |
case False |
|
240 |
then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto |
|
241 |
moreover with False have "0 \<noteq> Fract a b" by simp |
|
242 |
with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) |
|
243 |
with Fract `q = Fract a b` `b \<noteq> 0` show C by auto |
|
244 |
qed |
|
245 |
||
33805 | 246 |
subsubsection {* Function @{text normalize} *} |
247 |
||
248 |
text{* |
|
249 |
Decompose a fraction into normalized, i.e. coprime numerator and denominator: |
|
250 |
*} |
|
251 |
||
252 |
definition normalize :: "rat \<Rightarrow> int \<times> int" where |
|
253 |
"normalize x \<equiv> THE pair. x = Fract (fst pair) (snd pair) & |
|
254 |
snd pair > 0 & gcd (fst pair) (snd pair) = 1" |
|
255 |
||
256 |
declare normalize_def[code del] |
|
257 |
||
258 |
lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" |
|
259 |
proof (cases "a = 0 | b = 0") |
|
260 |
case True then show ?thesis by (auto simp add: eq_rat) |
|
261 |
next |
|
262 |
let ?c = "gcd a b" |
|
263 |
case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto |
|
264 |
then have "?c \<noteq> 0" by simp |
|
265 |
then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat) |
|
266 |
moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" |
|
267 |
by (simp add: semiring_div_class.mod_div_equality) |
|
268 |
moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
269 |
moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
270 |
ultimately show ?thesis |
|
271 |
by (simp add: mult_rat [symmetric]) |
|
272 |
qed |
|
273 |
||
274 |
text{* Proof by Ren\'e Thiemann: *} |
|
275 |
lemma normalize_code[code]: |
|
276 |
"normalize (Fract a b) = |
|
277 |
(if b > 0 then (let g = gcd a b in (a div g, b div g)) |
|
278 |
else if b = 0 then (0,1) |
|
279 |
else (let g = - gcd a b in (a div g, b div g)))" |
|
280 |
proof - |
|
281 |
let ?cond = "% r p. r = Fract (fst p) (snd p) & snd p > 0 & |
|
282 |
gcd (fst p) (snd p) = 1" |
|
283 |
show ?thesis |
|
284 |
proof (cases "b = 0") |
|
285 |
case True |
|
286 |
thus ?thesis |
|
287 |
proof (simp add: normalize_def) |
|
288 |
show "(THE pair. ?cond (Fract a 0) pair) = (0,1)" |
|
289 |
proof |
|
290 |
show "?cond (Fract a 0) (0,1)" |
|
291 |
by (simp add: rat_number_collapse) |
|
292 |
next |
|
293 |
fix pair |
|
294 |
assume cond: "?cond (Fract a 0) pair" |
|
295 |
show "pair = (0,1)" |
|
296 |
proof (cases pair) |
|
297 |
case (Pair den num) |
|
298 |
with cond have num: "num > 0" by auto |
|
299 |
with Pair cond have den: "den = 0" by (simp add: eq_rat) |
|
300 |
show ?thesis |
|
301 |
proof (cases "num = 1", simp add: Pair den) |
|
302 |
case False |
|
303 |
with num have gr: "num > 1" by auto |
|
304 |
with den have "gcd den num = num" by auto |
|
305 |
with Pair cond False gr show ?thesis by auto |
|
306 |
qed |
|
307 |
qed |
|
308 |
qed |
|
309 |
qed |
|
310 |
next |
|
311 |
{ fix a b :: int assume b: "b > 0" |
|
312 |
hence b0: "b \<noteq> 0" and "b >= 0" by auto |
|
313 |
let ?g = "gcd a b" |
|
314 |
from b0 have g0: "?g \<noteq> 0" by auto |
|
315 |
then have gp: "?g > 0" by simp |
|
316 |
then have gs: "?g <= b" by (metis b gcd_le2_int) |
|
317 |
from gcd_dvd1_int[of a b] obtain a' where a': "a = ?g * a'" |
|
318 |
unfolding dvd_def by auto |
|
319 |
from gcd_dvd2_int[of a b] obtain b' where b': "b = ?g * b'" |
|
320 |
unfolding dvd_def by auto |
|
321 |
hence b'2: "b' * ?g = b" by (simp add: ring_simps) |
|
322 |
with b0 have b'0: "b' \<noteq> 0" by auto |
|
323 |
from b b' zero_less_mult_iff[of ?g b'] gp have b'p: "b' > 0" by arith |
|
324 |
have "normalize (Fract a b) = (a div ?g, b div ?g)" |
|
325 |
proof (simp add: normalize_def) |
|
326 |
show "(THE pair. ?cond (Fract a b) pair) = (a div ?g, b div ?g)" |
|
327 |
proof |
|
328 |
have "1 = b div b" using b0 by auto |
|
329 |
also have "\<dots> <= b div ?g" by (rule zdiv_mono2[OF `b >= 0` gp gs]) |
|
330 |
finally have div0: "b div ?g > 0" by simp |
|
331 |
show "?cond (Fract a b) (a div ?g, b div ?g)" |
|
332 |
by (simp add: b0 Fract_norm div_gcd_coprime_int div0) |
|
333 |
next |
|
334 |
fix pair assume cond: "?cond (Fract a b) pair" |
|
335 |
show "pair = (a div ?g, b div ?g)" |
|
336 |
proof (cases pair) |
|
337 |
case (Pair den num) |
|
338 |
with cond |
|
339 |
have num: "num > 0" and num0: "num \<noteq> 0" and gcd: "gcd den num = 1" |
|
340 |
by auto |
|
341 |
obtain g where g: "g = ?g" by auto |
|
342 |
with gp have gg0: "g > 0" by auto |
|
343 |
from cond Pair eq_rat(1)[OF b0 num0] |
|
344 |
have eq: "a * num = den * b" by auto |
|
345 |
hence "a' * g * num = den * g * b'" |
|
346 |
using a'[simplified g[symmetric]] b'[simplified g[symmetric]] |
|
347 |
by simp |
|
348 |
hence "a' * num * g = b' * den * g" by (simp add: algebra_simps) |
|
349 |
hence eq2: "a' * num = b' * den" using gg0 by auto |
|
350 |
have "a div ?g = ?g * a' div ?g" using a' by force |
|
351 |
hence adiv: "a div ?g = a'" using g0 by auto |
|
352 |
have "b div ?g = ?g * b' div ?g" using b' by force |
|
353 |
hence bdiv: "b div ?g = b'" using g0 by auto |
|
354 |
from div_gcd_coprime_int[of a b] b0 |
|
355 |
have "gcd (a div ?g) (b div ?g) = 1" by auto |
|
356 |
with adiv bdiv have gcd2: "gcd a' b' = 1" by auto |
|
357 |
from gcd have gcd3: "gcd num den = 1" |
|
358 |
by (simp add: gcd_commute_int[of den num]) |
|
359 |
from gcd2 have gcd4: "gcd b' a' = 1" |
|
360 |
by (simp add: gcd_commute_int[of a' b']) |
|
361 |
have one: "num dvd b'" |
|
33814 | 362 |
by (metis coprime_dvd_mult_int[OF gcd3] dvd_triv_right eq2) |
363 |
have two: "b' dvd num" |
|
364 |
by (metis coprime_dvd_mult_int[OF gcd4] dvd_triv_left eq2 zmult_commute) |
|
365 |
from zdvd_antisym_abs[OF one two] b'p num |
|
366 |
have numb': "num = b'" by auto |
|
33805 | 367 |
with eq2 b'0 have "a' = den" by auto |
368 |
with numb' adiv bdiv Pair show ?thesis by simp |
|
369 |
qed |
|
370 |
qed |
|
371 |
qed |
|
372 |
} |
|
373 |
note main = this |
|
374 |
assume "b \<noteq> 0" |
|
375 |
hence "b > 0 | b < 0" by arith |
|
376 |
thus ?thesis |
|
377 |
proof |
|
378 |
assume b: "b > 0" thus ?thesis by (simp add: Let_def main[OF b]) |
|
379 |
next |
|
380 |
assume b: "b < 0" |
|
381 |
thus ?thesis |
|
382 |
by(simp add:main Let_def minus_rat_cancel[of a b, symmetric] |
|
383 |
zdiv_zminus2 del:minus_rat_cancel) |
|
384 |
qed |
|
385 |
qed |
|
386 |
qed |
|
387 |
||
388 |
lemma normalize_id: "normalize (Fract a b) = (p,q) \<Longrightarrow> Fract p q = Fract a b" |
|
389 |
by(auto simp add: normalize_code Let_def Fract_norm dvd_div_neg rat_number_collapse |
|
390 |
split:split_if_asm) |
|
391 |
||
392 |
lemma normalize_denom_pos: "normalize (Fract a b) = (p,q) \<Longrightarrow> q > 0" |
|
393 |
by(auto simp add: normalize_code Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff |
|
394 |
split:split_if_asm) |
|
395 |
||
396 |
lemma normalize_coprime: "normalize (Fract a b) = (p,q) \<Longrightarrow> coprime p q" |
|
397 |
by(auto simp add: normalize_code Let_def dvd_div_neg div_gcd_coprime_int |
|
398 |
split:split_if_asm) |
|
399 |
||
27551 | 400 |
|
401 |
subsubsection {* The field of rational numbers *} |
|
402 |
||
403 |
instantiation rat :: "{field, division_by_zero}" |
|
404 |
begin |
|
405 |
||
406 |
definition |
|
28562 | 407 |
inverse_rat_def [code del]: |
27551 | 408 |
"inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. |
409 |
ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" |
|
410 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
411 |
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" |
27551 | 412 |
proof - |
413 |
have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel" |
|
414 |
by (auto simp add: congruent_def mult_commute) |
|
415 |
then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel) |
|
27509 | 416 |
qed |
417 |
||
27551 | 418 |
definition |
28562 | 419 |
divide_rat_def [code del]: "q / r = q * inverse (r::rat)" |
27551 | 420 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
421 |
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
422 |
by (simp add: divide_rat_def) |
27551 | 423 |
|
424 |
instance proof |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
425 |
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand) |
27551 | 426 |
(simp add: rat_number_collapse) |
427 |
next |
|
428 |
fix q :: rat |
|
429 |
assume "q \<noteq> 0" |
|
430 |
then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero) |
|
431 |
(simp_all add: mult_rat inverse_rat rat_number_expand eq_rat) |
|
432 |
next |
|
433 |
fix q r :: rat |
|
434 |
show "q / r = q * inverse r" by (simp add: divide_rat_def) |
|
435 |
qed |
|
436 |
||
437 |
end |
|
438 |
||
439 |
||
440 |
subsubsection {* Various *} |
|
441 |
||
442 |
lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
443 |
by (simp add: rat_number_expand) |
27551 | 444 |
|
445 |
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
446 |
by (simp add: Fract_of_int_eq [symmetric]) |
27551 | 447 |
|
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
448 |
lemma Fract_number_of_quotient [code_post]: |
27551 | 449 |
"Fract (number_of k) (number_of l) = number_of k / number_of l" |
450 |
unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. |
|
451 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset
|
452 |
lemma Fract_1_number_of [code_post]: |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
453 |
"Fract 1 (number_of k) = 1 / number_of k" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
454 |
unfolding Fract_of_int_quotient number_of_eq by simp |
27551 | 455 |
|
456 |
subsubsection {* The ordered field of rational numbers *} |
|
27509 | 457 |
|
458 |
instantiation rat :: linorder |
|
459 |
begin |
|
460 |
||
461 |
definition |
|
28562 | 462 |
le_rat_def [code del]: |
27509 | 463 |
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
27551 | 464 |
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" |
465 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
466 |
lemma le_rat [simp]: |
27551 | 467 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
468 |
shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
469 |
proof - |
|
470 |
have "(\<lambda>x y. {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)}) |
|
471 |
respects2 ratrel" |
|
472 |
proof (clarsimp simp add: congruent2_def) |
|
473 |
fix a b a' b' c d c' d'::int |
|
474 |
assume neq: "b \<noteq> 0" "b' \<noteq> 0" "d \<noteq> 0" "d' \<noteq> 0" |
|
475 |
assume eq1: "a * b' = a' * b" |
|
476 |
assume eq2: "c * d' = c' * d" |
|
477 |
||
478 |
let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" |
|
479 |
{ |
|
480 |
fix a b c d x :: int assume x: "x \<noteq> 0" |
|
481 |
have "?le a b c d = ?le (a * x) (b * x) c d" |
|
482 |
proof - |
|
483 |
from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) |
|
484 |
hence "?le a b c d = |
|
485 |
((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" |
|
486 |
by (simp add: mult_le_cancel_right) |
|
487 |
also have "... = ?le (a * x) (b * x) c d" |
|
488 |
by (simp add: mult_ac) |
|
489 |
finally show ?thesis . |
|
490 |
qed |
|
491 |
} note le_factor = this |
|
492 |
||
493 |
let ?D = "b * d" and ?D' = "b' * d'" |
|
494 |
from neq have D: "?D \<noteq> 0" by simp |
|
495 |
from neq have "?D' \<noteq> 0" by simp |
|
496 |
hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" |
|
497 |
by (rule le_factor) |
|
27668 | 498 |
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" |
27551 | 499 |
by (simp add: mult_ac) |
500 |
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')" |
|
501 |
by (simp only: eq1 eq2) |
|
502 |
also have "... = ?le (a' * ?D) (b' * ?D) c' d'" |
|
503 |
by (simp add: mult_ac) |
|
504 |
also from D have "... = ?le a' b' c' d'" |
|
505 |
by (rule le_factor [symmetric]) |
|
506 |
finally show "?le a b c d = ?le a' b' c' d'" . |
|
507 |
qed |
|
508 |
with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2) |
|
509 |
qed |
|
27509 | 510 |
|
511 |
definition |
|
28562 | 512 |
less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" |
27509 | 513 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
514 |
lemma less_rat [simp]: |
27551 | 515 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
516 |
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
517 |
using assms by (simp add: less_rat_def eq_rat order_less_le) |
27509 | 518 |
|
519 |
instance proof |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
520 |
fix q r s :: rat |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
521 |
{ |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
522 |
assume "q \<le> r" and "r \<le> s" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
523 |
show "q \<le> s" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
524 |
proof (insert prems, induct q, induct r, induct s) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
525 |
fix a b c d e f :: int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
526 |
assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
527 |
assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
528 |
show "Fract a b \<le> Fract e f" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
529 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
530 |
from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
531 |
by (auto simp add: zero_less_mult_iff linorder_neq_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
532 |
have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
533 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
534 |
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
535 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
536 |
with ff show ?thesis by (simp add: mult_le_cancel_right) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
537 |
qed |
27668 | 538 |
also have "... = (c * f) * (d * f) * (b * b)" by algebra |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
539 |
also have "... \<le> (e * d) * (d * f) * (b * b)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
540 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
541 |
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
542 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
543 |
with bb show ?thesis by (simp add: mult_le_cancel_right) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
544 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
545 |
finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
546 |
by (simp only: mult_ac) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
547 |
with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
548 |
by (simp add: mult_le_cancel_right) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
549 |
with neq show ?thesis by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
550 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
551 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
552 |
next |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
553 |
assume "q \<le> r" and "r \<le> q" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
554 |
show "q = r" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
555 |
proof (insert prems, induct q, induct r) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
556 |
fix a b c d :: int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
557 |
assume neq: "b \<noteq> 0" "d \<noteq> 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
558 |
assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
559 |
show "Fract a b = Fract c d" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
560 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
561 |
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
562 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
563 |
also have "... \<le> (a * d) * (b * d)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
564 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
565 |
from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
566 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
567 |
thus ?thesis by (simp only: mult_ac) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
568 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
569 |
finally have "(a * d) * (b * d) = (c * b) * (b * d)" . |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
570 |
moreover from neq have "b * d \<noteq> 0" by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
571 |
ultimately have "a * d = c * b" by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
572 |
with neq show ?thesis by (simp add: eq_rat) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
573 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
574 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
575 |
next |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
576 |
show "q \<le> q" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
577 |
by (induct q) simp |
27682 | 578 |
show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" |
579 |
by (induct q, induct r) (auto simp add: le_less mult_commute) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
580 |
show "q \<le> r \<or> r \<le> q" |
18913 | 581 |
by (induct q, induct r) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
582 |
(simp add: mult_commute, rule linorder_linear) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
583 |
} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
584 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
585 |
|
27509 | 586 |
end |
587 |
||
27551 | 588 |
instantiation rat :: "{distrib_lattice, abs_if, sgn_if}" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
589 |
begin |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
590 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
591 |
definition |
28562 | 592 |
abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))" |
27551 | 593 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
594 |
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
27551 | 595 |
by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps) |
596 |
||
597 |
definition |
|
28562 | 598 |
sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" |
27551 | 599 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
600 |
lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)" |
27551 | 601 |
unfolding Fract_of_int_eq |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
602 |
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) |
27551 | 603 |
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) |
604 |
||
605 |
definition |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
606 |
"(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
607 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
608 |
definition |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
609 |
"(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
610 |
|
27551 | 611 |
instance by intro_classes |
612 |
(auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) |
|
22456 | 613 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
614 |
end |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
615 |
|
27551 | 616 |
instance rat :: ordered_field |
617 |
proof |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
618 |
fix q r s :: rat |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
619 |
show "q \<le> r ==> s + q \<le> s + r" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
620 |
proof (induct q, induct r, induct s) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
621 |
fix a b c d e f :: int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
622 |
assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
623 |
assume le: "Fract a b \<le> Fract c d" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
624 |
show "Fract e f + Fract a b \<le> Fract e f + Fract c d" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
625 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
626 |
let ?F = "f * f" from neq have F: "0 < ?F" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
627 |
by (auto simp add: zero_less_mult_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
628 |
from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
629 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
630 |
with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
631 |
by (simp add: mult_le_cancel_right) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
632 |
with neq show ?thesis by (simp add: mult_ac int_distrib) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
633 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
634 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
635 |
show "q < r ==> 0 < s ==> s * q < s * r" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
636 |
proof (induct q, induct r, induct s) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
637 |
fix a b c d e f :: int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
638 |
assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
639 |
assume le: "Fract a b < Fract c d" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
640 |
assume gt: "0 < Fract e f" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
641 |
show "Fract e f * Fract a b < Fract e f * Fract c d" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
642 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
643 |
let ?E = "e * f" and ?F = "f * f" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
644 |
from neq gt have "0 < ?E" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
645 |
by (auto simp add: Zero_rat_def order_less_le eq_rat) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
646 |
moreover from neq have "0 < ?F" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
647 |
by (auto simp add: zero_less_mult_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
648 |
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
649 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
650 |
ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
651 |
by (simp add: mult_less_cancel_right) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
652 |
with neq show ?thesis |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
653 |
by (simp add: mult_ac) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
654 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
655 |
qed |
27551 | 656 |
qed auto |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
657 |
|
27551 | 658 |
lemma Rat_induct_pos [case_names Fract, induct type: rat]: |
659 |
assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
|
660 |
shows "P q" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
661 |
proof (cases q) |
27551 | 662 |
have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
663 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
664 |
fix a::int and b::int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
665 |
assume b: "b < 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
666 |
hence "0 < -b" by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
667 |
hence "P (Fract (-a) (-b))" by (rule step) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
668 |
thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
669 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
670 |
case (Fract a b) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
671 |
thus "P q" by (force simp add: linorder_neq_iff step step') |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
672 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
673 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
674 |
lemma zero_less_Fract_iff: |
30095
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
675 |
"0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
676 |
by (simp add: Zero_rat_def zero_less_mult_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
677 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
678 |
lemma Fract_less_zero_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
679 |
"0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
680 |
by (simp add: Zero_rat_def mult_less_0_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
681 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
682 |
lemma zero_le_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
683 |
"0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
684 |
by (simp add: Zero_rat_def zero_le_mult_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
685 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
686 |
lemma Fract_le_zero_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
687 |
"0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
688 |
by (simp add: Zero_rat_def mult_le_0_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
689 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
690 |
lemma one_less_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
691 |
"0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
692 |
by (simp add: One_rat_def mult_less_cancel_right_disj) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
693 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
694 |
lemma Fract_less_one_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
695 |
"0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
696 |
by (simp add: One_rat_def mult_less_cancel_right_disj) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
697 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
698 |
lemma one_le_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
699 |
"0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
700 |
by (simp add: One_rat_def mult_le_cancel_right) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
701 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
702 |
lemma Fract_le_one_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
703 |
"0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
704 |
by (simp add: One_rat_def mult_le_cancel_right) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
705 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
706 |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
707 |
subsubsection {* Rationals are an Archimedean field *} |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
708 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
709 |
lemma rat_floor_lemma: |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
710 |
assumes "0 < b" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
711 |
shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
712 |
proof - |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
713 |
have "Fract a b = of_int (a div b) + Fract (a mod b) b" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
714 |
using `0 < b` by (simp add: of_int_rat) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
715 |
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
716 |
using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
717 |
ultimately show ?thesis by simp |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
718 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
719 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
720 |
instance rat :: archimedean_field |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
721 |
proof |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
722 |
fix r :: rat |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
723 |
show "\<exists>z. r \<le> of_int z" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
724 |
proof (induct r) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
725 |
case (Fract a b) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
726 |
then have "Fract a b \<le> of_int (a div b + 1)" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
727 |
using rat_floor_lemma [of b a] by simp |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
728 |
then show "\<exists>z. Fract a b \<le> of_int z" .. |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
729 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
730 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
731 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
732 |
lemma floor_Fract: |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
733 |
assumes "0 < b" shows "floor (Fract a b) = a div b" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
734 |
using rat_floor_lemma [OF `0 < b`, of a] |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
735 |
by (simp add: floor_unique) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
736 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
737 |
|
31100 | 738 |
subsection {* Linear arithmetic setup *} |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
739 |
|
31100 | 740 |
declaration {* |
741 |
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] |
|
742 |
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) |
|
743 |
#> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] |
|
744 |
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) |
|
745 |
#> Lin_Arith.add_simps [@{thm neg_less_iff_less}, |
|
746 |
@{thm True_implies_equals}, |
|
747 |
read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, |
|
748 |
@{thm divide_1}, @{thm divide_zero_left}, |
|
749 |
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
|
750 |
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
|
751 |
@{thm of_int_minus}, @{thm of_int_diff}, |
|
752 |
@{thm of_int_of_nat_eq}] |
|
753 |
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors |
|
754 |
#> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) |
|
755 |
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) |
|
756 |
*} |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
757 |
|
23342 | 758 |
|
759 |
subsection {* Embedding from Rationals to other Fields *} |
|
760 |
||
24198 | 761 |
class field_char_0 = field + ring_char_0 |
23342 | 762 |
|
27551 | 763 |
subclass (in ordered_field) field_char_0 .. |
23342 | 764 |
|
27551 | 765 |
context field_char_0 |
766 |
begin |
|
767 |
||
768 |
definition of_rat :: "rat \<Rightarrow> 'a" where |
|
28562 | 769 |
[code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})" |
23342 | 770 |
|
27551 | 771 |
end |
772 |
||
23342 | 773 |
lemma of_rat_congruent: |
27551 | 774 |
"(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel" |
23342 | 775 |
apply (rule congruent.intro) |
776 |
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) |
|
777 |
apply (simp only: of_int_mult [symmetric]) |
|
778 |
done |
|
779 |
||
27551 | 780 |
lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b" |
781 |
unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent) |
|
23342 | 782 |
|
783 |
lemma of_rat_0 [simp]: "of_rat 0 = 0" |
|
784 |
by (simp add: Zero_rat_def of_rat_rat) |
|
785 |
||
786 |
lemma of_rat_1 [simp]: "of_rat 1 = 1" |
|
787 |
by (simp add: One_rat_def of_rat_rat) |
|
788 |
||
789 |
lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
790 |
by (induct a, induct b, simp add: of_rat_rat add_frac_eq) |
23342 | 791 |
|
23343 | 792 |
lemma of_rat_minus: "of_rat (- a) = - of_rat a" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
793 |
by (induct a, simp add: of_rat_rat) |
23343 | 794 |
|
795 |
lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" |
|
796 |
by (simp only: diff_minus of_rat_add of_rat_minus) |
|
797 |
||
23342 | 798 |
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
799 |
apply (induct a, induct b, simp add: of_rat_rat) |
23342 | 800 |
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) |
801 |
done |
|
802 |
||
803 |
lemma nonzero_of_rat_inverse: |
|
804 |
"a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)" |
|
23343 | 805 |
apply (rule inverse_unique [symmetric]) |
806 |
apply (simp add: of_rat_mult [symmetric]) |
|
23342 | 807 |
done |
808 |
||
809 |
lemma of_rat_inverse: |
|
810 |
"(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) = |
|
811 |
inverse (of_rat a)" |
|
812 |
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) |
|
813 |
||
814 |
lemma nonzero_of_rat_divide: |
|
815 |
"b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b" |
|
816 |
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) |
|
817 |
||
818 |
lemma of_rat_divide: |
|
819 |
"(of_rat (a / b)::'a::{field_char_0,division_by_zero}) |
|
820 |
= of_rat a / of_rat b" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
821 |
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) |
23342 | 822 |
|
23343 | 823 |
lemma of_rat_power: |
31017 | 824 |
"(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
825 |
by (induct n) (simp_all add: of_rat_mult) |
23343 | 826 |
|
827 |
lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" |
|
828 |
apply (induct a, induct b) |
|
829 |
apply (simp add: of_rat_rat eq_rat) |
|
830 |
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) |
|
831 |
apply (simp only: of_int_mult [symmetric] of_int_eq_iff) |
|
832 |
done |
|
833 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
834 |
lemma of_rat_less: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
835 |
"(of_rat r :: 'a::ordered_field) < of_rat s \<longleftrightarrow> r < s" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
836 |
proof (induct r, induct s) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
837 |
fix a b c d :: int |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
838 |
assume not_zero: "b > 0" "d > 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
839 |
then have "b * d > 0" by (rule mult_pos_pos) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
840 |
have of_int_divide_less_eq: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
841 |
"(of_int a :: 'a) / of_int b < of_int c / of_int d |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
842 |
\<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
843 |
using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
844 |
show "(of_rat (Fract a b) :: 'a::ordered_field) < of_rat (Fract c d) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
845 |
\<longleftrightarrow> Fract a b < Fract c d" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
846 |
using not_zero `b * d > 0` |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
847 |
by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
848 |
qed |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
849 |
|
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
850 |
lemma of_rat_less_eq: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
851 |
"(of_rat r :: 'a::ordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
852 |
unfolding le_less by (auto simp add: of_rat_less) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
853 |
|
23343 | 854 |
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] |
855 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
856 |
lemma of_rat_eq_id [simp]: "of_rat = id" |
23343 | 857 |
proof |
858 |
fix a |
|
859 |
show "of_rat a = id a" |
|
860 |
by (induct a) |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
861 |
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) |
23343 | 862 |
qed |
863 |
||
864 |
text{*Collapse nested embeddings*} |
|
865 |
lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" |
|
866 |
by (induct n) (simp_all add: of_rat_add) |
|
867 |
||
868 |
lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
869 |
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) |
23343 | 870 |
|
871 |
lemma of_rat_number_of_eq [simp]: |
|
872 |
"of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})" |
|
873 |
by (simp add: number_of_eq) |
|
874 |
||
23879 | 875 |
lemmas zero_rat = Zero_rat_def |
876 |
lemmas one_rat = One_rat_def |
|
877 |
||
24198 | 878 |
abbreviation |
879 |
rat_of_nat :: "nat \<Rightarrow> rat" |
|
880 |
where |
|
881 |
"rat_of_nat \<equiv> of_nat" |
|
882 |
||
883 |
abbreviation |
|
884 |
rat_of_int :: "int \<Rightarrow> rat" |
|
885 |
where |
|
886 |
"rat_of_int \<equiv> of_int" |
|
887 |
||
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
888 |
subsection {* The Set of Rational Numbers *} |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
889 |
|
28001 | 890 |
context field_char_0 |
891 |
begin |
|
892 |
||
893 |
definition |
|
894 |
Rats :: "'a set" where |
|
28562 | 895 |
[code del]: "Rats = range of_rat" |
28001 | 896 |
|
897 |
notation (xsymbols) |
|
898 |
Rats ("\<rat>") |
|
899 |
||
900 |
end |
|
901 |
||
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
902 |
lemma Rats_of_rat [simp]: "of_rat r \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
903 |
by (simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
904 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
905 |
lemma Rats_of_int [simp]: "of_int z \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
906 |
by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
907 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
908 |
lemma Rats_of_nat [simp]: "of_nat n \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
909 |
by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
910 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
911 |
lemma Rats_number_of [simp]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
912 |
"(number_of w::'a::{number_ring,field_char_0}) \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
913 |
by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
914 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
915 |
lemma Rats_0 [simp]: "0 \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
916 |
apply (unfold Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
917 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
918 |
apply (rule of_rat_0 [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
919 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
920 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
921 |
lemma Rats_1 [simp]: "1 \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
922 |
apply (unfold Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
923 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
924 |
apply (rule of_rat_1 [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
925 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
926 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
927 |
lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
928 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
929 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
930 |
apply (rule of_rat_add [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
931 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
932 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
933 |
lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
934 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
935 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
936 |
apply (rule of_rat_minus [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
937 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
938 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
939 |
lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
940 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
941 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
942 |
apply (rule of_rat_diff [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
943 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
944 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
945 |
lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
946 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
947 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
948 |
apply (rule of_rat_mult [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
949 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
950 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
951 |
lemma nonzero_Rats_inverse: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
952 |
fixes a :: "'a::field_char_0" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
953 |
shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
954 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
955 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
956 |
apply (erule nonzero_of_rat_inverse [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
957 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
958 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
959 |
lemma Rats_inverse [simp]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
960 |
fixes a :: "'a::{field_char_0,division_by_zero}" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
961 |
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
962 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
963 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
964 |
apply (rule of_rat_inverse [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
965 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
966 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
967 |
lemma nonzero_Rats_divide: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
968 |
fixes a b :: "'a::field_char_0" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
969 |
shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
970 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
971 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
972 |
apply (erule nonzero_of_rat_divide [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
973 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
974 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
975 |
lemma Rats_divide [simp]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
976 |
fixes a b :: "'a::{field_char_0,division_by_zero}" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
977 |
shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
978 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
979 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
980 |
apply (rule of_rat_divide [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
981 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
982 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
983 |
lemma Rats_power [simp]: |
31017 | 984 |
fixes a :: "'a::field_char_0" |
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
985 |
shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
986 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
987 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
988 |
apply (rule of_rat_power [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
989 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
990 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
991 |
lemma Rats_cases [cases set: Rats]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
992 |
assumes "q \<in> \<rat>" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
993 |
obtains (of_rat) r where "q = of_rat r" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
994 |
unfolding Rats_def |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
995 |
proof - |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
996 |
from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def . |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
997 |
then obtain r where "q = of_rat r" .. |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
998 |
then show thesis .. |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
999 |
qed |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
1000 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
1001 |
lemma Rats_induct [case_names of_rat, induct set: Rats]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
1002 |
"q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
1003 |
by (rule Rats_cases) auto |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
1004 |
|
28001 | 1005 |
|
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1006 |
subsection {* Implementation of rational numbers as pairs of integers *} |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1007 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1008 |
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where |
28562 | 1009 |
[simp, code del]: "Fract_norm a b = Fract a b" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1010 |
|
31706 | 1011 |
lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = gcd a b in |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1012 |
if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1013 |
by (simp add: eq_rat Zero_rat_def Let_def Fract_norm) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1014 |
|
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1015 |
lemma [code]: |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1016 |
"of_rat (Fract a b) = (if b \<noteq> 0 then of_int a / of_int b else 0)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1017 |
by (cases "b = 0") (simp_all add: rat_number_collapse of_rat_rat) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1018 |
|
26513 | 1019 |
instantiation rat :: eq |
1020 |
begin |
|
1021 |
||
28562 | 1022 |
definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0" |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1023 |
|
26513 | 1024 |
instance by default (simp add: eq_rat_def) |
1025 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1026 |
lemma rat_eq_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1027 |
"eq_class.eq (Fract a b) (Fract c d) \<longleftrightarrow> (if b = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1028 |
then c = 0 \<or> d = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1029 |
else if d = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1030 |
then a = 0 \<or> b = 0 |
29332 | 1031 |
else a * d = b * c)" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1032 |
by (auto simp add: eq eq_rat) |
26513 | 1033 |
|
28351 | 1034 |
lemma rat_eq_refl [code nbe]: |
1035 |
"eq_class.eq (r::rat) r \<longleftrightarrow> True" |
|
1036 |
by (rule HOL.eq_refl) |
|
1037 |
||
26513 | 1038 |
end |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1039 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1040 |
lemma le_rat': |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1041 |
assumes "b \<noteq> 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1042 |
and "d \<noteq> 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1043 |
shows "Fract a b \<le> Fract c d \<longleftrightarrow> a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d" |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1044 |
proof - |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1045 |
have abs_sgn: "\<And>k::int. \<bar>k\<bar> = k * sgn k" unfolding abs_if sgn_if by simp |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1046 |
have "a * d * (b * d) \<le> c * b * (b * d) \<longleftrightarrow> a * d * (sgn b * sgn d) \<le> c * b * (sgn b * sgn d)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1047 |
proof (cases "b * d > 0") |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1048 |
case True |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1049 |
moreover from True have "sgn b * sgn d = 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1050 |
by (simp add: sgn_times [symmetric] sgn_1_pos) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1051 |
ultimately show ?thesis by (simp add: mult_le_cancel_right) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1052 |
next |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1053 |
case False with assms have "b * d < 0" by (simp add: less_le) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1054 |
moreover from this have "sgn b * sgn d = - 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1055 |
by (simp only: sgn_times [symmetric] sgn_1_neg) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1056 |
ultimately show ?thesis by (simp add: mult_le_cancel_right) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1057 |
qed |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1058 |
also have "\<dots> \<longleftrightarrow> a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1059 |
by (simp add: abs_sgn mult_ac) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1060 |
finally show ?thesis using assms by simp |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1061 |
qed |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1062 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1063 |
lemma less_rat': |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1064 |
assumes "b \<noteq> 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1065 |
and "d \<noteq> 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1066 |
shows "Fract a b < Fract c d \<longleftrightarrow> a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d" |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1067 |
proof - |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1068 |
have abs_sgn: "\<And>k::int. \<bar>k\<bar> = k * sgn k" unfolding abs_if sgn_if by simp |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1069 |
have "a * d * (b * d) < c * b * (b * d) \<longleftrightarrow> a * d * (sgn b * sgn d) < c * b * (sgn b * sgn d)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1070 |
proof (cases "b * d > 0") |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1071 |
case True |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1072 |
moreover from True have "sgn b * sgn d = 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1073 |
by (simp add: sgn_times [symmetric] sgn_1_pos) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1074 |
ultimately show ?thesis by (simp add: mult_less_cancel_right) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1075 |
next |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1076 |
case False with assms have "b * d < 0" by (simp add: less_le) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1077 |
moreover from this have "sgn b * sgn d = - 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1078 |
by (simp only: sgn_times [symmetric] sgn_1_neg) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1079 |
ultimately show ?thesis by (simp add: mult_less_cancel_right) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1080 |
qed |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1081 |
also have "\<dots> \<longleftrightarrow> a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1082 |
by (simp add: abs_sgn mult_ac) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1083 |
finally show ?thesis using assms by simp |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1084 |
qed |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1085 |
|
29940 | 1086 |
lemma (in ordered_idom) sgn_greater [simp]: |
1087 |
"0 < sgn a \<longleftrightarrow> 0 < a" |
|
1088 |
unfolding sgn_if by auto |
|
1089 |
||
1090 |
lemma (in ordered_idom) sgn_less [simp]: |
|
1091 |
"sgn a < 0 \<longleftrightarrow> a < 0" |
|
1092 |
unfolding sgn_if by auto |
|
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1093 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1094 |
lemma rat_le_eq_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1095 |
"Fract a b < Fract c d \<longleftrightarrow> (if b = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1096 |
then sgn c * sgn d > 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1097 |
else if d = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1098 |
then sgn a * sgn b < 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1099 |
else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)" |
29940 | 1100 |
by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat) |
1101 |
||
1102 |
lemma rat_less_eq_code [code]: |
|
1103 |
"Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0 |
|
1104 |
then sgn c * sgn d \<ge> 0 |
|
1105 |
else if d = 0 |
|
1106 |
then sgn a * sgn b \<le> 0 |
|
1107 |
else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)" |
|
1108 |
by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat) |
|
1109 |
(auto simp add: le_less not_less sgn_0_0) |
|
1110 |
||
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1111 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1112 |
lemma rat_plus_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1113 |
"Fract a b + Fract c d = (if b = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1114 |
then Fract c d |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1115 |
else if d = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1116 |
then Fract a b |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1117 |
else Fract_norm (a * d + c * b) (b * d))" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1118 |
by (simp add: eq_rat, simp add: Zero_rat_def) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1119 |
|
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1120 |
lemma rat_times_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1121 |
"Fract a b * Fract c d = Fract_norm (a * c) (b * d)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1122 |
by simp |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1123 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1124 |
lemma rat_minus_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1125 |
"Fract a b - Fract c d = (if b = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1126 |
then Fract (- c) d |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1127 |
else if d = 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1128 |
then Fract a b |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1129 |
else Fract_norm (a * d - c * b) (b * d))" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1130 |
by (simp add: eq_rat, simp add: Zero_rat_def) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1131 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1132 |
lemma rat_inverse_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1133 |
"inverse (Fract a b) = (if b = 0 then Fract 1 0 |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1134 |
else if a < 0 then Fract (- b) (- a) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1135 |
else Fract b a)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1136 |
by (simp add: eq_rat) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1137 |
|
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1138 |
lemma rat_divide_code [code]: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1139 |
"Fract a b / Fract c d = Fract_norm (a * d) (b * c)" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1140 |
by simp |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1141 |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1142 |
definition (in term_syntax) |
32657 | 1143 |
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1144 |
[code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l" |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1145 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1146 |
notation fcomp (infixl "o>" 60) |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1147 |
notation scomp (infixl "o\<rightarrow>" 60) |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1148 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1149 |
instantiation rat :: random |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1150 |
begin |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1151 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1152 |
definition |
31641 | 1153 |
"Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair ( |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
1154 |
let j = Code_Numeral.int_of (denom + 1) |
32657 | 1155 |
in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))" |
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1156 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1157 |
instance .. |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1158 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1159 |
end |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1160 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1161 |
no_notation fcomp (infixl "o>" 60) |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1162 |
no_notation scomp (infixl "o\<rightarrow>" 60) |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1163 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1164 |
hide (open) const Fract_norm |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1165 |
|
24622 | 1166 |
text {* Setup for SML code generator *} |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1167 |
|
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1168 |
types_code |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1169 |
rat ("(int */ int)") |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1170 |
attach (term_of) {* |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1171 |
fun term_of_rat (p, q) = |
24622 | 1172 |
let |
24661 | 1173 |
val rT = Type ("Rational.rat", []) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1174 |
in |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1175 |
if q = 1 orelse p = 0 then HOLogic.mk_number rT p |
25885 | 1176 |
else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $ |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1177 |
HOLogic.mk_number rT p $ HOLogic.mk_number rT q |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1178 |
end; |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1179 |
*} |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1180 |
attach (test) {* |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1181 |
fun gen_rat i = |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1182 |
let |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1183 |
val p = random_range 0 i; |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1184 |
val q = random_range 1 (i + 1); |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1185 |
val g = Integer.gcd p q; |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24622
diff
changeset
|
1186 |
val p' = p div g; |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24622
diff
changeset
|
1187 |
val q' = q div g; |
25885 | 1188 |
val r = (if one_of [true, false] then p' else ~ p', |
31666 | 1189 |
if p' = 0 then 1 else q') |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1190 |
in |
25885 | 1191 |
(r, fn () => term_of_rat r) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1192 |
end; |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1193 |
*} |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1194 |
|
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1195 |
consts_code |
27551 | 1196 |
Fract ("(_,/ _)") |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1197 |
|
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1198 |
consts_code |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1199 |
"of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1200 |
attach {* |
31674 | 1201 |
fun rat_of_int i = (i, 1); |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1202 |
*} |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1203 |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1204 |
setup {* |
33209 | 1205 |
Nitpick.register_frac_type @{type_name rat} |
1206 |
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
|
1207 |
(@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
|
1208 |
(@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
|
1209 |
(@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
|
1210 |
(@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |
|
1211 |
(@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}), |
|
1212 |
(@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), |
|
1213 |
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), |
|
1214 |
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}), |
|
1215 |
(@{const_name field_char_0_class.Rats}, @{const_name UNIV})] |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1216 |
*} |
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1217 |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1218 |
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat |
33209 | 1219 |
number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat |
1220 |
plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat |
|
1221 |
zero_rat_inst.zero_rat |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1222 |
|
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29667
diff
changeset
|
1223 |
end |