author  paulson 
Tue, 27 Jan 2004 15:39:51 +0100  
changeset 14365  3d4df8c166ae 
parent 14348  744c868ee0b7 
child 14369  c50188fe6366 
permissions  rwrr 
5588  1 
(* Title : Real/RealDef.thy 
7219  2 
ID : $Id$ 
5588  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

5 
Description : The reals 

14269  6 
*) 
7 

8 
theory RealDef = PReal: 

5588  9 

10 
constdefs 

11 
realrel :: "((preal * preal) * (preal * preal)) set" 

14269  12 
"realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
13 

14 
typedef (REAL) real = "UNIV//realrel" 

15 
by (auto simp add: quotient_def) 

5588  16 

14269  17 
instance real :: ord .. 
18 
instance real :: zero .. 

19 
instance real :: one .. 

20 
instance real :: plus .. 

21 
instance real :: times .. 

22 
instance real :: minus .. 

23 
instance real :: inverse .. 

24 

25 
consts 

26 
(*Overloaded constants denoting the Nat and Real subsets of enclosing 

27 
types such as hypreal and complex*) 

28 
Nats :: "'a set" 

29 
Reals :: "'a set" 

30 

31 
(*overloaded constant for injecting other types into "real"*) 

32 
real :: "'a => real" 

5588  33 

34 

14269  35 
defs (overloaded) 
5588  36 

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

38 
"0 == Abs_REAL(realrel``{(preal_of_rat 1, preal_of_rat 1)})" 
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

39 

14269  40 
real_one_def: 
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

41 
"1 == Abs_REAL(realrel`` 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

42 
{(preal_of_rat 1 + preal_of_rat 1, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

43 
preal_of_rat 1)})" 
5588  44 

14269  45 
real_minus_def: 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

46 
" R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})" 
10606  47 

14269  48 
real_diff_def: 
10606  49 
"R  (S::real) == R +  S" 
5588  50 

14269  51 
real_inverse_def: 
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11701
diff
changeset

52 
"inverse (R::real) == (SOME S. (R = 0 & S = 0)  S * R = 1)" 
5588  53 

14269  54 
real_divide_def: 
10606  55 
"R / (S::real) == R * inverse S" 
14269  56 

5588  57 
constdefs 
58 

12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

59 
(** these don't use the overloaded "real" function: users don't see them **) 
14269  60 

61 
real_of_preal :: "preal => real" 

7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

62 
"real_of_preal m == 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

63 
Abs_REAL(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})" 
5588  64 

14269  65 
defs (overloaded) 
5588  66 

14269  67 
real_add_def: 
14329  68 
"P+Q == Abs_REAL(\<Union>p1\<in>Rep_REAL(P). \<Union>p2\<in>Rep_REAL(Q). 
10834  69 
(%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)" 
14269  70 

71 
real_mult_def: 

14329  72 
"P*Q == Abs_REAL(\<Union>p1\<in>Rep_REAL(P). \<Union>p2\<in>Rep_REAL(Q). 
10834  73 
(%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)}) 
10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

74 
p2) p1)" 
5588  75 

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

76 
real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

77 

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

78 

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

80 
"P \<le> (Q::real) == \<exists>x1 y1 x2 y2. x1 + y2 \<le> x2 + y1 & 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

81 
(x1,y1) \<in> Rep_REAL(P) & (x2,y2) \<in> Rep_REAL(Q)" 
5588  82 

14334  83 
real_abs_def: "abs (r::real) == (if 0 \<le> r then r else r)" 
84 

85 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12018
diff
changeset

86 
syntax (xsymbols) 
14269  87 
Reals :: "'a set" ("\<real>") 
88 
Nats :: "'a set" ("\<nat>") 

89 

90 

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

91 
defs (overloaded) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

93 
"real z == Abs_REAL(\<Union>(i,j) \<in> Rep_Integ z. realrel `` 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

94 
{(preal_of_rat(rat(int(Suc i))), 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

95 
preal_of_rat(rat(int(Suc j))))})" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

96 

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

97 
real_of_nat_def: "real n == real (int n)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

98 

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

99 

14329  100 
subsection{*Proving that realrel is an equivalence relation*} 
14269  101 

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

103 
assumes "x + y1 = x1 + y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

104 
and "x + y2 = x2 + y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

105 
shows "x1 + y2 = x2 + (y1::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

107 
have "(x1 + y2) + x = (x + y2) + x1" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

108 
also have "... = (x2 + y) + x1" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

109 
also have "... = x2 + (x1 + y)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

110 
also have "... = x2 + (x + y1)" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

111 
also have "... = (x2 + y1) + x" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

112 
finally have "(x1 + y2) + x = (x2 + y1) + x" . 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

113 
thus ?thesis by (simp add: preal_add_right_cancel_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

115 

14269  116 

117 
lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)" 

118 
by (unfold realrel_def, blast) 

119 

120 
lemma realrel_refl: "(x,x): realrel" 

121 
apply (case_tac "x") 

122 
apply (simp add: realrel_def) 

123 
done 

124 

125 
lemma equiv_realrel: "equiv UNIV realrel" 

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

126 
apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

127 
apply (blast dest: preal_trans_lemma) 
14269  128 
done 
129 

130 
(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *) 

131 
lemmas equiv_realrel_iff = 

132 
eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I] 

133 

134 
declare equiv_realrel_iff [simp] 

135 

136 
lemma realrel_in_real [simp]: "realrel``{(x,y)}: REAL" 

137 
by (unfold REAL_def realrel_def quotient_def, blast) 

138 

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

139 

14269  140 
lemma inj_on_Abs_REAL: "inj_on Abs_REAL REAL" 
141 
apply (rule inj_on_inverseI) 

142 
apply (erule Abs_REAL_inverse) 

143 
done 

144 

145 
declare inj_on_Abs_REAL [THEN inj_on_iff, simp] 

146 
declare Abs_REAL_inverse [simp] 

147 

148 

149 
lemmas eq_realrelD = equiv_realrel [THEN [2] eq_equiv_class] 

150 

151 
lemma inj_Rep_REAL: "inj Rep_REAL" 

152 
apply (rule inj_on_inverseI) 

153 
apply (rule Rep_REAL_inverse) 

154 
done 

155 

156 
(** real_of_preal: the injection from preal to real **) 

157 
lemma inj_real_of_preal: "inj(real_of_preal)" 

