author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 50178  ad52ddd35c3a 
permissions  rwrr 
35372  1 
(* Title: HOL/Rat.thy 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

4 

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

6 

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

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

10 

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

12 

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

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

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

18 

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

22 

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

18913  25 

47906  26 
lemma symp_ratrel: "symp ratrel" 
27 
by (simp add: ratrel_def symp_def) 

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

28 

47906  29 
lemma transp_ratrel: "transp ratrel" 
30 
proof (rule transpI, unfold split_paired_all) 

27551  31 
fix a b a' b' a'' b'' :: int 
47906  32 
assume A: "ratrel (a, b) (a', b')" 
33 
assume B: "ratrel (a', b') (a'', b'')" 

27551  34 
have "b' * (a * b'') = b'' * (a * b')" by simp 
35 
also from A have "a * b' = a' * b" by auto 

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

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

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

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

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

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

47906  42 
with A B show "ratrel (a, b) (a'', b'')" by auto 
27551  43 
qed 
44 

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

47 

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

49 
morphisms Rep_Rat Abs_Rat 

50 
by (rule part_equivp_ratrel) 

27551  51 

47906  52 
declare rat.forall_transfer [transfer_rule del] 
53 

54 
lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *) 

55 
"(fun_rel (fun_rel cr_rat op =) op =) 

56 
(transfer_bforall (\<lambda>x. snd x \<noteq> 0)) transfer_forall" 

57 
using rat.forall_transfer by simp 

27551  58 

59 

60 
subsubsection {* Representation and basic operations *} 

61 

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

64 
by simp 

27551  65 

66 
lemma eq_rat: 

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

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

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

69 
and "\<And>a c. Fract 0 a = Fract 0 c" 
47906  70 
by (transfer, simp)+ 
27551  71 

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

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

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

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

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

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

78 
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

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

80 
from `b \<noteq> 0` have "?b * gcd a b = b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

82 
with `b \<noteq> 0` have "?b \<noteq> 0" by auto 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

83 
from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

84 
by (simp add: eq_rat dvd_div_mult mult_commute [of a]) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

85 
from `b \<noteq> 0` have coprime: "coprime ?a ?b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

86 
by (auto intro: div_gcd_coprime_int) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

87 
show C proof (cases "b > 0") 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

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

91 
moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

93 
ultimately show C . 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

96 
note assms 
47906  97 
moreover have "q = Fract ( ?a) ( ?b)" unfolding q by transfer simp 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

98 
moreover from False `b \<noteq> 0` have " ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

99 
moreover from coprime have "coprime ( ?a) ( ?b)" by simp 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

100 
ultimately show C . 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

103 

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

104 
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

105 
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

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

107 
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

108 

47906  109 
instantiation rat :: field_inverse_zero 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

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

111 

47906  112 
lift_definition zero_rat :: "rat" is "(0, 1)" 
113 
by simp 

114 

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

116 
by simp 

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

117 

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

18913  120 

47906  121 
lemma One_rat_def: "1 = Fract 1 1" 
122 
by transfer simp 

123 

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

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

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

126 
by (clarsimp, simp add: distrib_right, simp add: mult_ac) 
27551  127 

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

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

47906  131 
using assms by transfer simp 
18913  132 

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

27551  135 

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

136 
lemma minus_rat [simp]: " Fract a b = Fract ( a) b" 
47906  137 
by transfer simp 
27551  138 

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

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

141 

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

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

143 
diff_rat_def: "q  r = q +  (r::rat)" 
18913  144 

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

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

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

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

149 

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

152 
by (simp add: mult_ac) 

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

153 

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

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

156 

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

157 
lemma mult_rat_cancel: 
27551  158 
assumes "c \<noteq> 0" 
159 
shows "Fract (c * a) (c * b) = Fract a b" 

47906  160 
using assms by transfer simp 
161 

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

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

164 
by (auto simp add: mult_commute) 

165 

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

167 
by transfer simp 

168 

169 
definition 

170 
divide_rat_def: "q / r = q * inverse (r::rat)" 

171 

172 
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" 

173 
by (simp add: divide_rat_def) 

27509  174 

175 
instance proof 

47906  176 
fix q r s :: rat 
177 
show "(q * r) * s = q * (r * s)" 

