author  hoelzl 
Tue, 12 Nov 2013 19:28:51 +0100  
changeset 54409  2e501a90dec7 
parent 54230  b1d955791529 
child 54489  03ff4d1e6784 
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 

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

52 
lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\<lambda>x. snd x \<noteq> 0)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
52146
diff
changeset

53 
by (simp add: rat.domain_eq) 
27551  54 

55 
subsubsection {* Representation and basic operations *} 

56 

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

59 
by simp 

27551  60 

61 
lemma eq_rat: 

62 
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

63 
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

64 
and "\<And>a c. Fract 0 a = Fract 0 c" 
47906  65 
by (transfer, simp)+ 
27551  66 

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

67 
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

68 
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

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

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

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

73 
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

74 
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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
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

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

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

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

86 
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

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

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

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

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

91 
note assms 
47906  92 
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

93 
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

94 
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

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

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

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

98 

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

99 
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

100 
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

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

102 
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

103 

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

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

106 

47906  107 
lift_definition zero_rat :: "rat" is "(0, 1)" 
108 
by simp 

109 

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

111 
by simp 

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

112 

47906  113 
lemma Zero_rat_def: "0 = Fract 0 1" 
114 
by transfer simp 

18913  115 

47906  116 
lemma One_rat_def: "1 = Fract 1 1" 
117 
by transfer simp 

118 

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

120 
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

121 
by (clarsimp, simp add: distrib_right, simp add: mult_ac) 
27551  122 

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

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

47906  126 
using assms by transfer simp 
18913  127 

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

27551  130 

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

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

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

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

136 

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

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

138 
diff_rat_def: "q  r = q +  (r::rat)" 
18913  139 

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

140 
lemma diff_rat [simp]: 
27551  141 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
142 
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

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

144 

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

147 
by (simp add: mult_ac) 

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

148 

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

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

151 

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

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

47906  155 
using assms by transfer simp 
156 

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

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

159 
by (auto simp add: mult_commute) 

160 

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

162 
by transfer simp 

163 

164 
definition 

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

166 

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

168 
by (simp add: divide_rat_def) 

27509  169 

170 
instance proof 

47906  171 
fix q r s :: rat 
172 
show "(q * r) * s = q * (r * s)" 

173 
by transfer simp 

174 
show "q * r = r * q" 

175 
by transfer simp 

176 
show "1 * q = q" 

177 
by transfer simp 

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

179 
by transfer (simp add: algebra_simps) 

180 
show "q + r = r + q" 

181 
by transfer simp 

182 
show "0 + q = q" 

183 
by transfer simp 

184 
show " q + q = 0" 

185 
by transfer simp 

186 
show "q  r = q +  r" 

187 
by (fact diff_rat_def) 

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

189 
by transfer (simp add: algebra_simps) 

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

191 
by transfer simp 

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

193 
by transfer simp } 

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

195 
by (fact divide_rat_def) 

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

197 
by transfer simp 

27509  198 
qed 
199 

200 
end 

201 

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

203 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  204 

205 
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

206 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  207 

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

209 
by (rule of_nat_rat [symmetric]) 

210 

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

212 
by (rule of_int_rat [symmetric]) 

213 

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

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

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

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

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

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

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

222 
by (simp_all add: Zero_rat_def One_rat_def eq_rat) 
27551  223 

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

224 
lemma rat_number_expand: 
27551  225 
"0 = Fract 0 1" 
226 
"1 = Fract 1 1" 

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

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

228 
"neg_numeral k = Fract (neg_numeral k) 1" 
27551  229 
by (simp_all add: rat_number_collapse) 
230 

231 
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

232 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
27551  233 
assumes 0: "q = 0 \<Longrightarrow> C" 
234 
shows C 

235 
proof (cases "q = 0") 

236 
case True then show C using 0 by auto 

237 
next 

238 
case False 

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

239 
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

240 
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

241 
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

242 
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast 
27551  243 
qed 
244 

33805  245 
subsubsection {* Function @{text normalize} *} 
246 

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

247 
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

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

249 
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

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

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

252 
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

253 
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

254 
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

255 
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

256 
qed 
33805  257 

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

258 
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

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

260 
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

261 
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

262 

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

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

264 
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

265 
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

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

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

268 
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

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

