author  wenzelm 
Mon, 26 Oct 2009 20:02:37 +0100  
changeset 33209  d36ca3960e33 
parent 33197  de6285ebcc05 
child 33805  0461a101e27e 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

1 
(* Title: HOL/Rational.thy 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

4 

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

6 

15131  7 
theory Rational 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

8 
imports GCD Archimedean_Field 
15131  9 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

10 

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

12 

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

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

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

16 
ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where 
27551  17 
"ratrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

18 

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

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

22 

30198  23 
lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel" 
24 
by (auto simp add: refl_on_def ratrel_def) 

18913  25 

26 
lemma sym_ratrel: "sym ratrel" 

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

28 

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

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

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

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

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

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

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

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

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

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

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

42 
with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto 

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

43 
qed 
27551  44 

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

30198  46 
by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel]) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

47 

18913  48 
lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] 
49 
lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] 

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

50 

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

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

54 
by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms) 

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

55 

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

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

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

60 
qed 

61 

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

63 
by (simp add: Rat_def quotientI) 

64 

65 
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] 

66 

67 

68 
subsubsection {* Representation and basic operations *} 

69 

70 
definition 

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

28562  72 
[code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

73 

27551  74 
code_datatype Fract 
75 

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

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

78 
shows C 

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

80 

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

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

83 
shows "P q" 

84 
using assms by (cases q) simp 

85 

86 
lemma eq_rat: 

87 
shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" 

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

88 
and "\<And>a. Fract a 0 = Fract 0 1" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

31017  92 
instantiation rat :: comm_ring_1 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

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

94 

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

95 
definition 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

96 
Zero_rat_def [code, code_unfold]: "0 = Fract 0 1" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

97 

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

98 
definition 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

99 
One_rat_def [code, code_unfold]: "1 = Fract 1 1" 
18913  100 

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

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

105 

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

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

109 
proof  

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

111 
respects2 ratrel" 

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

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

114 
qed 

18913  115 

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

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

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

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

123 
by (simp add: congruent_def) 

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

125 
qed 

126 

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

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

129 

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

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

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

133 
lemma diff_rat [simp]: 
27551  134 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
135 
shows "Fract a b  Fract c d = Fract (a * d  c * b) (b * d)" 

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

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

137 

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

138 
definition 
28562  139 
mult_rat_def [code del]: 
27551  140 
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
141 
ratrel``{(fst x * fst y, snd x * snd y)})" 

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

142 

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

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

146 
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all 

147 
then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2) 

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

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

149 

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

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

153 
proof  

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

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

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

158 
instance proof 

27668  159 
fix q r s :: rat show "(q * r) * s = q * (r * s)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

160 
by (cases q, cases r, cases s) (simp add: eq_rat) 
27551  161 
next 
162 
fix q r :: rat show "q * r = r * q" 

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

163 
by (cases q, cases r) (simp add: eq_rat) 
27551  164 
next 
165 
fix q :: rat show "1 * q = q" 

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

166 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  167 
next 
168 
fix q r s :: rat show "(q + r) + s = q + (r + s)" 

29667  169 
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) 
27551  170 
next 
171 
fix q r :: rat show "q + r = r + q" 

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

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

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

175 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  176 
next 
177 
fix q :: rat show " q + q = 0" 

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

178 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  179 
next 
180 
fix q r :: rat show "q  r = q +  r" 

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

181 
by (cases q, cases r) (simp add: eq_rat) 
27551  182 
next 
183 
fix q r s :: rat show "(q + r) * s = q * s + r * s" 

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

27509  187 
qed 
188 

189 
end 

190 

27551  191 
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

192 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  193 

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

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

195 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  196 

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

198 
by (rule of_nat_rat [symmetric]) 

199 

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

201 
by (rule of_int_rat [symmetric]) 

202 

203 
instantiation rat :: number_ring 

204 
begin 

205 

206 
definition 

