10751
|
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 |
|
14297
|
8 |
theory HyperOrd = HyperDef:
|
|
9 |
|
14310
|
10 |
|
|
11 |
(*** Monotonicity results ***)
|
|
12 |
|
|
13 |
lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
|
|
14 |
by (rule Ring_and_Field.add_less_cancel_right)
|
|
15 |
|
|
16 |
lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
|
|
17 |
by (rule Ring_and_Field.add_less_cancel_left)
|
|
18 |
|
|
19 |
lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))"
|
|
20 |
by (rule Ring_and_Field.add_le_cancel_right)
|
|
21 |
|
|
22 |
lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))"
|
|
23 |
by (rule Ring_and_Field.add_le_cancel_left)
|
|
24 |
|
|
25 |
lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"
|
|
26 |
by (rule Ring_and_Field.add_strict_mono)
|
|
27 |
|
|
28 |
lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j; k\<le>l |] ==> i + k \<le> j + l"
|
|
29 |
by (rule Ring_and_Field.add_mono)
|
|
30 |
|
|
31 |
lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l"
|
|
32 |
by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
|
|
33 |
|
|
34 |
lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B"
|
|
35 |
by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute)
|
|
36 |
|
|
37 |
lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j; k<l |] ==> i + k < j + l"
|
|
38 |
apply (erule add_right_mono [THEN order_le_less_trans])
|
|
39 |
apply (erule add_strict_left_mono)
|
|
40 |
done
|
|
41 |
|
|
42 |
lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
|
|
43 |
apply (simp (no_asm_use))
|
|
44 |
done
|
|
45 |
|
|
46 |
lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
|
|
47 |
apply (simp (no_asm_use))
|
|
48 |
done
|
|
49 |
|
|
50 |
lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y"
|
|
51 |
by (auto dest: hypreal_add_less_le_mono)
|
|
52 |
|
14312
|
53 |
lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B"
|
|
54 |
by (rule Ring_and_Field.add_le_imp_le_right)
|
14297
|
55 |
|
14312
|
56 |
lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B"
|
|
57 |
apply (simp add: );
|
14297
|
58 |
done
|
|
59 |
|
14312
|
60 |
lemma hypreal_le_square [simp]: "(0::hypreal) \<le> x*x"
|
|
61 |
by (rule Ring_and_Field.zero_le_square)
|
14310
|
62 |
|
|
63 |
lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"
|
|
64 |
apply (erule order_less_trans)
|
|
65 |
apply (drule hypreal_add_less_mono2, simp)
|
|
66 |
done
|
14297
|
67 |
|
14310
|
68 |
lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
|
|
69 |
apply (drule order_le_imp_less_or_eq)+
|
|
70 |
apply (auto intro: hypreal_add_order order_less_imp_le)
|
|
71 |
done
|
|
72 |
|
|
73 |
text{*The precondition could be weakened to @{term "0\<le>x"}*}
|
|
74 |
lemma hypreal_mult_less_mono:
|
|
75 |
"[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
|
|
76 |
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
|
|
77 |
|
|
78 |
lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
|
|
79 |
by (rule Ring_and_Field.positive_imp_inverse_positive)
|
|
80 |
|
|
81 |
lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
|
|
82 |
by (rule Ring_and_Field.negative_imp_inverse_negative)
|
14297
|
83 |
|
|
84 |
|
14312
|
85 |
subsection{*Existence of Infinite Hyperreal Number*}
|
14297
|
86 |
|
14299
|
87 |
lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
|
14297
|
88 |
apply (unfold omega_def)
|
|
89 |
apply (rule Rep_hypreal)
|
|
90 |
done
|
|
91 |
|
|
92 |
(* existence of infinite number not corresponding to any real number *)
|
|
93 |
(* use assumption that member FreeUltrafilterNat is not finite *)
|
|
94 |
(* a few lemmas first *)
|
|
95 |
|
|
96 |
lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
|
14299
|
97 |
(\<exists>y. {n::nat. x = real n} = {y})"
|
14297
|
98 |
by (force dest: inj_real_of_nat [THEN injD])
|
|
99 |
|
|
100 |
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
|
|
101 |
by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
|
|
102 |
|
|
103 |
lemma not_ex_hypreal_of_real_eq_omega:
|
14299
|
104 |
"~ (\<exists>x. hypreal_of_real x = omega)"
|
14297
|
105 |
apply (unfold omega_def hypreal_of_real_def)
|
|
106 |
apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
|
|
107 |
done
|
|
108 |
|
14299
|
109 |
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
|
14297
|
110 |
by (cut_tac not_ex_hypreal_of_real_eq_omega, auto)
|
|
111 |
|
|
112 |
(* existence of infinitesimal number also not *)
|
|
113 |
(* corresponding to any real number *)
|
|
114 |
|
|
115 |
lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y"
|
|
116 |
by (rule inj_real_of_nat [THEN injD], simp)
|
|
117 |
|
|
118 |
lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} |
|
14299
|
119 |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
|
14297
|
120 |
apply (auto simp add: inj_real_of_nat [THEN inj_eq])
|
|
121 |
done
|
|
122 |
|
|
123 |
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
|
|
124 |
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
|
|
125 |
|
|
126 |
lemma not_ex_hypreal_of_real_eq_epsilon:
|
14299
|
127 |
"~ (\<exists>x. hypreal_of_real x = epsilon)"
|
14297
|
128 |
apply (unfold epsilon_def hypreal_of_real_def)
|
|
129 |
apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
|
|
130 |
done
|
|
131 |
|
14299
|
132 |
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
|
14297
|
133 |
by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
|
|
134 |
|
14299
|
135 |
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
|
14297
|
136 |
by (unfold epsilon_def hypreal_zero_def, auto)
|
|
137 |
|
|
138 |
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
|
|
139 |
by (simp add: hypreal_inverse omega_def epsilon_def)
|
|
140 |
|
|
141 |
|
14303
|
142 |
subsection{*Routine Properties*}
|
10751
|
143 |
|
14303
|
144 |
(* this proof is so much simpler than one for reals!! *)
|
|
145 |
lemma hypreal_inverse_less_swap:
|
|
146 |
"[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"
|
|
147 |
by (rule Ring_and_Field.less_imp_inverse_less)
|
14297
|
148 |
|
14303
|
149 |
lemma hypreal_inverse_less_iff:
|
|
150 |
"[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)"
|
|
151 |
by (rule Ring_and_Field.inverse_less_iff_less)
|
14297
|
152 |
|
14303
|
153 |
lemma hypreal_inverse_le_iff:
|
|
154 |
"[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::hypreal))"
|
|
155 |
by (rule Ring_and_Field.inverse_le_iff_le)
|
14297
|
156 |
|
|
157 |
|
14303
|
158 |
subsection{*Convenient Biconditionals for Products of Signs*}
|
14297
|
159 |
|
14303
|
160 |
lemma hypreal_0_less_mult_iff:
|
|
161 |
"((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
|
|
162 |
by (rule Ring_and_Field.zero_less_mult_iff)
|
14297
|
163 |
|
14303
|
164 |
lemma hypreal_0_le_mult_iff: "((0::hypreal) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
|
|
165 |
by (rule Ring_and_Field.zero_le_mult_iff)
|
14297
|
166 |
|
|
167 |
lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"
|
14303
|
168 |
by (rule Ring_and_Field.mult_less_0_iff)
|
|
169 |
|
|
170 |
lemma hypreal_mult_le_0_iff: "(x*y \<le> (0::hypreal)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
|
|
171 |
by (rule Ring_and_Field.mult_le_0_iff)
|
|
172 |
|
14297
|
173 |
|
14303
|
174 |
lemma hypreal_mult_self_sum_ge_zero: "(0::hypreal) \<le> x*x + y*y"
|
|
175 |
proof -
|
|
176 |
have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square)
|
|
177 |
thus ?thesis by simp
|
|
178 |
qed
|
14297
|
179 |
|
14299
|
180 |
(*TO BE DELETED*)
|
|
181 |
ML
|
|
182 |
{*
|
|
183 |
val hypreal_add_ac = thms"hypreal_add_ac";
|
|
184 |
val hypreal_mult_ac = thms"hypreal_mult_ac";
|
|
185 |
|
|
186 |
val hypreal_less_irrefl = thm"hypreal_less_irrefl";
|
|
187 |
*}
|
14297
|
188 |
|
|
189 |
ML
|
|
190 |
{*
|
|
191 |
val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1";
|
|
192 |
val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2";
|
|
193 |
val hypreal_mult_order = thm"hypreal_mult_order";
|
|
194 |
val hypreal_le_add_order = thm"hypreal_le_add_order";
|
|
195 |
val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less";
|
|
196 |
val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less";
|
|
197 |
val hypreal_add_right_cancel_le = thm"hypreal_add_right_cancel_le";
|
|
198 |
val hypreal_add_left_cancel_le = thm"hypreal_add_left_cancel_le";
|
|
199 |
val hypreal_add_less_mono = thm"hypreal_add_less_mono";
|
|
200 |
val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1";
|
|
201 |
val hypreal_add_le_mono = thm"hypreal_add_le_mono";
|
|
202 |
val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono";
|
|
203 |
val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono";
|
|
204 |
val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel";
|
|
205 |
val hypreal_less_add_left_cancel = thm"hypreal_less_add_left_cancel";
|
|
206 |
val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono";
|
|
207 |
val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel";
|
|
208 |
val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel";
|
|
209 |
val hypreal_le_square = thm"hypreal_le_square";
|
|
210 |
val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1";
|
|
211 |
val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
|
|
212 |
val hypreal_mult_less_mono = thm"hypreal_mult_less_mono";
|
|
213 |
val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0";
|
|
214 |
val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0";
|
|
215 |
val Rep_hypreal_omega = thm"Rep_hypreal_omega";
|
|
216 |
val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
|
|
217 |
val lemma_finite_omega_set = thm"lemma_finite_omega_set";
|
|
218 |
val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
|
|
219 |
val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
|
|
220 |
val real_of_nat_inverse_inj = thm"real_of_nat_inverse_inj";
|
|
221 |
val lemma_epsilon_empty_singleton_disj = thm"lemma_epsilon_empty_singleton_disj";
|
|
222 |
val lemma_finite_epsilon_set = thm"lemma_finite_epsilon_set";
|
|
223 |
val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
|
|
224 |
val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
|
|
225 |
val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
|
|
226 |
val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
|
|
227 |
val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap";
|
|
228 |
val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff";
|
14303
|
229 |
val hypreal_inverse_le_iff = thm"hypreal_inverse_le_iff";
|
14297
|
230 |
val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff";
|
|
231 |
val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff";
|
|
232 |
val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff";
|
|
233 |
val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff";
|
14303
|
234 |
val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero";
|
14297
|
235 |
*}
|
10751
|
236 |
|
|
237 |
end
|