10751
|
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) --> (EX n. ALL 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) --> (EX 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 someI2 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 someI2 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 someI2 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 "UNIV : FreeUltrafilterNat";
|
|
111 |
by Auto_tac;
|
|
112 |
qed "FreeUltrafilterNat_Nat_set";
|
|
113 |
Addsimps [FreeUltrafilterNat_Nat_set];
|
|
114 |
|
|
115 |
Goal "{n. P(n) = P(n)} : FreeUltrafilterNat";
|
|
116 |
by (Simp_tac 1);
|
|
117 |
qed "FreeUltrafilterNat_Nat_set_refl";
|
|
118 |
AddIs [FreeUltrafilterNat_Nat_set_refl];
|
|
119 |
|
|
120 |
Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
|
|
121 |
by (rtac ccontr 1);
|
|
122 |
by (rotate_tac 1 1);
|
|
123 |
by (Asm_full_simp_tac 1);
|
|
124 |
qed "FreeUltrafilterNat_P";
|
|
125 |
|
|
126 |
Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
|
|
127 |
by (rtac ccontr 1 THEN rotate_tac 1 1);
|
|
128 |
by (Asm_full_simp_tac 1);
|
|
129 |
qed "FreeUltrafilterNat_Ex_P";
|
|
130 |
|
|
131 |
Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
|
|
132 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset()));
|
|
133 |
qed "FreeUltrafilterNat_all";
|
|
134 |
|
|
135 |
(*-------------------------------------------------------
|
|
136 |
Define and use Ultrafilter tactics
|
|
137 |
-------------------------------------------------------*)
|
|
138 |
use "fuf.ML";
|
|
139 |
|
|
140 |
(*-------------------------------------------------------
|
|
141 |
Now prove one further property of our free ultrafilter
|
|
142 |
-------------------------------------------------------*)
|
|
143 |
Goal "X Un Y: FreeUltrafilterNat \
|
|
144 |
\ ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
|
|
145 |
by Auto_tac;
|
|
146 |
by (Ultra_tac 1);
|
|
147 |
qed "FreeUltrafilterNat_Un";
|
|
148 |
|
|
149 |
(*-------------------------------------------------------
|
|
150 |
Properties of hyprel
|
|
151 |
-------------------------------------------------------*)
|
|
152 |
|
|
153 |
(** Proving that hyprel is an equivalence relation **)
|
|
154 |
(** Natural deduction for hyprel **)
|
|
155 |
|
|
156 |
Goalw [hyprel_def]
|
|
157 |
"((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)";
|
|
158 |
by (Fast_tac 1);
|
|
159 |
qed "hyprel_iff";
|
|
160 |
|
|
161 |
Goalw [hyprel_def]
|
|
162 |
"{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hyprel";
|
|
163 |
by (Fast_tac 1);
|
|
164 |
qed "hyprelI";
|
|
165 |
|
|
166 |
Goalw [hyprel_def]
|
|
167 |
"p: hyprel --> (EX X Y. \
|
|
168 |
\ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
|
|
169 |
by (Fast_tac 1);
|
|
170 |
qed "hyprelE_lemma";
|
|
171 |
|
|
172 |
val [major,minor] = goal (the_context ())
|
|
173 |
"[| p: hyprel; \
|
|
174 |
\ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
|
|
175 |
\ |] ==> Q |] ==> Q";
|
|
176 |
by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1);
|
|
177 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
|
|
178 |
qed "hyprelE";
|
|
179 |
|
|
180 |
AddSIs [hyprelI];
|
|
181 |
AddSEs [hyprelE];
|
|
182 |
|
|
183 |
Goalw [hyprel_def] "(x,x): hyprel";
|
|
184 |
by (auto_tac (claset(),
|
|
185 |
simpset() addsimps [FreeUltrafilterNat_Nat_set]));
|
|
186 |
qed "hyprel_refl";
|
|
187 |
|
|
188 |
Goal "{n. X n = Y n} = {n. Y n = X n}";
|
|
189 |
by Auto_tac;
|
|
190 |
qed "lemma_perm";
|
|
191 |
|
|
192 |
Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
|
|
193 |
by (auto_tac (claset() addIs [lemma_perm RS subst], simpset()));
|
|
194 |
qed_spec_mp "hyprel_sym";
|
|
195 |
|
|
196 |
Goalw [hyprel_def]
|
|
197 |
"(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
|
|
198 |
by Auto_tac;
|
|
199 |
by (Ultra_tac 1);
|
|
200 |
qed_spec_mp "hyprel_trans";
|
|
201 |
|
|
202 |
Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel";
|
|
203 |
by (auto_tac (claset() addSIs [hyprel_refl]
|
|
204 |
addSEs [hyprel_sym,hyprel_trans]
|
|
205 |
delrules [hyprelI,hyprelE],
|
|
206 |
simpset() addsimps [FreeUltrafilterNat_Nat_set]));
|
|
207 |
qed "equiv_hyprel";
|
|
208 |
|
10797
|
209 |
(* (hyprel ``` {x} = hyprel ``` {y}) = ((x,y) : hyprel) *)
|
10751
|
210 |
bind_thm ("equiv_hyprel_iff",
|
|
211 |
[equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
|
|
212 |
|
10797
|
213 |
Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel```{x}:hypreal";
|
10751
|
214 |
by (Blast_tac 1);
|
|
215 |
qed "hyprel_in_hypreal";
|
|
216 |
|
|
217 |
Goal "inj_on Abs_hypreal hypreal";
|
|
218 |
by (rtac inj_on_inverseI 1);
|
|
219 |
by (etac Abs_hypreal_inverse 1);
|
|
220 |
qed "inj_on_Abs_hypreal";
|
|
221 |
|
|
222 |
Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff,
|
|
223 |
hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
|
|
224 |
|
|
225 |
Addsimps [equiv_hyprel RS eq_equiv_class_iff];
|
|
226 |
bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class));
|
|
227 |
|
|
228 |
Goal "inj(Rep_hypreal)";
|
|
229 |
by (rtac inj_inverseI 1);
|
|
230 |
by (rtac Rep_hypreal_inverse 1);
|
|
231 |
qed "inj_Rep_hypreal";
|
|
232 |
|
10797
|
233 |
Goalw [hyprel_def] "x: hyprel ``` {x}";
|
10751
|
234 |
by (Step_tac 1);
|
|
235 |
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
|
|
236 |
qed "lemma_hyprel_refl";
|
|
237 |
|
|
238 |
Addsimps [lemma_hyprel_refl];
|
|
239 |
|
|
240 |
Goalw [hypreal_def] "{} ~: hypreal";
|
|
241 |
by (auto_tac (claset() addSEs [quotientE], simpset()));
|
|
242 |
qed "hypreal_empty_not_mem";
|
|
243 |
|
|
244 |
Addsimps [hypreal_empty_not_mem];
|
|
245 |
|
|
246 |
Goal "Rep_hypreal x ~= {}";
|
|
247 |
by (cut_inst_tac [("x","x")] Rep_hypreal 1);
|
|
248 |
by Auto_tac;
|
|
249 |
qed "Rep_hypreal_nonempty";
|
|
250 |
|
|
251 |
Addsimps [Rep_hypreal_nonempty];
|
|
252 |
|
|
253 |
(*------------------------------------------------------------------------
|
|
254 |
hypreal_of_real: the injection from real to hypreal
|
|
255 |
------------------------------------------------------------------------*)
|
|
256 |
|
|
257 |
Goal "inj(hypreal_of_real)";
|
|
258 |
by (rtac injI 1);
|
|
259 |
by (rewtac hypreal_of_real_def);
|
|
260 |
by (dtac (inj_on_Abs_hypreal RS inj_onD) 1);
|
|
261 |
by (REPEAT (rtac hyprel_in_hypreal 1));
|
|
262 |
by (dtac eq_equiv_class 1);
|
|
263 |
by (rtac equiv_hyprel 1);
|
|
264 |
by (Fast_tac 1);
|
|
265 |
by (rtac ccontr 1 THEN rotate_tac 1 1);
|
|
266 |
by Auto_tac;
|
|
267 |
qed "inj_hypreal_of_real";
|
|
268 |
|
|
269 |
val [prem] = goal (the_context ())
|
10797
|
270 |
"(!!x y. z = Abs_hypreal(hyprel```{x}) ==> P) ==> P";
|
10751
|
271 |
by (res_inst_tac [("x1","z")]
|
|
272 |
(rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
|
|
273 |
by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
274 |
by (res_inst_tac [("x","x")] prem 1);
|
|
275 |
by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1);
|
|
276 |
qed "eq_Abs_hypreal";
|
|
277 |
|
|
278 |
(**** hypreal_minus: additive inverse on hypreal ****)
|
|
279 |
|
|
280 |
Goalw [congruent_def]
|
10797
|
281 |
"congruent hyprel (%X. hyprel```{%n. - (X n)})";
|
10751
|
282 |
by Safe_tac;
|
|
283 |
by (ALLGOALS Ultra_tac);
|
|
284 |
qed "hypreal_minus_congruent";
|
|
285 |
|
|
286 |
Goalw [hypreal_minus_def]
|
10797
|
287 |
"- (Abs_hypreal(hyprel```{%n. X n})) = Abs_hypreal(hyprel ``` {%n. -(X n)})";
|
10751
|
288 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
289 |
by (simp_tac (simpset() addsimps
|
|
290 |
[hyprel_in_hypreal RS Abs_hypreal_inverse,
|
|
291 |
[equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
|
|
292 |
qed "hypreal_minus";
|
|
293 |
|
|
294 |
Goal "- (- z) = (z::hypreal)";
|
|
295 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
296 |
by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);
|
|
297 |
qed "hypreal_minus_minus";
|
|
298 |
|
|
299 |
Addsimps [hypreal_minus_minus];
|
|
300 |
|
|
301 |
Goal "inj(%r::hypreal. -r)";
|
|
302 |
by (rtac injI 1);
|
|
303 |
by (dres_inst_tac [("f","uminus")] arg_cong 1);
|
|
304 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
|
|
305 |
qed "inj_hypreal_minus";
|
|
306 |
|
|
307 |
Goalw [hypreal_zero_def] "-0 = (0::hypreal)";
|
|
308 |
by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
|
|
309 |
qed "hypreal_minus_zero";
|
|
310 |
Addsimps [hypreal_minus_zero];
|
|
311 |
|
|
312 |
Goal "(-x = 0) = (x = (0::hypreal))";
|
|
313 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
314 |
by (auto_tac (claset(),
|
|
315 |
simpset() addsimps [hypreal_zero_def, hypreal_minus, eq_commute] @
|
|
316 |
real_add_ac));
|
|
317 |
qed "hypreal_minus_zero_iff";
|
|
318 |
|
|
319 |
Addsimps [hypreal_minus_zero_iff];
|
|
320 |
|
|
321 |
|
|
322 |
(**** hyperreal addition: hypreal_add ****)
|
|
323 |
|
|
324 |
Goalw [congruent2_def]
|
10797
|
325 |
"congruent2 hyprel (%X Y. hyprel```{%n. X n + Y n})";
|
10751
|
326 |
by Safe_tac;
|
|
327 |
by (ALLGOALS(Ultra_tac));
|
|
328 |
qed "hypreal_add_congruent2";
|
|
329 |
|
|
330 |
Goalw [hypreal_add_def]
|
10797
|
331 |
"Abs_hypreal(hyprel```{%n. X n}) + Abs_hypreal(hyprel```{%n. Y n}) = \
|
|
332 |
\ Abs_hypreal(hyprel```{%n. X n + Y n})";
|
10751
|
333 |
by (simp_tac (simpset() addsimps
|
|
334 |
[[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
|
|
335 |
qed "hypreal_add";
|
|
336 |
|
10797
|
337 |
Goal "Abs_hypreal(hyprel```{%n. X n}) - Abs_hypreal(hyprel```{%n. Y n}) = \
|
|
338 |
\ Abs_hypreal(hyprel```{%n. X n - Y n})";
|
10751
|
339 |
by (simp_tac (simpset() addsimps
|
|
340 |
[hypreal_diff_def, hypreal_minus,hypreal_add]) 1);
|
|
341 |
qed "hypreal_diff";
|
|
342 |
|
|
343 |
Goal "(z::hypreal) + w = w + z";
|
|
344 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
345 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
346 |
by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
|
|
347 |
qed "hypreal_add_commute";
|
|
348 |
|
|
349 |
Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
|
|
350 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
351 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
352 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
|
|
353 |
by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
|
|
354 |
qed "hypreal_add_assoc";
|
|
355 |
|
|
356 |
(*For AC rewriting*)
|
|
357 |
Goal "(x::hypreal)+(y+z)=y+(x+z)";
|
|
358 |
by (rtac (hypreal_add_commute RS trans) 1);
|
|
359 |
by (rtac (hypreal_add_assoc RS trans) 1);
|
|
360 |
by (rtac (hypreal_add_commute RS arg_cong) 1);
|
|
361 |
qed "hypreal_add_left_commute";
|
|
362 |
|
|
363 |
(* hypreal addition is an AC operator *)
|
|
364 |
bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
|
|
365 |
hypreal_add_left_commute]);
|
|
366 |
|
|
367 |
Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
|
|
368 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
369 |
by (asm_full_simp_tac (simpset() addsimps
|
|
370 |
[hypreal_add]) 1);
|
|
371 |
qed "hypreal_add_zero_left";
|
|
372 |
|
|
373 |
Goal "z + (0::hypreal) = z";
|
|
374 |
by (simp_tac (simpset() addsimps
|
|
375 |
[hypreal_add_zero_left,hypreal_add_commute]) 1);
|
|
376 |
qed "hypreal_add_zero_right";
|
|
377 |
|
|
378 |
Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
|
|
379 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
380 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1);
|
|
381 |
qed "hypreal_add_minus";
|
|
382 |
|
|
383 |
Goal "-z + z = (0::hypreal)";
|
|
384 |
by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1);
|
|
385 |
qed "hypreal_add_minus_left";
|
|
386 |
|
|
387 |
Addsimps [hypreal_add_minus,hypreal_add_minus_left,
|
|
388 |
hypreal_add_zero_left,hypreal_add_zero_right];
|
|
389 |
|
|
390 |
Goal "EX y. (x::hypreal) + y = 0";
|
|
391 |
by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
|
|
392 |
qed "hypreal_minus_ex";
|
|
393 |
|
|
394 |
Goal "EX! y. (x::hypreal) + y = 0";
|
|
395 |
by (auto_tac (claset() addIs [hypreal_add_minus], simpset()));
|
|
396 |
by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
|
|
397 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
398 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
399 |
qed "hypreal_minus_ex1";
|
|
400 |
|
|
401 |
Goal "EX! y. y + (x::hypreal) = 0";
|
|
402 |
by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset()));
|
|
403 |
by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
|
|
404 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
|
|
405 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
406 |
qed "hypreal_minus_left_ex1";
|
|
407 |
|
|
408 |
Goal "x + y = (0::hypreal) ==> x = -y";
|
|
409 |
by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
|
|
410 |
by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
|
|
411 |
by (Blast_tac 1);
|
|
412 |
qed "hypreal_add_minus_eq_minus";
|
|
413 |
|
|
414 |
Goal "EX y::hypreal. x = -y";
|
|
415 |
by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
|
|
416 |
by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
|
|
417 |
by (Fast_tac 1);
|
|
418 |
qed "hypreal_as_add_inverse_ex";
|
|
419 |
|
|
420 |
Goal "-(x + (y::hypreal)) = -x + -y";
|
|
421 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
422 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
423 |
by (auto_tac (claset(),
|
|
424 |
simpset() addsimps [hypreal_minus, hypreal_add,
|
|
425 |
real_minus_add_distrib]));
|
|
426 |
qed "hypreal_minus_add_distrib";
|
|
427 |
Addsimps [hypreal_minus_add_distrib];
|
|
428 |
|
|
429 |
Goal "-(y + -(x::hypreal)) = x + -y";
|
|
430 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
431 |
qed "hypreal_minus_distrib1";
|
|
432 |
|
|
433 |
Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
|
|
434 |
by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
|
|
435 |
by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
|
|
436 |
hypreal_add_assoc]) 1);
|
|
437 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
438 |
qed "hypreal_add_minus_cancel1";
|
|
439 |
|
|
440 |
Goal "((x::hypreal) + y = x + z) = (y = z)";
|
|
441 |
by (Step_tac 1);
|
|
442 |
by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
|
|
443 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
444 |
qed "hypreal_add_left_cancel";
|
|
445 |
|
|
446 |
Goal "z + (x + (y + -z)) = x + (y::hypreal)";
|
|
447 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
448 |
qed "hypreal_add_minus_cancel2";
|
|
449 |
Addsimps [hypreal_add_minus_cancel2];
|
|
450 |
|
|
451 |
Goal "y + -(x + y) = -(x::hypreal)";
|
|
452 |
by (Full_simp_tac 1);
|
|
453 |
by (rtac (hypreal_add_left_commute RS subst) 1);
|
|
454 |
by (Full_simp_tac 1);
|
|
455 |
qed "hypreal_add_minus_cancel";
|
|
456 |
Addsimps [hypreal_add_minus_cancel];
|
|
457 |
|
|
458 |
Goal "y + -(y + x) = -(x::hypreal)";
|
|
459 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
460 |
qed "hypreal_add_minus_cancelc";
|
|
461 |
Addsimps [hypreal_add_minus_cancelc];
|
|
462 |
|
|
463 |
Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
|
|
464 |
by (full_simp_tac
|
|
465 |
(simpset() addsimps [hypreal_minus_add_distrib RS sym,
|
|
466 |
hypreal_add_left_cancel] @ hypreal_add_ac
|
|
467 |
delsimps [hypreal_minus_add_distrib]) 1);
|
|
468 |
qed "hypreal_add_minus_cancel3";
|
|
469 |
Addsimps [hypreal_add_minus_cancel3];
|
|
470 |
|
|
471 |
Goal "(y + (x::hypreal)= z + x) = (y = z)";
|
|
472 |
by (simp_tac (simpset() addsimps [hypreal_add_commute,
|
|
473 |
hypreal_add_left_cancel]) 1);
|
|
474 |
qed "hypreal_add_right_cancel";
|
|
475 |
|
|
476 |
Goal "z + (y + -z) = (y::hypreal)";
|
|
477 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
478 |
qed "hypreal_add_minus_cancel4";
|
|
479 |
Addsimps [hypreal_add_minus_cancel4];
|
|
480 |
|
|
481 |
Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
|
|
482 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
483 |
qed "hypreal_add_minus_cancel5";
|
|
484 |
Addsimps [hypreal_add_minus_cancel5];
|
|
485 |
|
|
486 |
Goal "z + ((- z) + w) = (w::hypreal)";
|
|
487 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
488 |
qed "hypreal_add_minus_cancelA";
|
|
489 |
|
|
490 |
Goal "(-z) + (z + w) = (w::hypreal)";
|
|
491 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
492 |
qed "hypreal_minus_add_cancelA";
|
|
493 |
|
|
494 |
Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
|
|
495 |
|
|
496 |
(**** hyperreal multiplication: hypreal_mult ****)
|
|
497 |
|
|
498 |
Goalw [congruent2_def]
|
10797
|
499 |
"congruent2 hyprel (%X Y. hyprel```{%n. X n * Y n})";
|
10751
|
500 |
by Safe_tac;
|
|
501 |
by (ALLGOALS(Ultra_tac));
|
|
502 |
qed "hypreal_mult_congruent2";
|
|
503 |
|
|
504 |
Goalw [hypreal_mult_def]
|
10797
|
505 |
"Abs_hypreal(hyprel```{%n. X n}) * Abs_hypreal(hyprel```{%n. Y n}) = \
|
|
506 |
\ Abs_hypreal(hyprel```{%n. X n * Y n})";
|
10751
|
507 |
by (simp_tac (simpset() addsimps
|
|
508 |
[[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
|
|
509 |
qed "hypreal_mult";
|
|
510 |
|
|
511 |
Goal "(z::hypreal) * w = w * z";
|
|
512 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
513 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
514 |
by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
|
|
515 |
qed "hypreal_mult_commute";
|
|
516 |
|
|
517 |
Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
|
|
518 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
519 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
520 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
|
|
521 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
|
|
522 |
qed "hypreal_mult_assoc";
|
|
523 |
|
|
524 |
qed_goal "hypreal_mult_left_commute" (the_context ())
|
|
525 |
"(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
|
|
526 |
(fn _ => [rtac (hypreal_mult_commute RS trans) 1,
|
|
527 |
rtac (hypreal_mult_assoc RS trans) 1,
|
|
528 |
rtac (hypreal_mult_commute RS arg_cong) 1]);
|
|
529 |
|
|
530 |
(* hypreal multiplication is an AC operator *)
|
|
531 |
bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute,
|
|
532 |
hypreal_mult_left_commute]);
|
|
533 |
|
|
534 |
Goalw [hypreal_one_def] "1hr * z = z";
|
|
535 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
536 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
|
|
537 |
qed "hypreal_mult_1";
|
|
538 |
|
|
539 |
Goal "z * 1hr = z";
|
|
540 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute,
|
|
541 |
hypreal_mult_1]) 1);
|
|
542 |
qed "hypreal_mult_1_right";
|
|
543 |
|
|
544 |
Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
|
|
545 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
546 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
|
|
547 |
qed "hypreal_mult_0";
|
|
548 |
|
|
549 |
Goal "z * 0 = (0::hypreal)";
|
|
550 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute, hypreal_mult_0]) 1);
|
|
551 |
qed "hypreal_mult_0_right";
|
|
552 |
|
|
553 |
Addsimps [hypreal_mult_0,hypreal_mult_0_right];
|
|
554 |
|
|
555 |
Goal "-(x * y) = -x * (y::hypreal)";
|
|
556 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
557 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
558 |
by (auto_tac (claset(),
|
|
559 |
simpset() addsimps [hypreal_minus, hypreal_mult]
|
|
560 |
@ real_mult_ac @ real_add_ac));
|
|
561 |
qed "hypreal_minus_mult_eq1";
|
|
562 |
|
|
563 |
Goal "-(x * y) = (x::hypreal) * -y";
|
|
564 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
565 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
566 |
by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult]
|
|
567 |
@ real_mult_ac @ real_add_ac));
|
|
568 |
qed "hypreal_minus_mult_eq2";
|
|
569 |
|
|
570 |
(*Pull negations out*)
|
|
571 |
Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
|
|
572 |
|
|
573 |
Goal "-x*y = (x::hypreal)*-y";
|
|
574 |
by Auto_tac;
|
|
575 |
qed "hypreal_minus_mult_commute";
|
|
576 |
|
|
577 |
(*-----------------------------------------------------------------------------
|
|
578 |
A few more theorems
|
|
579 |
----------------------------------------------------------------------------*)
|
|
580 |
Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
|
|
581 |
by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
582 |
qed "hypreal_add_assoc_cong";
|
|
583 |
|
|
584 |
Goal "(z::hypreal) + (v + w) = v + (z + w)";
|
|
585 |
by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
|
|
586 |
qed "hypreal_add_assoc_swap";
|
|
587 |
|
|
588 |
Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
|
|
589 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
|
|
590 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
|
|
591 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
|
|
592 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
|
|
593 |
real_add_mult_distrib]) 1);
|
|
594 |
qed "hypreal_add_mult_distrib";
|
|
595 |
|
|
596 |
val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
|
|
597 |
|
|
598 |
Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
|
|
599 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
|
|
600 |
qed "hypreal_add_mult_distrib2";
|
|
601 |
|
|
602 |
bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
|
|
603 |
Addsimps hypreal_mult_simps;
|
|
604 |
|
|
605 |
(* 07/00 *)
|
|
606 |
|
|
607 |
Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
|
|
608 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
|
|
609 |
qed "hypreal_diff_mult_distrib";
|
|
610 |
|
|
611 |
Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
|
|
612 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute',
|
|
613 |
hypreal_diff_mult_distrib]) 1);
|
|
614 |
qed "hypreal_diff_mult_distrib2";
|
|
615 |
|
|
616 |
(*** one and zero are distinct ***)
|
|
617 |
Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
|
|
618 |
by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
|
|
619 |
qed "hypreal_zero_not_eq_one";
|
|
620 |
|
|
621 |
|
|
622 |
(**** multiplicative inverse on hypreal ****)
|
|
623 |
|
|
624 |
Goalw [congruent_def]
|
10797
|
625 |
"congruent hyprel (%X. hyprel```{%n. if X n = #0 then #0 else inverse(X n)})";
|
10751
|
626 |
by (Auto_tac THEN Ultra_tac 1);
|
|
627 |
qed "hypreal_inverse_congruent";
|
|
628 |
|
|
629 |
Goalw [hypreal_inverse_def]
|
10797
|
630 |
"inverse (Abs_hypreal(hyprel```{%n. X n})) = \
|
|
631 |
\ Abs_hypreal(hyprel ``` {%n. if X n = #0 then #0 else inverse(X n)})";
|
10751
|
632 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
633 |
by (simp_tac (simpset() addsimps
|
|
634 |
[hyprel_in_hypreal RS Abs_hypreal_inverse,
|
|
635 |
[equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
|
|
636 |
qed "hypreal_inverse";
|
|
637 |
|
|
638 |
Goal "inverse 0 = (0::hypreal)";
|
|
639 |
by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1);
|
|
640 |
qed "HYPREAL_INVERSE_ZERO";
|
|
641 |
|
|
642 |
Goal "a / (0::hypreal) = 0";
|
|
643 |
by (simp_tac
|
|
644 |
(simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1);
|
|
645 |
qed "HYPREAL_DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)
|
|
646 |
|
|
647 |
fun hypreal_div_undefined_case_tac s i =
|
|
648 |
case_tac s i THEN
|
|
649 |
asm_simp_tac
|
|
650 |
(simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i;
|
|
651 |
|
|
652 |
Goal "inverse (inverse (z::hypreal)) = z";
|
|
653 |
by (hypreal_div_undefined_case_tac "z=0" 1);
|
|
654 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
655 |
by (asm_full_simp_tac (simpset() addsimps
|
|
656 |
[hypreal_inverse, hypreal_zero_def]) 1);
|
|
657 |
qed "hypreal_inverse_inverse";
|
|
658 |
Addsimps [hypreal_inverse_inverse];
|
|
659 |
|
|
660 |
Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
|
|
661 |
by (full_simp_tac (simpset() addsimps [hypreal_inverse,
|
|
662 |
real_zero_not_eq_one RS not_sym]) 1);
|
|
663 |
qed "hypreal_inverse_1";
|
|
664 |
Addsimps [hypreal_inverse_1];
|
|
665 |
|
|
666 |
|
|
667 |
(*** existence of inverse ***)
|
|
668 |
|
|
669 |
Goalw [hypreal_one_def,hypreal_zero_def]
|
|
670 |
"x ~= 0 ==> x*inverse(x) = 1hr";
|
|
671 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
672 |
by (rotate_tac 1 1);
|
|
673 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
|
|
674 |
by (dtac FreeUltrafilterNat_Compl_mem 1);
|
|
675 |
by (blast_tac (claset() addSIs [real_mult_inv_right,
|
|
676 |
FreeUltrafilterNat_subset]) 1);
|
|
677 |
qed "hypreal_mult_inverse";
|
|
678 |
|
|
679 |
Goal "x ~= 0 ==> inverse(x)*x = 1hr";
|
|
680 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse,
|
|
681 |
hypreal_mult_commute]) 1);
|
|
682 |
qed "hypreal_mult_inverse_left";
|
|
683 |
|
|
684 |
Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
|
|
685 |
by Auto_tac;
|
|
686 |
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
|
|
687 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1);
|
|
688 |
qed "hypreal_mult_left_cancel";
|
|
689 |
|
|
690 |
Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)";
|
|
691 |
by (Step_tac 1);
|
|
692 |
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
|
|
693 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1);
|
|
694 |
qed "hypreal_mult_right_cancel";
|
|
695 |
|
|
696 |
Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0";
|
|
697 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
698 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
|
|
699 |
qed "hypreal_inverse_not_zero";
|
|
700 |
|
|
701 |
Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left];
|
|
702 |
|
|
703 |
Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";
|
|
704 |
by (Step_tac 1);
|
|
705 |
by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
|
|
706 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
|
|
707 |
qed "hypreal_mult_not_0";
|
|
708 |
|
|
709 |
Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
|
|
710 |
by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0],
|
|
711 |
simpset()));
|
|
712 |
qed "hypreal_mult_zero_disj";
|
|
713 |
|
|
714 |
Goal "inverse(-x) = -inverse(x::hypreal)";
|
|
715 |
by (hypreal_div_undefined_case_tac "x=0" 1);
|
|
716 |
by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
|
|
717 |
by (stac hypreal_mult_inverse_left 2);
|
|
718 |
by Auto_tac;
|
|
719 |
qed "hypreal_minus_inverse";
|
|
720 |
|
|
721 |
Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
|
|
722 |
by (hypreal_div_undefined_case_tac "x=0" 1);
|
|
723 |
by (hypreal_div_undefined_case_tac "y=0" 1);
|
|
724 |
by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
|
|
725 |
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
726 |
by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym]));
|
|
727 |
by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
|
|
728 |
by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute]));
|
|
729 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
|
|
730 |
qed "hypreal_inverse_distrib";
|
|
731 |
|
|
732 |
(*------------------------------------------------------------------
|
|
733 |
Theorems for ordering
|
|
734 |
------------------------------------------------------------------*)
|
|
735 |
|
|
736 |
(* prove introduction and elimination rules for hypreal_less *)
|
|
737 |
|
|
738 |
Goalw [hypreal_less_def]
|
|
739 |
"P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
|
|
740 |
\ Y : Rep_hypreal(Q) & \
|
|
741 |
\ {n. X n < Y n} : FreeUltrafilterNat)";
|
|
742 |
by (Fast_tac 1);
|
|
743 |
qed "hypreal_less_iff";
|
|
744 |
|
|
745 |
Goalw [hypreal_less_def]
|
|
746 |
"[| {n. X n < Y n} : FreeUltrafilterNat; \
|
|
747 |
\ X : Rep_hypreal(P); \
|
|
748 |
\ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
|
|
749 |
by (Fast_tac 1);
|
|
750 |
qed "hypreal_lessI";
|
|
751 |
|
|
752 |
|
|
753 |
Goalw [hypreal_less_def]
|
|
754 |
"!! R1. [| R1 < (R2::hypreal); \
|
|
755 |
\ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
|
|
756 |
\ !!X. X : Rep_hypreal(R1) ==> P; \
|
|
757 |
\ !!Y. Y : Rep_hypreal(R2) ==> P |] \
|
|
758 |
\ ==> P";
|
|
759 |
by Auto_tac;
|
|
760 |
qed "hypreal_lessE";
|
|
761 |
|
|
762 |
Goalw [hypreal_less_def]
|
|
763 |
"R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
|
|
764 |
\ X : Rep_hypreal(R1) & \
|
|
765 |
\ Y : Rep_hypreal(R2))";
|
|
766 |
by (Fast_tac 1);
|
|
767 |
qed "hypreal_lessD";
|
|
768 |
|
|
769 |
Goal "~ (R::hypreal) < R";
|
|
770 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
|
|
771 |
by (auto_tac (claset(), simpset() addsimps [hypreal_less_def]));
|
|
772 |
by (Ultra_tac 1);
|
|
773 |
qed "hypreal_less_not_refl";
|
|
774 |
|
|
775 |
(*** y < y ==> P ***)
|
|
776 |
bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
|
|
777 |
AddSEs [hypreal_less_irrefl];
|
|
778 |
|
|
779 |
Goal "!!(x::hypreal). x < y ==> x ~= y";
|
|
780 |
by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl]));
|
|
781 |
qed "hypreal_not_refl2";
|
|
782 |
|
|
783 |
Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
|
|
784 |
by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
|
|
785 |
by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
|
|
786 |
by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
|
|
787 |
by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def]));
|
|
788 |
by (ultra_tac (claset() addIs [order_less_trans], simpset()) 1);
|
|
789 |
qed "hypreal_less_trans";
|
|
790 |
|
|
791 |
Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
|
|
792 |
by (dtac hypreal_less_trans 1 THEN assume_tac 1);
|
|
793 |
by (asm_full_simp_tac (simpset() addsimps
|
|
794 |
[hypreal_less_not_refl]) 1);
|
|
795 |
qed "hypreal_less_asym";
|
|
796 |
|
|
797 |
(*-------------------------------------------------------
|
|
798 |
TODO: The following theorem should have been proved
|
|
799 |
first and then used througout the proofs as it probably
|
|
800 |
makes many of them more straightforward.
|
|
801 |
-------------------------------------------------------*)
|
|
802 |
Goalw [hypreal_less_def]
|
10797
|
803 |
"(Abs_hypreal(hyprel```{%n. X n}) < \
|
|
804 |
\ Abs_hypreal(hyprel```{%n. Y n})) = \
|
10751
|
805 |
\ ({n. X n < Y n} : FreeUltrafilterNat)";
|
|
806 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
|
|
807 |
by (Ultra_tac 1);
|
|
808 |
qed "hypreal_less";
|
|
809 |
|
|
810 |
(*---------------------------------------------------------------------------------
|
|
811 |
Hyperreals as a linearly ordered field
|
|
812 |
---------------------------------------------------------------------------------*)
|
|
813 |
(*** sum order
|
|
814 |
Goalw [hypreal_zero_def]
|
|
815 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
|
|
816 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
817 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
818 |
by (auto_tac (claset(),simpset() addsimps
|
|
819 |
[hypreal_less_def,hypreal_add]));
|
|
820 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps
|
|
821 |
[hypreal_less_def,hypreal_add]));
|
|
822 |
by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
|
|
823 |
qed "hypreal_add_order";
|
|
824 |
***)
|
|
825 |
|
|
826 |
(*** mult order
|
|
827 |
Goalw [hypreal_zero_def]
|
|
828 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
|
|
829 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
830 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
831 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps
|
|
832 |
[hypreal_less_def,hypreal_mult]));
|
|
833 |
by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
|
|
834 |
simpset()) 1);
|
|
835 |
qed "hypreal_mult_order";
|
|
836 |
****)
|
|
837 |
|
|
838 |
|
|
839 |
(*---------------------------------------------------------------------------------
|
|
840 |
Trichotomy of the hyperreals
|
|
841 |
--------------------------------------------------------------------------------*)
|
|
842 |
|
10797
|
843 |
Goalw [hyprel_def] "EX x. x: hyprel ``` {%n. #0}";
|
10751
|
844 |
by (res_inst_tac [("x","%n. #0")] exI 1);
|
|
845 |
by (Step_tac 1);
|
|
846 |
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
|
|
847 |
qed "lemma_hyprel_0r_mem";
|
|
848 |
|
|
849 |
Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)";
|
|
850 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
851 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
|
|
852 |
by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
|
|
853 |
by (dres_inst_tac [("x","xa")] spec 1);
|
|
854 |
by (dres_inst_tac [("x","x")] spec 1);
|
|
855 |
by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
|
|
856 |
by Auto_tac;
|
|
857 |
by (dres_inst_tac [("x","x")] spec 1);
|
|
858 |
by (dres_inst_tac [("x","xa")] spec 1);
|
|
859 |
by Auto_tac;
|
|
860 |
by (Ultra_tac 1);
|
|
861 |
by (auto_tac (claset() addIs [real_linear_less2],simpset()));
|
|
862 |
qed "hypreal_trichotomy";
|
|
863 |
|
|
864 |
val prems = Goal "[| (0::hypreal) < x ==> P; \
|
|
865 |
\ x = 0 ==> P; \
|
|
866 |
\ x < 0 ==> P |] ==> P";
|
|
867 |
by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
|
|
868 |
by (REPEAT (eresolve_tac (disjE::prems) 1));
|
|
869 |
qed "hypreal_trichotomyE";
|
|
870 |
|
|
871 |
(*----------------------------------------------------------------------------
|
|
872 |
More properties of <
|
|
873 |
----------------------------------------------------------------------------*)
|
|
874 |
|
|
875 |
Goal "((x::hypreal) < y) = (0 < y + -x)";
|
|
876 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
877 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
878 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add,
|
|
879 |
hypreal_zero_def,hypreal_minus,hypreal_less]));
|
|
880 |
by (ALLGOALS(Ultra_tac));
|
|
881 |
qed "hypreal_less_minus_iff";
|
|
882 |
|
|
883 |
Goal "((x::hypreal) < y) = (x + -y < 0)";
|
|
884 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
885 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
886 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add,
|
|
887 |
hypreal_zero_def,hypreal_minus,hypreal_less]));
|
|
888 |
by (ALLGOALS(Ultra_tac));
|
|
889 |
qed "hypreal_less_minus_iff2";
|
|
890 |
|
|
891 |
Goal "((x::hypreal) = y) = (x + - y = 0)";
|
|
892 |
by Auto_tac;
|
|
893 |
by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
|
|
894 |
by Auto_tac;
|
|
895 |
qed "hypreal_eq_minus_iff";
|
|
896 |
|
|
897 |
Goal "((x::hypreal) = y) = (0 = y + - x)";
|
|
898 |
by Auto_tac;
|
|
899 |
by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
|
|
900 |
by Auto_tac;
|
|
901 |
qed "hypreal_eq_minus_iff2";
|
|
902 |
|
|
903 |
(* 07/00 *)
|
|
904 |
Goal "(0::hypreal) - x = -x";
|
|
905 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
|
|
906 |
qed "hypreal_diff_zero";
|
|
907 |
|
|
908 |
Goal "x - (0::hypreal) = x";
|
|
909 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
|
|
910 |
qed "hypreal_diff_zero_right";
|
|
911 |
|
|
912 |
Goal "x - x = (0::hypreal)";
|
|
913 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
|
|
914 |
qed "hypreal_diff_self";
|
|
915 |
|
|
916 |
Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self];
|
|
917 |
|
|
918 |
Goal "(x = y + z) = (x + -z = (y::hypreal))";
|
|
919 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
|
|
920 |
qed "hypreal_eq_minus_iff3";
|
|
921 |
|
|
922 |
Goal "(x ~= a) = (x + -a ~= (0::hypreal))";
|
|
923 |
by (auto_tac (claset() addDs [hypreal_eq_minus_iff RS iffD2],
|
|
924 |
simpset()));
|
|
925 |
qed "hypreal_not_eq_minus_iff";
|
|
926 |
|
|
927 |
Goal "(x+y = (0::hypreal)) = (x = -y)";
|
|
928 |
by (stac hypreal_eq_minus_iff 1);
|
|
929 |
by Auto_tac;
|
|
930 |
qed "hypreal_add_eq_0_iff";
|
|
931 |
AddIffs [hypreal_add_eq_0_iff];
|
|
932 |
|
|
933 |
|
|
934 |
(*** linearity ***)
|
|
935 |
|
|
936 |
Goal "(x::hypreal) < y | x = y | y < x";
|
|
937 |
by (stac hypreal_eq_minus_iff2 1);
|
|
938 |
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
|
|
939 |
by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
|
|
940 |
by (rtac hypreal_trichotomyE 1);
|
|
941 |
by Auto_tac;
|
|
942 |
qed "hypreal_linear";
|
|
943 |
|
|
944 |
Goal "((w::hypreal) ~= z) = (w<z | z<w)";
|
|
945 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
946 |
by (Blast_tac 1);
|
|
947 |
qed "hypreal_neq_iff";
|
|
948 |
|
|
949 |
Goal "!!(x::hypreal). [| x < y ==> P; x = y ==> P; \
|
|
950 |
\ y < x ==> P |] ==> P";
|
|
951 |
by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
|
|
952 |
by Auto_tac;
|
|
953 |
qed "hypreal_linear_less2";
|
|
954 |
|
|
955 |
(*------------------------------------------------------------------------------
|
|
956 |
Properties of <=
|
|
957 |
------------------------------------------------------------------------------*)
|
|
958 |
(*------ hypreal le iff reals le a.e ------*)
|
|
959 |
|
|
960 |
Goalw [hypreal_le_def,real_le_def]
|
10797
|
961 |
"(Abs_hypreal(hyprel```{%n. X n}) <= \
|
|
962 |
\ Abs_hypreal(hyprel```{%n. Y n})) = \
|
10751
|
963 |
\ ({n. X n <= Y n} : FreeUltrafilterNat)";
|
|
964 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
|
|
965 |
by (ALLGOALS(Ultra_tac));
|
|
966 |
qed "hypreal_le";
|
|
967 |
|
|
968 |
(*---------------------------------------------------------*)
|
|
969 |
(*---------------------------------------------------------*)
|
|
970 |
Goalw [hypreal_le_def]
|
|
971 |
"~(w < z) ==> z <= (w::hypreal)";
|
|
972 |
by (assume_tac 1);
|
|
973 |
qed "hypreal_leI";
|
|
974 |
|
|
975 |
Goalw [hypreal_le_def]
|
|
976 |
"z<=w ==> ~(w<(z::hypreal))";
|
|
977 |
by (assume_tac 1);
|
|
978 |
qed "hypreal_leD";
|
|
979 |
|
|
980 |
bind_thm ("hypreal_leE", make_elim hypreal_leD);
|
|
981 |
|
|
982 |
Goal "(~(w < z)) = (z <= (w::hypreal))";
|
|
983 |
by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
|
|
984 |
qed "hypreal_less_le_iff";
|
|
985 |
|
|
986 |
Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
|
|
987 |
by (Fast_tac 1);
|
|
988 |
qed "not_hypreal_leE";
|
|
989 |
|
|
990 |
Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
|
|
991 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
992 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
|
|
993 |
qed "hypreal_le_imp_less_or_eq";
|
|
994 |
|
|
995 |
Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
|
|
996 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
997 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
|
|
998 |
qed "hypreal_less_or_eq_imp_le";
|
|
999 |
|
|
1000 |
Goal "(x <= (y::hypreal)) = (x < y | x=y)";
|
|
1001 |
by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
|
|
1002 |
qed "hypreal_le_eq_less_or_eq";
|
|
1003 |
val hypreal_le_less = hypreal_le_eq_less_or_eq;
|
|
1004 |
|
|
1005 |
Goal "w <= (w::hypreal)";
|
|
1006 |
by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
|
|
1007 |
qed "hypreal_le_refl";
|
|
1008 |
|
|
1009 |
(* Axiom 'linorder_linear' of class 'linorder': *)
|
|
1010 |
Goal "(z::hypreal) <= w | w <= z";
|
|
1011 |
by (simp_tac (simpset() addsimps [hypreal_le_less]) 1);
|
|
1012 |
by (cut_facts_tac [hypreal_linear] 1);
|
|
1013 |
by (Blast_tac 1);
|
|
1014 |
qed "hypreal_le_linear";
|
|
1015 |
|
|
1016 |
Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
|
|
1017 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
|
|
1018 |
rtac hypreal_less_or_eq_imp_le,
|
|
1019 |
fast_tac (claset() addIs [hypreal_less_trans])]);
|
|
1020 |
qed "hypreal_le_trans";
|
|
1021 |
|
|
1022 |
Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
|
|
1023 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
|
|
1024 |
fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
|
|
1025 |
qed "hypreal_le_anti_sym";
|
|
1026 |
|
|
1027 |
Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
|
|
1028 |
by (rtac not_hypreal_leE 1);
|
|
1029 |
by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
|
|
1030 |
qed "not_less_not_eq_hypreal_less";
|
|
1031 |
|
|
1032 |
(* Axiom 'order_less_le' of class 'order': *)
|
|
1033 |
Goal "(w::hypreal) < z = (w <= z & w ~= z)";
|
|
1034 |
by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
|
|
1035 |
by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
|
|
1036 |
qed "hypreal_less_le";
|
|
1037 |
|
|
1038 |
Goal "(0 < -R) = (R < (0::hypreal))";
|
|
1039 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
|
|
1040 |
by (auto_tac (claset(),
|
|
1041 |
simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
|
|
1042 |
qed "hypreal_minus_zero_less_iff";
|
|
1043 |
Addsimps [hypreal_minus_zero_less_iff];
|
|
1044 |
|
|
1045 |
Goal "(-R < 0) = ((0::hypreal) < R)";
|
|
1046 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
|
|
1047 |
by (auto_tac (claset(),
|
|
1048 |
simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
|
|
1049 |
by (ALLGOALS(Ultra_tac));
|
|
1050 |
qed "hypreal_minus_zero_less_iff2";
|
|
1051 |
|
|
1052 |
Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))";
|
|
1053 |
by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1);
|
|
1054 |
qed "hypreal_minus_zero_le_iff";
|
|
1055 |
Addsimps [hypreal_minus_zero_le_iff];
|
|
1056 |
|
|
1057 |
(*----------------------------------------------------------
|
|
1058 |
hypreal_of_real preserves field and order properties
|
|
1059 |
-----------------------------------------------------------*)
|
|
1060 |
Goalw [hypreal_of_real_def]
|
|
1061 |
"hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2";
|
|
1062 |
by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1);
|
|
1063 |
qed "hypreal_of_real_add";
|
|
1064 |
Addsimps [hypreal_of_real_add];
|
|
1065 |
|
|
1066 |
Goalw [hypreal_of_real_def]
|
|
1067 |
"hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2";
|
|
1068 |
by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1);
|
|
1069 |
qed "hypreal_of_real_mult";
|
|
1070 |
Addsimps [hypreal_of_real_mult];
|
|
1071 |
|
|
1072 |
Goalw [hypreal_less_def,hypreal_of_real_def]
|
|
1073 |
"(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)";
|
|
1074 |
by Auto_tac;
|
|
1075 |
by (res_inst_tac [("x","%n. z1")] exI 2);
|
|
1076 |
by (Step_tac 1);
|
|
1077 |
by (res_inst_tac [("x","%n. z2")] exI 3);
|
|
1078 |
by Auto_tac;
|
|
1079 |
by (rtac FreeUltrafilterNat_P 1);
|
|
1080 |
by (Ultra_tac 1);
|
|
1081 |
qed "hypreal_of_real_less_iff";
|
|
1082 |
Addsimps [hypreal_of_real_less_iff];
|
|
1083 |
|
|
1084 |
Goalw [hypreal_le_def,real_le_def]
|
|
1085 |
"(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)";
|
|
1086 |
by Auto_tac;
|
|
1087 |
qed "hypreal_of_real_le_iff";
|
|
1088 |
Addsimps [hypreal_of_real_le_iff];
|
|
1089 |
|
|
1090 |
Goal "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)";
|
|
1091 |
by (force_tac (claset() addIs [order_antisym, hypreal_of_real_le_iff RS iffD1],
|
|
1092 |
simpset()) 1);
|
|
1093 |
qed "hypreal_of_real_eq_iff";
|
|
1094 |
Addsimps [hypreal_of_real_eq_iff];
|
|
1095 |
|
|
1096 |
Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r";
|
|
1097 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
|
|
1098 |
qed "hypreal_of_real_minus";
|
|
1099 |
Addsimps [hypreal_of_real_minus];
|
|
1100 |
|
|
1101 |
(*DON'T insert this or the next one as default simprules.
|
|
1102 |
They are used in both orientations and anyway aren't the ones we finally
|
|
1103 |
need, which would use binary literals.*)
|
|
1104 |
Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real #1 = 1hr";
|
|
1105 |
by (Step_tac 1);
|
|
1106 |
qed "hypreal_of_real_one";
|
|
1107 |
|
|
1108 |
Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0";
|
|
1109 |
by (Step_tac 1);
|
|
1110 |
qed "hypreal_of_real_zero";
|
|
1111 |
|
|
1112 |
Goal "(hypreal_of_real r = 0) = (r = #0)";
|
|
1113 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
|
|
1114 |
simpset() addsimps [hypreal_of_real_def,
|
|
1115 |
hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
|
|
1116 |
qed "hypreal_of_real_zero_iff";
|
|
1117 |
|
|
1118 |
Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)";
|
|
1119 |
by (case_tac "r=#0" 1);
|
|
1120 |
by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO,
|
|
1121 |
HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1);
|
|
1122 |
by (res_inst_tac [("c1","hypreal_of_real r")]
|
|
1123 |
(hypreal_mult_left_cancel RS iffD1) 1);
|
|
1124 |
by (stac (hypreal_of_real_mult RS sym) 2);
|
|
1125 |
by (auto_tac (claset(),
|
|
1126 |
simpset() addsimps [hypreal_of_real_one, hypreal_of_real_zero_iff]));
|
|
1127 |
qed "hypreal_of_real_inverse";
|
|
1128 |
Addsimps [hypreal_of_real_inverse];
|
|
1129 |
|
|
1130 |
Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2";
|
|
1131 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1);
|
|
1132 |
qed "hypreal_of_real_divide";
|
|
1133 |
Addsimps [hypreal_of_real_divide];
|
|
1134 |
|
|
1135 |
|
|
1136 |
(*** Division lemmas ***)
|
|
1137 |
|
|
1138 |
Goal "(0::hypreal)/x = 0";
|
|
1139 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
|
|
1140 |
qed "hypreal_zero_divide";
|
|
1141 |
|
|
1142 |
Goal "x/1hr = x";
|
|
1143 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
|
|
1144 |
qed "hypreal_divide_one";
|
|
1145 |
Addsimps [hypreal_zero_divide, hypreal_divide_one];
|
|
1146 |
|
|
1147 |
Goal "(x::hypreal) * (y/z) = (x*y)/z";
|
|
1148 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
|
|
1149 |
qed "hypreal_times_divide1_eq";
|
|
1150 |
|
|
1151 |
Goal "(y/z) * (x::hypreal) = (y*x)/z";
|
|
1152 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1);
|
|
1153 |
qed "hypreal_times_divide2_eq";
|
|
1154 |
|
|
1155 |
Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq];
|
|
1156 |
|
|
1157 |
Goal "(x::hypreal) / (y/z) = (x*z)/y";
|
|
1158 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@
|
|
1159 |
hypreal_mult_ac) 1);
|
|
1160 |
qed "hypreal_divide_divide1_eq";
|
|
1161 |
|
|
1162 |
Goal "((x::hypreal) / y) / z = x/(y*z)";
|
|
1163 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib,
|
|
1164 |
hypreal_mult_assoc]) 1);
|
|
1165 |
qed "hypreal_divide_divide2_eq";
|
|
1166 |
|
|
1167 |
Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq];
|
|
1168 |
|
|
1169 |
(** As with multiplication, pull minus signs OUT of the / operator **)
|
|
1170 |
|
|
1171 |
Goal "(-x) / (y::hypreal) = - (x/y)";
|
|
1172 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
|
|
1173 |
qed "hypreal_minus_divide_eq";
|
|
1174 |
Addsimps [hypreal_minus_divide_eq];
|
|
1175 |
|
|
1176 |
Goal "(x / -(y::hypreal)) = - (x/y)";
|
|
1177 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
|
|
1178 |
qed "hypreal_divide_minus_eq";
|
|
1179 |
Addsimps [hypreal_divide_minus_eq];
|
|
1180 |
|
|
1181 |
Goal "(x+y)/(z::hypreal) = x/z + y/z";
|
|
1182 |
by (simp_tac (simpset() addsimps [hypreal_divide_def,
|
|
1183 |
hypreal_add_mult_distrib]) 1);
|
|
1184 |
qed "hypreal_add_divide_distrib";
|
|
1185 |
|
|
1186 |
Goal "[|(x::hypreal) ~= 0; y ~= 0 |] \
|
|
1187 |
\ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
|
|
1188 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib,
|
|
1189 |
hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
|
|
1190 |
by (stac hypreal_mult_assoc 1);
|
|
1191 |
by (rtac (hypreal_mult_left_commute RS subst) 1);
|
|
1192 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
|
|
1193 |
qed "hypreal_inverse_add";
|
|
1194 |
|
|
1195 |
Goal "x = -x ==> x = (0::hypreal)";
|
|
1196 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
1197 |
by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_zero_def]));
|
|
1198 |
by (Ultra_tac 1);
|
|
1199 |
qed "hypreal_self_eq_minus_self_zero";
|
|
1200 |
|
|
1201 |
Goal "(x + x = 0) = (x = (0::hypreal))";
|
|
1202 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
1203 |
by (auto_tac (claset(), simpset() addsimps [hypreal_add, hypreal_zero_def]));
|
|
1204 |
qed "hypreal_add_self_zero_cancel";
|
|
1205 |
Addsimps [hypreal_add_self_zero_cancel];
|
|
1206 |
|
|
1207 |
Goal "(x + x + y = y) = (x = (0::hypreal))";
|
|
1208 |
by Auto_tac;
|
|
1209 |
by (dtac (hypreal_eq_minus_iff RS iffD1) 1);
|
|
1210 |
by (auto_tac (claset(),
|
|
1211 |
simpset() addsimps [hypreal_add_assoc, hypreal_self_eq_minus_self_zero]));
|
|
1212 |
qed "hypreal_add_self_zero_cancel2";
|
|
1213 |
Addsimps [hypreal_add_self_zero_cancel2];
|
|
1214 |
|
|
1215 |
Goal "(x + (x + y) = y) = (x = (0::hypreal))";
|
|
1216 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
|
|
1217 |
qed "hypreal_add_self_zero_cancel2a";
|
|
1218 |
Addsimps [hypreal_add_self_zero_cancel2a];
|
|
1219 |
|
|
1220 |
Goal "(b = -a) = (-b = (a::hypreal))";
|
|
1221 |
by Auto_tac;
|
|
1222 |
qed "hypreal_minus_eq_swap";
|
|
1223 |
|
|
1224 |
Goal "(-b = -a) = (b = (a::hypreal))";
|
|
1225 |
by (asm_full_simp_tac (simpset() addsimps
|
|
1226 |
[hypreal_minus_eq_swap]) 1);
|
|
1227 |
qed "hypreal_minus_eq_cancel";
|
|
1228 |
Addsimps [hypreal_minus_eq_cancel];
|
|
1229 |
|
|
1230 |
Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
|
|
1231 |
by (rtac hypreal_less_minus_iff2 1);
|
|
1232 |
qed "hypreal_less_eq_diff";
|
|
1233 |
|
|
1234 |
(*** Subtraction laws ***)
|
|
1235 |
|
|
1236 |
Goal "x + (y - z) = (x + y) - (z::hypreal)";
|
|
1237 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1238 |
qed "hypreal_add_diff_eq";
|
|
1239 |
|
|
1240 |
Goal "(x - y) + z = (x + z) - (y::hypreal)";
|
|
1241 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1242 |
qed "hypreal_diff_add_eq";
|
|
1243 |
|
|
1244 |
Goal "(x - y) - z = x - (y + (z::hypreal))";
|
|
1245 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1246 |
qed "hypreal_diff_diff_eq";
|
|
1247 |
|
|
1248 |
Goal "x - (y - z) = (x + z) - (y::hypreal)";
|
|
1249 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1250 |
qed "hypreal_diff_diff_eq2";
|
|
1251 |
|
|
1252 |
Goal "(x-y < z) = (x < z + (y::hypreal))";
|
|
1253 |
by (stac hypreal_less_eq_diff 1);
|
|
1254 |
by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1);
|
|
1255 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1256 |
qed "hypreal_diff_less_eq";
|
|
1257 |
|
|
1258 |
Goal "(x < z-y) = (x + (y::hypreal) < z)";
|
|
1259 |
by (stac hypreal_less_eq_diff 1);
|
|
1260 |
by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1);
|
|
1261 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
|
|
1262 |
qed "hypreal_less_diff_eq";
|
|
1263 |
|
|
1264 |
Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))";
|
|
1265 |
by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1);
|
|
1266 |
qed "hypreal_diff_le_eq";
|
|
1267 |
|
|
1268 |
Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)";
|
|
1269 |
by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
|
|
1270 |
qed "hypreal_le_diff_eq";
|
|
1271 |
|
|
1272 |
Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))";
|
|
1273 |
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
|
|
1274 |
qed "hypreal_diff_eq_eq";
|
|
1275 |
|
|
1276 |
Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)";
|
|
1277 |
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
|
|
1278 |
qed "hypreal_eq_diff_eq";
|
|
1279 |
|
|
1280 |
(*This list of rewrites simplifies (in)equalities by bringing subtractions
|
|
1281 |
to the top and then moving negative terms to the other side.
|
|
1282 |
Use with hypreal_add_ac*)
|
|
1283 |
val hypreal_compare_rls =
|
|
1284 |
[symmetric hypreal_diff_def,
|
|
1285 |
hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq,
|
|
1286 |
hypreal_diff_diff_eq2,
|
|
1287 |
hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq,
|
|
1288 |
hypreal_le_diff_eq, hypreal_diff_eq_eq, hypreal_eq_diff_eq];
|
|
1289 |
|
|
1290 |
|
|
1291 |
(** For the cancellation simproc.
|
|
1292 |
The idea is to cancel like terms on opposite sides by subtraction **)
|
|
1293 |
|
|
1294 |
Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')";
|
|
1295 |
by (stac hypreal_less_eq_diff 1);
|
|
1296 |
by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1);
|
|
1297 |
by (Asm_simp_tac 1);
|
|
1298 |
qed "hypreal_less_eqI";
|
|
1299 |
|
|
1300 |
Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')";
|
|
1301 |
by (dtac hypreal_less_eqI 1);
|
|
1302 |
by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1);
|
|
1303 |
qed "hypreal_le_eqI";
|
|
1304 |
|
|
1305 |
Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')";
|
|
1306 |
by Safe_tac;
|
|
1307 |
by (ALLGOALS
|
|
1308 |
(asm_full_simp_tac
|
|
1309 |
(simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
|
|
1310 |
qed "hypreal_eq_eqI";
|
|
1311 |
|