178 
by transfer simp 

179 
show "q * r = r * q" 

180 
by transfer simp 

181 
show "1 * q = q" 

182 
by transfer simp 

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

184 
by transfer (simp add: algebra_simps) 

185 
show "q + r = r + q" 

186 
by transfer simp 

187 
show "0 + q = q" 

188 
by transfer simp 

189 
show " q + q = 0" 

190 
by transfer simp 

191 
show "q  r = q +  r" 

192 
by (fact diff_rat_def) 

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

194 
by transfer (simp add: algebra_simps) 

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

196 
by transfer simp 

197 
{ assume "q \<noteq> 0" thus "inverse q * q = 1" 

198 
by transfer simp } 

199 
show "q / r = q * inverse r" 

200 
by (fact divide_rat_def) 

201 
show "inverse 0 = (0::rat)" 

202 
by transfer simp 

27509  203 
qed 
204 

205 
end 

206 

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

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

210 
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

211 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  212 

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

214 
by (rule of_nat_rat [symmetric]) 

215 

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

217 
by (rule of_int_rat [symmetric]) 

218 

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

219 
lemma rat_number_collapse: 
27551  220 
"Fract 0 k = 0" 
221 
"Fract 1 1 = 1" 

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

222 
"Fract (numeral w) 1 = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

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

226 
using Fract_of_int_eq [of "neg_numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

227 
by (simp_all add: Zero_rat_def One_rat_def eq_rat) 
27551  228 

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

229 
lemma rat_number_expand: 
27551  230 
"0 = Fract 0 1" 
231 
"1 = Fract 1 1" 

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

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

233 
"neg_numeral k = Fract (neg_numeral k) 1" 
27551  234 
by (simp_all add: rat_number_collapse) 
235 

236 
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

237 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
27551  238 
assumes 0: "q = 0 \<Longrightarrow> C" 
239 
shows C 

240 
proof (cases "q = 0") 

241 
case True then show C using 0 by auto 

242 
next 

243 
case False 

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

244 
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto 
27551  245 
moreover with False have "0 \<noteq> Fract a b" by simp 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

246 
with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

247 
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast 
27551  248 
qed 
249 

33805  250 
subsubsection {* Function @{text normalize} *} 
251 

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

252 
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

253 
proof (cases "b = 0") 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

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

257 
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

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

259 
ultimately have "b div gcd a b \<noteq> 0" by auto 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

260 
with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a]) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

261 
qed 
33805  262 

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

263 
definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" where 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

264 
"normalize p = (if snd p > 0 then (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

265 
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

266 
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

267 

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

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

269 
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

270 
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

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

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

273 
have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \<Longrightarrow> q * gcd r s = sgn (q * s) * s * gcd p q \<Longrightarrow> p * s = q * r" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

275 
assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

276 
then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

277 
with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

279 
from assms show ?thesis 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

280 
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) 
33805  281 
qed 
282 

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

283 
lemma normalize_eq: "normalize (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

284 
by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

286 

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

287 
lemma normalize_denom_pos: "normalize 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

288 
by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

290 

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

291 
lemma normalize_coprime: "normalize 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

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

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

294 

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

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

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

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

298 

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

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

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

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

302 

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

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

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

305 
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

306 

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

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

308 
Decompose a fraction into normalized, i.e. coprime numerator and denominator: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

310 

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

311 
definition quotient_of :: "rat \<Rightarrow> int \<times> int" where 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

312 
"quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

313 
snd pair > 0 & coprime (fst pair) (snd pair))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

314 

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

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

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

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

318 
case (Fract a b) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

319 
then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" by auto 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

320 
then show ?thesis proof (rule ex1I) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

322 
obtain c d :: int where p: "p = (c, d)" by (cases p) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

323 
assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

324 
with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

325 
have "c = a \<and> d = b" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

326 
proof (cases "a = 0") 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

327 
case True with Fract Fract' show ?thesis by (simp add: eq_rat) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

330 
with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

331 
then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

332 
with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

333 
with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

334 
from `coprime a b` `coprime c d` 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>" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

336 
with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

337 
then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

338 
with sgn * show ?thesis by (auto simp add: sgn_0_0) 
33805  339 
qed 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

