author  paulson 
Thu, 01 Jan 2004 21:47:07 +0100  
changeset 14335  9c0b5e081037 
parent 14334  6137d24eef79 
child 14341  a09441bd4f1e 
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: 
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

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

39 
preal_of_prat(prat_of_pnat 1))})" 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

40 

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

42 
"1 == Abs_REAL(realrel`` 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

43 
{(preal_of_prat(prat_of_pnat 1) + preal_of_prat(prat_of_pnat 1), 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

44 
preal_of_prat(prat_of_pnat 1))})" 
5588  45 

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

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

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

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

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

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

5588  58 
constdefs 
59 

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

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

62 
real_of_preal :: "preal => real" 

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

63 
"real_of_preal m == 
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

64 
Abs_REAL(realrel``{(m + preal_of_prat(prat_of_pnat 1), 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset

65 
preal_of_prat(prat_of_pnat 1))})" 
5588  66 

14269  67 
real_of_posnat :: "nat => real" 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

68 
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5787
diff
changeset

69 

5588  70 

14269  71 
defs (overloaded) 
5588  72 

14269  73 
real_of_nat_def: "real n == real_of_posnat n + ( 1)" 
10919
144ede948e58
renamings: real_of_nat, real_of_int > (overloaded) real
paulson
parents:
10834
diff
changeset

74 

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

79 
real_mult_def: 

14329  80 
"P*Q == Abs_REAL(\<Union>p1\<in>Rep_REAL(P). \<Union>p2\<in>Rep_REAL(Q). 
10834  81 
(%(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

82 
p2) p1)" 
5588  83 

14269  84 
real_less_def: 
85 
"P<Q == \<exists>x1 y1 x2 y2. x1 + y2 < x2 + y1 & 

14329  86 
(x1,y1)\<in>Rep_REAL(P) & (x2,y2)\<in>Rep_REAL(Q)" 
14269  87 
real_le_def: 
88 
"P \<le> (Q::real) == ~(Q < P)" 

5588  89 

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

92 

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

93 
syntax (xsymbols) 
14269  94 
Reals :: "'a set" ("\<real>") 
95 
Nats :: "'a set" ("\<nat>") 

96 

97 

14329  98 
subsection{*Proving that realrel is an equivalence relation*} 
14269  99 

14270  100 
lemma preal_trans_lemma: 
101 
"[ (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 ] 

14269  102 
==> x1 + y3 = x3 + y1" 
103 
apply (rule_tac C = y2 in preal_add_right_cancel) 

104 
apply (rotate_tac 1, drule sym) 

105 
apply (simp add: preal_add_ac) 

106 
apply (rule preal_add_left_commute [THEN subst]) 

107 
apply (rule_tac x1 = x1 in preal_add_assoc [THEN subst]) 

108 
apply (simp add: preal_add_ac) 

109 
done 

110 

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

112 
by (unfold realrel_def, blast) 

113 

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

115 
apply (case_tac "x") 

116 
apply (simp add: realrel_def) 

117 
done 

118 

119 
lemma equiv_realrel: "equiv UNIV realrel" 

120 
apply (unfold equiv_def refl_def sym_def trans_def realrel_def) 

121 
apply (fast elim!: sym preal_trans_lemma) 

122 
done 

123 

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

125 
lemmas equiv_realrel_iff = 

126 
eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I] 

127 

128 
declare equiv_realrel_iff [simp] 

129 

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

131 
by (unfold REAL_def realrel_def quotient_def, blast) 

132 

133 
lemma inj_on_Abs_REAL: "inj_on Abs_REAL REAL" 

134 
apply (rule inj_on_inverseI) 

135 
apply (erule Abs_REAL_inverse) 

136 
done 

137 

138 
declare inj_on_Abs_REAL [THEN inj_on_iff, simp] 

139 
declare Abs_REAL_inverse [simp] 

140 

141 

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

143 

144 
lemma inj_Rep_REAL: "inj Rep_REAL" 

145 
apply (rule inj_on_inverseI) 

146 
apply (rule Rep_REAL_inverse) 

147 
done 

148 

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

150 
lemma inj_real_of_preal: "inj(real_of_preal)" 

151 
apply (rule inj_onI) 

152 
apply (unfold real_of_preal_def) 

153 
apply (drule inj_on_Abs_REAL [THEN inj_onD]) 

154 
apply (rule realrel_in_real)+ 

155 
apply (drule eq_equiv_class) 

156 
apply (rule equiv_realrel, blast) 

157 
apply (simp add: realrel_def) 

158 
done 

159 

160 
lemma eq_Abs_REAL: 

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

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

163 
apply (drule_tac f = Abs_REAL in arg_cong) 

164 
apply (case_tac "x") 

165 
apply (simp add: Rep_REAL_inverse) 

166 
done 

167 

168 

14329  169 
subsection{*Congruence property for addition*} 
14269  170 

171 
lemma real_add_congruent2_lemma: 

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

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

174 
apply (simp add: preal_add_assoc) 

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

176 
apply (simp add: preal_add_assoc [symmetric]) 

177 
apply (simp add: preal_add_ac) 

178 
done 

179 

180 
lemma real_add: 

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

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

183 
apply (simp add: real_add_def UN_UN_split_split_eq) 

184 
apply (subst equiv_realrel [THEN UN_equiv_class2]) 

185 
apply (auto simp add: congruent2_def) 

186 
apply (blast intro: real_add_congruent2_lemma) 

187 
done 

188 

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

190 
apply (rule_tac z = z in eq_Abs_REAL) 

191 
apply (rule_tac z = w in eq_Abs_REAL) 

192 
apply (simp add: preal_add_ac real_add) 

193 
done 

194 

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

196 
apply (rule_tac z = z1 in eq_Abs_REAL) 

197 
apply (rule_tac z = z2 in eq_Abs_REAL) 

198 
apply (rule_tac z = z3 in eq_Abs_REAL) 

