author  haftmann 
Fri, 11 Jul 2008 09:03:11 +0200  
changeset 27551  9a5543d4cc24 
parent 27509  63161d5f8f29 
child 27652  818666de6c24 
permissions  rwrr 
27551  1 
(* Title: HOL/Library/Rational.thy 
2 
ID: $Id$ 

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

3 
Author: Markus Wenzel, TU Muenchen 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

5 

14691  6 
header {* Rational numbers *} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

7 

15131  8 
theory Rational 
27551  9 
imports "../Presburger" GCD Abstract_Rat 
16417  10 
uses ("rat_arith.ML") 
15131  11 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

12 

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

14 

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

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

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

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

20 

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

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

24 

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

18913  27 

28 
lemma sym_ratrel: "sym ratrel" 

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

30 

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

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

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

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

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

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

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

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

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

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

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

44 
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

45 
qed 
27551  46 

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

48 
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

49 

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

52 

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

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

56 
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

57 

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

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

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

62 
qed 

63 

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

65 
by (simp add: Rat_def quotientI) 

66 

67 
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] 

68 

69 

70 
subsubsection {* Representation and basic operations *} 

71 

72 
definition 

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

74 
[code func 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

75 

27551  76 
code_datatype Fract 
77 

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

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

80 
shows C 

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

82 

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

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

85 
shows "P q" 

86 
using assms by (cases q) simp 

87 

88 
lemma eq_rat: 

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

90 
and "\<And>a c. Fract a 0 = Fract c 0" 

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 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

103 
add_rat_def [code func 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 

107 
lemma add_rat: 

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 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

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

121 
lemma minus_rat: " Fract a b = Fract ( a) b" 

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 

128 
lemma minus_rat_cancel [simp]: 

129 
"Fract ( a) ( b) = Fract a b" 

130 
by (cases "b = 0") (simp_all add: eq_rat) 

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

131 

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

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

133 
diff_rat_def [code func del]: "q  r = q +  (r::rat)" 
18913  134 

27551  135 
lemma diff_rat: 
136 
assumes "b \<noteq> 0" and "d \<noteq> 0" 

137 
shows "Fract a b  Fract c d = Fract (a * d  c * b) (b * d)" 

138 
using assms by (simp add: diff_rat_def add_rat minus_rat) 

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

139 

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

140 
definition 
27551  141 
mult_rat_def [code func del]: 
142 
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 

143 
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

144 

27551  145 
lemma mult_rat: "Fract a b * Fract c d = Fract (a * c) (b * d)" 
146 
proof  

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

148 
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all 

149 
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

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

151 

27551  152 
lemma mult_rat_cancel [simp]: 
153 
assumes "c \<noteq> 0" 

154 
shows "Fract (c * a) (c * b) = Fract a b" 

155 
proof  

156 
from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) 

157 
then show ?thesis by (simp add: mult_rat [symmetric] mult_rat) 

158 
qed 

27509  159 

160 
primrec power_rat 

161 
where 

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

27509  164 

165 
instance proof 

27551  166 
fix q r s :: rat show "(q * r) * s = q * (r * s)" 
167 
by (cases q, cases r, cases s) (simp add: mult_rat eq_rat) 

168 
next 

169 
fix q r :: rat show "q * r = r * q" 

170 
by (cases q, cases r) (simp add: mult_rat eq_rat) 

171 
next 

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

173 
by (cases q) (simp add: One_rat_def mult_rat eq_rat) 

174 
next 

175 
fix q r s :: rat show "(q + r) + s = q + (r + s)" 

176 
by (cases q, cases r, cases s) (simp add: add_rat eq_rat ring_simps) 

177 
next 

178 
fix q r :: rat show "q + r = r + q" 

179 
by (cases q, cases r) (simp add: add_rat eq_rat) 

180 
next 

181 
fix q :: rat show "0 + q = q" 

182 
by (cases q) (simp add: Zero_rat_def add_rat eq_rat) 

183 
next 

184 
fix q :: rat show " q + q = 0" 

185 
by (cases q) (simp add: Zero_rat_def add_rat minus_rat eq_rat) 

186 
next 

187 
fix q r :: rat show "q  r = q +  r" 

188 
by (cases q, cases r) (simp add: diff_rat add_rat minus_rat eq_rat) 

189 
next 

190 
fix q r s :: rat show "(q + r) * s = q * s + r * s" 

191 
by (cases q, cases r, cases s) (simp add: add_rat mult_rat eq_rat ring_simps) 

192 
next 

193 
show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat) 

