author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 47906  09a896d295bd 
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 
35343  9 
uses ("Tools/float_syntax.ML") 
15131  10 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

11 

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

13 

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

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

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

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

19 

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

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

23 

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

18913  26 

27 
lemma sym_ratrel: "sym ratrel" 

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

29 

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

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

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

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

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

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

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

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

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

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

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

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

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

44 
qed 
27551  45 

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

40815  47 
by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel]) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

48 

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

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

51 

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

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

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

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

56 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45507
diff
changeset

57 
definition "Rat = {x. snd x \<noteq> 0} // ratrel" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45507
diff
changeset

58 

4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45507
diff
changeset

59 
typedef (open) rat = Rat 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45507
diff
changeset

60 
morphisms Rep_Rat Abs_Rat 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45507
diff
changeset

61 
unfolding Rat_def 
27551  62 
proof 
63 
have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp 

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

65 
qed 

66 

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

68 
by (simp add: Rat_def quotientI) 

69 

70 
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] 

71 

72 

73 
subsubsection {* Representation and basic operations *} 

74 

75 
definition 

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

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

77 
"Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" 
27551  78 

79 
lemma eq_rat: 

80 
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

81 
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

82 
and "\<And>a c. Fract 0 a = Fract 0 c" 
27551  83 
by (simp_all add: Fract_def) 
84 

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

85 
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

86 
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

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

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

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

90 
by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

91 
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

92 
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

93 
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

94 
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

95 
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

96 
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

97 
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

98 
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

99 
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

100 
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

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

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

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

104 
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

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

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

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

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

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

110 
moreover from q have "q = Fract ( ?a) ( ?b)" by (simp add: Fract_def) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

111 
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

112 
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

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

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

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

116 

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

117 
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

118 
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

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

120 
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

121 

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

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

124 

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

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

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

127 

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

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

129 
One_rat_def: "1 = Fract 1 1" 
18913  130 

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

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

132 
add_rat_def: 
27551  133 
"q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
134 
ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" 

135 

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

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

139 
proof  

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

141 
respects2 ratrel" 

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

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

144 
qed 

18913  145 

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

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

147 
minus_rat_def: 
27551  148 
" q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {( fst x, snd x)})" 
149 

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

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

40819
2ac5af6eb8a8
adapted proofs to slightly changed definitions of congruent(2)
haftmann
parents:
40816
diff
changeset

153 
by (simp add: congruent_def split_paired_all) 
27551  154 
then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel) 
155 
qed 

156 

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

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

159 

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

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

161 
diff_rat_def: "q  r = q +  (r::rat)" 
18913  162 

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

163 
lemma diff_rat [simp]: 
27551  164 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
165 
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

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

167 

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

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

169 
mult_rat_def: 
27551  170 
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
171 
ratrel``{(fst x * fst y, snd x * snd y)})" 

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

172 

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

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

176 
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all 

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

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

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

179 

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

180 
lemma mult_rat_cancel: 
27551  181 
assumes "c \<noteq> 0" 
182 
shows "Fract (c * a) (c * b) = Fract a b" 

183 
proof  

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

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

185 
then show ?thesis by (simp add: mult_rat [symmetric]) 
27551  186 
qed 
27509  187 

188 
instance proof 

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

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

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

193 
by (cases q, cases r) (simp add: eq_rat) 
27551  194 
next 
195 
fix q :: rat show "1 * q = q" 

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

196 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  197 
next 
198 
fix q r s :: rat show "(q + r) + s = q + (r + s)" 

29667  199 
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) 
27551  200 
next 
201 
fix q r :: rat show "q + r = r + q" 

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

202 
by (cases q, cases r) (simp add: eq_rat) 
27551  203 
next 
204 
fix q :: rat show "0 + q = q" 

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

205 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  206 
next 
207 
fix q :: rat show " q + q = 0" 

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

208 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  209 
next 
210 
fix q r :: rat show "q  r = q +  r" 

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

211 
by (cases q, cases r) (simp add: eq_rat) 
27551  212 
next 
213 
fix q r s :: rat show "(q + r) * s = q * s + r * s" 

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

