author  nipkow 
Mon, 16 Aug 2004 14:22:27 +0200  
changeset 15131  c69542757a4d 
parent 15055  aed573241bea 
child 15140  322485b816ac 
permissions  rwrr 
7219  1 
(* Title : PReal.thy 
2 
ID : $Id$ 

5078  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

5 
Description : The positive reals as Dedekind sections of positive 

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

9 

15131  10 
theory PReal 
11 
import Rational 

12 
begin 

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

13 

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

14 
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

15 
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

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

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

18 
text{*As a special case, the sum of two positives is positive. One of the 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

19 
premises could be weakened to the relation @{text "\<le>"}.*} 
14738  20 
lemma pos_add_strict: "[0<a; b<c] ==> b < a + (c::'a::ordered_semidom)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

21 
by (insert add_strict_mono [of 0 a b c], simp) 
14335  22 

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

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

24 
"({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

25 
by (blast dest: dense intro: order_less_trans) 
14335  26 

5078  27 

28 
constdefs 

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

29 
cut :: "rat set => bool" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

31 
A < {r. 0 < r} & 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

32 
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y > z \<in> A) & (\<exists>u \<in> A. y < u)))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

33 

5078  34 

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

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

36 
assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

38 
let ?A = "{r::rat. 0 < r & r < q}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

39 
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

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

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

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

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

44 
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

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

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

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

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

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

50 

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

51 

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

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

53 
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

54 

14691  55 
instance preal :: "{ord, plus, minus, times, inverse}" .. 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

56 

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

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

58 
preal_of_rat :: "rat => preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

59 
"preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})" 
5078  60 

14335  61 
psup :: "preal set => preal" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

63 

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

64 
add_set :: "[rat set,rat set] => rat set" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

65 
"add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

66 

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

67 
diff_set :: "[rat set,rat set] => rat set" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

68 
"diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

69 

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

70 
mult_set :: "[rat set,rat set] => rat set" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

71 
"mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

72 

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

73 
inverse_set :: "rat set => rat set" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

74 
"inverse_set A == {x. \<exists>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

75 

5078  76 

14335  77 
defs (overloaded) 
5078  78 

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

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

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

81 

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

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

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

84 

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 

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

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

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

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

92 
"R * S == Abs_preal(mult_set (Rep_preal R) (Rep_preal S))" 
5078  93 

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

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

95 
"inverse R == Abs_preal(inverse_set (Rep_preal R))" 
14335  96 

97 

98 
lemma inj_on_Abs_preal: "inj_on Abs_preal preal" 

99 
apply (rule inj_on_inverseI) 

100 
apply (erule Abs_preal_inverse) 

101 
done 

102 

103 
declare inj_on_Abs_preal [THEN inj_on_iff, simp] 

104 

105 
lemma inj_Rep_preal: "inj(Rep_preal)" 

106 
apply (rule inj_on_inverseI) 

107 
apply (rule Rep_preal_inverse) 

108 
done 

109 

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

110 
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

111 
by (unfold preal_def cut_def, blast) 
14335  112 

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

113 
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

114 
by (force simp add: preal_def cut_def) 
14335  115 

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

116 
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

117 
by (drule preal_imp_psubset_positives, auto) 
14335  118 

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

119 
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

120 
by (unfold preal_def cut_def, blast) 
14335  121 

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

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

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

124 
apply (unfold preal_def cut_def, blast) 
14335  125 
done 
126 

127 
declare Abs_preal_inverse [simp] 

128 

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

129 
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

130 
by (unfold preal_def cut_def, blast) 
14335  131 

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

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

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

134 
"[ 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

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

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

137 
done 
14335  138 

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

139 
lemma Rep_preal_exists_bound: "\<exists>x. 0 < x & x \<notin> Rep_preal X" 
14335  140 
apply (cut_tac x = X in Rep_preal) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

141 
apply (drule preal_imp_psubset_positives) 
14335  142 
apply (auto simp add: psubset_def) 
143 
done 

144 

145 

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

147 

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

148 
lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

151 
apply (blast dest: dense intro: order_less_trans) 
14335  152 
done 
153 

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

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