158 
apply (rule inj_onI) 

159 
apply (unfold real_of_preal_def) 

160 
apply (drule inj_on_Abs_REAL [THEN inj_onD]) 

161 
apply (rule realrel_in_real)+ 

162 
apply (drule eq_equiv_class) 

163 
apply (rule equiv_realrel, blast) 

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

164 
apply (simp add: realrel_def preal_add_right_cancel_iff) 
14269  165 
done 
166 

167 
lemma eq_Abs_REAL: 

168 
"(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P" 

169 
apply (rule_tac x1 = z in Rep_REAL [unfolded REAL_def, THEN quotientE]) 

170 
apply (drule_tac f = Abs_REAL in arg_cong) 

171 
apply (case_tac "x") 

172 
apply (simp add: Rep_REAL_inverse) 

173 
done 

174 

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

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

176 
"[(x1,y1) \<in> Rep_REAL w; (x2,y2) \<in> Rep_REAL z] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

177 
==> (z = w) = (x1+y2 = x2+y1)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

178 
apply (insert quotient_eq_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

179 
[OF equiv_realrel, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

180 
of "Rep_REAL w" "Rep_REAL z" "(x1,y1)" "(x2,y2)"]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

181 
apply (simp add: Rep_REAL [unfolded REAL_def] Rep_REAL_inject eq_commute) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

183 

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

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

185 
"[R \<in> REAL; (x1,y1) \<in> R; (x2,y2) \<in> R] ==> x1+y2 = x2+y1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

186 
apply (auto simp add: REAL_def realrel_def quotient_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

187 
apply (blast dest: preal_trans_lemma) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

189 

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

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

191 
"((x + z, y + z) \<in> Rep_REAL R) = ((x, y) \<in> Rep_REAL R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

192 
apply (rule_tac z = R in eq_Abs_REAL, simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

193 
apply (rename_tac u v) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

194 
apply (subgoal_tac "(u + (y + z) = x + z + v) = ((u + y) + z = (x + v) + z)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

195 
prefer 2 apply (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

198 

14269  199 

14329  200 
subsection{*Congruence property for addition*} 
14269  201 

202 
lemma real_add_congruent2_lemma: 

203 
"[a + ba = aa + b; ab + bc = ac + bb] 

204 
==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))" 

205 
apply (simp add: preal_add_assoc) 

206 
apply (rule preal_add_left_commute [of ab, THEN ssubst]) 

207 
apply (simp add: preal_add_assoc [symmetric]) 

208 
apply (simp add: preal_add_ac) 

209 
done 

210 

211 
lemma real_add: 

212 
"Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) = 

213 
Abs_REAL(realrel``{(x1+x2, y1+y2)})" 

214 
apply (simp add: real_add_def UN_UN_split_split_eq) 

215 
apply (subst equiv_realrel [THEN UN_equiv_class2]) 

216 
apply (auto simp add: congruent2_def) 

217 
apply (blast intro: real_add_congruent2_lemma) 

218 
done 

219 

220 
lemma real_add_commute: "(z::real) + w = w + z" 

221 
apply (rule_tac z = z in eq_Abs_REAL) 

222 
apply (rule_tac z = w in eq_Abs_REAL) 

223 
apply (simp add: preal_add_ac real_add) 

224 
done 

225 

226 
lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)" 

227 
apply (rule_tac z = z1 in eq_Abs_REAL) 

228 
apply (rule_tac z = z2 in eq_Abs_REAL) 

229 
apply (rule_tac z = z3 in eq_Abs_REAL) 

230 
apply (simp add: real_add preal_add_assoc) 

231 
done 

232 

233 
lemma real_add_zero_left: "(0::real) + z = z" 

234 
apply (unfold real_of_preal_def real_zero_def) 

235 
apply (rule_tac z = z in eq_Abs_REAL) 

236 
apply (simp add: real_add preal_add_ac) 

237 
done 

238 

239 
lemma real_add_zero_right: "z + (0::real) = z" 

14334  240 
by (simp add: real_add_zero_left real_add_commute) 
14269  241 

242 
instance real :: plus_ac0 

243 
by (intro_classes, 

244 
(assumption  

245 
rule real_add_commute real_add_assoc real_add_zero_left)+) 

246 

247 

14334  248 
subsection{*Additive Inverse on real*} 
249 

250 
lemma real_minus_congruent: 

251 
"congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)" 

252 
apply (unfold congruent_def, clarify) 

253 
apply (simp add: preal_add_commute) 

254 
done 

255 

256 
lemma real_minus: 

257 
" (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})" 

258 
apply (unfold real_minus_def) 

259 
apply (rule_tac f = Abs_REAL in arg_cong) 

260 
apply (simp add: realrel_in_real [THEN Abs_REAL_inverse] 

261 
UN_equiv_class [OF equiv_realrel real_minus_congruent]) 

262 
done 

263 

264 
lemma real_add_minus_left: "(z) + z = (0::real)" 

14269  265 
apply (unfold real_zero_def) 
266 
apply (rule_tac z = z in eq_Abs_REAL) 

267 
apply (simp add: real_minus real_add preal_add_commute) 

268 
done 

269 

270 

14329  271 
subsection{*Congruence property for multiplication*} 
14269  272 

14329  273 
lemma real_mult_congruent2_lemma: 
274 
"!!(x1::preal). [ x1 + y2 = x2 + y1 ] ==> 

14269  275 
x * x1 + y * y1 + (x * y2 + x2 * y) = 
276 
x * x2 + y * y2 + (x * y1 + x1 * y)" 

277 
apply (simp add: preal_add_left_commute preal_add_assoc [symmetric] preal_add_mult_distrib2 [symmetric]) 

278 
apply (rule preal_mult_commute [THEN subst]) 

279 
apply (rule_tac y1 = x2 in preal_mult_commute [THEN subst]) 

280 
apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric]) 

281 
apply (simp add: preal_add_commute) 

282 
done 

283 

284 
lemma real_mult_congruent2: 

285 
"congruent2 realrel (%p1 p2. 

286 
(%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)" 

287 
apply (rule equiv_realrel [THEN congruent2_commuteI], clarify) 

288 
apply (unfold split_def) 

289 
apply (simp add: preal_mult_commute preal_add_commute) 

290 
apply (auto simp add: real_mult_congruent2_lemma) 

291 
done 

292 

293 
lemma real_mult: 

294 
"Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) = 

