author  chaieb@chaieblaptop 
Fri, 06 Feb 2009 00:10:58 +0000  
changeset 29811  026b0f9f579f 
parent 29667  53103fc8ffa3 
child 32115  8f10fb3bb46e 
permissions  rwrr 
7219  1 
(* Title : PReal.thy 
5078  2 
Author : Jacques D. Fleuriot 
3 
Copyright : 1998 University of Cambridge 

4 
Description : The positive reals as Dedekind sections of positive 

14335  5 
rationals. Fundamentals of Abstract Analysis [Gleason p. 121] 
5078  6 
provides some of the definitions. 
7 
*) 

8 

17428  9 
header {* Positive real numbers *} 
10 

15131  11 
theory PReal 
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

12 
imports Rational 
15131  13 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

14 

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

15 
text{*Could be generalized and moved to @{text Ring_and_Field}*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

16 
lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

17 
by (rule_tac x="ba" in exI, simp) 
5078  18 

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

20 
cut :: "rat set => bool" where 
28562  21 
[code del]: "cut A = ({} \<subset> A & 
19765  22 
A < {r. 0 < r} & 
23 
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y > z \<in> A) & (\<exists>u \<in> A. y < u))))" 

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

24 

29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

25 
lemma interval_empty_iff: 
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

26 
"{y. (x::'a::dense_linear_order) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" 
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

27 
by (auto dest: dense) 
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

28 

026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29667
diff
changeset

29 

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

30 
lemma cut_of_rat: 
20495  31 
assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A") 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

33 
from q have pos: "?A < {r. 0 < r}" by force 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

34 
have nonempty: "{} \<subset> ?A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

36 
show "{} \<subseteq> ?A" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

37 
show "{} \<noteq> ?A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

