author  nipkow 
Tue, 26 Aug 2008 12:07:06 +0200  
changeset 28001  4642317e0deb 
parent 27682  25aceefd4786 
child 28010  8312edc51969 
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 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

9 
imports "../Presburger" GCD 
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" 

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

90 
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

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

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

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

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

96 

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

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

99 

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

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

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

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

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

107 

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

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

111 
proof  

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

113 
respects2 ratrel" 

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

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

116 
qed 

18913  117 

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

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

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

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

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

125 
by (simp add: congruent_def) 

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

127 
qed 

128 

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

129 
lemma minus_rat_cancel [simp]: "Fract ( a) ( b) = Fract a b" 
27551  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 

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

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

138 
using assms by (simp add: diff_rat_def) 
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 

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

145 
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" 
27551  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 

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

152 
lemma mult_rat_cancel: 
27551  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) 

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

157 
then show ?thesis by (simp add: mult_rat [symmetric]) 
27551  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 

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

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

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

173 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  174 
next 
175 
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

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

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

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

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

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

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

191 
by (cases q, cases r, cases s) (simp add: eq_rat ring_simps) 
27551  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" 

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

196 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  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" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

209 
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

210 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  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 

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

272 
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" 
27551  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 

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

282 
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

283 
by (simp add: divide_rat_def) 
27551  284 

285 
instance proof 

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

286 
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand) 
27551  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" 

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

304 
by (simp add: rat_number_expand) 
27551  305 

306 
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

307 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  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 

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

313 
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

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

315 
unfolding Fract_of_int_quotient number_of_eq by simp 
27551  316 

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

27509  318 

319 
instantiation rat :: linorder 

320 
begin 

321 

322 
definition 

323 
le_rat_def [code func del]: 

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

27551  325 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
326 

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

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

330 
proof  

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

332 
respects2 ratrel" 

333 
proof (clarsimp simp add: congruent2_def) 

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

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

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

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

338 

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

340 
{ 

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

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

343 
proof  

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

345 
hence "?le a b c d = 

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

347 
by (simp add: mult_le_cancel_right) 

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

349 
by (simp add: mult_ac) 

350 
finally show ?thesis . 

351 
qed 

352 
} note le_factor = this 

353 

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

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

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

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

358 
by (rule le_factor) 

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

362 
by (simp only: eq1 eq2) 

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

364 
by (simp add: mult_ac) 

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

366 
by (rule le_factor [symmetric]) 

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

368 
qed 

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

370 
qed 

27509  371 

372 
definition 

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

374 

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

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

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

380 
instance proof 

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

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

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

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

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

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

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

387 
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

388 
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

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

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

391 
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

392 
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

393 
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

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

395 
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

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

397 
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

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

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

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

402 
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

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

404 
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

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

406 
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

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

408 
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

409 
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

410 
with neq show ?thesis by simp 
14365
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 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

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

419 
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

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

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

422 
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

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

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

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

426 
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

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

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

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

430 
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

431 
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

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

433 
with neq show ?thesis by (simp add: eq_rat) 
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 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

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

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

446 

27509  447 
end 
448 

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

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

451 

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

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

453 
abs_rat_def [code func del]: "\<bar>q\<bar> = (if q < 0 then q else (q::rat))" 
27551  454 

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

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

458 
definition 

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

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

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

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

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

466 
definition 

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

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

468 

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

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

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

471 

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

22456  474 

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

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

476 

27551  477 
instance rat :: ordered_field 
478 
proof 

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

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

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

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

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

483 
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

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

485 
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

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

487 
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

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

489 
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

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

491 
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

492 
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

493 
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

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

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

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

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

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

499 
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

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

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

502 
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

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

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

505 
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

506 
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

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

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

509 
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

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

511 
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

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

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

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

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

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

518 

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

521 
shows "P q" 

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

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

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

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

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

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

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

529 
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

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

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

532 
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

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

534 

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

535 
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

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

537 
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

538 

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

539 

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

541 

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

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

544 

23342  545 

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

547 

24198  548 
class field_char_0 = field + ring_char_0 
23342  549 

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

27551  552 
context field_char_0 
553 
begin 

554 

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

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

27551  558 
end 
559 

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

564 
apply (simp only: of_int_mult [symmetric]) 