194 
next 

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

196 
by (cases q) (simp add: One_rat_def mult_rat eq_rat) 

197 
next 

27509  198 
fix q :: rat 
199 
fix n :: nat 

200 
show "q ^ 0 = 1" by simp 

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

202 
qed 

203 

204 
end 

205 

27551  206 
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" 
207 
by (induct k) (simp_all add: Zero_rat_def One_rat_def add_rat) 

208 

209 
lemma of_int_rat: "of_int k = Fract k 1" 

210 
by (cases k rule: int_diff_cases, simp add: of_nat_rat diff_rat) 

211 

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

213 
by (rule of_nat_rat [symmetric]) 

214 

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

216 
by (rule of_int_rat [symmetric]) 

217 

218 
instantiation rat :: number_ring 

219 
begin 

220 

221 
definition 

222 
rat_number_of_def [code func del]: "number_of w = Fract w 1" 

223 

224 
instance by intro_classes (simp add: rat_number_of_def of_int_rat) 

225 

226 
end 

227 

228 
lemma rat_number_collapse [code post]: 

229 
"Fract 0 k = 0" 

230 
"Fract 1 1 = 1" 

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

232 
"Fract k 0 = 0" 

233 
by (cases "k = 0") 

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

235 

236 
lemma rat_number_expand [code unfold]: 

237 
"0 = Fract 0 1" 

238 
"1 = Fract 1 1" 

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

240 
by (simp_all add: rat_number_collapse) 

241 

242 
lemma iszero_rat [simp]: 

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

244 
by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) 

245 

246 
lemma Rat_cases_nonzero [case_names Fract 0]: 

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

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

249 
shows C 

250 
proof (cases "q = 0") 

251 
case True then show C using 0 by auto 

252 
next 

253 
case False 

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

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

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

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

258 
qed 

259 

260 

261 

262 
subsubsection {* The field of rational numbers *} 

263 

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

265 
begin 

266 

267 
definition 

268 
inverse_rat_def [code func del]: 

269 
"inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. 

270 
ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" 

271 

272 
lemma inverse_rat: "inverse (Fract a b) = Fract b a" 

273 
proof  

274 
have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel" 

275 
by (auto simp add: congruent_def mult_commute) 

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

27509  277 
qed 
278 

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

281 

282 
lemma divide_rat: "Fract a b / Fract c d = Fract (a * d) (b * c)" 

283 
by (simp add: divide_rat_def inverse_rat mult_rat) 

284 

285 
instance proof 

286 
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand inverse_rat) 

287 
(simp add: rat_number_collapse) 

288 
next 

289 
fix q :: rat 

290 
assume "q \<noteq> 0" 

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

292 
(simp_all add: mult_rat inverse_rat rat_number_expand eq_rat) 

293 
next 

294 
fix q r :: rat 

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

296 
qed 

297 

298 
end 

299 

300 

301 
subsubsection {* Various *} 

302 

303 
lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1" 

304 
by (simp add: rat_number_expand add_rat) 

305 

306 
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" 

307 
by (simp add: Fract_of_int_eq [symmetric] divide_rat) 

308 

309 
lemma Fract_number_of_quotient [code post]: 

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

311 
unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. 

312 

313 

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

27509  315 

316 
instantiation rat :: linorder 

317 
begin 

318 

319 
definition 

320 
le_rat_def [code func del]: 

321 
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 

27551  322 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
323 

324 
lemma le_rat: 

325 
assumes "b \<noteq> 0" and "d \<noteq> 0" 

326 
shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" 

327 
proof  

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

329 
respects2 ratrel" 

330 
proof (clarsimp simp add: congruent2_def) 

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

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

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

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

335 

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

337 
{ 

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

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

340 
proof  

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

342 
hence "?le a b c d = 

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

344 
by (simp add: mult_le_cancel_right) 

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

346 
by (simp add: mult_ac) 

347 
finally show ?thesis . 

348 
qed 

349 
} note le_factor = this 

350 

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

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

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

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

355 
by (rule le_factor) 

356 
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 

357 
by (simp add: mult_ac) 

358 
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')" 

359 
by (simp only: eq1 eq2) 

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

361 
by (simp add: mult_ac) 

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

363 
by (rule le_factor [symmetric]) 

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

365 
qed 

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

367 
qed 

27509  368 

369 
definition 

370 
less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" 

371 

27551  372 
lemma less_rat: 
373 
assumes "b \<noteq> 0" and "d \<noteq> 0" 

374 
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" 