295 
Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})" 

296 
apply (unfold real_mult_def) 

297 
apply (simp add: equiv_realrel [THEN UN_equiv_class2] real_mult_congruent2) 

298 
done 

299 

300 
lemma real_mult_commute: "(z::real) * w = w * z" 

301 
apply (rule_tac z = z in eq_Abs_REAL) 

302 
apply (rule_tac z = w in eq_Abs_REAL) 

303 
apply (simp add: real_mult preal_add_ac preal_mult_ac) 

304 
done 

305 

306 
lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)" 

307 
apply (rule_tac z = z1 in eq_Abs_REAL) 

308 
apply (rule_tac z = z2 in eq_Abs_REAL) 

309 
apply (rule_tac z = z3 in eq_Abs_REAL) 

310 
apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac) 

311 
done 

312 

313 
lemma real_mult_1: "(1::real) * z = z" 

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

314 
apply (unfold real_one_def) 
14269  315 
apply (rule_tac z = z in eq_Abs_REAL) 
14334  316 
apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right 
317 
preal_mult_ac preal_add_ac) 

14269  318 
done 
319 

320 
lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" 

321 
apply (rule_tac z = z1 in eq_Abs_REAL) 

322 
apply (rule_tac z = z2 in eq_Abs_REAL) 

323 
apply (rule_tac z = w in eq_Abs_REAL) 

324 
apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac) 

325 
done 

326 

14329  327 
text{*one and zero are distinct*} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

328 
lemma real_zero_not_eq_one: "0 \<noteq> (1::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

329 
apply (subgoal_tac "preal_of_rat 1 < preal_of_rat 1 + preal_of_rat 1") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

330 
prefer 2 apply (simp add: preal_self_less_add_left) 
14269  331 
apply (unfold real_zero_def real_one_def) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

332 
apply (auto simp add: preal_add_right_cancel_iff) 
14269  333 
done 
334 

14329  335 
subsection{*existence of inverse*} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

336 

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

337 
lemma real_zero_iff: "Abs_REAL (realrel `` {(x, x)}) = 0" 
14269  338 
apply (unfold real_zero_def) 
339 
apply (auto simp add: preal_add_commute) 

340 
done 

341 

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

342 
text{*Instead of using an existential quantifier and constructing the inverse 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

343 
within the proof, we could define the inverse explicitly.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

344 

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

345 
lemma real_mult_inverse_left_ex: "x \<noteq> 0 ==> \<exists>y. y*x = (1::real)" 
14269  346 
apply (unfold real_zero_def real_one_def) 
347 
apply (rule_tac z = x in eq_Abs_REAL) 

348 
apply (cut_tac x = xa and y = y in linorder_less_linear) 

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

349 
apply (auto dest!: less_add_left_Ex simp add: real_zero_iff) 
14334  350 
apply (rule_tac 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

351 
x = "Abs_REAL (realrel `` { (preal_of_rat 1, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

352 
inverse (D) + preal_of_rat 1)}) " 
14334  353 
in exI) 
354 
apply (rule_tac [2] 

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

355 
x = "Abs_REAL (realrel `` { (inverse (D) + preal_of_rat 1, 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

356 
preal_of_rat 1)})" 
14334  357 
in exI) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

358 
apply (auto simp add: real_mult preal_mult_1_right 
14329  359 
preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

360 
preal_mult_inverse_right preal_add_ac preal_mult_ac) 
14269  361 
done 
362 

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

363 
lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)" 
14269  364 
apply (unfold real_inverse_def) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

365 
apply (frule real_mult_inverse_left_ex, safe) 
14269  366 
apply (rule someI2, auto) 
367 
done 

14334  368 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

369 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

370 
subsection{*The Real Numbers form a Field*} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

371 

14334  372 
instance real :: field 
373 
proof 

374 
fix x y z :: real 

375 
show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) 

376 
show "x + y = y + x" by (rule real_add_commute) 

377 
show "0 + x = x" by simp 

378 
show " x + x = 0" by (rule real_add_minus_left) 

379 
show "x  y = x + (y)" by (simp add: real_diff_def) 

380 
show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) 

381 
show "x * y = y * x" by (rule real_mult_commute) 

382 
show "1 * x = x" by (rule real_mult_1) 

383 
show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) 

384 
show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one) 

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

385 
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left) 
14334  386 
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

387 
assume eq: "z+x = z+y" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

388 
hence "(z + z) + x = (z + z) + y" by (simp only: eq real_add_assoc) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

389 
thus "x = y" by (simp add: real_add_minus_left) 
14334  390 
qed 
391 

392 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

393 
text{*Inverse of zero! Useful to simplify certain equations*} 
14269  394 

14334  395 
lemma INVERSE_ZERO: "inverse 0 = (0::real)" 
396 
apply (unfold real_inverse_def) 

397 
apply (rule someI2) 

398 
apply (auto simp add: zero_neq_one) 

14269  399 
done 
14334  400 

401 
lemma DIVISION_BY_ZERO: "a / (0::real) = 0" 

402 
by (simp add: real_divide_def INVERSE_ZERO) 

403 

404 
instance real :: division_by_zero 

405 
proof 

406 
fix x :: real 

407 
show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) 

408 
show "x/0 = 0" by (rule DIVISION_BY_ZERO) 

409 
qed 

410 

411 

412 
(*Pull negations out*) 

413 
declare minus_mult_right [symmetric, simp] 

414 
minus_mult_left [symmetric, simp] 

415 

416 
lemma real_mult_1_right: "z * (1::real) = z" 

417 
by (rule Ring_and_Field.mult_1_right) 

14269  418 

419 

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

420 
subsection{*The @{text "\<le>"} Ordering*} 
14269  421 

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

422 
lemma real_le_refl: "w \<le> (w::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