28562  207 
rat_number_of_def [code del]: "number_of w = Fract w 1" 
27551  208 

30960  209 
instance proof 
210 
qed (simp add: rat_number_of_def of_int_rat) 

27551  211 

212 
end 

213 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

214 
lemma rat_number_collapse [code_post]: 
27551  215 
"Fract 0 k = 0" 
216 
"Fract 1 1 = 1" 

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

218 
"Fract k 0 = 0" 

219 
by (cases "k = 0") 

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

221 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

222 
lemma rat_number_expand [code_unfold]: 
27551  223 
"0 = Fract 0 1" 
224 
"1 = Fract 1 1" 

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

226 
by (simp_all add: rat_number_collapse) 

227 

228 
lemma iszero_rat [simp]: 

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

230 
by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) 

231 

232 
lemma Rat_cases_nonzero [case_names Fract 0]: 

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

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

235 
shows C 

236 
proof (cases "q = 0") 

237 
case True then show C using 0 by auto 

238 
next 

239 
case False 

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

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

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

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

244 
qed 

245 

246 

247 
subsubsection {* The field of rational numbers *} 

248 

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

250 
begin 

251 

252 
definition 

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

256 

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

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

260 
by (auto simp add: congruent_def mult_commute) 

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

27509  262 
qed 
263 

27551  264 
definition 
28562  265 
divide_rat_def [code del]: "q / r = q * inverse (r::rat)" 
27551  266 

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

267 
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

268 
by (simp add: divide_rat_def) 
27551  269 

270 
instance proof 

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

271 
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand) 
27551  272 
(simp add: rat_number_collapse) 
273 
next 

274 
fix q :: rat 

275 
assume "q \<noteq> 0" 

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

277 
(simp_all add: mult_rat inverse_rat rat_number_expand eq_rat) 

278 
next 

279 
fix q r :: rat 

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

281 
qed 

282 

283 
end 

284 

285 

286 
subsubsection {* Various *} 

287 

288 
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

289 
by (simp add: rat_number_expand) 
27551  290 

291 
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

292 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  293 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

294 
lemma Fract_number_of_quotient [code_post]: 
27551  295 
"Fract (number_of k) (number_of l) = number_of k / number_of l" 
296 
unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. 

297 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31707
diff
changeset

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

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

300 
unfolding Fract_of_int_quotient number_of_eq by simp 
27551  301 

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

27509  303 

304 
instantiation rat :: linorder 

305 
begin 

306 

307 
definition 

28562  308 
le_rat_def [code del]: 
27509  309 
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
27551  310 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
311 

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

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

315 
proof  

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

317 
respects2 ratrel" 

318 
proof (clarsimp simp add: congruent2_def) 

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

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

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

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

323 

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

325 
{ 

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

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

328 
proof  

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

330 
hence "?le a b c d = 

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

332 
by (simp add: mult_le_cancel_right) 

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

334 
by (simp add: mult_ac) 

335 
finally show ?thesis . 

336 
qed 

337 
} note le_factor = this 

338 

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

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

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

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

343 
by (rule le_factor) 

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

347 
by (simp only: eq1 eq2) 

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

349 
by (simp add: mult_ac) 

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

351 
by (rule le_factor [symmetric]) 

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

353 
qed 

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

355 
qed 

27509  356 

357 
definition 

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

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

360 
lemma less_rat [simp]: 
27551  361 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
362 
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

363 
using assms by (simp add: less_rat_def eq_rat order_less_le) 
27509  364 

365 
instance proof 

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

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

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

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

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

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

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

372 
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

373 
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

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

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

376 
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

377 
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

378 
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

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

380 
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

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

382 
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

383 
qed 
27668  384 
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

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

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

387 
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

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

389 
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

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

391 
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

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

393 
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

394 
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

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

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

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

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

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

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

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

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

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

404 
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

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

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

407 
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

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

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

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

411 
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

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

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

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

415 
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

416 
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

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

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

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

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

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

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

