author  haftmann 
Mon, 16 Feb 2009 19:11:55 +0100  
changeset 29940  83b373f61d41 
parent 29925  17d1e32ef867 
child 30095  c6e184561159 
child 30240  5b25fee0362c 
permissions  rwrr 
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 
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29667
diff
changeset

8 
imports GCD 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

9 
uses ("Tools/rat_arith.ML") 
15131  10 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

11 

27551  12 
subsection {* Rational numbers as quotient *} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

13 

27551  14 
subsubsection {* Construction of the type of rational numbers *} 
18913  15 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20522
diff
changeset

16 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20522
diff
changeset

17 
ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where 
27551  18 
"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

19 

18913  20 
lemma ratrel_iff [simp]: 
27551  21 
"(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x" 
22 
by (simp add: ratrel_def) 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

23 

27551  24 
lemma refl_ratrel: "refl {x. snd x \<noteq> 0} ratrel" 
25 
by (auto simp add: refl_def ratrel_def) 

18913  26 

27 
lemma sym_ratrel: "sym ratrel" 

27551  28 
by (simp add: ratrel_def sym_def) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

29 

18913  30 
lemma trans_ratrel: "trans ratrel" 
27551  31 
proof (rule transI, unfold split_paired_all) 
32 
fix a b a' b' a'' b'' :: int 

33 
assume A: "((a, b), (a', b')) \<in> ratrel" 

34 
assume B: "((a', b'), (a'', b'')) \<in> ratrel" 

35 
have "b' * (a * b'') = b'' * (a * b')" by simp 

36 
also from A have "a * b' = a' * b" by auto 

37 
also have "b'' * (a' * b) = b * (a' * b'')" by simp 

38 
also from B have "a' * b'' = a'' * b'" by auto 

39 
also have "b * (a'' * b') = b' * (a'' * b)" by simp 

40 
finally have "b' * (a * b'') = b' * (a'' * b)" . 

41 
moreover from B have "b' \<noteq> 0" by auto 

42 
ultimately have "a * b'' = a'' * b" by simp 

43 
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

44 
qed 
27551  45 

46 
lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel" 

47 
by (rule equiv.intro [OF refl_ratrel sym_ratrel trans_ratrel]) 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

48 

18913  49 
lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] 
50 
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

51 

27551  52 
lemma equiv_ratrel_iff [iff]: 
53 
assumes "snd x \<noteq> 0" and "snd y \<noteq> 0" 

54 
shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel" 

55 
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

56 

27551  57 
typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel" 
58 
proof 

59 
have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp 

60 
then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI) 

61 
qed 

62 

63 
lemma ratrel_in_Rat [simp]: "snd x \<noteq> 0 \<Longrightarrow> ratrel `` {x} \<in> Rat" 

64 
by (simp add: Rat_def quotientI) 

65 

66 
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] 

67 

68 

69 
subsubsection {* Representation and basic operations *} 

70 

71 
definition 

72 
Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where 

28562  73 
[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

74 

27551  75 
code_datatype Fract 
76 

77 
lemma Rat_cases [case_names Fract, cases type: rat]: 

78 
assumes "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> C" 

79 
shows C 

80 
using assms by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) 

81 

82 
lemma Rat_induct [case_names Fract, induct type: rat]: 

83 
assumes "\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)" 

84 
shows "P q" 

85 
using assms by (cases q) simp 

86 

87 
lemma eq_rat: 

88 
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

89 
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

90 
and "\<And>a c. Fract 0 a = Fract 0 c" 
27551  91 
by (simp_all add: Fract_def) 
92 

93 
instantiation rat :: "{comm_ring_1, recpower}" 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

94 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

95 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

96 
definition 
27551  97 
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

98 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

99 
definition 
27551  100 
One_rat_def [code, code unfold]: "1 = Fract 1 1" 
18913  101 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

102 
definition 
28562  103 
add_rat_def [code del]: 
27551  104 
"q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
105 
ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" 

106 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

107 
lemma add_rat [simp]: 
27551  108 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
109 
shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" 

110 
proof  

111 
have "(\<lambda>x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)}) 

112 
respects2 ratrel" 

113 
by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib) 

114 
with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2) 

115 
qed 

18913  116 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

