author  haftmann 
Wed, 24 Feb 2010 14:19:53 +0100  
changeset 35369  e4a7947e02b8 
parent 35293  06a98796453e 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

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

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

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

4 

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

6 

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

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

10 

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

12 

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

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

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

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

18 

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

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

22 

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

18913  25 

26 
lemma sym_ratrel: "sym ratrel" 

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

28 

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

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

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

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

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

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

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

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

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

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

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

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

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

43 
qed 
27551  44 

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

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

47 

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

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

50 

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

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

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

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

55 

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

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

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

60 
qed 

61 

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

63 
by (simp add: Rat_def quotientI) 

64 

65 
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] 

66 

67 

68 
subsubsection {* Representation and basic operations *} 

69 

70 
definition 

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

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

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

74 
lemma eq_rat: 

75 
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

76 
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

77 
and "\<And>a c. Fract 0 a = Fract 0 c" 
27551  78 
by (simp_all add: Fract_def) 
79 

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

80 
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

81 
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

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

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

84 
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

85 
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

86 
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

87 
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

88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
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

95 
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

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

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

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

99 
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

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

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

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

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

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

105 
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

106 
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

107 
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

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

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

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

111 

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

112 
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

113 
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

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

115 
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

116 

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

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

119 

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

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

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

122 

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

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

124 
One_rat_def: "1 = Fract 1 1" 
18913  125 

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

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

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

130 

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

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

134 
proof  

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

136 
respects2 ratrel" 

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

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

139 
qed 

18913  140 

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

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

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

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

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

148 
by (simp add: congruent_def) 

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

150 
qed 

151 

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

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

154 

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

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

156 
diff_rat_def: "q  r = q +  (r::rat)" 
18913  157 

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

158 
lemma diff_rat [simp]: 
27551  159 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
160 
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

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

162 

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

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

164 
mult_rat_def: 
27551  165 
"q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
166 
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

167 

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

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

171 
by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all 

172 
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

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

174 

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

175 
lemma mult_rat_cancel: 
27551  176 
assumes "c \<noteq> 0" 
177 
shows "Fract (c * a) (c * b) = Fract a b" 

178 
proof  

179 
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

180 
then show ?thesis by (simp add: mult_rat [symmetric]) 
27551  181 
qed 
27509  182 

183 
instance proof 

27668  184 
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

185 
by (cases q, cases r, cases s) (simp add: eq_rat) 
27551  186 
next 
187 
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

188 
by (cases q, cases r) (simp add: eq_rat) 
27551  189 
next 
190 
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

191 
by (cases q) (simp add: One_rat_def eq_rat) 
27551  192 
next 
193 
fix q r s :: rat show "(q + r) + s = q + (r + s)" 

29667  194 
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) 
27551  195 
next 
196 
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

197 
by (cases q, cases r) (simp add: eq_rat) 
27551  198 
next 
199 
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

200 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  201 
next 
202 
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

203 
by (cases q) (simp add: Zero_rat_def eq_rat) 
27551  204 
next 
205 
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

206 
by (cases q, cases r) (simp add: eq_rat) 
27551  207 
next 
208 
fix q r s :: rat show "(q + r) * s = q * s + r * s" 

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

27509  212 
qed 
213 

214 
end 

215 

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

217 
by (induct k) (simp_all add: Zero_rat_def One_rat_def) 
27551  218 

219 
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

220 
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) 
27551  221 

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

223 
by (rule of_nat_rat [symmetric]) 

224 

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

226 
by (rule of_int_rat [symmetric]) 

227 

228 
instantiation rat :: number_ring 

229 
begin 

230 

231 
definition 

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

232 
rat_number_of_def: "number_of w = Fract w 1" 
27551  233 

30960  234 
instance proof 
235 
qed (simp add: rat_number_of_def of_int_rat) 

27551  236 

237 
end 

238 

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

239 
lemma rat_number_collapse: 
27551  240 
"Fract 0 k = 0" 
241 
"Fract 1 1 = 1" 

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

243 
"Fract k 0 = 0" 

244 
by (cases "k = 0") 

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

246 

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

247 
lemma rat_number_expand [code_unfold]: 
27551  248 
"0 = Fract 0 1" 
249 
"1 = Fract 1 1" 

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

251 
by (simp_all add: rat_number_collapse) 

252 

253 
lemma iszero_rat [simp]: 

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

255 
by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) 

256 

257 
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

258 
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" 
27551  259 
assumes 0: "q = 0 \<Longrightarrow> C" 
260 
shows C 

261 
proof (cases "q = 0") 

262 
case True then show C using 0 by auto 

263 
next 

264 
case False 

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

265 
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto 
27551  266 
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

267 
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

268 
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast 
27551  269 
qed 
270 

33805  271 
subsubsection {* Function @{text normalize} *} 
272 

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

273 
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

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

275 
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

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

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

278 
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

279 
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

280 
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

281 
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

282 
qed 
33805  283 

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

284 
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

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

286 
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

287 
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

288 

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

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

290 
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

291 
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

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

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

294 
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

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

296 
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

297 
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

298 
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

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

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

301 
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) 
33805  302 
qed 
303 

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