155 
"[{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x] ==> x \<le> y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

156 
apply (simp add: linorder_not_less [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

157 
apply (blast dest: dense intro: order_less_trans) 
14335  158 
done 
159 

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

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

161 
"[{u::rat. 0 < u & u < x} = {u. 0 < u & u < y}; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

162 
0 < x; 0 < y] ==> x = y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

164 

14335  165 

166 

167 
subsection{*Theorems for Ordering*} 

168 

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

170 
Gleason p. 122  Remark (1)*} 

171 

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

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

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

174 
and notx: "x \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

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

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

181 
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

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

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

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

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

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

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

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

189 

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

190 
lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal] 
14335  191 

192 

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

193 
subsection{*The @{text "\<le>"} Ordering*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

194 

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

195 
lemma preal_le_refl: "w \<le> (w::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

196 
by (simp add: preal_le_def) 
14335  197 

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

198 
lemma preal_le_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> (k::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

200 

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

201 
lemma preal_le_anti_sym: "[ z \<le> w; w \<le> z ] ==> z = (w::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

203 
apply (rule Rep_preal_inject [THEN iffD1], blast) 
14335  204 
done 
205 

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

206 
(* Axiom 'order_less_le' of class 'order': *) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

207 
lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

208 
by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

209 

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

210 
instance preal :: order 
14691  211 
by intro_classes 
212 
(assumption  

213 
rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+ 

14335  214 

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

215 
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

216 
by (insert preal_imp_psubset_positives, blast) 
14335  217 

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

218 
lemma preal_le_linear: "x <= y  y <= (x::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

221 
apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

222 
elim: order_less_asym) 
14335  223 
done 
224 

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

225 
instance preal :: linorder 
14691  226 
by intro_classes (rule preal_le_linear) 
14335  227 

228 

229 

230 
subsection{*Properties of Addition*} 

231 

232 
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

233 
apply (unfold preal_add_def add_set_def) 
14335  234 
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

235 
apply (force simp add: add_commute) 
14335  236 
done 
237 

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

238 
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

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

240 

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

241 
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

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

243 

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

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

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

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

247 
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

248 
apply (auto simp add: add_set_def) 
14335  249 
done 
250 

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

251 
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

252 
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

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

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

255 
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

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

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

258 
apply (drule not_in_preal_ub, assumption+)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

259 
apply (force dest: add_strict_mono) 
14335  260 
done 
261 

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

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

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

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

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

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

267 
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

268 
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

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

270 
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

271 
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

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

273 

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

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

276 
"[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

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

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

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

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

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

282 
and [simp]: "0 < z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

283 
and zless: "z < x + y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

286 
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

287 
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

288 
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

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

290 
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

291 
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

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

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

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

295 
show "z = x*?f + y*?f" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

296 
by (simp add: left_distrib [symmetric] divide_inverse mult_ac 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

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

302 
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

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

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

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

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

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

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

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

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

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

312 
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

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

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

315 
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

316 
qed 
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 
qed 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

319 

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

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

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

322 
"[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

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

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

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

326 
apply (auto intro: add_strict_left_mono) 
14335  327 
done 
328 

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

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

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

331 
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

332 
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

333 
add_set_lemma3 add_set_lemma4) 
14335  334 
done 
335 

336 
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

337 
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

338 
apply (force simp add: add_set_def add_ac) 
14335  339 
done 
340 

341 
lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)" 

342 
apply (rule mk_left_commute [of "op +"]) 

343 
apply (rule preal_add_assoc) 

344 
apply (rule preal_add_commute) 

345 
done 

346 

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

347 
text{* Positive Real addition is an AC operator *} 
14335  348 
lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute 
349 

350 

351 
subsection{*Properties of Multiplication*} 

352 

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

354 

355 
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

356 
apply (unfold preal_mult_def mult_set_def) 
14335  357 
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

358 
apply (force simp add: mult_commute) 
14335  359 
done 
360 

15055  361 
text{*Multiplication of two positive reals gives a positive real.*} 
14335  362 

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

364 

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

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

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

367 
"[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

368 
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

369 
apply (auto simp add: mult_set_def) 
14335  370 
done 
371 

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

373 
lemma preal_not_mem_mult_set_Ex: 

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

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

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

376 
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

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

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

379 
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

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

381 
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

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

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

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

385 
show "x * y \<notin> mult_set A B" 
14377  386 
proof  
387 
{ fix u::rat and v::rat 

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

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

391 
moreover 

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

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

394 
moreover 

395 
from calculation 

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

397 
ultimately have False by force } 

14377  398 
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

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

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

401 
qed 
14335  402 

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

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

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

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

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

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

408 
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

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

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

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

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

413 
by (insert preal_not_mem_mult_set_Ex [OF A B], blast) 
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 

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

416 

14335  417 

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

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

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

420 
"[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

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

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

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

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

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

426 
and [simp]: "0 < z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

427 
and zless: "z < x * y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

430 
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

431 
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

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

433 
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

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

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

436 
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

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

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

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

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

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

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

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

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

445 
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

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

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

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

449 

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

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

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

452 
"[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

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

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

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

456 
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

457 
mult_strict_right_mono) 
14335  458 
done 
459 