423 
apply (rule_tac z = w in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

424 
apply (force simp add: real_le_def) 
14269  425 
done 
426 

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

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

428 
assumes le1: "x1 + y2 \<le> x2 + y1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

429 
and le2: "u1 + v2 \<le> u2 + v1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

430 
and eq: "x2 + v1 = u1 + y2" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

431 
shows "x1 + v2 + u1 + y2 \<le> u2 + u1 + y2 + (y1::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

433 
have "x1 + v2 + u1 + y2 = (x1 + y2) + (u1 + v2)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

434 
also have "... \<le> (x2 + y1) + (u1 + v2)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

435 
by (simp add: prems preal_add_le_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

436 
also have "... \<le> (x2 + y1) + (u2 + v1)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

437 
by (simp add: prems preal_add_le_cancel_left) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

438 
also have "... = (x2 + v1) + (u2 + y1)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

439 
also have "... = (u1 + y2) + (u2 + y1)" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

440 
also have "... = u2 + u1 + y2 + y1" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

442 
qed 
14269  443 

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

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

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

446 
apply (rename_tac x1 u1 y1 v1 x2 u2 y2 v2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

447 
apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

450 
apply (rule_tac x="u2 + (x2 + v1)" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

451 
apply (rule_tac x="v2 + (u1 + y2)" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

452 
apply (simp add: Rep_REAL_cancel_right preal_add_le_cancel_right 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

453 
preal_add_assoc [symmetric] real_le_trans_lemma) 
14269  454 
done 
455 

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

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

457 
assumes le1: "x1 + y2 \<le> x2 + y1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

458 
and le2: "u1 + v2 \<le> u2 + v1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

459 
and eq1: "x1 + v2 = u2 + y1" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

460 
and eq2: "x2 + v1 = u1 + y2" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

461 
shows "x2 + y1 = x1 + (y2::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

462 
proof (rule order_antisym) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

463 
show "x1 + y2 \<le> x2 + y1" . 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

464 
have "(x2 + y1) + (u1+u2) = x2 + u1 + (u2 + y1)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

465 
also have "... = x2 + u1 + (x1 + v2)" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

466 
also have "... = (x2 + x1) + (u1 + v2)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

467 
also have "... \<le> (x2 + x1) + (u2 + v1)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

469 
also have "... = (x1 + u2) + (x2 + v1)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

470 
also have "... = (x1 + u2) + (u1 + y2)" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

471 
also have "... = (x1 + y2) + (u1 + u2)" by (simp add: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

472 
finally show "x2 + y1 \<le> x1 + y2" by (simp add: preal_add_le_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

473 
qed 
14334  474 

475 
lemma real_le_anti_sym: "[ z \<le> w; w \<le> z ] ==> z = (w::real)" 

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

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

477 
apply (rule real_eq_iff [THEN iffD2], assumption+) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

478 
apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

479 
apply (blast intro: real_le_anti_sym_lemma) 
14334  480 
done 
481 

482 
(* Axiom 'order_less_le' of class 'order': *) 

483 
lemma real_less_le: "((w::real) < z) = (w \<le> z & w \<noteq> z)" 

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

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

485 

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

486 
instance real :: order 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

489 
rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

490 

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

491 
text{*Simplifies a strange formula that occurs quantified.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

492 
lemma preal_strange_le_eq: "(x1 + x2 \<le> x2 + y1) = (x1 \<le> (y1::preal))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

493 
by (simp add: preal_add_commute [of x1] preal_add_le_cancel_left) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

494 

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

495 
text{*This is the nicest way to prove linearity*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

496 
lemma real_le_linear_0: "(z::real) \<le> 0  0 \<le> z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

497 
apply (rule_tac z = z in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

498 
apply (auto simp add: real_le_def real_zero_def preal_add_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

500 
apply (cut_tac x=x and y=y in linorder_linear, auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

502 

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

503 
lemma real_minus_zero_le_iff: "(0 \<le> R) = (R \<le> (0::real))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

504 
apply (rule_tac z = R in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

505 
apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

506 
preal_cancels preal_strange_le_eq) 
14334  507 
done 
508 

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

509 
lemma real_le_imp_diff_le_0: "x \<le> y ==> xy \<le> (0::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

510 
apply (rule_tac z = x in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

511 
apply (rule_tac z = y in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

512 
apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

513 
real_add preal_add_ac preal_cancels preal_strange_le_eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

514 
apply (rule exI)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

515 
apply (rule conjI, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

516 
apply (subgoal_tac " x + (x2 + y1 + ya) = (x + y1) + (x2 + ya)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

517 
prefer 2 apply (simp (no_asm) only: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

518 
apply (subgoal_tac "x1 + y2 + (xa + y) = (x1 + y) + (xa + y2)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

519 
prefer 2 apply (simp (no_asm) only: preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

522 

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

523 
lemma real_diff_le_0_imp_le: "xy \<le> (0::real) ==> x \<le> y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

524 
apply (rule_tac z = x in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

525 
apply (rule_tac z = y in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

526 
apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

527 
real_add preal_add_ac preal_cancels preal_strange_le_eq) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

528 
apply (rule exI)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

529 
apply (rule conjI, rule_tac [2] conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

530 
apply (rule_tac [2] refl)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

531 
apply (subgoal_tac "(x + ya) + (x1 + y1) \<le> (xa + y) + (x1 + y1)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

533 
apply (subgoal_tac "x1 + (x + (y1 + ya)) \<le> y1 + (x1 + (xa + y))") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

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

537 

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

538 
lemma real_le_eq_diff: "(x \<le> y) = (xy \<le> (0::real))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

539 
by (blast intro!: real_diff_le_0_imp_le real_le_imp_diff_le_0) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

540 

14334  541 

542 
(* Axiom 'linorder_linear' of class 'linorder': *) 

543 
lemma real_le_linear: "(z::real) \<le> w  w \<le> z" 

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

544 
apply (insert real_le_linear_0 [of "zw"]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

545 
apply (auto simp add: real_le_eq_diff [of w] real_le_eq_diff [of z] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

546 
real_minus_zero_le_iff [symmetric]) 
14334  547 
done 
548 

549 
instance real :: linorder 

550 
by (intro_classes, rule real_le_linear) 

551 

552 

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

553 
lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

554 
apply (auto simp add: real_le_eq_diff [of x] real_le_eq_diff [of "z+x"]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

555 
apply (subgoal_tac "z + x  (z + y) = (z + z) + (x  y)") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

556 
prefer 2 apply (simp add: diff_minus add_ac, simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

557 
done 
14334  558 

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

559 

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

560 
lemma real_minus_zero_le_iff2: "(R \<le> 0) = (0 \<le> (R::real))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

561 
apply (rule_tac z = R in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

562 
apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

563 
preal_cancels preal_strange_le_eq) 
14334  564 
done 
565 

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

566 
lemma real_minus_zero_less_iff: "(0 < R) = (R < (0::real))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

567 
by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

568 

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

569 
lemma real_minus_zero_less_iff2: "(R < 0) = ((0::real) < R)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

570 
by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff) 
14334  571 

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

572 
lemma real_sum_gt_zero_less: "(0 < S + (W::real)) ==> (W < S)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

573 
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

574 

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

575 
text{*Used a few times in Lim and Transcendental*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

576 
lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (W::real))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

577 
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) 
14334  578 

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

579 
text{*Handles other strange cases that arise in these proofs.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

580 
lemma forall_imp_less: "\<forall>u v. u \<le> v \<longrightarrow> x + v \<noteq> u + (y::preal) ==> y < x"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

581 
apply (drule_tac x=x in spec) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

582 
apply (drule_tac x=y in spec) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

583 
apply (simp add: preal_add_commute linorder_not_le) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

584 
done 
14334  585 

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

586 
text{*The arithmetic decision procedure is not set up for type preal.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

588 
assumes eq: "a+b = c+d" and le: "c \<le> a" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

589 
shows "b \<le> (d::preal)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

591 
have "c+d \<le> a+d" by (simp add: prems preal_cancels) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

592 
hence "a+b \<le> a+d" by (simp add: prems) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

593 
thus "b \<le> d" by (simp add: preal_cancels) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

594 
qed 
14334  595 

596 
lemma real_mult_order: "[ 0 < x; 0 < y ] ==> (0::real) < x * y" 

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

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

598 
{*Reduce to the (simpler) @{text "\<le>"} relation *} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

599 
apply (rule_tac z = x in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

600 
apply (rule_tac z = y in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

601 
apply (auto simp add: real_zero_def real_le_def real_mult preal_add_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

603 
apply (drule preal_eq_le_imp_le, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

604 
apply (auto dest!: forall_imp_less less_add_left_Ex 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

605 
simp add: preal_add_ac preal_mult_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

607 
apply (insert preal_self_less_add_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

608 
apply (simp add: linorder_not_le [symmetric]) 
14334  609 
done 
610 

611 
lemma real_mult_less_mono2: "[ (0::real) < z; x < y ] ==> z * x < z * y" 

612 
apply (rule real_sum_gt_zero_less) 

613 
apply (drule real_less_sum_gt_zero [of x y]) 

614 
apply (drule real_mult_order, assumption) 

615 
apply (simp add: right_distrib) 

616 
done 

617 

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

618 
text{*lemma for proving @{term "0<(1::real)"}*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

619 
lemma real_zero_le_one: "0 \<le> (1::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

620 
apply (auto simp add: real_zero_def real_one_def real_le_def preal_add_ac 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

623 
apply (rule_tac x="preal_of_rat 1" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

624 
apply (auto simp add: preal_add_ac preal_self_less_add_left order_less_imp_le) 
14334  625 
done 
626 

627 
subsection{*The Reals Form an Ordered Field*} 

628 

629 
instance real :: ordered_field 

630 
proof 

631 
fix x y z :: real 

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

632 
show "0 < (1::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

633 
by (simp add: real_less_def real_zero_le_one real_zero_not_eq_one) 
14334  634 
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono) 
635 
show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) 

636 
show "\<bar>x\<bar> = (if x < 0 then x else x)" 

637 
by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) 

638 
qed 

639 

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

640 

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

641 

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

642 
text{*The function @{term real_of_preal} requires many proofs, but it seems 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

643 
to be essential for proving completeness of the reals from that of the 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

644 
positive reals.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

645 

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

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

647 
"real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

648 
by (simp add: real_of_preal_def real_add preal_add_mult_distrib preal_mult_1 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

650 

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

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

652 
"real_of_preal ((x::preal) * y) = real_of_preal x* real_of_preal y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

653 
by (simp add: real_of_preal_def real_mult preal_add_mult_distrib2 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

654 
preal_mult_1 preal_mult_1_right preal_add_ac preal_mult_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

655 

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

656 

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

657 
text{*Gleason prop 94.4 p 127*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

659 
"\<exists>m. (x::real) = real_of_preal m  x = 0  x = (real_of_preal m)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

660 
apply (unfold real_of_preal_def real_zero_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

661 
apply (rule_tac z = x in eq_Abs_REAL) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

662 
apply (auto simp add: real_minus preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

663 
apply (cut_tac x = x and y = y in linorder_less_linear) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

664 
apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

667 

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

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

669 
"real_of_preal m1 \<le> real_of_preal m2 ==> m1 \<le> m2" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

670 
apply (unfold real_of_preal_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

671 
apply (auto simp add: real_le_def preal_add_ac) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

672 
apply (auto simp add: preal_add_assoc [symmetric] preal_add_right_cancel_iff) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

673 
apply (auto simp add: preal_add_ac preal_add_le_cancel_left) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

675 

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

676 
lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

677 
by (auto simp add: real_of_preal_leD linorder_not_le [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

678 

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

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

680 
"real_of_preal m1 < real_of_preal m2 ==> m1 < m2" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

682 
apply (drule real_of_preal_leD) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

685 

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

686 
lemma real_of_preal_less_iff [simp]: 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

687 
"(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

688 
by (blast intro: real_of_preal_lessI real_of_preal_lessD) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

689 

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

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

691 
"(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

693 

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

694 
lemma real_of_preal_zero_less: "0 < real_of_preal m" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

695 
apply (auto simp add: real_zero_def real_of_preal_def real_less_def real_le_def 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

697 
apply (simp_all add: preal_add_assoc [symmetric] preal_cancels) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

698 
apply (blast intro: preal_self_less_add_left order_less_imp_le) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

699 
apply (insert preal_not_eq_self [of "preal_of_rat 1" m]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

702 

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

703 
lemma real_of_preal_minus_less_zero: " real_of_preal m < 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

705 

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

706 
lemma real_of_preal_not_minus_gt_zero: "~ 0 <  real_of_preal m" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

707 
apply (cut_tac real_of_preal_minus_less_zero) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

708 
apply (fast dest: order_less_trans) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

710 

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

711 

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

712 
subsection{*Theorems About the Ordering*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

713 

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

714 
text{*obsolete but used a lot*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

715 

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

716 
lemma real_not_refl2: "x < y ==> x \<noteq> (y::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

718 

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

719 
lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y  x = y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

721 

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

722 
lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

724 
apply (cut_tac x = x in real_of_preal_trichotomy) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

725 
apply (blast elim!: real_of_preal_not_minus_gt_zero [THEN notE]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

727 

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

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

729 
"real_of_preal z < x ==> \<exists>y. x = real_of_preal y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

730 
by (blast dest!: real_of_preal_zero_less [THEN order_less_trans] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

731 
intro: real_gt_zero_preal_Ex [THEN iffD1]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

732 

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

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

734 
"real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

735 
by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

736 

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

737 
lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

738 
by (auto elim: order_le_imp_less_or_eq [THEN disjE] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

739 
intro: real_of_preal_zero_less [THEN [2] order_less_trans] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

740 
simp add: real_of_preal_zero_less) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

741 

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

742 
lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

743 
by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

744 

14334  745 
lemma real_add_less_le_mono: "[ w'<w; z'\<le>z ] ==> w' + z' < w + (z::real)" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

746 
by (rule Ring_and_Field.add_less_le_mono) 
14334  747 

748 
lemma real_add_le_less_mono: 

749 
"!!z z'::real. [ w'\<le>w; z'<z ] ==> w' + z' < w + z" 

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

750 
by (rule Ring_and_Field.add_le_less_mono) 
14334  751 

752 
lemma real_zero_less_one: "0 < (1::real)" 

753 
by (rule Ring_and_Field.zero_less_one) 

754 

755 
lemma real_le_square [simp]: "(0::real) \<le> x*x" 

756 
by (rule Ring_and_Field.zero_le_square) 

757 

758 

759 
subsection{*More Lemmas*} 

760 

761 
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)" 

762 
by auto 

763 

764 
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)" 

765 
by auto 

766 

767 
text{*The precondition could be weakened to @{term "0\<le>x"}*} 

768 
lemma real_mult_less_mono: 

769 
"[ u<v; x<y; (0::real) < v; 0 < x ] ==> u*x < v* y" 

770 
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) 

771 

772 
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" 

773 
by (force elim: order_less_asym 

774 
simp add: Ring_and_Field.mult_less_cancel_right) 

775 

776 
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" 

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

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

778 
apply (blast intro: elim: order_less_asym) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

779 
done 
14334  780 

781 
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" 

782 
by (force elim: order_less_asym 

783 
simp add: Ring_and_Field.mult_le_cancel_left) 

784 

785 
text{*Only two uses?*} 

786 
lemma real_mult_less_mono': 

787 
"[ x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x] ==> r1 * x < r2 * y" 

788 
by (rule Ring_and_Field.mult_strict_mono') 

789 

790 
text{*FIXME: delete or at least combine the next two lemmas*} 

791 
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" 

792 
apply (drule Ring_and_Field.equals_zero_I [THEN sym]) 

793 
apply (cut_tac x = y in real_le_square) 

794 
apply (auto, drule real_le_anti_sym, auto) 

795 
done 

796 

797 
lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" 

798 
apply (rule_tac y = x in real_sum_squares_cancel) 

799 
apply (simp add: real_add_commute) 

800 
done 

801 

802 
lemma real_add_order: "[ 0 < x; 0 < y ] ==> (0::real) < x + y" 

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

803 
by (drule add_strict_mono [of concl: 0 0], assumption, simp) 
14334  804 

805 
lemma real_le_add_order: "[ 0 \<le> x; 0 \<le> y ] ==> (0::real) \<le> x + y" 

806 
apply (drule order_le_imp_less_or_eq)+ 

807 
apply (auto intro: real_add_order order_less_imp_le) 

808 
done 

809 

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

810 
lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

811 
apply (case_tac "x \<noteq> 0") 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

812 
apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

813 
done 
14334  814 

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

815 
lemma real_inverse_gt_one: "[ (0::real) < x; x < 1 ] ==> 1 < inverse x" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

816 
by (auto dest: less_imp_inverse_less) 
14334  817 

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

818 
lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

820 
have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

821 
thus ?thesis by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

823 

14334  824 

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

825 
subsection{*Embedding the Integers into the Reals*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

826 

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

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

828 
"congruent intrel (%p. (%(i,j). realrel `` 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

829 
{(preal_of_rat (rat (int(Suc i))), preal_of_rat (rat (int(Suc j))))}) p)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

830 
apply (simp add: congruent_def add_ac del: int_Suc, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

831 
(*OPTION raised if only is changed to add?????????*) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

832 
apply (simp only: add_Suc_right zero_less_rat_of_int_iff zadd_int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

833 
preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric], simp) 
14334  834 
done 
835 

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

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

837 
"real (Abs_Integ (intrel `` {(i, j)})) = 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

838 
Abs_REAL(realrel `` 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

839 
{(preal_of_rat (rat (int(Suc i))), 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

840 
preal_of_rat (rat (int(Suc j))))})" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

841 
apply (unfold real_of_int_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

842 
apply (rule_tac f = Abs_REAL in arg_cong) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

843 
apply (simp del: int_Suc 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

844 
add: realrel_in_real [THEN Abs_REAL_inverse] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

845 
UN_equiv_class [OF equiv_intrel real_of_int_congruent]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

847 

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

848 
lemma inj_real_of_int: "inj(real :: int => real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

849 
apply (rule inj_onI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

850 
apply (rule_tac z = x in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

851 
apply (rule_tac z = y in eq_Abs_Integ, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

852 
apply (simp del: int_Suc 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

853 
add: real_of_int zadd_int preal_of_rat_eq_iff 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

854 
preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

856 

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

857 
lemma real_of_int_int_zero: "real (int 0) = 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

858 
by (simp add: int_def real_zero_def real_of_int preal_add_commute) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

859 

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

860 
lemma real_of_int_zero [simp]: "real (0::int) = 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

861 
by (insert real_of_int_int_zero, simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

862 

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

863 
lemma real_of_one [simp]: "real (1::int) = (1::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

864 
apply (subst int_1 [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

865 
apply (simp add: int_def real_one_def) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

866 
apply (simp add: real_of_int preal_of_rat_add [symmetric]) 
14334  867 
done 
868 

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

869 
lemma real_of_int_add: "real (x::int) + real y = real (x + y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

870 
apply (rule_tac z = x in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

871 
apply (rule_tac z = y in eq_Abs_Integ, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

872 
apply (simp del: int_Suc 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

873 
add: pos_add_strict real_of_int real_add zadd 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

874 
preal_of_rat_add [symmetric], simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

876 
declare real_of_int_add [symmetric, simp] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

877 

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

878 
lemma real_of_int_minus: "real (x::int) = real (x)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

879 
apply (rule_tac z = x in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

880 
apply (auto simp add: real_of_int real_minus zminus) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

882 
declare real_of_int_minus [symmetric, simp] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

883 

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

884 
lemma real_of_int_diff: "real (x::int)  real y = real (x  y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

885 
by (simp only: zdiff_def real_diff_def real_of_int_add real_of_int_minus) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

886 
declare real_of_int_diff [symmetric, simp] 
14334  887 

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

888 
lemma real_of_int_mult: "real (x::int) * real y = real (x * y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

889 
apply (rule_tac z = x in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

890 
apply (rule_tac z = y in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

891 
apply (rename_tac a b c d) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

892 
apply (simp del: int_Suc 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

893 
add: pos_add_strict mult_pos real_of_int real_mult zmult 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

894 
preal_of_rat_add [symmetric] preal_of_rat_mult [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

895 
apply (rule_tac f=preal_of_rat in arg_cong) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

896 
apply (simp only: int_Suc right_distrib add_ac mult_ac zadd_int zmult_int 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

897 
rat_of_int_add_distrib [symmetric] rat_of_int_mult_distrib [symmetric] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

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

900 
declare real_of_int_mult [symmetric, simp] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

901 

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

902 
lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

903 
by (simp only: real_of_one [symmetric] zadd_int add_ac int_Suc real_of_int_add) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

904 

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

905 
lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

906 
by (auto intro: inj_real_of_int [THEN injD]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

907 

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

908 
lemma zero_le_real_of_int: "0 \<le> real y ==> 0 \<le> (y::int)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

909 
apply (rule_tac z = y in eq_Abs_Integ) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

911 
apply (rename_tac a b c d) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

912 
apply (simp del: int_Suc zdiff_def [symmetric] 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

913 
add: real_zero_def real_of_int zle_def zless_def zdiff_def zadd 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

914 
zminus neg_def preal_add_ac preal_cancels) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

915 
apply (drule sym, drule preal_eq_le_imp_le, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

916 
apply (simp del: int_Suc add: preal_of_rat_le_iff) 
14334  917 
done 
918 

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

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

920 
assumes le: "real (x::int) \<le> real y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

921 
shows "x \<le> y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

923 
have "real x  real x \<le> real y  real x" using le 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

924 
by (simp only: diff_minus add_le_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

925 
hence "0 \<le> real y  real x" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

926 
hence "0 \<le> y  x" by (simp only: real_of_int_diff zero_le_real_of_int) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

927 
hence "0 + x \<le> (y  x) + x" by (simp only: add_le_cancel_right) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

928 
thus "x \<le> y" by simp 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

930 

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

931 
lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

932 
by (blast dest!: inj_real_of_int [THEN injD]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

933 

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

934 
lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

936 

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

937 
lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

939 
apply (auto dest!: real_of_int_less_cancel simp add: order_le_less) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

941 

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

942 
lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

943 
by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

944 

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

945 
lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

947 

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

948 

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

949 
subsection{*Embedding the Naturals into the Reals*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

950 

14334  951 
lemma real_of_nat_zero [simp]: "real (0::nat) = 0" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

952 
by (simp add: real_of_nat_def) 
14334  953 

954 
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" 

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

955 
by (simp add: real_of_nat_def) 
14334  956 

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

957 
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

958 
by (simp add: real_of_nat_def add_ac) 
14334  959 

960 
(*Not for addsimps: often the LHS is used to represent a positive natural*) 

961 
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" 

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

962 
by (simp add: real_of_nat_def add_ac) 
14334  963 

964 
lemma real_of_nat_less_iff [iff]: 

965 
"(real (n::nat) < real m) = (n < m)" 

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

966 
by (simp add: real_of_nat_def) 
14334  967 

968 
lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)" 

969 
by (simp add: linorder_not_less [symmetric]) 

970 

971 
lemma inj_real_of_nat: "inj (real :: nat => real)" 

972 
apply (rule inj_onI) 

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

973 
apply (simp add: real_of_nat_def) 
14334  974 
done 
975 

976 
lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)" 

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

977 
apply (insert real_of_int_le_iff [of 0 "int n"]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

978 
apply (simp add: real_of_nat_def) 
14334  979 
done 
980 

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

981 
lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

982 
by (insert real_of_nat_less_iff [of 0 "Suc n"], simp) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

983 

14334  984 
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

985 
by (simp add: real_of_nat_def zmult_int [symmetric]) 
14334  986 

987 
lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" 

988 
by (auto dest: inj_real_of_nat [THEN injD]) 

989 

990 
lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)" 

991 
proof 

992 
assume "real n = 0" 

993 
have "real n = real (0::nat)" by simp 

994 
then show "n = 0" by (simp only: real_of_nat_inject) 

995 
next 

996 
show "n = 0 \<Longrightarrow> real n = 0" by simp 

997 
qed 

998 

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

999 
lemma real_of_nat_diff: "n \<le> m ==> real (m  n) = real (m::nat)  real n" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1000 
by (simp add: real_of_nat_def zdiff_int [symmetric]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1001 

14334  1002 
lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0" 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1003 
by (simp add: neg_nat) 
14334  1004 

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

1005 
lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1006 
by (rule real_of_nat_less_iff [THEN subst], auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1007 

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

1008 
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

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

1010 
apply (simp only: real_of_nat_le_iff, simp) 
14334  1011 
done 
1012 

1013 

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

1014 
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1015 
by (simp add: linorder_not_less real_of_nat_ge_zero) 
14334  1016 

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

1017 
lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1018 
by (simp add: linorder_not_less) 
14334  1019 

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

1020 
text{*Now obsolete, but used in Hyperreal/IntFloor???*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1021 
lemma real_of_int_real_of_nat: "real (int n) = real n" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1022 
by (simp add: real_of_nat_def) 
14334  1023 

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

1024 
lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1025 
by (simp add: not_neg_eq_ge_0 real_of_nat_def) 
14334  1026 

1027 
ML 

1028 
{* 

1029 
val real_abs_def = thm "real_abs_def"; 

1030 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1031 
val real_le_def = thm "real_le_def"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1032 
val real_diff_def = thm "real_diff_def"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1033 
val real_divide_def = thm "real_divide_def"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1034 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1035 
val preal_trans_lemma = thm"preal_trans_lemma"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1036 
val realrel_iff = thm"realrel_iff"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1037 
val realrel_refl = thm"realrel_refl"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1038 
val equiv_realrel = thm"equiv_realrel"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1039 
val equiv_realrel_iff = thm"equiv_realrel_iff"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1040 
val realrel_in_real = thm"realrel_in_real"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1041 
val inj_on_Abs_REAL = thm"inj_on_Abs_REAL"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1042 
val eq_realrelD = thm"eq_realrelD"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1043 
val inj_Rep_REAL = thm"inj_Rep_REAL"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1044 
val inj_real_of_preal = thm"inj_real_of_preal"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1045 
val eq_Abs_REAL = thm"eq_Abs_REAL"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1046 
val real_minus_congruent = thm"real_minus_congruent"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1047 
val real_minus = thm"real_minus"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1048 
val real_add = thm"real_add"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1049 
val real_add_commute = thm"real_add_commute"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1050 
val real_add_assoc = thm"real_add_assoc"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1051 
val real_add_zero_left = thm"real_add_zero_left"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1052 
val real_add_zero_right = thm"real_add_zero_right"; 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset

1053 

14334  1054 
val real_mult = thm"real_mult"; 
1055 
val real_mult_commute = thm"real_mult_commute"; 

1056 
val real_mult_assoc = thm"real_mult_assoc"; 

1057 
val real_mult_1 = thm"real_mult_1"; 

1058 
val real_mult_1_right = thm"real_mult_1_right"; 

1059 
val preal_le_linear = thm"preal_le_linear"; 

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

1060 
val real_mult_inverse_left = thm"real_mult_inverse_left"; 
14334  1061 
val real_not_refl2 = thm"real_not_refl2"; 
1062 
val real_of_preal_add = thm"real_of_preal_add"; 

1063 
val real_of_preal_mult = thm"real_of_preal_mult"; 

1064 
val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; 

1065 
val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; 

1066 
val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; 

1067 
val real_of_preal_zero_less = thm"real_of_preal_zero_less"; 

1068 
val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; 

1069 
val real_le_refl = thm"real_le_refl"; 

1070 
val real_le_linear = thm"real_le_linear"; 

1071 
val real_le_trans = thm"real_le_trans"; 

1072 
val real_le_anti_sym = thm"real_le_anti_sym"; 

1073 
val real_less_le = thm"real_less_le"; 

1074 
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; 

1075 
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex"; 

1076 
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex"; 

1077 
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex"; 

1078 
val real_less_all_preal = thm "real_less_all_preal"; 

1079 
val real_less_all_real2 = thm "real_less_all_real2"; 

1080 
val real_of_preal_le_iff = thm "real_of_preal_le_iff"; 

1081 
val real_mult_order = thm "real_mult_order"; 

1082 
val real_zero_less_one = thm "real_zero_less_one"; 

1083 
val real_add_less_le_mono = thm "real_add_less_le_mono"; 

1084 
val real_add_le_less_mono = thm "real_add_le_less_mono"; 

1085 
val real_add_order = thm "real_add_order"; 

1086 
val real_le_add_order = thm "real_le_add_order"; 

1087 
val real_le_square = thm "real_le_square"; 

1088 
val real_mult_less_mono2 = thm "real_mult_less_mono2"; 

1089 

1090 
val real_mult_less_iff1 = thm "real_mult_less_iff1"; 

1091 
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; 

1092 
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; 

1093 
val real_mult_less_mono = thm "real_mult_less_mono"; 

1094 
val real_mult_less_mono' = thm "real_mult_less_mono'"; 

1095 
val real_sum_squares_cancel = thm "real_sum_squares_cancel"; 

1096 
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; 

1097 

1098 
val real_mult_left_cancel = thm"real_mult_left_cancel"; 

1099 
val real_mult_right_cancel = thm"real_mult_right_cancel"; 

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

1100 
val real_inverse_unique = thm "real_inverse_unique"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1101 
val real_inverse_gt_one = thm "real_inverse_gt_one"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1102 

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

1103 
val real_of_int = thm"real_of_int"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1104 
val inj_real_of_int = thm"inj_real_of_int"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1105 
val real_of_int_zero = thm"real_of_int_zero"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1106 
val real_of_one = thm"real_of_one"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1107 
val real_of_int_add = thm"real_of_int_add"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1108 
val real_of_int_minus = thm"real_of_int_minus"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1109 
val real_of_int_diff = thm"real_of_int_diff"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1110 
val real_of_int_mult = thm"real_of_int_mult"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1111 
val real_of_int_Suc = thm"real_of_int_Suc"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1112 
val real_of_int_real_of_nat = thm"real_of_int_real_of_nat"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1113 
val real_of_nat_real_of_int = thm"real_of_nat_real_of_int"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1114 
val real_of_int_less_cancel = thm"real_of_int_less_cancel"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1115 
val real_of_int_inject = thm"real_of_int_inject"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1116 
val real_of_int_less_mono = thm"real_of_int_less_mono"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1117 
val real_of_int_less_iff = thm"real_of_int_less_iff"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14348
diff
changeset

1118 
val real_of_int_le_iff = thm"real_of_int_le_iff"; 
14334  1119 
val real_of_nat_zero = thm "real_of_nat_zero"; 
1120 
val real_of_nat_one = thm "real_of_nat_one"; 

1121 
val real_of_nat_add = thm "real_of_nat_add"; 

1122 
val real_of_nat_Suc = thm "real_of_nat_Suc"; 

1123 
val real_of_nat_less_iff = thm "real_of_nat_less_iff"; 

1124 
val real_of_nat_le_iff = thm "real_of_nat_le_iff"; 

1125 
val inj_real_of_nat = thm "inj_real_of_nat"; 

1126 
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; 

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

1127 
val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero"; 
14334  1128 
val real_of_nat_mult = thm "real_of_nat_mult"; 
1129 
val real_of_nat_inject = thm "real_of_nat_inject"; 

1130 
val real_of_nat_diff = thm "real_of_nat_diff"; 

1131 
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; 

1132 
val real_of_nat_neg_int = thm "real_of_nat_neg_int"; 

1133 
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; 

1134 
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; 

1135 
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; 

1136 
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; 

1137 
*} 

10752
c4f1bf2acf4c
tidying, and separation of HOLHyperreal from HOLReal
paulson
parents:
10648
diff
changeset

1138 

5588  1139 
end 