304 
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

305 
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

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

307 

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

308 
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

309 
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

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

311 

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

312 
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

313 
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

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

315 

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

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

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

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

319 

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

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

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

322 
by (simp add: normalize_def) 
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 
lemma normalize_negative [simp]: 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

326 
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

327 

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

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

329 
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

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

331 

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

332 
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

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

334 
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

335 

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

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

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

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

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

340 
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

341 
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

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

343 
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

344 
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

345 
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

346 
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

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

348 
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

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

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

351 
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

352 
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

353 
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

354 
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

355 
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

356 
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

357 
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

358 
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

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

361 
with p show "p = (a, b)" by simp 
33805  362 
qed 
363 
qed 

364 

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

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

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

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

368 
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

369 
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

370 
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

371 
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

372 
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

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

374 
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

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

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

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

378 
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

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

380 

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

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

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

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

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

385 
by (simp_all add: rat_number_expand quotient_of_Fract) 
33805  386 

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

387 
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

388 
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

389 

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

390 
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

391 
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

392 

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

393 
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

394 
by (cases r) (simp add: quotient_of_Fract normalize_coprime) 
33805  395 

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

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

397 
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

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

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

400 
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

401 
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

402 
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

403 
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

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

405 

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

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

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

408 
by (auto simp add: quotient_of_inject) 
33805  409 

27551  410 

411 
subsubsection {* The field of rational numbers *} 

412 

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

414 
begin 

415 

416 
definition 

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

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

420 

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

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

424 
by (auto simp add: congruent_def mult_commute) 

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

27509  426 
qed 
427 

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

429 
divide_rat_def: "q / r = q * inverse (r::rat)" 
27551  430 

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

431 
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

432 
by (simp add: divide_rat_def) 
27551  433 

434 
instance proof 

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

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

438 
fix q :: rat 

439 
assume "q \<noteq> 0" 

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

35216  441 
(simp_all add: rat_number_expand eq_rat) 
27551  442 
next 
443 
fix q r :: rat 

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

445 
qed 

446 

447 
end 

448 

449 

450 
subsubsection {* Various *} 

451 

452 
lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1" 

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

453 
by (simp add: rat_number_expand) 
27551  454 

455 
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

456 
by (simp add: Fract_of_int_eq [symmetric]) 
27551  457 

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

458 
lemma Fract_number_of_quotient: 
27551  459 
"Fract (number_of k) (number_of l) = number_of k / number_of l" 
460 
unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. 

461 

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

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

463 
"Fract 1 (number_of k) = 1 / number_of k" 
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset

464 
unfolding Fract_of_int_quotient number_of_eq by simp 
27551  465 

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

27509  467 

468 
instantiation rat :: linorder 

469 
begin 

470 

471 
definition 

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

472 
le_rat_def: 
27509  473 
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. 
27551  474 
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})" 
475 

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

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

479 
proof  

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

481 
respects2 ratrel" 

482 
proof (clarsimp simp add: congruent2_def) 

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

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

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

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

487 

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

489 
{ 

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

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

492 
proof  

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

494 
hence "?le a b c d = 

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

496 
by (simp add: mult_le_cancel_right) 

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

498 
by (simp add: mult_ac) 

499 
finally show ?thesis . 

500 
qed 

501 
} note le_factor = this 

502 

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

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

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

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

507 
by (rule le_factor) 

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

511 
by (simp only: eq1 eq2) 

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

513 
by (simp add: mult_ac) 

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

515 
by (rule le_factor [symmetric]) 

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

517 
qed 

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

519 
qed 

27509  520 

521 
definition 

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

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

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

524 
lemma less_rat [simp]: 
27551  525 
assumes "b \<noteq> 0" and "d \<noteq> 0" 
526 
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

527 
using assms by (simp add: less_rat_def eq_rat order_less_le) 
27509  528 

529 
instance proof 

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

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

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

532 
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

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

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

535 
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

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

537 
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

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

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

540 
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

541 
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

542 
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

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

544 
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

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

546 
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

547 
qed 
27668  548 
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

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

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

551 
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

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

553 
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

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

555 
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

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

557 
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

558 
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

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

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

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

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

563 
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

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

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

566 
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

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

568 
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

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

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

571 
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

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

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

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

575 
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

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

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

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

579 
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

580 
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

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

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

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

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

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

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

587 
by (induct q) simp 
27682  588 
show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" 
589 
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

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

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

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

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

595 

27509  596 
end 
597 

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

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

600 

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

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

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

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

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

607 
definition 

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

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

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

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

612 
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) 
27551  613 
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) 
614 

615 
definition 

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

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

617 

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

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

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

620 

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

22456  623 

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

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

625 

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

626 
instance rat :: linordered_field 
27551  627 
proof 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset

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

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

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

631 
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

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

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

634 
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

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

636 
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

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

638 
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

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

640 
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

641 
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

642 
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

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

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

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

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

647 
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

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

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

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

651 
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

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

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

654 
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

655 
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

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

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

658 
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

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

660 
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

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

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

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

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

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

667 

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

670 
shows "P q" 

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

671 
proof (cases q) 
27551  672 
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

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

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

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

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

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