375 
using assms by (simp add: less_rat_def le_rat eq_rat order_less_le) 

27509  376 

377 
instance proof 

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

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

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

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

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

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

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

384 
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

385 
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

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

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

388 
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

389 
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

390 
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

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

392 
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

394 
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

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

396 
also have "... = (c * f) * (d * f) * (b * b)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

400 
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

402 
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

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

404 
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

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

406 
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

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

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

409 
qed 
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 
next 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

417 
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

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

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

420 
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

424 
from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

428 
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

429 
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

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

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

432 
qed 
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 
next 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

436 
by (induct q) (simp add: le_rat) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

437 
show "(q < r) = (q \<le> r \<and> q \<noteq> r)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

439 
show "q \<le> r \<or> r \<le> q" 
18913  440 
by (induct q, induct r) 
441 
(simp add: le_rat mult_commute, rule linorder_linear) 

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

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

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

444 

27509  445 
end 
446 

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

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

449 

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

450 
definition 
27551  451 
abs_rat_def: "\<bar>q\<bar> = (if q < 0 then q else (q::rat))" 
452 

453 
lemma abs_rat: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" 

454 
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) 

455 

456 
definition 

457 
sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else  1)" 

458 

459 
lemma sgn_rat: "sgn (Fract a b) = Fract (sgn a * sgn b) 1" 

460 
unfolding Fract_of_int_eq 

461 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat less_rat) 

462 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 

463 

464 
definition 

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

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

466 

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

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

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

469 

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

22456  472 

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

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

474 

27551  475 
instance rat :: ordered_field 
476 
proof 

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

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

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

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

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

481 
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

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

483 
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

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

485 
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

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

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

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

489 
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

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

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

492 
qed 
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 
show "q < r ==> 0 < s ==> s * q < s * r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

497 
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

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

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

500 
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

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

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

503 
from neq gt have "0 < ?E" 
23879  504 
by (auto simp add: Zero_rat_def less_rat le_rat order_less_le eq_rat) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

507 
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

509 
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

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

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

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

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

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

516 

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

519 
shows "P q" 

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

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

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

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

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

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

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

527 
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

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

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

530 
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

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

532 

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

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

534 
"0 < b ==> (0 < Fract a b) = (0 < a)" 
23879  535 
by (simp add: Zero_rat_def less_rat 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

536 

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

537 

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

539 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

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

542 

23342  543 

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

545 

24198  546 
class field_char_0 = field + ring_char_0 
23342  547 

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

27551  550 
context field_char_0 
551 
begin 

552 

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

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

27551  556 
end 
557 

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

562 
apply (simp only: of_int_mult [symmetric]) 

563 
done 

564 

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

23342  567 

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

569 
by (simp add: Zero_rat_def of_rat_rat) 

570 

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

572 
by (simp add: One_rat_def of_rat_rat) 

573 

574 
lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" 

575 
by (induct a, induct b, simp add: add_rat of_rat_rat add_frac_eq) 

576 

23343  577 
lemma of_rat_minus: "of_rat ( a) =  of_rat a" 
578 
by (induct a, simp add: minus_rat of_rat_rat) 

579 

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

581 
by (simp only: diff_minus of_rat_add of_rat_minus) 

582 

23342  583 
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" 
584 
apply (induct a, induct b, simp add: mult_rat of_rat_rat) 

585 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 

586 
done 

587 

588 
lemma nonzero_of_rat_inverse: 

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

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

23342  592 
done 
593 

594 
lemma of_rat_inverse: 

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

596 
inverse (of_rat a)" 

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

598 

599 
lemma nonzero_of_rat_divide: 

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

601 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

602 

603 
lemma of_rat_divide: 

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

605 
= of_rat a / of_rat b" 

606 
by (cases "b = 0", simp_all add: nonzero_of_rat_divide) 

607 

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

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

611 

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

613 
apply (induct a, induct b) 

614 
apply (simp add: of_rat_rat eq_rat) 

615 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

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

617 
done 

618 

619 
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] 

620 

621 
lemma of_rat_eq_id [simp]: "of_rat = (id :: rat \<Rightarrow> rat)" 

622 
proof 

623 
fix a 

624 
show "of_rat a = id a" 

625 
by (induct a) 

626 
(simp add: of_rat_rat divide_rat Fract_of_int_eq [symmetric]) 

627 
qed 

628 

629 
text{*Collapse nested embeddings*} 

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

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

632 

633 
lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" 

23365  634 
by (cases z rule: int_diff_cases, simp add: of_rat_diff) 
23343  635 