423 
by (induct q) simp 
27682  424 
show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" 
425 
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

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

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

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

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

431 

27509  432 
end 
433 

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

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

436 

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

437 
definition 
28562  438 
abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then q else (q::rat))" 
27551  439 

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

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

443 
definition 

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

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

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

448 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  449 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
450 

451 
definition 

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

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

453 

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

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

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

456 

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

22456  459 

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

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

461 

27551  462 
instance rat :: ordered_field 
463 
proof 

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

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

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

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

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

468 
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

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

470 
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

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

472 
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

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

474 
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

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

476 
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

477 
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

478 
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

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

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

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

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

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

484 
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

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

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

487 
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

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

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

490 
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

491 
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

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

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

494 
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

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

496 
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

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

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

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

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

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

503 

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

506 
shows "P q" 

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

507 
proof (cases q) 
27551  508 
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

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

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

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

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

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

514 
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

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

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

517 
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

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

519 

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

520 
lemma zero_less_Fract_iff: 
30095
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

521 
"0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

522 
by (simp add: Zero_rat_def zero_less_mult_iff) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

523 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

524 
lemma Fract_less_zero_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

525 
"0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

526 
by (simp add: Zero_rat_def mult_less_0_iff) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

527 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

528 
lemma zero_le_Fract_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

529 
"0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

530 
by (simp add: Zero_rat_def zero_le_mult_iff) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

531 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

532 
lemma Fract_le_zero_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

533 
"0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

534 
by (simp add: Zero_rat_def mult_le_0_iff) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

535 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

536 
lemma one_less_Fract_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

537 
"0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

538 
by (simp add: One_rat_def mult_less_cancel_right_disj) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

539 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

540 
lemma Fract_less_one_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

541 
"0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

542 
by (simp add: One_rat_def mult_less_cancel_right_disj) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

543 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

544 
lemma one_le_Fract_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

545 
"0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

546 
by (simp add: One_rat_def mult_le_cancel_right) 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

547 

c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

548 
lemma Fract_le_one_iff: 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

549 
"0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" 
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset

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

551 

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

552 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

553 
subsubsection {* Rationals are an Archimedean field *} 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

554 

57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

555 
lemma rat_floor_lemma: 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

556 
assumes "0 < b" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

557 
shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

558 
proof  
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

559 
have "Fract a b = of_int (a div b) + Fract (a mod b) b" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

560 
using `0 < b` by (simp add: of_int_rat) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

561 
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

562 
using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

563 
ultimately show ?thesis by simp 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

564 
qed 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

565 

57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

566 
instance rat :: archimedean_field 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

567 
proof 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

568 
fix r :: rat 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

569 
show "\<exists>z. r \<le> of_int z" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

570 
proof (induct r) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

571 
case (Fract a b) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

572 
then have "Fract a b \<le> of_int (a div b + 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

573 
using rat_floor_lemma [of b a] by simp 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

574 
then show "\<exists>z. Fract a b \<le> of_int z" .. 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

575 
qed 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

576 
qed 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

577 

57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

578 
lemma floor_Fract: 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

579 
assumes "0 < b" shows "floor (Fract a b) = a div b" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

580 
using rat_floor_lemma [OF `0 < b`, of a] 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

581 
by (simp add: floor_unique) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

582 

57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

583 

31100  584 
subsection {* Linear arithmetic setup *} 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

585 

31100  586 
declaration {* 
587 
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 

588 
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) 

589 
#> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] 

590 
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) 

591 
#> Lin_Arith.add_simps [@{thm neg_less_iff_less}, 

592 
@{thm True_implies_equals}, 

593 
read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, 

594 
@{thm divide_1}, @{thm divide_zero_left}, 

595 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 

596 
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, 

597 
@{thm of_int_minus}, @{thm of_int_diff}, 

598 
@{thm of_int_of_nat_eq}] 

599 
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors 

600 
#> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) 

601 
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) 

602 
*} 

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