27509  217 
qed 
218 

219 
end 

220 

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

222 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  223 

224 
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

225 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  226 

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

228 
by (rule of_nat_rat [symmetric]) 

229 

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

231 
by (rule of_int_rat [symmetric]) 

232 

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

233 
lemma rat_number_collapse: 
27551  234 
"Fract 0 k = 0" 
235 
"Fract 1 1 = 1" 

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

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

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

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

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

241 
by (simp_all add: Zero_rat_def One_rat_def eq_rat) 
27551  242 

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

243 
lemma rat_number_expand: 
27551  244 
"0 = Fract 0 1" 
245 
"1 = Fract 1 1" 

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

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

247 
"neg_numeral k = Fract (neg_numeral k) 1" 
27551  248 
by (simp_all add: rat_number_collapse) 
249 

250 
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

251 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
27551  252 
assumes 0: "q = 0 \<Longrightarrow> C" 
253 
shows C 

254 
proof (cases "q = 0") 

255 
case True then show C using 0 by auto 

256 
next 

257 
case False 

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

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

260 
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

261 
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast 
27551  262 
qed 
263 

33805  264 
subsubsection {* Function @{text normalize} *} 
265 

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

266 
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

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

268 
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

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

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

271 
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

272 
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

273 
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

274 
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

275 
qed 
33805  276 

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

277 
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

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

279 
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

280 
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

281 

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

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

283 
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

284 
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

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

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

287 
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

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

289 
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

290 
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

291 
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

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

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

294 
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) 
33805  295 
qed 
296 

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

297 
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

298 
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

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

300 

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

301 
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

302 
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

303 
split:split_if_asm) 
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 
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

306 
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

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

308 

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

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

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

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

312 

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

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

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

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

316 

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

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

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

319 
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

320 

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

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

322 
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

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

324 

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

325 
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

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

327 
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

328 

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

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

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

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

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

333 
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

334 
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

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

336 
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

337 
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

338 
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

339 
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

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

341 
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

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

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

344 
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

345 
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

346 
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

347 
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

348 
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

349 
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

350 
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

351 
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

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

354 
with p show "p = (a, b)" by simp 
33805  355 
qed 
356 
qed 

357 

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

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

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

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

361 
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

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

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

364 
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

365 
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

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

367 
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

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

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

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

371 
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

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

373 

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

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

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

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

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

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

379 
by (simp_all add: rat_number_expand quotient_of_Fract) 
33805  380 

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

381 
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

382 
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

383 

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

384 
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

385 
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

386 

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

387 
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

388 
by (cases r) (simp add: quotient_of_Fract normalize_coprime) 
33805  389 

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

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

391 
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

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

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

394 
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

395 
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

396 
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

397 
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

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

399 

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

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

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

402 
by (auto simp add: quotient_of_inject) 
33805  403 

27551  404 

405 
subsubsection {* The field of rational numbers *} 

406 

36409  407 
instantiation rat :: field_inverse_zero 
27551  408 
begin 
409 

410 
definition 

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

411 
inverse_rat_def: 
27551  412 
"inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q. 
413 
ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" 

414 

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

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

418 
by (auto simp add: congruent_def mult_commute) 

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

27509  420 
qed 
421 

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

423 
divide_rat_def: "q / r = q * inverse (r::rat)" 
27551  424 

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

425 
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

426 
by (simp add: divide_rat_def) 
27551  427 

428 
instance proof 

429 
fix q :: rat 

430 
assume "q \<noteq> 0" 

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

35216  432 
(simp_all add: rat_number_expand eq_rat) 
27551  433 
next 
434 
fix q r :: rat 

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

36415  436 
next 
437 
show "inverse 0 = (0::rat)" by (simp add: rat_number_expand, simp add: rat_number_collapse) 

438 
qed 

27551  439 

440 
end 

441 

442 

443 
subsubsection {* Various *} 

444 

445 
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

446 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  447 

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

448 
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

449 
by (simp add: rat_number_expand) 
27551  450 

451 

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

27509  453 

