author  haftmann 
Fri, 14 Jun 2019 08:34:27 +0000  
changeset 70344  050104f01bf9 
parent 69593  3dda49e08b9d 
child 70345  80a1aa30e24d 
permissions  rwrr 
63494  1 
(* Title: HOL/Rat.thy 
2 
Author: Markus Wenzel, TU Muenchen 

14365
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 

60758  5 
section \<open>Rational numbers\<close> 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

6 

35372  7 
theory Rat 
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
64849
diff
changeset

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

10 

60758  11 
subsection \<open>Rational numbers as quotient\<close> 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

12 

60758  13 
subsubsection \<open>Construction of the type of rational numbers\<close> 
18913  14 

63326  15 
definition ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" 
16 
where "ratrel = (\<lambda>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

17 

63326  18 
lemma ratrel_iff [simp]: "ratrel x y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x" 
27551  19 
by (simp add: ratrel_def) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

20 

47906  21 
lemma exists_ratrel_refl: "\<exists>x. ratrel x x" 
22 
by (auto intro!: one_neq_zero) 

18913  23 

47906  24 
lemma symp_ratrel: "symp ratrel" 
25 
by (simp add: ratrel_def symp_def) 

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

26 

47906  27 
lemma transp_ratrel: "transp ratrel" 
28 
proof (rule transpI, unfold split_paired_all) 

27551  29 
fix a b a' b' a'' b'' :: int 
63494  30 
assume *: "ratrel (a, b) (a', b')" 
31 
assume **: "ratrel (a', b') (a'', b'')" 

27551  32 
have "b' * (a * b'') = b'' * (a * b')" by simp 
63494  33 
also from * have "a * b' = a' * b" by auto 
27551  34 
also have "b'' * (a' * b) = b * (a' * b'')" by simp 
63494  35 
also from ** have "a' * b'' = a'' * b'" by auto 
27551  36 
also have "b * (a'' * b') = b' * (a'' * b)" by simp 
37 
finally have "b' * (a * b'') = b' * (a'' * b)" . 

63494  38 
moreover from ** have "b' \<noteq> 0" by auto 
27551  39 
ultimately have "a * b'' = a'' * b" by simp 
63494  40 
with * ** show "ratrel (a, b) (a'', b'')" by auto 
27551  41 
qed 
42 

47906  43 
lemma part_equivp_ratrel: "part_equivp ratrel" 
44 
by (rule part_equivpI [OF exists_ratrel_refl symp_ratrel transp_ratrel]) 

45 

46 
quotient_type rat = "int \<times> int" / partial: "ratrel" 

47 
morphisms Rep_Rat Abs_Rat 

48 
by (rule part_equivp_ratrel) 

27551  49 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
52146
diff
changeset

50 
lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\<lambda>x. snd x \<noteq> 0)" 
63326  51 
by (simp add: rat.domain_eq) 
52 

27551  53 

60758  54 
subsubsection \<open>Representation and basic operations\<close> 
27551  55 

47906  56 
lift_definition Fract :: "int \<Rightarrow> int \<Rightarrow> rat" 
57 
is "\<lambda>a b. if b = 0 then (0, 1) else (a, b)" 

58 
by simp 

27551  59 

60 
lemma eq_rat: 

63326  61 
"\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" 
62 
"\<And>a. Fract a 0 = Fract 0 1" 

63 
"\<And>a c. Fract 0 a = Fract 0 c" 

47906  64 
by (transfer, simp)+ 
27551  65 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

66 
lemma Rat_cases [case_names Fract, cases type: rat]: 
63326  67 
assumes that: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

68 
shows C 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

69 
proof  
63326  70 
obtain a b :: int where q: "q = Fract a b" and b: "b \<noteq> 0" 
47906  71 
by transfer simp 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

72 
let ?a = "a div gcd a b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

73 
let ?b = "b div gcd a b" 
63326  74 
from b have "?b * gcd a b = b" 
58834  75 
by simp 
63326  76 
with b have "?b \<noteq> 0" 
77 
by fastforce 

78 
with q b have q2: "q = Fract ?a ?b" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57275
diff
changeset

79 
by (simp add: eq_rat dvd_div_mult mult.commute [of a]) 
63326  80 
from b have coprime: "coprime ?a ?b" 
62348  81 
by (auto intro: div_gcd_coprime) 
63326  82 
show C 
83 
proof (cases "b > 0") 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

84 
case True 
63326  85 
then have "?b > 0" 
86 
by (simp add: nonneg1_imp_zdiv_pos_iff) 

87 
from q2 this coprime show C by (rule that) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

88 
next 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

89 
case False 
63326  90 
have "q = Fract ( ?a) ( ?b)" 
91 
unfolding q2 by transfer simp 

92 
moreover from False b have " ?b > 0" 

93 
by (simp add: pos_imp_zdiv_neg_iff) 

94 
moreover from coprime have "coprime ( ?a) ( ?b)" 

95 
by simp 

96 
ultimately show C 

97 
by (rule that) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

98 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

99 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

100 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

101 
lemma Rat_induct [case_names Fract, induct type: rat]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

102 
assumes "\<And>a b. b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> P (Fract a b)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

103 
shows "P q" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

104 
using assms by (cases q) simp 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

105 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59667
diff
changeset

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

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

108 

47906  109 
lift_definition zero_rat :: "rat" is "(0, 1)" 
110 
by simp 

111 

112 
lift_definition one_rat :: "rat" is "(1, 1)" 

113 
by simp 

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

114 

47906  115 
lemma Zero_rat_def: "0 = Fract 0 1" 
116 
by transfer simp 

18913  117 

47906  118 
lemma One_rat_def: "1 = Fract 1 1" 
119 
by transfer simp 

120 

121 
lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" 

122 
is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)" 

63494  123 
by (auto simp: distrib_right) (simp add: ac_simps) 
27551  124 

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

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

47906  128 
using assms by transfer simp 
18913  129 

47906  130 
lift_definition uminus_rat :: "rat \<Rightarrow> rat" is "\<lambda>x. ( fst x, snd x)" 
131 
by simp 

27551  132 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

133 
lemma minus_rat [simp]: " Fract a b = Fract ( a) b" 
47906  134 
by transfer simp 
27551  135 

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

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

138 

63326  139 
definition diff_rat_def: "q  r = q +  r" for q r :: rat 
18913  140 

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

141 
lemma diff_rat [simp]: 
63494  142 
"b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b  Fract c d = Fract (a * d  c * b) (b * d)" 
143 
by (simp add: diff_rat_def) 

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

144 