460 

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

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

462 
"[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

463 
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

464 
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

465 
mult_set_lemma3 mult_set_lemma4) 
14335  466 
done 
467 

468 
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

469 
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

470 
apply (force simp add: mult_set_def mult_ac) 
14335  471 
done 
472 

473 
lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)" 

474 
apply (rule mk_left_commute [of "op *"]) 

475 
apply (rule preal_mult_assoc) 

476 
apply (rule preal_mult_commute) 

477 
done 

478 

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

479 

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

480 
text{* Positive Real multiplication is an AC operator *} 
14335  481 
lemmas preal_mult_ac = 
482 
preal_mult_assoc preal_mult_commute preal_mult_left_commute 

483 

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

484 

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

485 
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

486 

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

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

488 
by (simp add: preal_def cut_of_rat) 
14335  489 

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

490 
lemma preal_mult_1: "(preal_of_rat 1) * z = z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

494 
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

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

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

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

498 
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

499 
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

500 
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

501 
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

502 
thus "u * v \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

503 
by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

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

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

510 
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

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

512 
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

513 
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

514 
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

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

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

517 
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

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

519 
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

520 
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

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

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

523 
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

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

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

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

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

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

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

530 
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

531 
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

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

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

534 

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

535 

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

536 
lemma preal_mult_1_right: "z * (preal_of_rat 1) = z" 
14335  537 
apply (rule preal_mult_commute [THEN subst]) 
538 
apply (rule preal_mult_1) 

539 
done 

540 

541 

542 
subsection{*Distribution of Multiplication across Addition*} 

543 

544 
lemma mem_Rep_preal_add_iff: 

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

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

546 
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

547 
apply (simp add: add_set_def) 
14335  548 
done 
549 

550 
lemma mem_Rep_preal_mult_iff: 

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

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

552 
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

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

554 
done 
14335  555 

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

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

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

558 
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

559 
apply (force simp add: right_distrib) 
14335  560 
done 
561 

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

562 
lemma linorder_le_cases [case_names le ge]: 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

563 
"((x::'a::linorder) <= y ==> P) ==> (y <= x ==> P) ==> P" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

565 
done 
14335  566 

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

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

568 
assumes a: "a \<in> Rep_preal w" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

569 
and b: "b \<in> Rep_preal w" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

570 
and d: "d \<in> Rep_preal x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

571 
and e: "e \<in> Rep_preal y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

572 
shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

575 
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

576 
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

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

578 
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

579 
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

580 
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

581 
show "?c \<in> Rep_preal w" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

584 
hence "?c \<le> b" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

587 
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

590 
hence "?c \<le> a" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

593 
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

596 

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

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

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

599 
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

600 
apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto) 
14335  601 
done 
602 

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

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

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

605 
apply (rule equalityI [OF distrib_subset1 distrib_subset2]) 
14335  606 
done 
607 

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

608 
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

609 
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

610 

14335  611 

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

613 

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

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

615 
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

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

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

618 
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

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

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

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

622 
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

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

624 
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

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

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

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

628 
qed 
14335  629 

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

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

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

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

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