454 
instantiation rat :: linorder 

455 
begin 

456 

457 
definition 

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

458 
le_rat_def: 
39910  459 
"q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
27551  460 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
461 

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

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

465 
proof  

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

467 
respects2 ratrel" 

468 
proof (clarsimp simp add: congruent2_def) 

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

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

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

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

473 

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

475 
{ 

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

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

478 
proof  

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

480 
hence "?le a b c d = 

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

482 
by (simp add: mult_le_cancel_right) 

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

484 
by (simp add: mult_ac) 

485 
finally show ?thesis . 

486 
qed 

487 
} note le_factor = this 

488 

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

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

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

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

493 
by (rule le_factor) 

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

497 
by (simp only: eq1 eq2) 

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

499 
by (simp add: mult_ac) 

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

501 
by (rule le_factor [symmetric]) 

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

503 
qed 

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

505 
qed 

27509  506 

507 
definition 

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

508 
less_rat_def: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" 
27509  509 

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

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

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

513 
using assms by (simp add: less_rat_def eq_rat order_less_le) 
27509  514 

515 
instance proof 

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

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

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

518 
assume "q \<le> r" and "r \<le> s" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

519 
then show "q \<le> s" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

521 
fix a b c d e f :: int 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

522 
assume neq: "b > 0" "d > 0" "f > 0" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

524 
show "Fract a b \<le> Fract e f" 
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 
from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

530 
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

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

533 
qed 
27668  534 
also have "... = (c * f) * (d * f) * (b * b)" by algebra 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

537 
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

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

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

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

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

543 
with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

549 
assume "q \<le> r" and "r \<le> q" 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

550 
then show "q = r" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

552 
fix a b c d :: int 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

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

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

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

557 
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

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

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

561 
from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

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

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

565 
finally have "(a * d) * (b * d) = (c * b) * (b * d)" . 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

566 
moreover from neq have "b * d \<noteq> 0" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

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

573 
by (induct q) simp 
27682  574 
show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" 
575 
by (induct q, induct r) (auto simp add: le_less mult_commute) 

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

576 
show "q \<le> r \<or> r \<le> q" 
18913  577 
by (induct q, induct r) 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

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

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

581 

27509  582 
end 
583 

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

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

586 

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

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

588 
abs_rat_def: "\<bar>q\<bar> = (if q < 0 then q else (q::rat))" 
27551  589 

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

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

593 
definition 

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

594 
sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else  1)" 
27551  595 

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

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

598 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  599 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
600 

601 
definition 

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

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

603 

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

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

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

606 

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

22456  609 

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

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

611 

36409  612 
instance rat :: linordered_field_inverse_zero 
27551  613 
proof 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

617 
fix a b c d e f :: int 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

618 
assume neq: "b > 0" "d > 0" "f > 0" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

622 
let ?F = "f * f" from neq have F: "0 < ?F" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

624 
from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

626 
with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

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

633 
fix a b c d e f :: int 
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

634 
assume neq: "b > 0" "d > 0" "f > 0" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

637 
show "Fract e f * Fract a b < Fract e f * Fract c d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

640 
from neq gt have "0 < ?E" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

641 
by (auto simp add: Zero_rat_def order_less_le eq_rat) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

644 
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

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

646 
ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

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

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

653 

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

656 
shows "P q" 

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

657 
proof (cases q) 
27551  658 
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

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

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

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

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

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

664 
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

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

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

667 
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

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

669 

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

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

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

672 
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

673 

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

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

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

676 
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

677 

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

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

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

680 
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

681 

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

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

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

684 
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

685 

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

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

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

688 
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

689 

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

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

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

692 
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

693 

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

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

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

696 
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

697 

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

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

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

700 
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

701 

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

702 

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

703 
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

704 

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

705 
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

706 
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

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

708 
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

709 
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

710 
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

711 
unfolding Fract_of_int_quotient 
36409  712 
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

713 
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

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

715 

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

716 
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

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

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

719 
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

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

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

722 
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

723 
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

724 
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

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

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

727 

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

728 
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

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