47906  145 
lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" 
146 
is "\<lambda>x y. (fst x * fst y, snd x * snd y)" 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

148 

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

149 
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" 
47906  150 
by transfer simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

151 

63494  152 
lemma mult_rat_cancel: "c \<noteq> 0 \<Longrightarrow> Fract (c * a) (c * b) = Fract a b" 
153 
by transfer simp 

47906  154 

155 
lift_definition inverse_rat :: "rat \<Rightarrow> rat" 

156 
is "\<lambda>x. if fst x = 0 then (0, 1) else (snd x, fst x)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57275
diff
changeset

157 
by (auto simp add: mult.commute) 
47906  158 

159 
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" 

160 
by transfer simp 

161 

63326  162 
definition divide_rat_def: "q div r = q * inverse r" for q r :: rat 
47906  163 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60352
diff
changeset

164 
lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" 
47906  165 
by (simp add: divide_rat_def) 
27509  166 

63326  167 
instance 
168 
proof 

47906  169 
fix q r s :: rat 
170 
show "(q * r) * s = q * (r * s)" 

171 
by transfer simp 

172 
show "q * r = r * q" 

173 
by transfer simp 

174 
show "1 * q = q" 

175 
by transfer simp 

176 
show "(q + r) + s = q + (r + s)" 

177 
by transfer (simp add: algebra_simps) 

178 
show "q + r = r + q" 

179 
by transfer simp 

180 
show "0 + q = q" 

181 
by transfer simp 

182 
show " q + q = 0" 

183 
by transfer simp 

184 
show "q  r = q +  r" 

185 
by (fact diff_rat_def) 

186 
show "(q + r) * s = q * s + r * s" 

187 
by transfer (simp add: algebra_simps) 

188 
show "(0::rat) \<noteq> 1" 

189 
by transfer simp 

63326  190 
show "inverse q * q = 1" if "q \<noteq> 0" 
191 
using that by transfer simp 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60352
diff
changeset

192 
show "q div r = q * inverse r" 
47906  193 
by (fact divide_rat_def) 
194 
show "inverse 0 = (0::rat)" 

195 
by transfer simp 

27509  196 
qed 
197 

198 
end 

199 

63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

200 
(* We cannot state these two rules earlier because of pending sort hypotheses *) 
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

201 
lemma div_add_self1_no_field [simp]: 
66806
a4e82b58d833
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
haftmann
parents:
65552
diff
changeset

202 
assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0" 
63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

203 
shows "(b + a) div b = a div b + 1" 
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

204 
using assms(2) by (fact div_add_self1) 
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

205 

9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

206 
lemma div_add_self2_no_field [simp]: 
66806
a4e82b58d833
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
haftmann
parents:
65552
diff
changeset

207 
assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0" 
63499
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

208 
shows "(a + b) div b = a div b + 1" 
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

209 
using assms(2) by (fact div_add_self2) 
9c9a59949887
Tuned looping simp rules in semiring_div
eberlm <eberlm@in.tum.de>
parents:
63326
diff
changeset

210 

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

212 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  213 

214 
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

215 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  216 

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

218 
by (rule of_nat_rat [symmetric]) 

219 

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

221 
by (rule of_int_rat [symmetric]) 

222 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

223 
lemma rat_number_collapse: 
27551  224 
"Fract 0 k = 0" 
225 
"Fract 1 1 = 1" 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

226 
"Fract (numeral w) 1 = numeral w" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

227 
"Fract ( numeral w) 1 =  numeral w" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

228 
"Fract ( 1) 1 =  1" 
27551  229 
"Fract k 0 = 0" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

230 
using Fract_of_int_eq [of "numeral w"] 
63494  231 
and Fract_of_int_eq [of " numeral w"] 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

232 
by (simp_all add: Zero_rat_def One_rat_def eq_rat) 
27551  233 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

234 
lemma rat_number_expand: 
27551  235 
"0 = Fract 0 1" 
236 
"1 = Fract 1 1" 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

237 
"numeral k = Fract (numeral k) 1" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

238 
" 1 = Fract ( 1) 1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

239 
" numeral k = Fract ( numeral k) 1" 
27551  240 
by (simp_all add: rat_number_collapse) 
241 

242 
lemma Rat_cases_nonzero [case_names Fract 0]: 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

243 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
63326  244 
and 0: "q = 0 \<Longrightarrow> C" 
27551  245 
shows C 
246 
proof (cases "q = 0") 

63326  247 
case True 
248 
then show C using 0 by auto 

27551  249 
next 
250 
case False 

63326  251 
then obtain a b where *: "q = Fract a b" "b > 0" "coprime a b" 
252 
by (cases q) auto 

253 
with False have "0 \<noteq> Fract a b" 

254 
by simp 

255 
with \<open>b > 0\<close> have "a \<noteq> 0" 

256 
by (simp add: Zero_rat_def eq_rat) 

257 
with Fract * show C by blast 

27551  258 
qed 
259 

63326  260 

61799  261 
subsubsection \<open>Function \<open>normalize\<close>\<close> 
33805  262 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

263 
lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

264 
proof (cases "b = 0") 
63326  265 
case True 
63494  266 
then show ?thesis 
267 
by (simp add: eq_rat) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

268 
next 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

269 
case False 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

270 
moreover have "b div gcd a b * gcd a b = b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

271 
by (rule dvd_div_mult_self) simp 
63326  272 
ultimately have "b div gcd a b * gcd a b \<noteq> 0" 
273 
by simp 

274 
then have "b div gcd a b \<noteq> 0" 

275 
by fastforce 

276 
with False show ?thesis 

277 
by (simp add: eq_rat dvd_div_mult mult.commute [of a]) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

278 
qed 
33805  279 

63326  280 
definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" 
281 
where "normalize p = 

282 
(if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

283 
else if snd p = 0 then (0, 1) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

284 
else (let a =  gcd (fst p) (snd p) in (fst p div a, snd p div a)))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

285 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

286 
lemma normalize_crossproduct: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

287 
assumes "q \<noteq> 0" "s \<noteq> 0" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

288 
assumes "normalize (p, q) = normalize (r, s)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

289 
shows "p * s = r * q" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

290 
proof  
63326  291 
have *: "p * s = q * r" 
292 
if "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

293 
proof  
63494  294 
from that have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = 
295 
(q * gcd r s) * (sgn (q * s) * r * gcd p q)" 

63326  296 
by simp 
297 
with assms show ?thesis 

64240  298 
by (auto simp add: ac_simps sgn_mult sgn_0_0) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

299 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