565 
done 

566 

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

23342  569 

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

571 
by (simp add: Zero_rat_def of_rat_rat) 

572 

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

574 
by (simp add: One_rat_def of_rat_rat) 

575 

576 
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

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

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

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

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

583 
by (simp only: diff_minus of_rat_add of_rat_minus) 

584 

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

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

589 

590 
lemma nonzero_of_rat_inverse: 

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

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

23342  594 
done 
595 

596 
lemma of_rat_inverse: 

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

598 
inverse (of_rat a)" 

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

600 

601 
lemma nonzero_of_rat_divide: 

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

603 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

604 

605 
lemma of_rat_divide: 

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

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

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

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

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

613 

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

615 
apply (induct a, induct b) 

616 
apply (simp add: of_rat_rat eq_rat) 

617 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

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

619 
done 

620 

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

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

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

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

624 
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

625 
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

626 
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

627 
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

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

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

630 
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

631 
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

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

633 
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

634 
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

635 
(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

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

637 

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

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

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

640 
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

641 

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

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

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

647 
show "of_rat a = id a" 

648 
by (induct a) 

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

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

652 
text{*Collapse nested embeddings*} 

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

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

655 

656 
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

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

659 
lemma of_rat_number_of_eq [simp]: 

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

661 
by (simp add: number_of_eq) 

662 

23879  663 
lemmas zero_rat = Zero_rat_def 
664 
lemmas one_rat = One_rat_def 

665 

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

668 
where 

669 
"rat_of_nat \<equiv> of_nat" 

670 

671 
abbreviation 

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

673 
where 

674 
"rat_of_int \<equiv> of_int" 

675 

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 

682 
[code func del]: "Rats = range of_rat" 

683 

684 
notation (xsymbols) 

685 
Rats ("\<rat>") 

686 

687 
end 

688 

689 

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

690 
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

691 

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

692 
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

693 
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

694 
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

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

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

697 
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

698 
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

699 
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

700 
moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

702 
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

703 
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

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

705 
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

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

707 

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

708 
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

709 
[simp, code func del]: "Fract_norm a b = Fract a b" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

710 

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

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

712 
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

713 
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

714 

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

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

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

717 
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

718 

26513  719 
instantiation rat :: eq 
720 
begin 

721 

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

722 
definition [code func 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

723 

26513  724 
instance by default (simp add: eq_rat_def) 
725 

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

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

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

728 
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

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

730 
then a = 0 \<or> b = 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

731 
else a * d = b * c)" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

732 
by (auto simp add: eq eq_rat) 
26513  733 

734 
end 

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

735 

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

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

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

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

739 
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

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

741 
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

742 
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

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

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

745 
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

746 
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

747 
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

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

749 
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

750 
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

751 
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

752 
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

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

754 
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

755 
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

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

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

758 

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

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

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

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

762 
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

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

764 
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

765 
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

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

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

768 
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

769 
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

770 
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

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

772 
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

773 
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

774 
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

775 
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

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

777 
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

778 
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

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

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

781 

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

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

783 
"Fract a b \<le> 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

784 
then sgn c * sgn d \<ge> 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

786 
then sgn a * sgn b \<le> 0 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

787 
else 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

788 
by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

789 
(auto simp add: sgn_times sgn_0_0 le_less sgn_1_pos [symmetric] sgn_1_neg [symmetric]) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

790 

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

791 
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

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

793 
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

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

795 
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

796 
else 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

797 
by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

798 
(auto simp add: sgn_times sgn_0_0 sgn_1_pos [symmetric] sgn_1_neg [symmetric], 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

799 
auto simp add: sgn_1_pos) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

800 

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

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

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

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

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

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

806 
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

807 
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

808 

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

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

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

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

812 

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

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

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

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

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

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

818 
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

819 
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

820 

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

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

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

823 
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

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

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

826 

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

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

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

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

830 

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

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

832 

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

834 

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

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

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

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

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

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

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

844 
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

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

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

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

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

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

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

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

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

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

854 
val q' = q div g; 
25885  855 
val r = (if one_of [true, false] then p' else ~ p', 
856 
if p' = 0 then 0 else q') 

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

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

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

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

861 

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

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

864 

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

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

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

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

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

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

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

871 

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

872 
end 