270 
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

271 
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

272 
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

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

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

275 
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) 
33805  276 
qed 
277 

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

278 
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

279 
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

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

281 

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

282 
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

283 
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

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

285 

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

286 
lemma normalize_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

287 
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

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

289 

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

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

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

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

293 

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

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

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

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

297 

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

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

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

300 
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

301 

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

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

303 
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

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

305 

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

306 
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

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

308 
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

309 

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

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

311 
"\<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

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

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

314 
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

315 
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

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

317 
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

318 
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

319 
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

320 
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

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

322 
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

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

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

325 
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

326 
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

327 
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

328 
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

329 
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

330 
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

331 
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

332 
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

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

335 
with p show "p = (a, b)" by simp 
33805  336 
qed 
337 
qed 

338 

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

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

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

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

342 
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

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

345 
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

346 
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

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

348 
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

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

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

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

352 
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

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

354 

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

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

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

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

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

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

360 
by (simp_all add: rat_number_expand quotient_of_Fract) 
33805  361 

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

362 
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

363 
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

364 

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

365 
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

366 
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

367 

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

368 
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

369 
by (cases r) (simp add: quotient_of_Fract normalize_coprime) 
33805  370 

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

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

372 
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

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

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

375 
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

376 
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

377 
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

378 
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

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

380 

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

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

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

383 
by (auto simp add: quotient_of_inject) 
33805  384 

27551  385 

386 
subsubsection {* Various *} 

387 

388 
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

389 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  390 

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

391 
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

392 
by (simp add: rat_number_expand) 
27551  393 

50178  394 
lemma quotient_of_div: 
395 
assumes r: "quotient_of r = (n,d)" 

396 
shows "r = of_int n / of_int d" 

397 
proof  

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

399 
have "r = Fract n d" by simp 

400 
thus ?thesis using Fract_of_int_quotient by simp 

401 
qed 

27551  402 

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

27509  404 

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

407 
proof (clarsimp) 

408 
fix a b c d :: int 

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

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

411 
by simp 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52146
diff
changeset

412 
hence "a * b * d\<^sup>2 = c * d * b\<^sup>2" 
47907  413 
unfolding power2_eq_square by (simp add: mult_ac) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52146
diff
changeset

414 
hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2" 
47907  415 
by simp 
416 
thus "0 < a * b \<longleftrightarrow> 0 < c * d" 

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

418 
by (simp add: zero_less_mult_iff) 

419 
qed 

420 

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

422 
by transfer simp 

423 

424 
lemma positive_add: 

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

426 
apply transfer 

427 
apply (simp add: zero_less_mult_iff) 

428 
apply (elim disjE, simp_all add: add_pos_pos add_neg_neg 

429 
mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg) 

430 
done 

431 

432 
lemma positive_mult: 

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

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

435 

436 
lemma positive_minus: 

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

438 
by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff) 

439 

440 
instantiation rat :: linordered_field_inverse_zero 

27509  441 
begin 
442 

47907  443 
definition 
444 
"x < y \<longleftrightarrow> positive (y  x)" 

445 

446 
definition 

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

448 

449 
definition 

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

451 

452 
definition 

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

47906  454 

47907  455 
instance proof 
456 
fix a b c :: rat 

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

458 
by (rule abs_rat_def) 

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

460 
unfolding less_eq_rat_def less_rat_def 

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

462 
show "a \<le> a" 

463 
unfolding less_eq_rat_def by simp 

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

465 
unfolding less_eq_rat_def less_rat_def 

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

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

468 
unfolding less_eq_rat_def less_rat_def 

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

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

471 
unfolding less_eq_rat_def less_rat_def by auto 
47907  472 
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else  1)" 
473 
by (rule sgn_rat_def) 

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

475 
unfolding less_eq_rat_def less_rat_def 

476 
by (auto dest!: positive_minus) 

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

478 
unfolding less_rat_def 

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

47906  480 
qed 
27551  481 

47907  482 
end 
483 

484 
instantiation rat :: distrib_lattice 

485 
begin 

486 

487 
definition 

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

27509  489 

490 
definition 

47907  491 
"(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max" 
492 

493 
instance proof 

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

495 

496 
end 

497 

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

499 
by transfer simp 

27509  500 

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

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