634 
apply (auto simp add: inverse_set_def) 
14335  635 
done 
636 

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

638 

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

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

640 
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

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

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

643 
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

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

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

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

647 
show "inverse x \<notin> inverse_set A" 
14377  648 
proof  
649 
{ fix y::rat 

650 
assume ygt: "inverse x < y" 

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

652 
have iyless: "inverse y < x" 

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

654 
have "inverse y \<in> A" 

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

656 
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

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

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

659 
qed 
14335  660 

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

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

662 
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

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

664 
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

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

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

667 
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

668 
qed 
14335  669 

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

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

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

672 
"[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

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

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

675 
apply (auto intro: order_less_trans) 
14335  676 
done 
677 

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

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

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

680 
"[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

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

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

683 
apply (blast intro: order_less_trans) 
14335  684 
done 
685 

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

686 

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

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

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

689 
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

690 
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

691 
inverse_set_lemma3 inverse_set_lemma4) 
14335  692 
done 
693 

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

694 

14335  695 
subsection{*Gleason's Lemma 93.4, page 122*} 
696 

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

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

698 
assumes A: "A \<in> preal" 
14369  699 
and "\<forall>x\<in>A. x + u \<in> A" 
700 
and "0 \<le> z" 

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

701 
shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A" 
14369  702 
proof (cases z rule: int_cases) 
703 
case (nonneg n) 

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

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

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

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

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

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

709 
case (Suc k) 
15013  710 
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

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

712 
thus ?case by (force simp add: left_distrib add_ac prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

714 
next 
14369  715 
case (neg n) 
716 
with prems show ?thesis by simp 

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

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

718 

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

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

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

721 
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

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

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

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

725 
assume bpos [simp]: "0 < b" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

726 
and dpos [simp]: "0 < d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

727 
and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

728 
and upos: "0 < Fract c d" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

729 
and ypos: "0 < Fract a b" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

730 
and notin: "Fract a b \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

732 
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

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

734 
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

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

736 
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

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

738 
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

739 
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

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

741 
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

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

743 
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

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

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

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

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

748 
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

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

750 
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

751 
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

752 
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

753 
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

754 
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

755 
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

756 
qed 
14335  757 

758 

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

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

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

761 
and upos: "0 < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

762 
shows "\<exists>r \<in> A. r + u \<notin> A" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

764 
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

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

766 
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

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

768 
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

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

770 

14335  771 

772 

773 
subsection{*Gleason's Lemma 93.6*} 

774 

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

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

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

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

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

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

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

781 
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

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

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

784 
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

785 
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

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

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

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

789 
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

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

791 
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

792 
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

793 
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

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

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

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

797 
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

798 
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

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

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

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

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

803 
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

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

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

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

807 
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

808 
also with ypos have "... = (r/y) * (y + ?d)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

810 
also have "... = r*x" using ypos 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

815 
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

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

817 
qed 
14335  818 

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

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

820 

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

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

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

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

824 
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

825 
apply (simp add: inverse_set_def) 
14335  826 
done 
827 

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

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

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

830 
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

831 

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

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

833 
assumes xpos: "0 < x" and xless: "x < 1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

834 
shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

835 
u \<in> Rep_preal R & x = r * u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

837 
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

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

839 
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

840 
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

841 
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

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

843 
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

844 
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

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

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

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

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

849 
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

850 
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

851 
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

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

853 
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

854 
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

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

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

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

858 

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

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

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

861 
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

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

863 
apply (blast dest: subset_inverse_mult_lemma) 
14335  864 
done 
865 

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

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

867 
assumes rpos: "0 < r" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

869 
and notin: "inverse y \<notin> Rep_preal R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

871 
shows "r*q < 1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

874 
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

875 
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

876 
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

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

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

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

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

881 

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

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

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

884 
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

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

886 
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

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

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

889 

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

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

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

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

893 
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

894 
done 
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 preal_mult_inverse_right: 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

899 
apply (rule preal_mult_inverse) 
14335  900 
done 
901 

902 

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

903 
text{*Theorems needing @{text Gleason9_34}*} 
14335  904 

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

905 
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

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

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

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

909 
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

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

911 
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

912 
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

913 
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

914 
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

915 
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

916 
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

917 
qed 
14335  918 

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

919 
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

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

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

922 
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

923 
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

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

925 
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

926 
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

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 
thus ?thesis using notin by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

929 
qed 
14335  930 

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

931 
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

932 
by (insert Rep_preal_sum_not_subset, blast) 
14335  933 

934 
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

935 
lemma preal_self_less_add_left: "(R::preal) < R + S" 
14335  936 
apply (unfold preal_less_def psubset_def) 
937 
apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym]) 

938 
done 

939 

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

940 
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

941 
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

942 

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

943 
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

944 
by (insert preal_self_less_add_left [of x y], auto) 
14335  945 

946 

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

947 
subsection{*Subtraction for Positive Reals*} 
14335  948 

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

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

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

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

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

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

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

955 
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

956 
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

957 
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

958 
apply (cut_tac a=x and b=u in add_eq_exists, force) 
14335  959 
done 
960 

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

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

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

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

964 
apply (cut_tac X = S in Rep_preal_exists_bound) 
14335  965 
apply (erule exE) 
966 
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

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

968 
apply (auto dest: Rep_preal [THEN preal_downwards_closed]) 
14335  969 
done 
970 

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

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

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

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

974 
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

975 
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

976 
qed 
14335  977 

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

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

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

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

981 
==> 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

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

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

984 
apply (drule Rep_preal [THEN preal_downwards_closed], auto) 
14335  985 
done 
986 

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

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

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

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

990 
==> \<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

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

992 
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

993 
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

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

995 
apply (auto simp add: add_ac) 
14335  996 
done 
997 

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

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

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

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

1001 
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

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

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

1004 

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

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

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

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

1008 
(\<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

1009 
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

1010 
apply (force simp add: diff_set_def) 
14335  1011 
done 
1012 

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

1013 

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

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

1015 

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

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

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

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

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

1020 
and "c \<notin> Rep_preal R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

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

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

1025 
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

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

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

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

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

1030 
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

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

1032 

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

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

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

1035 
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

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

1037 
apply (blast intro: less_add_left_lemma) 
14335  1038 
done 
1039 

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

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

1042 
lemma lemma_sum_mem_Rep_preal_ex: 

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

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

1044 
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

1045 
apply (cut_tac a=x and b=u in add_eq_exists, auto) 
14335  1046 
done 
1047 

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

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

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

1050 
and x: "x \<in> Rep_preal S" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1051 
and xnot: "x \<notin> Rep_preal R" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1052 
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

1053 
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

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

1055 
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

1056 
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

1057 
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

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

1059 
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

1060 
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

1061 
from add_eq_exists [of r x] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1062 
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

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

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

1065 
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

1066 
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

1067 
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

1068 
show "x = r + y" by (simp add: eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1069 
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

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

1071 
show "0 < y" using rless eq by arith 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1074 

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

1075 
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

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

1077 
apply (case_tac "x \<in> Rep_preal R") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1078 
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

1079 
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

1080 
apply (blast dest: less_add_left_lemma2) 
14335  1081 
done 
1082 

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

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

1084 
by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2]) 
14335  1085 

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

1086 
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

1087 
by (fast dest: less_add_left) 
14335  1088 

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

1089 
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

1090 
apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc) 
14335  1091 
apply (rule_tac y1 = D in preal_add_commute [THEN subst]) 
1092 
apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric]) 