199 
apply (simp add: real_add preal_add_assoc) 

200 
done 

201 

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

203 
apply (unfold real_of_preal_def real_zero_def) 

204 
apply (rule_tac z = z in eq_Abs_REAL) 

205 
apply (simp add: real_add preal_add_ac) 

206 
done 

207 

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

14334  209 
by (simp add: real_add_zero_left real_add_commute) 
14269  210 

211 
instance real :: plus_ac0 

212 
by (intro_classes, 

213 
(assumption  

214 
rule real_add_commute real_add_assoc real_add_zero_left)+) 

215 

216 

14334  217 
subsection{*Additive Inverse on real*} 
218 

219 
lemma real_minus_congruent: 

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

221 
apply (unfold congruent_def, clarify) 

222 
apply (simp add: preal_add_commute) 

223 
done 

224 

225 
lemma real_minus: 

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

227 
apply (unfold real_minus_def) 

228 
apply (rule_tac f = Abs_REAL in arg_cong) 

229 
apply (simp add: realrel_in_real [THEN Abs_REAL_inverse] 

230 
UN_equiv_class [OF equiv_realrel real_minus_congruent]) 

231 
done 

232 

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

14269  234 
apply (unfold real_zero_def) 
235 
apply (rule_tac z = z in eq_Abs_REAL) 

236 
apply (simp add: real_minus real_add preal_add_commute) 

237 
done 

238 

239 

14329  240 
subsection{*Congruence property for multiplication*} 
14269  241 

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

14269  244 
x * x1 + y * y1 + (x * y2 + x2 * y) = 
245 
x * x2 + y * y2 + (x * y1 + x1 * y)" 

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

247 
apply (rule preal_mult_commute [THEN subst]) 

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

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

250 
apply (simp add: preal_add_commute) 

251 
done 

252 

253 
lemma real_mult_congruent2: 

254 
"congruent2 realrel (%p1 p2. 

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

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

257 
apply (unfold split_def) 

258 
apply (simp add: preal_mult_commute preal_add_commute) 

259 
apply (auto simp add: real_mult_congruent2_lemma) 

260 
done 

261 

262 
lemma real_mult: 

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

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

265 
apply (unfold real_mult_def) 

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

267 
done 

268 

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

270 
apply (rule_tac z = z in eq_Abs_REAL) 

271 
apply (rule_tac z = w in eq_Abs_REAL) 

272 
apply (simp add: real_mult preal_add_ac preal_mult_ac) 

273 
done 

274 

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

276 
apply (rule_tac z = z1 in eq_Abs_REAL) 

277 
apply (rule_tac z = z2 in eq_Abs_REAL) 

278 
apply (rule_tac z = z3 in eq_Abs_REAL) 

279 
apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac) 

280 
done 

281 

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

283 
apply (unfold real_one_def pnat_one_def) 

284 
apply (rule_tac z = z in eq_Abs_REAL) 

14334  285 
apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right 
286 
preal_mult_ac preal_add_ac) 

14269  287 
done 
288 

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

290 
apply (rule_tac z = z1 in eq_Abs_REAL) 

291 
apply (rule_tac z = z2 in eq_Abs_REAL) 

292 
apply (rule_tac z = w in eq_Abs_REAL) 

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

294 
done 

295 

14329  296 
text{*one and zero are distinct*} 
14269  297 
lemma real_zero_not_eq_one: "0 ~= (1::real)" 
298 
apply (unfold real_zero_def real_one_def) 

299 
apply (auto simp add: preal_self_less_add_left [THEN preal_not_refl2]) 

300 
done 

301 

14329  302 
subsection{*existence of inverse*} 
14269  303 
(** lemma  alternative definition of 0 **) 
304 
lemma real_zero_iff: "0 = Abs_REAL (realrel `` {(x, x)})" 

305 
apply (unfold real_zero_def) 

306 
apply (auto simp add: preal_add_commute) 

307 
done 

308 

14334  309 
lemma real_mult_inv_left_ex: "x ~= 0 ==> \<exists>y. y*x = (1::real)" 
14269  310 
apply (unfold real_zero_def real_one_def) 
311 
apply (rule_tac z = x in eq_Abs_REAL) 

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

313 
apply (auto dest!: preal_less_add_left_Ex simp add: real_zero_iff [symmetric]) 

14334  314 
apply (rule_tac 
315 
x = "Abs_REAL (realrel `` { (preal_of_prat (prat_of_pnat 1), 

316 
pinv (D) + preal_of_prat (prat_of_pnat 1))}) " 

317 
in exI) 

318 
apply (rule_tac [2] 

319 
x = "Abs_REAL (realrel `` { (pinv (D) + preal_of_prat (prat_of_pnat 1), 

320 
preal_of_prat (prat_of_pnat 1))})" 

321 
in exI) 

14329  322 
apply (auto simp add: real_mult pnat_one_def preal_mult_1_right 
323 
preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 

324 
preal_mult_inv_right preal_add_ac preal_mult_ac) 

14269  325 
done 
326 

327 
lemma real_mult_inv_left: "x ~= 0 ==> inverse(x)*x = (1::real)" 

328 
apply (unfold real_inverse_def) 

329 
apply (frule real_mult_inv_left_ex, safe) 

330 
apply (rule someI2, auto) 

331 
done 

14334  332 

333 
instance real :: field 

334 
proof 

335 
fix x y z :: real 

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

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

338 
show "0 + x = x" by simp 

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

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

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

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

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

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

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

346 
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inv_left) 

347 
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) 

348 
qed 

349 

350 

351 
(** Inverse of zero! Useful to simplify certain equations **) 

14269  352 

14334  353 
lemma INVERSE_ZERO: "inverse 0 = (0::real)" 
354 
apply (unfold real_inverse_def) 

355 
apply (rule someI2) 

356 
apply (auto simp add: zero_neq_one) 

14269  357 
done 
14334  358 

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