636 
lemma of_rat_number_of_eq [simp]: 

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

638 
by (simp add: number_of_eq) 

639 

23879  640 
lemmas zero_rat = Zero_rat_def 
641 
lemmas one_rat = One_rat_def 

642 

24198  643 
abbreviation 
644 
rat_of_nat :: "nat \<Rightarrow> rat" 

645 
where 

646 
"rat_of_nat \<equiv> of_nat" 

647 

648 
abbreviation 

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

650 
where 

651 
"rat_of_int \<equiv> of_int" 

652 

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

653 

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

654 
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

655 

27551  656 
lemma INum_Fract [simp]: "INum = split Fract" 
657 
by (auto simp add: expand_fun_eq INum_def Fract_of_int_quotient) 

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

658 

27551  659 
lemma split_Fract_normNum [simp]: "split Fract (normNum (k, l)) = Fract k l" 
660 
unfolding INum_Fract [symmetric] normNum by simp 

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

661 

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

662 
lemma [code]: 
27551  663 
"of_rat (Fract k l) = (if l \<noteq> 0 then of_int k / of_int l else 0)" 
664 
by (cases "l = 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

665 

26513  666 
instantiation rat :: eq 
667 
begin 

668 

27551  669 
definition [code func del]: "eq_class.eq (r\<Colon>rat) s \<longleftrightarrow> r  s = 0" 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

670 

26513  671 
instance by default (simp add: eq_rat_def) 
672 

27551  673 
lemma rat_eq_code [code]: "eq_class.eq (Fract k l) (Fract r s) \<longleftrightarrow> eq_class.eq (normNum (k, l)) (normNum (r, s))" 
674 
by (simp add: eq INum_normNum_iff [where ?'a = rat, symmetric]) 

26513  675 

676 
end 

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

677 

27551  678 
lemma rat_less_eq_code [code]: "Fract k l \<le> Fract r s \<longleftrightarrow> normNum (k, l) \<le>\<^sub>N normNum (r, s)" 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

679 
proof  
27551  680 
have "normNum (k, l) \<le>\<^sub>N normNum (r, s) \<longleftrightarrow> split Fract (normNum (k, l)) \<le> split Fract (normNum (r, s))" 
681 
by (simp add: INum_Fract [symmetric] del: INum_Fract normNum) 

682 
also have "\<dots> = (Fract k l \<le> Fract r s)" by simp 

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

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

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

685 

27551  686 
lemma rat_less_code [code]: "Fract k l < Fract r s \<longleftrightarrow> normNum (k, l) <\<^sub>N normNum (r, s)" 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

687 
proof  
27551  688 
have "normNum (k, l) <\<^sub>N normNum (r, s) \<longleftrightarrow> split Fract (normNum (k, l)) < split Fract (normNum (r, s))" 
689 
by (simp add: INum_Fract [symmetric] del: INum_Fract normNum) 

690 
also have "\<dots> = (Fract k l < Fract r s)" by simp 

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

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

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

693 

27551  694 
lemma rat_add_code [code]: "Fract k l + Fract r s = split Fract ((k, l) +\<^sub>N (r, s))" 
695 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp) 

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

696 

27551  697 
lemma rat_mul_code [code]: "Fract k l * Fract r s = split Fract ((k, l) *\<^sub>N (r, s))" 
698 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp) 

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

699 

27551  700 
lemma rat_neg_code [code]: " Fract k l = split Fract (~\<^sub>N (k, l))" 
701 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp) 

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

702 

27551  703 
lemma rat_sub_code [code]: "Fract k l  Fract r s = split Fract ((k, l) \<^sub>N (r, s))" 
704 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp) 

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

705 

27551  706 
lemma rat_inv_code [code]: "inverse (Fract k l) = split Fract (Ninv (k, l))" 
707 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp add: divide_rat_def) 

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

708 

27551  709 
lemma rat_div_code [code]: "Fract k l / Fract r s = split Fract ((k, l) \<div>\<^sub>N (r, s))" 
710 
by (simp add: INum_Fract [symmetric] del: INum_Fract, simp) 

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

711 

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

713 

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

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

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

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

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

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

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

723 
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

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

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

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

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

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

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

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

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

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

733 
val q' = q div g; 
25885  734 
val r = (if one_of [true, false] then p' else ~ p', 
735 
if p' = 0 then 0 else q') 

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

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

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

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

740 

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

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

743 

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

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

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

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

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

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

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

750 

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

751 
end 