340 
with p show "p = (a, b)" by simp 
33805  341 
qed 
342 
qed 

343 

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

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

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

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

347 
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

348 
by (rule sym) (auto intro: normalize_eq) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

350 
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

351 
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

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

353 
ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

355 
"(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> coprime (fst p) (snd p)) = normalize (a, b)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

357 
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

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

359 

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

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

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

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

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

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

365 
by (simp_all add: rat_number_expand quotient_of_Fract) 
33805  366 

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

367 
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

368 
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

369 

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

370 
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

371 
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

372 

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

373 
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

374 
by (cases r) (simp add: quotient_of_Fract normalize_coprime) 
33805  375 

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

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

377 
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

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

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

380 
obtain p q r s where a: "a = Fract p q" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

381 
and b: "b = Fract r s" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

382 
and "q > 0" and "s > 0" by (cases a, cases b) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

383 
with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

385 

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

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

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

388 
by (auto simp add: quotient_of_inject) 
33805  389 

27551  390 

391 
subsubsection {* Various *} 

392 

393 
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

394 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  395 

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

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

397 
by (simp add: rat_number_expand) 
27551  398 

399 

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

27509  401 

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

404 
proof (clarsimp) 

405 
fix a b c d :: int 

406 
assume "b \<noteq> 0" and "d \<noteq> 0" and "a * d = c * b" 

407 
hence "a * d * b * d = c * b * b * d" 

408 
by simp 

409 
hence "a * b * d\<twosuperior> = c * d * b\<twosuperior>" 

410 
unfolding power2_eq_square by (simp add: mult_ac) 

411 
hence "0 < a * b * d\<twosuperior> \<longleftrightarrow> 0 < c * d * b\<twosuperior>" 

412 
by simp 

413 
thus "0 < a * b \<longleftrightarrow> 0 < c * d" 

414 
using `b \<noteq> 0` and `d \<noteq> 0` 

415 
by (simp add: zero_less_mult_iff) 

416 
qed 

417 

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

419 
by transfer simp 

420 

421 
lemma positive_add: 

422 
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)" 

423 
apply transfer 

424 
apply (simp add: zero_less_mult_iff) 

425 
apply (elim disjE, simp_all add: add_pos_pos add_neg_neg 

426 
mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg) 

427 
done 

428 

429 
lemma positive_mult: 

430 
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)" 

431 
by transfer (drule (1) mult_pos_pos, simp add: mult_ac) 

432 

433 
lemma positive_minus: 

434 
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive ( x)" 

435 
by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff) 

436 

437 
instantiation rat :: linordered_field_inverse_zero 

27509  438 
begin 
439 

47907  440 
definition 
441 
"x < y \<longleftrightarrow> positive (y  x)" 

442 

443 
definition 

444 
"x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y" 

445 

446 
definition 

447 
"abs (a::rat) = (if a < 0 then  a else a)" 

448 

449 
definition 

450 
"sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else  1)" 

47906  451 

47907  452 
instance proof 
453 
fix a b c :: rat 

454 
show "\<bar>a\<bar> = (if a < 0 then  a else a)" 

455 
by (rule abs_rat_def) 

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

457 
unfolding less_eq_rat_def less_rat_def 

458 
by (auto, drule (1) positive_add, simp_all add: positive_zero) 

459 
show "a \<le> a" 

460 
unfolding less_eq_rat_def by simp 

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

462 
unfolding less_eq_rat_def less_rat_def 

463 
by (auto, drule (1) positive_add, simp add: algebra_simps) 

464 
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b" 

465 
unfolding less_eq_rat_def less_rat_def 

466 
by (auto, drule (1) positive_add, simp add: positive_zero) 

467 
show "a \<le> b \<Longrightarrow> c + a \<le> c + b" 

468 
unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus) 

469 
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else  1)" 

470 
by (rule sgn_rat_def) 

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

472 
unfolding less_eq_rat_def less_rat_def 

473 
by (auto dest!: positive_minus) 

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

475 
unfolding less_rat_def 

476 
by (drule (1) positive_mult, simp add: algebra_simps) 

47906  477 
qed 
27551  478 

47907  479 
end 
480 

481 
instantiation rat :: distrib_lattice 

482 
begin 

483 

484 
definition 