360 
by (simp add: real_divide_def INVERSE_ZERO) 

361 

362 
instance real :: division_by_zero 

363 
proof 

364 
fix x :: real 

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

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

367 
qed 

368 

369 

370 
(*Pull negations out*) 

371 
declare minus_mult_right [symmetric, simp] 

372 
minus_mult_left [symmetric, simp] 

373 

374 
text{*Used in RealBin*} 

375 
lemma real_minus_mult_commute: "(x) * y = x * ( y :: real)" 

376 
by simp 

377 

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

379 
by (rule Ring_and_Field.mult_1_right) 

14269  380 

381 

14329  382 
subsection{*Theorems for Ordering*} 
383 

384 
(* real_less is a strict order: irreflexive *) 

14269  385 

14329  386 
text{*lemmas*} 
387 
lemma preal_lemma_eq_rev_sum: 

388 
"!!(x::preal). [ x = y; x1 = y1 ] ==> x + y1 = x1 + y" 

14269  389 
by (simp add: preal_add_commute) 
390 

14329  391 
lemma preal_add_left_commute_cancel: 
392 
"!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1" 

14269  393 
by (simp add: preal_add_ac) 
394 

14329  395 
lemma preal_lemma_for_not_refl: 
396 
"!!(x::preal). [ x + y2a = x2a + y; 

14269  397 
x + y2b = x2b + y ] 
398 
==> x2a + y2b = x2b + y2a" 

399 
apply (drule preal_lemma_eq_rev_sum, assumption) 

400 
apply (erule_tac V = "x + y2b = x2b + y" in thin_rl) 

401 
apply (simp add: preal_add_ac) 

402 
apply (drule preal_add_left_commute_cancel) 

403 
apply (simp add: preal_add_ac) 

404 
done 

405 

406 
lemma real_less_not_refl: "~ (R::real) < R" 

407 
apply (rule_tac z = R in eq_Abs_REAL) 

408 
apply (auto simp add: real_less_def) 

409 
apply (drule preal_lemma_for_not_refl, assumption, auto) 

410 
done 

411 

412 
(*** y < y ==> P ***) 

413 
lemmas real_less_irrefl = real_less_not_refl [THEN notE, standard] 

414 
declare real_less_irrefl [elim!] 

415 

416 
lemma real_not_refl2: "!!(x::real). x < y ==> x ~= y" 

417 
by (auto simp add: real_less_not_refl) 

418 

419 
(* lemma rearranging and eliminating terms *) 

420 
lemma preal_lemma_trans: "!! (a::preal). [ a + b = c + d; 

421 
x2b + d + (c + y2e) < a + y2b + (x2e + b) ] 

422 
==> x2b + y2e < x2e + y2b" 

423 
apply (simp add: preal_add_ac) 

424 
apply (rule_tac C = "c+d" in preal_add_left_less_cancel) 

425 
apply (simp add: preal_add_assoc [symmetric]) 

426 
done 

427 

428 
(** A MESS! heavy rewriting involved*) 

429 
lemma real_less_trans: "!!(R1::real). [ R1 < R2; R2 < R3 ] ==> R1 < R3" 

430 
apply (rule_tac z = R1 in eq_Abs_REAL) 

431 
apply (rule_tac z = R2 in eq_Abs_REAL) 

432 
apply (rule_tac z = R3 in eq_Abs_REAL) 

433 
apply (auto simp add: real_less_def) 

434 
apply (rule exI)+ 

435 
apply (rule conjI, rule_tac [2] conjI) 

436 
prefer 2 apply blast 

437 
prefer 2 apply blast 

438 
apply (drule preal_lemma_for_not_refl, assumption) 

439 
apply (blast dest: preal_add_less_mono intro: preal_lemma_trans) 

440 
done 

441 

442 
lemma real_less_not_sym: "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)" 

443 
apply (rule notI) 

444 
apply (drule real_less_trans, assumption) 

445 
apply (simp add: real_less_not_refl) 

446 
done 

447 

448 
(* [ x < y; ~P ==> y < x ] ==> P *) 

449 
lemmas real_less_asym = real_less_not_sym [THEN contrapos_np, standard] 

450 

451 
lemma real_of_preal_add: 

452 
"real_of_preal ((z1::preal) + z2) = 

453 
real_of_preal z1 + real_of_preal z2" 

454 
apply (unfold real_of_preal_def) 

455 
apply (simp add: real_add preal_add_mult_distrib preal_mult_1 add: preal_add_ac) 

456 
done 

457 

458 
lemma real_of_preal_mult: 

459 
"real_of_preal ((z1::preal) * z2) = 

460 
real_of_preal z1* real_of_preal z2" 

461 
apply (unfold real_of_preal_def) 

462 
apply (simp (no_asm_use) add: real_mult preal_add_mult_distrib2 preal_mult_1 preal_mult_1_right pnat_one_def preal_add_ac preal_mult_ac) 

463 
done 

464 

465 
lemma real_of_preal_ExI: 

466 
"!!(x::preal). y < x ==> 

467 
\<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m" 

468 
apply (unfold real_of_preal_def) 

469 
apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac) 

470 
done 

471 

472 
lemma real_of_preal_ExD: 

473 
"!!(x::preal). \<exists>m. Abs_REAL (realrel `` {(x,y)}) = 

474 
real_of_preal m ==> y < x" 

475 
apply (unfold real_of_preal_def) 

476 
apply (auto simp add: preal_add_commute preal_add_assoc) 

477 
apply (simp add: preal_add_assoc [symmetric] preal_self_less_add_left) 

478 
done 

479 

14329  480 
lemma real_of_preal_iff: 
481 
"(\<exists>m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)" 

14269  482 
by (blast intro!: real_of_preal_ExI real_of_preal_ExD) 
483 

