7218
|
1 |
(* Title : HOL/Real/Hyperreal/Hyper.ML
|
|
2 |
ID : $Id$
|
|
3 |
Author : Jacques D. Fleuriot
|
|
4 |
Copyright : 1998 University of Cambridge
|
|
5 |
Description : Ultrapower construction of hyperreals
|
|
6 |
*)
|
|
7 |
|
|
8 |
(*------------------------------------------------------------------------
|
|
9 |
Proof that the set of naturals is not finite
|
|
10 |
------------------------------------------------------------------------*)
|
|
11 |
|
|
12 |
(*** based on James' proof that the set of naturals is not finite ***)
|
|
13 |
Goal "finite (A::nat set) --> (? n. !m. Suc (n + m) ~: A)";
|
|
14 |
by (rtac impI 1);
|
|
15 |
by (eres_inst_tac [("F","A")] finite_induct 1);
|
|
16 |
by (Blast_tac 1 THEN etac exE 1);
|
|
17 |
by (res_inst_tac [("x","n + x")] exI 1);
|
|
18 |
by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1);
|
|
19 |
by (auto_tac (claset(), simpset() addsimps add_ac));
|
|
20 |
by (auto_tac (claset(),
|
|
21 |
simpset() addsimps [add_assoc RS sym,
|
|
22 |
less_add_Suc2 RS less_not_refl2]));
|
|
23 |
qed_spec_mp "finite_exhausts";
|
|
24 |
|
|
25 |
Goal "finite (A :: nat set) --> (? n. n ~:A)";
|
|
26 |
by (rtac impI 1 THEN dtac finite_exhausts 1);
|
|
27 |
by (Blast_tac 1);
|
|
28 |
qed_spec_mp "finite_not_covers";
|
|
29 |
|
|
30 |
Goal "~ finite(UNIV:: nat set)";
|
|
31 |
by (fast_tac (claset() addSDs [finite_exhausts]) 1);
|
|
32 |
qed "not_finite_nat";
|
|
33 |
|
|
34 |
(*------------------------------------------------------------------------
|
|
35 |
Existence of free ultrafilter over the naturals and proof of various
|
|
36 |
properties of the FreeUltrafilterNat- an arbitrary free ultrafilter
|
|
37 |
------------------------------------------------------------------------*)
|
|
38 |
|
|
39 |
Goal "EX U. U: FreeUltrafilter (UNIV::nat set)";
|
|
40 |
by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1);
|
|
41 |
qed "FreeUltrafilterNat_Ex";
|
|
42 |
|
|
43 |
Goalw [FreeUltrafilterNat_def]
|
|
44 |
"FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
|
|
45 |
by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
|
|
46 |
by (rtac selectI2 1 THEN ALLGOALS(assume_tac));
|
|
47 |
qed "FreeUltrafilterNat_mem";
|
|
48 |
Addsimps [FreeUltrafilterNat_mem];
|
|
49 |
|
|
50 |
Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
|
|
51 |
by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
|
|
52 |
by (rtac selectI2 1 THEN assume_tac 1);
|
|
53 |
by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
|
|
54 |
qed "FreeUltrafilterNat_finite";
|
|
55 |
|
|
56 |
Goal "x: FreeUltrafilterNat ==> ~ finite x";
|
|
57 |
by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1);
|
|
58 |
qed "FreeUltrafilterNat_not_finite";
|
|
59 |
|
|
60 |
Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
|
|
61 |
by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
|
|
62 |
by (rtac selectI2 1 THEN assume_tac 1);
|
|
63 |
by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
|
|
64 |
Ultrafilter_Filter,Filter_empty_not_mem]) 1);
|
|
65 |
qed "FreeUltrafilterNat_empty";
|
|
66 |
Addsimps [FreeUltrafilterNat_empty];
|
|
67 |
|
|
68 |
Goal "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] \
|
|
69 |
\ ==> X Int Y : FreeUltrafilterNat";
|
|
70 |
by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
|
|
71 |
by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
|
|
72 |
Ultrafilter_Filter,mem_FiltersetD1]) 1);
|
|
73 |
qed "FreeUltrafilterNat_Int";
|
|
74 |
|
|
75 |
Goal "[| X: FreeUltrafilterNat; X <= Y |] \
|
|
76 |
\ ==> Y : FreeUltrafilterNat";
|
|
77 |
by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
|
|
78 |
by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
|
|
79 |
Ultrafilter_Filter,mem_FiltersetD2]) 1);
|
|
80 |
qed "FreeUltrafilterNat_subset";
|
|
81 |
|
|
82 |
Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat";
|
|
83 |
by (Step_tac 1);
|
|
84 |
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
|
|
85 |
by Auto_tac;
|
|
86 |
qed "FreeUltrafilterNat_Compl";
|
|
87 |
|
|
88 |
Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
|
|
89 |
by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
|
|
90 |
by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
|
|
91 |
by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl]));
|
|
92 |
qed "FreeUltrafilterNat_Compl_mem";
|
|
93 |
|
|
94 |
Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
|
|
95 |
by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl,
|
|
96 |
FreeUltrafilterNat_Compl_mem]) 1);
|
|
97 |
qed "FreeUltrafilterNat_Compl_iff1";
|
|
98 |
|
|
99 |
Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)";
|
|
100 |
by (auto_tac (claset(),
|
|
101 |
simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym]));
|
|
102 |
qed "FreeUltrafilterNat_Compl_iff2";
|
|
103 |
|
|
104 |
Goal "(UNIV::nat set) : FreeUltrafilterNat";
|
|
105 |
by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS
|
|
106 |
Ultrafilter_Filter RS mem_FiltersetD4) 1);
|
|
107 |
qed "FreeUltrafilterNat_UNIV";
|
|
108 |
Addsimps [FreeUltrafilterNat_UNIV];
|
|
109 |
|
|
110 |
Goal "{n::nat. True}: FreeUltrafilterNat";
|
|
111 |
by (subgoal_tac "{n::nat. True} = (UNIV::nat set)" 1);
|
|
112 |
by Auto_tac;
|
|
113 |
qed "FreeUltrafilterNat_Nat_set";
|
|
114 |
Addsimps [FreeUltrafilterNat_Nat_set];
|
|
115 |
|
|
116 |
Goal "{n. P(n) = P(n)} : FreeUltrafilterNat";
|
|
117 |
by (Simp_tac 1);
|
|
118 |
qed "FreeUltrafilterNat_Nat_set_refl";
|
|
119 |
AddIs [FreeUltrafilterNat_Nat_set_refl];
|
|
120 |
|
|
121 |
Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
|
|
122 |
by (rtac ccontr 1);
|
|
123 |
by (rotate_tac 1 1);
|
|
124 |
by (Asm_full_simp_tac 1);
|
|
125 |
qed "FreeUltrafilterNat_P";
|
|
126 |
|
|
127 |
Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
|
|
128 |
by (rtac ccontr 1 THEN rotate_tac 1 1);
|
|
129 |
by (Asm_full_simp_tac 1);
|
|
130 |
qed "FreeUltrafilterNat_Ex_P";
|
|
131 |
|
|
132 |
Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
|
|
133 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
|
|
134 |
qed "FreeUltrafilterNat_all";
|
|
135 |
|
|
136 |
(*-----------------------------------------
|
|
137 |
Define and use Ultrafilter tactics
|
|
138 |
-----------------------------------------*)
|
|
139 |
use "fuf.ML";
|
|
140 |
|
|
141 |
|
|
142 |
|
|
143 |
(*------------------------------------------------------
|
|
144 |
Now prove one further property of our free ultrafilter
|
|
145 |
-------------------------------------------------------*)
|
|
146 |
Goal "X Un Y: FreeUltrafilterNat \
|
|
147 |
\ ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
|
|
148 |
by Auto_tac;
|
|
149 |
by (Ultra_tac 1);
|
|
150 |
qed "FreeUltrafilterNat_Un";
|
|
151 |
|
|
152 |
(*------------------------------------------------------------------------
|
|
153 |
Properties of hyprel
|
|
154 |
------------------------------------------------------------------------*)
|
|
155 |
|
|
156 |
(** Proving that hyprel is an equivalence relation **)
|
|
157 |
(** Natural deduction for hyprel **)
|
|
158 |
|
|
159 |
Goalw [hyprel_def]
|
|
160 |
"((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)";
|
|
161 |
by (Fast_tac 1);
|
|
162 |
qed "hyprel_iff";
|
|
163 |
|
|
164 |
Goalw [hyprel_def]
|
|
165 |
"{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hyprel";
|
|
166 |
by (Fast_tac 1);
|
|
167 |
qed "hyprelI";
|
|
168 |
|
|
169 |
Goalw [hyprel_def]
|
|
170 |
"p: hyprel --> (EX X Y. \
|
|
171 |
\ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
|
|
172 |
by (Fast_tac 1);
|
|
173 |
qed "hyprelE_lemma";
|
|
174 |
|
|
175 |
val [major,minor] = goal thy
|
|
176 |
"[| p: hyprel; \
|
|
177 |
\ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
|
|
178 |
\ |] ==> Q |] ==> Q";
|
|
179 |
by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1);
|
|
180 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
|
|
181 |
qed "hyprelE";
|
|
182 |
|
|
183 |
AddSIs [hyprelI];
|
|
184 |
AddSEs [hyprelE];
|
|
185 |
|
|
186 |
Goalw [hyprel_def] "(x,x): hyprel";
|
|
187 |
by (auto_tac (claset(),simpset() addsimps
|
|
188 |
[FreeUltrafilterNat_Nat_set]));
|
|
189 |
qed "hyprel_refl";
|
|
190 |
|
|
191 |
Goal "{n. X n = Y n} = {n. Y n = X n}";
|
|
192 |
by Auto_tac;
|
|
193 |
qed "lemma_perm";
|
|
194 |
|
|
195 |
Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
|
|
196 |
by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
|
|
197 |
qed_spec_mp "hyprel_sym";
|
|
198 |
|
|
199 |
Goalw [hyprel_def]
|
|
200 |
"(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
|
|
201 |
by Auto_tac;
|
|
202 |
by (Ultra_tac 1);
|
|
203 |
qed_spec_mp "hyprel_trans";
|
|
204 |
|
|
205 |
Goalw [equiv_def, refl_def, sym_def, trans_def]
|
|
206 |
"equiv {x::nat=>real. True} hyprel";
|
|
207 |
by (auto_tac (claset() addSIs [hyprel_refl]
|
|
208 |
addSEs [hyprel_sym,hyprel_trans]
|
|
209 |
delrules [hyprelI,hyprelE],
|
|
210 |
simpset() addsimps [FreeUltrafilterNat_Nat_set]));
|
|
211 |
qed "equiv_hyprel";
|
|
212 |
|
|
213 |
val equiv_hyprel_iff =
|
|
214 |
[TrueI, TrueI] MRS
|
|
215 |
([CollectI, CollectI] MRS
|
|
216 |
(equiv_hyprel RS eq_equiv_class_iff));
|
|
217 |
|
|
218 |
Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
|
|
219 |
by (Blast_tac 1);
|
|
220 |
qed "hyprel_in_hypreal";
|
|
221 |
|
|
222 |
Goal "inj_on Abs_hypreal hypreal";
|
|
223 |
by (rtac inj_on_inverseI 1);
|
|
224 |
by (etac Abs_hypreal_inverse 1);
|
|
225 |
qed "inj_on_Abs_hypreal";
|
|
226 |
|
|
227 |
Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff,
|
|
228 |
hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
|
|
229 |
|
|
230 |
Addsimps [equiv_hyprel RS eq_equiv_class_iff];
|
|
231 |
val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class);
|
|
232 |
|
|
233 |
Goal "inj(Rep_hypreal)";
|
|
234 |
by (rtac inj_inverseI 1);
|
|
235 |
by (rtac Rep_hypreal_inverse 1);
|
|
236 |
qed "inj_Rep_hypreal";
|
|
237 |
|
|
238 |
Goalw [hyprel_def] "x: hyprel ^^ {x}";
|
|
239 |
by (Step_tac 1);
|
|
240 |
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
|
|
241 |
qed "lemma_hyprel_refl";
|
|
242 |
|
|
243 |
Addsimps [lemma_hyprel_refl];
|
|
244 |
|
|
245 |
Goalw [hypreal_def] "{} ~: hypreal";
|
|
246 |
by (auto_tac (claset() addSEs [quotientE], simpset()));
|
|
247 |
qed "hypreal_empty_not_mem";
|
|
248 |
|
|
249 |
Addsimps [hypreal_empty_not_mem];
|
|
250 |
|
|
251 |
Goal "Rep_hypreal x ~= {}";
|
|
252 |
by (cut_inst_tac [("x","x")] Rep_hypreal 1);
|
|
253 |
by Auto_tac;
|
|
254 |
qed "Rep_hypreal_nonempty";
|
|
255 |
|
|
256 |
Addsimps [Rep_hypreal_nonempty];
|
|
257 |
|
|
258 |
(*------------------------------------------------------------------------
|
|
259 |
hypreal_of_real: the injection from real to hypreal
|
|
260 |
------------------------------------------------------------------------*)
|
|
261 |
|
|
262 |
Goal "inj(hypreal_of_real)";
|
|
263 |
by (rtac injI 1);
|
|
264 |
by (rewtac hypreal_of_real_def);
|
|
265 |
by (dtac (inj_on_Abs_hypreal RS inj_onD) 1);
|
|
266 |
by (REPEAT (rtac hyprel_in_hypreal 1));
|
|
267 |
by (dtac eq_equiv_class 1);
|
|
268 |
by (rtac equiv_hyprel 1);
|
|
269 |
by (Fast_tac 1);
|
|
270 |
by (rtac ccontr 1 THEN rotate_tac 1 1);
|
|
271 |
by Auto_tac;
|
|
272 |
qed "inj_hypreal_of_real";
|
|
273 |
|
|
274 |
val [prem] = goal thy
|
|
275 |
"(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P";
|
|
276 |
by (res_inst_tac [("x1","z")]
|
|
277 |
(rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
|
|
278 |
by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
279 |
by (res_inst_tac [("x","x")] prem 1);
|
|
280 |
by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1);
|
|
281 |
qed "eq_Abs_hypreal";
|
|
282 |
|
|
283 |
(**** hypreal_minus: additive inverse on hypreal ****)
|
|
284 |
|
|
285 |
Goalw [congruent_def]
|
|
286 |
"congruent hyprel (%X. hyprel^^{%n. - (X n)})";
|
|
287 |
by Safe_tac;
|
|
288 |
by (ALLGOALS Ultra_tac);
|
|
289 |
qed "hypreal_minus_congruent";
|
|
290 |
|
|
291 |
(*Resolve th against the corresponding facts for hypreal_minus*)
|
|
292 |
val hypreal_minus_ize = RSLIST [equiv_hyprel, hypreal_minus_congruent];
|
|
293 |
|
|
294 |
Goalw [hypreal_minus_def]
|
|
295 |
"- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
|
|
296 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
297 |
by (simp_tac (simpset() addsimps
|
|
298 |
[hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_minus_ize UN_equiv_class]) 1);
|
|
299 |
qed "hypreal_minus";
|
|
300 |
|
|
301 |
Goal "- (- z) = (z::hypreal)";
|
|
302 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
303 |
by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);
|
|
304 |
qed "hypreal_minus_minus";
|
|
305 |
|
|
306 |
Addsimps [hypreal_minus_minus];
|
|
307 |
|
|
308 |
Goal "inj(%r::hypreal. -r)";
|
|
309 |
by (rtac injI 1);
|
|
310 |
by (dres_inst_tac [("f","uminus")] arg_cong 1);
|
|
311 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
|
|
312 |
qed "inj_hypreal_minus";
|
|
313 |
|
|
314 |
Goalw [hypreal_zero_def] "-0hr = 0hr";
|
|
315 |
by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
|
|
316 |
qed "hypreal_minus_zero";
|
|
317 |
|
|
318 |
Addsimps [hypreal_minus_zero];
|
|
319 |
|
|
320 |
Goal "(-x = 0hr) = (x = 0hr)";
|
|
321 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
322 |
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
|
|
323 |
hypreal_minus] @ real_add_ac));
|
|
324 |
qed "hypreal_minus_zero_iff";
|
|
325 |
|
|
326 |
Addsimps [hypreal_minus_zero_iff];
|
|
327 |
(**** hrinv: multiplicative inverse on hypreal ****)
|
|
328 |
|
|
329 |
Goalw [congruent_def]
|
|
330 |
"congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
|
|
331 |
by (Auto_tac THEN Ultra_tac 1);
|
|
332 |
qed "hypreal_hrinv_congruent";
|
|
333 |
|
|
334 |
(* Resolve th against the corresponding facts for hrinv *)
|
|
335 |
val hypreal_hrinv_ize = RSLIST [equiv_hyprel, hypreal_hrinv_congruent];
|
|
336 |
|
|
337 |
Goalw [hrinv_def]
|
|
338 |
"hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
|
|
339 |
\ Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
|
|
340 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
341 |
by (simp_tac (simpset() addsimps
|
|
342 |
[hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
|
|
343 |
qed "hypreal_hrinv";
|
|
344 |
|
|
345 |
Goal "z ~= 0hr ==> hrinv (hrinv z) = z";
|
|
346 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
347 |
by (rotate_tac 1 1);
|
|
348 |
by (asm_full_simp_tac (simpset() addsimps
|
|
349 |
[hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
|
|
350 |
by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
|
|
351 |
qed "hypreal_hrinv_hrinv";
|
|
352 |
|
|
353 |
Addsimps [hypreal_hrinv_hrinv];
|
|
354 |
|
|
355 |
Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
|
|
356 |
by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
|
|
357 |
real_zero_not_eq_one RS not_sym]
|
|
358 |
setloop (split_tac [expand_if])) 1);
|
|
359 |
qed "hypreal_hrinv_1";
|
|
360 |
Addsimps [hypreal_hrinv_1];
|
|
361 |
|
|
362 |
(**** hyperreal addition: hypreal_add ****)
|
|
363 |
|
|
364 |
Goalw [congruent2_def]
|
|
365 |
"congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
|
|
366 |
by Safe_tac;
|
|
367 |
by (ALLGOALS(Ultra_tac));
|
|
368 |
qed "hypreal_add_congruent2";
|
|
369 |
|
|
370 |
(*Resolve th against the corresponding facts for hyppreal_add*)
|
|
371 |
val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
|
|
372 |
|
|
373 |
Goalw [hypreal_add_def]
|
|
374 |
"Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
|
|
375 |
\ Abs_hypreal(hyprel^^{%n. X n + Y n})";
|
|
376 |
by (asm_simp_tac
|
|
377 |
(simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
|
|
378 |
qed "hypreal_add";
|
|
379 |
|
|
380 |
Goal "(z::hypreal) + w = w + z";
|
|
381 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
382 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
383 |
by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
|
|
384 |
qed "hypreal_add_commute";
|
|
385 |
|
|
386 |
Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
|
|
387 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
388 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
389 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
|
|
390 |
by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
|
|
391 |
qed "hypreal_add_assoc";
|
|
392 |
|
|
393 |
(*For AC rewriting*)
|
|
394 |
Goal "(x::hypreal)+(y+z)=y+(x+z)";
|
|
395 |
by (rtac (hypreal_add_commute RS trans) 1);
|
|
396 |
by (rtac (hypreal_add_assoc RS trans) 1);
|
|
397 |
by (rtac (hypreal_add_commute RS arg_cong) 1);
|
|
398 |
qed "hypreal_add_left_commute";
|
|
399 |
|
|
400 |
(* hypreal addition is an AC operator *)
|
|
401 |
val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
|
|
402 |
hypreal_add_left_commute];
|
|
403 |
|
|
404 |
Goalw [hypreal_zero_def] "0hr + z = z";
|
|
405 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
406 |
by (asm_full_simp_tac (simpset() addsimps
|
|
407 |
[hypreal_add]) 1);
|
|
408 |
qed "hypreal_add_zero_left";
|
|
409 |
|
|
410 |
Goal "z + 0hr = z";
|
|
411 |
by (simp_tac (simpset() addsimps
|
|
412 |
[hypreal_add_zero_left,hypreal_add_commute]) 1);
|
|
413 |
qed "hypreal_add_zero_right";
|
|
414 |
|
|
415 |
Goalw [hypreal_zero_def] "z + -z = 0hr";
|
|
416 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
417 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
|
|
418 |
hypreal_add]) 1);
|
|
419 |
qed "hypreal_add_minus";
|
|
420 |
|
|
421 |
Goal "-z + z = 0hr";
|
|
422 |
by (simp_tac (simpset() addsimps
|
|
423 |
[hypreal_add_commute,hypreal_add_minus]) 1);
|
|
424 |
qed "hypreal_add_minus_left";
|
|
425 |
|
|
426 |
Addsimps [hypreal_add_minus,hypreal_add_minus_left,
|
|
427 |
hypreal_add_zero_left,hypreal_add_zero_right];
|
|
428 |
|
|
429 |
Goal "? y. (x::hypreal) + y = 0hr";
|
|
430 |
by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
|
|
431 |
qed "hypreal_minus_ex";
|
|
432 |
|
|
433 |
Goal "?! y. (x::hypreal) + y = 0hr";
|
|
434 |
by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
|
|
435 |
by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
|
|
436 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
437 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
438 |
qed "hypreal_minus_ex1";
|
|
439 |
|
|
440 |
Goal "?! y. y + (x::hypreal) = 0hr";
|
|
441 |
by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
|
|
442 |
by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
|
|
443 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
|
|
444 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
445 |
qed "hypreal_minus_left_ex1";
|
|
446 |
|
|
447 |
Goal "x + y = 0hr ==> x = -y";
|
|
448 |
by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
|
|
449 |
by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
|
|
450 |
by (Blast_tac 1);
|
|
451 |
qed "hypreal_add_minus_eq_minus";
|
|
452 |
|
|
453 |
Goal "? y::hypreal. x = -y";
|
|
454 |
by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
|
|
455 |
by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
|
|
456 |
by (Fast_tac 1);
|
|
457 |
qed "hypreal_as_add_inverse_ex";
|
|
458 |
|
|
459 |
Goal "-(x + (y::hypreal)) = -x + -y";
|
|
460 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
461 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
462 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
|
|
463 |
hypreal_add,real_minus_add_distrib]));
|
|
464 |
qed "hypreal_minus_add_distrib";
|
|
465 |
|
|
466 |
Goal "-(y + -(x::hypreal)) = x + -y";
|
|
467 |
by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
|
|
468 |
hypreal_add_commute]) 1);
|
|
469 |
qed "hypreal_minus_distrib1";
|
|
470 |
|
|
471 |
Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
|
|
472 |
by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
|
|
473 |
by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
|
|
474 |
hypreal_add_assoc]) 1);
|
|
475 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
476 |
qed "hypreal_add_minus_cancel1";
|
|
477 |
|
|
478 |
Goal "((x::hypreal) + y = x + z) = (y = z)";
|
|
479 |
by (Step_tac 1);
|
|
480 |
by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
|
|
481 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
482 |
qed "hypreal_add_left_cancel";
|
|
483 |
|
|
484 |
Goal "z + (x + (y + -z)) = x + (y::hypreal)";
|
|
485 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
486 |
qed "hypreal_add_minus_cancel2";
|
|
487 |
Addsimps [hypreal_add_minus_cancel2];
|
|
488 |
|
|
489 |
Goal "y + -(x + y) = -(x::hypreal)";
|
|
490 |
by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
|
|
491 |
by (rtac (hypreal_add_left_commute RS subst) 1);
|
|
492 |
by (Full_simp_tac 1);
|
|
493 |
qed "hypreal_add_minus_cancel";
|
|
494 |
Addsimps [hypreal_add_minus_cancel];
|
|
495 |
|
|
496 |
Goal "y + -(y + x) = -(x::hypreal)";
|
|
497 |
by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
|
|
498 |
hypreal_add_assoc RS sym]) 1);
|
|
499 |
qed "hypreal_add_minus_cancelc";
|
|
500 |
Addsimps [hypreal_add_minus_cancelc];
|
|
501 |
|
|
502 |
Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
|
|
503 |
by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
|
|
504 |
RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1);
|
|
505 |
qed "hypreal_add_minus_cancel3";
|
|
506 |
Addsimps [hypreal_add_minus_cancel3];
|
|
507 |
|
|
508 |
Goal "(y + (x::hypreal)= z + x) = (y = z)";
|
|
509 |
by (simp_tac (simpset() addsimps [hypreal_add_commute,
|
|
510 |
hypreal_add_left_cancel]) 1);
|
|
511 |
qed "hypreal_add_right_cancel";
|
|
512 |
|
|
513 |
Goal "z + (y + -z) = (y::hypreal)";
|
|
514 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
515 |
qed "hypreal_add_minus_cancel4";
|
|
516 |
Addsimps [hypreal_add_minus_cancel4];
|
|
517 |
|
|
518 |
Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
|
|
519 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
520 |
qed "hypreal_add_minus_cancel5";
|
|
521 |
Addsimps [hypreal_add_minus_cancel5];
|
|
522 |
|
|
523 |
|
|
524 |
(**** hyperreal multiplication: hypreal_mult ****)
|
|
525 |
|
|
526 |
Goalw [congruent2_def]
|
|
527 |
"congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
|
|
528 |
by Safe_tac;
|
|
529 |
by (ALLGOALS(Ultra_tac));
|
|
530 |
qed "hypreal_mult_congruent2";
|
|
531 |
|
|
532 |
(*Resolve th against the corresponding facts for hypreal_mult*)
|
|
533 |
val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
|
|
534 |
|
|
535 |
Goalw [hypreal_mult_def]
|
|
536 |
"Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
|
|
537 |
\ Abs_hypreal(hyprel^^{%n. X n * Y n})";
|
|
538 |
by (asm_simp_tac
|
|
539 |
(simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
|
|
540 |
qed "hypreal_mult";
|
|
541 |
|
|
542 |
Goal "(z::hypreal) * w = w * z";
|
|
543 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
544 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
545 |
by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
|
|
546 |
qed "hypreal_mult_commute";
|
|
547 |
|
|
548 |
Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
|
|
549 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
550 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
551 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
|
|
552 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
|
|
553 |
qed "hypreal_mult_assoc";
|
|
554 |
|
|
555 |
qed_goal "hypreal_mult_left_commute" thy
|
|
556 |
"(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
|
|
557 |
(fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
|
|
558 |
rtac (hypreal_mult_commute RS arg_cong) 1]);
|
|
559 |
|
|
560 |
(* hypreal multiplication is an AC operator *)
|
|
561 |
val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute,
|
|
562 |
hypreal_mult_left_commute];
|
|
563 |
|
|
564 |
Goalw [hypreal_one_def] "1hr * z = z";
|
|
565 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
566 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
|
|
567 |
qed "hypreal_mult_1";
|
|
568 |
|
|
569 |
Goal "z * 1hr = z";
|
|
570 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute,
|
|
571 |
hypreal_mult_1]) 1);
|
|
572 |
qed "hypreal_mult_1_right";
|
|
573 |
|
|
574 |
Goalw [hypreal_zero_def] "0hr * z = 0hr";
|
|
575 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
576 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
|
|
577 |
qed "hypreal_mult_0";
|
|
578 |
|
|
579 |
Goal "z * 0hr = 0hr";
|
|
580 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute,
|
|
581 |
hypreal_mult_0]) 1);
|
|
582 |
qed "hypreal_mult_0_right";
|
|
583 |
|
|
584 |
Addsimps [hypreal_mult_0,hypreal_mult_0_right];
|
|
585 |
|
|
586 |
Goal "-(x * y) = -x * (y::hypreal)";
|
|
587 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
588 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
589 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
|
|
590 |
hypreal_mult,real_minus_mult_eq1]
|
|
591 |
@ real_mult_ac @ real_add_ac));
|
|
592 |
qed "hypreal_minus_mult_eq1";
|
|
593 |
|
|
594 |
Goal "-(x * y) = (x::hypreal) * -y";
|
|
595 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
596 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
597 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
|
|
598 |
hypreal_mult,real_minus_mult_eq2]
|
|
599 |
@ real_mult_ac @ real_add_ac));
|
|
600 |
qed "hypreal_minus_mult_eq2";
|
|
601 |
|
|
602 |
Goal "-x*-y = x*(y::hypreal)";
|
|
603 |
by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
|
|
604 |
hypreal_minus_mult_eq1 RS sym]) 1);
|
|
605 |
qed "hypreal_minus_mult_cancel";
|
|
606 |
|
|
607 |
Addsimps [hypreal_minus_mult_cancel];
|
|
608 |
|
|
609 |
Goal "-x*y = (x::hypreal)*-y";
|
|
610 |
by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
|
|
611 |
hypreal_minus_mult_eq1 RS sym]) 1);
|
|
612 |
qed "hypreal_minus_mult_commute";
|
|
613 |
|
|
614 |
|
|
615 |
(*-----------------------------------------------------------------------------
|
|
616 |
A few more theorems
|
|
617 |
----------------------------------------------------------------------------*)
|
|
618 |
Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
|
|
619 |
by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
620 |
qed "hypreal_add_assoc_cong";
|
|
621 |
|
|
622 |
Goal "(z::hypreal) + (v + w) = v + (z + w)";
|
|
623 |
by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
|
|
624 |
qed "hypreal_add_assoc_swap";
|
|
625 |
|
|
626 |
Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
|
|
627 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
628 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
629 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
630 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
|
|
631 |
real_add_mult_distrib]) 1);
|
|
632 |
qed "hypreal_add_mult_distrib";
|
|
633 |
|
|
634 |
val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
|
|
635 |
|
|
636 |
Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
|
|
637 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
|
|
638 |
qed "hypreal_add_mult_distrib2";
|
|
639 |
|
|
640 |
val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
|
|
641 |
Addsimps hypreal_mult_simps;
|
|
642 |
|
|
643 |
(*** one and zero are distinct ***)
|
|
644 |
Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr";
|
|
645 |
by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
|
|
646 |
qed "hypreal_zero_not_eq_one";
|
|
647 |
|
|
648 |
(*** existence of inverse ***)
|
|
649 |
Goalw [hypreal_one_def,hypreal_zero_def]
|
|
650 |
"x ~= 0hr ==> x*hrinv(x) = 1hr";
|
|
651 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
652 |
by (rotate_tac 1 1);
|
|
653 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
|
|
654 |
hypreal_mult] setloop (split_tac [expand_if])) 1);
|
|
655 |
by (dtac FreeUltrafilterNat_Compl_mem 1);
|
|
656 |
by (blast_tac (claset() addSIs [real_mult_inv_right,
|
|
657 |
FreeUltrafilterNat_subset]) 1);
|
|
658 |
qed "hypreal_mult_hrinv";
|
|
659 |
|
|
660 |
Goal "x ~= 0hr ==> hrinv(x)*x = 1hr";
|
|
661 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
|
|
662 |
hypreal_mult_commute]) 1);
|
|
663 |
qed "hypreal_mult_hrinv_left";
|
|
664 |
|
|
665 |
Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr";
|
|
666 |
by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
|
|
667 |
qed "hypreal_hrinv_ex";
|
|
668 |
|
|
669 |
Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr";
|
|
670 |
by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
|
|
671 |
qed "hypreal_hrinv_left_ex";
|
|
672 |
|
|
673 |
Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr";
|
|
674 |
by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
|
|
675 |
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
|
|
676 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
|
|
677 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
|
|
678 |
qed "hypreal_hrinv_ex1";
|
|
679 |
|
|
680 |
Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr";
|
|
681 |
by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
|
|
682 |
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
|
|
683 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
|
|
684 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
|
|
685 |
qed "hypreal_hrinv_left_ex1";
|
|
686 |
|
|
687 |
Goal "[| y~= 0hr; x * y = 1hr |] ==> x = hrinv y";
|
|
688 |
by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
|
|
689 |
by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
|
|
690 |
by (assume_tac 1);
|
|
691 |
by (Blast_tac 1);
|
|
692 |
qed "hypreal_mult_inv_hrinv";
|
|
693 |
|
|
694 |
Goal "x ~= 0hr ==> ? y. x = hrinv y";
|
|
695 |
by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
|
|
696 |
by (etac exE 1 THEN
|
|
697 |
forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
|
|
698 |
by (res_inst_tac [("x","y")] exI 2);
|
|
699 |
by Auto_tac;
|
|
700 |
qed "hypreal_as_inverse_ex";
|
|
701 |
|
|
702 |
Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)";
|
|
703 |
by Auto_tac;
|
|
704 |
by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
|
|
705 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1);
|
|
706 |
qed "hypreal_mult_left_cancel";
|
|
707 |
|
|
708 |
Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)";
|
|
709 |
by (Step_tac 1);
|
|
710 |
by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
|
|
711 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1);
|
|
712 |
qed "hypreal_mult_right_cancel";
|
|
713 |
|
|
714 |
Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr";
|
|
715 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
716 |
by (rotate_tac 1 1);
|
|
717 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
|
|
718 |
hypreal_mult] setloop (split_tac [expand_if])) 1);
|
|
719 |
by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
|
|
720 |
by (ultra_tac (claset() addIs [ccontr] addDs
|
|
721 |
[rinv_not_zero],simpset()) 1);
|
|
722 |
qed "hrinv_not_zero";
|
|
723 |
|
|
724 |
Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
|
|
725 |
|
|
726 |
Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr";
|
|
727 |
by (Step_tac 1);
|
|
728 |
by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
|
|
729 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
|
|
730 |
qed "hypreal_mult_not_0";
|
|
731 |
|
|
732 |
bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
|
|
733 |
|
|
734 |
Goal "x ~= 0hr ==> x * x ~= 0hr";
|
|
735 |
by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
|
|
736 |
qed "hypreal_mult_self_not_zero";
|
|
737 |
|
|
738 |
Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
|
|
739 |
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
740 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
|
|
741 |
hypreal_mult_not_0]));
|
|
742 |
by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
|
|
743 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
|
|
744 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
|
|
745 |
qed "hrinv_mult_eq";
|
|
746 |
|
|
747 |
Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)";
|
|
748 |
by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1);
|
|
749 |
by Auto_tac;
|
|
750 |
qed "hypreal_minus_hrinv";
|
|
751 |
|
|
752 |
Goal "[| x ~= 0hr; y ~= 0hr |] \
|
|
753 |
\ ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
|
|
754 |
by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
|
|
755 |
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
756 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
|
|
757 |
by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
758 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
|
|
759 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
|
|
760 |
qed "hypreal_hrinv_distrib";
|
|
761 |
|
|
762 |
(*------------------------------------------------------------------
|
|
763 |
Theorems for ordering
|
|
764 |
------------------------------------------------------------------*)
|
|
765 |
|
|
766 |
(* prove introduction and elimination rules for hypreal_less *)
|
|
767 |
|
|
768 |
Goalw [hypreal_less_def]
|
|
769 |
"P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
|
|
770 |
\ Y : Rep_hypreal(Q) & \
|
|
771 |
\ {n. X n < Y n} : FreeUltrafilterNat)";
|
|
772 |
by (Fast_tac 1);
|
|
773 |
qed "hypreal_less_iff";
|
|
774 |
|
|
775 |
Goalw [hypreal_less_def]
|
|
776 |
"[| {n. X n < Y n} : FreeUltrafilterNat; \
|
|
777 |
\ X : Rep_hypreal(P); \
|
|
778 |
\ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
|
|
779 |
by (Fast_tac 1);
|
|
780 |
qed "hypreal_lessI";
|
|
781 |
|
|
782 |
|
|
783 |
Goalw [hypreal_less_def]
|
|
784 |
"!! R1. [| R1 < (R2::hypreal); \
|
|
785 |
\ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
|
|
786 |
\ !!X. X : Rep_hypreal(R1) ==> P; \
|
|
787 |
\ !!Y. Y : Rep_hypreal(R2) ==> P |] \
|
|
788 |
\ ==> P";
|
|
789 |
by Auto_tac;
|
|
790 |
qed "hypreal_lessE";
|
|
791 |
|
|
792 |
Goalw [hypreal_less_def]
|
|
793 |
"R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
|
|
794 |
\ X : Rep_hypreal(R1) & \
|
|
795 |
\ Y : Rep_hypreal(R2))";
|
|
796 |
by (Fast_tac 1);
|
|
797 |
qed "hypreal_lessD";
|
|
798 |
|
|
799 |
Goal "~ (R::hypreal) < R";
|
|
800 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
|
|
801 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
|
|
802 |
by (Ultra_tac 1);
|
|
803 |
qed "hypreal_less_not_refl";
|
|
804 |
|
|
805 |
(*** y < y ==> P ***)
|
|
806 |
bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
|
|
807 |
|
|
808 |
Goal "!!(x::hypreal). x < y ==> x ~= y";
|
|
809 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
|
|
810 |
qed "hypreal_not_refl2";
|
|
811 |
|
|
812 |
Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
|
|
813 |
by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
|
|
814 |
by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
|
|
815 |
by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
|
|
816 |
by (auto_tac (claset() addSIs [exI],simpset()
|
|
817 |
addsimps [hypreal_less_def]));
|
|
818 |
by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
|
|
819 |
qed "hypreal_less_trans";
|
|
820 |
|
|
821 |
Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
|
|
822 |
by (dtac hypreal_less_trans 1 THEN assume_tac 1);
|
|
823 |
by (asm_full_simp_tac (simpset() addsimps
|
|
824 |
[hypreal_less_not_refl]) 1);
|
|
825 |
qed "hypreal_less_asym";
|
|
826 |
|
|
827 |
(*--------------------------------------------------------
|
|
828 |
TODO: The following theorem should have been proved
|
|
829 |
first and then used througout the proofs as it probably
|
|
830 |
makes many of them more straightforward.
|
|
831 |
-------------------------------------------------------*)
|
|
832 |
Goalw [hypreal_less_def]
|
|
833 |
"(Abs_hypreal(hyprel^^{%n. X n}) < \
|
|
834 |
\ Abs_hypreal(hyprel^^{%n. Y n})) = \
|
|
835 |
\ ({n. X n < Y n} : FreeUltrafilterNat)";
|
|
836 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
|
|
837 |
by (Ultra_tac 1);
|
|
838 |
qed "hypreal_less";
|
|
839 |
|
|
840 |
(*---------------------------------------------------------------------------------
|
|
841 |
Hyperreals as a linearly ordered field
|
|
842 |
---------------------------------------------------------------------------------*)
|
|
843 |
(*** sum order ***)
|
|
844 |
|
|
845 |
Goalw [hypreal_zero_def]
|
|
846 |
"[| 0hr < x; 0hr < y |] ==> 0hr < x + y";
|
|
847 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
848 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
849 |
by (auto_tac (claset(),simpset() addsimps
|
|
850 |
[hypreal_less_def,hypreal_add]));
|
|
851 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps
|
|
852 |
[hypreal_less_def,hypreal_add]));
|
|
853 |
by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
|
|
854 |
qed "hypreal_add_order";
|
|
855 |
|
|
856 |
(*** mult order ***)
|
|
857 |
|
|
858 |
Goalw [hypreal_zero_def]
|
|
859 |
"[| 0hr < x; 0hr < y |] ==> 0hr < x * y";
|
|
860 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
861 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
862 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps
|
|
863 |
[hypreal_less_def,hypreal_mult]));
|
|
864 |
by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
|
|
865 |
qed "hypreal_mult_order";
|
|
866 |
|
|
867 |
(*---------------------------------------------------------------------------------
|
|
868 |
Trichotomy of the hyperreals
|
|
869 |
--------------------------------------------------------------------------------*)
|
|
870 |
|
|
871 |
Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
|
|
872 |
by (res_inst_tac [("x","%n. 0r")] exI 1);
|
|
873 |
by (Step_tac 1);
|
|
874 |
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
|
|
875 |
qed "lemma_hyprel_0r_mem";
|
|
876 |
|
|
877 |
Goalw [hypreal_zero_def]"0hr < x | x = 0hr | x < 0hr";
|
|
878 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
879 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
|
|
880 |
by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
|
|
881 |
by (dres_inst_tac [("x","xa")] spec 1);
|
|
882 |
by (dres_inst_tac [("x","x")] spec 1);
|
|
883 |
by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
|
|
884 |
by Auto_tac;
|
|
885 |
by (dres_inst_tac [("x","x")] spec 1);
|
|
886 |
by (dres_inst_tac [("x","xa")] spec 1);
|
|
887 |
by Auto_tac;
|
|
888 |
by (Ultra_tac 1);
|
|
889 |
by (auto_tac (claset() addIs [real_linear_less2],simpset()));
|
|
890 |
qed "hypreal_trichotomy";
|
|
891 |
|
|
892 |
val prems = Goal "[| 0hr < x ==> P; \
|
|
893 |
\ x = 0hr ==> P; \
|
|
894 |
\ x < 0hr ==> P |] ==> P";
|
|
895 |
by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
|
|
896 |
by (REPEAT (eresolve_tac (disjE::prems) 1));
|
|
897 |
qed "hypreal_trichotomyE";
|
|
898 |
|
|
899 |
(*----------------------------------------------------------------------------
|
|
900 |
More properties of <
|
|
901 |
----------------------------------------------------------------------------*)
|
|
902 |
Goal "!!(A::hypreal). A < B ==> A + C < B + C";
|
|
903 |
by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
|
|
904 |
by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
|
|
905 |
by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
|
|
906 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps
|
|
907 |
[hypreal_less_def,hypreal_add]));
|
|
908 |
by (Ultra_tac 1);
|
|
909 |
qed "hypreal_add_less_mono1";
|
|
910 |
|
|
911 |
Goal "!!(A::hypreal). A < B ==> C + A < C + B";
|
|
912 |
by (auto_tac (claset() addIs [hypreal_add_less_mono1],
|
|
913 |
simpset() addsimps [hypreal_add_commute]));
|
|
914 |
qed "hypreal_add_less_mono2";
|
|
915 |
|
|
916 |
Goal "((x::hypreal) < y) = (0hr < y + -x)";
|
|
917 |
by (Step_tac 1);
|
|
918 |
by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
|
|
919 |
by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
|
|
920 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
921 |
qed "hypreal_less_minus_iff";
|
|
922 |
|
|
923 |
Goal "((x::hypreal) < y) = (x + -y< 0hr)";
|
|
924 |
by (Step_tac 1);
|
|
925 |
by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
|
|
926 |
by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
|
|
927 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
928 |
qed "hypreal_less_minus_iff2";
|
|
929 |
|
|
930 |
Goal "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
|
|
931 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
|
|
932 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
|
|
933 |
by (dtac hypreal_add_order 1 THEN assume_tac 1);
|
|
934 |
by (thin_tac "0hr < y2 + - z2" 1);
|
|
935 |
by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
|
|
936 |
by (auto_tac (claset(),simpset() addsimps
|
|
937 |
[hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
|
|
938 |
qed "hypreal_add_less_mono";
|
|
939 |
|
|
940 |
Goal "((x::hypreal) = y) = (0hr = x + - y)";
|
|
941 |
by Auto_tac;
|
|
942 |
by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
|
|
943 |
by Auto_tac;
|
|
944 |
qed "hypreal_eq_minus_iff";
|
|
945 |
|
|
946 |
Goal "((x::hypreal) = y) = (0hr = y + - x)";
|
|
947 |
by Auto_tac;
|
|
948 |
by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
|
|
949 |
by Auto_tac;
|
|
950 |
qed "hypreal_eq_minus_iff2";
|
|
951 |
|
|
952 |
Goal "(x = y + z) = (x + -z = (y::hypreal))";
|
|
953 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
954 |
qed "hypreal_eq_minus_iff3";
|
|
955 |
|
|
956 |
Goal "(x = z + y) = (x + -z = (y::hypreal))";
|
|
957 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
|
|
958 |
qed "hypreal_eq_minus_iff4";
|
|
959 |
|
|
960 |
Goal "(x ~= a) = (x + -a ~= 0hr)";
|
|
961 |
by (auto_tac (claset() addDs [sym RS
|
|
962 |
(hypreal_eq_minus_iff RS iffD2)],simpset()));
|
|
963 |
qed "hypreal_not_eq_minus_iff";
|
|
964 |
|
|
965 |
(*** linearity ***)
|
|
966 |
Goal "(x::hypreal) < y | x = y | y < x";
|
|
967 |
by (rtac (hypreal_eq_minus_iff2 RS ssubst) 1);
|
|
968 |
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
|
|
969 |
by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
|
|
970 |
by (rtac hypreal_trichotomyE 1);
|
|
971 |
by Auto_tac;
|
|
972 |
qed "hypreal_linear";
|
|
973 |
|
|
974 |
Goal "!!(x::hypreal). [| x < y ==> P; x = y ==> P; \
|
|
975 |
\ y < x ==> P |] ==> P";
|
|
976 |
by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
|
|
977 |
by Auto_tac;
|
|
978 |
qed "hypreal_linear_less2";
|
|
979 |
|
|
980 |
(*------------------------------------------------------------------------------
|
|
981 |
Properties of <=
|
|
982 |
------------------------------------------------------------------------------*)
|
|
983 |
(*------ hypreal le iff reals le a.e ------*)
|
|
984 |
|
|
985 |
Goalw [hypreal_le_def,real_le_def]
|
|
986 |
"(Abs_hypreal(hyprel^^{%n. X n}) <= \
|
|
987 |
\ Abs_hypreal(hyprel^^{%n. Y n})) = \
|
|
988 |
\ ({n. X n <= Y n} : FreeUltrafilterNat)";
|
|
989 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
|
|
990 |
by (ALLGOALS(Ultra_tac));
|
|
991 |
qed "hypreal_le";
|
|
992 |
|
|
993 |
(*---------------------------------------------------------*)
|
|
994 |
(*---------------------------------------------------------*)
|
|
995 |
Goalw [hypreal_le_def]
|
|
996 |
"~(w < z) ==> z <= (w::hypreal)";
|
|
997 |
by (assume_tac 1);
|
|
998 |
qed "hypreal_leI";
|
|
999 |
|
|
1000 |
Goalw [hypreal_le_def]
|
|
1001 |
"z<=w ==> ~(w<(z::hypreal))";
|
|
1002 |
by (assume_tac 1);
|
|
1003 |
qed "hypreal_leD";
|
|
1004 |
|
|
1005 |
val hypreal_leE = make_elim hypreal_leD;
|
|
1006 |
|
|
1007 |
Goal "(~(w < z)) = (z <= (w::hypreal))";
|
|
1008 |
by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
|
|
1009 |
qed "hypreal_less_le_iff";
|
|
1010 |
|
|
1011 |
Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
|
|
1012 |
by (Fast_tac 1);
|
|
1013 |
qed "not_hypreal_leE";
|
|
1014 |
|
|
1015 |
Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)";
|
|
1016 |
by (fast_tac (claset() addEs [hypreal_less_asym]) 1);
|
|
1017 |
qed "hypreal_less_imp_le";
|
|
1018 |
|
|
1019 |
Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
|
|
1020 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
1021 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
|
|
1022 |
qed "hypreal_le_imp_less_or_eq";
|
|
1023 |
|
|
1024 |
Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
|
|
1025 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
1026 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
|
|
1027 |
qed "hypreal_less_or_eq_imp_le";
|
|
1028 |
|
|
1029 |
Goal "(x <= (y::hypreal)) = (x < y | x=y)";
|
|
1030 |
by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
|
|
1031 |
qed "hypreal_le_eq_less_or_eq";
|
|
1032 |
|
|
1033 |
Goal "w <= (w::hypreal)";
|
|
1034 |
by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
|
|
1035 |
qed "hypreal_le_refl";
|
|
1036 |
Addsimps [hypreal_le_refl];
|
|
1037 |
|
|
1038 |
Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
|
|
1039 |
by (dtac hypreal_le_imp_less_or_eq 1);
|
|
1040 |
by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
|
|
1041 |
qed "hypreal_le_less_trans";
|
|
1042 |
|
|
1043 |
Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k";
|
|
1044 |
by (dtac hypreal_le_imp_less_or_eq 1);
|
|
1045 |
by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
|
|
1046 |
qed "hypreal_less_le_trans";
|
|
1047 |
|
|
1048 |
Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
|
|
1049 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
|
|
1050 |
rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]);
|
|
1051 |
qed "hypreal_le_trans";
|
|
1052 |
|
|
1053 |
Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
|
|
1054 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
|
|
1055 |
fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
|
|
1056 |
qed "hypreal_le_anti_sym";
|
|
1057 |
|
|
1058 |
Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y";
|
|
1059 |
by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
|
|
1060 |
addIs [hypreal_add_order],simpset()));
|
|
1061 |
qed "hypreal_add_order_le";
|
|
1062 |
|
|
1063 |
(*------------------------------------------------------------------------
|
|
1064 |
------------------------------------------------------------------------*)
|
|
1065 |
|
|
1066 |
Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
|
|
1067 |
by (rtac not_hypreal_leE 1);
|
|
1068 |
by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
|
|
1069 |
qed "not_less_not_eq_hypreal_less";
|
|
1070 |
|
|
1071 |
Goal "(0hr < -R) = (R < 0hr)";
|
|
1072 |
by (Step_tac 1);
|
|
1073 |
by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
|
|
1074 |
by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
|
|
1075 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
1076 |
qed "hypreal_minus_zero_less_iff";
|
|
1077 |
|
|
1078 |
Goal "(-R < 0hr) = (0hr < R)";
|
|
1079 |
by (Step_tac 1);
|
|
1080 |
by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
|
|
1081 |
by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
|
|
1082 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
1083 |
qed "hypreal_minus_zero_less_iff2";
|
|
1084 |
|
|
1085 |
Goal "((x::hypreal) < y) = (-y < -x)";
|
|
1086 |
by (rtac (hypreal_less_minus_iff RS ssubst) 1);
|
|
1087 |
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
|
|
1088 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
1089 |
qed "hypreal_less_swap_iff";
|
|
1090 |
|
|
1091 |
Goal "(0hr < x) = (-x < x)";
|
|
1092 |
by (Step_tac 1);
|
|
1093 |
by (rtac ccontr 2 THEN forward_tac
|
|
1094 |
[hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
|
|
1095 |
by (Step_tac 2);
|
|
1096 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
|
|
1097 |
by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
|
|
1098 |
by (Auto_tac );
|
|
1099 |
by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1);
|
|
1100 |
by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
|
|
1101 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
1102 |
qed "hypreal_gt_zero_iff";
|
|
1103 |
|
|
1104 |
Goal "(x < 0hr) = (x < -x)";
|
|
1105 |
by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
|
|
1106 |
by (rtac (hypreal_gt_zero_iff RS ssubst) 1);
|
|
1107 |
by (Full_simp_tac 1);
|
|
1108 |
qed "hypreal_lt_zero_iff";
|
|
1109 |
|
|
1110 |
Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)";
|
|
1111 |
by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
|
|
1112 |
qed "hypreal_ge_zero_iff";
|
|
1113 |
|
|
1114 |
Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)";
|
|
1115 |
by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
|
|
1116 |
qed "hypreal_le_zero_iff";
|
|
1117 |
|
|
1118 |
Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y";
|
|
1119 |
by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
|
|
1120 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
|
|
1121 |
by (Asm_full_simp_tac 1);
|
|
1122 |
qed "hypreal_mult_less_zero1";
|
|
1123 |
|
|
1124 |
Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y";
|
|
1125 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
|
|
1126 |
by (auto_tac (claset() addIs [hypreal_mult_order,
|
|
1127 |
hypreal_less_imp_le],simpset()));
|
|
1128 |
qed "hypreal_le_mult_order";
|
|
1129 |
|
|
1130 |
Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y";
|
|
1131 |
by (rtac hypreal_less_or_eq_imp_le 1);
|
|
1132 |
by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
|
|
1133 |
by Auto_tac;
|
|
1134 |
by (dtac hypreal_le_imp_less_or_eq 1);
|
|
1135 |
by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
|
|
1136 |
qed "real_mult_le_zero1";
|
|
1137 |
|
|
1138 |
Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr";
|
|
1139 |
by (rtac hypreal_less_or_eq_imp_le 1);
|
|
1140 |
by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
|
|
1141 |
by Auto_tac;
|
|
1142 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
|
|
1143 |
by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
|
|
1144 |
by (blast_tac (claset() addDs [hypreal_mult_order]
|
|
1145 |
addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
|
|
1146 |
qed "hypreal_mult_le_zero";
|
|
1147 |
|
|
1148 |
Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr";
|
|
1149 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
|
|
1150 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
|
|
1151 |
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
|
|
1152 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1);
|
|
1153 |
qed "hypreal_mult_less_zero";
|
|
1154 |
|
|
1155 |
Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
|
|
1156 |
by (res_inst_tac [("x","%n. 0r")] exI 1);
|
|
1157 |
by (res_inst_tac [("x","%n. 1r")] exI 1);
|
|
1158 |
by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
|
|
1159 |
FreeUltrafilterNat_Nat_set]));
|
|
1160 |
qed "hypreal_zero_less_one";
|
|
1161 |
|
|
1162 |
Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y";
|
|
1163 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
|
|
1164 |
by (auto_tac (claset() addIs [hypreal_add_order,
|
|
1165 |
hypreal_less_imp_le],simpset()));
|
|
1166 |
qed "hypreal_le_add_order";
|
|
1167 |
|
|
1168 |
Goal "!!(q1::hypreal). q1 <= q2 ==> x + q1 <= x + q2";
|
|
1169 |
by (dtac hypreal_le_imp_less_or_eq 1);
|
|
1170 |
by (Step_tac 1);
|
|
1171 |
by (auto_tac (claset() addSIs [hypreal_le_refl,
|
|
1172 |
hypreal_less_imp_le,hypreal_add_less_mono1],
|
|
1173 |
simpset() addsimps [hypreal_add_commute]));
|
|
1174 |
qed "hypreal_add_left_le_mono1";
|
|
1175 |
|
|
1176 |
Goal "!!(q1::hypreal). q1 <= q2 ==> q1 + x <= q2 + x";
|
|
1177 |
by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
|
|
1178 |
simpset() addsimps [hypreal_add_commute]));
|
|
1179 |
qed "hypreal_add_le_mono1";
|
|
1180 |
|
|
1181 |
Goal "!!k l::hypreal. [|i<=j; k<=l |] ==> i + k <= j + l";
|
|
1182 |
by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
|
|
1183 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
1184 |
(*j moves to the end because it is free while k, l are bound*)
|
|
1185 |
by (etac hypreal_add_le_mono1 1);
|
|
1186 |
qed "hypreal_add_le_mono";
|
|
1187 |
|
|
1188 |
Goal "!!k l::hypreal. [|i<j; k<=l |] ==> i + k < j + l";
|
|
1189 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq]
|
|
1190 |
addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
|
|
1191 |
qed "hypreal_add_less_le_mono";
|
|
1192 |
|
|
1193 |
Goal "!!k l::hypreal. [|i<=j; k<l |] ==> i + k < j + l";
|
|
1194 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq]
|
|
1195 |
addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
|
|
1196 |
qed "hypreal_add_le_less_mono";
|
|
1197 |
|
|
1198 |
Goal "(0hr*x<r)=(0hr<r)";
|
|
1199 |
by (Simp_tac 1);
|
|
1200 |
qed "hypreal_mult_0_less";
|
|
1201 |
|
|
1202 |
Goal "[| 0hr < z; x < y |] ==> x*z < y*z";
|
|
1203 |
by (rotate_tac 1 1);
|
|
1204 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
|
|
1205 |
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
|
|
1206 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
|
|
1207 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
|
|
1208 |
hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1);
|
|
1209 |
qed "hypreal_mult_less_mono1";
|
|
1210 |
|
|
1211 |
Goal "[| 0hr<z; x<y |] ==> z*x<z*y";
|
|
1212 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
|
|
1213 |
qed "hypreal_mult_less_mono2";
|
|
1214 |
|
|
1215 |
Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z";
|
|
1216 |
by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
|
|
1217 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
|
|
1218 |
qed "hypreal_mult_le_less_mono1";
|
|
1219 |
|
|
1220 |
Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y";
|
|
1221 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
|
|
1222 |
hypreal_mult_le_less_mono1]) 1);
|
|
1223 |
qed "hypreal_mult_le_less_mono2";
|
|
1224 |
|
|
1225 |
Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y";
|
|
1226 |
by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
|
|
1227 |
by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
|
|
1228 |
qed "hypreal_mult_le_le_mono1";
|
|
1229 |
|
|
1230 |
val prem1::prem2::prem3::rest = goal thy
|
|
1231 |
"[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s";
|
|
1232 |
by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
|
|
1233 |
qed "hypreal_mult_less_trans";
|
|
1234 |
|
|
1235 |
Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s";
|
|
1236 |
by (dtac hypreal_le_imp_less_or_eq 1);
|
|
1237 |
by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
|
|
1238 |
qed "hypreal_mult_le_less_trans";
|
|
1239 |
|
|
1240 |
Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s";
|
|
1241 |
by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
|
|
1242 |
by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
|
|
1243 |
qed "hypreal_mult_le_le_trans";
|
|
1244 |
|
|
1245 |
Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \
|
|
1246 |
\ ==> r1 * x < r2 * y";
|
|
1247 |
by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
|
|
1248 |
by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2);
|
|
1249 |
by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
|
|
1250 |
by Auto_tac;
|
|
1251 |
by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
|
|
1252 |
qed "hypreal_mult_less_mono";
|
|
1253 |
|
|
1254 |
Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \
|
|
1255 |
\ ==> 0hr < r2 * y";
|
|
1256 |
by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1);
|
|
1257 |
by (assume_tac 1);
|
|
1258 |
by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
|
|
1259 |
qed "hypreal_mult_order_trans";
|
|
1260 |
|
|
1261 |
Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \
|
|
1262 |
\ ==> r1 * x <= r2 * y";
|
|
1263 |
by (rtac hypreal_less_or_eq_imp_le 1);
|
|
1264 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
|
|
1265 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono,
|
|
1266 |
hypreal_mult_less_mono1,hypreal_mult_less_mono2,
|
|
1267 |
hypreal_mult_order_trans,hypreal_mult_order],simpset()));
|
|
1268 |
qed "hypreal_mult_le_mono";
|
|
1269 |
|
|
1270 |
(*----------------------------------------------------------
|
|
1271 |
hypreal_of_real preserves field and order properties
|
|
1272 |
-----------------------------------------------------------*)
|
|
1273 |
Goalw [hypreal_of_real_def]
|
|
1274 |
"hypreal_of_real ((z1::real) + z2) = \
|
|
1275 |
\ hypreal_of_real z1 + hypreal_of_real z2";
|
|
1276 |
by (asm_simp_tac (simpset() addsimps [hypreal_add,
|
|
1277 |
hypreal_add_mult_distrib]) 1);
|
|
1278 |
qed "hypreal_of_real_add";
|
|
1279 |
|
|
1280 |
Goalw [hypreal_of_real_def]
|
|
1281 |
"hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2";
|
|
1282 |
by (full_simp_tac (simpset() addsimps [hypreal_mult,
|
|
1283 |
hypreal_add_mult_distrib2]) 1);
|
|
1284 |
qed "hypreal_of_real_mult";
|
|
1285 |
|
|
1286 |
Goalw [hypreal_less_def,hypreal_of_real_def]
|
|
1287 |
"(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)";
|
|
1288 |
by Auto_tac;
|
|
1289 |
by (res_inst_tac [("x","%n. z1")] exI 1);
|
|
1290 |
by (Step_tac 1);
|
|
1291 |
by (res_inst_tac [("x","%n. z2")] exI 2);
|
|
1292 |
by Auto_tac;
|
|
1293 |
by (rtac FreeUltrafilterNat_P 1);
|
|
1294 |
by (Ultra_tac 1);
|
|
1295 |
qed "hypreal_of_real_less_iff";
|
|
1296 |
|
|
1297 |
Addsimps [hypreal_of_real_less_iff RS sym];
|
|
1298 |
|
|
1299 |
Goalw [hypreal_le_def,real_le_def]
|
|
1300 |
"(z1 <= z2) = (hypreal_of_real z1 <= hypreal_of_real z2)";
|
|
1301 |
by Auto_tac;
|
|
1302 |
qed "hypreal_of_real_le_iff";
|
|
1303 |
|
|
1304 |
Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r";
|
|
1305 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
|
|
1306 |
qed "hypreal_of_real_minus";
|
|
1307 |
|
|
1308 |
Goal "0hr < x ==> 0hr < hrinv x";
|
|
1309 |
by (EVERY1[rtac ccontr, dtac hypreal_leI]);
|
|
1310 |
by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
|
|
1311 |
by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
|
|
1312 |
by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
|
|
1313 |
by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]);
|
|
1314 |
by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
|
|
1315 |
by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
|
|
1316 |
simpset() addsimps [hypreal_minus_mult_eq1 RS sym,
|
|
1317 |
hypreal_minus_zero_less_iff]));
|
|
1318 |
qed "hypreal_hrinv_gt_zero";
|
|
1319 |
|
|
1320 |
Goal "x < 0hr ==> hrinv x < 0hr";
|
|
1321 |
by (forward_tac [hypreal_not_refl2] 1);
|
|
1322 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
|
|
1323 |
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
|
|
1324 |
by (dtac (hypreal_minus_hrinv RS sym) 1);
|
|
1325 |
by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
|
|
1326 |
simpset()));
|
|
1327 |
qed "hypreal_hrinv_less_zero";
|
|
1328 |
|
|
1329 |
Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real 1r = 1hr";
|
|
1330 |
by (Step_tac 1);
|
|
1331 |
qed "hypreal_of_real_one";
|
|
1332 |
|
|
1333 |
Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real 0r = 0hr";
|
|
1334 |
by (Step_tac 1);
|
|
1335 |
qed "hypreal_of_real_zero";
|
|
1336 |
|
|
1337 |
Goal "(hypreal_of_real r = 0hr) = (r = 0r)";
|
|
1338 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
|
|
1339 |
simpset() addsimps [hypreal_of_real_def,
|
|
1340 |
hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
|
|
1341 |
qed "hypreal_of_real_zero_iff";
|
|
1342 |
|
|
1343 |
Goal "(hypreal_of_real r ~= 0hr) = (r ~= 0r)";
|
|
1344 |
by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
|
|
1345 |
qed "hypreal_of_real_not_zero_iff";
|
|
1346 |
|
|
1347 |
Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
|
|
1348 |
\ hypreal_of_real (rinv r)";
|
|
1349 |
by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
1350 |
by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
|
|
1351 |
by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
|
|
1352 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
|
|
1353 |
qed "hypreal_of_real_hrinv";
|
|
1354 |
|
|
1355 |
Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \
|
|
1356 |
\ hypreal_of_real (rinv r)";
|
|
1357 |
by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
|
|
1358 |
qed "hypreal_of_real_hrinv2";
|
|
1359 |
|
|
1360 |
Goal "x+x=x*(1hr+1hr)";
|
|
1361 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
|
|
1362 |
qed "hypreal_add_self";
|
|
1363 |
|
|
1364 |
Goal "1hr < 1hr + 1hr";
|
|
1365 |
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
|
|
1366 |
by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
|
|
1367 |
hypreal_add_assoc]) 1);
|
|
1368 |
qed "hypreal_one_less_two";
|
|
1369 |
|
|
1370 |
Goal "0hr < 1hr + 1hr";
|
|
1371 |
by (rtac ([hypreal_zero_less_one,
|
|
1372 |
hypreal_one_less_two] MRS hypreal_less_trans) 1);
|
|
1373 |
qed "hypreal_zero_less_two";
|
|
1374 |
|
|
1375 |
Goal "1hr + 1hr ~= 0hr";
|
|
1376 |
by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
|
|
1377 |
qed "hypreal_two_not_zero";
|
|
1378 |
Addsimps [hypreal_two_not_zero];
|
|
1379 |
|
|
1380 |
Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
|
|
1381 |
by (rtac (hypreal_add_self RS ssubst) 1);
|
|
1382 |
by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
|
|
1383 |
qed "hypreal_sum_of_halves";
|
|
1384 |
|
|
1385 |
Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)";
|
|
1386 |
by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1);
|
|
1387 |
qed "lemma_chain";
|
|
1388 |
|
|
1389 |
Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)";
|
|
1390 |
by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero
|
|
1391 |
RS hypreal_mult_less_mono1) 1);
|
|
1392 |
by Auto_tac;
|
|
1393 |
qed "hypreal_half_gt_zero";
|
|
1394 |
|
|
1395 |
(* TODO: remove redundant 0hr < x *)
|
|
1396 |
Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
|
|
1397 |
by (forward_tac [hypreal_hrinv_gt_zero] 1);
|
|
1398 |
by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
|
|
1399 |
by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
|
|
1400 |
by (assume_tac 1);
|
|
1401 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS
|
|
1402 |
not_sym RS hypreal_mult_hrinv]) 1);
|
|
1403 |
by (forward_tac [hypreal_hrinv_gt_zero] 1);
|
|
1404 |
by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
|
|
1405 |
by (assume_tac 1);
|
|
1406 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS
|
|
1407 |
not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
|
|
1408 |
qed "hypreal_hrinv_less_swap";
|
|
1409 |
|
|
1410 |
Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)";
|
|
1411 |
by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
|
|
1412 |
by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
|
|
1413 |
by (etac (hypreal_not_refl2 RS not_sym) 1);
|
|
1414 |
by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
|
|
1415 |
by (etac (hypreal_not_refl2 RS not_sym) 1);
|
|
1416 |
by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
|
|
1417 |
simpset() addsimps [hypreal_hrinv_gt_zero]));
|
|
1418 |
qed "hypreal_hrinv_less_iff";
|
|
1419 |
|
|
1420 |
Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
|
|
1421 |
by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
|
|
1422 |
hypreal_hrinv_gt_zero]) 1);
|
|
1423 |
qed "hypreal_mult_hrinv_less_mono1";
|
|
1424 |
|
|
1425 |
Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
|
|
1426 |
by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
|
|
1427 |
hypreal_hrinv_gt_zero]) 1);
|
|
1428 |
qed "hypreal_mult_hrinv_less_mono2";
|
|
1429 |
|
|
1430 |
Goal "[| 0hr < z; x*z < y*z |] ==> x < y";
|
|
1431 |
by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
|
|
1432 |
by (dtac (hypreal_not_refl2 RS not_sym) 2);
|
|
1433 |
by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
|
|
1434 |
simpset() addsimps hypreal_mult_ac));
|
|
1435 |
qed "hypreal_less_mult_right_cancel";
|
|
1436 |
|
|
1437 |
Goal "[| 0hr < z; z*x < z*y |] ==> x < y";
|
|
1438 |
by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
|
|
1439 |
simpset() addsimps [hypreal_mult_commute]));
|
|
1440 |
qed "hypreal_less_mult_left_cancel";
|
|
1441 |
|
|
1442 |
Goal "[| 0hr < r; 0hr < ra; \
|
|
1443 |
\ r < x; ra < y |] \
|
|
1444 |
\ ==> r*ra < x*y";
|
|
1445 |
by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
|
|
1446 |
by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
|
|
1447 |
by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
|
|
1448 |
by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
|
|
1449 |
qed "hypreal_mult_less_gt_zero";
|
|
1450 |
|
|
1451 |
Goal "[| 0hr < r; 0hr < ra; \
|
|
1452 |
\ r <= x; ra <= y |] \
|
|
1453 |
\ ==> r*ra <= x*y";
|
|
1454 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
|
|
1455 |
by (rtac hypreal_less_or_eq_imp_le 1);
|
|
1456 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
|
|
1457 |
hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
|
|
1458 |
simpset()));
|
|
1459 |
qed "hypreal_mult_le_ge_zero";
|
|
1460 |
|
|
1461 |
Goal "? (x::hypreal). x < y";
|
|
1462 |
by (rtac (hypreal_add_zero_right RS subst) 1);
|
|
1463 |
by (res_inst_tac [("x","y + -1hr")] exI 1);
|
|
1464 |
by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
|
|
1465 |
simpset() addsimps [hypreal_minus_zero_less_iff2,
|
|
1466 |
hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
|
|
1467 |
qed "hypreal_less_Ex";
|
|
1468 |
|
|
1469 |
Goal "!!(A::hypreal). A + C < B + C ==> A < B";
|
|
1470 |
by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
|
|
1471 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
|
|
1472 |
qed "hypreal_less_add_right_cancel";
|
|
1473 |
|
|
1474 |
Goal "!!(A::hypreal). C + A < C + B ==> A < B";
|
|
1475 |
by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
|
|
1476 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
1477 |
qed "hypreal_less_add_left_cancel";
|
|
1478 |
|
|
1479 |
Goal "0hr <= x*x";
|
|
1480 |
by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1);
|
|
1481 |
by (auto_tac (claset() addIs [hypreal_mult_order,
|
|
1482 |
hypreal_mult_less_zero1,hypreal_less_imp_le],
|
|
1483 |
simpset()));
|
|
1484 |
qed "hypreal_le_square";
|
|
1485 |
Addsimps [hypreal_le_square];
|
|
1486 |
|
|
1487 |
Goalw [hypreal_le_def] "- (x*x) <= 0hr";
|
|
1488 |
by (auto_tac (claset() addSDs [(hypreal_le_square RS
|
|
1489 |
hypreal_le_less_trans)],simpset() addsimps
|
|
1490 |
[hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
|
|
1491 |
qed "hypreal_less_minus_square";
|
|
1492 |
Addsimps [hypreal_less_minus_square];
|
|
1493 |
|
|
1494 |
Goal "[|x ~= 0hr; y ~= 0hr |] ==> \
|
|
1495 |
\ hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
|
|
1496 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
|
|
1497 |
hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
|
|
1498 |
by (rtac (hypreal_mult_assoc RS ssubst) 1);
|
|
1499 |
by (rtac (hypreal_mult_left_commute RS subst) 1);
|
|
1500 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
1501 |
qed "hypreal_hrinv_add";
|
|
1502 |
|
|
1503 |
Goal "x = -x ==> x = 0hr";
|
|
1504 |
by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
|
|
1505 |
by (Asm_full_simp_tac 1);
|
|
1506 |
by (dtac (hypreal_add_self RS subst) 1);
|
|
1507 |
by (rtac ccontr 1);
|
|
1508 |
by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
|
|
1509 |
(2,hypreal_mult_not_0)]) 1);
|
|
1510 |
qed "hypreal_self_eq_minus_self_zero";
|
|
1511 |
|
|
1512 |
Goal "(x + x = 0hr) = (x = 0hr)";
|
|
1513 |
by Auto_tac;
|
|
1514 |
by (dtac (hypreal_add_self RS subst) 1);
|
|
1515 |
by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
|
|
1516 |
by Auto_tac;
|
|
1517 |
qed "hypreal_add_self_zero_cancel";
|
|
1518 |
Addsimps [hypreal_add_self_zero_cancel];
|
|
1519 |
|
|
1520 |
Goal "(x + x + y = y) = (x = 0hr)";
|
|
1521 |
by Auto_tac;
|
|
1522 |
by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
|
|
1523 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
1524 |
qed "hypreal_add_self_zero_cancel2";
|
|
1525 |
Addsimps [hypreal_add_self_zero_cancel2];
|
|
1526 |
|
|
1527 |
Goal "(x + (x + y) = y) = (x = 0hr)";
|
|
1528 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
1529 |
qed "hypreal_add_self_zero_cancel2a";
|
|
1530 |
Addsimps [hypreal_add_self_zero_cancel2a];
|
|
1531 |
|
|
1532 |
Goal "(b = -a) = (-b = (a::hypreal))";
|
|
1533 |
by Auto_tac;
|
|
1534 |
qed "hypreal_minus_eq_swap";
|
|
1535 |
|
|
1536 |
Goal "(-b = -a) = (b = (a::hypreal))";
|
|
1537 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1538 |
[hypreal_minus_eq_swap]) 1);
|
|
1539 |
qed "hypreal_minus_eq_cancel";
|
|
1540 |
Addsimps [hypreal_minus_eq_cancel];
|
|
1541 |
|
|
1542 |
Goal "x < x + 1hr";
|
|
1543 |
by (cut_inst_tac [("C","x")]
|
|
1544 |
(hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
|
|
1545 |
by (Asm_full_simp_tac 1);
|
|
1546 |
qed "hypreal_less_self_add_one";
|
|
1547 |
Addsimps [hypreal_less_self_add_one];
|
|
1548 |
|
|
1549 |
Goal "((x::hypreal) + x = y + y) = (x = y)";
|
|
1550 |
by (auto_tac (claset() addIs [hypreal_two_not_zero RS
|
|
1551 |
hypreal_mult_left_cancel RS iffD1],simpset() addsimps
|
|
1552 |
[hypreal_add_mult_distrib]));
|
|
1553 |
qed "hypreal_add_self_cancel";
|
|
1554 |
Addsimps [hypreal_add_self_cancel];
|
|
1555 |
|
|
1556 |
Goal "(y = x + - y + x) = (y = (x::hypreal))";
|
|
1557 |
by Auto_tac;
|
|
1558 |
by (dres_inst_tac [("x1","y")]
|
|
1559 |
(hypreal_add_right_cancel RS iffD2) 1);
|
|
1560 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
|
|
1561 |
qed "hypreal_add_self_minus_cancel";
|
|
1562 |
Addsimps [hypreal_add_self_minus_cancel];
|
|
1563 |
|
|
1564 |
Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
|
|
1565 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1566 |
[hypreal_add_assoc RS sym])1);
|
|
1567 |
qed "hypreal_add_self_minus_cancel2";
|
|
1568 |
Addsimps [hypreal_add_self_minus_cancel2];
|
|
1569 |
|
|
1570 |
Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
|
|
1571 |
by Auto_tac;
|
|
1572 |
by (dres_inst_tac [("x1","z")]
|
|
1573 |
(hypreal_add_right_cancel RS iffD2) 1);
|
|
1574 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1575 |
[hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
|
|
1576 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1577 |
[hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
|
|
1578 |
qed "hypreal_add_self_minus_cancel3";
|
|
1579 |
Addsimps [hypreal_add_self_minus_cancel3];
|
|
1580 |
|
|
1581 |
(* check why this does not work without 2nd substiution anymore! *)
|
|
1582 |
Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
|
|
1583 |
by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
|
|
1584 |
by (dtac (hypreal_add_self RS subst) 1);
|
|
1585 |
by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS
|
|
1586 |
hypreal_mult_less_mono1) 1);
|
|
1587 |
by (auto_tac (claset() addDs [hypreal_two_not_zero RS
|
|
1588 |
(hypreal_mult_hrinv RS subst)],simpset()
|
|
1589 |
addsimps [hypreal_mult_assoc]));
|
|
1590 |
qed "hypreal_less_half_sum";
|
|
1591 |
|
|
1592 |
(* check why this does not work without 2nd substiution anymore! *)
|
|
1593 |
Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
|
|
1594 |
by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
|
|
1595 |
by (dtac (hypreal_add_self RS subst) 1);
|
|
1596 |
by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS
|
|
1597 |
hypreal_mult_less_mono1) 1);
|
|
1598 |
by (auto_tac (claset() addDs [hypreal_two_not_zero RS
|
|
1599 |
(hypreal_mult_hrinv RS subst)],simpset()
|
|
1600 |
addsimps [hypreal_mult_assoc]));
|
|
1601 |
qed "hypreal_gt_half_sum";
|
|
1602 |
|
|
1603 |
Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
|
|
1604 |
by (blast_tac (claset() addSIs [hypreal_less_half_sum,
|
|
1605 |
hypreal_gt_half_sum]) 1);
|
|
1606 |
qed "hypreal_dense";
|
|
1607 |
|
|
1608 |
Goal "(x * x = 0hr) = (x = 0hr)";
|
|
1609 |
by Auto_tac;
|
|
1610 |
by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
|
|
1611 |
qed "hypreal_mult_self_eq_zero_iff";
|
|
1612 |
Addsimps [hypreal_mult_self_eq_zero_iff];
|
|
1613 |
|
|
1614 |
Goal "(0hr = x * x) = (x = 0hr)";
|
|
1615 |
by (auto_tac (claset() addDs [sym],simpset()));
|
|
1616 |
qed "hypreal_mult_self_eq_zero_iff2";
|
|
1617 |
Addsimps [hypreal_mult_self_eq_zero_iff2];
|
|
1618 |
|
|
1619 |
Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)";
|
|
1620 |
by Auto_tac;
|
|
1621 |
by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1)) 1);
|
|
1622 |
by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 2);
|
|
1623 |
by (ALLGOALS(rtac ccontr));
|
|
1624 |
by (ALLGOALS(dtac hypreal_mult_self_not_zero));
|
|
1625 |
by (cut_inst_tac [("x1","x")] (hypreal_le_square
|
|
1626 |
RS hypreal_le_imp_less_or_eq) 1);
|
|
1627 |
by (cut_inst_tac [("x1","y")] (hypreal_le_square
|
|
1628 |
RS hypreal_le_imp_less_or_eq) 2);
|
|
1629 |
by (auto_tac (claset() addDs [sym],simpset()));
|
|
1630 |
by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square
|
|
1631 |
RS hypreal_le_less_trans) 1);
|
|
1632 |
by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square
|
|
1633 |
RS hypreal_le_less_trans) 2);
|
|
1634 |
by (auto_tac (claset(),simpset() addsimps
|
|
1635 |
[hypreal_less_not_refl]));
|
|
1636 |
qed "hypreal_squares_add_zero_iff";
|
|
1637 |
Addsimps [hypreal_squares_add_zero_iff];
|
|
1638 |
|
|
1639 |
Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z";
|
|
1640 |
by (cut_inst_tac [("x1","x")] (hypreal_le_square
|
|
1641 |
RS hypreal_le_imp_less_or_eq) 1);
|
|
1642 |
by (auto_tac (claset() addSIs
|
|
1643 |
[hypreal_add_order_le],simpset()));
|
|
1644 |
qed "hypreal_sum_squares3_gt_zero";
|
|
1645 |
|
|
1646 |
Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z";
|
|
1647 |
by (dtac hypreal_sum_squares3_gt_zero 1);
|
|
1648 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
|
|
1649 |
qed "hypreal_sum_squares3_gt_zero2";
|
|
1650 |
|
|
1651 |
Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x";
|
|
1652 |
by (dtac hypreal_sum_squares3_gt_zero 1);
|
|
1653 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
|
|
1654 |
qed "hypreal_sum_squares3_gt_zero3";
|
|
1655 |
|
|
1656 |
Goal "(x*x + y*y + z*z = 0hr) = \
|
|
1657 |
\ (x = 0hr & y = 0hr & z = 0hr)";
|
|
1658 |
by Auto_tac;
|
|
1659 |
by (ALLGOALS(rtac ccontr));
|
|
1660 |
by (ALLGOALS(dtac hypreal_mult_self_not_zero));
|
|
1661 |
by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
|
|
1662 |
hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
|
|
1663 |
hypreal_sum_squares3_gt_zero2],simpset() delsimps
|
|
1664 |
[hypreal_mult_self_eq_zero_iff]));
|
|
1665 |
qed "hypreal_three_squares_add_zero_iff";
|
|
1666 |
Addsimps [hypreal_three_squares_add_zero_iff];
|
|
1667 |
|
|
1668 |
Goal "(x::hypreal)*x <= x*x + y*y";
|
|
1669 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
1670 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
1671 |
by (auto_tac (claset(),simpset() addsimps
|
|
1672 |
[hypreal_mult,hypreal_add,hypreal_le]));
|
|
1673 |
qed "hypreal_self_le_add_pos";
|
|
1674 |
Addsimps [hypreal_self_le_add_pos];
|
|
1675 |
|
|
1676 |
Goal "(x::hypreal)*x <= x*x + y*y + z*z";
|
|
1677 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
1678 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
1679 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
1680 |
by (auto_tac (claset(),simpset() addsimps
|
|
1681 |
[hypreal_mult,hypreal_add,hypreal_le,
|
|
1682 |
real_le_add_order]));
|
|
1683 |
qed "hypreal_self_le_add_pos2";
|
|
1684 |
Addsimps [hypreal_self_le_add_pos2];
|
|
1685 |
|
|
1686 |
(*---------------------------------------------------------------------------------
|
|
1687 |
Embedding of the naturals in the hyperreals
|
|
1688 |
---------------------------------------------------------------------------------*)
|
|
1689 |
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
|
|
1690 |
by (full_simp_tac (simpset() addsimps
|
|
1691 |
[pnat_one_iff RS sym,real_of_preal_def]) 1);
|
|
1692 |
by (fold_tac [real_one_def]);
|
|
1693 |
by (rtac hypreal_of_real_one 1);
|
|
1694 |
qed "hypreal_of_posnat_one";
|
|
1695 |
|
|
1696 |
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
|
|
1697 |
by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
|
|
1698 |
hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
|
|
1699 |
real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
|
|
1700 |
qed "hypreal_of_posnat_two";
|
|
1701 |
|
|
1702 |
Goalw [hypreal_of_posnat_def]
|
|
1703 |
"hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
|
|
1704 |
\ hypreal_of_posnat (n1 + n2) + 1hr";
|
|
1705 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
|
|
1706 |
hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
|
|
1707 |
preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
|
|
1708 |
qed "hypreal_of_posnat_add";
|
|
1709 |
|
|
1710 |
Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
|
|
1711 |
by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
|
|
1712 |
by (rtac (hypreal_of_posnat_add RS subst) 1);
|
|
1713 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
|
|
1714 |
qed "hypreal_of_posnat_add_one";
|
|
1715 |
|
|
1716 |
Goalw [real_of_posnat_def,hypreal_of_posnat_def]
|
|
1717 |
"hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
|
|
1718 |
by (rtac refl 1);
|
|
1719 |
qed "hypreal_of_real_of_posnat";
|
|
1720 |
|
|
1721 |
Goalw [hypreal_of_posnat_def]
|
|
1722 |
"(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
|
|
1723 |
by Auto_tac;
|
|
1724 |
qed "hypreal_of_posnat_less_iff";
|
|
1725 |
|
|
1726 |
Addsimps [hypreal_of_posnat_less_iff RS sym];
|
|
1727 |
(*---------------------------------------------------------------------------------
|
|
1728 |
Existence of infinite hyperreal number
|
|
1729 |
---------------------------------------------------------------------------------*)
|
|
1730 |
|
|
1731 |
Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
|
|
1732 |
by Auto_tac;
|
|
1733 |
qed "hypreal_omega";
|
|
1734 |
|
|
1735 |
Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
|
|
1736 |
by (rtac Rep_hypreal 1);
|
|
1737 |
qed "Rep_hypreal_omega";
|
|
1738 |
|
|
1739 |
(* existence of infinite number not corresponding to any real number *)
|
|
1740 |
(* use assumption that member FreeUltrafilterNat is not finite *)
|
|
1741 |
(* a few lemmas first *)
|
|
1742 |
|
|
1743 |
Goal "{n::nat. x = real_of_posnat n} = {} | \
|
|
1744 |
\ (? y. {n::nat. x = real_of_posnat n} = {y})";
|
|
1745 |
by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
|
|
1746 |
qed "lemma_omega_empty_singleton_disj";
|
|
1747 |
|
|
1748 |
Goal "finite {n::nat. x = real_of_posnat n}";
|
|
1749 |
by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
|
|
1750 |
by Auto_tac;
|
|
1751 |
qed "lemma_finite_omega_set";
|
|
1752 |
|
|
1753 |
Goalw [omega_def,hypreal_of_real_def]
|
|
1754 |
"~ (? x. hypreal_of_real x = whr)";
|
|
1755 |
by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set
|
|
1756 |
RS FreeUltrafilterNat_finite]));
|
|
1757 |
qed "not_ex_hypreal_of_real_eq_omega";
|
|
1758 |
|
|
1759 |
Goal "hypreal_of_real x ~= whr";
|
|
1760 |
by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
|
|
1761 |
by Auto_tac;
|
|
1762 |
qed "hypreal_of_real_not_eq_omega";
|
|
1763 |
|
|
1764 |
(* existence of infinitesimal number also not *)
|
|
1765 |
(* corresponding to any real number *)
|
|
1766 |
|
|
1767 |
Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
|
|
1768 |
\ (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
|
|
1769 |
by (Step_tac 1 THEN Step_tac 1);
|
|
1770 |
by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
|
|
1771 |
qed "lemma_epsilon_empty_singleton_disj";
|
|
1772 |
|
|
1773 |
Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
|
|
1774 |
by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
|
|
1775 |
by Auto_tac;
|
|
1776 |
qed "lemma_finite_epsilon_set";
|
|
1777 |
|
|
1778 |
Goalw [epsilon_def,hypreal_of_real_def]
|
|
1779 |
"~ (? x. hypreal_of_real x = ehr)";
|
|
1780 |
by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set
|
|
1781 |
RS FreeUltrafilterNat_finite]));
|
|
1782 |
qed "not_ex_hypreal_of_real_eq_epsilon";
|
|
1783 |
|
|
1784 |
Goal "hypreal_of_real x ~= ehr";
|
|
1785 |
by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
|
|
1786 |
by Auto_tac;
|
|
1787 |
qed "hypreal_of_real_not_eq_epsilon";
|
|
1788 |
|
|
1789 |
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
|
|
1790 |
by (auto_tac (claset(),simpset() addsimps
|
|
1791 |
[real_of_posnat_rinv_not_zero]));
|
|
1792 |
qed "hypreal_epsilon_not_zero";
|
|
1793 |
|
|
1794 |
Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
|
|
1795 |
by (Simp_tac 1);
|
|
1796 |
qed "hypreal_omega_not_zero";
|
|
1797 |
|
|
1798 |
Goal "ehr = hrinv(whr)";
|
|
1799 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1800 |
[hypreal_hrinv,omega_def,epsilon_def]
|
|
1801 |
setloop (split_tac [expand_if])) 1);
|
|
1802 |
qed "hypreal_epsilon_hrinv_omega";
|
|
1803 |
|
|
1804 |
(*----------------------------------------------------------------
|
|
1805 |
Another embedding of the naturals in the
|
|
1806 |
hyperreals (see hypreal_of_posnat)
|
|
1807 |
----------------------------------------------------------------*)
|
|
1808 |
Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr";
|
|
1809 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
|
|
1810 |
qed "hypreal_of_nat_zero";
|
|
1811 |
|
|
1812 |
Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
|
|
1813 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
|
|
1814 |
hypreal_add_assoc]) 1);
|
|
1815 |
qed "hypreal_of_nat_one";
|
|
1816 |
|
|
1817 |
Goalw [hypreal_of_nat_def]
|
|
1818 |
"hypreal_of_nat n1 + hypreal_of_nat n2 = \
|
|
1819 |
\ hypreal_of_nat (n1 + n2)";
|
|
1820 |
by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
1821 |
by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
|
|
1822 |
hypreal_add_assoc RS sym]) 1);
|
|
1823 |
by (rtac (hypreal_add_commute RS subst) 1);
|
|
1824 |
by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
|
|
1825 |
hypreal_add_assoc]) 1);
|
|
1826 |
qed "hypreal_of_nat_add";
|
|
1827 |
|
|
1828 |
Goal "hypreal_of_nat 2 = 1hr + 1hr";
|
|
1829 |
by (simp_tac (simpset() addsimps [hypreal_of_nat_one
|
|
1830 |
RS sym,hypreal_of_nat_add]) 1);
|
|
1831 |
qed "hypreal_of_nat_two";
|
|
1832 |
|
|
1833 |
Goalw [hypreal_of_nat_def]
|
|
1834 |
"(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
|
|
1835 |
by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
|
|
1836 |
by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
|
|
1837 |
by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
|
|
1838 |
qed "hypreal_of_nat_less_iff";
|
|
1839 |
Addsimps [hypreal_of_nat_less_iff RS sym];
|
|
1840 |
|
|
1841 |
(* naturals embedded in hyperreals is an hyperreal *)
|
|
1842 |
Goalw [hypreal_of_nat_def,real_of_nat_def]
|
|
1843 |
"hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
|
|
1844 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
|
|
1845 |
hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
|
|
1846 |
qed "hypreal_of_nat_iff";
|
|
1847 |
|
|
1848 |
Goal "inj hypreal_of_nat";
|
|
1849 |
by (rtac injI 1);
|
|
1850 |
by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
|
|
1851 |
simpset() addsimps [hypreal_of_nat_iff,
|
|
1852 |
real_add_right_cancel,inj_real_of_nat RS injD]));
|
|
1853 |
qed "inj_hypreal_of_nat";
|
|
1854 |
|
|
1855 |
Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
|
|
1856 |
real_of_posnat_def,hypreal_one_def,real_of_nat_def]
|
|
1857 |
"hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
|
|
1858 |
by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
|
|
1859 |
qed "hypreal_of_nat_real_of_nat";
|
|
1860 |
|
|
1861 |
|
|
1862 |
|
|
1863 |
|
|
1864 |
|
|
1865 |
|
|
1866 |
|
|
1867 |
|
|
1868 |
|
|
1869 |
|
|
1870 |
|
|
1871 |
|
|
1872 |
|
|
1873 |
|
|
1874 |
|
|
1875 |
|
|
1876 |
|
|
1877 |
|
|
1878 |
|
|
1879 |
|
|
1880 |
|
|
1881 |
|
|
1882 |
|
|
1883 |
|
|
1884 |
|
|
1885 |
|
|
1886 |
|
|
1887 |
|
|
1888 |
|
|
1889 |
|
|
1890 |
|
|
1891 |
|
|
1892 |
|
|
1893 |
|
|
1894 |
|
|
1895 |
|
|
1896 |
|
|
1897 |
|
|
1898 |
|
|
1899 |
|
|
1900 |
|
|
1901 |
|
|
1902 |
|
|
1903 |
|
|
1904 |
|
|
1905 |
|
|
1906 |
|
|
1907 |
|
|
1908 |
|
|
1909 |
|
|
1910 |
|
|
1911 |
|
|
1912 |
|
|
1913 |
|
|
1914 |
|
|
1915 |
|
|
1916 |
|
|
1917 |
|
|
1918 |
|
|
1919 |
|
|
1920 |
|
|
1921 |
|
|
1922 |
|
|
1923 |
|
|
1924 |
|
|
1925 |
|
|
1926 |
|
|
1927 |
|
|
1928 |
|
|
1929 |
|
|
1930 |
|
|
1931 |
|
|
1932 |
|
|
1933 |
|
|
1934 |
|
|
1935 |
|
|
1936 |
|
|
1937 |
|
|
1938 |
|
|
1939 |
|
|
1940 |
|
|
1941 |
|
|
1942 |
|
|
1943 |
|
|
1944 |
|
|
1945 |
|
|
1946 |
|
|
1947 |
|
|
1948 |
|
|
1949 |
|
|
1950 |
|
|
1951 |
|
|
1952 |
|
|
1953 |
|
|
1954 |
|
|
1955 |
|
|
1956 |
|
|
1957 |
|
|
1958 |
|
|
1959 |
|
|
1960 |
|
|
1961 |
|
|
1962 |
|
|
1963 |
|
|
1964 |
|
|
1965 |
|
|
1966 |
|
|
1967 |
|
|
1968 |
|
|
1969 |
|
|
1970 |
|
|
1971 |
|
|
1972 |
|
|
1973 |
|
|
1974 |
|
|
1975 |
|
|
1976 |
|
|
1977 |
|
|
1978 |
|
|
1979 |
|
|
1980 |
|
|
1981 |
|
|
1982 |
|
|
1983 |
|
|
1984 |
|
|
1985 |
|
|
1986 |
|
|
1987 |
|
|
1988 |
|
|
1989 |
|
|
1990 |
|
|
1991 |
|
|
1992 |
|
|
1993 |
|
|
1994 |
|
|
1995 |
|
|
1996 |
|
|
1997 |
|
|
1998 |
|
|
1999 |
|
|
2000 |
|
|
2001 |
|
|
2002 |
|
|
2003 |
|
|
2004 |
|
|
2005 |
|
|
2006 |
|
|
2007 |
|
|
2008 |
|
|
2009 |
|
|
2010 |
|
|
2011 |
|
|
2012 |
|
|
2013 |
|
|
2014 |
|
|
2015 |
|
|
2016 |
|
|
2017 |
|
|
2018 |
|
|
2019 |
|
|
2020 |
|
|
2021 |
|
|
2022 |
|
|
2023 |
|
|
2024 |
|
|
2025 |
|
|
2026 |
|
|
2027 |
|
|
2028 |
|
|
2029 |
|
|
2030 |
|
|
2031 |
|
|
2032 |
|
|
2033 |
|
|
2034 |
|
|
2035 |
|
|
2036 |
|
|
2037 |
|
|
2038 |
|
|
2039 |
|
|
2040 |
|
|
2041 |
|
|
2042 |
|
|
2043 |
|
|
2044 |
|
|
2045 |
|
|
2046 |
|
|
2047 |
|
|
2048 |
|
|
2049 |
|
|
2050 |
|
|
2051 |
|
|
2052 |
|
|
2053 |
|
|
2054 |
|
|
2055 |
|
|
2056 |
|
|
2057 |
|
|
2058 |
|
|
2059 |
|
|
2060 |
|
|
2061 |
|
|
2062 |
|
|
2063 |
|
|
2064 |
|
|
2065 |
|
|
2066 |
|
|
2067 |
|
|
2068 |
|
|
2069 |
|
|
2070 |
|
|
2071 |
|
|
2072 |
|
|
2073 |
|
|
2074 |
|
|
2075 |
|
|
2076 |
|
|
2077 |
|
|
2078 |
|
|
2079 |
|
|
2080 |
|
|
2081 |
|
|
2082 |
|
|
2083 |
|
|
2084 |
|
|
2085 |
|
|
2086 |
|
|
2087 |
|
|
2088 |
|
|
2089 |
|
|
2090 |
|
|
2091 |
|
|
2092 |
|
|
2093 |
|
|
2094 |
|
|
2095 |
|
|
2096 |
|
|
2097 |
|
|
2098 |
|
|
2099 |
|
|
2100 |
|
|
2101 |
|
|
2102 |
|
|
2103 |
|
|
2104 |
|
|
2105 |
|
|
2106 |
|
|
2107 |
|
|
2108 |
|
|
2109 |
|
|
2110 |
|
|
2111 |
|
|
2112 |
|
|
2113 |
|
|
2114 |
|
|
2115 |
|
|
2116 |
|
|
2117 |
|
|
2118 |
|
|
2119 |
|
|
2120 |
|
|
2121 |
|
|
2122 |
|
|
2123 |
|
|
2124 |
|
|
2125 |
|
|
2126 |
|
|
2127 |
|
|
2128 |
|
|
2129 |
|
|
2130 |
|
|
2131 |
|
|
2132 |
|
|
2133 |
|
|
2134 |
|
|
2135 |
|
|
2136 |
|
|
2137 |
|
|
2138 |
|
|
2139 |
|
|
2140 |
|
|
2141 |
|
|
2142 |
|
|
2143 |
|
|
2144 |
|
|
2145 |
|
|
2146 |
|
|
2147 |
|
|
2148 |
|
|
2149 |
|
|
2150 |
|
|
2151 |
|
|
2152 |
|
|
2153 |
|
|
2154 |
|
|
2155 |
|
|
2156 |
|
|
2157 |
|
|
2158 |
|
|
2159 |
|
|
2160 |
|
|
2161 |
|
|
2162 |
|
|
2163 |
|
|
2164 |
|
|
2165 |
|
|
2166 |
|
|
2167 |
|
|
2168 |
|
|
2169 |
|
|
2170 |
|
|
2171 |
|
|
2172 |
|
|
2173 |
|
|
2174 |
|
|
2175 |
|
|
2176 |
|
|
2177 |
|
|
2178 |
|
|
2179 |
|
|
2180 |
|
|
2181 |
|
|
2182 |
|
|
2183 |
|
|
2184 |
|
|
2185 |
|
|
2186 |
|
|
2187 |
|
|
2188 |
|
|
2189 |
|
|
2190 |
|
|
2191 |
|
|
2192 |
|
|
2193 |
|
|
2194 |
|
|
2195 |
|
|
2196 |
|
|
2197 |
|
|
2198 |
|
|
2199 |
|
|
2200 |
|
|
2201 |
|
|
2202 |
|
|
2203 |
|
|
2204 |
|
|
2205 |
|
|
2206 |
|
|
2207 |
|
|
2208 |
|
|
2209 |
|
|
2210 |
|
|
2211 |
|
|
2212 |
|
|
2213 |
|
|
2214 |
|
|
2215 |
|
|
2216 |
|
|
2217 |
|
|
2218 |
|
|
2219 |
|
|
2220 |
|
|
2221 |
|
|
2222 |
|
|
2223 |
|
|
2224 |
|
|
2225 |
|
|
2226 |
|
|
2227 |
|