300 
from assms show ?thesis 
64240  301 
by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult 
63326  302 
split: if_splits intro: *) 
33805  303 
qed 
304 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

305 
lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" 
63494  306 
by (auto simp: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse 
63326  307 
split: if_split_asm) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

308 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

309 
lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0" 
63494  310 
by (auto simp: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff 
63326  311 
split: if_split_asm) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

312 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

313 
lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q" 
63494  314 
by (auto simp: normalize_def Let_def dvd_div_neg div_gcd_coprime split: if_split_asm) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

315 

63326  316 
lemma normalize_stable [simp]: "q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

317 
by (simp add: normalize_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

318 

63326  319 
lemma normalize_denom_zero [simp]: "normalize (p, 0) = (0, 1)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

320 
by (simp add: normalize_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

321 

63326  322 
lemma normalize_negative [simp]: "q < 0 \<Longrightarrow> normalize (p, q) = normalize ( p,  q)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

323 
by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

324 

60758  325 
text\<open> 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

326 
Decompose a fraction into normalized, i.e. coprime numerator and denominator: 
60758  327 
\<close> 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

328 

63326  329 
definition quotient_of :: "rat \<Rightarrow> int \<times> int" 
330 
where "quotient_of x = 

331 
(THE pair. x = Fract (fst pair) (snd pair) \<and> snd pair > 0 \<and> coprime (fst pair) (snd pair))" 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

332 

63326  333 
lemma quotient_of_unique: "\<exists>!p. r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

334 
proof (cases r) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

335 
case (Fract a b) 
63494  336 
then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> 
337 
snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" 

63326  338 
by auto 
339 
then show ?thesis 

340 
proof (rule ex1I) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

341 
fix p 
63911  342 
assume r: "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" 
343 
obtain c d where p: "p = (c, d)" by (cases p) 

344 
with r have Fract': "r = Fract c d" "d > 0" "coprime c d" 

63326  345 
by simp_all 
63911  346 
have "(c, d) = (a, b)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

347 
proof (cases "a = 0") 
63326  348 
case True 
349 
with Fract Fract' show ?thesis 

350 
by (simp add: eq_rat) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

351 
next 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

352 
case False 
63326  353 
with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" 
354 
by (auto simp add: eq_rat) 

355 
then have "c * b > 0 \<longleftrightarrow> a * d > 0" 

356 
by auto 

357 
with \<open>b > 0\<close> \<open>d > 0\<close> have "a > 0 \<longleftrightarrow> c > 0" 

358 
by (simp add: zero_less_mult_iff) 

359 
with \<open>a \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have sgn: "sgn a = sgn c" 

360 
by (auto simp add: not_less) 

60758  361 
from \<open>coprime a b\<close> \<open>coprime c d\<close> have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

362 
by (simp add: coprime_crossproduct_int) 
63326  363 
with \<open>b > 0\<close> \<open>d > 0\<close> have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" 
364 
by simp 

365 
then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" 

366 
by (simp add: abs_sgn) 

367 
with sgn * show ?thesis 

368 
by (auto simp add: sgn_0_0) 

33805  369 
qed 
63326  370 
with p show "p = (a, b)" 
371 
by simp 

33805  372 
qed 
373 
qed 

374 

63326  375 
lemma quotient_of_Fract [code]: "quotient_of (Fract a b) = normalize (a, b)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

376 
proof  
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

377 
have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

378 
by (rule sym) (auto intro: normalize_eq) 
52146  379 
moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

380 
by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

381 
moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

382 
by (rule normalize_coprime) simp 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

383 
ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast 
63911  384 
then have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> 
385 
coprime (fst p) (snd p)) = normalize (a, b)" 

386 
by (rule the1_equality [OF quotient_of_unique]) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

387 
then show ?thesis by (simp add: quotient_of_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

388 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

389 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

390 
lemma quotient_of_number [simp]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

391 
"quotient_of 0 = (0, 1)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

392 
"quotient_of 1 = (1, 1)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

393 
"quotient_of (numeral k) = (numeral k, 1)" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

394 
"quotient_of ( 1) = ( 1, 1)" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

395 
"quotient_of ( numeral k) = ( numeral k, 1)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

396 
by (simp_all add: rat_number_expand quotient_of_Fract) 
33805  397 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

398 
lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

399 
by (simp add: quotient_of_Fract normalize_eq) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

400 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

401 
lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

402 
by (cases r) (simp add: quotient_of_Fract normalize_denom_pos) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

403 

64849  404 
lemma quotient_of_denom_pos': "snd (quotient_of r) > 0" 
405 
using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff) 

65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
64849
diff
changeset

406 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

407 
lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

408 
by (cases r) (simp add: quotient_of_Fract normalize_coprime) 
33805  409 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

410 
lemma quotient_of_inject: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

411 
assumes "quotient_of a = quotient_of b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

412 
shows "a = b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

413 
proof  
63326  414 
obtain p q r s where a: "a = Fract p q" and b: "b = Fract r s" and "q > 0" and "s > 0" 
415 
by (cases a, cases b) 

416 
with assms show ?thesis 

417 
by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

418 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

419 

63326  420 
lemma quotient_of_inject_eq: "quotient_of a = quotient_of b \<longleftrightarrow> a = b" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

421 
by (auto simp add: quotient_of_inject) 
33805  422 

27551  423 

60758  424 
subsubsection \<open>Various\<close> 
27551  425 

426 
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

427 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  428 

63326  429 
lemma Fract_add_one: "n \<noteq> 0 \<Longrightarrow> Fract (m + n) n = Fract m n + 1" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

430 
by (simp add: rat_number_expand) 
27551  431 

50178  432 
lemma quotient_of_div: 
433 
assumes r: "quotient_of r = (n,d)" 

434 
shows "r = of_int n / of_int d" 

435 
proof  

436 
from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]] 

437 
have "r = Fract n d" by simp 

63326  438 
then show ?thesis using Fract_of_int_quotient 
439 
by simp 

50178  440 
qed 
27551  441 

63326  442 

60758  443 
subsubsection \<open>The ordered field of rational numbers\<close> 
27509  444 

47907  445 
lift_definition positive :: "rat \<Rightarrow> bool" 
446 
is "\<lambda>x. 0 < fst x * snd x" 

63326  447 
proof clarsimp 
47907  448 
fix a b c d :: int 
449 
assume "b \<noteq> 0" and "d \<noteq> 0" and "a * d = c * b" 

63326  450 
then have "a * d * b * d = c * b * b * d" 
47907  451 
by simp 
63326  452 
then have "a * b * d\<^sup>2 = c * d * b\<^sup>2" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