14329  484 
text{*Gleason prop 94.4 p 127*} 
14269  485 
lemma real_of_preal_trichotomy: 
486 
"\<exists>m. (x::real) = real_of_preal m  x = 0  x = (real_of_preal m)" 

487 
apply (unfold real_of_preal_def real_zero_def) 

488 
apply (rule_tac z = x in eq_Abs_REAL) 

489 
apply (auto simp add: real_minus preal_add_ac) 

490 
apply (cut_tac x = x and y = y in linorder_less_linear) 

491 
apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc [symmetric]) 

492 
apply (auto simp add: preal_add_commute) 

493 
done 

494 

14329  495 
lemma real_of_preal_trichotomyE: 
496 
"!!P. [ !!m. x = real_of_preal m ==> P; 

14269  497 
x = 0 ==> P; 
498 
!!m. x = (real_of_preal m) ==> P ] ==> P" 

499 
apply (cut_tac x = x in real_of_preal_trichotomy, auto) 

500 
done 

501 

502 
lemma real_of_preal_lessD: 

503 
"real_of_preal m1 < real_of_preal m2 ==> m1 < m2" 

504 
apply (unfold real_of_preal_def) 

505 
apply (auto simp add: real_less_def preal_add_ac) 

506 
apply (auto simp add: preal_add_assoc [symmetric]) 

507 
apply (auto simp add: preal_add_ac) 

508 
done 

509 

510 
lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2" 

511 
apply (drule preal_less_add_left_Ex) 

512 
apply (auto simp add: real_of_preal_add real_of_preal_def real_less_def) 

513 
apply (rule exI)+ 

514 
apply (rule conjI, rule_tac [2] conjI) 

515 
apply (rule_tac [2] refl)+ 

516 
apply (simp add: preal_self_less_add_left del: preal_add_less_iff2) 

517 
done 

518 

14329  519 
lemma real_of_preal_less_iff1: 
520 
"(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" 

14269  521 
by (blast intro: real_of_preal_lessI real_of_preal_lessD) 
522 

523 
declare real_of_preal_less_iff1 [simp] 

524 

525 
lemma real_of_preal_minus_less_self: " real_of_preal m < real_of_preal m" 

526 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

527 
apply (rule exI)+ 

528 
apply (rule conjI, rule_tac [2] conjI) 

529 
apply (rule_tac [2] refl)+ 

530 
apply (simp (no_asm_use) add: preal_add_ac) 

531 
apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric]) 

532 
done 

533 

534 
lemma real_of_preal_minus_less_zero: " real_of_preal m < 0" 

535 
apply (unfold real_zero_def) 

536 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

537 
apply (rule exI)+ 

538 
apply (rule conjI, rule_tac [2] conjI) 

539 
apply (rule_tac [2] refl)+ 

540 
apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac) 

541 
done 

542 

543 
lemma real_of_preal_not_minus_gt_zero: "~ 0 <  real_of_preal m" 

544 
apply (cut_tac real_of_preal_minus_less_zero) 

545 
apply (fast dest: real_less_trans elim: real_less_irrefl) 

546 
done 

547 

548 
lemma real_of_preal_zero_less: "0 < real_of_preal m" 

549 
apply (unfold real_zero_def) 

550 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

551 
apply (rule exI)+ 

552 
apply (rule conjI, rule_tac [2] conjI) 

553 
apply (rule_tac [2] refl)+ 

554 
apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_ac) 

555 
done 

556 

557 
lemma real_of_preal_not_less_zero: "~ real_of_preal m < 0" 

558 
apply (cut_tac real_of_preal_zero_less) 

559 
apply (blast dest: real_less_trans elim: real_less_irrefl) 

560 
done 

561 

562 
lemma real_minus_minus_zero_less: "0 <  ( real_of_preal m)" 

563 
by (simp add: real_of_preal_zero_less) 

564 

565 
(* another lemma *) 

566 
lemma real_of_preal_sum_zero_less: 

567 
"0 < real_of_preal m + real_of_preal m1" 

568 
apply (unfold real_zero_def) 

569 
apply (auto simp add: real_of_preal_def real_less_def real_add) 

570 
apply (rule exI)+ 

571 
apply (rule conjI, rule_tac [2] conjI) 

572 
apply (rule_tac [2] refl)+ 

573 
apply (simp (no_asm_use) add: preal_add_ac) 

574 
apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric]) 

575 
done 

576 

577 
lemma real_of_preal_minus_less_all: " real_of_preal m < real_of_preal m1" 

578 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

579 
apply (rule exI)+ 

580 
apply (rule conjI, rule_tac [2] conjI) 

581 
apply (rule_tac [2] refl)+ 

582 
apply (simp (no_asm_use) add: preal_add_ac) 

583 
apply (simp (no_asm_use) add: preal_self_less_add_right preal_add_assoc [symmetric]) 

584 
done 

585 

586 
lemma real_of_preal_not_minus_gt_all: "~ real_of_preal m <  real_of_preal m1" 

587 
apply (cut_tac real_of_preal_minus_less_all) 

588 
apply (blast dest: real_less_trans elim: real_less_irrefl) 

589 
done 

590 

14329  591 
lemma real_of_preal_minus_less_rev1: 
592 
" real_of_preal m1 <  real_of_preal m2 

14269  593 
==> real_of_preal m2 < real_of_preal m1" 
594 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

595 
apply (rule exI)+ 

596 
apply (rule conjI, rule_tac [2] conjI) 

597 
apply (rule_tac [2] refl)+ 

598 
apply (auto simp add: preal_add_ac) 

599 
apply (simp add: preal_add_assoc [symmetric]) 

600 
apply (auto simp add: preal_add_ac) 

601 
done 

602 

14329  603 
lemma real_of_preal_minus_less_rev2: 
604 
"real_of_preal m1 < real_of_preal m2 

14269  605 
==>  real_of_preal m2 <  real_of_preal m1" 
606 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

607 
apply (rule exI)+ 

608 
apply (rule conjI, rule_tac [2] conjI) 

