1 (* Title: Real/Hyperreal/HyperOrd.thy |
|
2 Author: Jacques D. Fleuriot |
|
3 Copyright: 2000 University of Edinburgh |
|
4 Description: Type "hypreal" is a linear order and also |
|
5 satisfies plus_ac0: + is an AC-operator with zero |
|
6 *) |
|
7 |
|
8 theory HyperOrd = HyperDef: |
1 theory HyperOrd = HyperDef: |
9 |
2 |
10 |
|
11 (*** Monotonicity results ***) |
|
12 |
|
13 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l" |
|
14 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 add_strict_mono) |
|
15 |
|
16 lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B" |
|
17 by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
18 |
|
19 lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j; k<l |] ==> i + k < j + l" |
|
20 apply (erule add_right_mono [THEN order_le_less_trans]) |
|
21 apply (erule add_strict_left_mono) |
|
22 done |
|
23 |
|
24 lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y" |
|
25 by (auto dest: hypreal_add_less_le_mono) |
|
26 |
|
27 lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y" |
|
28 apply (erule order_less_trans) |
|
29 apply (drule hypreal_add_less_mono2, simp) |
|
30 done |
|
31 |
|
32 lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y" |
|
33 apply (drule order_le_imp_less_or_eq)+ |
|
34 apply (auto intro: hypreal_add_order order_less_imp_le) |
|
35 done |
|
36 |
|
37 text{*The precondition could be weakened to @{term "0\<le>x"}*} |
|
38 lemma hypreal_mult_less_mono: |
|
39 "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
|
40 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
|
41 |
|
42 |
|
43 subsection{*Existence of Infinite Hyperreal Number*} |
|
44 |
|
45 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal" |
|
46 apply (unfold omega_def) |
|
47 apply (rule Rep_hypreal) |
|
48 done |
|
49 |
|
50 text{*Existence of infinite number not corresponding to any real number. |
|
51 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
|
52 |
|
53 |
|
54 text{*A few lemmas first*} |
|
55 |
|
56 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
|
57 (\<exists>y. {n::nat. x = real n} = {y})" |
|
58 by (force dest: inj_real_of_nat [THEN injD]) |
|
59 |
|
60 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
61 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
|
62 |
|
63 lemma not_ex_hypreal_of_real_eq_omega: |
|
64 "~ (\<exists>x. hypreal_of_real x = omega)" |
|
65 apply (unfold omega_def hypreal_of_real_def) |
|
66 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] |
|
67 lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) |
|
68 done |
|
69 |
|
70 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega" |
|
71 by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) |
|
72 |
|
73 text{*Existence of infinitesimal number also not corresponding to any |
|
74 real number*} |
|
75 |
|
76 lemma lemma_epsilon_empty_singleton_disj: |
|
77 "{n::nat. x = inverse(real(Suc n))} = {} | |
|
78 (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
|
79 apply (auto simp add: inj_real_of_nat [THEN inj_eq]) |
|
80 done |
|
81 |
|
82 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
83 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
84 |
|
85 lemma not_ex_hypreal_of_real_eq_epsilon: |
|
86 "~ (\<exists>x. hypreal_of_real x = epsilon)" |
|
87 apply (unfold epsilon_def hypreal_of_real_def) |
|
88 apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) |
|
89 done |
|
90 |
|
91 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon" |
|
92 by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto) |
|
93 |
|
94 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
|
95 by (unfold epsilon_def hypreal_zero_def, auto) |
|
96 |
|
97 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
|
98 by (simp add: hypreal_inverse omega_def epsilon_def) |
|
99 |
3 |
100 |
4 |
101 ML |
5 ML |
102 {* |
6 {* |
103 val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1"; |
|
104 val hypreal_mult_order = thm"hypreal_mult_order"; |
|
105 val hypreal_le_add_order = thm"hypreal_le_add_order"; |
|
106 val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1"; |
|
107 val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono"; |
|
108 val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono"; |
|
109 val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono"; |
|
110 val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1"; |
|
111 val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; |
|
112 val hypreal_mult_less_mono = thm"hypreal_mult_less_mono"; |
|
113 val Rep_hypreal_omega = thm"Rep_hypreal_omega"; |
|
114 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; |
|
115 val lemma_finite_omega_set = thm"lemma_finite_omega_set"; |
|
116 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; |
|
117 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; |
|
118 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; |
|
119 val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon"; |
|
120 val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero"; |
|
121 val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega"; |
|
122 *} |
7 *} |
123 |
8 |
124 end |
9 end |