author  paulson 
Tue, 06 Jan 2004 10:40:15 +0100  
changeset 14341  a09441bd4f1e 
parent 14335  9c0b5e081037 
child 14348  744c868ee0b7 
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 

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

333 

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

334 
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

335 

14334  336 
instance real :: field 
337 
proof 

338 
fix x y z :: real 

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

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

341 
show "0 + x = x" by simp 

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

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

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

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

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

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

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

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

350 
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

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

352 
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

353 
thus "x = y" by (simp add: real_add_minus_left) 
14334  354 
qed 
355 

356 

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

357 
text{*Inverse of zero! Useful to simplify certain equations*} 
14269  358 

14334  359 
lemma INVERSE_ZERO: "inverse 0 = (0::real)" 
360 
apply (unfold real_inverse_def) 

361 
apply (rule someI2) 

362 
apply (auto simp add: zero_neq_one) 

14269  363 
done 
14334  364 

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

366 
by (simp add: real_divide_def INVERSE_ZERO) 

367 

368 
instance real :: division_by_zero 

369 
proof 

370 
fix x :: real 

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

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

373 
qed 

374 

375 

376 
(*Pull negations out*) 

377 
declare minus_mult_right [symmetric, simp] 

378 
minus_mult_left [symmetric, simp] 

379 

380 
text{*Used in RealBin*} 

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

382 
by simp 

383 

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

385 
by (rule Ring_and_Field.mult_1_right) 

14269  386 

387 

14329  388 
subsection{*Theorems for Ordering*} 
389 

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

14269  391 

14329  392 
text{*lemmas*} 
393 
lemma preal_lemma_eq_rev_sum: 

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

14269  395 
by (simp add: preal_add_commute) 
396 

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

14269  399 
by (simp add: preal_add_ac) 
400 

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

14269  403 
x + y2b = x2b + y ] 
404 
==> x2a + y2b = x2b + y2a" 

405 
apply (drule preal_lemma_eq_rev_sum, assumption) 

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

407 
apply (simp add: preal_add_ac) 

408 
apply (drule preal_add_left_commute_cancel) 

409 
apply (simp add: preal_add_ac) 

410 
done 

411 

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

413 
apply (rule_tac z = R in eq_Abs_REAL) 

414 
apply (auto simp add: real_less_def) 

415 
apply (drule preal_lemma_for_not_refl, assumption, auto) 

416 
done 

417 

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

419 
lemmas real_less_irrefl = real_less_not_refl [THEN notE, standard] 

420 
declare real_less_irrefl [elim!] 

421 

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

423 
by (auto simp add: real_less_not_refl) 

424 

425 
(* lemma rearranging and eliminating terms *) 

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

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

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

429 
apply (simp add: preal_add_ac) 

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

431 
apply (simp add: preal_add_assoc [symmetric]) 

432 
done 

433 

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

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

436 
apply (rule_tac z = R1 in eq_Abs_REAL) 

437 
apply (rule_tac z = R2 in eq_Abs_REAL) 

438 
apply (rule_tac z = R3 in eq_Abs_REAL) 

439 
apply (auto simp add: real_less_def) 

440 
apply (rule exI)+ 

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

442 
prefer 2 apply blast 

443 
prefer 2 apply blast 

444 
apply (drule preal_lemma_for_not_refl, assumption) 

445 
apply (blast dest: preal_add_less_mono intro: preal_lemma_trans) 

446 
done 

447 

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

449 
apply (rule notI) 

450 
apply (drule real_less_trans, assumption) 

451 
apply (simp add: real_less_not_refl) 

452 
done 

453 

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

455 
lemmas real_less_asym = real_less_not_sym [THEN contrapos_np, standard] 

456 

457 
lemma real_of_preal_add: 

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

459 
real_of_preal z1 + real_of_preal z2" 

460 
apply (unfold real_of_preal_def) 

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

462 
done 

463 

464 
lemma real_of_preal_mult: 

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

466 
real_of_preal z1* real_of_preal z2" 

467 
apply (unfold real_of_preal_def) 

468 
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) 

469 
done 

470 

471 
lemma real_of_preal_ExI: 

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

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

474 
apply (unfold real_of_preal_def) 

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

476 
done 

477 

478 
lemma real_of_preal_ExD: 

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

480 
real_of_preal m ==> y < x" 

481 
apply (unfold real_of_preal_def) 

482 
apply (auto simp add: preal_add_commute preal_add_assoc) 

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

484 
done 

485 

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