678 
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

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

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

681 
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

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

683 

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

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

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

686 
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

687 

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

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

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

690 
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

691 

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

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

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

694 
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

695 

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

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

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

698 
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

699 

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

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

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

702 
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

703 

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

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

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

706 
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

707 

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

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

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

710 
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

711 

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

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

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

714 
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

715 

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

716 

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

717 
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

718 

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

719 
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

720 
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

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

722 
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

723 
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

724 
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

725 
unfolding Fract_of_int_quotient 
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

726 
by (rule linorder_cases [of b 0]) 
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset

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

728 
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

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

730 

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

731 
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

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

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

734 
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

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

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

737 
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

738 
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

739 
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

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

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

742 

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

743 
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

744 
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

745 
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

746 

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

747 

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

749 

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

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

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

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

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

756 
@{thm True_implies_equals}, 

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

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 

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

779 
"of_rat q = contents (\<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" 
23342  785 
apply (rule congruent.intro) 
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: 

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

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: 

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

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 

881 
lemma of_rat_number_of_eq [simp]: 

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

883 
by (simp add: number_of_eq) 

884 

23879  885 
lemmas zero_rat = Zero_rat_def 
886 
lemmas one_rat = One_rat_def 

887 

24198  888 
abbreviation 
889 
rat_of_nat :: "nat \<Rightarrow> rat" 

890 
where 

891 
"rat_of_nat \<equiv> of_nat" 

892 

893 
abbreviation 

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

895 
where 

896 
"rat_of_int \<equiv> of_int" 

897 

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

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

899 

28001  900 
context field_char_0 
901 
begin 

902 

903 
definition 

904 
Rats :: "'a set" where 

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

905 
"Rats = range of_rat" 
28001  906 

907 
notation (xsymbols) 

908 
Rats ("\<rat>") 

909 

910 
end 

911 

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

912 
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

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

914 

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

915 
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

916 
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

917 

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

918 
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

919 
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

920 

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

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

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

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

924 

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

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

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

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

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

929 
done 
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_1 [simp]: "1 \<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_1 [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_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

938 
apply (auto simp add: 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_add [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_minus [simp]: "a \<in> Rats \<Longrightarrow>  a \<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_minus [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_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

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_diff [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_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

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_mult [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 nonzero_Rats_inverse: 
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset

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

963 
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

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

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

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

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

968 

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

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

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

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

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

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

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

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

976 

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

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

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

979 
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

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

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

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

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

984 

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

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

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

987 
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

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

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

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

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

992 

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

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

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

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

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

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

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

1000 

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

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

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

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

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

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

1006 
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

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

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

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

1010 

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

1011 
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

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

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

1014 

28001  1015 

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

1016 
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

1017 

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

1018 
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

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

1020 

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

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

1022 
proof (rule eq_reflection) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1023 
show "Frct (quotient_of x) = x" by (cases x) (auto intro: quotient_of_eq) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

1025 

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

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

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

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

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

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

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

1032 
"Frct (number_of k, number_of l) = number_of k / number_of l" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1033 
by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of) 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

1034 

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

1035 
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

1036 

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

1037 
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

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

1039 
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

1040 

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

1041 
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

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

1043 
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

1044 

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

1045 
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

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

1047 
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

1048 
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

1049 

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

1050 
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

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

1052 
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

1053 

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

1054 
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

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

1056 
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

1057 
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

1058 

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

1059 
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

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

1061 
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

1062 
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

1063 

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

1064 
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

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

1066 
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

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

1068 
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

1069 
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

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

1071 

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

1072 
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

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

1074 
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

1075 
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

1076 

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

1077 
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

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

1079 
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

1080 

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

1081 
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

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

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

1084 
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

1085 
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

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

1087 

26513  1088 
instantiation rat :: eq 
1089 
begin 

1090 

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

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

1092 
"eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b" 
26513  1093 

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

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

1095 
qed (simp add: eq_rat_def quotient_of_inject_eq) 
26513  1096 

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

1099 
by (rule HOL.eq_refl) 

1100 

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

1102 

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

1103 
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

1104 
"p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)" 
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset

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

1106 

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

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

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

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

1110 

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

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

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

1113 
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

1114 

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

1115 
definition (in term_syntax) 
32657  1116 
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 
1117 
[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

1118 

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

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

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

1121 

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

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

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

1124 

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

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

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

1129 

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

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

1131 

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

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

1133 

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

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

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

1136 

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

1138 

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

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

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

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

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

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

1146 
if q = 1 orelse p = 0 then HOLogic.mk_number rT p 
25885  1147 
else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $ 
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

1148 
HOLogic.mk_number rT p $ HOLogic.mk_number rT q 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

1165 

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

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

1168 

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

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

1170 
"of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") 
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset

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

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

1174 

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

1175 
setup {* 
33209  1176 
Nitpick.register_frac_type @{type_name rat} 
1177 
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), 

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

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

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

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

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

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

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

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

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

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

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

1188 

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

1189 
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat 
33209  1190 
number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat 
1191 
plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat 

1192 
zero_rat_inst.zero_rat 

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

1193 

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

1194 
end 