117 
definition 
28562  118 
minus_rat_def [code del]: 
27551  119 
" q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {( fst x, snd x)})" 
120 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

121 
lemma minus_rat [simp, code]: " Fract a b = Fract ( a) b" 
27551  122 
proof  
123 
have "(\<lambda>x. ratrel `` {( fst x, snd x)}) respects ratrel" 

124 
by (simp add: congruent_def) 

125 
then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel) 

126 
qed 

127 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

128 
lemma minus_rat_cancel [simp]: "Fract ( a) ( b) = Fract a b" 
27551  129 
by (cases "b = 0") (simp_all add: eq_rat) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

130 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

131 
definition 
28562  132 
diff_rat_def [code del]: "q  r = q +  (r::rat)" 
18913  133 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

134 
lemma diff_rat [simp]: 
27551  135 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
136 
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

137 
using assms by (simp add: diff_rat_def) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

138 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

139 
definition 
28562  140 
mult_rat_def [code del]: 
27551  141 
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
142 
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

143 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

144 
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" 
27551  145 
proof  
146 
have "(\<lambda>x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel" 

147 
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all 

148 
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

149 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

150 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

151 
lemma mult_rat_cancel: 
27551  152 
assumes "c \<noteq> 0" 
153 
shows "Fract (c * a) (c * b) = Fract a b" 

154 
proof  

155 
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

156 
then show ?thesis by (simp add: mult_rat [symmetric]) 
27551  157 
qed 
27509  158 

159 
primrec power_rat 

160 
where 

27551  161 
rat_power_0: "q ^ 0 = (1\<Colon>rat)" 
162 
 rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)" 

27509  163 

164 
instance proof 

27668  165 
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

166 
by (cases q, cases r, cases s) (simp add: eq_rat) 
27551  167 
next 
168 
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

169 
by (cases q, cases r) (simp add: eq_rat) 
27551  170 
next 
171 
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

172 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  173 
next 
174 
fix q r s :: rat show "(q + r) + s = q + (r + s)" 

29667  175 
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) 
27551  176 
next 
177 
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

178 
by (cases q, cases r) (simp add: eq_rat) 
27551  179 
next 
180 
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

181 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  182 
next 
183 
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

184 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  185 
next 
186 
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

187 
by (cases q, cases r) (simp add: eq_rat) 
27551  188 
next 
189 
fix q r s :: rat show "(q + r) * s = q * s + r * s" 

29667  190 
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) 
27551  191 
next 
192 
show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat) 

193 
next 

194 
fix q :: rat show "q * 1 = q" 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

195 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  196 
next 
27509  197 
fix q :: rat 
198 
fix n :: nat 

199 
show "q ^ 0 = 1" by simp 

200 
show "q ^ (Suc n) = q * (q ^ n)" by simp 

201 
qed 

202 

203 
end 

204 

27551  205 
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

206 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  207 

208 
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

209 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  210 

211 
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" 

212 
by (rule of_nat_rat [symmetric]) 

213 

214 
lemma Fract_of_int_eq: "Fract k 1 = of_int k" 

215 
by (rule of_int_rat [symmetric]) 

216 

217 
instantiation rat :: number_ring 

218 
begin 

219 

220 
definition 

28562  221 
rat_number_of_def [code del]: "number_of w = Fract w 1" 
27551  222 

223 
instance by intro_classes (simp add: rat_number_of_def of_int_rat) 

224 

225 
end 

226 

227 
lemma rat_number_collapse [code post]: 

228 
"Fract 0 k = 0" 

229 
"Fract 1 1 = 1" 

230 
"Fract (number_of k) 1 = number_of k" 

231 
"Fract k 0 = 0" 

232 
by (cases "k = 0") 

233 
(simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def) 

234 

235 
lemma rat_number_expand [code unfold]: 

236 
"0 = Fract 0 1" 

237 
"1 = Fract 1 1" 

238 
"number_of k = Fract (number_of k) 1" 

239 
by (simp_all add: rat_number_collapse) 

240 

241 
lemma iszero_rat [simp]: 

242 
"iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)" 

243 
by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) 

244 

245 
lemma Rat_cases_nonzero [case_names Fract 0]: 

246 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> C" 

247 
assumes 0: "q = 0 \<Longrightarrow> C" 

248 
shows C 