47907  504 
using assms unfolding less_rat_def 
505 
by (simp add: positive_rat algebra_simps) 

27509  506 

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

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

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

27551  511 

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

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

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

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

517 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  518 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
519 

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

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

522 
shows "P q" 

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

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

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

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

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

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

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

530 
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

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

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

533 
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

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

535 

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

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

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

538 
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

539 

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

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

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

542 
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

543 

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

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

545 
"0 < b \<Longrightarrow> 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

546 
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

547 

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

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

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

550 
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

551 

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

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

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

554 
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

555 

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

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

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

558 
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

559 

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

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

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

562 
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

563 

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

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

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

566 
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

567 

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

568 

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

569 
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

570 

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

571 
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

572 
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

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

574 
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

575 
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

576 
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

577 
unfolding Fract_of_int_quotient 
36409  578 
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

579 
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

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

581 

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

582 
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

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

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

585 
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

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

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

588 
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

589 
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

590 
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

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

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

593 

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

594 
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

595 
begin 
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 
definition [code del]: 
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset

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

599 

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

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

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

602 
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

603 
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

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

605 

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

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

607 

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

608 
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

609 
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

610 
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

611 

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

612 

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

614 

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

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

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

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

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

621 
@{thm True_implies_equals}, 

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

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

623 
read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left}, 
31100  624 
@{thm divide_1}, @{thm divide_zero_left}, 
625 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 

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

627 
@{thm of_int_minus}, @{thm of_int_diff}, 

628 
@{thm of_int_of_nat_eq}] 

629 
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors 

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

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

632 
*} 

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

633 

23342  634 

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

636 

24198  637 
class field_char_0 = field + ring_char_0 
23342  638 

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

639 
subclass (in linordered_field) field_char_0 .. 
23342  640 

27551  641 
context field_char_0 
642 
begin 

643 

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

23342  646 
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 
647 
apply (simp only: of_int_mult [symmetric]) 

648 
done 

649 

47906  650 
end 
651 

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

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

47906  656 
by transfer simp 
23342  657 

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

47906  659 
by transfer simp 
23342  660 

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

47906  662 
by transfer (simp add: add_frac_eq) 
23342  663 

23343  664 
lemma of_rat_minus: "of_rat ( a) =  of_rat a" 
47906  665 
by transfer simp 
23343  666 

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

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

23342  670 
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" 
47906  671 
apply transfer 
23342  672 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 
673 
done 

674 

675 
lemma nonzero_of_rat_inverse: 

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

23343  677 
apply (rule inverse_unique [symmetric]) 
678 
apply (simp add: of_rat_mult [symmetric]) 

23342  679 
done 
680 

681 
lemma of_rat_inverse: 

36409  682 
"(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = 
23342  683 
inverse (of_rat a)" 
684 
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) 

685 

686 
lemma nonzero_of_rat_divide: 

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

688 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

689 

690 
lemma of_rat_divide: 

36409  691 
"(of_rat (a / b)::'a::{field_char_0, field_inverse_zero}) 
23342  692 
= 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

693 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
23342  694 

23343  695 
lemma of_rat_power: 
31017  696 
"(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

697 
by (induct n) (simp_all add: of_rat_mult) 
23343  698 

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

47906  700 
apply transfer 
23343  701 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 
702 
apply (simp only: of_int_mult [symmetric] of_int_eq_iff) 

703 
done 

704 

54409  705 
lemma of_rat_eq_0_iff [simp]: "(of_rat a = 0) = (a = 0)" 
706 
using of_rat_eq_iff [of _ 0] by simp 

707 

708 
lemma zero_eq_of_rat_iff [simp]: "(0 = of_rat a) = (0 = a)" 

709 
by simp 

710 

711 
lemma of_rat_eq_1_iff [simp]: "(of_rat a = 1) = (a = 1)" 

712 
using of_rat_eq_iff [of _ 1] by simp 

713 

714 
lemma one_eq_of_rat_iff [simp]: "(1 = of_rat a) = (1 = a)" 

715 
by simp 

716 

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

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

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

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

720 
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

721 
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

722 
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

723 
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

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

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

726 
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

727 
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

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

729 
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

730 
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

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

732 

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

733 
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

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

735 
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

736 