453 
unfolding power2_eq_square by (simp add: ac_simps) 
63326  454 
then have "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2" 
47907  455 
by simp 
63326  456 
then show "0 < a * b \<longleftrightarrow> 0 < c * d" 
60758  457 
using \<open>b \<noteq> 0\<close> and \<open>d \<noteq> 0\<close> 
47907  458 
by (simp add: zero_less_mult_iff) 
459 
qed 

460 

461 
lemma positive_zero: "\<not> positive 0" 

462 
by transfer simp 

463 

63326  464 
lemma positive_add: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)" 
465 
apply transfer 

466 
apply (simp add: zero_less_mult_iff) 

63494  467 
apply (elim disjE) 
468 
apply (simp_all add: add_pos_pos add_neg_neg mult_pos_neg mult_neg_pos mult_neg_neg) 

63326  469 
done 
47907  470 

63326  471 
lemma positive_mult: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)" 
472 
apply transfer 

473 
apply (drule (1) mult_pos_pos) 

474 
apply (simp add: ac_simps) 

475 
done 

47907  476 

63326  477 
lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive ( x)" 
478 
by transfer (auto simp: neq_iff zero_less_mult_iff mult_less_0_iff) 

47907  479 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59667
diff
changeset

480 
instantiation rat :: linordered_field 
27509  481 
begin 
482 

63326  483 
definition "x < y \<longleftrightarrow> positive (y  x)" 
47907  484 

63326  485 
definition "x \<le> y \<longleftrightarrow> x < y \<or> x = y" for x y :: rat 
47907  486 

63326  487 
definition "\<bar>a\<bar> = (if a < 0 then  a else a)" for a :: rat 
47907  488 

63326  489 
definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else  1)" for a :: rat 
47906  490 

63326  491 
instance 
492 
proof 

47907  493 
fix a b c :: rat 
494 
show "\<bar>a\<bar> = (if a < 0 then  a else a)" 

495 
by (rule abs_rat_def) 

496 
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" 

497 
unfolding less_eq_rat_def less_rat_def 

63326  498 
apply auto 
63494  499 
apply (drule (1) positive_add) 
500 
apply (simp_all add: positive_zero) 

63326  501 
done 
47907  502 
show "a \<le> a" 
503 
unfolding less_eq_rat_def by simp 

504 
show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" 

505 
unfolding less_eq_rat_def less_rat_def 

63326  506 
apply auto 
507 
apply (drule (1) positive_add) 

508 
apply (simp add: algebra_simps) 

509 
done 

47907  510 
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b" 
511 
unfolding less_eq_rat_def less_rat_def 

63326  512 
apply auto 
513 
apply (drule (1) positive_add) 

514 
apply (simp add: positive_zero) 

515 
done 

47907  516 
show "a \<le> b \<Longrightarrow> c + a \<le> c + b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

517 
unfolding less_eq_rat_def less_rat_def by auto 
47907  518 
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else  1)" 
519 
by (rule sgn_rat_def) 

520 
show "a \<le> b \<or> b \<le> a" 

521 
unfolding less_eq_rat_def less_rat_def 

522 
by (auto dest!: positive_minus) 

523 
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 

524 
unfolding less_rat_def 

63326  525 
apply (drule (1) positive_mult) 
526 
apply (simp add: algebra_simps) 

527 
done 

47906  528 
qed 
27551  529 

47907  530 
end 
531 

70344  532 
text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs 
533 
of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case 

534 
explosions.\<close> 

535 

68536  536 
lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff 
537 
lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff 

538 

539 

47907  540 
instantiation rat :: distrib_lattice 
541 
begin 

542 

63326  543 
definition "(inf :: rat \<Rightarrow> rat \<Rightarrow> rat) = min" 
27509  544 

63326  545 
definition "(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max" 
47907  546 

63326  547 
instance 
548 
by standard (auto simp add: inf_rat_def sup_rat_def max_min_distrib2) 

47907  549 

550 
end 

551 

552 
lemma positive_rat: "positive (Fract a b) \<longleftrightarrow> 0 < a * b" 

553 
by transfer simp 

27509  554 

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

555 
lemma less_rat [simp]: 
63494  556 
"b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" 
557 
by (simp add: less_rat_def positive_rat algebra_simps) 

27509  558 

47907  559 
lemma le_rat [simp]: 
63494  560 
"b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" 
561 
by (simp add: le_less eq_rat) 

27551  562 

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

563 
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" 
35216  564 
by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff) 
27551  565 

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

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

568 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  569 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
570 

571 
lemma Rat_induct_pos [case_names Fract, induct type: rat]: 

572 
assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" 

573 
shows "P q" 

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

574 
proof (cases q) 
63326  575 
case (Fract a b) 
576 
have step': "P (Fract a b)" if b: "b < 0" for a b :: int 

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

577 
proof  
63326  578 
from b have "0 <  b" 
579 
by simp 

580 
then have "P (Fract ( a) ( b))" 

581 
by (rule step) 

582 
then show "P (Fract a b)" 

583 
by (simp add: order_less_imp_not_eq [OF b]) 

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

584 
qed 
63494  585 
from Fract show "P q" 
586 
by (auto simp add: linorder_neq_iff step step') 

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

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

588 

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

590 
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

591 

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

593 
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

594 

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

596 
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

597 

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

599 
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

600 

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

602 
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

603 

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

605 
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

606 

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

608 
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

609 

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

611 
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

612 

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

613 

60758  614 
subsubsection \<open>Rationals are an Archimedean field\<close> 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

615 

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

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

618 
have "Fract a b = of_int (a div b) + Fract (a mod b) b" 
63326  619 
by (cases "b = 0") (simp, simp add: of_int_rat) 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

620 
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1" 
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

621 
unfolding Fract_of_int_quotient 
56571
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56544
diff
changeset

622 
by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg) 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

623 
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

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

625 

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

626 
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

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

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

630 
case (Fract a b) 
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

631 
have "Fract a b \<le> of_int (a div b + 1)" 
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

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

633 
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

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

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

636 

43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

637 
instantiation rat :: floor_ceiling 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

638 
begin 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

639 

63326  640 
definition [code del]: "\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat 
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

641 

61942  642 
instance 
643 
proof 

63326  644 
show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)" for x :: rat 
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

