89 ------------------------------------------------------------------------*) |
89 ------------------------------------------------------------------------*) |
90 |
90 |
91 (*** based on James' proof that the set of naturals is not finite ***) |
91 (*** 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)" |
92 lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)" |
93 apply (rule impI) |
93 apply (rule impI) |
94 apply (erule_tac F = "A" in finite_induct) |
94 apply (erule_tac F = A in finite_induct) |
95 apply (blast , erule exE) |
95 apply (blast, erule exE) |
96 apply (rule_tac x = "n + x" in exI) |
96 apply (rule_tac x = "n + x" in exI) |
97 apply (rule allI , erule_tac x = "x + m" in allE) |
97 apply (rule allI, erule_tac x = "x + m" in allE) |
98 apply (auto simp add: add_ac) |
98 apply (auto simp add: add_ac) |
99 done |
99 done |
100 |
100 |
101 lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\<exists>n. n \<notin>A)" |
101 lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\<exists>n. n \<notin>A)" |
102 apply (rule impI , drule finite_exhausts) |
102 by (rule impI, drule finite_exhausts, blast) |
103 apply blast |
|
104 done |
|
105 |
103 |
106 lemma not_finite_nat: "~ finite(UNIV:: nat set)" |
104 lemma not_finite_nat: "~ finite(UNIV:: nat set)" |
107 apply (fast dest!: finite_exhausts) |
105 by (fast dest!: finite_exhausts) |
108 done |
|
109 |
106 |
110 (*------------------------------------------------------------------------ |
107 (*------------------------------------------------------------------------ |
111 Existence of free ultrafilter over the naturals and proof of various |
108 Existence of free ultrafilter over the naturals and proof of various |
112 properties of the FreeUltrafilterNat- an arbitrary free ultrafilter |
109 properties of the FreeUltrafilterNat- an arbitrary free ultrafilter |
113 ------------------------------------------------------------------------*) |
110 ------------------------------------------------------------------------*) |
114 |
111 |
115 lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)" |
112 lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)" |
116 apply (rule not_finite_nat [THEN FreeUltrafilter_Ex]) |
113 by (rule not_finite_nat [THEN FreeUltrafilter_Ex]) |
117 done |
114 |
118 |
115 lemma FreeUltrafilterNat_mem [simp]: |
119 lemma FreeUltrafilterNat_mem: |
|
120 "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)" |
116 "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)" |
121 apply (unfold FreeUltrafilterNat_def) |
117 apply (unfold FreeUltrafilterNat_def) |
122 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
118 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
123 apply (rule someI2) |
119 apply (rule someI2, assumption+) |
124 apply assumption+ |
120 done |
125 done |
|
126 declare FreeUltrafilterNat_mem [simp] |
|
127 |
121 |
128 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat" |
122 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat" |
129 apply (unfold FreeUltrafilterNat_def) |
123 apply (unfold FreeUltrafilterNat_def) |
130 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
124 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
131 apply (rule someI2 , assumption) |
125 apply (rule someI2, assumption) |
132 apply (blast dest: mem_FreeUltrafiltersetD1) |
126 apply (blast dest: mem_FreeUltrafiltersetD1) |
133 done |
127 done |
134 |
128 |
135 lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x" |
129 lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x" |
136 apply (blast dest: FreeUltrafilterNat_finite) |
130 by (blast dest: FreeUltrafilterNat_finite) |
137 done |
131 |
138 |
132 lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat" |
139 lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat" |
|
140 apply (unfold FreeUltrafilterNat_def) |
133 apply (unfold FreeUltrafilterNat_def) |
141 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
134 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
142 apply (rule someI2 , assumption) |
135 apply (rule someI2, assumption) |
143 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter Filter_empty_not_mem) |
136 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter |
144 done |
137 Filter_empty_not_mem) |
145 declare FreeUltrafilterNat_empty [simp] |
138 done |
146 |
139 |
147 lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] |
140 lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] |
148 ==> X Int Y \<in> FreeUltrafilterNat" |
141 ==> X Int Y \<in> FreeUltrafilterNat" |
149 apply (cut_tac FreeUltrafilterNat_mem) |
142 apply (cut_tac FreeUltrafilterNat_mem) |
150 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) |
143 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) |
155 apply (cut_tac FreeUltrafilterNat_mem) |
148 apply (cut_tac FreeUltrafilterNat_mem) |
156 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) |
149 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) |
157 done |
150 done |
158 |
151 |
159 lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
152 lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
160 apply (safe) |
153 apply safe |
161 apply (drule FreeUltrafilterNat_Int , assumption) |
154 apply (drule FreeUltrafilterNat_Int, assumption, auto) |
162 apply auto |
|
163 done |
155 done |
164 |
156 |
165 lemma FreeUltrafilterNat_Compl_mem: "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
157 lemma FreeUltrafilterNat_Compl_mem: "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
166 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) |
158 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) |
167 apply (safe , drule_tac x = "X" in bspec) |
159 apply (safe, drule_tac x = X in bspec) |
168 apply (auto simp add: UNIV_diff_Compl) |
160 apply (auto simp add: UNIV_diff_Compl) |
169 done |
161 done |
170 |
162 |
171 lemma FreeUltrafilterNat_Compl_iff1: "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" |
163 lemma FreeUltrafilterNat_Compl_iff1: "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" |
172 apply (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) |
164 by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) |
173 done |
|
174 |
165 |
175 lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
166 lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
176 apply (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
167 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
177 done |
168 |
178 |
169 lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat" |
179 lemma FreeUltrafilterNat_UNIV: "(UNIV::nat set) \<in> FreeUltrafilterNat" |
170 by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) |
180 apply (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) |
171 |
181 done |
172 lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat" |
182 declare FreeUltrafilterNat_UNIV [simp] |
173 by auto |
183 |
174 |
184 lemma FreeUltrafilterNat_Nat_set: "UNIV \<in> FreeUltrafilterNat" |
175 lemma FreeUltrafilterNat_Nat_set_refl [intro]: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat" |
185 apply auto |
176 by simp |
186 done |
|
187 declare FreeUltrafilterNat_Nat_set [simp] |
|
188 |
|
189 lemma FreeUltrafilterNat_Nat_set_refl: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat" |
|
190 apply (simp (no_asm)) |
|
191 done |
|
192 declare FreeUltrafilterNat_Nat_set_refl [intro] |
|
193 |
177 |
194 lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P" |
178 lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P" |
195 apply (rule ccontr) |
179 by (rule ccontr, simp) |
196 apply simp |
|
197 done |
|
198 |
180 |
199 lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)" |
181 lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)" |
200 apply (rule ccontr) |
182 by (rule ccontr, simp) |
201 apply simp |
|
202 done |
|
203 |
183 |
204 lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat" |
184 lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat" |
205 apply (auto intro: FreeUltrafilterNat_Nat_set) |
185 by (auto intro: FreeUltrafilterNat_Nat_set) |
206 done |
|
207 |
186 |
208 (*------------------------------------------------------- |
187 (*------------------------------------------------------- |
209 Define and use Ultrafilter tactics |
188 Define and use Ultrafilter tactics |
210 -------------------------------------------------------*) |
189 -------------------------------------------------------*) |
211 use "fuf.ML" |
190 use "fuf.ML" |
463 apply (simp add: hypreal_add_assoc) |
415 apply (simp add: hypreal_add_assoc) |
464 apply (simp add: hypreal_add_commute) |
416 apply (simp add: hypreal_add_commute) |
465 done |
417 done |
466 |
418 |
467 lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" |
419 lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" |
468 apply (cut_tac z = "y" in hypreal_add_minus_left) |
420 apply (cut_tac z = y in hypreal_add_minus_left) |
469 apply (rule_tac x1 = "y" in hypreal_minus_left_ex1 [THEN ex1E]) |
421 apply (rule_tac x1 = y in hypreal_minus_left_ex1 [THEN ex1E], blast) |
470 apply blast |
|
471 done |
422 done |
472 |
423 |
473 lemma hypreal_as_add_inverse_ex: "\<exists>y::hypreal. x = -y" |
424 lemma hypreal_as_add_inverse_ex: "\<exists>y::hypreal. x = -y" |
474 apply (cut_tac x = "x" in hypreal_minus_ex) |
425 apply (cut_tac x = x in hypreal_minus_ex) |
475 apply (erule exE , drule hypreal_add_minus_eq_minus) |
426 apply (erule exE, drule hypreal_add_minus_eq_minus, fast) |
476 apply fast |
427 done |
477 done |
428 |
478 |
429 lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" |
479 lemma hypreal_minus_add_distrib: "-(x + (y::hypreal)) = -x + -y" |
430 apply (rule_tac z = x in eq_Abs_hypreal) |
480 apply (rule_tac z = "x" in eq_Abs_hypreal) |
431 apply (rule_tac z = y in eq_Abs_hypreal) |
481 apply (rule_tac z = "y" in eq_Abs_hypreal) |
|
482 apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib) |
432 apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib) |
483 done |
433 done |
484 declare hypreal_minus_add_distrib [simp] |
|
485 |
434 |
486 lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" |
435 lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" |
487 apply (simp (no_asm) add: hypreal_add_commute) |
436 by (simp add: hypreal_add_commute) |
488 done |
|
489 |
437 |
490 lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" |
438 lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" |
491 apply (safe) |
439 apply safe |
492 apply (drule_tac f = "%t.-x + t" in arg_cong) |
440 apply (drule_tac f = "%t.-x + t" in arg_cong) |
493 apply (simp add: hypreal_add_assoc [symmetric]) |
441 apply (simp add: hypreal_add_assoc [symmetric]) |
494 done |
442 done |
495 |
443 |
496 lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)" |
444 lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)" |
497 apply (simp (no_asm) add: hypreal_add_commute hypreal_add_left_cancel) |
445 by (simp add: hypreal_add_commute hypreal_add_left_cancel) |
498 done |
446 |
499 |
447 lemma hypreal_add_minus_cancelA [simp]: "z + ((- z) + w) = (w::hypreal)" |
500 lemma hypreal_add_minus_cancelA: "z + ((- z) + w) = (w::hypreal)" |
448 by (simp add: hypreal_add_assoc [symmetric]) |
501 apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) |
449 |
502 done |
450 lemma hypreal_minus_add_cancelA [simp]: "(-z) + (z + w) = (w::hypreal)" |
503 |
451 by (simp add: hypreal_add_assoc [symmetric]) |
504 lemma hypreal_minus_add_cancelA: "(-z) + (z + w) = (w::hypreal)" |
|
505 apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) |
|
506 done |
|
507 |
|
508 declare hypreal_add_minus_cancelA [simp] hypreal_minus_add_cancelA [simp] |
|
509 |
452 |
510 (**** hyperreal multiplication: hypreal_mult ****) |
453 (**** hyperreal multiplication: hypreal_mult ****) |
511 |
454 |
512 lemma hypreal_mult_congruent2: |
455 lemma hypreal_mult_congruent2: |
513 "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})" |
456 "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})" |
514 apply (unfold congruent2_def) |
457 apply (unfold congruent2_def, auto, ultra) |
515 apply auto |
|
516 apply (ultra) |
|
517 done |
458 done |
518 |
459 |
519 lemma hypreal_mult: |
460 lemma hypreal_mult: |
520 "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = |
461 "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = |
521 Abs_hypreal(hyprel``{%n. X n * Y n})" |
462 Abs_hypreal(hyprel``{%n. X n * Y n})" |
522 apply (unfold hypreal_mult_def) |
463 apply (unfold hypreal_mult_def) |
523 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2]) |
464 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2]) |
524 done |
465 done |
525 |
466 |
526 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" |
467 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" |
527 apply (rule_tac z = "z" in eq_Abs_hypreal) |
468 apply (rule_tac z = z in eq_Abs_hypreal) |
528 apply (rule_tac z = "w" in eq_Abs_hypreal) |
469 apply (rule_tac z = w in eq_Abs_hypreal) |
529 apply (simp (no_asm_simp) add: hypreal_mult real_mult_ac) |
470 apply (simp add: hypreal_mult real_mult_ac) |
530 done |
471 done |
531 |
472 |
532 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)" |
473 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)" |
533 apply (rule_tac z = "z1" in eq_Abs_hypreal) |
474 apply (rule_tac z = z1 in eq_Abs_hypreal) |
534 apply (rule_tac z = "z2" in eq_Abs_hypreal) |
475 apply (rule_tac z = z2 in eq_Abs_hypreal) |
535 apply (rule_tac z = "z3" in eq_Abs_hypreal) |
476 apply (rule_tac z = z3 in eq_Abs_hypreal) |
536 apply (simp (no_asm_simp) add: hypreal_mult real_mult_assoc) |
477 apply (simp add: hypreal_mult real_mult_assoc) |
537 done |
478 done |
538 |
479 |
539 lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" |
480 lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" |
540 apply (rule mk_left_commute [of "op *"]) |
481 apply (rule mk_left_commute [of "op *"]) |
541 apply (rule hypreal_mult_assoc) |
482 apply (rule hypreal_mult_assoc) |
544 |
485 |
545 (* hypreal multiplication is an AC operator *) |
486 (* hypreal multiplication is an AC operator *) |
546 lemmas hypreal_mult_ac = |
487 lemmas hypreal_mult_ac = |
547 hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute |
488 hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute |
548 |
489 |
549 lemma hypreal_mult_1: "(1::hypreal) * z = z" |
490 lemma hypreal_mult_1 [simp]: "(1::hypreal) * z = z" |
550 apply (unfold hypreal_one_def) |
491 apply (unfold hypreal_one_def) |
551 apply (rule_tac z = "z" in eq_Abs_hypreal) |
492 apply (rule_tac z = z in eq_Abs_hypreal) |
552 apply (simp add: hypreal_mult) |
493 apply (simp add: hypreal_mult) |
553 done |
494 done |
554 declare hypreal_mult_1 [simp] |
495 |
555 |
496 lemma hypreal_mult_1_right [simp]: "z * (1::hypreal) = z" |
556 lemma hypreal_mult_1_right: "z * (1::hypreal) = z" |
497 by (simp add: hypreal_mult_commute hypreal_mult_1) |
557 apply (simp (no_asm) add: hypreal_mult_commute hypreal_mult_1) |
498 |
558 done |
499 lemma hypreal_mult_0 [simp]: "0 * z = (0::hypreal)" |
559 declare hypreal_mult_1_right [simp] |
|
560 |
|
561 lemma hypreal_mult_0: "0 * z = (0::hypreal)" |
|
562 apply (unfold hypreal_zero_def) |
500 apply (unfold hypreal_zero_def) |
563 apply (rule_tac z = "z" in eq_Abs_hypreal) |
501 apply (rule_tac z = z in eq_Abs_hypreal) |
564 apply (simp add: hypreal_mult) |
502 apply (simp add: hypreal_mult) |
565 done |
503 done |
566 declare hypreal_mult_0 [simp] |
504 |
567 |
505 lemma hypreal_mult_0_right [simp]: "z * 0 = (0::hypreal)" |
568 lemma hypreal_mult_0_right: "z * 0 = (0::hypreal)" |
506 by (simp add: hypreal_mult_commute) |
569 apply (simp (no_asm) add: hypreal_mult_commute) |
|
570 done |
|
571 declare hypreal_mult_0_right [simp] |
|
572 |
507 |
573 lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)" |
508 lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)" |
574 apply (rule_tac z = "x" in eq_Abs_hypreal) |
509 apply (rule_tac z = x in eq_Abs_hypreal) |
575 apply (rule_tac z = "y" in eq_Abs_hypreal) |
510 apply (rule_tac z = y in eq_Abs_hypreal) |
576 apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) |
511 apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) |
577 done |
512 done |
578 |
513 |
579 lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y" |
514 lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y" |
580 apply (rule_tac z = "x" in eq_Abs_hypreal) |
515 apply (rule_tac z = x in eq_Abs_hypreal) |
581 apply (rule_tac z = "y" in eq_Abs_hypreal) |
516 apply (rule_tac z = y in eq_Abs_hypreal) |
582 apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) |
517 apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) |
583 done |
518 done |
584 |
519 |
585 (*Pull negations out*) |
520 (*Pull negations out*) |
586 declare hypreal_minus_mult_eq2 [symmetric, simp] hypreal_minus_mult_eq1 [symmetric, simp] |
521 declare hypreal_minus_mult_eq2 [symmetric, simp] |
587 |
522 hypreal_minus_mult_eq1 [symmetric, simp] |
588 lemma hypreal_mult_minus_1: "(- (1::hypreal)) * z = -z" |
523 |
589 apply (simp (no_asm)) |
524 lemma hypreal_mult_minus_1 [simp]: "(- (1::hypreal)) * z = -z" |
590 done |
525 by simp |
591 declare hypreal_mult_minus_1 [simp] |
526 |
592 |
527 lemma hypreal_mult_minus_1_right [simp]: "z * (- (1::hypreal)) = -z" |
593 lemma hypreal_mult_minus_1_right: "z * (- (1::hypreal)) = -z" |
528 by (subst hypreal_mult_commute, simp) |
594 apply (subst hypreal_mult_commute) |
|
595 apply (simp (no_asm)) |
|
596 done |
|
597 declare hypreal_mult_minus_1_right [simp] |
|
598 |
529 |
599 lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" |
530 lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" |
600 apply auto |
531 by auto |
601 done |
|
602 |
532 |
603 (*----------------------------------------------------------------------------- |
533 (*----------------------------------------------------------------------------- |
604 A few more theorems |
534 A few more theorems |
605 ----------------------------------------------------------------------------*) |
535 ----------------------------------------------------------------------------*) |
606 lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
536 lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
607 apply (simp (no_asm_simp) add: hypreal_add_assoc [symmetric]) |
537 by (simp add: hypreal_add_assoc [symmetric]) |
608 done |
|
609 |
538 |
610 lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" |
539 lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" |
611 apply (rule_tac z = "z1" in eq_Abs_hypreal) |
540 apply (rule_tac z = z1 in eq_Abs_hypreal) |
612 apply (rule_tac z = "z2" in eq_Abs_hypreal) |
541 apply (rule_tac z = z2 in eq_Abs_hypreal) |
613 apply (rule_tac z = "w" in eq_Abs_hypreal) |
542 apply (rule_tac z = w in eq_Abs_hypreal) |
614 apply (simp (no_asm_simp) add: hypreal_mult hypreal_add real_add_mult_distrib) |
543 apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) |
615 done |
544 done |
616 |
545 |
617 lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" |
546 lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" |
618 apply (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) |
547 by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) |
619 done |
|
620 |
548 |
621 |
549 |
622 lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" |
550 lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" |
623 |
551 |
624 apply (unfold hypreal_diff_def) |
552 apply (unfold hypreal_diff_def) |
625 apply (simp (no_asm) add: hypreal_add_mult_distrib) |
553 apply (simp add: hypreal_add_mult_distrib) |
626 done |
554 done |
627 |
555 |
628 lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" |
556 lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" |
629 apply (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) |
557 by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) |
630 done |
|
631 |
558 |
632 (*** one and zero are distinct ***) |
559 (*** one and zero are distinct ***) |
633 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)" |
560 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)" |
634 apply (unfold hypreal_zero_def hypreal_one_def) |
561 apply (unfold hypreal_zero_def hypreal_one_def) |
635 apply (auto simp add: real_zero_not_eq_one) |
562 apply (auto simp add: real_zero_not_eq_one) |
639 (**** multiplicative inverse on hypreal ****) |
566 (**** multiplicative inverse on hypreal ****) |
640 |
567 |
641 lemma hypreal_inverse_congruent: |
568 lemma hypreal_inverse_congruent: |
642 "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" |
569 "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" |
643 apply (unfold congruent_def) |
570 apply (unfold congruent_def) |
644 apply (auto , ultra) |
571 apply (auto, ultra) |
645 done |
572 done |
646 |
573 |
647 lemma hypreal_inverse: |
574 lemma hypreal_inverse: |
648 "inverse (Abs_hypreal(hyprel``{%n. X n})) = |
575 "inverse (Abs_hypreal(hyprel``{%n. X n})) = |
649 Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})" |
576 Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})" |
650 apply (unfold hypreal_inverse_def) |
577 apply (unfold hypreal_inverse_def) |
651 apply (rule_tac f = "Abs_hypreal" in arg_cong) |
578 apply (rule_tac f = Abs_hypreal in arg_cong) |
652 apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] |
579 apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] |
653 UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent]) |
580 UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent]) |
654 done |
581 done |
655 |
582 |
656 lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" |
583 lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" |
657 apply (simp (no_asm) add: hypreal_inverse hypreal_zero_def) |
584 by (simp add: hypreal_inverse hypreal_zero_def) |
658 done |
|
659 |
585 |
660 lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" |
586 lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" |
661 apply (simp (no_asm) add: hypreal_divide_def HYPREAL_INVERSE_ZERO) |
587 by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO) |
662 done |
588 |
663 |
589 lemma hypreal_inverse_inverse [simp]: "inverse (inverse (z::hypreal)) = z" |
664 lemma hypreal_inverse_inverse: "inverse (inverse (z::hypreal)) = z" |
|
665 apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO) |
590 apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO) |
666 apply (rule_tac z = "z" in eq_Abs_hypreal) |
591 apply (rule_tac z = z in eq_Abs_hypreal) |
667 apply (simp add: hypreal_inverse hypreal_zero_def) |
592 apply (simp add: hypreal_inverse hypreal_zero_def) |
668 done |
593 done |
669 declare hypreal_inverse_inverse [simp] |
594 |
670 |
595 lemma hypreal_inverse_1 [simp]: "inverse((1::hypreal)) = (1::hypreal)" |
671 lemma hypreal_inverse_1: "inverse((1::hypreal)) = (1::hypreal)" |
|
672 apply (unfold hypreal_one_def) |
596 apply (unfold hypreal_one_def) |
673 apply (simp (no_asm_use) add: hypreal_inverse real_zero_not_eq_one [THEN not_sym]) |
597 apply (simp add: hypreal_inverse real_zero_not_eq_one [THEN not_sym]) |
674 done |
598 done |
675 declare hypreal_inverse_1 [simp] |
|
676 |
599 |
677 |
600 |
678 (*** existence of inverse ***) |
601 (*** existence of inverse ***) |
679 |
602 |
680 lemma hypreal_mult_inverse: |
603 lemma hypreal_mult_inverse [simp]: |
681 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
604 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
682 |
|
683 apply (unfold hypreal_one_def hypreal_zero_def) |
605 apply (unfold hypreal_one_def hypreal_zero_def) |
684 apply (rule_tac z = "x" in eq_Abs_hypreal) |
606 apply (rule_tac z = x in eq_Abs_hypreal) |
685 apply (simp add: hypreal_inverse hypreal_mult) |
607 apply (simp add: hypreal_inverse hypreal_mult) |
686 apply (drule FreeUltrafilterNat_Compl_mem) |
608 apply (drule FreeUltrafilterNat_Compl_mem) |
687 apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) |
609 apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) |
688 done |
610 done |
689 |
611 |
690 lemma hypreal_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)" |
612 lemma hypreal_mult_inverse_left [simp]: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)" |
691 apply (simp (no_asm_simp) add: hypreal_mult_inverse hypreal_mult_commute) |
613 by (simp add: hypreal_mult_inverse hypreal_mult_commute) |
692 done |
|
693 |
614 |
694 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
615 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
695 apply auto |
616 apply auto |
696 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
617 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
697 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
618 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
698 done |
619 done |
699 |
620 |
700 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
621 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
701 apply (safe) |
622 apply safe |
702 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
623 apply (drule_tac f = "%x. x*inverse c" in arg_cong) |
703 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
624 apply (simp add: hypreal_mult_inverse hypreal_mult_ac) |
704 done |
625 done |
705 |
626 |
706 lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0" |
627 lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0" |
707 apply (unfold hypreal_zero_def) |
628 apply (unfold hypreal_zero_def) |
708 apply (rule_tac z = "x" in eq_Abs_hypreal) |
629 apply (rule_tac z = x in eq_Abs_hypreal) |
709 apply (simp add: hypreal_inverse hypreal_mult) |
630 apply (simp add: hypreal_inverse hypreal_mult) |
710 done |
631 done |
711 |
632 |
712 declare hypreal_mult_inverse [simp] hypreal_mult_inverse_left [simp] |
|
713 |
633 |
714 lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)" |
634 lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)" |
715 apply (safe) |
635 apply safe |
716 apply (drule_tac f = "%z. inverse x*z" in arg_cong) |
636 apply (drule_tac f = "%z. inverse x*z" in arg_cong) |
717 apply (simp add: hypreal_mult_assoc [symmetric]) |
637 apply (simp add: hypreal_mult_assoc [symmetric]) |
718 done |
638 done |
719 |
639 |
720 lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0" |
640 lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0" |
721 apply (auto intro: ccontr dest: hypreal_mult_not_0) |
641 by (auto intro: ccontr dest: hypreal_mult_not_0) |
722 done |
|
723 |
642 |
724 lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" |
643 lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" |
725 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
644 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
726 apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1]) |
645 apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1], simp) |
727 apply (simp add: ); |
646 apply (subst hypreal_mult_inverse_left, auto) |
728 apply (subst hypreal_mult_inverse_left) |
|
729 apply auto |
|
730 done |
647 done |
731 |
648 |
732 lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" |
649 lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" |
733 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
650 apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) |
734 apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO) |
651 apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO) |
735 apply (frule_tac y = "y" in hypreal_mult_not_0 , assumption) |
652 apply (frule_tac y = y in hypreal_mult_not_0, assumption) |
736 apply (rule_tac c1 = "x" in hypreal_mult_left_cancel [THEN iffD1]) |
653 apply (rule_tac c1 = x in hypreal_mult_left_cancel [THEN iffD1]) |
737 apply (auto simp add: hypreal_mult_assoc [symmetric]) |
654 apply (auto simp add: hypreal_mult_assoc [symmetric]) |
738 apply (rule_tac c1 = "y" in hypreal_mult_left_cancel [THEN iffD1]) |
655 apply (rule_tac c1 = y in hypreal_mult_left_cancel [THEN iffD1]) |
739 apply (auto simp add: hypreal_mult_left_commute) |
656 apply (auto simp add: hypreal_mult_left_commute) |
740 apply (simp (no_asm_simp) add: hypreal_mult_assoc [symmetric]) |
657 apply (simp add: hypreal_mult_assoc [symmetric]) |
741 done |
658 done |
742 |
659 |
743 (*------------------------------------------------------------------ |
660 (*------------------------------------------------------------------ |
744 Theorems for ordering |
661 Theorems for ordering |
745 ------------------------------------------------------------------*) |
662 ------------------------------------------------------------------*) |
749 lemma hypreal_less_iff: |
666 lemma hypreal_less_iff: |
750 "(P < (Q::hypreal)) = (\<exists>X Y. X \<in> Rep_hypreal(P) & |
667 "(P < (Q::hypreal)) = (\<exists>X Y. X \<in> Rep_hypreal(P) & |
751 Y \<in> Rep_hypreal(Q) & |
668 Y \<in> Rep_hypreal(Q) & |
752 {n. X n < Y n} \<in> FreeUltrafilterNat)" |
669 {n. X n < Y n} \<in> FreeUltrafilterNat)" |
753 |
670 |
754 apply (unfold hypreal_less_def) |
671 apply (unfold hypreal_less_def, fast) |
755 apply fast |
|
756 done |
672 done |
757 |
673 |
758 lemma hypreal_lessI: |
674 lemma hypreal_lessI: |
759 "[| {n. X n < Y n} \<in> FreeUltrafilterNat; |
675 "[| {n. X n < Y n} \<in> FreeUltrafilterNat; |
760 X \<in> Rep_hypreal(P); |
676 X \<in> Rep_hypreal(P); |
761 Y \<in> Rep_hypreal(Q) |] ==> P < (Q::hypreal)" |
677 Y \<in> Rep_hypreal(Q) |] ==> P < (Q::hypreal)" |
762 apply (unfold hypreal_less_def) |
678 apply (unfold hypreal_less_def, fast) |
763 apply fast |
|
764 done |
679 done |
765 |
680 |
766 |
681 |
767 lemma hypreal_lessE: |
682 lemma hypreal_lessE: |
768 "!! R1. [| R1 < (R2::hypreal); |
683 "!! R1. [| R1 < (R2::hypreal); |
769 !!X Y. {n. X n < Y n} \<in> FreeUltrafilterNat ==> P; |
684 !!X Y. {n. X n < Y n} \<in> FreeUltrafilterNat ==> P; |
770 !!X. X \<in> Rep_hypreal(R1) ==> P; |
685 !!X. X \<in> Rep_hypreal(R1) ==> P; |
771 !!Y. Y \<in> Rep_hypreal(R2) ==> P |] |
686 !!Y. Y \<in> Rep_hypreal(R2) ==> P |] |
772 ==> P" |
687 ==> P" |
773 |
688 |
774 apply (unfold hypreal_less_def) |
689 apply (unfold hypreal_less_def, auto) |
775 apply auto |
|
776 done |
690 done |
777 |
691 |
778 lemma hypreal_lessD: |
692 lemma hypreal_lessD: |
779 "R1 < (R2::hypreal) ==> (\<exists>X Y. {n. X n < Y n} \<in> FreeUltrafilterNat & |
693 "R1 < (R2::hypreal) ==> (\<exists>X Y. {n. X n < Y n} \<in> FreeUltrafilterNat & |
780 X \<in> Rep_hypreal(R1) & |
694 X \<in> Rep_hypreal(R1) & |
781 Y \<in> Rep_hypreal(R2))" |
695 Y \<in> Rep_hypreal(R2))" |
782 apply (unfold hypreal_less_def) |
696 apply (unfold hypreal_less_def, fast) |
783 apply fast |
|
784 done |
697 done |
785 |
698 |
786 lemma hypreal_less_not_refl: "~ (R::hypreal) < R" |
699 lemma hypreal_less_not_refl: "~ (R::hypreal) < R" |
787 apply (rule_tac z = "R" in eq_Abs_hypreal) |
700 apply (rule_tac z = R in eq_Abs_hypreal) |
788 apply (auto simp add: hypreal_less_def) |
701 apply (auto simp add: hypreal_less_def, ultra) |
789 apply (ultra) |
|
790 done |
702 done |
791 |
703 |
792 (*** y < y ==> P ***) |
704 (*** y < y ==> P ***) |
793 lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] |
705 lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] |
794 declare hypreal_less_irrefl [elim!] |
706 declare hypreal_less_irrefl [elim!] |
795 |
707 |
796 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
708 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
797 apply (auto simp add: hypreal_less_not_refl) |
709 by (auto simp add: hypreal_less_not_refl) |
798 done |
|
799 |
710 |
800 lemma hypreal_less_trans: "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3" |
711 lemma hypreal_less_trans: "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3" |
801 apply (rule_tac z = "R1" in eq_Abs_hypreal) |
712 apply (rule_tac z = R1 in eq_Abs_hypreal) |
802 apply (rule_tac z = "R2" in eq_Abs_hypreal) |
713 apply (rule_tac z = R2 in eq_Abs_hypreal) |
803 apply (rule_tac z = "R3" in eq_Abs_hypreal) |
714 apply (rule_tac z = R3 in eq_Abs_hypreal) |
804 apply (auto intro!: exI simp add: hypreal_less_def) |
715 apply (auto intro!: exI simp add: hypreal_less_def, ultra) |
805 apply ultra |
|
806 done |
716 done |
807 |
717 |
808 lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P" |
718 lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P" |
809 apply (drule hypreal_less_trans , assumption) |
719 apply (drule hypreal_less_trans, assumption) |
810 apply (simp add: hypreal_less_not_refl) |
720 apply (simp add: hypreal_less_not_refl) |
811 done |
721 done |
812 |
722 |
813 (*------------------------------------------------------- |
723 (*------------------------------------------------------- |
814 TODO: The following theorem should have been proved |
724 TODO: The following theorem should have been proved |
818 lemma hypreal_less: |
728 lemma hypreal_less: |
819 "(Abs_hypreal(hyprel``{%n. X n}) < |
729 "(Abs_hypreal(hyprel``{%n. X n}) < |
820 Abs_hypreal(hyprel``{%n. Y n})) = |
730 Abs_hypreal(hyprel``{%n. Y n})) = |
821 ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
731 ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
822 apply (unfold hypreal_less_def) |
732 apply (unfold hypreal_less_def) |
823 apply (auto intro!: lemma_hyprel_refl) |
733 apply (auto intro!: lemma_hyprel_refl, ultra) |
824 apply (ultra) |
|
825 done |
734 done |
826 |
735 |
827 (*---------------------------------------------------------------------------- |
736 (*---------------------------------------------------------------------------- |
828 Trichotomy: the hyperreals are linearly ordered |
737 Trichotomy: the hyperreals are linearly ordered |
829 ---------------------------------------------------------------------------*) |
738 ---------------------------------------------------------------------------*) |
830 |
739 |
831 lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}" |
740 lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}" |
832 |
741 |
833 apply (unfold hyprel_def) |
742 apply (unfold hyprel_def) |
834 apply (rule_tac x = "%n. 0" in exI) |
743 apply (rule_tac x = "%n. 0" in exI, safe) |
835 apply (safe) |
|
836 apply (auto intro!: FreeUltrafilterNat_Nat_set) |
744 apply (auto intro!: FreeUltrafilterNat_Nat_set) |
837 done |
745 done |
838 |
746 |
839 lemma hypreal_trichotomy: "0 < x | x = 0 | x < (0::hypreal)" |
747 lemma hypreal_trichotomy: "0 < x | x = 0 | x < (0::hypreal)" |
840 apply (unfold hypreal_zero_def) |
748 apply (unfold hypreal_zero_def) |
841 apply (rule_tac z = "x" in eq_Abs_hypreal) |
749 apply (rule_tac z = x in eq_Abs_hypreal) |
842 apply (auto simp add: hypreal_less_def) |
750 apply (auto simp add: hypreal_less_def) |
843 apply (cut_tac lemma_hyprel_0_mem , erule exE) |
751 apply (cut_tac lemma_hyprel_0_mem, erule exE) |
844 apply (drule_tac x = "xa" in spec) |
752 apply (drule_tac x = xa in spec) |
845 apply (drule_tac x = "x" in spec) |
753 apply (drule_tac x = x in spec) |
846 apply (cut_tac x = "x" in lemma_hyprel_refl) |
754 apply (cut_tac x = x in lemma_hyprel_refl, auto) |
847 apply auto |
755 apply (drule_tac x = x in spec) |
848 apply (drule_tac x = "x" in spec) |
756 apply (drule_tac x = xa in spec, auto, ultra) |
849 apply (drule_tac x = "xa" in spec) |
|
850 apply auto |
|
851 apply (ultra) |
|
852 done |
757 done |
853 |
758 |
854 lemma hypreal_trichotomyE: |
759 lemma hypreal_trichotomyE: |
855 "[| (0::hypreal) < x ==> P; |
760 "[| (0::hypreal) < x ==> P; |
856 x = 0 ==> P; |
761 x = 0 ==> P; |
857 x < 0 ==> P |] ==> P" |
762 x < 0 ==> P |] ==> P" |
858 apply (insert hypreal_trichotomy [of x]) |
763 apply (insert hypreal_trichotomy [of x], blast) |
859 apply (blast intro: elim:); |
|
860 done |
764 done |
861 |
765 |
862 (*---------------------------------------------------------------------------- |
766 (*---------------------------------------------------------------------------- |
863 More properties of < |
767 More properties of < |
864 ----------------------------------------------------------------------------*) |
768 ----------------------------------------------------------------------------*) |
865 |
769 |
866 lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" |
770 lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" |
867 apply (rule_tac z = "x" in eq_Abs_hypreal) |
771 apply (rule_tac z = x in eq_Abs_hypreal) |
868 apply (rule_tac z = "y" in eq_Abs_hypreal) |
772 apply (rule_tac z = y in eq_Abs_hypreal) |
869 apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) |
773 apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) |
870 done |
774 done |
871 |
775 |
872 lemma hypreal_less_minus_iff2: "((x::hypreal) < y) = (x + -y < 0)" |
776 lemma hypreal_less_minus_iff2: "((x::hypreal) < y) = (x + -y < 0)" |
873 apply (rule_tac z = "x" in eq_Abs_hypreal) |
777 apply (rule_tac z = x in eq_Abs_hypreal) |
874 apply (rule_tac z = "y" in eq_Abs_hypreal) |
778 apply (rule_tac z = y in eq_Abs_hypreal) |
875 apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) |
779 apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) |
876 done |
780 done |
877 |
781 |
878 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
782 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
879 apply auto |
783 apply auto |
880 apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1]) |
784 apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1], auto) |
881 apply auto |
|
882 done |
785 done |
883 |
786 |
884 lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" |
787 lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" |
885 apply auto |
788 apply auto |
886 apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1]) |
789 apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto) |
887 apply auto |
|
888 done |
790 done |
889 |
791 |
890 (* 07/00 *) |
792 (* 07/00 *) |
891 lemma hypreal_diff_zero: "(0::hypreal) - x = -x" |
793 lemma hypreal_diff_zero [simp]: "(0::hypreal) - x = -x" |
892 apply (simp (no_asm) add: hypreal_diff_def) |
794 by (simp add: hypreal_diff_def) |
893 done |
795 |
894 |
796 lemma hypreal_diff_zero_right [simp]: "x - (0::hypreal) = x" |
895 lemma hypreal_diff_zero_right: "x - (0::hypreal) = x" |
797 by (simp add: hypreal_diff_def) |
896 apply (simp (no_asm) add: hypreal_diff_def) |
798 |
897 done |
799 lemma hypreal_diff_self [simp]: "x - x = (0::hypreal)" |
898 |
800 by (simp add: hypreal_diff_def) |
899 lemma hypreal_diff_self: "x - x = (0::hypreal)" |
|
900 apply (simp (no_asm) add: hypreal_diff_def) |
|
901 done |
|
902 |
|
903 declare hypreal_diff_zero [simp] hypreal_diff_zero_right [simp] hypreal_diff_self [simp] |
|
904 |
801 |
905 lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" |
802 lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" |
906 apply (auto simp add: hypreal_add_assoc) |
803 by (auto simp add: hypreal_add_assoc) |
907 done |
|
908 |
804 |
909 lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))" |
805 lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))" |
910 apply (auto dest: hypreal_eq_minus_iff [THEN iffD2]) |
806 by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) |
911 done |
|
912 |
807 |
913 |
808 |
914 (*** linearity ***) |
809 (*** linearity ***) |
915 |
810 |
916 lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" |
811 lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" |
917 apply (subst hypreal_eq_minus_iff2) |
812 apply (subst hypreal_eq_minus_iff2) |
918 apply (rule_tac x1 = "x" in hypreal_less_minus_iff [THEN ssubst]) |
813 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
919 apply (rule_tac x1 = "y" in hypreal_less_minus_iff2 [THEN ssubst]) |
814 apply (rule_tac x1 = y in hypreal_less_minus_iff2 [THEN ssubst]) |
920 apply (rule hypreal_trichotomyE) |
815 apply (rule hypreal_trichotomyE, auto) |
921 apply auto |
|
922 done |
816 done |
923 |
817 |
924 lemma hypreal_neq_iff: "((w::hypreal) \<noteq> z) = (w<z | z<w)" |
818 lemma hypreal_neq_iff: "((w::hypreal) \<noteq> z) = (w<z | z<w)" |
925 apply (cut_tac hypreal_linear) |
819 by (cut_tac hypreal_linear, blast) |
926 apply blast |
|
927 done |
|
928 |
820 |
929 lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P; x = y ==> P; |
821 lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P; x = y ==> P; |
930 y < x ==> P |] ==> P" |
822 y < x ==> P |] ==> P" |
931 apply (cut_tac x = "x" and y = "y" in hypreal_linear) |
823 apply (cut_tac x = x and y = y in hypreal_linear, auto) |
932 apply auto |
|
933 done |
824 done |
934 |
825 |
935 (*------------------------------------------------------------------------------ |
826 (*------------------------------------------------------------------------------ |
936 Properties of <= |
827 Properties of <= |
937 ------------------------------------------------------------------------------*) |
828 ------------------------------------------------------------------------------*) |
1015 apply (fast dest: hypreal_le_imp_less_or_eq) |
899 apply (fast dest: hypreal_le_imp_less_or_eq) |
1016 done |
900 done |
1017 |
901 |
1018 (* Axiom 'order_less_le' of class 'order': *) |
902 (* Axiom 'order_less_le' of class 'order': *) |
1019 lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)" |
903 lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)" |
1020 apply (simp (no_asm) add: hypreal_le_def hypreal_neq_iff) |
904 apply (simp add: hypreal_le_def hypreal_neq_iff) |
1021 apply (blast intro: hypreal_less_asym) |
905 apply (blast intro: hypreal_less_asym) |
1022 done |
906 done |
1023 |
907 |
1024 lemma hypreal_minus_zero_less_iff: "(0 < -R) = (R < (0::hypreal))" |
908 lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))" |
1025 apply (rule_tac z = "R" in eq_Abs_hypreal) |
909 apply (rule_tac z = R in eq_Abs_hypreal) |
1026 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
910 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
1027 done |
911 done |
1028 declare hypreal_minus_zero_less_iff [simp] |
912 |
1029 |
913 lemma hypreal_minus_zero_less_iff2 [simp]: "(-R < 0) = ((0::hypreal) < R)" |
1030 lemma hypreal_minus_zero_less_iff2: "(-R < 0) = ((0::hypreal) < R)" |
914 apply (rule_tac z = R in eq_Abs_hypreal) |
1031 apply (rule_tac z = "R" in eq_Abs_hypreal) |
|
1032 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
915 apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) |
1033 done |
916 done |
1034 declare hypreal_minus_zero_less_iff2 [simp] |
917 |
1035 |
918 lemma hypreal_minus_zero_le_iff [simp]: "((0::hypreal) <= -r) = (r <= 0)" |
1036 lemma hypreal_minus_zero_le_iff: "((0::hypreal) <= -r) = (r <= 0)" |
|
1037 apply (unfold hypreal_le_def) |
919 apply (unfold hypreal_le_def) |
1038 apply (simp (no_asm) add: hypreal_minus_zero_less_iff2) |
920 apply (simp add: hypreal_minus_zero_less_iff2) |
1039 done |
921 done |
1040 declare hypreal_minus_zero_le_iff [simp] |
922 |
1041 |
923 lemma hypreal_minus_zero_le_iff2 [simp]: "(-r <= (0::hypreal)) = (0 <= r)" |
1042 lemma hypreal_minus_zero_le_iff2: "(-r <= (0::hypreal)) = (0 <= r)" |
|
1043 apply (unfold hypreal_le_def) |
924 apply (unfold hypreal_le_def) |
1044 apply (simp (no_asm) add: hypreal_minus_zero_less_iff2) |
925 apply (simp add: hypreal_minus_zero_less_iff2) |
1045 done |
926 done |
1046 declare hypreal_minus_zero_le_iff2 [simp] |
|
1047 |
927 |
1048 (*---------------------------------------------------------- |
928 (*---------------------------------------------------------- |
1049 hypreal_of_real preserves field and order properties |
929 hypreal_of_real preserves field and order properties |
1050 -----------------------------------------------------------*) |
930 -----------------------------------------------------------*) |
1051 lemma hypreal_of_real_add: |
931 lemma hypreal_of_real_add [simp]: |
1052 "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" |
932 "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" |
1053 apply (unfold hypreal_of_real_def) |
933 apply (unfold hypreal_of_real_def) |
1054 apply (simp (no_asm) add: hypreal_add hypreal_add_mult_distrib) |
934 apply (simp add: hypreal_add hypreal_add_mult_distrib) |
1055 done |
935 done |
1056 declare hypreal_of_real_add [simp] |
936 |
1057 |
937 lemma hypreal_of_real_mult [simp]: |
1058 lemma hypreal_of_real_mult: |
|
1059 "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2" |
938 "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2" |
1060 apply (unfold hypreal_of_real_def) |
939 apply (unfold hypreal_of_real_def) |
1061 apply (simp (no_asm) add: hypreal_mult hypreal_add_mult_distrib2) |
940 apply (simp add: hypreal_mult hypreal_add_mult_distrib2) |
1062 done |
941 done |
1063 declare hypreal_of_real_mult [simp] |
942 |
1064 |
943 lemma hypreal_of_real_less_iff [simp]: |
1065 lemma hypreal_of_real_less_iff: |
|
1066 "(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)" |
944 "(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)" |
1067 apply (unfold hypreal_less_def hypreal_of_real_def) |
945 apply (unfold hypreal_less_def hypreal_of_real_def, auto) |
1068 apply auto |
946 apply (rule_tac [2] x = "%n. z1" in exI, safe) |
1069 apply (rule_tac [2] x = "%n. z1" in exI) |
947 apply (rule_tac [3] x = "%n. z2" in exI, auto) |
1070 apply (safe) |
948 apply (rule FreeUltrafilterNat_P, ultra) |
1071 apply (rule_tac [3] x = "%n. z2" in exI) |
949 done |
1072 apply auto |
950 |
1073 apply (rule FreeUltrafilterNat_P) |
951 lemma hypreal_of_real_le_iff [simp]: |
1074 apply (ultra) |
|
1075 done |
|
1076 declare hypreal_of_real_less_iff [simp] |
|
1077 |
|
1078 lemma hypreal_of_real_le_iff: |
|
1079 "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)" |
952 "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)" |
1080 apply (unfold hypreal_le_def real_le_def) |
953 apply (unfold hypreal_le_def real_le_def, auto) |
1081 apply auto |
954 done |
1082 done |
955 |
1083 declare hypreal_of_real_le_iff [simp] |
956 lemma hypreal_of_real_eq_iff [simp]: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" |
1084 |
957 by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) |
1085 lemma hypreal_of_real_eq_iff: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" |
958 |
1086 apply (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) |
959 lemma hypreal_of_real_minus [simp]: "hypreal_of_real (-r) = - hypreal_of_real r" |
1087 done |
|
1088 declare hypreal_of_real_eq_iff [simp] |
|
1089 |
|
1090 lemma hypreal_of_real_minus: "hypreal_of_real (-r) = - hypreal_of_real r" |
|
1091 apply (unfold hypreal_of_real_def) |
960 apply (unfold hypreal_of_real_def) |
1092 apply (auto simp add: hypreal_minus) |
961 apply (auto simp add: hypreal_minus) |
1093 done |
962 done |
1094 declare hypreal_of_real_minus [simp] |
963 |
1095 |
964 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)" |
1096 lemma hypreal_of_real_one: "hypreal_of_real 1 = (1::hypreal)" |
965 by (unfold hypreal_of_real_def hypreal_one_def, simp) |
1097 apply (unfold hypreal_of_real_def hypreal_one_def) |
966 |
1098 apply (simp (no_asm)) |
967 lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0" |
1099 done |
968 by (unfold hypreal_of_real_def hypreal_zero_def, simp) |
1100 declare hypreal_of_real_one [simp] |
|
1101 |
|
1102 lemma hypreal_of_real_zero: "hypreal_of_real 0 = 0" |
|
1103 apply (unfold hypreal_of_real_def hypreal_zero_def) |
|
1104 apply (simp (no_asm)) |
|
1105 done |
|
1106 declare hypreal_of_real_zero [simp] |
|
1107 |
969 |
1108 lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" |
970 lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" |
1109 apply (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) |
971 by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) |
1110 done |
972 |
1111 |
973 lemma hypreal_of_real_inverse [simp]: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" |
1112 lemma hypreal_of_real_inverse: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" |
|
1113 apply (case_tac "r=0") |
974 apply (case_tac "r=0") |
1114 apply (simp (no_asm_simp) add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) |
975 apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) |
1115 apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) |
976 apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) |
1116 apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) |
977 apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) |
1117 done |
978 done |
1118 declare hypreal_of_real_inverse [simp] |
979 |
1119 |
980 lemma hypreal_of_real_divide [simp]: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" |
1120 lemma hypreal_of_real_divide: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" |
981 by (simp add: hypreal_divide_def real_divide_def) |
1121 apply (simp (no_asm) add: hypreal_divide_def real_divide_def) |
|
1122 done |
|
1123 declare hypreal_of_real_divide [simp] |
|
1124 |
982 |
1125 |
983 |
1126 (*** Division lemmas ***) |
984 (*** Division lemmas ***) |
1127 |
985 |
1128 lemma hypreal_zero_divide: "(0::hypreal)/x = 0" |
986 lemma hypreal_zero_divide: "(0::hypreal)/x = 0" |
1129 apply (simp (no_asm) add: hypreal_divide_def) |
987 by (simp add: hypreal_divide_def) |
1130 done |
|
1131 |
988 |
1132 lemma hypreal_divide_one: "x/(1::hypreal) = x" |
989 lemma hypreal_divide_one: "x/(1::hypreal) = x" |
1133 apply (simp (no_asm) add: hypreal_divide_def) |
990 by (simp add: hypreal_divide_def) |
1134 done |
|
1135 declare hypreal_zero_divide [simp] hypreal_divide_one [simp] |
991 declare hypreal_zero_divide [simp] hypreal_divide_one [simp] |
1136 |
992 |
1137 lemma hypreal_times_divide1_eq: "(x::hypreal) * (y/z) = (x*y)/z" |
993 lemma hypreal_times_divide1_eq [simp]: "(x::hypreal) * (y/z) = (x*y)/z" |
1138 apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_assoc) |
994 by (simp add: hypreal_divide_def hypreal_mult_assoc) |
1139 done |
995 |
1140 |
996 lemma hypreal_times_divide2_eq [simp]: "(y/z) * (x::hypreal) = (y*x)/z" |
1141 lemma hypreal_times_divide2_eq: "(y/z) * (x::hypreal) = (y*x)/z" |
997 by (simp add: hypreal_divide_def hypreal_mult_ac) |
1142 apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_ac) |
998 |
1143 done |
999 |
1144 |
1000 lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y" |
1145 declare hypreal_times_divide1_eq [simp] hypreal_times_divide2_eq [simp] |
1001 by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) |
1146 |
1002 |
1147 lemma hypreal_divide_divide1_eq: "(x::hypreal) / (y/z) = (x*z)/y" |
1003 lemma hypreal_divide_divide2_eq [simp]: "((x::hypreal) / y) / z = x/(y*z)" |
1148 apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) |
1004 by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc) |
1149 done |
1005 |
1150 |
|
1151 lemma hypreal_divide_divide2_eq: "((x::hypreal) / y) / z = x/(y*z)" |
|
1152 apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc) |
|
1153 done |
|
1154 |
|
1155 declare hypreal_divide_divide1_eq [simp] hypreal_divide_divide2_eq [simp] |
|
1156 |
1006 |
1157 (** As with multiplication, pull minus signs OUT of the / operator **) |
1007 (** As with multiplication, pull minus signs OUT of the / operator **) |
1158 |
1008 |
1159 lemma hypreal_minus_divide_eq: "(-x) / (y::hypreal) = - (x/y)" |
1009 lemma hypreal_minus_divide_eq [simp]: "(-x) / (y::hypreal) = - (x/y)" |
1160 apply (simp (no_asm) add: hypreal_divide_def) |
1010 by (simp add: hypreal_divide_def) |
1161 done |
1011 |
1162 declare hypreal_minus_divide_eq [simp] |
1012 lemma hypreal_divide_minus_eq [simp]: "(x / -(y::hypreal)) = - (x/y)" |
1163 |
1013 by (simp add: hypreal_divide_def hypreal_minus_inverse) |
1164 lemma hypreal_divide_minus_eq: "(x / -(y::hypreal)) = - (x/y)" |
|
1165 apply (simp (no_asm) add: hypreal_divide_def hypreal_minus_inverse) |
|
1166 done |
|
1167 declare hypreal_divide_minus_eq [simp] |
|
1168 |
1014 |
1169 lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" |
1015 lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" |
1170 apply (simp (no_asm) add: hypreal_divide_def hypreal_add_mult_distrib) |
1016 by (simp add: hypreal_divide_def hypreal_add_mult_distrib) |
1171 done |
|
1172 |
1017 |
1173 lemma hypreal_inverse_add: "[|(x::hypreal) \<noteq> 0; y \<noteq> 0 |] |
1018 lemma hypreal_inverse_add: "[|(x::hypreal) \<noteq> 0; y \<noteq> 0 |] |
1174 ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" |
1019 ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" |
1175 apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric]) |
1020 apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric]) |
1176 apply (subst hypreal_mult_assoc) |
1021 apply (subst hypreal_mult_assoc) |
1177 apply (rule hypreal_mult_left_commute [THEN subst]) |
1022 apply (rule hypreal_mult_left_commute [THEN subst]) |
1178 apply (simp add: hypreal_add_commute) |
1023 apply (simp add: hypreal_add_commute) |
1179 done |
1024 done |
1180 |
1025 |
1181 lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" |
1026 lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" |
1182 apply (rule_tac z = "x" in eq_Abs_hypreal) |
1027 apply (rule_tac z = x in eq_Abs_hypreal) |
1183 apply (auto simp add: hypreal_minus hypreal_zero_def) |
1028 apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) |
1184 apply (ultra) |
1029 done |
1185 done |
1030 |
1186 |
1031 lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" |
1187 lemma hypreal_add_self_zero_cancel: "(x + x = 0) = (x = (0::hypreal))" |
1032 apply (rule_tac z = x in eq_Abs_hypreal) |
1188 apply (rule_tac z = "x" in eq_Abs_hypreal) |
|
1189 apply (auto simp add: hypreal_add hypreal_zero_def) |
1033 apply (auto simp add: hypreal_add hypreal_zero_def) |
1190 done |
1034 done |
1191 declare hypreal_add_self_zero_cancel [simp] |
1035 |
1192 |
1036 lemma hypreal_add_self_zero_cancel2 [simp]: "(x + x + y = y) = (x = (0::hypreal))" |
1193 lemma hypreal_add_self_zero_cancel2: "(x + x + y = y) = (x = (0::hypreal))" |
|
1194 apply auto |
1037 apply auto |
1195 apply (drule hypreal_eq_minus_iff [THEN iffD1]) |
1038 apply (drule hypreal_eq_minus_iff [THEN iffD1]) |
1196 apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) |
1039 apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) |
1197 done |
1040 done |
1198 declare hypreal_add_self_zero_cancel2 [simp] |
1041 |
1199 |
1042 lemma hypreal_add_self_zero_cancel2a [simp]: "(x + (x + y) = y) = (x = (0::hypreal))" |
1200 lemma hypreal_add_self_zero_cancel2a: "(x + (x + y) = y) = (x = (0::hypreal))" |
1043 by (simp add: hypreal_add_assoc [symmetric]) |
1201 apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) |
|
1202 done |
|
1203 declare hypreal_add_self_zero_cancel2a [simp] |
|
1204 |
1044 |
1205 lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" |
1045 lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" |
1206 apply auto |
1046 by auto |
1207 done |
1047 |
1208 |
1048 lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" |
1209 lemma hypreal_minus_eq_cancel: "(-b = -a) = (b = (a::hypreal))" |
1049 by (simp add: hypreal_minus_eq_swap) |
1210 apply (simp add: hypreal_minus_eq_swap) |
|
1211 done |
|
1212 declare hypreal_minus_eq_cancel [simp] |
|
1213 |
1050 |
1214 lemma hypreal_less_eq_diff: "(x<y) = (x-y < (0::hypreal))" |
1051 lemma hypreal_less_eq_diff: "(x<y) = (x-y < (0::hypreal))" |
1215 apply (unfold hypreal_diff_def) |
1052 apply (unfold hypreal_diff_def) |
1216 apply (rule hypreal_less_minus_iff2) |
1053 apply (rule hypreal_less_minus_iff2) |
1217 done |
1054 done |
1218 |
1055 |
1219 (*** Subtraction laws ***) |
1056 (*** Subtraction laws ***) |
1220 |
1057 |
1221 lemma hypreal_add_diff_eq: "x + (y - z) = (x + y) - (z::hypreal)" |
1058 lemma hypreal_add_diff_eq: "x + (y - z) = (x + y) - (z::hypreal)" |
1222 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1059 by (simp add: hypreal_diff_def hypreal_add_ac) |
1223 done |
|
1224 |
1060 |
1225 lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)" |
1061 lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)" |
1226 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1062 by (simp add: hypreal_diff_def hypreal_add_ac) |
1227 done |
|
1228 |
1063 |
1229 lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))" |
1064 lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))" |
1230 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1065 by (simp add: hypreal_diff_def hypreal_add_ac) |
1231 done |
|
1232 |
1066 |
1233 lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)" |
1067 lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)" |
1234 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1068 by (simp add: hypreal_diff_def hypreal_add_ac) |
1235 done |
|
1236 |
1069 |
1237 lemma hypreal_diff_less_eq: "(x-y < z) = (x < z + (y::hypreal))" |
1070 lemma hypreal_diff_less_eq: "(x-y < z) = (x < z + (y::hypreal))" |
1238 apply (subst hypreal_less_eq_diff) |
1071 apply (subst hypreal_less_eq_diff) |
1239 apply (rule_tac y1 = "z" in hypreal_less_eq_diff [THEN ssubst]) |
1072 apply (rule_tac y1 = z in hypreal_less_eq_diff [THEN ssubst]) |
1240 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1073 apply (simp add: hypreal_diff_def hypreal_add_ac) |
1241 done |
1074 done |
1242 |
1075 |
1243 lemma hypreal_less_diff_eq: "(x < z-y) = (x + (y::hypreal) < z)" |
1076 lemma hypreal_less_diff_eq: "(x < z-y) = (x + (y::hypreal) < z)" |
1244 apply (subst hypreal_less_eq_diff) |
1077 apply (subst hypreal_less_eq_diff) |
1245 apply (rule_tac y1 = "z-y" in hypreal_less_eq_diff [THEN ssubst]) |
1078 apply (rule_tac y1 = "z-y" in hypreal_less_eq_diff [THEN ssubst]) |
1246 apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac) |
1079 apply (simp add: hypreal_diff_def hypreal_add_ac) |
1247 done |
1080 done |
1248 |
1081 |
1249 lemma hypreal_diff_le_eq: "(x-y <= z) = (x <= z + (y::hypreal))" |
1082 lemma hypreal_diff_le_eq: "(x-y <= z) = (x <= z + (y::hypreal))" |
1250 apply (unfold hypreal_le_def) |
1083 apply (unfold hypreal_le_def) |
1251 apply (simp (no_asm) add: hypreal_less_diff_eq) |
1084 apply (simp add: hypreal_less_diff_eq) |
1252 done |
1085 done |
1253 |
1086 |
1254 lemma hypreal_le_diff_eq: "(x <= z-y) = (x + (y::hypreal) <= z)" |
1087 lemma hypreal_le_diff_eq: "(x <= z-y) = (x + (y::hypreal) <= z)" |
1255 apply (unfold hypreal_le_def) |
1088 apply (unfold hypreal_le_def) |
1256 apply (simp (no_asm) add: hypreal_diff_less_eq) |
1089 apply (simp add: hypreal_diff_less_eq) |
1257 done |
1090 done |
1258 |
1091 |
1259 lemma hypreal_diff_eq_eq: "(x-y = z) = (x = z + (y::hypreal))" |
1092 lemma hypreal_diff_eq_eq: "(x-y = z) = (x = z + (y::hypreal))" |
1260 apply (unfold hypreal_diff_def) |
1093 apply (unfold hypreal_diff_def) |
1261 apply (auto simp add: hypreal_add_assoc) |
1094 apply (auto simp add: hypreal_add_assoc) |