249 
proof (cases "q = 0") 

250 
case True then show C using 0 by auto 

251 
next 

252 
case False 

253 
then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto 

254 
moreover with False have "0 \<noteq> Fract a b" by simp 

255 
with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) 

256 
with Fract `q = Fract a b` `b \<noteq> 0` show C by auto 

257 
qed 

258 

259 

260 

261 
subsubsection {* The field of rational numbers *} 

262 

263 
instantiation rat :: "{field, division_by_zero}" 

264 
begin 

265 

266 
definition 

28562  267 
inverse_rat_def [code del]: 
27551  268 
"inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. 
269 
ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" 

270 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

271 
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" 
27551  272 
proof  
273 
have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel" 

274 
by (auto simp add: congruent_def mult_commute) 

275 
then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel) 

27509  276 
qed 
277 

27551  278 
definition 
28562  279 
divide_rat_def [code del]: "q / r = q * inverse (r::rat)" 
27551  280 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

281 
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

282 
by (simp add: divide_rat_def) 
27551  283 

284 
instance proof 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

285 
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand) 
27551  286 
(simp add: rat_number_collapse) 
287 
next 

288 
fix q :: rat 

289 
assume "q \<noteq> 0" 

290 
then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero) 

291 
(simp_all add: mult_rat inverse_rat rat_number_expand eq_rat) 

292 
next 

293 
fix q r :: rat 

294 
show "q / r = q * inverse r" by (simp add: divide_rat_def) 

295 
qed 

296 

297 
end 

298 

299 

300 
subsubsection {* Various *} 

301 

302 
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

303 
by (simp add: rat_number_expand) 
27551  304 

305 
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

306 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  307 

308 
lemma Fract_number_of_quotient [code post]: 

309 
"Fract (number_of k) (number_of l) = number_of k / number_of l" 

310 
unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. 

311 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

312 
lemma Fract_1_number_of [code post]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

313 
"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

314 
unfolding Fract_of_int_quotient number_of_eq by simp 
27551  315 

316 
subsubsection {* The ordered field of rational numbers *} 

27509  317 

318 
instantiation rat :: linorder 

319 
begin 

320 

321 
definition 

28562  322 
le_rat_def [code del]: 
27509  323 
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
27551  324 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
325 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

326 
lemma le_rat [simp]: 
27551  327 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
328 
shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" 

329 
proof  

330 
have "(\<lambda>x y. {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)}) 

331 
respects2 ratrel" 

332 
proof (clarsimp simp add: congruent2_def) 

333 
fix a b a' b' c d c' d'::int 

334 
assume neq: "b \<noteq> 0" "b' \<noteq> 0" "d \<noteq> 0" "d' \<noteq> 0" 

335 
assume eq1: "a * b' = a' * b" 

336 
assume eq2: "c * d' = c' * d" 

337 

338 
let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" 

339 
{ 

340 
fix a b c d x :: int assume x: "x \<noteq> 0" 

341 
have "?le a b c d = ?le (a * x) (b * x) c d" 

342 
proof  

343 
from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) 

344 
hence "?le a b c d = 

345 
((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" 

346 
by (simp add: mult_le_cancel_right) 

347 
also have "... = ?le (a * x) (b * x) c d" 

348 
by (simp add: mult_ac) 

349 
finally show ?thesis . 

350 
qed 

351 
} note le_factor = this 

352 

353 
let ?D = "b * d" and ?D' = "b' * d'" 

354 
from neq have D: "?D \<noteq> 0" by simp 

355 
from neq have "?D' \<noteq> 0" by simp 

356 
hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" 

357 
by (rule le_factor) 

27668  358 
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
27551  359 
by (simp add: mult_ac) 
360 
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')" 

361 
by (simp only: eq1 eq2) 

362 
also have "... = ?le (a' * ?D) (b' * ?D) c' d'" 

363 
by (simp add: mult_ac) 

364 
also from D have "... = ?le a' b' c' d'" 

365 
by (rule le_factor [symmetric]) 

366 
finally show "?le a b c d = ?le a' b' c' d'" . 

367 
qed 

368 
with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2) 

369 
qed 

27509  370 

371 
definition 

28562  372 
less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" 
27509  373 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

374 
lemma less_rat [simp]: 
27551  375 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
376 
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