485 
"(inf :: rat \<Rightarrow> rat \<Rightarrow> rat) = min" 

27509  486 

487 
definition 

47907  488 
"(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max" 
489 

490 
instance proof 

491 
qed (auto simp add: inf_rat_def sup_rat_def min_max.sup_inf_distrib1) 

492 

493 
end 

494 

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

496 
by transfer simp 

27509  497 

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

498 
lemma less_rat [simp]: 
27551  499 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
500 
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" 

47907  501 
using assms unfolding less_rat_def 
502 
by (simp add: positive_rat algebra_simps) 

27509  503 

47907  504 
lemma le_rat [simp]: 
505 
assumes "b \<noteq> 0" and "d \<noteq> 0" 

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

507 
using assms unfolding le_less by (simp add: eq_rat) 

27551  508 

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

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

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

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

514 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  515 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
516 

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

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

519 
shows "P q" 

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

520 
proof (cases q) 
27551  521 
have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

527 
thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

530 
thus "P q" by (force simp add: linorder_neq_iff step step') 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

532 

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

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

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

535 
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

536 

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

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

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

539 
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

540 

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

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

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

543 
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

544 

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

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

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

547 
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

548 

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

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

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

551 
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

552 

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

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

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

555 
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

556 

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

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

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

559 
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

560 

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

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

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

563 
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

564 

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

565 

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

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

567 

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

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

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

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

571 
have "Fract a b = of_int (a div b) + Fract (a mod b) b" 
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

572 
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

573 
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

574 
unfolding Fract_of_int_quotient 
36409  575 
by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos) 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset

576 
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

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

578 

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

579 
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

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

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

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

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

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

585 
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

586 
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

587 
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

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

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

590 

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

591 
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

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

593 

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

594 
definition [code del]: 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

595 
"floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

596 

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

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

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

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

600 
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

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

602 

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

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

604 

35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

605 
lemma floor_Fract: "floor (Fract a b) = a div b" 
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

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

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

608 

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

609 

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

611 

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

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

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

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

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

618 
@{thm True_implies_equals}, 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

619 
read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left}, 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

620 
read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left}, 
31100  621 
@{thm divide_1}, @{thm divide_zero_left}, 
622 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 

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

624 
@{thm of_int_minus}, @{thm of_int_diff}, 

625 
@{thm of_int_of_nat_eq}] 

626 
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors 

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

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

629 
*} 

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

630 

23342  631 

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

633 

24198  634 
class field_char_0 = field + ring_char_0 
23342  635 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33814
diff
changeset

636 
subclass (in linordered_field) field_char_0 .. 
23342  637 

27551  638 
context field_char_0 
639 
begin 

640 

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

23342  643 
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 
644 
apply (simp only: of_int_mult [symmetric]) 

645 
done 

646 

47906  647 
end 
648 

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

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

47906  653 
by transfer simp 
23342  654 

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

47906  656 
by transfer simp 
23342  657 

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

47906  659 
by transfer (simp add: add_frac_eq) 
23342  660 

23343  661 
lemma of_rat_minus: "of_rat ( a) =  of_rat a" 
47906  662 
by transfer simp 
23343  663 

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

665 
by (simp only: diff_minus of_rat_add of_rat_minus) 

666 

23342  667 
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" 
47906  668 
apply transfer 
23342  669 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 
670 
done 

671 

672 
lemma nonzero_of_rat_inverse: 

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

23343  674 
apply (rule inverse_unique [symmetric]) 
675 
apply (simp add: of_rat_mult [symmetric]) 

23342  676 
done 
677 

678 
lemma of_rat_inverse: 

36409  679 
"(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = 
23342  680 
inverse (of_rat a)" 
681 
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) 

682 

683 
lemma nonzero_of_rat_divide: 

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

685 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

686 

687 
lemma of_rat_divide: 

36409  688 
"(of_rat (a / b)::'a::{field_char_0, field_inverse_zero}) 
23342  689 
= of_rat a / of_rat b" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

690 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
23342  691 

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

694 
by (induct n) (simp_all add: of_rat_mult) 
23343  695 

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

47906  697 
apply transfer 
23343  698 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 
699 
apply (simp only: of_int_mult [symmetric] of_int_eq_iff) 

700 
done 

701 

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