730 

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

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

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

733 

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

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

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

736 
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

737 
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

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

739 

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

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

741 

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

742 
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

743 
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

744 
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

745 

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

746 

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

748 

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

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

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

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

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

755 
@{thm True_implies_equals}, 

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

756 
read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib}, 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset

757 
read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib}, 
31100  758 
@{thm divide_1}, @{thm divide_zero_left}, 
759 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 

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

761 
@{thm of_int_minus}, @{thm of_int_diff}, 

762 
@{thm of_int_of_nat_eq}] 

763 
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors 

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

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

766 
*} 

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

767 

23342  768 

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

770 

24198  771 
class field_char_0 = field + ring_char_0 
23342  772 

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

773 
subclass (in linordered_field) field_char_0 .. 
23342  774 

27551  775 
context field_char_0 
776 
begin 

777 

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

39910  779 
"of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})" 
23342  780 

27551  781 
end 
782 

23342  783 
lemma of_rat_congruent: 
27551  784 
"(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel" 
40816
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

785 
apply (rule congruentI) 
23342  786 
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 
787 
apply (simp only: of_int_mult [symmetric]) 

788 
done 

789 

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

23342  792 

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

794 
by (simp add: Zero_rat_def of_rat_rat) 

795 

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

797 
by (simp add: One_rat_def of_rat_rat) 

798 

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

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

800 
by (induct a, induct b, simp add: of_rat_rat add_frac_eq) 
23342  801 

23343  802 
lemma of_rat_minus: "of_rat ( a) =  of_rat a" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

803 
by (induct a, simp add: of_rat_rat) 
23343  804 

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

806 
by (simp only: diff_minus of_rat_add of_rat_minus) 

807 

23342  808 
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

809 
apply (induct a, induct b, simp add: of_rat_rat) 
23342  810 
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) 
811 
done 

812 

813 
lemma nonzero_of_rat_inverse: 

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

23343  815 
apply (rule inverse_unique [symmetric]) 
816 
apply (simp add: of_rat_mult [symmetric]) 

23342  817 
done 
818 

819 
lemma of_rat_inverse: 

36409  820 
"(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = 
23342  821 
inverse (of_rat a)" 
822 
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) 

823 

824 
lemma nonzero_of_rat_divide: 

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

826 
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) 

827 

828 
lemma of_rat_divide: 

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

831 
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) 
23342  832 

23343  833 
lemma of_rat_power: 
31017  834 
"(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

835 
by (induct n) (simp_all add: of_rat_mult) 
23343  836 

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

838 
apply (induct a, induct b) 

839 
apply (simp add: of_rat_rat eq_rat) 

840 
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) 

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

842 
done 

843 

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

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

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

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

847 
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

848 
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

849 
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

850 
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

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

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

853 
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

854 
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

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

856 
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

857 
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

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

859 

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

860 
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

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

862 
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

863 

23343  864 
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] 
865 

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

866 
lemma of_rat_eq_id [simp]: "of_rat = id" 
23343  867 
proof 
868 
fix a 

869 
show "of_rat a = id a" 

870 
by (induct a) 

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

871 
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) 
23343  872 
qed 
873 

874 
text{*Collapse nested embeddings*} 

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

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

877 

878 
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

879 
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) 
23343  880 

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

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

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

883 
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

884 

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

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

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

887 
using of_rat_of_int_eq [of "neg_numeral w"] by simp 
23343  888 

23879  889 
lemmas zero_rat = Zero_rat_def 
890 
lemmas one_rat = One_rat_def 

891 

24198  892 
abbreviation 
893 
rat_of_nat :: "nat \<Rightarrow> rat" 

894 
where 

895 
"rat_of_nat \<equiv> of_nat" 

896 

897 
abbreviation 

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

899 
where 

900 
"rat_of_int \<equiv> of_int" 

901 

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

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

903 

28001  904 
context field_char_0 
905 
begin 

906 

907 
definition 

908 
Rats :: "'a set" where 

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

909 
"Rats = range of_rat" 
28001  910 

911 
notation (xsymbols) 