14269  488 
by (blast intro!: real_of_preal_ExI real_of_preal_ExD) 
489 

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

493 
apply (unfold real_of_preal_def real_zero_def) 

494 
apply (rule_tac z = x in eq_Abs_REAL) 

495 
apply (auto simp add: real_minus preal_add_ac) 

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

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

498 
apply (auto simp add: preal_add_commute) 

499 
done 

500 

14329  501 
lemma real_of_preal_trichotomyE: 
502 
"!!P. [ !!m. x = real_of_preal m ==> P; 

14269  503 
x = 0 ==> P; 
504 
!!m. x = (real_of_preal m) ==> P ] ==> P" 

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

506 
done 

507 

508 
lemma real_of_preal_lessD: 

509 
"real_of_preal m1 < real_of_preal m2 ==> m1 < m2" 

510 
apply (unfold real_of_preal_def) 

511 
apply (auto simp add: real_less_def preal_add_ac) 

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

513 
apply (auto simp add: preal_add_ac) 

514 
done 

515 

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

517 
apply (drule preal_less_add_left_Ex) 

518 
apply (auto simp add: real_of_preal_add real_of_preal_def real_less_def) 

519 
apply (rule exI)+ 

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

521 
apply (rule_tac [2] refl)+ 

522 
apply (simp add: preal_self_less_add_left del: preal_add_less_iff2) 

523 
done 

524 

14329  525 
lemma real_of_preal_less_iff1: 
526 
"(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" 

14269  527 
by (blast intro: real_of_preal_lessI real_of_preal_lessD) 
528 

529 
declare real_of_preal_less_iff1 [simp] 

530 

531 
lemma real_of_preal_minus_less_self: " real_of_preal m < real_of_preal m" 

532 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

533 
apply (rule exI)+ 

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

535 
apply (rule_tac [2] refl)+ 

536 
apply (simp (no_asm_use) add: preal_add_ac) 

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

538 
done 

539 

540 
lemma real_of_preal_minus_less_zero: " real_of_preal m < 0" 

541 
apply (unfold real_zero_def) 

542 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

543 
apply (rule exI)+ 

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

545 
apply (rule_tac [2] refl)+ 

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

547 
done 

548 

549 
lemma real_of_preal_not_minus_gt_zero: "~ 0 <  real_of_preal m" 

550 
apply (cut_tac real_of_preal_minus_less_zero) 

551 
apply (fast dest: real_less_trans elim: real_less_irrefl) 

552 
done 

553 

554 
lemma real_of_preal_zero_less: "0 < real_of_preal m" 

555 
apply (unfold real_zero_def) 

556 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

557 
apply (rule exI)+ 

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

559 
apply (rule_tac [2] refl)+ 

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

561 
done 

562 

563 
lemma real_of_preal_not_less_zero: "~ real_of_preal m < 0" 

564 
apply (cut_tac real_of_preal_zero_less) 

565 
apply (blast dest: real_less_trans elim: real_less_irrefl) 

566 
done 

567 

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

569 
by (simp add: real_of_preal_zero_less) 

570 

571 
(* another lemma *) 

572 
lemma real_of_preal_sum_zero_less: 

573 
"0 < real_of_preal m + real_of_preal m1" 

574 
apply (unfold real_zero_def) 

575 
apply (auto simp add: real_of_preal_def real_less_def real_add) 

576 
apply (rule exI)+ 

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

578 
apply (rule_tac [2] refl)+ 

579 
apply (simp (no_asm_use) add: preal_add_ac) 

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

581 
done 

582 

583 
lemma real_of_preal_minus_less_all: " real_of_preal m < real_of_preal m1" 

584 
apply (auto simp add: real_of_preal_def real_less_def real_minus) 

585 
apply (rule exI)+ 

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

587 
apply (rule_tac [2] refl)+ 

588 
apply (simp (no_asm_use) add: preal_add_ac) 

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

590 
done 

591 

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

593 
apply (cut_tac real_of_preal_minus_less_all) 

594 
apply (blast dest: real_less_trans elim: real_less_irrefl) 

595 
done 

596 

14329  597 
lemma real_of_preal_minus_less_rev1: 
598 
" real_of_preal m1 <  real_of_preal m2 

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

601 
apply (rule exI)+ 

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

603 
apply (rule_tac [2] refl)+ 

604 
apply (auto simp add: preal_add_ac) 

605 
apply (simp add: preal_add_assoc [symmetric]) 

606 
apply (auto simp add: preal_add_ac) 