377 
using assms by (simp add: less_rat_def eq_rat order_less_le) 
27509  378 

379 
instance proof 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

380 
fix q r s :: rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

381 
{ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

382 
assume "q \<le> r" and "r \<le> s" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

383 
show "q \<le> s" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

384 
proof (insert prems, induct q, induct r, induct s) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

385 
fix a b c d e f :: int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

386 
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

387 
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

388 
show "Fract a b \<le> Fract e f" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

389 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

390 
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

391 
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

392 
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

393 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

394 
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

395 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

396 
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

397 
qed 
27668  398 
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

399 
also have "... \<le> (e * d) * (d * f) * (b * b)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

400 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

401 
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

402 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

403 
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

404 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

405 
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

406 
by (simp only: mult_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

407 
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

408 
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

409 
with neq show ?thesis by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

410 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

411 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

412 
next 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

413 
assume "q \<le> r" and "r \<le> q" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

414 
show "q = r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

415 
proof (insert prems, induct q, induct r) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

416 
fix a b c d :: int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

417 
assume neq: "b \<noteq> 0" "d \<noteq> 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

418 
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

419 
show "Fract a b = Fract c d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

420 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

421 
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

422 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

423 
also have "... \<le> (a * d) * (b * d)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

424 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

425 
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

426 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

427 
thus ?thesis by (simp only: mult_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

428 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

429 
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

430 
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

431 
ultimately have "a * d = c * b" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

432 
with neq show ?thesis by (simp add: eq_rat) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

433 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

434 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

435 
next 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

436 
show "q \<le> q" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

437 
by (induct q) simp 
27682  438 
show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" 
439 
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

440 
show "q \<le> r \<or> r \<le> q" 
18913  441 
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

442 
(simp add: mult_commute, rule linorder_linear) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

443 
} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

444 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

445 

27509  446 
end 
447 

27551  448 
instantiation rat :: "{distrib_lattice, abs_if, sgn_if}" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

449 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

450 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

451 
definition 
28562  452 
abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then q else (q::rat))" 
27551  453 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

454 
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" 
27551  455 
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) 
456 

457 
definition 

28562  458 
sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else  1)" 
27551  459 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

460 
lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)" 
27551  461 
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

462 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  463 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
464 

465 
definition 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

466 
"(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

467 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

468 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

469 
"(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

470 

27551  471 
instance by intro_classes 
472 
(auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) 

22456  473 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

474 
end 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

475 

27551  476 
instance rat :: ordered_field 
477 
proof 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

478 
fix q r s :: rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

479 
show "q \<le> r ==> s + q \<le> s + r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

480 
proof (induct q, induct r, induct s) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

481 
fix a b c d e f :: int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

482 
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

483 
assume le: "Fract a b \<le> Fract c d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

484 
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

485 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

486 
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