645 
unfolding floor_rat_def using floor_exists1 by (rule theI') 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

646 
qed 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

647 

6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

648 
end 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

649 

61942  650 
lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b" 
59984
4f1eccec320c
conversion between division on nat/int and division in archmedean fields
haftmann
parents:
59867
diff
changeset

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

652 

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

653 

60758  654 
subsection \<open>Linear arithmetic setup\<close> 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

655 

60758  656 
declaration \<open> 
31100  657 
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 
658 
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) 

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

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

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

662 
@{thm True_implies_equals}, 

55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
54863
diff
changeset

663 
@{thm distrib_left [where a = "numeral v" for v]}, 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
54863
diff
changeset

664 
@{thm distrib_left [where a = " numeral v" for v]}, 
64240  665 
@{thm div_by_1}, @{thm div_0}, 
31100  666 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 
667 
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, 

63711
e4843a8a8b18
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
boehmes
parents:
63502
diff
changeset

668 
@{thm add_divide_distrib}, @{thm diff_divide_distrib}, 
31100  669 
@{thm of_int_minus}, @{thm of_int_diff}, 
670 
@{thm of_int_of_nat_eq}] 

61144  671 
#> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor] 
69593  672 
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> rat\<close>) 
673 
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> rat\<close>)) 

60758  674 
\<close> 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

675 

23342  676 

60758  677 
subsection \<open>Embedding from Rationals to other Fields\<close> 
23342  678 

27551  679 
context field_char_0 
680 
begin 

681 

47906  682 
lift_definition of_rat :: "rat \<Rightarrow> 'a" 
683 
is "\<lambda>x. of_int (fst x) / of_int (snd x)" 

63494  684 
by (auto simp: nonzero_divide_eq_eq nonzero_eq_divide_eq) (simp only: of_int_mult [symmetric]) 
23342  685 

47906  686 
end 
687 

27551  688 
lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b" 
47906  689 
by transfer simp 
23342  690 

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

47906  692 
by transfer simp 
23342  693 

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

47906  695 
by transfer simp 
23342  696 

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

47906  698 
by transfer (simp add: add_frac_eq) 
23342  699 

23343  700 
lemma of_rat_minus: "of_rat ( a) =  of_rat a" 
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56409
diff
changeset

701 
by transfer simp 
23343  702 

63326  703 
lemma of_rat_neg_one [simp]: "of_rat ( 1) =  1" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

704 
by (simp add: of_rat_minus) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54409
diff
changeset

705 

23343  706 
lemma of_rat_diff: "of_rat (a  b) = of_rat a  of_rat b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

707 
using of_rat_add [of a " b"] by (simp add: of_rat_minus) 
23343  708 

23342  709 
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" 
63326  710 
by transfer (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps) 
23342  711 

64267  712 
lemma of_rat_sum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))" 
59000  713 
by (induct rule: infinite_finite_induct) (auto simp: of_rat_add) 
714 

64272  715 
lemma of_rat_prod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))" 
59000  716 
by (induct rule: infinite_finite_induct) (auto simp: of_rat_mult) 
717 

63326  718 
lemma nonzero_of_rat_inverse: "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)" 
719 
by (rule inverse_unique [symmetric]) (simp add: of_rat_mult [symmetric]) 

23342  720 

68441  721 
lemma of_rat_inverse: "(of_rat (inverse a) :: 'a::field_char_0) = inverse (of_rat a)" 
63326  722 
by (cases "a = 0") (simp_all add: nonzero_of_rat_inverse) 
23342  723 

63326  724 
lemma nonzero_of_rat_divide: "b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b" 
725 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

23342  726 

68441  727 
lemma of_rat_divide: "(of_rat (a / b) :: 'a::field_char_0) = of_rat a / of_rat b" 
63326  728 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
729 

730 
lemma of_rat_power: "(of_rat (a ^ n) :: 'a::field_char_0) = of_rat a ^ n" 

731 
by (induct n) (simp_all add: of_rat_mult) 

23342  732 

63326  733 
lemma of_rat_eq_iff [simp]: "of_rat a = of_rat b \<longleftrightarrow> a = b" 
734 
apply transfer 

735 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

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

737 
done 

23343  738 

63326  739 
lemma of_rat_eq_0_iff [simp]: "of_rat a = 0 \<longleftrightarrow> a = 0" 
54409  740 
using of_rat_eq_iff [of _ 0] by simp 
741 

63326  742 
lemma zero_eq_of_rat_iff [simp]: "0 = of_rat a \<longleftrightarrow> 0 = a" 
54409  743 
by simp 
744 

63326  745 
lemma of_rat_eq_1_iff [simp]: "of_rat a = 1 \<longleftrightarrow> a = 1" 
54409  746 
using of_rat_eq_iff [of _ 1] by simp 
747 

63326  748 
lemma one_eq_of_rat_iff [simp]: "1 = of_rat a \<longleftrightarrow> 1 = a" 
54409  749 
by simp 
750 

63326  751 
lemma of_rat_less: "(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

753 
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

754 
assume not_zero: "b > 0" "d > 0" 
56544  755 
then have "b * d > 0" by simp 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

756 
have of_int_divide_less_eq: 
63326  757 
"(of_int a :: 'a) / of_int b < of_int c / of_int d \<longleftrightarrow> 
758 
(of_int a :: 'a) * of_int d < of_int c * of_int b" 

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

759 
using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) 
63326  760 
show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) \<longleftrightarrow> 
761 
Fract a b < Fract c d" 

60758  762 
using not_zero \<open>b * d > 0\<close> 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

763 
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

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

765 

63326  766 
lemma of_rat_less_eq: "(of_rat r :: 'a::linordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

767 
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

768 

63326  769 
lemma of_rat_le_0_iff [simp]: "(of_rat r :: 'a::linordered_field) \<le> 0 \<longleftrightarrow> r \<le> 0" 
770 
using of_rat_less_eq [of r 0, where 'a = 'a] by simp 

54409  771 

63326  772 
lemma zero_le_of_rat_iff [simp]: "0 \<le> (of_rat r :: 'a::linordered_field) \<longleftrightarrow> 0 \<le> r" 
773 
using of_rat_less_eq [of 0 r, where 'a = 'a] by simp 

54409  774 

63326  775 
lemma of_rat_le_1_iff [simp]: "(of_rat r :: 'a::linordered_field) \<le> 1 \<longleftrightarrow> r \<le> 1" 
54409  776 
using of_rat_less_eq [of r 1] by simp 
777 

63326  778 
lemma one_le_of_rat_iff [simp]: "1 \<le> (of_rat r :: 'a::linordered_field) \<longleftrightarrow> 1 \<le> r" 
54409  779 
using of_rat_less_eq [of 1 r] by simp 
780 