609 
apply (rule_tac [2] refl)+ 

610 
apply (auto simp add: preal_add_ac) 

611 
apply (simp add: preal_add_assoc [symmetric]) 

612 
apply (auto simp add: preal_add_ac) 

613 
done 

614 

14329  615 
lemma real_of_preal_minus_less_rev_iff: 
616 
"( real_of_preal m1 <  real_of_preal m2) = 

14269  617 
(real_of_preal m2 < real_of_preal m1)" 
618 
apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2) 

619 
done 

620 

14270  621 

622 
subsection{*Linearity of the Ordering*} 

623 

14269  624 
lemma real_linear: "(x::real) < y  x = y  y < x" 
625 
apply (rule_tac x = x in real_of_preal_trichotomyE) 

626 
apply (rule_tac [!] x = y in real_of_preal_trichotomyE) 

14270  627 
apply (auto dest!: preal_le_anti_sym 
628 
simp add: preal_less_le_iff real_of_preal_minus_less_zero 

14334  629 
real_of_preal_zero_less real_of_preal_minus_less_all 
630 
real_of_preal_minus_less_rev_iff) 

14269  631 
done 
632 

633 
lemma real_neq_iff: "!!w::real. (w ~= z) = (w<z  z<w)" 

634 
by (cut_tac real_linear, blast) 

635 

636 

14329  637 
lemma real_linear_less2: 
638 
"!!(R1::real). [ R1 < R2 ==> P; R1 = R2 ==> P; 

14269  639 
R2 < R1 ==> P ] ==> P" 
640 
apply (cut_tac x = R1 and y = R2 in real_linear, auto) 

641 
done 

642 

643 
lemma real_minus_zero_less_iff: "(0 < R) = (R < (0::real))" 

644 
apply (rule_tac x = R in real_of_preal_trichotomyE) 

645 
apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero) 

646 
done 

647 
declare real_minus_zero_less_iff [simp] 

648 

649 
lemma real_minus_zero_less_iff2: "(R < 0) = ((0::real) < R)" 

650 
apply (rule_tac x = R in real_of_preal_trichotomyE) 

651 
apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero) 

652 
done 

653 
declare real_minus_zero_less_iff2 [simp] 

654 

655 
ML 

656 
{* 

657 
val real_le_def = thm "real_le_def"; 

658 
val real_diff_def = thm "real_diff_def"; 

659 
val real_divide_def = thm "real_divide_def"; 

660 
val real_of_nat_def = thm "real_of_nat_def"; 

661 

662 
val preal_trans_lemma = thm"preal_trans_lemma"; 

663 
val realrel_iff = thm"realrel_iff"; 

664 
val realrel_refl = thm"realrel_refl"; 

665 
val equiv_realrel = thm"equiv_realrel"; 

666 
val equiv_realrel_iff = thm"equiv_realrel_iff"; 

667 
val realrel_in_real = thm"realrel_in_real"; 

668 
val inj_on_Abs_REAL = thm"inj_on_Abs_REAL"; 

669 
val eq_realrelD = thm"eq_realrelD"; 

670 
val inj_Rep_REAL = thm"inj_Rep_REAL"; 

671 
val inj_real_of_preal = thm"inj_real_of_preal"; 

672 
val eq_Abs_REAL = thm"eq_Abs_REAL"; 

673 
val real_minus_congruent = thm"real_minus_congruent"; 

674 
val real_minus = thm"real_minus"; 

675 
val real_add = thm"real_add"; 

676 
val real_add_commute = thm"real_add_commute"; 

677 
val real_add_assoc = thm"real_add_assoc"; 

678 
val real_add_zero_left = thm"real_add_zero_left"; 

679 
val real_add_zero_right = thm"real_add_zero_right"; 

680 

681 
*} 

682 

14334  683 
subsection{*Properties of LessThan Or Equals*} 
684 

685 
lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y  x = y" 

686 
apply (unfold real_le_def) 

687 
apply (cut_tac real_linear) 

688 
apply (blast elim: real_less_irrefl real_less_asym) 

689 
done 

690 

691 
lemma real_less_or_eq_imp_le: "z<w  z=w ==> z \<le>(w::real)" 

692 
apply (unfold real_le_def) 

693 
apply (cut_tac real_linear) 

694 
apply (fast elim: real_less_irrefl real_less_asym) 

695 
done 

696 

697 
lemma real_le_less: "(x \<le> (y::real)) = (x < y  x=y)" 

698 
by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq) 

699 

700 
lemma real_le_refl: "w \<le> (w::real)" 

701 
by (simp add: real_le_less) 

702 

703 
lemma real_le_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> (k::real)" 

704 
apply (drule real_le_imp_less_or_eq) 

705 
apply (drule real_le_imp_less_or_eq) 

706 
apply (rule real_less_or_eq_imp_le) 

707 
apply (blast intro: real_less_trans) 

708 
done 

709 

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

711 
apply (drule real_le_imp_less_or_eq) 

712 
apply (drule real_le_imp_less_or_eq) 

713 
apply (fast elim: real_less_irrefl real_less_asym) 

714 
done 

715 

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

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

718 
apply (simp add: real_le_def real_neq_iff) 

719 
apply (blast elim!: real_less_asym) 

720 
done 

721 

722 
instance real :: order 

723 
by (intro_classes, 

724 
(assumption  

725 
rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) 

726 

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

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

729 
apply (simp add: real_le_less) 

730 
apply (cut_tac real_linear, blast) 

731 
done 

732 

733 
instance real :: linorder 

734 
by (intro_classes, rule real_le_linear) 

735 

736 

737 
subsection{*Theorems About the Ordering*} 

738 

739 
lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)" 

740 
apply (auto simp add: real_of_preal_zero_less) 

741 
apply (cut_tac x = x in real_of_preal_trichotomy) 

742 
apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) 

743 
done 

744 