607 
done 

608 

14329  609 
lemma real_of_preal_minus_less_rev2: 
610 
"real_of_preal m1 < real_of_preal m2 

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

613 
apply (rule exI)+ 

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

615 
apply (rule_tac [2] refl)+ 

616 
apply (auto simp add: preal_add_ac) 

617 
apply (simp add: preal_add_assoc [symmetric]) 

618 
apply (auto simp add: preal_add_ac) 

619 
done 

620 

14329  621 
lemma real_of_preal_minus_less_rev_iff: 
622 
"( real_of_preal m1 <  real_of_preal m2) = 

14269  623 
(real_of_preal m2 < real_of_preal m1)" 
624 
apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2) 

625 
done 

626 

14270  627 

628 
subsection{*Linearity of the Ordering*} 

629 

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

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

14270  633 
apply (auto dest!: preal_le_anti_sym 
634 
simp add: preal_less_le_iff real_of_preal_minus_less_zero 

14334  635 
real_of_preal_zero_less real_of_preal_minus_less_all 
636 
real_of_preal_minus_less_rev_iff) 

14269  637 
done 
638 

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

640 
by (cut_tac real_linear, blast) 

641 

642 

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

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

647 
done 

648 

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

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_iff [simp] 

654 

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

656 
apply (rule_tac x = R in real_of_preal_trichotomyE) 

657 
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) 

658 
done 

659 
declare real_minus_zero_less_iff2 [simp] 

660 

661 

14334  662 
subsection{*Properties of LessThan Or Equals*} 
663 

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

665 
apply (unfold real_le_def) 

666 
apply (cut_tac real_linear) 

667 
apply (blast elim: real_less_irrefl real_less_asym) 

668 
done 

669 

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

671 
apply (unfold real_le_def) 

672 
apply (cut_tac real_linear) 

673 
apply (fast elim: real_less_irrefl real_less_asym) 

674 
done 

675 

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

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

678 

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

680 
by (simp add: real_le_less) 

681 

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

683 
apply (drule real_le_imp_less_or_eq) 

684 
apply (drule real_le_imp_less_or_eq) 

685 
apply (rule real_less_or_eq_imp_le) 

686 
apply (blast intro: real_less_trans) 

687 
done 

688 

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

690 
apply (drule real_le_imp_less_or_eq) 

691 
apply (drule real_le_imp_less_or_eq) 

692 
apply (fast elim: real_less_irrefl real_less_asym) 

693 
done 

694 

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

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

697 
apply (simp add: real_le_def real_neq_iff) 

698 
apply (blast elim!: real_less_asym) 

699 
done 

700 

701 
instance real :: order 

702 
by (intro_classes, 

703 
(assumption  

704 
rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) 

705 

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

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

708 
apply (simp add: real_le_less) 

709 
apply (cut_tac real_linear, blast) 

710 
done 

711 

712 
instance real :: linorder 

713 
by (intro_classes, rule real_le_linear) 

714 

715 

716 
subsection{*Theorems About the Ordering*} 

717 

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

719 
apply (auto simp add: real_of_preal_zero_less) 

720 
apply (cut_tac x = x in real_of_preal_trichotomy) 

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

722 
done 

723 

724 
lemma real_gt_preal_preal_Ex: 

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

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

727 
intro: real_gt_zero_preal_Ex [THEN iffD1]) 

728 

729 
lemma real_ge_preal_preal_Ex: 

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

731 
by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) 

732 

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

734 
by (auto elim: order_le_imp_less_or_eq [THEN disjE] 

735 
intro: real_of_preal_zero_less [THEN [2] real_less_trans] 

736 
simp add: real_of_preal_zero_less) 

737 

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

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

740 

741 
lemma real_of_preal_le_iff: 

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

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

14334  745 

746 

747 
subsection{*Monotonicity of Addition*} 

748 

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

750 
apply (auto simp add: real_gt_zero_preal_Ex) 

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

752 
apply (simp (no_asm_use) add: real_of_preal_mult) 

753 
done 

754 

755 
(*Alternative definition for real_less*) 

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

757 
apply (rule_tac x = R in real_of_preal_trichotomyE) 

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

14335  759 
apply (auto dest!: preal_less_add_left_Ex 
760 
simp add: real_of_preal_not_minus_gt_all real_of_preal_add 

761 
real_of_preal_not_less_zero real_less_not_refl 

762 
real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff) 

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

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