603 

23342  604 

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

606 

24198  607 
class field_char_0 = field + ring_char_0 
23342  608 

27551  609 
subclass (in ordered_field) field_char_0 .. 
23342  610 

27551  611 
context field_char_0 
612 
begin 

613 

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

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

27551  617 
end 
618 

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

623 
apply (simp only: of_int_mult [symmetric]) 

624 
done 

625 

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

23342  628 

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

630 
by (simp add: Zero_rat_def of_rat_rat) 

631 

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

633 
by (simp add: One_rat_def of_rat_rat) 

634 

635 
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

636 
by (induct a, induct b, simp add: of_rat_rat add_frac_eq) 
23342  637 

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

639 
by (induct a, simp add: of_rat_rat) 
23343  640 

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

642 
by (simp only: diff_minus of_rat_add of_rat_minus) 

643 

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

645 
apply (induct a, induct b, simp add: of_rat_rat) 
23342  646 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 
647 
done 

648 

649 
lemma nonzero_of_rat_inverse: 

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

23343  651 
apply (rule inverse_unique [symmetric]) 
652 
apply (simp add: of_rat_mult [symmetric]) 

23342  653 
done 
654 

655 
lemma of_rat_inverse: 

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

657 
inverse (of_rat a)" 

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

659 

660 
lemma nonzero_of_rat_divide: 

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

662 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

663 

664 
lemma of_rat_divide: 

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

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

667 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
23342  668 

23343  669 
lemma of_rat_power: 
31017  670 
"(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

671 
by (induct n) (simp_all add: of_rat_mult) 
23343  672 

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

674 
apply (induct a, induct b) 

675 
apply (simp add: of_rat_rat eq_rat) 

676 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

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

678 
done 

679 

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

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

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

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

683 
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

684 
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

685 
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

686 
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

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

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

689 
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

690 
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

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

692 
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

693 
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

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

695 

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

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

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

698 
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

699 

23343  700 
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] 
701 

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

702 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  703 
proof 
704 
fix a 

705 
show "of_rat a = id a" 

706 
by (induct a) 

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

707 
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) 
23343  708 
qed 
709 

710 
text{*Collapse nested embeddings*} 

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

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

713 

714 
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

715 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  716 

717 
lemma of_rat_number_of_eq [simp]: 

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

719 
by (simp add: number_of_eq) 

720 

23879  721 
lemmas zero_rat = Zero_rat_def 
722 
lemmas one_rat = One_rat_def 

723 

24198  724 
abbreviation 
725 
rat_of_nat :: "nat \<Rightarrow> rat" 

726 
where 

727 
"rat_of_nat \<equiv> of_nat" 

728 

729 
abbreviation 

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

731 
where 

732 
"rat_of_int \<equiv> of_int" 

733 

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

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

735 

28001  736 
context field_char_0 
737 
begin 

738 

739 
definition 

740 
Rats :: "'a set" where 

28562  741 
[code del]: "Rats = range of_rat" 
28001  742 

743 
notation (xsymbols) 

744 
Rats ("\<rat>") 

745 

746 
end 

747 

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

748 
lemma Rats_of_rat [simp]: "of_rat r \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

750 

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

751 
lemma Rats_of_int [simp]: "of_int z \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

752 
by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

753 

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

754 
lemma Rats_of_nat [simp]: "of_nat n \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

755 
by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

756 

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

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

758 
"(number_of w::'a::{number_ring,field_char_0}) \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

759 
by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat) 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

760 

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

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

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

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

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

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

766 

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

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

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

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

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

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

772 

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

773 
lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

778 

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

779 
lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow>  a \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

784 

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

785 
lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a  b \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

790 

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

791 
lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

796 

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

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

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

799 
shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

804 

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

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

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

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

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

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

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

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

812 

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

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

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

815 
shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

820 

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

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

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

823 
shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

828 

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