745 
lemma real_gt_preal_preal_Ex: 

746 
"real_of_preal z < x ==> \<exists>y. x = real_of_preal y" 

747 
by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] 

748 
intro: real_gt_zero_preal_Ex [THEN iffD1]) 

749 

750 
lemma real_ge_preal_preal_Ex: 

751 
"real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y" 

752 
by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) 

753 

754 
lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x" 

755 
by (auto elim: order_le_imp_less_or_eq [THEN disjE] 

756 
intro: real_of_preal_zero_less [THEN [2] real_less_trans] 

757 
simp add: real_of_preal_zero_less) 

758 

759 
lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" 

760 
by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) 

761 

762 
lemma real_of_preal_le_iff: 

763 
"(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)" 

14335  764 
by (auto intro!: preal_le_iff_less_or_eq [THEN iffD1] 
765 
simp add: linorder_not_less [symmetric]) 

14334  766 

767 

768 
subsection{*Monotonicity of Addition*} 

769 

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

771 
apply (auto simp add: real_gt_zero_preal_Ex) 

772 
apply (rule_tac x = "y*ya" in exI) 

773 
apply (simp (no_asm_use) add: real_of_preal_mult) 

774 
done 

775 

776 
(*Alternative definition for real_less*) 

777 
lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S" 

778 
apply (rule_tac x = R in real_of_preal_trichotomyE) 

779 
apply (rule_tac [!] x = S in real_of_preal_trichotomyE) 

14335  780 
apply (auto dest!: preal_less_add_left_Ex 
781 
simp add: real_of_preal_not_minus_gt_all real_of_preal_add 

782 
real_of_preal_not_less_zero real_less_not_refl 

783 
real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff) 

14334  784 
apply (rule real_of_preal_zero_less) 
785 
apply (rule_tac [1] x = "real_of_preal m+real_of_preal ma" in exI) 

786 
apply (rule_tac [2] x = "real_of_preal D" in exI) 

14335  787 
apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less 
788 
real_of_preal_sum_zero_less real_add_assoc) 

14334  789 
apply (simp add: real_add_assoc [symmetric]) 
790 
done 

791 

792 
lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (W::real))" 

793 
apply (drule real_less_add_positive_left_Ex) 

794 
apply (auto simp add: add_ac) 

795 
done 

796 

797 
lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (W)" 

798 
by (simp add: add_ac) 

799 

800 
(* FIXME: long! *) 

801 
lemma real_sum_gt_zero_less: "(0 < S + (W::real)) ==> (W < S)" 

802 
apply (rule ccontr) 

803 
apply (drule linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq]) 

804 
apply (auto simp add: real_less_not_refl) 

805 
apply (drule real_less_add_positive_left_Ex, clarify, simp) 

806 
apply (drule real_lemma_change_eq_subj, auto) 

807 
apply (drule real_less_sum_gt_zero) 

808 
apply (auto elim: real_less_asym simp add: add_left_commute [of W] add_ac) 

809 
done 

810 

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

812 
apply (rule real_sum_gt_zero_less) 

813 
apply (drule real_less_sum_gt_zero [of x y]) 

814 
apply (drule real_mult_order, assumption) 

815 
apply (simp add: right_distrib) 

816 
done 

817 

818 
lemma real_less_sum_gt_0_iff: "(0 < S + (W::real)) = (W < S)" 

819 
by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) 

820 

821 
lemma real_less_eq_diff: "(x<y) = (xy < (0::real))" 

822 
apply (unfold real_diff_def) 

823 
apply (subst real_minus_zero_less_iff [symmetric]) 

824 
apply (simp add: real_add_commute real_less_sum_gt_0_iff) 

825 
done 

826 

827 
lemma real_less_eqI: "(x::real)  y = x'  y' ==> (x<y) = (x'<y')" 

828 
apply (subst real_less_eq_diff) 

829 
apply (rule_tac y1 = y in real_less_eq_diff [THEN ssubst], simp) 

830 
done 

831 

832 
lemma real_le_eqI: "(x::real)  y = x'  y' ==> (y\<le>x) = (y'\<le>x')" 

833 
apply (drule real_less_eqI) 

834 
apply (simp add: real_le_def) 

835 
done 

836 

837 
lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)" 

838 
apply (rule real_le_eqI [THEN iffD1]) 

839 
prefer 2 apply assumption 

840 
apply (simp add: real_diff_def add_ac) 

841 
done 

842 

843 

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

845 

846 
instance real :: ordered_field 

847 
proof 

848 
fix x y z :: real 

849 
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono) 

850 
show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) 

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

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

853 
qed 

854 

855 
text{*These two need to be proved in @{text Ring_and_Field}*} 

856 
lemma real_add_less_le_mono: "[ w'<w; z'\<le>z ] ==> w' + z' < w + (z::real)" 

857 
apply (erule add_strict_right_mono [THEN order_less_le_trans]) 

858 
apply (erule add_left_mono) 

859 
done 

860 

861 
lemma real_add_le_less_mono: 

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

863 
apply (erule add_right_mono [THEN order_le_less_trans]) 

864 
apply (erule add_strict_left_mono) 

865 
done 

866 

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

868 
by (rule Ring_and_Field.zero_less_one) 

869 

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

871 
by (rule Ring_and_Field.zero_le_square) 

872 

873 

874 
subsection{*More Lemmas*} 

875 

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

877 
by auto 

878 

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

880 
by auto 

881 

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

883 
lemma real_mult_less_mono: 

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

885 
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) 

886 

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

888 
by (force elim: order_less_asym 

889 
simp add: Ring_and_Field.mult_less_cancel_right) 

890 

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

892 
by (auto simp add: real_le_def) 

893 

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

895 
by (force elim: order_less_asym 

896 
simp add: Ring_and_Field.mult_le_cancel_left) 

897 

898 
text{*Only two uses?*} 

899 
lemma real_mult_less_mono': 

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