14335  766 
apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less 
767 
real_of_preal_sum_zero_less real_add_assoc) 

14334  768 
apply (simp add: real_add_assoc [symmetric]) 
769 
done 

770 

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

772 
apply (drule real_less_add_positive_left_Ex) 

773 
apply (auto simp add: add_ac) 

774 
done 

775 

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

777 
by (simp add: add_ac) 

778 

779 
(* FIXME: long! *) 

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

781 
apply (rule ccontr) 

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

783 
apply (auto simp add: real_less_not_refl) 

784 
apply (drule real_less_add_positive_left_Ex, clarify, simp) 

785 
apply (drule real_lemma_change_eq_subj, auto) 

786 
apply (drule real_less_sum_gt_zero) 

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

788 
done 

789 

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

791 
apply (rule real_sum_gt_zero_less) 

792 
apply (drule real_less_sum_gt_zero [of x y]) 

793 
apply (drule real_mult_order, assumption) 

794 
apply (simp add: right_distrib) 

795 
done 

796 

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

798 
by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) 

799 

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

801 
apply (unfold real_diff_def) 

802 
apply (subst real_minus_zero_less_iff [symmetric]) 

803 
apply (simp add: real_add_commute real_less_sum_gt_0_iff) 

804 
done 

805 

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

807 
apply (subst real_less_eq_diff) 

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

809 
done 

810 

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

812 
apply (drule real_less_eqI) 

813 
apply (simp add: real_le_def) 

814 
done 

815 

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

817 
apply (rule real_le_eqI [THEN iffD1]) 

818 
prefer 2 apply assumption 

819 
apply (simp add: real_diff_def add_ac) 

820 
done 

821 

822 

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

824 

825 
instance real :: ordered_field 

826 
proof 

827 
fix x y z :: real 

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

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

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

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

832 
qed 

833 

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

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

836 
apply (erule add_strict_right_mono [THEN order_less_le_trans]) 

837 
apply (erule add_left_mono) 

838 
done 

839 

840 
lemma real_add_le_less_mono: 

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

842 
apply (erule add_right_mono [THEN order_le_less_trans]) 

843 
apply (erule add_strict_left_mono) 

844 
done 

845 

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

847 
by (rule Ring_and_Field.zero_less_one) 

848 

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

850 
by (rule Ring_and_Field.zero_le_square) 

851 

852 

853 
subsection{*More Lemmas*} 

854 

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

856 
by auto 

857 

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

859 
by auto 

860 

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

862 
lemma real_mult_less_mono: 

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

864 
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) 

865 

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

867 
by (force elim: order_less_asym 

868 
simp add: Ring_and_Field.mult_less_cancel_right) 

869 

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

871 
by (auto simp add: real_le_def) 

872 

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

874 
by (force elim: order_less_asym 

875 
simp add: Ring_and_Field.mult_le_cancel_left) 

876 

877 
text{*Only two uses?*} 

878 
lemma real_mult_less_mono': 

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

880 
by (rule Ring_and_Field.mult_strict_mono') 

881 

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

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

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

885 
apply (cut_tac x = y in real_le_square) 

886 
apply (auto, drule real_le_anti_sym, auto) 

887 
done 

888 

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

890 
apply (rule_tac y = x in real_sum_squares_cancel) 

891 
apply (simp add: real_add_commute) 

892 
done 

893 

894 

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

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

897 
apply simp 

898 
done 

899 

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

901 
apply (drule order_le_imp_less_or_eq)+ 

902 
apply (auto intro: real_add_order order_less_imp_le) 

903 
done 

904 

905 

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

907 

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

909 
by (simp add: real_of_posnat_def pnat_one_iff [symmetric] 

910 
real_of_preal_def symmetric real_one_def) 

911 

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

913 
by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq 

914 
real_add 

915 
prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric] 

916 
pnat_add_ac) 

917 

918 
lemma real_of_posnat_add: 

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

920 
apply (unfold real_of_posnat_def) 

921 
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) 

922 
done 

923 

924 
lemma real_of_posnat_add_one: 

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

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

927 
apply (rule real_of_posnat_add [THEN subst]) 

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

929 
done 

930 

931 
lemma real_of_posnat_Suc: 

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

933 
by (subst real_of_posnat_add_one [symmetric], simp) 

934 

935 
lemma inj_real_of_posnat: "inj(real_of_posnat)" 

936 
apply (rule inj_onI) 

937 
apply (unfold real_of_posnat_def) 

938 
apply (drule inj_real_of_preal [THEN injD]) 