38 
by (force simp only: q eq_commute [of "{}"] interval_empty_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

40 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

41 
by (simp add: cut_def pos nonempty, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

42 
blast dest: dense intro: order_less_trans) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

44 

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

45 

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

46 
typedef preal = "{A. cut A}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

47 
by (blast intro: cut_of_rat [OF zero_less_one]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

48 

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

50 
preal_of_rat :: "rat => preal" where 
20495  51 
"preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}" 
5078  52 

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

53 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20495
diff
changeset

54 
psup :: "preal set => preal" where 
20495  55 
"psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

56 

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

57 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20495
diff
changeset

58 
add_set :: "[rat set,rat set] => rat set" where 
19765  59 
"add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

60 

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

61 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20495
diff
changeset

62 
diff_set :: "[rat set,rat set] => rat set" where 
28562  63 
[code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

64 

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

65 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20495
diff
changeset

66 
mult_set :: "[rat set,rat set] => rat set" where 
19765  67 
"mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

68 

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

69 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20495
diff
changeset

70 
inverse_set :: "rat set => rat set" where 
28562  71 
[code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

72 

26511  73 
instantiation preal :: "{ord, plus, minus, times, inverse, one}" 
74 
begin 

5078  75 

26511  76 
definition 
28562  77 
preal_less_def [code del]: 
20495  78 
"R < S == Rep_preal R < Rep_preal S" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

79 

26511  80 
definition 
28562  81 
preal_le_def [code del]: 
20495  82 
"R \<le> S == Rep_preal R \<subseteq> Rep_preal S" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

83 

26511  84 
definition 
14335  85 
preal_add_def: 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

86 
"R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

87 

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

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

90 
"R  S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))" 
5078  91 

26511  92 
definition 
14335  93 
preal_mult_def: 
20495  94 
"R * S == Abs_preal (mult_set (Rep_preal R) (Rep_preal S))" 
5078  95 

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

97 
preal_inverse_def: 
20495  98 
"inverse R == Abs_preal (inverse_set (Rep_preal R))" 
14335  99 

26564  100 
definition "R / S = R * inverse (S\<Colon>preal)" 
101 

26511  102 
definition 
23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

103 
preal_one_def: 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

104 
"1 == preal_of_rat 1" 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

105 

26511  106 
instance .. 
107 

108 
end 

109 

14335  110 

15413  111 
text{*Reduces equality on abstractions to equality on representatives*} 
112 
declare Abs_preal_inject [simp] 

20495  113 
declare Abs_preal_inverse [simp] 
114 

115 
lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal" 

116 
by (simp add: preal_def cut_of_rat) 

14335  117 

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

118 
lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

119 
by (unfold preal_def cut_def, blast) 
14335  120 

20495  121 
lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A" 
122 
by (drule preal_nonempty, fast) 

123 

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

124 
lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

125 
by (force simp add: preal_def cut_def) 
14335  126 

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

127 
lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

128 
by (drule preal_imp_psubset_positives, auto) 
14335  129 

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

130 
lemma preal_exists_greater: "[ A \<in> preal; y \<in> A ] ==> \<exists>u \<in> A. y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

131 
by (unfold preal_def cut_def, blast) 
14335  132 

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

133 
lemma preal_downwards_closed: "[ A \<in> preal; y \<in> A; 0 < z; z < y ] ==> z \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

134 
by (unfold preal_def cut_def, blast) 
14335  135 

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

136 
text{*Relaxing the final premise*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

137 
lemma preal_downwards_closed': 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

138 
"[ A \<in> preal; y \<in> A; 0 < z; z \<le> y ] ==> z \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

139 
apply (simp add: order_le_less) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

140 
apply (blast intro: preal_downwards_closed) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

141 
done 
14335  142 

143 
text{*A positive fraction not in a positive real is an upper bound. 

144 
Gleason p. 122  Remark (1)*} 

145 

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

146 
lemma not_in_preal_ub: 
19765  147 
assumes A: "A \<in> preal" 
148 
and notx: "x \<notin> A" 

149 
and y: "y \<in> A" 

150 
and pos: "0 < x" 

151 
shows "y < x" 

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

152 
proof (cases rule: linorder_cases) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

153 
assume "x<y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

154 
with notx show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

155 
by (simp add: preal_downwards_closed [OF A y] pos) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

157 
assume "x=y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

158 
with notx and y show ?thesis by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

160 
assume "y<x" 
20495  161 
thus ?thesis . 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

163 

20495  164 
text {* preal lemmas instantiated to @{term "Rep_preal X"} *} 
165 

166 
lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X" 

167 
by (rule preal_Ex_mem [OF Rep_preal]) 

168 

169 
lemma Rep_preal_exists_bound: "\<exists>x>0. x \<notin> Rep_preal X" 

170 
by (rule preal_exists_bound [OF Rep_preal]) 

171 

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

172 
lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal] 
14335  173 

174 

20495  175 

176 
subsection{*@{term preal_of_prat}: the Injection from prat to preal*} 

177 

178 
lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal" 

179 
by (simp add: preal_def cut_of_rat) 

180 

181 
lemma rat_subset_imp_le: 

182 
"[{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x] ==> x \<le> y" 

183 
apply (simp add: linorder_not_less [symmetric]) 

184 
apply (blast dest: dense intro: order_less_trans) 

185 
done 

186 

187 
lemma rat_set_eq_imp_eq: 

188 
"[{u::rat. 0 < u & u < x} = {u. 0 < u & u < y}; 

189 
0 < x; 0 < y] ==> x = y" 

190 
by (blast intro: rat_subset_imp_le order_antisym) 

191 

192 

193 

194 
subsection{*Properties of Ordering*} 

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

195 

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

196 
instance preal :: order 
27682  197 
proof 
198 
fix w :: preal 

199 
show "w \<le> w" by (simp add: preal_le_def) 

200 
next 

201 
fix i j k :: preal 

202 
assume "i \<le> j" and "j \<le> k" 

203 
then show "i \<le> k" by (simp add: preal_le_def) 

204 
next 

205 
fix z w :: preal 

206 
assume "z \<le> w" and "w \<le> z" 

207 
then show "z = w" by (simp add: preal_le_def Rep_preal_inject) 

208 
next 

209 
fix z w :: preal 

210 
show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" 

211 
by (auto simp add: preal_le_def preal_less_def Rep_preal_inject) 

212 
qed 

14335  213 

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

214 
lemma preal_imp_pos: "[A \<in> preal; r \<in> A] ==> 0 < r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

215 
by (insert preal_imp_psubset_positives, blast) 
14335  216 

27682  217 
instance preal :: linorder 
218 
proof 

219 
fix x y :: preal 

220 
show "x <= y  y <= x" 

221 
apply (auto simp add: preal_le_def) 

222 
apply (rule ccontr) 

223 
apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal] 

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

224 
elim: order_less_asym) 
27682  225 
done 
226 
qed 

14335  227 

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

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

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

230 

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

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

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

233 

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

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

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

236 

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

237 
instance 
22483  238 
by intro_classes 
239 
(auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1) 

14335  240 

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

241 
end 
14335  242 

243 
subsection{*Properties of Addition*} 

244 

245 
lemma preal_add_commute: "(x::preal) + y = y + x" 

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

246 
apply (unfold preal_add_def add_set_def) 
14335  247 
apply (rule_tac f = Abs_preal in arg_cong) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

248 
apply (force simp add: add_commute) 
14335  249 
done 
250 

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

251 
text{*Lemmas for proving that addition of two positive reals gives 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

252 
a positive real*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

253 

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

254 
lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

256 

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

257 
text{*Part 1 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

259 
"[A \<in> preal; B \<in> preal] ==> {} \<subset> add_set A B" 
20495  260 
apply (drule preal_nonempty)+ 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

261 
apply (auto simp add: add_set_def) 
14335  262 
done 
263 

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

264 
text{*Part 2 of Dedekind sections definition. A structured version of 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

265 
this proof is @{text preal_not_mem_mult_set_Ex} below.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

266 
lemma preal_not_mem_add_set_Ex: 
20495  267 
"[A \<in> preal; B \<in> preal] ==> \<exists>q>0. q \<notin> add_set A B" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

268 
apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

269 
apply (rule_tac x = "x+xa" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

270 
apply (simp add: add_set_def, clarify) 
20495  271 
apply (drule (3) not_in_preal_ub)+ 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

272 
apply (force dest: add_strict_mono) 
14335  273 
done 
274 

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

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

276 
assumes A: "A \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

277 
and B: "B \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

278 
shows "add_set A B < {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

280 
from preal_imp_pos [OF A] preal_imp_pos [OF B] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

281 
show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

283 
show "add_set A B \<noteq> {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

284 
by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

286 

14335  287 
text{*Part 3 of Dedekind sections definition*} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

289 
"[A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

290 
==> z \<in> add_set A B" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

291 
proof (unfold add_set_def, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

292 
fix x::rat and y::rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

293 
assume A: "A \<in> preal" 
19765  294 
and B: "B \<in> preal" 
295 
and [simp]: "0 < z" 

296 
and zless: "z < x + y" 

297 
and x: "x \<in> A" 

298 
and y: "y \<in> B" 

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

299 
have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

300 
have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

301 
have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

302 
let ?f = "z/(x+y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

303 
have fless: "?f < 1" by (simp add: zless pos_divide_less_eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

304 
show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'" 
20495  305 
proof (intro bexI) 
306 
show "z = x*?f + y*?f" 

307 
by (simp add: left_distrib [symmetric] divide_inverse mult_ac 

308 
order_less_imp_not_eq2) 

309 
next 

310 
show "y * ?f \<in> B" 

311 
proof (rule preal_downwards_closed [OF B y]) 

312 
show "0 < y * ?f" 

313 
by (simp add: divide_inverse zero_less_mult_iff) 

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

314 
next 
20495  315 
show "y * ?f < y" 
316 
by (insert mult_strict_left_mono [OF fless ypos], simp) 

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

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

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

319 
show "x * ?f \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

320 
proof (rule preal_downwards_closed [OF A x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

321 
show "0 < x * ?f" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

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

324 
show "x * ?f < x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

325 
by (insert mult_strict_left_mono [OF fless xpos], simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

329 

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

330 
text{*Part 4 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

332 
"[A \<in> preal; B \<in> preal; y \<in> add_set A B] ==> \<exists>u \<in> add_set A B. y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

334 
apply (frule preal_exists_greater [of A], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

335 
apply (rule_tac x="u + y" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

336 
apply (auto intro: add_strict_left_mono) 
14335  337 
done 
338 

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

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

340 
"[A \<in> preal; B \<in> preal] ==> add_set A B \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

341 
apply (simp (no_asm_simp) add: preal_def cut_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

342 
apply (blast intro!: add_set_not_empty add_set_not_rat_set 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

343 
add_set_lemma3 add_set_lemma4) 
14335  344 
done 
345 

346 
lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)" 

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

347 
apply (simp add: preal_add_def mem_add_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

348 
apply (force simp add: add_set_def add_ac) 
14335  349 
done 
350 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

351 
instance preal :: ab_semigroup_add 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

352 
proof 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

353 
fix a b c :: preal 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

354 
show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc) 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

355 
show "a + b = b + a" by (rule preal_add_commute) 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

356 
qed 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

357 

14335  358 
lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)" 
23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

359 
by (rule add_left_commute) 
14335  360 

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

361 
text{* Positive Real addition is an AC operator *} 
14335  362 
lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute 
363 

364 

365 
subsection{*Properties of Multiplication*} 

366 

367 
text{*Proofs essentially same as for addition*} 

368 

369 
lemma preal_mult_commute: "(x::preal) * y = y * x" 

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

370 
apply (unfold preal_mult_def mult_set_def) 
14335  371 
apply (rule_tac f = Abs_preal in arg_cong) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

372 
apply (force simp add: mult_commute) 
14335  373 
done 
374 

15055  375 
text{*Multiplication of two positive reals gives a positive real.*} 
14335  376 

377 
text{*Lemmas for proving positive reals multiplication set in @{typ preal}*} 

378 

379 
text{*Part 1 of Dedekind sections definition*} 

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

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

381 
"[A \<in> preal; B \<in> preal] ==> {} \<subset> mult_set A B" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

382 
apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

383 
apply (auto simp add: mult_set_def) 
14335  384 
done 
385 

386 
text{*Part 2 of Dedekind sections definition*} 

387 
lemma preal_not_mem_mult_set_Ex: 

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

388 
assumes A: "A \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

389 
and B: "B \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

390 
shows "\<exists>q. 0 < q & q \<notin> mult_set A B" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

392 
from preal_exists_bound [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

393 
obtain x where [simp]: "0 < x" "x \<notin> A" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

394 
from preal_exists_bound [OF B] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

395 
obtain y where [simp]: "0 < y" "y \<notin> B" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

396 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

397 
proof (intro exI conjI) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15413
diff
changeset

398 
show "0 < x*y" by (simp add: mult_pos_pos) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

399 
show "x * y \<notin> mult_set A B" 
14377  400 
proof  
401 
{ fix u::rat and v::rat 

14550  402 
assume "u \<in> A" and "v \<in> B" and "x*y = u*v" 
403 
moreover 

404 
with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+ 

405 
moreover 

406 
with prems have "0\<le>v" 

407 
by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems) 

408 
moreover 

409 
from calculation 

410 
have "u*v < x*y" by (blast intro: mult_strict_mono prems) 

411 
ultimately have False by force } 

14377  412 
thus ?thesis by (auto simp add: mult_set_def) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

415 
qed 
14335  416 

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

417 
lemma mult_set_not_rat_set: 
19765  418 
assumes A: "A \<in> preal" 
419 
and B: "B \<in> preal" 

420 
shows "mult_set A B < {r. 0 < r}" 

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

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

422 
show "mult_set A B \<subseteq> {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

423 
by (force simp add: mult_set_def 
19765  424 
intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

425 
show "mult_set A B \<noteq> {r. 0 < r}" 
19765  426 
using preal_not_mem_mult_set_Ex [OF A B] by blast 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

428 

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

429 

14335  430 

431 
text{*Part 3 of Dedekind sections definition*} 

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

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

433 
"[A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

434 
==> z \<in> mult_set A B" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

435 
proof (unfold mult_set_def, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

436 
fix x::rat and y::rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

437 
assume A: "A \<in> preal" 
19765  438 
and B: "B \<in> preal" 
439 
and [simp]: "0 < z" 

440 
and zless: "z < x * y" 

441 
and x: "x \<in> A" 

442 
and y: "y \<in> B" 

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

443 
have [simp]: "0<y" by (rule preal_imp_pos [OF B y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

444 
show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

446 
show "\<exists>y'\<in>B. z = (z/y) * y'" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

448 
show "z = (z/y)*y" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

449 
by (simp add: divide_inverse mult_commute [of y] mult_assoc 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

450 
order_less_imp_not_eq2) 
23389  451 
show "y \<in> B" by fact 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

454 
show "z/y \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

455 
proof (rule preal_downwards_closed [OF A x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

456 
show "0 < z/y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

458 
show "z/y < x" by (simp add: pos_divide_less_eq zless) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

462 

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

463 
text{*Part 4 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

465 
"[A \<in> preal; B \<in> preal; y \<in> mult_set A B] ==> \<exists>u \<in> mult_set A B. y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

467 
apply (frule preal_exists_greater [of A], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

468 
apply (rule_tac x="u * y" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

469 
apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

470 
mult_strict_right_mono) 
14335  471 
done 
472 

473 

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

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

475 
"[A \<in> preal; B \<in> preal] ==> mult_set A B \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

476 
apply (simp (no_asm_simp) add: preal_def cut_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

477 
apply (blast intro!: mult_set_not_empty mult_set_not_rat_set 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

478 
mult_set_lemma3 mult_set_lemma4) 
14335  479 
done 
480 

481 
lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)" 

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

482 
apply (simp add: preal_mult_def mem_mult_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

483 
apply (force simp add: mult_set_def mult_ac) 
14335  484 
done 
485 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

486 
instance preal :: ab_semigroup_mult 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

487 
proof 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

488 
fix a b c :: preal 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

489 
show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc) 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

490 
show "a * b = b * a" by (rule preal_mult_commute) 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

491 
qed 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

492 

14335  493 
lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)" 
23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

494 
by (rule mult_left_commute) 
14335  495 

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

496 

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

497 
text{* Positive Real multiplication is an AC operator *} 
14335  498 
lemmas preal_mult_ac = 
499 
preal_mult_assoc preal_mult_commute preal_mult_left_commute 

500 

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

501 

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

502 
text{* Positive real 1 is the multiplicative identity element *} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

503 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

504 
lemma preal_mult_1: "(1::preal) * z = z" 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

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

506 
proof (induct z) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

507 
fix A :: "rat set" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

508 
assume A: "A \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

509 
have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

511 
show "?lhs \<subseteq> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

513 
fix x::rat and u::rat and v::rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

514 
assume upos: "0<u" and "u<1" and v: "v \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

515 
have vpos: "0<v" by (rule preal_imp_pos [OF A v]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

516 
hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

517 
thus "u * v \<in> A" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15413
diff
changeset

518 
by (force intro: preal_downwards_closed [OF A v] mult_pos_pos 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15413
diff
changeset

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

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

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

522 
show "A \<subseteq> ?lhs" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

524 
fix x::rat 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

525 
assume x: "x \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

526 
have xpos: "0<x" by (rule preal_imp_pos [OF A x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

527 
from preal_exists_greater [OF A x] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

528 
obtain v where v: "v \<in> A" and xlessv: "x < v" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

529 
have vpos: "0<v" by (rule preal_imp_pos [OF A v]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

530 
show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

531 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

532 
show "0 < x/v" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

533 
by (simp add: zero_less_divide_iff xpos vpos) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

534 
show "x / v < 1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

535 
by (simp add: pos_divide_less_eq vpos xlessv) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

536 
show "\<exists>v'\<in>A. x = (x / v) * v'" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

538 
show "x = (x/v)*v" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

539 
by (simp add: divide_inverse mult_assoc vpos 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

540 
order_less_imp_not_eq2) 
23389  541 
show "v \<in> A" by fact 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

546 
thus "preal_of_rat 1 * Abs_preal A = Abs_preal A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

547 
by (simp add: preal_of_rat_def preal_mult_def mult_set_def 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

550 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

551 
instance preal :: comm_monoid_mult 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

552 
by intro_classes (rule preal_mult_1) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

553 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

554 
lemma preal_mult_1_right: "z * (1::preal) = z" 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

555 
by (rule mult_1_right) 
14335  556 

557 

558 
subsection{*Distribution of Multiplication across Addition*} 

559 

560 
lemma mem_Rep_preal_add_iff: 

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

561 
"(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

562 
apply (simp add: preal_add_def mem_add_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

563 
apply (simp add: add_set_def) 
14335  564 
done 
565 

566 
lemma mem_Rep_preal_mult_iff: 

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

567 
"(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

568 
apply (simp add: preal_mult_def mem_mult_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

569 
apply (simp add: mult_set_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

570 
done 
14335  571 

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

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

573 
"Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

574 
apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

575 
apply (force simp add: right_distrib) 
14335  576 
done 
577 

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

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

579 
assumes a: "a \<in> Rep_preal w" 
19765  580 
and b: "b \<in> Rep_preal w" 
581 
and d: "d \<in> Rep_preal x" 

582 
and e: "e \<in> Rep_preal y" 

583 
shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)" 

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

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

585 
let ?c = "(a*d + b*e)/(d+e)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

586 
have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

587 
by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

588 
have cpos: "0 < ?c" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

590 
show "a * d + b * e = ?c * (d + e)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

591 
by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

592 
show "?c \<in> Rep_preal w" 
20495  593 
proof (cases rule: linorder_le_cases) 
594 
assume "a \<le> b" 

595 
hence "?c \<le> b" 

596 
by (simp add: pos_divide_le_eq right_distrib mult_right_mono 

597 
order_less_imp_le) 

598 
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos]) 

599 
next 

600 
assume "b \<le> a" 

601 
hence "?c \<le> a" 

602 
by (simp add: pos_divide_le_eq right_distrib mult_right_mono 

603 
order_less_imp_le) 

604 
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos]) 

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

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

607 

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

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

609 
"Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

610 
apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

611 
apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto) 
14335  612 
done 
613 

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

614 
lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)" 
15413  615 
apply (rule Rep_preal_inject [THEN iffD1]) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

616 
apply (rule equalityI [OF distrib_subset1 distrib_subset2]) 
14335  617 
done 
618 

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

619 
lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

620 
by (simp add: preal_mult_commute preal_add_mult_distrib2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

621 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

622 
instance preal :: comm_semiring 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

623 
by intro_classes (rule preal_add_mult_distrib) 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

624 

14335  625 

626 
subsection{*Existence of Inverse, a Positive Real*} 

627 

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

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

629 
assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

631 
from preal_exists_bound [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

632 
obtain x where [simp]: "0<x" "x \<notin> A" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

633 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

634 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

635 
show "0 < inverse (x+1)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

636 
by (simp add: order_less_trans [OF _ less_add_one]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

637 
show "inverse(x+1) < inverse x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

638 
by (simp add: less_imp_inverse_less less_add_one) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

639 
show "inverse (inverse x) \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

642 
qed 
14335  643 

644 
text{*Part 1 of Dedekind sections definition*} 

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

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

646 
"A \<in> preal ==> {} \<subset> inverse_set A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

647 
apply (insert mem_inv_set_ex [of A]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

648 
apply (auto simp add: inverse_set_def) 
14335  649 
done 
650 

651 
text{*Part 2 of Dedekind sections definition*} 

652 

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

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

654 
assumes A: "A \<in> preal" shows "\<exists>q. 0 < q & q \<notin> inverse_set A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

656 
from preal_nonempty [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

657 
obtain x where x: "x \<in> A" and xpos [simp]: "0<x" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

658 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

659 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

660 
show "0 < inverse x" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

661 
show "inverse x \<notin> inverse_set A" 
14377  662 
proof  
663 
{ fix y::rat 

664 
assume ygt: "inverse x < y" 

665 
have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt]) 

666 
have iyless: "inverse y < x" 

667 
by (simp add: inverse_less_imp_less [of x] ygt) 

668 
have "inverse y \<in> A" 

669 
by (simp add: preal_downwards_closed [OF A x] iyless)} 

670 
thus ?thesis by (auto simp add: inverse_set_def) 

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

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

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

673 
qed 
14335  674 

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

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

676 
assumes A: "A \<in> preal" shows "inverse_set A < {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

678 
show "inverse_set A \<subseteq> {r. 0 < r}" by (force simp add: inverse_set_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

680 
show "inverse_set A \<noteq> {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

681 
by (insert preal_not_mem_inverse_set_Ex [OF A], blast) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

682 
qed 
14335  683 

684 
text{*Part 3 of Dedekind sections definition*} 

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

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

686 
"[A \<in> preal; u \<in> inverse_set A; 0 < z; z < u] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

687 
==> z \<in> inverse_set A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

689 
apply (auto intro: order_less_trans) 
14335  690 
done 
691 

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

692 
text{*Part 4 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

694 
"[A \<in> preal; y \<in> inverse_set A] ==> \<exists>u \<in> inverse_set A. y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

696 
apply (drule dense [of y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

697 
apply (blast intro: order_less_trans) 
14335  698 
done 
699 

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

700 

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

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

702 
"A \<in> preal ==> inverse_set A \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

703 
apply (simp (no_asm_simp) add: preal_def cut_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

704 
apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

705 
inverse_set_lemma3 inverse_set_lemma4) 
14335  706 
done 
707 

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

708 

14335  709 
subsection{*Gleason's Lemma 93.4, page 122*} 
710 

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

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

712 
assumes A: "A \<in> preal" 
19765  713 
and "\<forall>x\<in>A. x + u \<in> A" 
714 
and "0 \<le> z" 

715 
shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A" 

14369  716 
proof (cases z rule: int_cases) 
717 
case (nonneg n) 

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

718 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

719 
proof (simp add: prems, induct n) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

721 
from preal_nonempty [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

722 
show ?case by force 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

723 
case (Suc k) 
15013  724 
from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" .. 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

725 
hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems) 
29667  726 
thus ?case by (force simp add: algebra_simps prems) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

728 
next 
14369  729 
case (neg n) 
730 
with prems show ?thesis by simp 

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

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

732 

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

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

734 
assumes A: "A \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

735 
shows "[\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A] ==> False" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

736 
proof (induct u, induct y) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

738 
fix c::int and d::int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

739 
assume bpos [simp]: "0 < b" 
19765  740 
and dpos [simp]: "0 < d" 
741 
and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A" 

742 
and upos: "0 < Fract c d" 

743 
and ypos: "0 < Fract a b" 

744 
and notin: "Fract a b \<notin> A" 

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

745 
have cpos [simp]: "0 < c" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

746 
by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

747 
have apos [simp]: "0 < a" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

748 
by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

749 
let ?k = "a*d" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

750 
have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

752 
have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

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

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

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

756 
by (rule mult_mono, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

757 
simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

760 
show ?thesis by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

762 
have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

763 
from Gleason9_34_exists [OF A closed k] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

764 
obtain z where z: "z \<in> A" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

765 
and mem: "z + of_int ?k * Fract c d \<in> A" .. 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

766 
have less: "z + of_int ?k * Fract c d < Fract a b" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

767 
by (rule not_in_preal_ub [OF A notin mem ypos]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

768 
have "0<z" by (rule preal_imp_pos [OF A z]) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14377
diff
changeset

769 
with frle and less show False by (simp add: Fract_of_int_eq) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

770 
qed 
14335  771 

772 

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

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

774 
assumes A: "A \<in> preal" 
19765  775 
and upos: "0 < u" 
776 
shows "\<exists>r \<in> A. r + u \<notin> A" 

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

777 
proof (rule ccontr, simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

778 
assume closed: "\<forall>r\<in>A. r + u \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

779 
from preal_exists_bound [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

780 
obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

782 
by (rule Gleason9_34_contra [OF A closed upos ypos y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

784 

14335  785 

786 

787 
subsection{*Gleason's Lemma 93.6*} 

788 

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

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

790 
assumes A: "A \<in> preal" 
19765  791 
and x: "1 < x" 
792 
shows "\<exists>r \<in> A. r*x \<notin> A" 

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

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

794 
from preal_nonempty [OF A] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

795 
obtain y where y: "y \<in> A" and ypos: "0<y" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

796 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

797 
proof (rule classical) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

798 
assume "~(\<exists>r\<in>A. r * x \<notin> A)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

799 
with y have ymem: "y * x \<in> A" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

800 
from ypos mult_strict_left_mono [OF x] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

801 
have yless: "y < y*x" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

802 
let ?d = "y*x  y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

803 
from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

804 
from Gleason9_34 [OF A dpos] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

805 
obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

806 
have rpos: "0<r" by (rule preal_imp_pos [OF A r]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

807 
with dpos have rdpos: "0 < r + ?d" by arith 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

808 
have "~ (r + ?d \<le> y + ?d)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

810 
assume le: "r + ?d \<le> y + ?d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

811 
from ymem have yd: "y + ?d \<in> A" by (simp add: eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

812 
have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

813 
with notin show False by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

815 
hence "y < r" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

816 
with ypos have dless: "?d < (r * ?d)/y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

817 
by (simp add: pos_less_divide_eq mult_commute [of ?d] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

819 
have "r + ?d < r*x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

821 
have "r + ?d < r + (r * ?d)/y" by (simp add: dless) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

822 
also with ypos have "... = (r/y) * (y + ?d)" 
29667  823 
by (simp only: algebra_simps divide_inverse, simp) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

824 
also have "... = r*x" using ypos 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

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

826 
finally show "r + ?d < r*x" . 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

828 
with r notin rdpos 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

829 
show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest: preal_downwards_closed [OF A]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

831 
qed 
14335  832 

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

833 
subsection{*Existence of Inverse: Part 2*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

834 

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

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

836 
"(z \<in> Rep_preal(inverse R)) = 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

837 
(0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

838 
apply (simp add: preal_inverse_def mem_inverse_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

839 
apply (simp add: inverse_set_def) 
14335  840 
done 
841 

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

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

843 
"0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

844 
by (simp add: preal_of_rat_def rat_mem_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

845 

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

846 
lemma subset_inverse_mult_lemma: 
19765  847 
assumes xpos: "0 < x" and xless: "x < 1" 
848 
shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 

849 
u \<in> Rep_preal R & x = r * u" 

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

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

851 
from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

852 
from lemma_gleason9_36 [OF Rep_preal this] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

853 
obtain r where r: "r \<in> Rep_preal R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

854 
and notin: "r * (inverse x) \<notin> Rep_preal R" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

855 
have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

856 
from preal_exists_greater [OF Rep_preal r] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

857 
obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

858 
have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

859 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

860 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

861 
show "0 < x/u" using xpos upos 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

863 
show "x/u < x/r" using xpos upos rpos 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

864 
by (simp add: divide_inverse mult_less_cancel_left rless) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

865 
show "inverse (x / r) \<notin> Rep_preal R" using notin 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

867 
show "u \<in> Rep_preal R" by (rule u) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

868 
show "x = x / u * u" using upos 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

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

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

872 

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

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

874 
"Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

875 
apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

877 
apply (blast dest: subset_inverse_mult_lemma) 
14335  878 
done 
879 

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

880 
lemma inverse_mult_subset_lemma: 
19765  881 
assumes rpos: "0 < r" 
882 
and rless: "r < y" 

883 
and notin: "inverse y \<notin> Rep_preal R" 

884 
and q: "q \<in> Rep_preal R" 

885 
shows "r*q < 1" 

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

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

887 
have "q < inverse y" using rpos rless 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

888 
by (simp add: not_in_preal_ub [OF Rep_preal notin] q) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

889 
hence "r * q < r/y" using rpos 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

891 
also have "... \<le> 1" using rpos rless 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

893 
finally show ?thesis . 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

895 

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

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

897 
"Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

898 
apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

900 
apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

901 
apply (blast intro: inverse_mult_subset_lemma) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

903 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

904 
lemma preal_mult_inverse: "inverse R * R = (1::preal)" 
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

905 
unfolding preal_one_def 
15413  906 
apply (rule Rep_preal_inject [THEN iffD1]) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

907 
apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

909 

23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

910 
lemma preal_mult_inverse_right: "R * inverse R = (1::preal)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

911 
apply (rule preal_mult_commute [THEN subst]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

912 
apply (rule preal_mult_inverse) 
14335  913 
done 
914 

915 

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

916 
text{*Theorems needing @{text Gleason9_34}*} 
14335  917 

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

918 
lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

921 
assume r: "r \<in> Rep_preal R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

922 
have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

924 
obtain y where y: "y \<in> Rep_preal S" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

925 
have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

926 
have ry: "r+y \<in> Rep_preal(R + S)" using r y 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

928 
show "r \<in> Rep_preal(R + S)" using r ypos rpos 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

929 
by (simp add: preal_downwards_closed [OF Rep_preal ry]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

930 
qed 
14335  931 

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

932 
lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

935 
obtain y where y: "y \<in> Rep_preal S" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

936 
have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

937 
from Gleason9_34 [OF Rep_preal ypos] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

938 
obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

939 
have "r + y \<in> Rep_preal (R + S)" using r y 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

941 
thus ?thesis using notin by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

942 
qed 
14335  943 

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

944 
lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

945 
by (insert Rep_preal_sum_not_subset, blast) 
14335  946 

947 
text{*at last, Gleason prop. 93.5(iii) page 123*} 

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

948 
lemma preal_self_less_add_left: "(R::preal) < R + S" 
26806  949 
apply (unfold preal_less_def less_le) 
14335  950 
apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym]) 
951 
done 

952 

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

953 
lemma preal_self_less_add_right: "(R::preal) < S + R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

954 
by (simp add: preal_add_commute preal_self_less_add_left) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

955 

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

956 
lemma preal_not_eq_self: "x \<noteq> x + (y::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

957 
by (insert preal_self_less_add_left [of x y], auto) 
14335  958 

959 

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

960 
subsection{*Subtraction for Positive Reals*} 
14335  961 

22710  962 
text{*Gleason prop. 93.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D = 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

963 
B"}. We define the claimed @{term D} and show that it is a positive real*} 
14335  964 

965 
text{*Part 1 of Dedekind sections definition*} 

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

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

967 
"R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

968 
apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

969 
apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

970 
apply (drule preal_imp_pos [OF Rep_preal], clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

971 
apply (cut_tac a=x and b=u in add_eq_exists, force) 
14335  972 
done 
973 

974 
text{*Part 2 of Dedekind sections definition*} 

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

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

976 
"\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

977 
apply (cut_tac X = S in Rep_preal_exists_bound) 
14335  978 
apply (erule exE) 
979 
apply (rule_tac x = x in exI, auto) 

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

980 
apply (simp add: diff_set_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

981 
apply (auto dest: Rep_preal [THEN preal_downwards_closed]) 
14335  982 
done 
983 

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

984 
lemma diff_set_not_rat_set: 
19765  985 
"diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs") 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

987 
show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

988 
show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

989 
qed 
14335  990 

991 
text{*Part 3 of Dedekind sections definition*} 

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

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

993 
"[R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

994 
==> z \<in> diff_set (Rep_preal S) (Rep_preal R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

996 
apply (rule_tac x=x in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

997 
apply (drule Rep_preal [THEN preal_downwards_closed], auto) 
14335  998 
done 
999 

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

1000 
text{*Part 4 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1002 
"[R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1003 
==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1005 
apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1006 
apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1007 
apply (rule_tac x="y+xa" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1008 
apply (auto simp add: add_ac) 
14335  1009 
done 
1010 

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

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

1012 
"R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1013 
apply (unfold preal_def cut_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1014 
apply (blast intro!: diff_set_not_empty diff_set_not_rat_set 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1017 

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

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

1019 
"R < S ==> 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1020 
(z \<in> Rep_preal(SR)) = 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1021 
(\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1022 
apply (simp add: preal_diff_def mem_diff_set Rep_preal) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1023 
apply (force simp add: diff_set_def) 
14335  1024 
done 
1025 

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

1026 

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

1027 
text{*proving that @{term "R + D \<le> S"}*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1028 

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

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

1030 
assumes Rless: "R < S" 
19765  1031 
and a: "a \<in> Rep_preal R" 
1032 
and cb: "c + b \<in> Rep_preal S" 

1033 
and "c \<notin> Rep_preal R" 

1034 
and "0 < b" 

1035 
and "0 < c" 

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

1036 
shows "a + b \<in> Rep_preal S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1038 
have "0<a" by (rule preal_imp_pos [OF Rep_preal a]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1040 
have "a < c" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1041 
by (blast intro: not_in_Rep_preal_ub ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1042 
ultimately show ?thesis using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1043 
by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1045 

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

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

1047 
"R < (S::preal) ==> R + (SR) \<le> S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1048 
apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1050 
apply (blast intro: less_add_left_lemma) 
14335  1051 
done 
1052 

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

1053 
subsection{*proving that @{term "S \<le> R + D"}  trickier*} 
14335  1054 

1055 
lemma lemma_sum_mem_Rep_preal_ex: 

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

1056 
"x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1057 
apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1058 
apply (cut_tac a=x and b=u in add_eq_exists, auto) 
14335  1059 
done 
1060 

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

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

1062 
assumes Rless: "R < S" 
19765  1063 
and x: "x \<in> Rep_preal S" 
1064 
and xnot: "x \<notin> Rep_preal R" 

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

1065 
shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1066 
z + v \<in> Rep_preal S & x = u + v" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1068 
have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1069 
from lemma_sum_mem_Rep_preal_ex [OF x] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1070 
obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1071 
from Gleason9_34 [OF Rep_preal epos] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1072 
obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" .. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1073 
with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1074 
from add_eq_exists [of r x] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1075 
obtain y where eq: "x = r+y" by auto 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1076 
show ?thesis 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1077 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1078 
show "r \<in> Rep_preal R" by (rule r) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1079 
show "r + e \<notin> Rep_preal R" by (rule notin) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1080 
show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1081 
show "x = r + y" by (simp add: eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1082 
show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1084 
show "0 < y" using rless eq by arith 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1087 

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

1088 
lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (SR)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1090 
apply (case_tac "x \<in> Rep_preal R") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1091 
apply (cut_tac Rep_preal_self_subset [of R], force) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1092 
apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1093 
apply (blast dest: less_add_left_lemma2) 
14335  1094 
done 
1095 

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

1096 
lemma less_add_left: "R < (S::preal) ==> R + (SR) = S" 
27682  1097 
by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2]) 
14335  1098 

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

1099 
lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1100 
by (fast dest: less_add_left) 
14335  1101 

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

1102 
lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1103 
apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc) 
14335  1104 
apply (rule_tac y1 = D in preal_add_commute [THEN subst]) 
1105 
apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric]) 

1106 
done 

1107 

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

1108 
lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1109 
by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T]) 
14335  1110 

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

1111 
lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1112 
apply (insert linorder_less_linear [of R S], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1113 
apply (drule_tac R = S and T = T in preal_add_less2_mono1) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1114 
apply (blast dest: order_less_trans) 
14335  1115 
done 
1116 

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

1117 
lemma preal_add_left_less_cancel: "T + R < T + S ==> R < (S::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1118 
by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T]) 
14335  1119 

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

1120 
lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)" 
14335  1121 
by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel) 
1122 

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

1123 
lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)" 
14335  1124 
by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel) 
1125 

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

1126 
lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1127 
by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1128 

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

1129 
lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1130 
by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1131 

14335  1132 
lemma preal_add_less_mono: 
1133 
"[ x1 < y1; x2 < y2 ] ==> x1 + x2 < y1 + (y2::preal)" 

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

1134 
apply (auto dest!: less_add_left_Ex simp add: preal_add_ac) 
14335  1135 
apply (rule preal_add_assoc [THEN subst]) 
1136 
apply (rule preal_self_less_add_right) 

1137 
done 

1138 

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

1139 
lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1140 
apply (insert linorder_less_linear [of R S], safe) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1141 
apply (drule_tac [!] T = T in preal_add_less2_mono1, auto) 
14335  1142 
done 
1143 

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

1144 
lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)" 
14335  1145 
by (auto intro: preal_add_right_cancel simp add: preal_add_commute) 
1146 

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

1147 
lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)" 
14335  1148 
by (fast intro: preal_add_left_cancel) 
1149 

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

1150 
lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)" 
14335  1151 
by (fast intro: preal_add_right_cancel) 
1152 

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

1153 
lemmas preal_cancels = 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1156 
preal_add_left_cancel_iff preal_add_right_cancel_iff 
14335  1157 

23285
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1158 
instance preal :: ordered_cancel_ab_semigroup_add 
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1159 
proof 
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1160 
fix a b c :: preal 
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1161 
show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel) 
23287
063039db59dd
define (1::preal); clean up instance declarations
huffman
parents:
23285
diff
changeset

1162 
show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left) 
23285
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1163 
qed 
c95a4f6b3881
instance preal :: ordered_cancel_ab_semigroup_add
huffman
parents:
22710
diff
changeset

1164 

14335  1165 

1166 
subsection{*Completeness of type @{typ preal}*} 

1167 

1168 
text{*Prove that supremum is a cut*} 

1169 

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

1170 
text{*Part 1 of Dedekind sections definition*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1171 

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

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

1173 
"P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1175 
apply (cut_tac X = x in mem_Rep_preal_Ex, auto) 
14335  1176 
done 
1177 

1178 

1179 
text{*Part 2 of Dedekind sections definition*} 

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

1180 

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

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

1182 
"\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1183 
apply (cut_tac X = Y in Rep_preal_exists_bound) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1184 
apply (auto simp add: preal_le_def) 
14335  1185 
done 
1186 

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

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

1188 
"\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1189 
apply (drule preal_sup_not_exists) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1190 
apply (blast intro: preal_imp_pos [OF Rep_preal]) 
14335  1191 
done 
1192 

1193 
text{*Part 3 of Dedekind sections definition*} 

1194 
lemma preal_sup_set_lemma3: 

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

1195 
"[P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1196 
==> z \<in> (\<Union>X \<in> P. Rep_preal(X))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1197 
by (auto elim: Rep_preal [THEN preal_downwards_closed]) 
14335  1198 

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

1199 
text{*Part 4 of Dedekind sections definition*} 
14335  1200 
lemma preal_sup_set_lemma4: 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1201 
"[P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) ] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1202 
==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1203 
by (blast dest: Rep_preal [THEN preal_exists_greater]) 
14335  1204 

1205 
lemma preal_sup: 

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

1206 
"[P \<noteq> {}; \<forall>X \<in> P. X \<le> Y] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1207 
apply (unfold preal_def cut_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1208 
apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1209 
preal_sup_set_lemma3 preal_sup_set_lemma4) 
14335  1210 
done 
1211 

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

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

1213 
"[ \<forall>X \<in> P. X \<le> Y; x \<in> P ] ==> x \<le> psup P" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1214 
apply (simp (no_asm_simp) add: preal_le_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1215 
apply (subgoal_tac "P \<noteq> {}") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1216 
apply (auto simp add: psup_def preal_sup) 
14335  1217 
done 
1218 

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

1219 
lemma psup_le_ub: "[ P \<noteq> {}; \<forall>X \<in> P. X \<le> Y ] ==> psup P \<le> Y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1220 
apply (simp (no_asm_simp) add: preal_le_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1221 
apply (simp add: psup_def preal_sup) 
14335  1222 
apply (auto simp add: preal_le_def) 
1223 
done 

1224 

1225 
text{*Supremum property*} 

1226 
lemma preal_complete: 

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

1227 
"[ P \<noteq> {}; \<forall>X \<in> P. X \<le> Y ] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1228 
apply (simp add: preal_less_def psup_def preal_sup) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1230 
apply (rename_tac U) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1231 
apply (cut_tac x = U and y = Z in linorder_less_linear) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1232 
apply (auto simp add: preal_less_def) 
14335  1233 
done 
1234 

1235 

20495  1236 
subsection{*The Embedding from @{typ rat} into @{typ preal}*} 
14335  1237 

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

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

1239 
"[x < y + z; 0 < x; 0 < y] ==> x * y * inverse (y + z) < (y::rat)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1240 
apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1242 
apply (simp add: mult_ac) 
14335  1243 
done 
1244 

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

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

1246 
assumes "u < x + y" 
19765  1247 
and "0 < x" 
1248 
and "0 < y" 

1249 
and "0 < u" 

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

1250 
shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1251 
proof (intro exI conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1252 
show "u * x * inverse(x+y) < x" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1254 
show "u * y * inverse(x+y) < y" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1255 
by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1256 
show "0 < u * x * inverse (x + y)" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1258 
show "0 < u * y * inverse (x + y)" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1260 
show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1261 
by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1263 

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

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

1265 
"[ 0 < x; 0 < y] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1266 
==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1267 
apply (unfold preal_of_rat_def preal_add_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1268 
apply (simp add: rat_mem_preal) 
14335  1269 
apply (rule_tac f = Abs_preal in arg_cong) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1271 
apply (blast dest: preal_of_rat_add_lemma2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1273 

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

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

1275 
"[x < y; 0 < x; 0 < z] ==> x * z * inverse y < (z::rat)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1276 
apply (frule_tac c = "z * inverse y" in mult_strict_right_mono) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1278 
apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1279 
apply (simp_all add: mult_ac) 
14335  1280 
done 
1281 

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

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

1283 
assumes xless: "x < y * z" 
19765  1284 
and xpos: "0 < x" 
1285 
and ypos: "0 < y" 

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

1286 
shows "x * z * inverse y * inverse z < (z::rat)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1288 
have "0 < y * z" using prems by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1289 
hence zpos: "0 < z" using prems by (simp add: zero_less_mult_iff) 