829 
lemma Rats_power [simp]: 
31017  830 
fixes a :: "'a::field_char_0" 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

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

836 

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

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

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

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

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

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

842 
from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def . 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

846 

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

847 
lemma Rats_induct [case_names of_rat, induct set: Rats]: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

848 
"q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

850 

28001  851 

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

852 
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

853 

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

855 
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

856 
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

857 
next 
31706  858 
let ?c = "gcd a b" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

859 
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

860 
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

861 
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

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

864 
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

865 
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

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

867 
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

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

869 

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

870 
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where 
28562  871 
[simp, code del]: "Fract_norm a b = Fract a b" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

872 

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

874 
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

875 
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

876 

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

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

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

879 
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

880 

26513  881 
instantiation rat :: eq 
882 
begin 

883 

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

885 

26513  886 
instance by default (simp add: eq_rat_def) 
887 

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

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

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

890 
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

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

892 
then a = 0 \<or> b = 0 
29332  893 
else a * d = b * c)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

894 
by (auto simp add: eq eq_rat) 
26513  895 

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

898 
by (rule HOL.eq_refl) 

899 

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

901 

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

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

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

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

905 
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

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

907 
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

908 
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

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

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

911 
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

912 
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

913 
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

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

915 
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

916 
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

917 
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

918 
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

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

920 
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

921 
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

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

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

924 

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

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

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

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

928 
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

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

930 
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

931 
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

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

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

934 
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

935 
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

936 
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

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

938 
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

939 
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

940 
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

941 
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

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

943 
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

944 
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

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

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

947 

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

950 
unfolding sgn_if by auto 

951 

952 
lemma (in ordered_idom) sgn_less [simp]: 

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

954 
unfolding sgn_if by auto 

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

955 

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

956 
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

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

958 
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

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

960 
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

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

964 
lemma rat_less_eq_code [code]: 

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

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

967 
else if d = 0 

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

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

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

971 
(auto simp add: le_less not_less sgn_0_0) 

972 

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

973 

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

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

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

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

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

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

979 
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

980 
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

981 

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

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

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

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

985 

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

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

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

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

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

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

991 
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

992 
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

993 

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

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

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

996 
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

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

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

999 

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

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

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

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

1003 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1004 
definition (in term_syntax) 
32657  1005 
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where 
1006 
[code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l" 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1007 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1008 
notation fcomp (infixl "o>" 60) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1009 
notation scomp (infixl "o\<rightarrow>" 60) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1010 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1011 
instantiation rat :: random 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1012 
begin 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1013 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1014 
definition 
31641  1015 
"Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair ( 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

1016 
let j = Code_Numeral.int_of (denom + 1) 
32657  1017 
in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1018 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1019 
instance .. 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1020 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1021 
end 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1022 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1023 
no_notation fcomp (infixl "o>" 60) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1024 
no_notation scomp (infixl "o\<rightarrow>" 60) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset

1025 

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

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

1027 

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

1029 

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

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

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

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

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

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

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

1039 
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

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

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

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

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

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

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

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

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

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

1049 
val q' = q div g; 
25885  1050 
val r = (if one_of [true, false] then p' else ~ p', 
31666  1051 
if p' = 0 then 1 else q') 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

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

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

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

1056 

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

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

1059 

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

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

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

1062 
attach {* 
31674  1063 
fun rat_of_int i = (i, 1); 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

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

1065 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1066 
setup {* 
33209  1067 
Nitpick.register_frac_type @{type_name rat} 
1068 
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), 

1069 
(@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), 

1070 
(@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), 

1071 
(@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), 

1072 
(@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), 

1073 
(@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}), 

1074 
(@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), 

1075 
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), 

1076 
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}), 

1077 
(@{const_name field_char_0_class.Rats}, @{const_name UNIV})] 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1078 
*} 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1079 

de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1080 
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat 
33209  1081 
number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat 
1082 
plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat 

1083 
zero_rat_inst.zero_rat 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1084 

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

1085 
end 