82 Y \<in> Rep_hypreal(Q) & |
82 Y \<in> Rep_hypreal(Q) & |
83 {n::nat. X n < Y n} \<in> FreeUltrafilterNat" |
83 {n::nat. X n < Y n} \<in> FreeUltrafilterNat" |
84 hypreal_le_def: |
84 hypreal_le_def: |
85 "P <= (Q::hypreal) == ~(Q < P)" |
85 "P <= (Q::hypreal) == ~(Q < P)" |
86 |
86 |
87 (*------------------------------------------------------------------------ |
87 hrabs_def: "abs (r::hypreal) == (if 0 \<le> r then r else -r)" |
88 Proof that the set of naturals is not finite |
88 |
89 ------------------------------------------------------------------------*) |
89 |
|
90 subsection{*The Set of Naturals is not Finite*} |
90 |
91 |
91 (*** based on James' proof that the set of naturals is not finite ***) |
92 (*** based on James' proof that the set of naturals is not finite ***) |
92 lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)" |
93 lemma finite_exhausts [rule_format]: |
|
94 "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)" |
93 apply (rule impI) |
95 apply (rule impI) |
94 apply (erule_tac F = A in finite_induct) |
96 apply (erule_tac F = A in finite_induct) |
95 apply (blast, erule exE) |
97 apply (blast, erule exE) |
96 apply (rule_tac x = "n + x" in exI) |
98 apply (rule_tac x = "n + x" in exI) |
97 apply (rule allI, erule_tac x = "x + m" in allE) |
99 apply (rule allI, erule_tac x = "x + m" in allE) |
98 apply (auto simp add: add_ac) |
100 apply (auto simp add: add_ac) |
99 done |
101 done |
100 |
102 |
101 lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\<exists>n. n \<notin>A)" |
103 lemma finite_not_covers [rule_format (no_asm)]: |
|
104 "finite (A :: nat set) --> (\<exists>n. n \<notin>A)" |
102 by (rule impI, drule finite_exhausts, blast) |
105 by (rule impI, drule finite_exhausts, blast) |
103 |
106 |
104 lemma not_finite_nat: "~ finite(UNIV:: nat set)" |
107 lemma not_finite_nat: "~ finite(UNIV:: nat set)" |
105 by (fast dest!: finite_exhausts) |
108 by (fast dest!: finite_exhausts) |
106 |
109 |
107 (*------------------------------------------------------------------------ |
110 |
108 Existence of free ultrafilter over the naturals and proof of various |
111 subsection{*Existence of Free Ultrafilter over the Naturals*} |
109 properties of the FreeUltrafilterNat- an arbitrary free ultrafilter |
112 |
110 ------------------------------------------------------------------------*) |
113 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
|
114 an arbitrary free ultrafilter*} |
111 |
115 |
112 lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)" |
116 lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)" |
113 by (rule not_finite_nat [THEN FreeUltrafilter_Ex]) |
117 by (rule not_finite_nat [THEN FreeUltrafilter_Ex]) |
114 |
118 |
115 lemma FreeUltrafilterNat_mem [simp]: |
119 lemma FreeUltrafilterNat_mem [simp]: |
135 apply (rule someI2, assumption) |
139 apply (rule someI2, assumption) |
136 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter |
140 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter |
137 Filter_empty_not_mem) |
141 Filter_empty_not_mem) |
138 done |
142 done |
139 |
143 |
140 lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] |
144 lemma FreeUltrafilterNat_Int: |
|
145 "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] |
141 ==> X Int Y \<in> FreeUltrafilterNat" |
146 ==> X Int Y \<in> FreeUltrafilterNat" |
142 apply (cut_tac FreeUltrafilterNat_mem) |
147 apply (cut_tac FreeUltrafilterNat_mem) |
143 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) |
148 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) |
144 done |
149 done |
145 |
150 |
146 lemma FreeUltrafilterNat_subset: "[| X: FreeUltrafilterNat; X <= Y |] |
151 lemma FreeUltrafilterNat_subset: |
|
152 "[| X: FreeUltrafilterNat; X <= Y |] |
147 ==> Y \<in> FreeUltrafilterNat" |
153 ==> Y \<in> FreeUltrafilterNat" |
148 apply (cut_tac FreeUltrafilterNat_mem) |
154 apply (cut_tac FreeUltrafilterNat_mem) |
149 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) |
155 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) |
150 done |
156 done |
151 |
157 |
152 lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
158 lemma FreeUltrafilterNat_Compl: |
|
159 "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
153 apply safe |
160 apply safe |
154 apply (drule FreeUltrafilterNat_Int, assumption, auto) |
161 apply (drule FreeUltrafilterNat_Int, assumption, auto) |
155 done |
162 done |
156 |
163 |
157 lemma FreeUltrafilterNat_Compl_mem: "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
164 lemma FreeUltrafilterNat_Compl_mem: |
|
165 "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
158 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) |
166 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) |
159 apply (safe, drule_tac x = X in bspec) |
167 apply (safe, drule_tac x = X in bspec) |
160 apply (auto simp add: UNIV_diff_Compl) |
168 apply (auto simp add: UNIV_diff_Compl) |
161 done |
169 done |
162 |
170 |
163 lemma FreeUltrafilterNat_Compl_iff1: "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" |
171 lemma FreeUltrafilterNat_Compl_iff1: |
|
172 "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" |
164 by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) |
173 by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) |
165 |
174 |
166 lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
175 lemma FreeUltrafilterNat_Compl_iff2: |
|
176 "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
167 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
177 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
168 |
178 |
169 lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat" |
179 lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat" |
170 by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) |
180 by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) |
171 |
181 |
172 lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat" |
182 lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat" |
173 by auto |
183 by auto |
174 |
184 |
175 lemma FreeUltrafilterNat_Nat_set_refl [intro]: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat" |
185 lemma FreeUltrafilterNat_Nat_set_refl [intro]: |
|
186 "{n. P(n) = P(n)} \<in> FreeUltrafilterNat" |
176 by simp |
187 by simp |
177 |
188 |
178 lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P" |
189 lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P" |
179 by (rule ccontr, simp) |
190 by (rule ccontr, simp) |
180 |
191 |
202 ultra_tac (Classical.get_local_claset ctxt, |
212 ultra_tac (Classical.get_local_claset ctxt, |
203 Simplifier.get_local_simpset ctxt) 1)) *} |
213 Simplifier.get_local_simpset ctxt) 1)) *} |
204 "ultrafilter tactic" |
214 "ultrafilter tactic" |
205 |
215 |
206 |
216 |
207 (*------------------------------------------------------- |
217 text{*One further property of our free ultrafilter*} |
208 Now prove one further property of our free ultrafilter |
218 lemma FreeUltrafilterNat_Un: |
209 -------------------------------------------------------*) |
219 "X Un Y: FreeUltrafilterNat |
210 lemma FreeUltrafilterNat_Un: "X Un Y: FreeUltrafilterNat |
|
211 ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat" |
220 ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat" |
212 apply auto |
221 apply auto |
213 apply ultra |
222 apply ultra |
214 done |
223 done |
215 |
224 |
216 (*------------------------------------------------------- |
225 |
217 Properties of hyprel |
226 subsection{*Properties of @{term hyprel}*} |
218 -------------------------------------------------------*) |
227 |
219 |
228 text{*Proving that @{term hyprel} is an equivalence relation*} |
220 (** Proving that hyprel is an equivalence relation **) |
|
221 (** Natural deduction for hyprel **) |
|
222 |
229 |
223 lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)" |
230 lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)" |
224 by (unfold hyprel_def, fast) |
231 by (unfold hyprel_def, fast) |
225 |
232 |
226 lemma hyprel_refl: "(x,x): hyprel" |
233 lemma hyprel_refl: "(x,x): hyprel" |
300 apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE]) |
306 apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE]) |
301 apply (drule_tac f = Abs_hypreal in arg_cong) |
307 apply (drule_tac f = Abs_hypreal in arg_cong) |
302 apply (force simp add: Rep_hypreal_inverse) |
308 apply (force simp add: Rep_hypreal_inverse) |
303 done |
309 done |
304 |
310 |
305 (**** hypreal_minus: additive inverse on hypreal ****) |
311 |
|
312 subsection{*Hyperreal Addition*} |
|
313 |
|
314 lemma hypreal_add_congruent2: |
|
315 "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" |
|
316 apply (unfold congruent2_def, auto, ultra) |
|
317 done |
|
318 |
|
319 lemma hypreal_add: |
|
320 "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = |
|
321 Abs_hypreal(hyprel``{%n. X n + Y n})" |
|
322 apply (unfold hypreal_add_def) |
|
323 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) |
|
324 done |
|
325 |
|
326 lemma hypreal_add_commute: "(z::hypreal) + w = w + z" |
|
327 apply (rule_tac z = z in eq_Abs_hypreal) |
|
328 apply (rule_tac z = w in eq_Abs_hypreal) |
|
329 apply (simp add: real_add_ac hypreal_add) |
|
330 done |
|
331 |
|
332 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" |
|
333 apply (rule_tac z = z1 in eq_Abs_hypreal) |
|
334 apply (rule_tac z = z2 in eq_Abs_hypreal) |
|
335 apply (rule_tac z = z3 in eq_Abs_hypreal) |
|
336 apply (simp add: hypreal_add real_add_assoc) |
|
337 done |
|
338 |
|
339 (*For AC rewriting*) |
|
340 lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" |
|
341 apply (rule mk_left_commute [of "op +"]) |
|
342 apply (rule hypreal_add_assoc) |
|
343 apply (rule hypreal_add_commute) |
|
344 done |
|
345 |
|
346 (* hypreal addition is an AC operator *) |
|
347 lemmas hypreal_add_ac = |
|
348 hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute |
|
349 |
|
350 lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z" |
|
351 apply (unfold hypreal_zero_def) |
|
352 apply (rule_tac z = z in eq_Abs_hypreal) |
|
353 apply (simp add: hypreal_add) |
|
354 done |
|
355 |
|
356 instance hypreal :: plus_ac0 |
|
357 by (intro_classes, |
|
358 (assumption | |
|
359 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) |
|
360 |
|
361 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z" |
|
362 by (simp add: hypreal_add_zero_left hypreal_add_commute) |
|
363 |
|
364 |
|
365 subsection{*Additive inverse on @{typ hypreal}*} |
306 |
366 |
307 lemma hypreal_minus_congruent: |
367 lemma hypreal_minus_congruent: |
308 "congruent hyprel (%X. hyprel``{%n. - (X n)})" |
368 "congruent hyprel (%X. hyprel``{%n. - (X n)})" |
309 by (force simp add: congruent_def) |
369 by (force simp add: congruent_def) |
310 |
370 |
335 lemma hypreal_minus_zero_iff [simp]: "(-x = 0) = (x = (0::hypreal))" |
395 lemma hypreal_minus_zero_iff [simp]: "(-x = 0) = (x = (0::hypreal))" |
336 apply (rule_tac z = x in eq_Abs_hypreal) |
396 apply (rule_tac z = x in eq_Abs_hypreal) |
337 apply (auto simp add: hypreal_zero_def hypreal_minus) |
397 apply (auto simp add: hypreal_zero_def hypreal_minus) |
338 done |
398 done |
339 |
399 |
340 |
400 lemma hypreal_diff: |
341 (**** hyperreal addition: hypreal_add ****) |
401 "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = |
342 |
|
343 lemma hypreal_add_congruent2: |
|
344 "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" |
|
345 apply (unfold congruent2_def, auto, ultra) |
|
346 done |
|
347 |
|
348 lemma hypreal_add: |
|
349 "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = |
|
350 Abs_hypreal(hyprel``{%n. X n + Y n})" |
|
351 apply (unfold hypreal_add_def) |
|
352 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) |
|
353 done |
|
354 |
|
355 lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = |
|
356 Abs_hypreal(hyprel``{%n. X n - Y n})" |
402 Abs_hypreal(hyprel``{%n. X n - Y n})" |
357 apply (simp add: hypreal_diff_def hypreal_minus hypreal_add) |
403 apply (simp add: hypreal_diff_def hypreal_minus hypreal_add) |
358 done |
404 done |
359 |
|
360 lemma hypreal_add_commute: "(z::hypreal) + w = w + z" |
|
361 apply (rule_tac z = z in eq_Abs_hypreal) |
|
362 apply (rule_tac z = w in eq_Abs_hypreal) |
|
363 apply (simp add: real_add_ac hypreal_add) |
|
364 done |
|
365 |
|
366 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" |
|
367 apply (rule_tac z = z1 in eq_Abs_hypreal) |
|
368 apply (rule_tac z = z2 in eq_Abs_hypreal) |
|
369 apply (rule_tac z = z3 in eq_Abs_hypreal) |
|
370 apply (simp add: hypreal_add real_add_assoc) |
|
371 done |
|
372 |
|
373 (*For AC rewriting*) |
|
374 lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" |
|
375 apply (rule mk_left_commute [of "op +"]) |
|
376 apply (rule hypreal_add_assoc) |
|
377 apply (rule hypreal_add_commute) |
|
378 done |
|
379 |
|
380 (* hypreal addition is an AC operator *) |
|
381 lemmas hypreal_add_ac = |
|
382 hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute |
|
383 |
|
384 lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z" |
|
385 apply (unfold hypreal_zero_def) |
|
386 apply (rule_tac z = z in eq_Abs_hypreal) |
|
387 apply (simp add: hypreal_add) |
|
388 done |
|
389 |
|
390 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z" |
|
391 by (simp add: hypreal_add_zero_left hypreal_add_commute) |
|
392 |
405 |
393 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)" |
406 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)" |
394 apply (unfold hypreal_zero_def) |
407 apply (unfold hypreal_zero_def) |
395 apply (rule_tac z = z in eq_Abs_hypreal) |
408 apply (rule_tac z = z in eq_Abs_hypreal) |
396 apply (simp add: hypreal_minus hypreal_add) |
409 apply (simp add: hypreal_minus hypreal_add) |
397 done |
410 done |
398 |
411 |
399 lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)" |
412 lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)" |
400 by (simp add: hypreal_add_commute hypreal_add_minus) |
413 by (simp add: hypreal_add_commute hypreal_add_minus) |
401 |
414 |
402 lemma hypreal_minus_ex: "\<exists>y. (x::hypreal) + y = 0" |
|
403 by (fast intro: hypreal_add_minus) |
|
404 |
|
405 lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0" |
|
406 apply (auto intro: hypreal_add_minus) |
|
407 apply (drule_tac f = "%x. ya+x" in arg_cong) |
|
408 apply (simp add: hypreal_add_assoc [symmetric]) |
|
409 apply (simp add: hypreal_add_commute) |
|
410 done |
|
411 |
|
412 lemma hypreal_minus_left_ex1: "EX! y. y + (x::hypreal) = 0" |
|
413 apply (auto intro: hypreal_add_minus_left) |
|
414 apply (drule_tac f = "%x. x+ya" in arg_cong) |
|
415 apply (simp add: hypreal_add_assoc) |
|
416 apply (simp add: hypreal_add_commute) |
|
417 done |
|
418 |
|
419 lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" |
|
420 apply (cut_tac z = y in hypreal_add_minus_left) |
|
421 apply (rule_tac x1 = y in hypreal_minus_left_ex1 [THEN ex1E], blast) |
|
422 done |
|
423 |
|
424 lemma hypreal_as_add_inverse_ex: "\<exists>y::hypreal. x = -y" |
|
425 apply (cut_tac x = x in hypreal_minus_ex) |
|
426 apply (erule exE, drule hypreal_add_minus_eq_minus, fast) |
|
427 done |
|
428 |
|
429 lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" |
|
430 apply (rule_tac z = x in eq_Abs_hypreal) |
|
431 apply (rule_tac z = y in eq_Abs_hypreal) |
|
432 apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib) |
|
433 done |
|
434 |
|
435 lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" |
|
436 by (simp add: hypreal_add_commute) |
|
437 |
|
438 lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" |
415 lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" |
439 apply safe |
416 apply safe |
440 apply (drule_tac f = "%t.-x + t" in arg_cong) |
417 apply (drule_tac f = "%t.-x + t" in arg_cong) |
441 apply (simp add: hypreal_add_assoc [symmetric]) |
418 apply (simp add: hypreal_add_assoc [symmetric]) |
442 done |
419 done |
528 by (subst hypreal_mult_commute, simp) |
506 by (subst hypreal_mult_commute, simp) |
529 |
507 |
530 lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" |
508 lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" |
531 by auto |
509 by auto |
532 |
510 |
533 (*----------------------------------------------------------------------------- |
511 subsection{*A few more theorems *} |
534 A few more theorems |
512 |
535 ----------------------------------------------------------------------------*) |
513 lemma hypreal_add_mult_distrib: |
536 lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
514 "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" |
537 by (simp add: hypreal_add_assoc [symmetric]) |
|
538 |
|
539 lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" |
|
540 apply (rule_tac z = z1 in eq_Abs_hypreal) |
515 apply (rule_tac z = z1 in eq_Abs_hypreal) |
541 apply (rule_tac z = z2 in eq_Abs_hypreal) |
516 apply (rule_tac z = z2 in eq_Abs_hypreal) |
542 apply (rule_tac z = w in eq_Abs_hypreal) |
517 apply (rule_tac z = w in eq_Abs_hypreal) |
543 apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) |
518 apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) |
544 done |
519 done |
545 |
520 |
546 lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" |
521 lemma hypreal_add_mult_distrib2: |
|
522 "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" |
547 by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) |
523 by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) |
548 |
524 |
549 |
525 |
550 lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" |
526 lemma hypreal_diff_mult_distrib: |
|
527 "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" |
551 |
528 |
552 apply (unfold hypreal_diff_def) |
529 apply (unfold hypreal_diff_def) |
553 apply (simp add: hypreal_add_mult_distrib) |
530 apply (simp add: hypreal_add_mult_distrib) |
554 done |
531 done |
555 |
532 |
556 lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" |
533 lemma hypreal_diff_mult_distrib2: |
|
534 "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" |
557 by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) |
535 by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) |
558 |
536 |
559 (*** one and zero are distinct ***) |
537 (*** one and zero are distinct ***) |
560 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)" |
538 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)" |
561 apply (unfold hypreal_zero_def hypreal_one_def) |
539 apply (unfold hypreal_zero_def hypreal_one_def) |
562 apply (auto simp add: real_zero_not_eq_one) |
540 apply (auto simp add: real_zero_not_eq_one) |
563 done |
541 done |
564 |
542 |
565 |
543 |
566 (**** multiplicative inverse on hypreal ****) |
544 subsection{*Multiplicative Inverse on @{typ hypreal} *} |
567 |
545 |
568 lemma hypreal_inverse_congruent: |
546 lemma hypreal_inverse_congruent: |
569 "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" |
547 "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" |
570 apply (unfold congruent_def) |
548 apply (unfold congruent_def) |
571 apply (auto, ultra) |
549 apply (auto, ultra) |
584 by (simp add: hypreal_inverse hypreal_zero_def) |
562 by (simp add: hypreal_inverse hypreal_zero_def) |
585 |
563 |
586 lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" |
564 lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" |
587 by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO) |
565 by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO) |
588 |
566 |
589 lemma hypreal_inverse_inverse [simp]: "inverse (inverse (z::hypreal)) = z" |
567 instance hypreal :: division_by_zero |
590 apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO) |
568 proof |
591 apply (rule_tac z = z in eq_Abs_hypreal) |
569 fix x :: hypreal |
592 apply (simp add: hypreal_inverse hypreal_zero_def) |
570 show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) |
593 done |
571 show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) |
594 |
572 qed |
595 lemma hypreal_inverse_1 [simp]: "inverse((1::hypreal)) = (1::hypreal)" |
573 |
596 apply (unfold hypreal_one_def) |
574 |
597 apply (simp add: hypreal_inverse real_zero_not_eq_one [THEN not_sym]) |
575 subsection{*Existence of Inverse*} |
598 done |
|
599 |
|
600 |
|
601 (*** existence of inverse ***) |
|
602 |
576 |
603 lemma hypreal_mult_inverse [simp]: |
577 lemma hypreal_mult_inverse [simp]: |
604 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
578 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
605 apply (unfold hypreal_one_def hypreal_zero_def) |
579 apply (unfold hypreal_one_def hypreal_zero_def) |
606 apply (rule_tac z = x in eq_Abs_hypreal) |
580 apply (rule_tac z = x in eq_Abs_hypreal) |
607 apply (simp add: hypreal_inverse hypreal_mult) |
581 apply (simp add: hypreal_inverse hypreal_mult) |
608 apply (drule FreeUltrafilterNat_Compl_mem) |
582 apply (drule FreeUltrafilterNat_Compl_mem) |
609 apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) |
583 apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) |
610 done |
584 done |
611 |
585 |
612 lemma hypreal_mult_inverse_left [simp]: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)" |
586 lemma hypreal_mult_inverse_left [simp]: |
|
587 "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)" |
613 by (simp add: hypreal_mult_inverse hypreal_mult_commute) |
588 by (simp add: hypreal_mult_inverse hypreal_mult_commute) |
614 |
589 |
615 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
590 |
616 apply auto |
591 subsection{*Theorems for Ordering*} |
617 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
592 |
618 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
593 text{*TODO: define @{text "\<le>"} as the primitive concept and quickly |
619 done |
594 establish membership in class @{text linorder}. Then proofs could be |
620 |
595 simplified, since properties of @{text "<"} would be generic.*} |
621 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
596 |
622 apply safe |
597 text{*TODO: The following theorem should be used througout the proofs |
623 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
598 as it probably makes many of them more straightforward.*} |
624 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
599 lemma hypreal_less: |
625 done |
600 "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) = |
626 |
601 ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
627 lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0" |
602 apply (unfold hypreal_less_def) |
628 apply (unfold hypreal_zero_def) |
603 apply (auto intro!: lemma_hyprel_refl, ultra) |
629 apply (rule_tac z = x in eq_Abs_hypreal) |
604 done |
630 apply (simp add: hypreal_inverse hypreal_mult) |
|
631 done |
|
632 |
|
633 |
|
634 lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)" |
|
635 apply safe |
|
636 apply (drule_tac f = "%z. inverse x*z" in arg_cong) |
|
637 apply (simp add: hypreal_mult_assoc [symmetric]) |
|
638 done |
|
639 |
|
640 lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0" |
|
641 by (auto intro: ccontr dest: hypreal_mult_not_0) |
|
642 |
|
643 lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" |
|
644 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
|
645 apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1], simp) |
|
646 apply (subst hypreal_mult_inverse_left, auto) |
|
647 done |
|
648 |
|
649 lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" |
|
650 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
|
651 apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO) |
|
652 apply (frule_tac y = y in hypreal_mult_not_0, assumption) |
|
653 apply (rule_tac c1 = x in hypreal_mult_left_cancel [THEN iffD1]) |
|
654 apply (auto simp add: hypreal_mult_assoc [symmetric]) |
|
655 apply (rule_tac c1 = y in hypreal_mult_left_cancel [THEN iffD1]) |
|
656 apply (auto simp add: hypreal_mult_left_commute) |
|
657 apply (simp add: hypreal_mult_assoc [symmetric]) |
|
658 done |
|
659 |
|
660 (*------------------------------------------------------------------ |
|
661 Theorems for ordering |
|
662 ------------------------------------------------------------------*) |
|
663 |
605 |
664 (* prove introduction and elimination rules for hypreal_less *) |
606 (* prove introduction and elimination rules for hypreal_less *) |
665 |
|
666 lemma hypreal_less_iff: |
|
667 "(P < (Q::hypreal)) = (\<exists>X Y. X \<in> Rep_hypreal(P) & |
|
668 Y \<in> Rep_hypreal(Q) & |
|
669 {n. X n < Y n} \<in> FreeUltrafilterNat)" |
|
670 |
|
671 apply (unfold hypreal_less_def, fast) |
|
672 done |
|
673 |
|
674 lemma hypreal_lessI: |
|
675 "[| {n. X n < Y n} \<in> FreeUltrafilterNat; |
|
676 X \<in> Rep_hypreal(P); |
|
677 Y \<in> Rep_hypreal(Q) |] ==> P < (Q::hypreal)" |
|
678 apply (unfold hypreal_less_def, fast) |
|
679 done |
|
680 |
|
681 |
|
682 lemma hypreal_lessE: |
|
683 "!! R1. [| R1 < (R2::hypreal); |
|
684 !!X Y. {n. X n < Y n} \<in> FreeUltrafilterNat ==> P; |
|
685 !!X. X \<in> Rep_hypreal(R1) ==> P; |
|
686 !!Y. Y \<in> Rep_hypreal(R2) ==> P |] |
|
687 ==> P" |
|
688 |
|
689 apply (unfold hypreal_less_def, auto) |
|
690 done |
|
691 |
|
692 lemma hypreal_lessD: |
|
693 "R1 < (R2::hypreal) ==> (\<exists>X Y. {n. X n < Y n} \<in> FreeUltrafilterNat & |
|
694 X \<in> Rep_hypreal(R1) & |
|
695 Y \<in> Rep_hypreal(R2))" |
|
696 apply (unfold hypreal_less_def, fast) |
|
697 done |
|
698 |
607 |
699 lemma hypreal_less_not_refl: "~ (R::hypreal) < R" |
608 lemma hypreal_less_not_refl: "~ (R::hypreal) < R" |
700 apply (rule_tac z = R in eq_Abs_hypreal) |
609 apply (rule_tac z = R in eq_Abs_hypreal) |
701 apply (auto simp add: hypreal_less_def, ultra) |
610 apply (auto simp add: hypreal_less_def, ultra) |
702 done |
611 done |
703 |
612 |
704 (*** y < y ==> P ***) |
|
705 lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] |
613 lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] |
706 declare hypreal_less_irrefl [elim!] |
614 declare hypreal_less_irrefl [elim!] |
707 |
615 |
708 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
616 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
709 by (auto simp add: hypreal_less_not_refl) |
617 by (auto simp add: hypreal_less_not_refl) |
718 lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P" |
626 lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P" |
719 apply (drule hypreal_less_trans, assumption) |
627 apply (drule hypreal_less_trans, assumption) |
720 apply (simp add: hypreal_less_not_refl) |
628 apply (simp add: hypreal_less_not_refl) |
721 done |
629 done |
722 |
630 |
723 (*------------------------------------------------------- |
631 |
724 TODO: The following theorem should have been proved |
632 subsection{*Trichotomy: the hyperreals are Linearly Ordered*} |
725 first and then used througout the proofs as it probably |
|
726 makes many of them more straightforward. |
|
727 -------------------------------------------------------*) |
|
728 lemma hypreal_less: |
|
729 "(Abs_hypreal(hyprel``{%n. X n}) < |
|
730 Abs_hypreal(hyprel``{%n. Y n})) = |
|
731 ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
|
732 apply (unfold hypreal_less_def) |
|
733 apply (auto intro!: lemma_hyprel_refl, ultra) |
|
734 done |
|
735 |
|
736 (*---------------------------------------------------------------------------- |
|
737 Trichotomy: the hyperreals are linearly ordered |
|
738 ---------------------------------------------------------------------------*) |
|
739 |
633 |
740 lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}" |
634 lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}" |
741 |
|
742 apply (unfold hyprel_def) |
635 apply (unfold hyprel_def) |
743 apply (rule_tac x = "%n. 0" in exI, safe) |
636 apply (rule_tac x = "%n. 0" in exI, safe) |
744 apply (auto intro!: FreeUltrafilterNat_Nat_set) |
637 apply (auto intro!: FreeUltrafilterNat_Nat_set) |
745 done |
638 done |
746 |
639 |
787 lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" |
678 lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" |
788 apply auto |
679 apply auto |
789 apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto) |
680 apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto) |
790 done |
681 done |
791 |
682 |
792 (* 07/00 *) |
683 |
793 lemma hypreal_diff_zero [simp]: "(0::hypreal) - x = -x" |
684 subsection{*Linearity*} |
794 by (simp add: hypreal_diff_def) |
|
795 |
|
796 lemma hypreal_diff_zero_right [simp]: "x - (0::hypreal) = x" |
|
797 by (simp add: hypreal_diff_def) |
|
798 |
|
799 lemma hypreal_diff_self [simp]: "x - x = (0::hypreal)" |
|
800 by (simp add: hypreal_diff_def) |
|
801 |
|
802 lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" |
|
803 by (auto simp add: hypreal_add_assoc) |
|
804 |
|
805 lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))" |
|
806 by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) |
|
807 |
|
808 |
|
809 (*** linearity ***) |
|
810 |
685 |
811 lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" |
686 lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" |
812 apply (subst hypreal_eq_minus_iff2) |
687 apply (subst hypreal_eq_minus_iff2) |
813 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
688 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
814 apply (rule_tac x1 = y in hypreal_less_minus_iff2 [THEN ssubst]) |
689 apply (rule_tac x1 = y in hypreal_less_minus_iff2 [THEN ssubst]) |
821 lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P; x = y ==> P; |
696 lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P; x = y ==> P; |
822 y < x ==> P |] ==> P" |
697 y < x ==> P |] ==> P" |
823 apply (cut_tac x = x and y = y in hypreal_linear, auto) |
698 apply (cut_tac x = x and y = y in hypreal_linear, auto) |
824 done |
699 done |
825 |
700 |
826 (*------------------------------------------------------------------------------ |
701 |
827 Properties of <= |
702 subsection{*Properties of The @{text "\<le>"} Relation*} |
828 ------------------------------------------------------------------------------*) |
|
829 (*------ hypreal le iff reals le a.e ------*) |
|
830 |
703 |
831 lemma hypreal_le: |
704 lemma hypreal_le: |
832 "(Abs_hypreal(hyprel``{%n. X n}) <= |
705 "(Abs_hypreal(hyprel``{%n. X n}) <= |
833 Abs_hypreal(hyprel``{%n. Y n})) = |
706 Abs_hypreal(hyprel``{%n. Y n})) = |
834 ({n. X n <= Y n} \<in> FreeUltrafilterNat)" |
707 ({n. X n <= Y n} \<in> FreeUltrafilterNat)" |
835 apply (unfold hypreal_le_def real_le_def) |
708 apply (unfold hypreal_le_def real_le_def) |
836 apply (auto simp add: hypreal_less) |
709 apply (auto simp add: hypreal_less) |
837 apply (ultra+) |
710 apply (ultra+) |
838 done |
711 done |
839 |
712 |
840 (*---------------------------------------------------------*) |
|
841 (*---------------------------------------------------------*) |
|
842 lemma hypreal_leI: |
713 lemma hypreal_leI: |
843 "~(w < z) ==> z <= (w::hypreal)" |
714 "~(w < z) ==> z <= (w::hypreal)" |
844 apply (unfold hypreal_le_def, assumption) |
715 apply (unfold hypreal_le_def, assumption) |
845 done |
716 done |
846 |
717 |
892 apply (drule hypreal_le_imp_less_or_eq) |
763 apply (drule hypreal_le_imp_less_or_eq) |
893 apply (drule hypreal_le_imp_less_or_eq) |
764 apply (drule hypreal_le_imp_less_or_eq) |
894 apply (fast elim: hypreal_less_irrefl hypreal_less_asym) |
765 apply (fast elim: hypreal_less_irrefl hypreal_less_asym) |
895 done |
766 done |
896 |
767 |
897 lemma not_less_not_eq_hypreal_less: "[| ~ y < x; y \<noteq> x |] ==> x < (y::hypreal)" |
|
898 apply (rule not_hypreal_leE) |
|
899 apply (fast dest: hypreal_le_imp_less_or_eq) |
|
900 done |
|
901 |
|
902 (* Axiom 'order_less_le' of class 'order': *) |
768 (* Axiom 'order_less_le' of class 'order': *) |
903 lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)" |
769 lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)" |
904 apply (simp add: hypreal_le_def hypreal_neq_iff) |
770 apply (simp add: hypreal_le_def hypreal_neq_iff) |
905 apply (blast intro: hypreal_less_asym) |
771 apply (blast intro: hypreal_less_asym) |
906 done |
772 done |
907 |
773 |
|
774 instance hypreal :: order |
|
775 by (intro_classes, |
|
776 (assumption | |
|
777 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym |
|
778 hypreal_less_le)+) |
|
779 |
|
780 instance hypreal :: linorder |
|
781 by (intro_classes, rule hypreal_le_linear) |
|
782 |
908 lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))" |
783 lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))" |
909 apply (rule_tac z = R in eq_Abs_hypreal) |
784 apply (rule_tac z = R in eq_Abs_hypreal) |
910 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
785 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
911 done |
786 done |
912 |
787 |
923 lemma hypreal_minus_zero_le_iff2 [simp]: "(-r <= (0::hypreal)) = (0 <= r)" |
798 lemma hypreal_minus_zero_le_iff2 [simp]: "(-r <= (0::hypreal)) = (0 <= r)" |
924 apply (unfold hypreal_le_def) |
799 apply (unfold hypreal_le_def) |
925 apply (simp add: hypreal_minus_zero_less_iff2) |
800 apply (simp add: hypreal_minus_zero_less_iff2) |
926 done |
801 done |
927 |
802 |
928 (*---------------------------------------------------------- |
803 |
929 hypreal_of_real preserves field and order properties |
804 lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" |
930 -----------------------------------------------------------*) |
805 apply (rule_tac z = x in eq_Abs_hypreal) |
|
806 apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) |
|
807 done |
|
808 |
|
809 lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" |
|
810 apply (rule_tac z = x in eq_Abs_hypreal) |
|
811 apply (auto simp add: hypreal_add hypreal_zero_def) |
|
812 done |
|
813 |
|
814 lemma hypreal_add_self_zero_cancel2 [simp]: |
|
815 "(x + x + y = y) = (x = (0::hypreal))" |
|
816 apply auto |
|
817 apply (drule hypreal_eq_minus_iff [THEN iffD1]) |
|
818 apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) |
|
819 done |
|
820 |
|
821 lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" |
|
822 by auto |
|
823 |
|
824 lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" |
|
825 by (simp add: hypreal_minus_eq_swap) |
|
826 |
|
827 lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" |
|
828 apply (rule_tac z = A in eq_Abs_hypreal) |
|
829 apply (rule_tac z = B in eq_Abs_hypreal) |
|
830 apply (rule_tac z = C in eq_Abs_hypreal) |
|
831 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
|
832 done |
|
833 |
|
834 lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" |
|
835 apply (unfold hypreal_zero_def) |
|
836 apply (rule_tac z = x in eq_Abs_hypreal) |
|
837 apply (rule_tac z = y in eq_Abs_hypreal) |
|
838 apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) |
|
839 apply (auto intro: real_mult_order) |
|
840 done |
|
841 |
|
842 lemma hypreal_add_left_le_mono1: "(q1::hypreal) \<le> q2 ==> x + q1 \<le> x + q2" |
|
843 apply (drule order_le_imp_less_or_eq) |
|
844 apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
845 done |
|
846 |
|
847 lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" |
|
848 apply (rotate_tac 1) |
|
849 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
850 apply (rule hypreal_less_minus_iff [THEN iffD2]) |
|
851 apply (drule hypreal_mult_order, assumption) |
|
852 apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute) |
|
853 done |
|
854 |
|
855 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y" |
|
856 apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1) |
|
857 done |
|
858 |
|
859 subsection{*The Hyperreals Form an Ordered Field*} |
|
860 |
|
861 instance hypreal :: inverse .. |
|
862 |
|
863 instance hypreal :: ordered_field |
|
864 proof |
|
865 fix x y z :: hypreal |
|
866 show "(x + y) + z = x + (y + z)" by (rule hypreal_add_assoc) |
|
867 show "x + y = y + x" by (rule hypreal_add_commute) |
|
868 show "0 + x = x" by simp |
|
869 show "- x + x = 0" by simp |
|
870 show "x - y = x + (-y)" by (simp add: hypreal_diff_def) |
|
871 show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc) |
|
872 show "x * y = y * x" by (rule hypreal_mult_commute) |
|
873 show "1 * x = x" by simp |
|
874 show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib) |
|
875 show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one) |
|
876 show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1) |
|
877 show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2) |
|
878 show "\<bar>x\<bar> = (if x < 0 then -x else x)" |
|
879 by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) |
|
880 show "x \<noteq> 0 ==> inverse x * x = 1" by simp |
|
881 show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) |
|
882 qed |
|
883 |
|
884 lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" |
|
885 by (rule Ring_and_Field.minus_add_distrib) |
|
886 |
|
887 (*Used ONCE: in NSA.ML*) |
|
888 lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" |
|
889 by (simp add: hypreal_add_commute) |
|
890 |
|
891 (*Used ONCE: in Lim.ML*) |
|
892 lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" |
|
893 by (auto simp add: hypreal_add_assoc) |
|
894 |
|
895 lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))" |
|
896 by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) |
|
897 |
|
898 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
|
899 apply auto |
|
900 done |
|
901 |
|
902 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
|
903 apply auto |
|
904 done |
|
905 |
|
906 lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0" |
|
907 by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) |
|
908 |
|
909 lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)" |
|
910 by simp |
|
911 |
|
912 lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" |
|
913 by (rule Ring_and_Field.inverse_minus_eq) |
|
914 |
|
915 lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" |
|
916 by (rule Ring_and_Field.inverse_mult_distrib) |
|
917 |
|
918 |
|
919 subsection{* Division lemmas *} |
|
920 |
|
921 lemma hypreal_divide_one: "x/(1::hypreal) = x" |
|
922 by (simp add: hypreal_divide_def) |
|
923 |
|
924 |
|
925 (** As with multiplication, pull minus signs OUT of the / operator **) |
|
926 |
|
927 lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" |
|
928 by (rule Ring_and_Field.add_divide_distrib) |
|
929 |
|
930 lemma hypreal_inverse_add: |
|
931 "[|(x::hypreal) \<noteq> 0; y \<noteq> 0 |] |
|
932 ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" |
|
933 by (simp add: Ring_and_Field.inverse_add mult_assoc) |
|
934 |
|
935 |
|
936 subsection{*@{term hypreal_of_real} Preserves Field and Order Properties*} |
|
937 |
931 lemma hypreal_of_real_add [simp]: |
938 lemma hypreal_of_real_add [simp]: |
932 "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" |
939 "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" |
933 apply (unfold hypreal_of_real_def) |
940 apply (unfold hypreal_of_real_def) |
934 apply (simp add: hypreal_add hypreal_add_mult_distrib) |
941 apply (simp add: hypreal_add hypreal_add_mult_distrib) |
935 done |
942 done |
968 by (unfold hypreal_of_real_def hypreal_zero_def, simp) |
977 by (unfold hypreal_of_real_def hypreal_zero_def, simp) |
969 |
978 |
970 lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" |
979 lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" |
971 by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) |
980 by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) |
972 |
981 |
973 lemma hypreal_of_real_inverse [simp]: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" |
982 lemma hypreal_of_real_inverse [simp]: |
|
983 "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" |
974 apply (case_tac "r=0") |
984 apply (case_tac "r=0") |
975 apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) |
985 apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) |
976 apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) |
986 apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) |
977 apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) |
987 apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) |
978 done |
988 done |
979 |
989 |
980 lemma hypreal_of_real_divide [simp]: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" |
990 lemma hypreal_of_real_divide [simp]: |
|
991 "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" |
981 by (simp add: hypreal_divide_def real_divide_def) |
992 by (simp add: hypreal_divide_def real_divide_def) |
982 |
993 |
983 |
994 |
984 (*** Division lemmas ***) |
995 subsection{*Misc Others*} |
985 |
|
986 lemma hypreal_zero_divide: "(0::hypreal)/x = 0" |
|
987 by (simp add: hypreal_divide_def) |
|
988 |
|
989 lemma hypreal_divide_one: "x/(1::hypreal) = x" |
|
990 by (simp add: hypreal_divide_def) |
|
991 declare hypreal_zero_divide [simp] hypreal_divide_one [simp] |
|
992 |
|
993 lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y" |
|
994 by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) |
|
995 |
|
996 lemma hypreal_divide_divide2_eq [simp]: "((x::hypreal) / y) / z = x/(y*z)" |
|
997 by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc) |
|
998 |
|
999 |
|
1000 (** As with multiplication, pull minus signs OUT of the / operator **) |
|
1001 |
|
1002 lemma hypreal_minus_divide_eq [simp]: "(-x) / (y::hypreal) = - (x/y)" |
|
1003 by (simp add: hypreal_divide_def) |
|
1004 |
|
1005 lemma hypreal_divide_minus_eq [simp]: "(x / -(y::hypreal)) = - (x/y)" |
|
1006 by (simp add: hypreal_divide_def hypreal_minus_inverse) |
|
1007 |
|
1008 lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" |
|
1009 by (simp add: hypreal_divide_def hypreal_add_mult_distrib) |
|
1010 |
|
1011 lemma hypreal_inverse_add: "[|(x::hypreal) \<noteq> 0; y \<noteq> 0 |] |
|
1012 ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" |
|
1013 apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric]) |
|
1014 apply (subst hypreal_mult_assoc) |
|
1015 apply (rule hypreal_mult_left_commute [THEN subst]) |
|
1016 apply (simp add: hypreal_add_commute) |
|
1017 done |
|
1018 |
|
1019 lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" |
|
1020 apply (rule_tac z = x in eq_Abs_hypreal) |
|
1021 apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) |
|
1022 done |
|
1023 |
|
1024 lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" |
|
1025 apply (rule_tac z = x in eq_Abs_hypreal) |
|
1026 apply (auto simp add: hypreal_add hypreal_zero_def) |
|
1027 done |
|
1028 |
|
1029 lemma hypreal_add_self_zero_cancel2 [simp]: "(x + x + y = y) = (x = (0::hypreal))" |
|
1030 apply auto |
|
1031 apply (drule hypreal_eq_minus_iff [THEN iffD1]) |
|
1032 apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) |
|
1033 done |
|
1034 |
|
1035 lemma hypreal_add_self_zero_cancel2a [simp]: "(x + (x + y) = y) = (x = (0::hypreal))" |
|
1036 by (simp add: hypreal_add_assoc [symmetric]) |
|
1037 |
|
1038 lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" |
|
1039 by auto |
|
1040 |
|
1041 lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" |
|
1042 by (simp add: hypreal_minus_eq_swap) |
|
1043 |
|
1044 lemma hypreal_less_eq_diff: "(x<y) = (x-y < (0::hypreal))" |
|
1045 apply (unfold hypreal_diff_def) |
|
1046 apply (rule hypreal_less_minus_iff2) |
|
1047 done |
|
1048 |
|
1049 (*** Subtraction laws ***) |
|
1050 |
|
1051 lemma hypreal_add_diff_eq: "x + (y - z) = (x + y) - (z::hypreal)" |
|
1052 by (simp add: hypreal_diff_def hypreal_add_ac) |
|
1053 |
|
1054 lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)" |
|
1055 by (simp add: hypreal_diff_def hypreal_add_ac) |
|
1056 |
|
1057 lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))" |
|
1058 by (simp add: hypreal_diff_def hypreal_add_ac) |
|
1059 |
|
1060 lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)" |
|
1061 by (simp add: hypreal_diff_def hypreal_add_ac) |
|
1062 |
|
1063 lemma hypreal_diff_less_eq: "(x-y < z) = (x < z + (y::hypreal))" |
|
1064 apply (subst hypreal_less_eq_diff) |
|
1065 apply (rule_tac y1 = z in hypreal_less_eq_diff [THEN ssubst]) |
|
1066 apply (simp add: hypreal_diff_def hypreal_add_ac) |
|
1067 done |
|
1068 |
|
1069 lemma hypreal_less_diff_eq: "(x < z-y) = (x + (y::hypreal) < z)" |
|
1070 apply (subst hypreal_less_eq_diff) |
|
1071 apply (rule_tac y1 = "z-y" in hypreal_less_eq_diff [THEN ssubst]) |
|
1072 apply (simp add: hypreal_diff_def hypreal_add_ac) |
|
1073 done |
|
1074 |
|
1075 lemma hypreal_diff_le_eq: "(x-y <= z) = (x <= z + (y::hypreal))" |
|
1076 apply (unfold hypreal_le_def) |
|
1077 apply (simp add: hypreal_less_diff_eq) |
|
1078 done |
|
1079 |
|
1080 lemma hypreal_le_diff_eq: "(x <= z-y) = (x + (y::hypreal) <= z)" |
|
1081 apply (unfold hypreal_le_def) |
|
1082 apply (simp add: hypreal_diff_less_eq) |
|
1083 done |
|
1084 |
|
1085 lemma hypreal_diff_eq_eq: "(x-y = z) = (x = z + (y::hypreal))" |
|
1086 apply (unfold hypreal_diff_def) |
|
1087 apply (auto simp add: hypreal_add_assoc) |
|
1088 done |
|
1089 |
|
1090 lemma hypreal_eq_diff_eq: "(x = z-y) = (x + (y::hypreal) = z)" |
|
1091 apply (unfold hypreal_diff_def) |
|
1092 apply (auto simp add: hypreal_add_assoc) |
|
1093 done |
|
1094 |
|
1095 |
|
1096 (** For the cancellation simproc. |
|
1097 The idea is to cancel like terms on opposite sides by subtraction **) |
|
1098 |
|
1099 lemma hypreal_less_eqI: "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')" |
|
1100 apply (subst hypreal_less_eq_diff) |
|
1101 apply (rule_tac y1 = y in hypreal_less_eq_diff [THEN ssubst], simp) |
|
1102 done |
|
1103 |
|
1104 lemma hypreal_le_eqI: "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')" |
|
1105 apply (drule hypreal_less_eqI) |
|
1106 apply (simp add: hypreal_le_def) |
|
1107 done |
|
1108 |
|
1109 lemma hypreal_eq_eqI: "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')" |
|
1110 apply safe |
|
1111 apply (simp_all add: hypreal_eq_diff_eq hypreal_diff_eq_eq) |
|
1112 done |
|
1113 |
996 |
1114 lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})" |
997 lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})" |
1115 by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric]) |
998 by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric]) |
1116 |
999 |
1117 lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})" |
1000 lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})" |
1187 val hypreal_add_left_commute = thm "hypreal_add_left_commute"; |
1081 val hypreal_add_left_commute = thm "hypreal_add_left_commute"; |
1188 val hypreal_add_zero_left = thm "hypreal_add_zero_left"; |
1082 val hypreal_add_zero_left = thm "hypreal_add_zero_left"; |
1189 val hypreal_add_zero_right = thm "hypreal_add_zero_right"; |
1083 val hypreal_add_zero_right = thm "hypreal_add_zero_right"; |
1190 val hypreal_add_minus = thm "hypreal_add_minus"; |
1084 val hypreal_add_minus = thm "hypreal_add_minus"; |
1191 val hypreal_add_minus_left = thm "hypreal_add_minus_left"; |
1085 val hypreal_add_minus_left = thm "hypreal_add_minus_left"; |
1192 val hypreal_minus_ex = thm "hypreal_minus_ex"; |
|
1193 val hypreal_minus_ex1 = thm "hypreal_minus_ex1"; |
|
1194 val hypreal_minus_left_ex1 = thm "hypreal_minus_left_ex1"; |
|
1195 val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; |
|
1196 val hypreal_as_add_inverse_ex = thm "hypreal_as_add_inverse_ex"; |
|
1197 val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib"; |
1086 val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib"; |
1198 val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1"; |
1087 val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1"; |
1199 val hypreal_add_left_cancel = thm "hypreal_add_left_cancel"; |
1088 val hypreal_add_left_cancel = thm "hypreal_add_left_cancel"; |
1200 val hypreal_add_right_cancel = thm "hypreal_add_right_cancel"; |
1089 val hypreal_add_right_cancel = thm "hypreal_add_right_cancel"; |
1201 val hypreal_add_minus_cancelA = thm "hypreal_add_minus_cancelA"; |
1090 val hypreal_add_minus_cancelA = thm "hypreal_add_minus_cancelA"; |
1212 val hypreal_minus_mult_eq1 = thm "hypreal_minus_mult_eq1"; |
1101 val hypreal_minus_mult_eq1 = thm "hypreal_minus_mult_eq1"; |
1213 val hypreal_minus_mult_eq2 = thm "hypreal_minus_mult_eq2"; |
1102 val hypreal_minus_mult_eq2 = thm "hypreal_minus_mult_eq2"; |
1214 val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1"; |
1103 val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1"; |
1215 val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right"; |
1104 val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right"; |
1216 val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute"; |
1105 val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute"; |
1217 val hypreal_add_assoc_cong = thm "hypreal_add_assoc_cong"; |
|
1218 val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib"; |
1106 val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib"; |
1219 val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2"; |
1107 val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2"; |
1220 val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib"; |
1108 val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib"; |
1221 val hypreal_diff_mult_distrib2 = thm "hypreal_diff_mult_distrib2"; |
1109 val hypreal_diff_mult_distrib2 = thm "hypreal_diff_mult_distrib2"; |
1222 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one"; |
1110 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one"; |
1223 val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; |
1111 val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; |
1224 val hypreal_inverse = thm "hypreal_inverse"; |
1112 val hypreal_inverse = thm "hypreal_inverse"; |
1225 val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO"; |
1113 val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO"; |
1226 val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO"; |
1114 val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO"; |
1227 val hypreal_inverse_inverse = thm "hypreal_inverse_inverse"; |
|
1228 val hypreal_inverse_1 = thm "hypreal_inverse_1"; |
|
1229 val hypreal_mult_inverse = thm "hypreal_mult_inverse"; |
1115 val hypreal_mult_inverse = thm "hypreal_mult_inverse"; |
1230 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left"; |
1116 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left"; |
1231 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; |
1117 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; |
1232 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; |
1118 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; |
1233 val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero"; |
1119 val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero"; |
1234 val hypreal_mult_not_0 = thm "hypreal_mult_not_0"; |
1120 val hypreal_mult_not_0 = thm "hypreal_mult_not_0"; |
1235 val hypreal_mult_zero_disj = thm "hypreal_mult_zero_disj"; |
|
1236 val hypreal_minus_inverse = thm "hypreal_minus_inverse"; |
1121 val hypreal_minus_inverse = thm "hypreal_minus_inverse"; |
1237 val hypreal_inverse_distrib = thm "hypreal_inverse_distrib"; |
1122 val hypreal_inverse_distrib = thm "hypreal_inverse_distrib"; |
1238 val hypreal_less_iff = thm "hypreal_less_iff"; |
|
1239 val hypreal_lessI = thm "hypreal_lessI"; |
|
1240 val hypreal_lessE = thm "hypreal_lessE"; |
|
1241 val hypreal_lessD = thm "hypreal_lessD"; |
|
1242 val hypreal_less_not_refl = thm "hypreal_less_not_refl"; |
1123 val hypreal_less_not_refl = thm "hypreal_less_not_refl"; |
1243 val hypreal_not_refl2 = thm "hypreal_not_refl2"; |
1124 val hypreal_not_refl2 = thm "hypreal_not_refl2"; |
1244 val hypreal_less_trans = thm "hypreal_less_trans"; |
1125 val hypreal_less_trans = thm "hypreal_less_trans"; |
1245 val hypreal_less_asym = thm "hypreal_less_asym"; |
1126 val hypreal_less_asym = thm "hypreal_less_asym"; |
1246 val hypreal_less = thm "hypreal_less"; |
1127 val hypreal_less = thm "hypreal_less"; |
1247 val hypreal_trichotomy = thm "hypreal_trichotomy"; |
1128 val hypreal_trichotomy = thm "hypreal_trichotomy"; |
1248 val hypreal_trichotomyE = thm "hypreal_trichotomyE"; |
|
1249 val hypreal_less_minus_iff = thm "hypreal_less_minus_iff"; |
1129 val hypreal_less_minus_iff = thm "hypreal_less_minus_iff"; |
1250 val hypreal_less_minus_iff2 = thm "hypreal_less_minus_iff2"; |
1130 val hypreal_less_minus_iff2 = thm "hypreal_less_minus_iff2"; |
1251 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; |
1131 val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; |
1252 val hypreal_eq_minus_iff2 = thm "hypreal_eq_minus_iff2"; |
1132 val hypreal_eq_minus_iff2 = thm "hypreal_eq_minus_iff2"; |
1253 val hypreal_diff_zero = thm "hypreal_diff_zero"; |
|
1254 val hypreal_diff_zero_right = thm "hypreal_diff_zero_right"; |
|
1255 val hypreal_diff_self = thm "hypreal_diff_self"; |
|
1256 val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3"; |
1133 val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3"; |
1257 val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff"; |
1134 val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff"; |
1258 val hypreal_linear = thm "hypreal_linear"; |
1135 val hypreal_linear = thm "hypreal_linear"; |
1259 val hypreal_neq_iff = thm "hypreal_neq_iff"; |
1136 val hypreal_neq_iff = thm "hypreal_neq_iff"; |
1260 val hypreal_linear_less2 = thm "hypreal_linear_less2"; |
1137 val hypreal_linear_less2 = thm "hypreal_linear_less2"; |
1285 val hypreal_of_real_one = thm "hypreal_of_real_one"; |
1161 val hypreal_of_real_one = thm "hypreal_of_real_one"; |
1286 val hypreal_of_real_zero = thm "hypreal_of_real_zero"; |
1162 val hypreal_of_real_zero = thm "hypreal_of_real_zero"; |
1287 val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff"; |
1163 val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff"; |
1288 val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; |
1164 val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; |
1289 val hypreal_of_real_divide = thm "hypreal_of_real_divide"; |
1165 val hypreal_of_real_divide = thm "hypreal_of_real_divide"; |
1290 val hypreal_zero_divide = thm "hypreal_zero_divide"; |
|
1291 val hypreal_divide_one = thm "hypreal_divide_one"; |
1166 val hypreal_divide_one = thm "hypreal_divide_one"; |
1292 val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq"; |
|
1293 val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq"; |
|
1294 val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq"; |
|
1295 val hypreal_divide_minus_eq = thm "hypreal_divide_minus_eq"; |
|
1296 val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib"; |
1167 val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib"; |
1297 val hypreal_inverse_add = thm "hypreal_inverse_add"; |
1168 val hypreal_inverse_add = thm "hypreal_inverse_add"; |
1298 val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero"; |
1169 val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero"; |
1299 val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel"; |
1170 val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel"; |
1300 val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2"; |
1171 val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2"; |
1301 val hypreal_add_self_zero_cancel2a = thm "hypreal_add_self_zero_cancel2a"; |
|
1302 val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap"; |
1172 val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap"; |
1303 val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel"; |
1173 val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel"; |
1304 val hypreal_less_eq_diff = thm "hypreal_less_eq_diff"; |
|
1305 val hypreal_add_diff_eq = thm "hypreal_add_diff_eq"; |
|
1306 val hypreal_diff_add_eq = thm "hypreal_diff_add_eq"; |
|
1307 val hypreal_diff_diff_eq = thm "hypreal_diff_diff_eq"; |
|
1308 val hypreal_diff_diff_eq2 = thm "hypreal_diff_diff_eq2"; |
|
1309 val hypreal_diff_less_eq = thm "hypreal_diff_less_eq"; |
|
1310 val hypreal_less_diff_eq = thm "hypreal_less_diff_eq"; |
|
1311 val hypreal_diff_le_eq = thm "hypreal_diff_le_eq"; |
|
1312 val hypreal_le_diff_eq = thm "hypreal_le_diff_eq"; |
|
1313 val hypreal_diff_eq_eq = thm "hypreal_diff_eq_eq"; |
|
1314 val hypreal_eq_diff_eq = thm "hypreal_eq_diff_eq"; |
|
1315 val hypreal_less_eqI = thm "hypreal_less_eqI"; |
|
1316 val hypreal_le_eqI = thm "hypreal_le_eqI"; |
|
1317 val hypreal_eq_eqI = thm "hypreal_eq_eqI"; |
|
1318 val hypreal_zero_num = thm "hypreal_zero_num"; |
1174 val hypreal_zero_num = thm "hypreal_zero_num"; |
1319 val hypreal_one_num = thm "hypreal_one_num"; |
1175 val hypreal_one_num = thm "hypreal_one_num"; |
1320 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; |
1176 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; |
1321 *} |
1177 *} |
1322 |
1178 |