487 
by (auto simp add: zero_less_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

488 
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

489 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

490 
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

491 
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

492 
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

493 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

494 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

495 
show "q < r ==> 0 < s ==> s * q < s * r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

496 
proof (induct q, induct r, induct s) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

497 
fix a b c d e f :: int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

498 
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

499 
assume le: "Fract a b < Fract c d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

500 
assume gt: "0 < Fract e f" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

501 
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

502 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

503 
let ?E = "e * f" and ?F = "f * f" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

504 
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

505 
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

506 
moreover from neq have "0 < ?F" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

507 
by (auto simp add: zero_less_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

508 
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

509 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

510 
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

511 
by (simp add: mult_less_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

512 
with neq show ?thesis 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

513 
by (simp add: mult_ac) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

514 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

515 
qed 
27551  516 
qed auto 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

517 

27551  518 
lemma Rat_induct_pos [case_names Fract, induct type: rat]: 
519 
assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" 

520 
shows "P q" 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

521 
proof (cases q) 
27551  522 
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

523 
proof  
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

524 
fix a::int and b::int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

525 
assume b: "b < 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

526 
hence "0 < b" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

527 
hence "P (Fract (a) (b))" by (rule step) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

528 
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

529 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

530 
case (Fract a b) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

531 
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

532 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

533 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

534 
lemma zero_less_Fract_iff: 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

535 
"0 < b ==> (0 < Fract a b) = (0 < a)" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

536 
by (simp add: Zero_rat_def order_less_imp_not_eq2 zero_less_mult_iff) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

537 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

538 

27551  539 
subsection {* Arithmetic setup *} 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

540 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

541 
use "Tools/rat_arith.ML" 
24075  542 
declaration {* K rat_arith_setup *} 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

543 

23342  544 

545 
subsection {* Embedding from Rationals to other Fields *} 

546 

24198  547 
class field_char_0 = field + ring_char_0 
23342  548 

27551  549 
subclass (in ordered_field) field_char_0 .. 
23342  550 

27551  551 
context field_char_0 
552 
begin 

553 

554 
definition of_rat :: "rat \<Rightarrow> 'a" where 

28562  555 
[code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})" 
23342  556 

27551  557 
end 
558 

23342  559 
lemma of_rat_congruent: 
27551  560 
"(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel" 
23342  561 
apply (rule congruent.intro) 
562 
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

563 
apply (simp only: of_int_mult [symmetric]) 

564 
done 

565 

27551  566 
lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b" 
567 
unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent) 

23342  568 

569 
lemma of_rat_0 [simp]: "of_rat 0 = 0" 

570 
by (simp add: Zero_rat_def of_rat_rat) 

571 

572 
lemma of_rat_1 [simp]: "of_rat 1 = 1" 

573 
by (simp add: One_rat_def of_rat_rat) 

574 

575 
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

576 
by (induct a, induct b, simp add: of_rat_rat add_frac_eq) 
23342  577 

23343  578 
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

579 
by (induct a, simp add: of_rat_rat) 
23343  580 

581 
lemma of_rat_diff: "of_rat (a  b) = of_rat a  of_rat b" 

582 
by (simp only: diff_minus of_rat_add of_rat_minus) 

583 

23342  584 
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

585 
apply (induct a, induct b, simp add: of_rat_rat) 
23342  586 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 
587 
done 

588 

589 
lemma nonzero_of_rat_inverse: 

590 
"a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)" 

23343  591 
apply (rule inverse_unique [symmetric]) 
592 
apply (simp add: of_rat_mult [symmetric]) 

23342  593 
done 
594 

595 
lemma of_rat_inverse: 

596 
"(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) = 

597 
inverse (of_rat a)" 

598 
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) 

599 

600 
lemma nonzero_of_rat_divide: 

601 
"b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b" 

602 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

603 

604 
lemma of_rat_divide: 

605 
"(of_rat (a / b)::'a::{field_char_0,division_by_zero}) 

606 
= 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

607 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
23342  608 

23343  609 
lemma of_rat_power: 
610 
"(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n" 

611 
by (induct n) (simp_all add: of_rat_mult power_Suc) 

612 

613 
lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" 

614 
apply (induct a, induct b) 

615 
apply (simp add: of_rat_rat eq_rat) 

616 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

617 
apply (simp only: of_int_mult [symmetric] of_int_eq_iff) 

618 
done 

619 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

620 
lemma of_rat_less: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

621 
"(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

622 
proof (induct r, induct s) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

623 
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

624 
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

625 
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

626 
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

627 
"(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

628 
\<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

629 
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

630 
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

631 
\<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

632 
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

633 
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

634 
(auto intro: mult_strict_right_mono mult_right_less_imp_less) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

635 
qed 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

636 

818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

637 
lemma of_rat_less_eq: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

638 
"(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

639 
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

640 

23343  641 
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] 
642 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

643 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  644 
proof 
645 
fix a 

646 
show "of_rat a = id a" 

647 
by (induct a) 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

648 
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) 
23343  649 
qed 
650 

651 
text{*Collapse nested embeddings*} 

652 
lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" 

653 
by (induct n) (simp_all add: of_rat_add) 

654 

655 
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

656 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  657 

658 
lemma of_rat_number_of_eq [simp]: 

659 
"of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})" 

660 
by (simp add: number_of_eq) 

661 

23879  662 
lemmas zero_rat = Zero_rat_def 
663 
lemmas one_rat = One_rat_def 

664 

24198  665 
abbreviation 
666 
rat_of_nat :: "nat \<Rightarrow> rat" 

667 
where 

668 
"rat_of_nat \<equiv> of_nat" 

669 