1093 
done 

1094 

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

1095 
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

1096 
by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T]) 
14335  1097 

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

1098 
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

1099 
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

1100 
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

1101 
apply (blast dest: order_less_trans) 
14335  1102 
done 
1103 

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

1104 
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

1105 
by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T]) 
14335  1106 

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

1107 
lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)" 
14335  1108 
by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel) 
1109 

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

1110 
lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)" 
14335  1111 
by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel) 
1112 

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

1113 
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

1114 
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

1115 

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

1116 
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

1117 
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

1118 

14335  1119 
lemma preal_add_less_mono: 
1120 
"[ 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

1121 
apply (auto dest!: less_add_left_Ex simp add: preal_add_ac) 
14335  1122 
apply (rule preal_add_assoc [THEN subst]) 
1123 
apply (rule preal_self_less_add_right) 

1124 
done 

1125 

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

1126 
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

1127 
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

1128 
apply (drule_tac [!] T = T in preal_add_less2_mono1, auto) 
14335  1129 
done 
1130 

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

1131 
lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)" 
14335  1132 
by (auto intro: preal_add_right_cancel simp add: preal_add_commute) 
1133 

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

1134 
lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)" 
14335  1135 
by (fast intro: preal_add_left_cancel) 
1136 

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

1137 
lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)" 
14335  1138 
by (fast intro: preal_add_right_cancel) 
1139 

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

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