901 
by (rule Ring_and_Field.mult_strict_mono') 

902 

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

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

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

906 
apply (cut_tac x = y in real_le_square) 

907 
apply (auto, drule real_le_anti_sym, auto) 

908 
done 

909 

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

911 
apply (rule_tac y = x in real_sum_squares_cancel) 

912 
apply (simp add: real_add_commute) 

913 
done 

914 

915 

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

917 
apply (drule add_strict_mono [of concl: 0 0], assumption) 

918 
apply simp 

919 
done 

920 

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

922 
apply (drule order_le_imp_less_or_eq)+ 

923 
apply (auto intro: real_add_order order_less_imp_le) 

924 
done 

925 

926 

927 
subsection{*An Embedding of the Naturals in the Reals*} 

928 

929 
lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)" 

930 
by (simp add: real_of_posnat_def pnat_one_iff [symmetric] 

931 
real_of_preal_def symmetric real_one_def) 

932 

933 
lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)" 

934 
by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq 

935 
real_add 

936 
prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric] 

937 
pnat_add_ac) 

938 

939 
lemma real_of_posnat_add: 

940 
"real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)" 

941 
apply (unfold real_of_posnat_def) 

942 
apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) 

943 
done 

944 

945 
lemma real_of_posnat_add_one: 

946 
"real_of_posnat (n + 1) = real_of_posnat n + (1::real)" 

947 
apply (rule_tac a1 = " (1::real) " in add_right_cancel [THEN iffD1]) 

948 
apply (rule real_of_posnat_add [THEN subst]) 

949 
apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc) 

950 
done 

951 

952 
lemma real_of_posnat_Suc: 

953 
"real_of_posnat (Suc n) = real_of_posnat n + (1::real)" 

954 
by (subst real_of_posnat_add_one [symmetric], simp) 

955 

956 
lemma inj_real_of_posnat: "inj(real_of_posnat)" 

957 
apply (rule inj_onI) 

958 
apply (unfold real_of_posnat_def) 

959 
apply (drule inj_real_of_preal [THEN injD]) 

960 
apply (drule inj_preal_of_prat [THEN injD]) 

961 
apply (drule inj_prat_of_pnat [THEN injD]) 

962 
apply (erule inj_pnat_of_nat [THEN injD]) 

963 
done 

964 

965 
lemma real_of_nat_zero [simp]: "real (0::nat) = 0" 

966 
by (simp add: real_of_nat_def real_of_posnat_one) 

967 

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

969 
by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc) 

970 

971 
lemma real_of_nat_add [simp]: 

972 
"real (m + n) = real (m::nat) + real n" 

973 
apply (simp add: real_of_nat_def add_ac) 

974 
apply (simp add: real_of_posnat_add add_assoc [symmetric]) 

975 
apply (simp add: add_commute) 

976 
apply (simp add: add_assoc [symmetric]) 

977 
done 

978 

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

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

981 
by (simp add: real_of_nat_def real_of_posnat_Suc add_ac) 

982 

983 
lemma real_of_nat_less_iff [iff]: 

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

985 
by (auto simp add: real_of_nat_def real_of_posnat_def) 

986 

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

988 
by (simp add: linorder_not_less [symmetric]) 

989 

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

991 
apply (rule inj_onI) 

992 
apply (auto intro!: inj_real_of_posnat [THEN injD] 

993 
simp add: real_of_nat_def add_right_cancel) 

994 
done 

995 

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

997 
apply (induct_tac "n") 

998 
apply (auto simp add: real_of_nat_Suc) 

999 
apply (drule real_add_le_less_mono) 

1000 
apply (rule zero_less_one) 

1001 
apply (simp add: order_less_imp_le) 

1002 
done 

1003 

1004 
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" 

1005 
apply (induct_tac "m") 

1006 
apply (auto simp add: real_of_nat_Suc left_distrib add_commute) 

1007 
done 

1008 

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

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

1011 

1012 
lemma real_of_nat_diff [rule_format]: 

1013 
"n \<le> m > real (m  n) = real (m::nat)  real n" 

1014 
apply (induct_tac "m", simp) 

1015 
apply (simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc add_ac) 

1016 
apply (simp add: add_left_commute [of _ " 1"]) 

1017 
done 

1018 

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

1020 
proof 

1021 
assume "real n = 0" 

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

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

1024 
next 

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

1026 
qed 

1027 

1028 
lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0" 

1029 
by (simp add: neg_nat real_of_nat_zero) 

1030 

1031 

1032 
lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" 

1033 
apply (case_tac "x \<noteq> 0") 

1034 
apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) 

1035 
done 

1036 

1037 
lemma real_inverse_gt_one: "[ (0::real) < x; x < 1 ] ==> 1 < inverse x" 

1038 
by (auto dest: less_imp_inverse_less) 

1039 

1040 
lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)" 

1041 
by (rule real_of_nat_less_iff [THEN subst], auto) 

1042 
declare real_of_nat_gt_zero_cancel_iff [simp] 

1043 

1044 
lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)" 

1045 
apply (rule real_of_nat_zero [THEN subst]) 

1046 
apply (subst real_of_nat_le_iff, auto) 

1047 
done 

1048 
declare real_of_nat_le_zero_cancel_iff [simp] 

1049 

1050 
lemma not_real_of_nat_less_zero: "~ real (n::nat) < 0" 

1051 
apply (simp (no_asm) add: real_le_def [symmetric] real_of_nat_ge_zero) 

1052 
done 

1053 
declare not_real_of_nat_less_zero [simp] 

1054 

1055 
lemma real_of_nat_ge_zero_cancel_iff [simp]: 

1056 
"(0 <= real (n::nat)) = (0 <= n)" 

1057 
apply (simp add: real_le_def le_def) 

1058 
done 

1059 

1060 
lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y" 

1061 
proof  

1062 
have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square) 

1063 
thus ?thesis by simp 