670 
abbreviation 

671 
rat_of_int :: "int \<Rightarrow> rat" 

672 
where 

673 
"rat_of_int \<equiv> of_int" 

674 

28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

675 
subsection {* The Set of Rational Numbers *} 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

676 

28001  677 
context field_char_0 
678 
begin 

679 

680 
definition 

681 
Rats :: "'a set" where 

28562  682 
[code del]: "Rats = range of_rat" 
28001  683 

684 
notation (xsymbols) 

685 
Rats ("\<rat>") 

686 

687 
end 

688 

28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

689 
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

690 
by (simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

691 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

692 
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

693 
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

694 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

695 
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

696 
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

697 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

698 
lemma Rats_number_of [simp]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

699 
"(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

700 
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

701 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

702 
lemma Rats_0 [simp]: "0 \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

703 
apply (unfold Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

704 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

705 
apply (rule of_rat_0 [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

706 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

707 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

708 
lemma Rats_1 [simp]: "1 \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

709 
apply (unfold Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

710 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

711 
apply (rule of_rat_1 [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

712 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

713 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

714 
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

715 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

716 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

717 
apply (rule of_rat_add [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

718 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

719 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

720 
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

721 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

722 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

723 
apply (rule of_rat_minus [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

724 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

725 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

726 
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

727 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

728 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

729 
apply (rule of_rat_diff [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

730 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

731 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

732 
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

733 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

734 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

735 
apply (rule of_rat_mult [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

736 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

737 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

738 
lemma nonzero_Rats_inverse: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

739 
fixes a :: "'a::field_char_0" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

740 
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

741 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

742 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

743 
apply (erule nonzero_of_rat_inverse [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

744 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

745 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

746 
lemma Rats_inverse [simp]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

747 
fixes a :: "'a::{field_char_0,division_by_zero}" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

748 
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

749 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

750 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

751 
apply (rule of_rat_inverse [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

752 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

753 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

754 
lemma nonzero_Rats_divide: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

755 
fixes a b :: "'a::field_char_0" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

756 
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

757 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

758 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

759 
apply (erule nonzero_of_rat_divide [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

760 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

761 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

762 
lemma Rats_divide [simp]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

763 
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

764 
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

765 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

766 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

767 
apply (rule of_rat_divide [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

768 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

769 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

770 
lemma Rats_power [simp]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

771 
fixes a :: "'a::{field_char_0,recpower}" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

772 
shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

773 
apply (auto simp add: Rats_def) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

774 
apply (rule range_eqI) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

775 
apply (rule of_rat_power [symmetric]) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

776 
done 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

777 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

778 
lemma Rats_cases [cases set: Rats]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

779 
assumes "q \<in> \<rat>" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

780 
obtains (of_rat) r where "q = of_rat r" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

781 
unfolding Rats_def 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

782 
proof  
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

783 
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

784 
then obtain r where "q = of_rat r" .. 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

785 
then show thesis .. 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

786 
qed 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

787 

8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

788 
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

789 
"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

790 
by (rule Rats_cases) auto 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

791 

28001  792 

24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

793 
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

794 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

795 
lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

796 
proof (cases "a = 0 \<or> b = 0") 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

797 
case True then show ?thesis by (auto simp add: eq_rat) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

798 
next 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

799 
let ?c = "zgcd a b" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

800 
case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

801 
then have "?c \<noteq> 0" by simp 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

802 
then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

803 
moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" 
29925  804 
by (simp add: semiring_div_class.mod_div_equality) 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

805 
moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

806 
moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric]) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

807 
ultimately show ?thesis 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

808 
by (simp add: mult_rat [symmetric]) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

809 
qed 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

810 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

811 
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where 
28562  812 
[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

813 

29332  814 
lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

815 
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

816 
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

817 

fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

818 
lemma [code]: 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

819 
"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

820 
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

821 

26513  822 
instantiation rat :: eq 
823 
begin 

824 

28562  825 
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

826 

26513  827 
instance by default (simp add: eq_rat_def) 
828 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

829 
lemma rat_eq_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

830 
"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

831 
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

832 
else if d = 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

833 
then a = 0 \<or> b = 0 
29332  834 
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

835 
by (auto simp add: eq eq_rat) 
26513  836 

28351  837 
lemma rat_eq_refl [code nbe]: 
838 
"eq_class.eq (r::rat) r \<longleftrightarrow> True" 

839 
by (rule HOL.eq_refl) 

840 

26513  841 
end 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

842 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

843 
lemma le_rat': 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

844 
assumes "b \<noteq> 0" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

845 
and "d \<noteq> 0" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

846 
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

847 
proof  
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

848 
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

849 
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

850 
proof (cases "b * d > 0") 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

851 
case True 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

852 
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

853 
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

854 
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

855 
next 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

856 
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

857 
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

858 
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

859 
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

860 
qed 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

861 
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

862 
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

863 
finally show ?thesis using assms by simp 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

864 
qed 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

865 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

866 
lemma less_rat': 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

867 
assumes "b \<noteq> 0" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

868 
and "d \<noteq> 0" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

869 
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

870 
proof  
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

871 
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

872 
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

873 
proof (cases "b * d > 0") 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

874 
case True 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

875 
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

876 
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

877 
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

878 
next 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

879 
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

880 
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

881 
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

882 
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

883 
qed 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

884 
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

885 
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

886 
finally show ?thesis using assms by simp 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

887 
qed 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

888 

29940  889 
lemma (in ordered_idom) sgn_greater [simp]: 
890 
"0 < sgn a \<longleftrightarrow> 0 < a" 

891 
unfolding sgn_if by auto 

892 

893 
lemma (in ordered_idom) sgn_less [simp]: 

894 
"sgn a < 0 \<longleftrightarrow> a < 0" 

895 
unfolding sgn_if by auto 

24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

896 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

897 
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

898 
"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

899 
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

900 
else if d = 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

901 
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

902 
else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)" 
29940  903 
by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat) 
904 

905 
lemma rat_less_eq_code [code]: 

906 
"Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0 

907 
then sgn c * sgn d \<ge> 0 

908 
else if d = 0 

909 
then sgn a * sgn b \<le> 0 

910 
else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)" 

911 
by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat) 

912 
(auto simp add: le_less not_less sgn_0_0) 

913 

24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

914 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

915 
lemma rat_plus_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

916 
"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

917 
then Fract c d 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

918 
else if d = 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

919 
then Fract a b 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

920 
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

921 
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

922 

818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

923 
lemma rat_times_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

924 
"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

925 
by simp 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

926 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

927 
lemma rat_minus_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

928 
"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

929 
then Fract ( c) d 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

930 
else if d = 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

931 
then Fract a b 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

932 
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

933 
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

934 

27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

935 
lemma rat_inverse_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

936 
"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

937 
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

938 
else Fract b a)" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

939 
by (simp add: eq_rat) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

940 

818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

941 
lemma rat_divide_code [code]: 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

942 
"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

943 
by simp 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

944 

818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

945 
hide (open) const Fract_norm 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

946 

24622  947 
text {* Setup for SML code generator *} 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

948 

fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

949 
types_code 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

950 
rat ("(int */ int)") 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

951 
attach (term_of) {* 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

952 
fun term_of_rat (p, q) = 
24622  953 
let 
24661  954 
val rT = Type ("Rational.rat", []) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

955 
in 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

956 
if q = 1 orelse p = 0 then HOLogic.mk_number rT p 
25885  957 
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

958 
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

959 
end; 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

960 
*} 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

961 
attach (test) {* 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

962 
fun gen_rat i = 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

963 
let 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

964 
val p = random_range 0 i; 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

965 
val q = random_range 1 (i + 1); 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

966 
val g = Integer.gcd p q; 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24622
diff
changeset

967 
val p' = p div g; 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24622
diff
changeset

968 
val q' = q div g; 
25885  969 
val r = (if one_of [true, false] then p' else ~ p', 
970 
if p' = 0 then 0 else q') 

24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

971 
in 
25885  972 
(r, fn () => term_of_rat r) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

973 
end; 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

974 
*} 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

975 

fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

976 
consts_code 
27551  977 
Fract ("(_,/ _)") 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

978 

fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

979 
consts_code 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

980 
"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

981 
attach {* 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

982 
fun rat_of_int 0 = (0, 0) 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

983 
 rat_of_int i = (i, 1); 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

984 
*} 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

985 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29667
diff
changeset

986 
end 