912 
Rats ("\<rat>") 

913 

914 
end 

915 

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

916 
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

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

918 

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

919 
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

920 
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

921 

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

922 
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

923 
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

924 

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

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

926 
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

927 

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

928 
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

929 
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

930 

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

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

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

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

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

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

936 

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

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

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

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

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

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

942 

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

943 
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

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

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

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

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

948 

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

949 
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

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

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

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

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

954 

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

955 
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

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

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

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

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

960 

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

961 
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

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

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

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

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

966 

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

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

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

969 
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

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

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

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

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

974 

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

975 
lemma Rats_inverse [simp]: 
36409  976 
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

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

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

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

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

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

982 

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

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

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

985 
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

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

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

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

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

990 

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

991 
lemma Rats_divide [simp]: 
36409  992 
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

993 
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

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

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

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

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

998 

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

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

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

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

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

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

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

1006 

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

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

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

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

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

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

1012 
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

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

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

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

1016 

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

1017 
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

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

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

1020 

28001  1021 

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

1022 
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

1023 

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

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

1025 

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

1026 
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

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

1028 

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

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

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

1031 
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

1032 

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

1033 

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

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

1035 

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

1036 
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

1037 

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

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

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

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

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

1042 

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

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

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

1045 
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

1046 

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

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

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

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

1050 

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

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

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

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

1054 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1068 

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

1069 

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

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

1071 

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

1072 
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

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

1074 
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

1075 

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

1076 
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

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

1078 
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

1079 

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

1080 
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

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

1082 
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

1083 
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

1084 

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

1085 
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

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

1087 
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

1088 

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

1089 
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

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

1091 
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

1092 
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

1093 

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

1094 
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

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

1096 
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

1097 
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

1098 

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

1099 
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

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

1101 
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

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

1103 
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

1104 
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

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

1106 

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

1107 
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

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

1109 
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

1110 
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

1111 

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

1112 
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

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

1114 
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

1115 

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

1116 
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

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

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

1119 
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

1120 
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

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

1122 

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

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

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

1125 
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

1126 

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

1127 
instantiation rat :: equal 
26513  1128 
begin 
1129 

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

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

1131 
"HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b" 
26513  1132 

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

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

1134 
qed (simp add: equal_rat_def quotient_of_inject_eq) 
26513  1135 

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

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

1138 
by (rule equal_refl) 
28351  1139 

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

1141 

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

1142 
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

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

1145 

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

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

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

1149 

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

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

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

1152 
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

1153 

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

1154 

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

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

1156 

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

1157 
definition (in term_syntax) 
32657  1158 
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 
1159 
[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

1160 

37751  1161 
notation fcomp (infixl "\<circ>>" 60) 
1162 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1163 

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

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

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

1166 

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

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

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

1171 

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

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

1173 

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

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

1175 

37751  1176 
no_notation fcomp (infixl "\<circ>>" 60) 
1177 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

1178 

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

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

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

1181 

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

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

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

1184 

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

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

1186 

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

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

1188 

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

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

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

1191 

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

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

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

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

1195 
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

1196 

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

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

1198 

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

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

1200 

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

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

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

1203 

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

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

1205 

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

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

1207 

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

1208 
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

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

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

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

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

1213 
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

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

1215 

43887  1216 
instantiation rat :: narrowing 
1217 
begin 

1218 

1219 
definition 

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

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

1221 
(Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing" 
43887  1222 

1223 
instance .. 

1224 

1225 
end 

1226 

1227 

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

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

1229 

38287  1230 
declaration {* 
1231 
Nitpick_HOL.register_frac_type @{type_name rat} 

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

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

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

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

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

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

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

1242 

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

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

1244 
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

1245 
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

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

1247 

35343  1248 
subsection{* Float syntax *} 
1249 

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

1251 

1252 
use "Tools/float_syntax.ML" 

1253 
setup Float_Syntax.setup 

1254 

1255 
text{* Test: *} 

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

1257 
by simp 

1258 

37143  1259 

1260 
hide_const (open) normalize 

1261 

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

1262 
end 