1064 
qed 

1065 

1066 

1067 
ML 

1068 
{* 

1069 
val real_abs_def = thm "real_abs_def"; 

1070 

1071 
val real_less_eq_diff = thm "real_less_eq_diff"; 

1072 

1073 
val real_mult = thm"real_mult"; 

1074 
val real_mult_commute = thm"real_mult_commute"; 

1075 
val real_mult_assoc = thm"real_mult_assoc"; 

1076 
val real_mult_1 = thm"real_mult_1"; 

1077 
val real_mult_1_right = thm"real_mult_1_right"; 

1078 
val real_minus_mult_commute = thm"real_minus_mult_commute"; 

1079 
val preal_le_linear = thm"preal_le_linear"; 

1080 
val real_mult_inv_left = thm"real_mult_inv_left"; 

1081 
val real_less_not_refl = thm"real_less_not_refl"; 

1082 
val real_less_irrefl = thm"real_less_irrefl"; 

1083 
val real_not_refl2 = thm"real_not_refl2"; 

1084 
val preal_lemma_trans = thm"preal_lemma_trans"; 

1085 
val real_less_trans = thm"real_less_trans"; 

1086 
val real_less_not_sym = thm"real_less_not_sym"; 

1087 
val real_less_asym = thm"real_less_asym"; 

1088 
val real_of_preal_add = thm"real_of_preal_add"; 

1089 
val real_of_preal_mult = thm"real_of_preal_mult"; 

1090 
val real_of_preal_ExI = thm"real_of_preal_ExI"; 

1091 
val real_of_preal_ExD = thm"real_of_preal_ExD"; 

1092 
val real_of_preal_iff = thm"real_of_preal_iff"; 

1093 
val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; 

1094 
val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; 

1095 
val real_of_preal_lessD = thm"real_of_preal_lessD"; 

1096 
val real_of_preal_lessI = thm"real_of_preal_lessI"; 

1097 
val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; 

1098 
val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; 

1099 
val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; 

1100 
val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; 

1101 
val real_of_preal_zero_less = thm"real_of_preal_zero_less"; 

1102 
val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; 

1103 
val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; 

1104 
val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; 

1105 
val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; 

1106 
val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; 

1107 
val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; 

1108 
val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; 

1109 
val real_linear = thm"real_linear"; 

1110 
val real_neq_iff = thm"real_neq_iff"; 

1111 
val real_linear_less2 = thm"real_linear_less2"; 

1112 
val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; 

1113 
val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; 

1114 
val real_le_less = thm"real_le_less"; 

1115 
val real_le_refl = thm"real_le_refl"; 

1116 
val real_le_linear = thm"real_le_linear"; 

1117 
val real_le_trans = thm"real_le_trans"; 

1118 
val real_le_anti_sym = thm"real_le_anti_sym"; 

1119 
val real_less_le = thm"real_less_le"; 

1120 
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; 

1121 
val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; 

1122 

1123 
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex"; 

1124 
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex"; 

1125 
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex"; 

1126 
val real_less_all_preal = thm "real_less_all_preal"; 

1127 
val real_less_all_real2 = thm "real_less_all_real2"; 

1128 
val real_of_preal_le_iff = thm "real_of_preal_le_iff"; 

1129 
val real_mult_order = thm "real_mult_order"; 

1130 
val real_zero_less_one = thm "real_zero_less_one"; 

1131 
val real_add_less_le_mono = thm "real_add_less_le_mono"; 

1132 
val real_add_le_less_mono = thm "real_add_le_less_mono"; 

1133 
val real_add_order = thm "real_add_order"; 

1134 
val real_le_add_order = thm "real_le_add_order"; 

1135 
val real_le_square = thm "real_le_square"; 

1136 
val real_mult_less_mono2 = thm "real_mult_less_mono2"; 

1137 

1138 
val real_mult_less_iff1 = thm "real_mult_less_iff1"; 

1139 
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; 

1140 
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; 

1141 
val real_mult_less_mono = thm "real_mult_less_mono"; 

1142 
val real_mult_less_mono' = thm "real_mult_less_mono'"; 

1143 
val real_sum_squares_cancel = thm "real_sum_squares_cancel"; 

1144 
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; 

1145 

1146 
val real_mult_left_cancel = thm"real_mult_left_cancel"; 

1147 
val real_mult_right_cancel = thm"real_mult_right_cancel"; 

1148 
val real_of_posnat_one = thm "real_of_posnat_one"; 

1149 
val real_of_posnat_two = thm "real_of_posnat_two"; 

1150 
val real_of_posnat_add = thm "real_of_posnat_add"; 

1151 
val real_of_posnat_add_one = thm "real_of_posnat_add_one"; 

1152 
val real_of_nat_zero = thm "real_of_nat_zero"; 

1153 
val real_of_nat_one = thm "real_of_nat_one"; 

1154 
val real_of_nat_add = thm "real_of_nat_add"; 

1155 
val real_of_nat_Suc = thm "real_of_nat_Suc"; 

1156 
val real_of_nat_less_iff = thm "real_of_nat_less_iff"; 

1157 
val real_of_nat_le_iff = thm "real_of_nat_le_iff"; 

1158 
val inj_real_of_nat = thm "inj_real_of_nat"; 

1159 
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; 

1160 
val real_of_nat_mult = thm "real_of_nat_mult"; 

1161 
val real_of_nat_inject = thm "real_of_nat_inject"; 

1162 
val real_of_nat_diff = thm "real_of_nat_diff"; 

1163 
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; 

1164 
val real_of_nat_neg_int = thm "real_of_nat_neg_int"; 

1165 
val real_inverse_unique = thm "real_inverse_unique"; 

1166 
val real_inverse_gt_one = thm "real_inverse_gt_one"; 

1167 
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; 

1168 
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; 

1169 
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; 

1170 
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; 

1171 
*} 

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

1172 

5588  1173 
end 