1141 
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

1142 
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

1143 
preal_add_left_cancel_iff preal_add_right_cancel_iff 
14335  1144 

1145 

1146 
subsection{*Completeness of type @{typ preal}*} 

1147 

1148 
text{*Prove that supremum is a cut*} 

1149 

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

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

1151 

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

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

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

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

1155 
apply (cut_tac X = x in mem_Rep_preal_Ex, auto) 
14335  1156 
done 
1157 

1158 

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

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

1160 

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

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

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

1163 
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

1164 
apply (auto simp add: preal_le_def) 
14335  1165 
done 
1166 

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

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

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

1169 
apply (drule preal_sup_not_exists) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1170 
apply (blast intro: preal_imp_pos [OF Rep_preal]) 
14335  1171 
done 
1172 

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

1174 
lemma preal_sup_set_lemma3: 

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

1175 
"[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

1176 
==> 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

1177 
by (auto elim: Rep_preal [THEN preal_downwards_closed]) 
14335  1178 

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

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

1181 
"[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

1182 
==> \<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

1183 
by (blast dest: Rep_preal [THEN preal_exists_greater]) 
14335  1184 

1185 
lemma preal_sup: 

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

1186 
"[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

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

1188 
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

1189 
preal_sup_set_lemma3 preal_sup_set_lemma4) 
14335  1190 
done 
1191 

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

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

1193 
"[ \<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

1194 
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

1195 
apply (subgoal_tac "P \<noteq> {}") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1196 
apply (auto simp add: psup_def preal_sup) 
14335  1197 
done 
1198 

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

1199 
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

1200 
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

1201 
apply (simp add: psup_def preal_sup) 
14335  1202 
apply (auto simp add: preal_le_def) 
1203 
done 

1204 

1205 
text{*Supremum property*} 

1206 
lemma preal_complete: 

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

1207 
"[ 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

1208 
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

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

1210 
apply (rename_tac U) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1211 
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

1212 
apply (auto simp add: preal_less_def) 
14335  1213 
done 
1214 

1215 

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

1216 
subsection{*The Embadding from @{typ rat} into @{typ preal}*} 
14335  1217 

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

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

1219 
"[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

1220 
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

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

1222 
apply (simp add: mult_ac) 
14335  1223 
done 
1224 

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

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

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

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

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

1229 
and "0 < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1230 
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

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

1232 
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

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

1234 
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

1235 
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

1236 
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

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

1238 
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

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

1240 
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

1241 
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

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

1243 

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

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

1245 
"[ 0 < x; 0 < y] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1246 
==> 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

1247 
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

1248 
apply (simp add: rat_mem_preal) 
14335  1249 
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

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

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

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

1253 

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

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

1255 
"[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

1256 
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

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

1258 
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

1259 
apply (simp_all add: mult_ac) 
14335  1260 
done 
1261 

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

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

1263 
assumes xless: "x < y * z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1266 
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

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

1268 
have "0 < y * z" using prems by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1269 
hence zpos: "0 < z" using prems by (simp add: zero_less_mult_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1270 
have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

1272 
also have "... = x/y" using zpos 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset

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

1274 
also have "... < z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1277 
qed 
14335  1278 

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

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

1280 
assumes uless: "u < x * y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1283 
and "0 < u" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

1284 
shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1287 
obtain r where "u < r" "r < x * y" by blast 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14335
diff
changeset

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

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

1290 
show "u * x * inverse r < x" using prems 