63326  781 
lemma of_rat_less_0_iff [simp]: "(of_rat r :: 'a::linordered_field) < 0 \<longleftrightarrow> r < 0" 
782 
using of_rat_less [of r 0, where 'a = 'a] by simp 

54409  783 

63326  784 
lemma zero_less_of_rat_iff [simp]: "0 < (of_rat r :: 'a::linordered_field) \<longleftrightarrow> 0 < r" 
785 
using of_rat_less [of 0 r, where 'a = 'a] by simp 

54409  786 

63326  787 
lemma of_rat_less_1_iff [simp]: "(of_rat r :: 'a::linordered_field) < 1 \<longleftrightarrow> r < 1" 
54409  788 
using of_rat_less [of r 1] by simp 
789 

63326  790 
lemma one_less_of_rat_iff [simp]: "1 < (of_rat r :: 'a::linordered_field) \<longleftrightarrow> 1 < r" 
54409  791 
using of_rat_less [of 1 r] by simp 
23343  792 

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

793 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  794 
proof 
63326  795 
show "of_rat a = id a" for a 
796 
by (induct a) (simp add: of_rat_rat Fract_of_int_eq [symmetric]) 

23343  797 
qed 
798 

63494  799 
text \<open>Collapse nested embeddings.\<close> 
23343  800 
lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" 
63326  801 
by (induct n) (simp_all add: of_rat_add) 
23343  802 

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

63326  804 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  805 

63326  806 
lemma of_rat_numeral_eq [simp]: "of_rat (numeral w) = numeral w" 
807 
using of_rat_of_int_eq [of "numeral w"] by simp 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

808 

63326  809 
lemma of_rat_neg_numeral_eq [simp]: "of_rat ( numeral w) =  numeral w" 
810 
using of_rat_of_int_eq [of " numeral w"] by simp 

23343  811 

23879  812 
lemmas zero_rat = Zero_rat_def 
813 
lemmas one_rat = One_rat_def 

814 

63326  815 
abbreviation rat_of_nat :: "nat \<Rightarrow> rat" 
816 
where "rat_of_nat \<equiv> of_nat" 

24198  817 

63326  818 
abbreviation rat_of_int :: "int \<Rightarrow> rat" 
819 
where "rat_of_int \<equiv> of_int" 

820 

24198  821 

60758  822 
subsection \<open>The Set of Rational Numbers\<close> 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

823 

28001  824 
context field_char_0 
825 
begin 

826 

61070  827 
definition Rats :: "'a set" ("\<rat>") 
828 
where "\<rat> = range of_rat" 

28001  829 

830 
end 

831 

68529  832 
lemma Rats_cases [cases set: Rats]: 
833 
assumes "q \<in> \<rat>" 

834 
obtains (of_rat) r where "q = of_rat r" 

835 
proof  

836 
from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat" 

837 
by (simp only: Rats_def) 

838 
then obtain r where "q = of_rat r" .. 

839 
then show thesis .. 

840 
qed 

841 

61070  842 
lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>" 
63326  843 
by (simp add: Rats_def) 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

844 

61070  845 
lemma Rats_of_int [simp]: "of_int z \<in> \<rat>" 
63326  846 
by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat) 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

847 

64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

848 
lemma Ints_subset_Rats: "\<int> \<subseteq> \<rat>" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

849 
using Ints_cases Rats_of_int by blast 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

850 

61070  851 
lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>" 
63326  852 
by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat) 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

853 

64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

854 
lemma Nats_subset_Rats: "\<nat> \<subseteq> \<rat>" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

855 
using Ints_subset_Rats Nats_subset_Ints by blast 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

856 

61070  857 
lemma Rats_number_of [simp]: "numeral w \<in> \<rat>" 
63326  858 
by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

859 

61070  860 
lemma Rats_0 [simp]: "0 \<in> \<rat>" 
63326  861 
unfolding Rats_def by (rule range_eqI) (rule of_rat_0 [symmetric]) 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

862 

61070  863 
lemma Rats_1 [simp]: "1 \<in> \<rat>" 
63326  864 
unfolding Rats_def by (rule range_eqI) (rule of_rat_1 [symmetric]) 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

865 

63326  866 
lemma Rats_add [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a + b \<in> \<rat>" 
867 
apply (auto simp add: Rats_def) 

868 
apply (rule range_eqI) 

869 
apply (rule of_rat_add [symmetric]) 

870 
done 

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

871 

68529  872 
lemma Rats_minus_iff [simp]: " a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>" 
873 
by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus) 

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

874 

63326  875 
lemma Rats_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a  b \<in> \<rat>" 
876 
apply (auto simp add: Rats_def) 

877 
apply (rule range_eqI) 

878 
apply (rule of_rat_diff [symmetric]) 

879 
done 

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

880 

63326  881 
lemma Rats_mult [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a * b \<in> \<rat>" 
882 
apply (auto simp add: Rats_def) 

883 
apply (rule range_eqI) 

884 
apply (rule of_rat_mult [symmetric]) 

885 
done 

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

886 

68441  887 
lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>" 
63494  888 
for a :: "'a::field_char_0" 
63326  889 
apply (auto simp add: Rats_def) 
890 
apply (rule range_eqI) 

891 
apply (rule of_rat_inverse [symmetric]) 

892 
done 

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

893 

68441  894 
lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>" 
63494  895 
for a b :: "'a::field_char_0" 
63326  896 
apply (auto simp add: Rats_def) 
897 
apply (rule range_eqI) 

898 
apply (rule of_rat_divide [symmetric]) 

899 
done 

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

900 

63494  901 
lemma Rats_power [simp]: "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>" 
902 
for a :: "'a::field_char_0" 

63326  903 
apply (auto simp add: Rats_def) 
904 
apply (rule range_eqI) 

905 
apply (rule of_rat_power [symmetric]) 

906 
done 

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

907 

63326  908 
lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

910 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57136
diff
changeset

911 
lemma Rats_infinite: "\<not> finite \<rat>" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57136
diff
changeset

912 
by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def) 
28001  913 

63326  914 

60758  915 
subsection \<open>Implementation of rational numbers as pairs of integers\<close> 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

916 

60758  917 
text \<open>Formal constructor\<close> 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

918 

63326  919 
definition Frct :: "int \<times> int \<Rightarrow> rat" 
920 
where [simp]: "Frct p = Fract (fst p) (snd p)" 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

921 

63326  922 
lemma [code abstype]: "Frct (quotient_of q) = q" 
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset

923 
by (cases q) (auto intro: quotient_of_eq) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

924 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