54409  737 
lemma of_rat_le_0_iff [simp]: "((of_rat r :: 'a::linordered_field) \<le> 0) = (r \<le> 0)" 
738 
using of_rat_less_eq [of r 0, where 'a='a] by simp 

739 

740 
lemma zero_le_of_rat_iff [simp]: "(0 \<le> (of_rat r :: 'a::linordered_field)) = (0 \<le> r)" 

741 
using of_rat_less_eq [of 0 r, where 'a='a] by simp 

742 

743 
lemma of_rat_le_1_iff [simp]: "((of_rat r :: 'a::linordered_field) \<le> 1) = (r \<le> 1)" 

744 
using of_rat_less_eq [of r 1] by simp 

745 

746 
lemma one_le_of_rat_iff [simp]: "(1 \<le> (of_rat r :: 'a::linordered_field)) = (1 \<le> r)" 

747 
using of_rat_less_eq [of 1 r] by simp 

748 

749 
lemma of_rat_less_0_iff [simp]: "((of_rat r :: 'a::linordered_field) < 0) = (r < 0)" 

750 
using of_rat_less [of r 0, where 'a='a] by simp 

751 

752 
lemma zero_less_of_rat_iff [simp]: "(0 < (of_rat r :: 'a::linordered_field)) = (0 < r)" 

753 
using of_rat_less [of 0 r, where 'a='a] by simp 

754 

755 
lemma of_rat_less_1_iff [simp]: "((of_rat r :: 'a::linordered_field) < 1) = (r < 1)" 

756 
using of_rat_less [of r 1] by simp 

757 

758 
lemma one_less_of_rat_iff [simp]: "(1 < (of_rat r :: 'a::linordered_field)) = (1 < r)" 

759 
using of_rat_less [of 1 r] by simp 

23343  760 

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

761 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  762 
proof 
763 
fix a 

764 
show "of_rat a = id a" 

765 
by (induct a) 

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

766 
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) 
23343  767 
qed 
768 

769 
text{*Collapse nested embeddings*} 

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

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

772 

773 
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

774 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  775 

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

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

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

778 
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

779 

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

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

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

782 
using of_rat_of_int_eq [of "neg_numeral w"] by simp 
23343  783 

23879  784 
lemmas zero_rat = Zero_rat_def 
785 
lemmas one_rat = One_rat_def 

786 

24198  787 
abbreviation 
788 
rat_of_nat :: "nat \<Rightarrow> rat" 

789 
where 

790 
"rat_of_nat \<equiv> of_nat" 

791 

792 
abbreviation 

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

794 
where 

795 
"rat_of_int \<equiv> of_int" 

796 

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

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

798 

28001  799 
context field_char_0 
800 
begin 

801 

802 
definition 

803 
Rats :: "'a set" where 

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

804 
"Rats = range of_rat" 
28001  805 

806 
notation (xsymbols) 

807 
Rats ("\<rat>") 

808 

809 
end 

810 

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

811 
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

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

813 

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

814 
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

815 
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

816 

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

817 
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

818 
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

819 

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

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

821 
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

822 

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

823 
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

824 
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

825 

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

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

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

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

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

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

831 

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

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

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

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

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

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

837 

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

838 
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

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

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

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

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

843 

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

844 
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

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

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

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

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

849 

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

850 
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

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

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

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

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

855 

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

856 
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

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

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

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

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

861 

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

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

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

864 
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

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

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

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

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

869 

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

870 
lemma Rats_inverse [simp]: 
36409  871 
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

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

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

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

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

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

877 

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

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

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

880 
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

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

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

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

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

885 

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

886 
lemma Rats_divide [simp]: 
36409  887 
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

888 
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

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

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

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

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

893 

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

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

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

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

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

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

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

901 

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

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

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

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

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

906 
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

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

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

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

910 

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

911 
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

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

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

914 

28001  915 

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

916 
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

917 

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

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

919 

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

920 
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