939 
apply (drule inj_preal_of_prat [THEN injD]) 

940 
apply (drule inj_prat_of_pnat [THEN injD]) 

941 
apply (erule inj_pnat_of_nat [THEN injD]) 

942 
done 

943 

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

945 
by (simp add: real_of_nat_def real_of_posnat_one) 

946 

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

948 
by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc) 

949 

950 
lemma real_of_nat_add [simp]: 

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

952 
apply (simp add: real_of_nat_def add_ac) 

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

954 
apply (simp add: add_commute) 

955 
apply (simp add: add_assoc [symmetric]) 

956 
done 

957 

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

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

960 
by (simp add: real_of_nat_def real_of_posnat_Suc add_ac) 

961 

962 
lemma real_of_nat_less_iff [iff]: 

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

964 
by (auto simp add: real_of_nat_def real_of_posnat_def) 

965 

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

967 
by (simp add: linorder_not_less [symmetric]) 

968 

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

970 
apply (rule inj_onI) 

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

972 
simp add: real_of_nat_def add_right_cancel) 

973 
done 

974 

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

976 
apply (induct_tac "n") 

977 
apply (auto simp add: real_of_nat_Suc) 

978 
apply (drule real_add_le_less_mono) 

979 
apply (rule zero_less_one) 

980 
apply (simp add: order_less_imp_le) 

981 
done 

982 

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

984 
apply (induct_tac "m") 

985 
apply (auto simp add: real_of_nat_Suc left_distrib add_commute) 

986 
done 

987 

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

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

990 

991 
lemma real_of_nat_diff [rule_format]: 

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

993 
apply (induct_tac "m", simp) 

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

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

996 
done 

997 

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

999 
proof 

1000 
assume "real n = 0" 

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

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

1003 
next 

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

1005 
qed 

1006 

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

1008 
by (simp add: neg_nat real_of_nat_zero) 

1009 

1010 

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

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

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

1014 
done 

1015 

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

1017 
by (auto dest: less_imp_inverse_less) 

1018 

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

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

1021 
declare real_of_nat_gt_zero_cancel_iff [simp] 

1022 

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

1024 
apply (rule real_of_nat_zero [THEN subst]) 

1025 
apply (subst real_of_nat_le_iff, auto) 

1026 
done 

1027 
declare real_of_nat_le_zero_cancel_iff [simp] 

1028 

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

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

1031 
done 

1032 
declare not_real_of_nat_less_zero [simp] 

1033 

1034 
lemma real_of_nat_ge_zero_cancel_iff [simp]: 

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

1036 
apply (simp add: real_le_def le_def) 

1037 
done 

1038 

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

1040 
proof  

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

1042 
thus ?thesis by simp 

1043 
qed 

1044 

1045 

1046 
ML 