925 

60758  926 
text \<open>Numerals\<close> 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

927 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

928 
declare quotient_of_Fract [code abstract] 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

929 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

930 
definition of_int :: "int \<Rightarrow> rat" 
63326  931 
where [code_abbrev]: "of_int = Int.of_int" 
932 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

933 
hide_const (open) of_int 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

934 

63326  935 
lemma quotient_of_int [code abstract]: "quotient_of (Rat.of_int a) = (a, 1)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

936 
by (simp add: of_int_def of_int_rat quotient_of_Fract) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

937 

63326  938 
lemma [code_unfold]: "numeral k = Rat.of_int (numeral k)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

939 
by (simp add: Rat.of_int_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

940 

63326  941 
lemma [code_unfold]: " numeral k = Rat.of_int ( numeral k)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

942 
by (simp add: Rat.of_int_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

943 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

944 
lemma Frct_code_post [code_post]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

945 
"Frct (0, a) = 0" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

946 
"Frct (a, 0) = 0" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

947 
"Frct (1, 1) = 1" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

948 
"Frct (numeral k, 1) = numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

949 
"Frct (1, numeral k) = 1 / numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

950 
"Frct (numeral k, numeral l) = numeral k / numeral l" 
57576
083dfad2727c
more appropriate postprocessing of rational numbers: extract sign to front of fraction
haftmann
parents:
57514
diff
changeset

951 
"Frct ( a, b) =  Frct (a, b)" 
083dfad2727c
more appropriate postprocessing of rational numbers: extract sign to front of fraction
haftmann
parents:
57514
diff
changeset

952 
"Frct (a,  b) =  Frct (a, b)" 
083dfad2727c
more appropriate postprocessing of rational numbers: extract sign to front of fraction
haftmann
parents:
57514
diff
changeset

953 
" ( Frct q) = Frct q" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

954 
by (simp_all add: Fract_of_int_quotient) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

955 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

956 

60758  957 
text \<open>Operations\<close> 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

958 

63326  959 
lemma rat_zero_code [code abstract]: "quotient_of 0 = (0, 1)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

960 
by (simp add: Zero_rat_def quotient_of_Fract normalize_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

961 

63326  962 
lemma rat_one_code [code abstract]: "quotient_of 1 = (1, 1)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

963 
by (simp add: One_rat_def quotient_of_Fract normalize_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

964 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

965 
lemma rat_plus_code [code abstract]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

966 
"quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

967 
in normalize (a * d + b * c, c * d))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

968 
by (cases p, cases q) (simp add: quotient_of_Fract) 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

969 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

970 
lemma rat_uminus_code [code abstract]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

971 
"quotient_of ( p) = (let (a, b) = quotient_of p in ( a, b))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

972 
by (cases p) (simp add: quotient_of_Fract) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

973 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

974 
lemma rat_minus_code [code abstract]: 
63326  975 
"quotient_of (p  q) = 
976 
(let (a, c) = quotient_of p; (b, d) = quotient_of q 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

977 
in normalize (a * d  b * c, c * d))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

978 
by (cases p, cases q) (simp add: quotient_of_Fract) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

979 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

980 
lemma rat_times_code [code abstract]: 
63326  981 
"quotient_of (p * q) = 
982 
(let (a, c) = quotient_of p; (b, d) = quotient_of q 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

983 
in normalize (a * b, c * d))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

985 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

986 
lemma rat_inverse_code [code abstract]: 
63326  987 
"quotient_of (inverse p) = 
988 
(let (a, b) = quotient_of p 

989 
in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))" 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

990 
proof (cases p) 
63326  991 
case (Fract a b) 
992 
then show ?thesis 

67051  993 
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps) 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

994 
qed 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

995 

e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

996 
lemma rat_divide_code [code abstract]: 
63326  997 
"quotient_of (p / q) = 
998 
(let (a, c) = quotient_of p; (b, d) = quotient_of q 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

999 
in normalize (a * d, c * b))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1000 
by (cases p, cases q) (simp add: quotient_of_Fract) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1001 

67051  1002 
lemma rat_abs_code [code abstract]: 
1003 
"quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))" 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1004 
by (cases p) (simp add: quotient_of_Fract) 
67051  1005 

63326  1006 
lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1007 
proof (cases p) 
63326  1008 
case (Fract a b) 
1009 
then show ?thesis 

1010 
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

1012 

63326  1013 
lemma rat_floor_code [code]: "\<lfloor>p\<rfloor> = (let (a, b) = quotient_of p in a div b)" 
61942  1014 
by (cases p) (simp add: quotient_of_Fract floor_Fract) 
43733
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset

1015 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1016 
instantiation rat :: equal 
26513  1017 
begin 
1018 

63326  1019 
definition [code]: "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b" 
26513  1020 

63326  1021 
instance 
1022 
by standard (simp add: equal_rat_def quotient_of_inject_eq) 

26513  1023 

63326  1024 
lemma rat_eq_refl [code nbe]: "HOL.equal (r::rat) r \<longleftrightarrow> True" 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

1025 
by (rule equal_refl) 
28351  1026 

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

1028 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1029 
lemma rat_less_eq_code [code]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1030 
"p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)" 
35726  1031 
by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

1032 

35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1033 
lemma rat_less_code [code]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1034 
"p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" 
35726  1035 
by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

1036 

63326  1037 
lemma [code]: "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1038 
by (cases p) (simp add: quotient_of_Fract of_rat_rat) 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

1039 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

1040 

60758  1041 
text \<open>Quickcheck\<close> 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

1042 

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

1043 
definition (in term_syntax) 
63494  1044 
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 
1045 
int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 

63326  1046 
rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" 
1047 
where [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

1048 

37751  1049 
notation fcomp (infixl "\<circ>>" 60) 
1050 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1051 

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

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

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

1054 

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

1055 
definition 
63326  1056 
"Quickcheck_Random.random i = 
1057 
Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair 

1058 
(let j = int_of_integer (integer_of_natural (denom + 1)) 

1059 
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

1060 

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

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

1062 

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

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

1064 

37751  1065 
no_notation fcomp (infixl "\<circ>>" 60) 
1066 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1067 

41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41792
diff
changeset

1068 
instantiation rat :: exhaustive 
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset

1069 
begin 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset

1070 

2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset

1071 
definition 
63326  1072 
"exhaustive_rat f d = 
1073 
Quickcheck_Exhaustive.exhaustive 

1074 
(\<lambda>l. Quickcheck_Exhaustive.exhaustive 

1075 
(\<lambda>k. f (Fract k (int_of_integer (integer_of_natural l) + 1))) d) d" 

42311
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1076 

eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1077 
instance .. 
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1078 

eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1079 
end 
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1080 

eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1081 
instantiation rat :: full_exhaustive 
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1082 
begin 
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1083 

eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1084 
definition 
63326  1085 
"full_exhaustive_rat f d = 
1086 
Quickcheck_Exhaustive.full_exhaustive 

1087 
(\<lambda>(l, _). Quickcheck_Exhaustive.full_exhaustive 

1088 
(\<lambda>k. f 

1089 
(let j = int_of_integer (integer_of_natural l) + 1 

1090 
in valterm_fract k (j, \<lambda>_. Code_Evaluation.term_of j))) d) d" 

43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1091 

90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1092 
instance .. 
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1093 

90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1094 
end 
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1095 

63326  1096 
instance rat :: partial_term_of .. 
1097 

43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1098 
lemma [code]: 
63326  1099 
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) \<equiv> 
1100 
Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" 

1101 
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) \<equiv> 

1102 
Code_Evaluation.App 

1103 
(Code_Evaluation.Const (STR ''Rat.Frct'') 

1104 
(Typerep.Typerep (STR ''fun'') 

1105 
[Typerep.Typerep (STR ''Product_Type.prod'') 

1106 
[Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []], 

1107 
Typerep.Typerep (STR ''Rat.rat'') []])) 

1108 
(Code_Evaluation.App 

1109 
(Code_Evaluation.App 

1110 
(Code_Evaluation.Const (STR ''Product_Type.Pair'') 

1111 
(Typerep.Typerep (STR ''fun'') 

1112 
[Typerep.Typerep (STR ''Int.int'') [], 

1113 
Typerep.Typerep (STR ''fun'') 

1114 
[Typerep.Typerep (STR ''Int.int'') [], 

1115 
Typerep.Typerep (STR ''Product_Type.prod'') 

1116 
[Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) 

1117 
(partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))" 

1118 
by (rule partial_term_of_anything)+ 

43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1119 

43887  1120 
instantiation rat :: narrowing 
1121 
begin 

1122 

1123 
definition 

63326  1124 
"narrowing = 
1125 
Quickcheck_Narrowing.apply 

1126 
(Quickcheck_Narrowing.apply 

1127 
(Quickcheck_Narrowing.cons (\<lambda>nom denom. Fract nom denom)) narrowing) narrowing" 

43887  1128 

1129 
instance .. 

1130 

1131 
end 

1132 

1133 

60758  1134 
subsection \<open>Setup for Nitpick\<close> 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

1135 

60758  1136 
declaration \<open> 
69593  1137 
Nitpick_HOL.register_frac_type \<^type_name>\<open>rat\<close> 
1138 
[(\<^const_name>\<open>Abs_Rat\<close>, \<^const_name>\<open>Nitpick.Abs_Frac\<close>), 

1139 
(\<^const_name>\<open>zero_rat_inst.zero_rat\<close>, \<^const_name>\<open>Nitpick.zero_frac\<close>), 

1140 
(\<^const_name>\<open>one_rat_inst.one_rat\<close>, \<^const_name>\<open>Nitpick.one_frac\<close>), 

1141 
(\<^const_name>\<open>plus_rat_inst.plus_rat\<close>, \<^const_name>\<open>Nitpick.plus_frac\<close>), 

1142 
(\<^const_name>\<open>times_rat_inst.times_rat\<close>, \<^const_name>\<open>Nitpick.times_frac\<close>), 

1143 
(\<^const_name>\<open>uminus_rat_inst.uminus_rat\<close>, \<^const_name>\<open>Nitpick.uminus_frac\<close>), 

1144 
(\<^const_name>\<open>inverse_rat_inst.inverse_rat\<close>, \<^const_name>\<open>Nitpick.inverse_frac\<close>), 

1145 
(\<^const_name>\<open>ord_rat_inst.less_rat\<close>, \<^const_name>\<open>Nitpick.less_frac\<close>), 

1146 
(\<^const_name>\<open>ord_rat_inst.less_eq_rat\<close>, \<^const_name>\<open>Nitpick.less_eq_frac\<close>), 

1147 
(\<^const_name>\<open>field_char_0_class.of_rat\<close>, \<^const_name>\<open>Nitpick.of_frac\<close>)] 

60758  1148 
\<close> 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1149 

63326  1150 
lemmas [nitpick_unfold] = 
1151 
inverse_rat_inst.inverse_rat 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

1152 
one_rat_inst.one_rat ord_rat_inst.less_rat 
37397
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset

1153 
ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat 
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset

1154 
uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

1155 

52146  1156 

60758  1157 
subsection \<open>Float syntax\<close> 
35343  1158 

1159 
syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_") 

1160 

60758  1161 
parse_translation \<open> 
52146  1162 
let 
1163 
fun mk_frac str = 

1164 
let 

1165 
val {mant = i, exp = n} = Lexicon.read_float str; 

69593  1166 
val exp = Syntax.const \<^const_syntax>\<open>Power.power\<close>; 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57576
diff
changeset

1167 
val ten = Numeral.mk_number_syntax 10; 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59984
diff
changeset

1168 
val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n; 
69593  1169 
in Syntax.const \<^const_syntax>\<open>Fields.inverse_divide\<close> $ Numeral.mk_number_syntax i $ exp10 end; 
52146  1170 

69593  1171 
fun float_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ t $ u] = c $ float_tr [t] $ u 
52146  1172 
 float_tr [t as Const (str, _)] = mk_frac str 
1173 
 float_tr ts = raise TERM ("float_tr", ts); 

69593  1174 
in [(\<^syntax_const>\<open>_Float\<close>, K float_tr)] end 
60758  1175 
\<close> 
35343  1176 

60758  1177 
text\<open>Test:\<close> 
35343  1178 
lemma "123.456 = 111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" 
52146  1179 
by simp 
35343  1180 

55974
c835a9379026
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
wenzelm
parents:
55143
diff
changeset

1181 

60758  1182 
subsection \<open>Hiding implementation details\<close> 
37143  1183 

47907  1184 
hide_const (open) normalize positive 
37143  1185 

53652
18fbca265e2e
use lifting_forget for deregistering numeric types as a quotient type
kuncar
parents:
53374
diff
changeset

1186 
lifting_update rat.lifting 
18fbca265e2e
use lifting_forget for deregistering numeric types as a quotient type
kuncar
parents:
53374
diff
changeset

1187 
lifting_forget rat.lifting 
47906  1188 

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

1189 
end 