702 
lemma of_rat_less: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33814
diff
changeset

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

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

705 
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

706 
assume not_zero: "b > 0" "d > 0" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

707 
then have "b * d > 0" by (rule mult_pos_pos) 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

709 
"(of_int a :: 'a) / of_int b < of_int c / of_int d 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

710 
\<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

711 
using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33814
diff
changeset

712 
show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

713 
\<longleftrightarrow> Fract a b < Fract c d" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

714 
using not_zero `b * d > 0` 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

715 
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

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

717 

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

718 
lemma of_rat_less_eq: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33814
diff
changeset

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

720 
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

721 

23343  722 
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] 
723 

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

724 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  725 
proof 
726 
fix a 

727 
show "of_rat a = id a" 

728 
by (induct a) 

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

729 
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) 
23343  730 
qed 
731 

732 
text{*Collapse nested embeddings*} 

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

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

735 

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

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

737 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  738 

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

739 
lemma of_rat_numeral_eq [simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

740 
"of_rat (numeral w) = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

741 
using of_rat_of_int_eq [of "numeral w"] by simp 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

742 

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

743 
lemma of_rat_neg_numeral_eq [simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

744 
"of_rat (neg_numeral w) = neg_numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

745 
using of_rat_of_int_eq [of "neg_numeral w"] by simp 
23343  746 

23879  747 
lemmas zero_rat = Zero_rat_def 
748 
lemmas one_rat = One_rat_def 

749 

24198  750 
abbreviation 
751 
rat_of_nat :: "nat \<Rightarrow> rat" 

752 
where 

753 
"rat_of_nat \<equiv> of_nat" 

754 

755 
abbreviation 

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

757 
where 

758 
"rat_of_int \<equiv> of_int" 

759 

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

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

761 

28001  762 
context field_char_0 
763 
begin 

764 

765 
definition 

766 
Rats :: "'a set" where 

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

767 
"Rats = range of_rat" 
28001  768 

769 
notation (xsymbols) 

770 
Rats ("\<rat>") 

771 

772 
end 

773 

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

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

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

776 

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

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

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

779 

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

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

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

782 

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

783 
lemma Rats_number_of [simp]: "numeral w \<in> Rats" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

784 
by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

785 

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

786 
lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

788 

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

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

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

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

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

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

794 

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

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

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

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

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

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

800 

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

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

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

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

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

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

806 

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

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

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

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

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

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

812 

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

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

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

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

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

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

818 

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

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

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

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

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

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

824 

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

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

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

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

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

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

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

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

832 

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

833 
lemma Rats_inverse [simp]: 
36409  834 
fixes a :: "'a::{field_char_0, field_inverse_zero}" 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

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

840 

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

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

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

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

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

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

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

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

848 

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

849 
lemma Rats_divide [simp]: 
36409  850 
fixes a b :: "'a::{field_char_0, field_inverse_zero}" 
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

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

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

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

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

856 

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

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

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

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

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

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

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

864 

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

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

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

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

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

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

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

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

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

873 

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

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

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

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

877 

28001  878 

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

879 
subsection {* Implementation of rational numbers as pairs of integers *} 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

880 

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

881 
text {* Formal constructor *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

882 

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

883 
definition Frct :: "int \<times> int \<Rightarrow> rat" where 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

884 
[simp]: "Frct p = Fract (fst p) (snd p)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

885 

36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset

886 
lemma [code abstype]: 
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset

887 
"Frct (quotient_of q) = q" 
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset

888 
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

889 

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

890 

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

891 
text {* Numerals *} 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

892 

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

893 
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

894 

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

895 
definition of_int :: "int \<Rightarrow> rat" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

897 
[code_abbrev]: "of_int = Int.of_int" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

899 

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

900 
lemma quotient_of_int [code abstract]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

901 
"quotient_of (Rat.of_int a) = (a, 1)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

902 
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

903 

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

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

905 
"numeral k = Rat.of_int (numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

907 

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

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

909 
"neg_numeral k = Rat.of_int (neg_numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

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

911 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

925 

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

926 

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

927 
text {* Operations *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

928 

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

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

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

931 
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

932 

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

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

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

935 
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

936 

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

937 
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

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

939 
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

940 
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

941 

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

942 
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

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

944 
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

945 

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

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

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

948 
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

949 
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

950 

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

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

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

953 
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

954 
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

955 

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

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

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

958 
in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

960 
case (Fract a b) then show ?thesis 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

963 

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

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

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

966 
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

967 
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

968 

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

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

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

971 
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

972 

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

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

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

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

976 
case (Fract a b) then show ?thesis 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

979 

43733
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset

980 
lemma rat_floor_code [code]: 
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset

981 
"floor p = (let (a, b) = quotient_of p in a div b)" 
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset

982 
by (cases p) (simp add: quotient_of_Fract floor_Fract) 
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset

983 

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

984 
instantiation rat :: equal 
26513  985 
begin 
986 

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

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

988 
"HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b" 
26513  989 

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

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

991 
qed (simp add: equal_rat_def quotient_of_inject_eq) 
26513  992 

28351  993 
lemma rat_eq_refl [code nbe]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

994 
"HOL.equal (r::rat) r \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset

995 
by (rule equal_refl) 
28351  996 

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

998 

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

999 
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

1000 
"p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)" 
35726  1001 
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

1002 

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

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

1004 
"p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" 
35726  1005 
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

1006 

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

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

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

1009 
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

1010 

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

1011 

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

1012 
text {* Quickcheck *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

1013 

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

1014 
definition (in term_syntax) 
32657  1015 
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where 
1016 
[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

1017 

37751  1018 
notation fcomp (infixl "\<circ>>" 60) 
1019 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1020 

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

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

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

1023 

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

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

1026 
let j = Code_Numeral.int_of (denom + 1) 
32657  1027 
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

1028 

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

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

1030 

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

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

1032 

37751  1033 
no_notation fcomp (infixl "\<circ>>" 60) 
1034 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1035 

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

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

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

1038 

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

1039 
definition 
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45694
diff
changeset

1040 
"exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d" 
42311
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1041 

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

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

1043 

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

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

1045 

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

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

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

1048 

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

1049 
definition 
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45694
diff
changeset

1050 
"full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k. 
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1051 
f (let j = Code_Numeral.int_of l + 1 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1052 
in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d" 
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset

1053 

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

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

1055 

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

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

1057 

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

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

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

1060 

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

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

1062 

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

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

1064 

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

1065 
lemma [code]: 
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
45818
diff
changeset

1066 
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" 
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
45818
diff
changeset

1067 
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) == 
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1068 
Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'') 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1069 
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []], 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1070 
Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))" 
43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1071 
by (rule partial_term_of_anything)+ 
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset

1072 

43887  1073 
instantiation rat :: narrowing 
1074 
begin 

1075 

1076 
definition 

45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1077 
"narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1078 
(Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing" 
43887  1079 

1080 
instance .. 

1081 

1082 
end 

1083 

1084 

45183
2e1ad4a54189
removing old code generator setup for rational numbers; tuned
bulwahn
parents:
43889
diff
changeset

1085 
subsection {* Setup for Nitpick *} 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

1086 

38287  1087 
declaration {* 
1088 
Nitpick_HOL.register_frac_type @{type_name rat} 

33209  1089 
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), 
1090 
(@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), 

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

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

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

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

37397
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset

1095 
(@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), 
33209  1096 
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), 
45478  1097 
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset

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

1099 

41792
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41231
diff
changeset

1100 
lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

1101 
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

1102 
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

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

1104 

35343  1105 
subsection{* Float syntax *} 
1106 

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

1108 

48891  1109 
ML_file "Tools/float_syntax.ML" 
35343  1110 
setup Float_Syntax.setup 
1111 

1112 
text{* Test: *} 

1113 
lemma "123.456 = 111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" 

1114 
by simp 

1115 

37143  1116 

47907  1117 
hide_const (open) normalize positive 
37143  1118 

47906  1119 
lemmas [transfer_rule del] = 
1120 
rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer 

1121 
Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer 

1122 
uminus_rat.transfer times_rat.transfer inverse_rat.transfer 

47907  1123 
positive.transfer of_rat.transfer 
47906  1124 

1125 
text {* Deregister @{text "rat"} as a quotient type: *} 

1126 

47952  1127 
declare Quotient_rat[quot_del] 
47906  1128 

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

1129 
end 