1047 
{* 

1048 
val real_abs_def = thm "real_abs_def"; 

1049 

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

1050 
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

1051 
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

1052 
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

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

1054 

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

1055 
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

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

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

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

1059 
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

1060 
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

1061 
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

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

1063 
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

1064 
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

1065 
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

1066 
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

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

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

1069 
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

1070 
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

1071 
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

1072 
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

1073 

14334  1074 
val real_less_eq_diff = thm "real_less_eq_diff"; 
1075 

1076 
val real_mult = thm"real_mult"; 

1077 
val real_mult_commute = thm"real_mult_commute"; 

1078 
val real_mult_assoc = thm"real_mult_assoc"; 

1079 
val real_mult_1 = thm"real_mult_1"; 

1080 
val real_mult_1_right = thm"real_mult_1_right"; 

1081 
val real_minus_mult_commute = thm"real_minus_mult_commute"; 

1082 
val preal_le_linear = thm"preal_le_linear"; 

1083 
val real_mult_inv_left = thm"real_mult_inv_left"; 

1084 
val real_less_not_refl = thm"real_less_not_refl"; 

1085 
val real_less_irrefl = thm"real_less_irrefl"; 

1086 
val real_not_refl2 = thm"real_not_refl2"; 

1087 
val preal_lemma_trans = thm"preal_lemma_trans"; 

1088 
val real_less_trans = thm"real_less_trans"; 

1089 
val real_less_not_sym = thm"real_less_not_sym"; 

1090 
val real_less_asym = thm"real_less_asym"; 

1091 
val real_of_preal_add = thm"real_of_preal_add"; 

1092 
val real_of_preal_mult = thm"real_of_preal_mult"; 

1093 
val real_of_preal_ExI = thm"real_of_preal_ExI"; 

1094 
val real_of_preal_ExD = thm"real_of_preal_ExD"; 

1095 
val real_of_preal_iff = thm"real_of_preal_iff"; 

1096 
val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; 

1097 
val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; 

1098 
val real_of_preal_lessD = thm"real_of_preal_lessD"; 

1099 
val real_of_preal_lessI = thm"real_of_preal_lessI"; 

1100 
val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; 

1101 
val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; 

1102 
val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; 

1103 
val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; 

1104 
val real_of_preal_zero_less = thm"real_of_preal_zero_less"; 

1105 
val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; 

1106 
val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; 

1107 
val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; 

1108 
val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; 

1109 
val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; 

1110 
val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; 

1111 
val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; 

1112 
val real_linear = thm"real_linear"; 

1113 
val real_neq_iff = thm"real_neq_iff"; 

1114 
val real_linear_less2 = thm"real_linear_less2"; 

1115 
val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; 

1116 
val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; 

1117 
val real_le_less = thm"real_le_less"; 

1118 
val real_le_refl = thm"real_le_refl"; 

1119 
val real_le_linear = thm"real_le_linear"; 

1120 
val real_le_trans = thm"real_le_trans"; 

1121 
val real_le_anti_sym = thm"real_le_anti_sym"; 

1122 
val real_less_le = thm"real_less_le"; 

1123 
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; 

1124 
val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; 

1125 

1126 
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex"; 

1127 
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex"; 

1128 
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex"; 

1129 
val real_less_all_preal = thm "real_less_all_preal"; 

1130 
val real_less_all_real2 = thm "real_less_all_real2"; 

1131 
val real_of_preal_le_iff = thm "real_of_preal_le_iff"; 

1132 
val real_mult_order = thm "real_mult_order"; 

1133 
val real_zero_less_one = thm "real_zero_less_one"; 

1134 
val real_add_less_le_mono = thm "real_add_less_le_mono"; 

1135 
val real_add_le_less_mono = thm "real_add_le_less_mono"; 

1136 
val real_add_order = thm "real_add_order"; 

1137 
val real_le_add_order = thm "real_le_add_order"; 

1138 
val real_le_square = thm "real_le_square"; 

1139 
val real_mult_less_mono2 = thm "real_mult_less_mono2"; 

1140 

1141 
val real_mult_less_iff1 = thm "real_mult_less_iff1"; 

1142 
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; 

1143 
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; 

1144 
val real_mult_less_mono = thm "real_mult_less_mono"; 

1145 
val real_mult_less_mono' = thm "real_mult_less_mono'"; 

1146 
val real_sum_squares_cancel = thm "real_sum_squares_cancel"; 

1147 
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; 

1148 

1149 
val real_mult_left_cancel = thm"real_mult_left_cancel"; 

1150 
val real_mult_right_cancel = thm"real_mult_right_cancel"; 

1151 
val real_of_posnat_one = thm "real_of_posnat_one"; 

1152 
val real_of_posnat_two = thm "real_of_posnat_two"; 

1153 
val real_of_posnat_add = thm "real_of_posnat_add"; 

1154 
val real_of_posnat_add_one = thm "real_of_posnat_add_one"; 

1155 
val real_of_nat_zero = thm "real_of_nat_zero"; 

1156 
val real_of_nat_one = thm "real_of_nat_one"; 

1157 
val real_of_nat_add = thm "real_of_nat_add"; 

1158 
val real_of_nat_Suc = thm "real_of_nat_Suc"; 

1159 
val real_of_nat_less_iff = thm "real_of_nat_less_iff"; 

1160 
val real_of_nat_le_iff = thm "real_of_nat_le_iff"; 

1161 
val inj_real_of_nat = thm "inj_real_of_nat"; 

1162 
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; 

1163 
val real_of_nat_mult = thm "real_of_nat_mult"; 

1164 
val real_of_nat_inject = thm "real_of_nat_inject"; 

1165 
val real_of_nat_diff = thm "real_of_nat_diff"; 

1166 
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; 

1167 
val real_of_nat_neg_int = thm "real_of_nat_neg_int"; 

1168 
val real_inverse_unique = thm "real_inverse_unique"; 

1169 
val real_inverse_gt_one = thm "real_inverse_gt_one"; 

1170 
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; 

1171 
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; 

1172 
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; 

1173 
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; 

1174 
*} 

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

1175 

5588  1176 
end 