921 
[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

922 

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

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

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

925 
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

926 

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

927 

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

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

929 

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

930 
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

931 

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

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

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

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

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

936 

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

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

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

939 
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

940 

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

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

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

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

944 

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

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

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

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

948 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

962 

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

963 

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

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

965 

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

966 
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

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

968 
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

969 

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

970 
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

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

972 
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

973 

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

974 
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

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

976 
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

977 
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

978 

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

979 
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

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

981 
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

982 

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

983 
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

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

985 
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

986 
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

987 

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

988 
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

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

990 
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

991 
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

992 

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

993 
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

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

995 
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

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

997 
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

998 
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

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

1000 

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

1001 
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

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

1003 
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

1004 
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

1005 

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

1006 
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

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

1008 
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

1009 

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

1010 
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

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

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

1013 
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

1014 
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

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

1016 

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

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

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

1019 
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

1020 

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

1021 
instantiation rat :: equal 
26513  1022 
begin 
1023 

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

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

1025 
"HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b" 
26513  1026 

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

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

1028 
qed (simp add: equal_rat_def quotient_of_inject_eq) 
26513  1029 

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

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

1032 
by (rule equal_refl) 
28351  1033 

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

1035 

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

1036 
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

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

1039 

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

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

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

1043 

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

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

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

1046 
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

1047 

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

1048 

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

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

1050 

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

1051 
definition (in term_syntax) 
32657  1052 
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 
1053 
[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

1054 

37751  1055 
notation fcomp (infixl "\<circ>>" 60) 
1056 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1057 

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

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

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

1060 

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

1061 
definition 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50178
diff
changeset

1062 
"Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair ( 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

1063 
let j = int_of_integer (integer_of_natural (denom + 1)) 
32657  1064 
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

1065 

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

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

1067 

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

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

1069 

37751  1070 
no_notation fcomp (infixl "\<circ>>" 60) 
1071 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1072 

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

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

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

1075 

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

1076 
definition 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

1077 
"exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

1078 
(\<lambda>l. Quickcheck_Exhaustive.exhaustive (\<lambda>k. f (Fract k (int_of_integer (integer_of_natural l) + 1))) d) d" 
42311
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset

1079 

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

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

1081 

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

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

1083 

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

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

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

1086 

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

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

1088 
"full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k. 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

1089 
f (let j = int_of_integer (integer_of_natural l) + 1 
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset

1090 
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

1091 

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

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

1093 

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

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

1095 

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

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

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

1098 

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

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

1100 

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

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

1102 

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

1103 
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

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

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

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

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

1108 
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

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

1110 

43887  1111 
instantiation rat :: narrowing 
1112 
begin 

1113 

1114 
definition 

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

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

1116 
(Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing" 
43887  1117 

1118 
instance .. 

1119 

1120 
end 

1121 

1122 

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

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

1124 

38287  1125 
declaration {* 
1126 
Nitpick_HOL.register_frac_type @{type_name rat} 

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

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

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

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

1132 
(@{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

1133 
(@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), 
33209  1134 
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), 
45478  1135 
(@{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

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

1137 

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

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

1139 
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

1140 
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

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

1142 

52146  1143 

1144 
subsection {* Float syntax *} 

35343  1145 

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

1147 

52146  1148 
parse_translation {* 
1149 
let 

1150 
fun mk_number i = 

1151 
let 

1152 
fun mk 1 = Syntax.const @{const_syntax Num.One} 

1153 
 mk i = 

1154 
let val (q, r) = Integer.div_mod i 2 

1155 
in HOLogic.mk_bit r $ (mk q) end; 

1156 
in 

1157 
if i = 0 then Syntax.const @{const_syntax Groups.zero} 

1158 
else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i 

1159 
else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i) 

1160 
end; 

1161 

1162 
fun mk_frac str = 

1163 
let 

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

1165 
val exp = Syntax.const @{const_syntax Power.power}; 

1166 
val ten = mk_number 10; 

1167 
val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; 

1168 
in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end; 

1169 

1170 
fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u 

1171 
 float_tr [t as Const (str, _)] = mk_frac str 

1172 
 float_tr ts = raise TERM ("float_tr", ts); 

1173 
in [(@{syntax_const "_Float"}, K float_tr)] end 

1174 
*} 

35343  1175 

1176 
text{* Test: *} 

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

52146  1178 
by simp 
35343  1179 

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

1180 
subsection {* Hiding implementation details *} 
37143  1181 

47907  1182 
hide_const (open) normalize positive 
37143  1183 

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

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

1185 
lifting_forget rat.lifting 
47906  1186 

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

1187 
end 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

1188 