author | paulson |
Tue, 12 Dec 2000 12:01:19 +0100 | |
changeset 10648 | a8c647cfa31f |
parent 10607 | 352f6f209775 |
child 10677 | 36625483213f |
permissions | -rw-r--r-- |
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 ***) |
|
9055 | 13 |
Goal "finite (A::nat set) --> (EX n. ALL m. Suc (n + m) ~: A)"; |
7218 | 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 |
||
9055 | 25 |
Goal "finite (A :: nat set) --> (EX n. n ~:A)"; |
7218 | 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); |
|
9969 | 46 |
by (rtac someI2 1 THEN ALLGOALS(assume_tac)); |
7218 | 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); |
|
9969 | 52 |
by (rtac someI2 1 THEN assume_tac 1); |
7218 | 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); |
|
9969 | 62 |
by (rtac someI2 1 THEN assume_tac 1); |
7218 | 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 |
||
9391 | 110 |
Goal "UNIV : FreeUltrafilterNat"; |
7218 | 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 |
||
10043 | 135 |
(*------------------------------------------------------- |
7218 | 136 |
Define and use Ultrafilter tactics |
10043 | 137 |
-------------------------------------------------------*) |
7218 | 138 |
use "fuf.ML"; |
139 |
||
10043 | 140 |
(*------------------------------------------------------- |
141 |
Now prove one further property of our free ultrafilter |
|
7218 | 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 |
||
10043 | 149 |
(*------------------------------------------------------- |
150 |
Properties of hyprel |
|
151 |
-------------------------------------------------------*) |
|
7218 | 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 |
||
9432 | 172 |
val [major,minor] = goal (the_context ()) |
7218 | 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(),simpset() addsimps |
|
185 |
[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 |
||
9391 | 202 |
Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel"; |
7218 | 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 |
||
9391 | 209 |
(* (hyprel ^^ {x} = hyprel ^^ {y}) = ((x,y) : hyprel) *) |
9108 | 210 |
bind_thm ("equiv_hyprel_iff", |
9391 | 211 |
[equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); |
7218 | 212 |
|
213 |
Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal"; |
|
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]; |
|
9108 | 226 |
bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class)); |
7218 | 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 |
||
233 |
Goalw [hyprel_def] "x: hyprel ^^ {x}"; |
|
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 |
||
9432 | 269 |
val [prem] = goal (the_context ()) |
7218 | 270 |
"(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P"; |
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] |
|
281 |
"congruent hyprel (%X. hyprel^^{%n. - (X n)})"; |
|
282 |
by Safe_tac; |
|
283 |
by (ALLGOALS Ultra_tac); |
|
284 |
qed "hypreal_minus_congruent"; |
|
285 |
||
286 |
Goalw [hypreal_minus_def] |
|
287 |
"- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})"; |
|
288 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
289 |
by (simp_tac (simpset() addsimps |
|
9391 | 290 |
[hyprel_in_hypreal RS Abs_hypreal_inverse, |
291 |
[equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1); |
|
7218 | 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 |
||
9055 | 307 |
Goalw [hypreal_zero_def] "-0 = (0::hypreal)"; |
7218 | 308 |
by (simp_tac (simpset() addsimps [hypreal_minus]) 1); |
309 |
qed "hypreal_minus_zero"; |
|
310 |
||
311 |
Addsimps [hypreal_minus_zero]; |
|
312 |
||
9055 | 313 |
Goal "(-x = 0) = (x = (0::hypreal))"; |
7218 | 314 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
315 |
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
|
316 |
hypreal_minus] @ real_add_ac)); |
|
317 |
qed "hypreal_minus_zero_iff"; |
|
318 |
||
319 |
Addsimps [hypreal_minus_zero_iff]; |
|
10607 | 320 |
(**** multiplicative inverse on hypreal ****) |
7218 | 321 |
|
322 |
Goalw [congruent_def] |
|
10607 | 323 |
"congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})"; |
7218 | 324 |
by (Auto_tac THEN Ultra_tac 1); |
10607 | 325 |
qed "hypreal_inverse_congruent"; |
7218 | 326 |
|
10607 | 327 |
Goalw [hypreal_inverse_def] |
328 |
"inverse (Abs_hypreal(hyprel^^{%n. X n})) = \ |
|
329 |
\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})"; |
|
7218 | 330 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
331 |
by (simp_tac (simpset() addsimps |
|
9391 | 332 |
[hyprel_in_hypreal RS Abs_hypreal_inverse, |
10607 | 333 |
[equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1); |
334 |
qed "hypreal_inverse"; |
|
7218 | 335 |
|
10607 | 336 |
Goal "z ~= 0 ==> inverse (inverse (z::hypreal)) = z"; |
7218 | 337 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
338 |
by (rotate_tac 1 1); |
|
339 |
by (asm_full_simp_tac (simpset() addsimps |
|
10607 | 340 |
[hypreal_inverse,hypreal_zero_def] addsplits [split_if]) 1); |
10648 | 341 |
by (ultra_tac (claset() addDs (map rename_numerals [real_inverse_not_zero]), |
342 |
simpset() addsimps [real_inverse_inverse]) 1); |
|
10607 | 343 |
qed "hypreal_inverse_inverse"; |
7218 | 344 |
|
10607 | 345 |
Addsimps [hypreal_inverse_inverse]; |
7218 | 346 |
|
10607 | 347 |
Goalw [hypreal_one_def] "inverse(1hr) = 1hr"; |
348 |
by (full_simp_tac (simpset() addsimps [hypreal_inverse, |
|
10648 | 349 |
real_zero_not_eq_one RS not_sym]) 1); |
10607 | 350 |
qed "hypreal_inverse_1"; |
351 |
Addsimps [hypreal_inverse_1]; |
|
7218 | 352 |
|
353 |
(**** hyperreal addition: hypreal_add ****) |
|
354 |
||
355 |
Goalw [congruent2_def] |
|
356 |
"congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})"; |
|
357 |
by Safe_tac; |
|
358 |
by (ALLGOALS(Ultra_tac)); |
|
359 |
qed "hypreal_add_congruent2"; |
|
360 |
||
361 |
Goalw [hypreal_add_def] |
|
362 |
"Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
363 |
\ Abs_hypreal(hyprel^^{%n. X n + Y n})"; |
|
9391 | 364 |
by (simp_tac (simpset() addsimps |
365 |
[[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1); |
|
7218 | 366 |
qed "hypreal_add"; |
367 |
||
368 |
Goal "(z::hypreal) + w = w + z"; |
|
369 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
370 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
371 |
by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1); |
|
372 |
qed "hypreal_add_commute"; |
|
373 |
||
374 |
Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"; |
|
375 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
376 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
377 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
378 |
by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1); |
|
379 |
qed "hypreal_add_assoc"; |
|
380 |
||
381 |
(*For AC rewriting*) |
|
382 |
Goal "(x::hypreal)+(y+z)=y+(x+z)"; |
|
383 |
by (rtac (hypreal_add_commute RS trans) 1); |
|
384 |
by (rtac (hypreal_add_assoc RS trans) 1); |
|
385 |
by (rtac (hypreal_add_commute RS arg_cong) 1); |
|
386 |
qed "hypreal_add_left_commute"; |
|
387 |
||
388 |
(* hypreal addition is an AC operator *) |
|
9108 | 389 |
bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute, |
390 |
hypreal_add_left_commute]); |
|
7218 | 391 |
|
9055 | 392 |
Goalw [hypreal_zero_def] "(0::hypreal) + z = z"; |
7218 | 393 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
394 |
by (asm_full_simp_tac (simpset() addsimps |
|
395 |
[hypreal_add]) 1); |
|
396 |
qed "hypreal_add_zero_left"; |
|
397 |
||
9055 | 398 |
Goal "z + (0::hypreal) = z"; |
7218 | 399 |
by (simp_tac (simpset() addsimps |
400 |
[hypreal_add_zero_left,hypreal_add_commute]) 1); |
|
401 |
qed "hypreal_add_zero_right"; |
|
402 |
||
9055 | 403 |
Goalw [hypreal_zero_def] "z + -z = (0::hypreal)"; |
7218 | 404 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
10648 | 405 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1); |
7218 | 406 |
qed "hypreal_add_minus"; |
407 |
||
9055 | 408 |
Goal "-z + z = (0::hypreal)"; |
10648 | 409 |
by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1); |
7218 | 410 |
qed "hypreal_add_minus_left"; |
411 |
||
412 |
Addsimps [hypreal_add_minus,hypreal_add_minus_left, |
|
413 |
hypreal_add_zero_left,hypreal_add_zero_right]; |
|
414 |
||
9055 | 415 |
Goal "EX y. (x::hypreal) + y = 0"; |
7218 | 416 |
by (fast_tac (claset() addIs [hypreal_add_minus]) 1); |
417 |
qed "hypreal_minus_ex"; |
|
418 |
||
9055 | 419 |
Goal "EX! y. (x::hypreal) + y = 0"; |
7218 | 420 |
by (auto_tac (claset() addIs [hypreal_add_minus],simpset())); |
421 |
by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); |
|
422 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
423 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
424 |
qed "hypreal_minus_ex1"; |
|
425 |
||
9055 | 426 |
Goal "EX! y. y + (x::hypreal) = 0"; |
7218 | 427 |
by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset())); |
428 |
by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); |
|
429 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
430 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
431 |
qed "hypreal_minus_left_ex1"; |
|
432 |
||
9055 | 433 |
Goal "x + y = (0::hypreal) ==> x = -y"; |
7218 | 434 |
by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1); |
435 |
by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1); |
|
436 |
by (Blast_tac 1); |
|
437 |
qed "hypreal_add_minus_eq_minus"; |
|
438 |
||
9055 | 439 |
Goal "EX y::hypreal. x = -y"; |
7218 | 440 |
by (cut_inst_tac [("x","x")] hypreal_minus_ex 1); |
441 |
by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1); |
|
442 |
by (Fast_tac 1); |
|
443 |
qed "hypreal_as_add_inverse_ex"; |
|
444 |
||
445 |
Goal "-(x + (y::hypreal)) = -x + -y"; |
|
446 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
447 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
10648 | 448 |
by (auto_tac (claset(), |
449 |
simpset() addsimps [hypreal_minus, hypreal_add, |
|
450 |
real_minus_add_distrib])); |
|
7218 | 451 |
qed "hypreal_minus_add_distrib"; |
10043 | 452 |
Addsimps [hypreal_minus_add_distrib]; |
7218 | 453 |
|
454 |
Goal "-(y + -(x::hypreal)) = x + -y"; |
|
10043 | 455 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
7218 | 456 |
qed "hypreal_minus_distrib1"; |
457 |
||
458 |
Goal "(x + - (y::hypreal)) + (y + - z) = x + -z"; |
|
459 |
by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1); |
|
460 |
by (simp_tac (simpset() addsimps [hypreal_add_left_commute, |
|
10648 | 461 |
hypreal_add_assoc]) 1); |
7218 | 462 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
463 |
qed "hypreal_add_minus_cancel1"; |
|
464 |
||
465 |
Goal "((x::hypreal) + y = x + z) = (y = z)"; |
|
466 |
by (Step_tac 1); |
|
467 |
by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); |
|
468 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
469 |
qed "hypreal_add_left_cancel"; |
|
470 |
||
471 |
Goal "z + (x + (y + -z)) = x + (y::hypreal)"; |
|
472 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
473 |
qed "hypreal_add_minus_cancel2"; |
|
474 |
Addsimps [hypreal_add_minus_cancel2]; |
|
475 |
||
476 |
Goal "y + -(x + y) = -(x::hypreal)"; |
|
10043 | 477 |
by (Full_simp_tac 1); |
7218 | 478 |
by (rtac (hypreal_add_left_commute RS subst) 1); |
479 |
by (Full_simp_tac 1); |
|
480 |
qed "hypreal_add_minus_cancel"; |
|
481 |
Addsimps [hypreal_add_minus_cancel]; |
|
482 |
||
483 |
Goal "y + -(y + x) = -(x::hypreal)"; |
|
10043 | 484 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
7218 | 485 |
qed "hypreal_add_minus_cancelc"; |
486 |
Addsimps [hypreal_add_minus_cancelc]; |
|
487 |
||
488 |
Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))"; |
|
10648 | 489 |
by (full_simp_tac |
490 |
(simpset() addsimps [hypreal_minus_add_distrib RS sym, |
|
491 |
hypreal_add_left_cancel] @ hypreal_add_ac |
|
492 |
delsimps [hypreal_minus_add_distrib]) 1); |
|
7218 | 493 |
qed "hypreal_add_minus_cancel3"; |
494 |
Addsimps [hypreal_add_minus_cancel3]; |
|
495 |
||
496 |
Goal "(y + (x::hypreal)= z + x) = (y = z)"; |
|
497 |
by (simp_tac (simpset() addsimps [hypreal_add_commute, |
|
10648 | 498 |
hypreal_add_left_cancel]) 1); |
7218 | 499 |
qed "hypreal_add_right_cancel"; |
500 |
||
501 |
Goal "z + (y + -z) = (y::hypreal)"; |
|
502 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
503 |
qed "hypreal_add_minus_cancel4"; |
|
504 |
Addsimps [hypreal_add_minus_cancel4]; |
|
505 |
||
506 |
Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)"; |
|
507 |
by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
508 |
qed "hypreal_add_minus_cancel5"; |
|
509 |
Addsimps [hypreal_add_minus_cancel5]; |
|
510 |
||
10043 | 511 |
Goal "z + ((- z) + w) = (w::hypreal)"; |
512 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
513 |
qed "hypreal_add_minus_cancelA"; |
|
514 |
||
515 |
Goal "(-z) + (z + w) = (w::hypreal)"; |
|
516 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
517 |
qed "hypreal_minus_add_cancelA"; |
|
518 |
||
519 |
Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]; |
|
7218 | 520 |
|
521 |
(**** hyperreal multiplication: hypreal_mult ****) |
|
522 |
||
523 |
Goalw [congruent2_def] |
|
524 |
"congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})"; |
|
525 |
by Safe_tac; |
|
526 |
by (ALLGOALS(Ultra_tac)); |
|
527 |
qed "hypreal_mult_congruent2"; |
|
528 |
||
529 |
Goalw [hypreal_mult_def] |
|
530 |
"Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
531 |
\ Abs_hypreal(hyprel^^{%n. X n * Y n})"; |
|
9391 | 532 |
by (simp_tac (simpset() addsimps |
533 |
[[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1); |
|
7218 | 534 |
qed "hypreal_mult"; |
535 |
||
536 |
Goal "(z::hypreal) * w = w * z"; |
|
537 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
538 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
539 |
by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1); |
|
540 |
qed "hypreal_mult_commute"; |
|
541 |
||
542 |
Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"; |
|
543 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
544 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
545 |
by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
546 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1); |
|
547 |
qed "hypreal_mult_assoc"; |
|
548 |
||
9432 | 549 |
qed_goal "hypreal_mult_left_commute" (the_context ()) |
7218 | 550 |
"(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" |
10648 | 551 |
(fn _ => [rtac (hypreal_mult_commute RS trans) 1, |
552 |
rtac (hypreal_mult_assoc RS trans) 1, |
|
7218 | 553 |
rtac (hypreal_mult_commute RS arg_cong) 1]); |
554 |
||
555 |
(* hypreal multiplication is an AC operator *) |
|
9108 | 556 |
bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, |
557 |
hypreal_mult_left_commute]); |
|
7218 | 558 |
|
559 |
Goalw [hypreal_one_def] "1hr * z = z"; |
|
560 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
561 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1); |
|
562 |
qed "hypreal_mult_1"; |
|
563 |
||
564 |
Goal "z * 1hr = z"; |
|
565 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
566 |
hypreal_mult_1]) 1); |
|
567 |
qed "hypreal_mult_1_right"; |
|
568 |
||
9055 | 569 |
Goalw [hypreal_zero_def] "0 * z = (0::hypreal)"; |
7218 | 570 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
571 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1); |
|
572 |
qed "hypreal_mult_0"; |
|
573 |
||
9055 | 574 |
Goal "z * 0 = (0::hypreal)"; |
7218 | 575 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute, |
576 |
hypreal_mult_0]) 1); |
|
577 |
qed "hypreal_mult_0_right"; |
|
578 |
||
579 |
Addsimps [hypreal_mult_0,hypreal_mult_0_right]; |
|
580 |
||
581 |
Goal "-(x * y) = -x * (y::hypreal)"; |
|
582 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
583 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
584 |
by (auto_tac (claset(), |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
585 |
simpset() addsimps [hypreal_minus, hypreal_mult] |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
586 |
@ real_mult_ac @ real_add_ac)); |
7218 | 587 |
qed "hypreal_minus_mult_eq1"; |
588 |
||
589 |
Goal "-(x * y) = (x::hypreal) * -y"; |
|
590 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
591 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
592 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
593 |
hypreal_mult] |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
594 |
@ real_mult_ac @ real_add_ac)); |
7218 | 595 |
qed "hypreal_minus_mult_eq2"; |
596 |
||
9055 | 597 |
(*Pull negations out*) |
598 |
Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym]; |
|
7218 | 599 |
|
600 |
Goal "-x*y = (x::hypreal)*-y"; |
|
9055 | 601 |
by Auto_tac; |
7218 | 602 |
qed "hypreal_minus_mult_commute"; |
603 |
||
604 |
(*----------------------------------------------------------------------------- |
|
605 |
A few more theorems |
|
606 |
----------------------------------------------------------------------------*) |
|
607 |
Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; |
|
608 |
by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
609 |
qed "hypreal_add_assoc_cong"; |
|
610 |
||
611 |
Goal "(z::hypreal) + (v + w) = v + (z + w)"; |
|
612 |
by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1)); |
|
613 |
qed "hypreal_add_assoc_swap"; |
|
614 |
||
615 |
Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"; |
|
616 |
by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
617 |
by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
618 |
by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
619 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add, |
|
620 |
real_add_mult_distrib]) 1); |
|
621 |
qed "hypreal_add_mult_distrib"; |
|
622 |
||
623 |
val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute; |
|
624 |
||
625 |
Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
626 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1); |
|
627 |
qed "hypreal_add_mult_distrib2"; |
|
628 |
||
9108 | 629 |
bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]); |
7218 | 630 |
Addsimps hypreal_mult_simps; |
631 |
||
10043 | 632 |
(* 07/00 *) |
633 |
||
634 |
Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)"; |
|
635 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1); |
|
636 |
qed "hypreal_diff_mult_distrib"; |
|
637 |
||
638 |
Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)"; |
|
639 |
by (simp_tac (simpset() addsimps [hypreal_mult_commute', |
|
640 |
hypreal_diff_mult_distrib]) 1); |
|
641 |
qed "hypreal_diff_mult_distrib2"; |
|
642 |
||
7218 | 643 |
(*** one and zero are distinct ***) |
9055 | 644 |
Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr"; |
7218 | 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] |
|
10607 | 650 |
"x ~= 0 ==> x*inverse(x) = 1hr"; |
7218 | 651 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
652 |
by (rotate_tac 1 1); |
|
10607 | 653 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, |
9387 | 654 |
hypreal_mult] addsplits [split_if]) 1); |
7218 | 655 |
by (dtac FreeUltrafilterNat_Compl_mem 1); |
656 |
by (blast_tac (claset() addSIs [real_mult_inv_right, |
|
657 |
FreeUltrafilterNat_subset]) 1); |
|
10607 | 658 |
qed "hypreal_mult_inverse"; |
7218 | 659 |
|
10607 | 660 |
Goal "x ~= 0 ==> inverse(x)*x = 1hr"; |
661 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse, |
|
9055 | 662 |
hypreal_mult_commute]) 1); |
10607 | 663 |
qed "hypreal_mult_inverse_left"; |
7218 | 664 |
|
9055 | 665 |
Goal "x ~= 0 ==> EX y. x * y = 1hr"; |
10607 | 666 |
by (fast_tac (claset() addDs [hypreal_mult_inverse]) 1); |
667 |
qed "hypreal_inverse_ex"; |
|
7218 | 668 |
|
9055 | 669 |
Goal "x ~= 0 ==> EX y. y * x = 1hr"; |
10607 | 670 |
by (fast_tac (claset() addDs [hypreal_mult_inverse_left]) 1); |
671 |
qed "hypreal_inverse_left_ex"; |
|
7218 | 672 |
|
9055 | 673 |
Goal "x ~= 0 ==> EX! y. x * y = 1hr"; |
10607 | 674 |
by (auto_tac (claset() addIs [hypreal_mult_inverse],simpset())); |
7218 | 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); |
|
10607 | 678 |
qed "hypreal_inverse_ex1"; |
7218 | 679 |
|
9055 | 680 |
Goal "x ~= 0 ==> EX! y. y * x = 1hr"; |
10607 | 681 |
by (auto_tac (claset() addIs [hypreal_mult_inverse_left],simpset())); |
7218 | 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); |
|
10607 | 685 |
qed "hypreal_inverse_left_ex1"; |
7218 | 686 |
|
10607 | 687 |
Goal "[| y~= 0; x * y = 1hr |] ==> x = inverse y"; |
688 |
by (forw_inst_tac [("x","y")] hypreal_mult_inverse_left 1); |
|
689 |
by (res_inst_tac [("x1","y")] (hypreal_inverse_left_ex1 RS ex1E) 1); |
|
7218 | 690 |
by (assume_tac 1); |
691 |
by (Blast_tac 1); |
|
10607 | 692 |
qed "hypreal_mult_inv_inverse"; |
7218 | 693 |
|
10607 | 694 |
Goal "x ~= 0 ==> EX y. x = inverse (y::hypreal)"; |
695 |
by (forw_inst_tac [("x","x")] hypreal_inverse_left_ex 1); |
|
7218 | 696 |
by (etac exE 1 THEN |
10607 | 697 |
forw_inst_tac [("x","y")] hypreal_mult_inv_inverse 1); |
7218 | 698 |
by (res_inst_tac [("x","y")] exI 2); |
699 |
by Auto_tac; |
|
700 |
qed "hypreal_as_inverse_ex"; |
|
701 |
||
9055 | 702 |
Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)"; |
7218 | 703 |
by Auto_tac; |
10607 | 704 |
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
705 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); |
|
7218 | 706 |
qed "hypreal_mult_left_cancel"; |
707 |
||
9055 | 708 |
Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)"; |
7218 | 709 |
by (Step_tac 1); |
10607 | 710 |
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
711 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); |
|
7218 | 712 |
qed "hypreal_mult_right_cancel"; |
713 |
||
10607 | 714 |
Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0"; |
7218 | 715 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
716 |
by (rotate_tac 1 1); |
|
10607 | 717 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, |
9387 | 718 |
hypreal_mult] addsplits [split_if]) 1); |
7218 | 719 |
by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1); |
9071 | 720 |
by (ultra_tac (claset() addIs [ccontr] |
10607 | 721 |
addDs [rename_numerals real_inverse_not_zero], |
9071 | 722 |
simpset()) 1); |
10607 | 723 |
qed "hypreal_inverse_not_zero"; |
7218 | 724 |
|
10607 | 725 |
Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left]; |
7218 | 726 |
|
9055 | 727 |
Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)"; |
7218 | 728 |
by (Step_tac 1); |
10607 | 729 |
by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1); |
7218 | 730 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
731 |
qed "hypreal_mult_not_0"; |
|
732 |
||
733 |
bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE); |
|
734 |
||
10043 | 735 |
Goal "x*y = (0::hypreal) ==> x = 0 | y = 0"; |
736 |
by (auto_tac (claset() addIs [ccontr] addDs |
|
737 |
[hypreal_mult_not_0],simpset())); |
|
738 |
qed "hypreal_mult_zero_disj"; |
|
739 |
||
9055 | 740 |
Goal "x ~= 0 ==> x * x ~= (0::hypreal)"; |
7218 | 741 |
by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1); |
742 |
qed "hypreal_mult_self_not_zero"; |
|
743 |
||
10607 | 744 |
Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)"; |
7218 | 745 |
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); |
746 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym, |
|
747 |
hypreal_mult_not_0])); |
|
748 |
by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1); |
|
749 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac)); |
|
750 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0])); |
|
10607 | 751 |
qed "inverse_mult_eq"; |
7218 | 752 |
|
10607 | 753 |
Goal "x ~= 0 ==> inverse(-x) = -inverse(x::hypreal)"; |
9055 | 754 |
by (rtac (hypreal_mult_right_cancel RS iffD1) 1); |
10607 | 755 |
by (stac hypreal_mult_inverse_left 2); |
7218 | 756 |
by Auto_tac; |
10607 | 757 |
qed "hypreal_minus_inverse"; |
7218 | 758 |
|
9055 | 759 |
Goal "[| x ~= 0; y ~= 0 |] \ |
10607 | 760 |
\ ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)"; |
7218 | 761 |
by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1); |
762 |
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
763 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym])); |
|
764 |
by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
765 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute])); |
|
766 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
10607 | 767 |
qed "hypreal_inverse_distrib"; |
7218 | 768 |
|
769 |
(*------------------------------------------------------------------ |
|
770 |
Theorems for ordering |
|
771 |
------------------------------------------------------------------*) |
|
772 |
||
773 |
(* prove introduction and elimination rules for hypreal_less *) |
|
774 |
||
775 |
Goalw [hypreal_less_def] |
|
776 |
"P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \ |
|
777 |
\ Y : Rep_hypreal(Q) & \ |
|
778 |
\ {n. X n < Y n} : FreeUltrafilterNat)"; |
|
779 |
by (Fast_tac 1); |
|
780 |
qed "hypreal_less_iff"; |
|
781 |
||
782 |
Goalw [hypreal_less_def] |
|
783 |
"[| {n. X n < Y n} : FreeUltrafilterNat; \ |
|
784 |
\ X : Rep_hypreal(P); \ |
|
785 |
\ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)"; |
|
786 |
by (Fast_tac 1); |
|
787 |
qed "hypreal_lessI"; |
|
788 |
||
789 |
||
790 |
Goalw [hypreal_less_def] |
|
791 |
"!! R1. [| R1 < (R2::hypreal); \ |
|
792 |
\ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \ |
|
793 |
\ !!X. X : Rep_hypreal(R1) ==> P; \ |
|
794 |
\ !!Y. Y : Rep_hypreal(R2) ==> P |] \ |
|
795 |
\ ==> P"; |
|
796 |
by Auto_tac; |
|
797 |
qed "hypreal_lessE"; |
|
798 |
||
799 |
Goalw [hypreal_less_def] |
|
800 |
"R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ |
|
801 |
\ X : Rep_hypreal(R1) & \ |
|
802 |
\ Y : Rep_hypreal(R2))"; |
|
803 |
by (Fast_tac 1); |
|
804 |
qed "hypreal_lessD"; |
|
805 |
||
806 |
Goal "~ (R::hypreal) < R"; |
|
807 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
808 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); |
|
809 |
by (Ultra_tac 1); |
|
810 |
qed "hypreal_less_not_refl"; |
|
811 |
||
812 |
(*** y < y ==> P ***) |
|
813 |
bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE); |
|
10043 | 814 |
AddSEs [hypreal_less_irrefl]; |
7218 | 815 |
|
816 |
Goal "!!(x::hypreal). x < y ==> x ~= y"; |
|
817 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl])); |
|
818 |
qed "hypreal_not_refl2"; |
|
819 |
||
820 |
Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; |
|
821 |
by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1); |
|
822 |
by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1); |
|
823 |
by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1); |
|
824 |
by (auto_tac (claset() addSIs [exI],simpset() |
|
825 |
addsimps [hypreal_less_def])); |
|
826 |
by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1); |
|
827 |
qed "hypreal_less_trans"; |
|
828 |
||
829 |
Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"; |
|
830 |
by (dtac hypreal_less_trans 1 THEN assume_tac 1); |
|
831 |
by (asm_full_simp_tac (simpset() addsimps |
|
832 |
[hypreal_less_not_refl]) 1); |
|
833 |
qed "hypreal_less_asym"; |
|
834 |
||
10043 | 835 |
(*------------------------------------------------------- |
7218 | 836 |
TODO: The following theorem should have been proved |
837 |
first and then used througout the proofs as it probably |
|
838 |
makes many of them more straightforward. |
|
839 |
-------------------------------------------------------*) |
|
840 |
Goalw [hypreal_less_def] |
|
841 |
"(Abs_hypreal(hyprel^^{%n. X n}) < \ |
|
842 |
\ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
843 |
\ ({n. X n < Y n} : FreeUltrafilterNat)"; |
|
844 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset())); |
|
845 |
by (Ultra_tac 1); |
|
846 |
qed "hypreal_less"; |
|
847 |
||
848 |
(*--------------------------------------------------------------------------------- |
|
849 |
Hyperreals as a linearly ordered field |
|
850 |
---------------------------------------------------------------------------------*) |
|
10607 | 851 |
(*** sum order |
7218 | 852 |
Goalw [hypreal_zero_def] |
9055 | 853 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"; |
7218 | 854 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
855 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
856 |
by (auto_tac (claset(),simpset() addsimps |
|
857 |
[hypreal_less_def,hypreal_add])); |
|
858 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
859 |
[hypreal_less_def,hypreal_add])); |
|
860 |
by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); |
|
861 |
qed "hypreal_add_order"; |
|
10607 | 862 |
***) |
7218 | 863 |
|
10607 | 864 |
(*** mult order |
7218 | 865 |
Goalw [hypreal_zero_def] |
9055 | 866 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"; |
7218 | 867 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
868 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
869 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
870 |
[hypreal_less_def,hypreal_mult])); |
|
9432 | 871 |
by (ultra_tac (claset() addIs [rename_numerals real_mult_order], |
9071 | 872 |
simpset()) 1); |
7218 | 873 |
qed "hypreal_mult_order"; |
10043 | 874 |
****) |
875 |
||
7218 | 876 |
|
877 |
(*--------------------------------------------------------------------------------- |
|
878 |
Trichotomy of the hyperreals |
|
879 |
--------------------------------------------------------------------------------*) |
|
880 |
||
9055 | 881 |
Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
882 |
by (res_inst_tac [("x","%n. #0")] exI 1); |
7218 | 883 |
by (Step_tac 1); |
884 |
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset())); |
|
885 |
qed "lemma_hyprel_0r_mem"; |
|
886 |
||
9055 | 887 |
Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)"; |
7218 | 888 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
889 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); |
|
890 |
by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1); |
|
891 |
by (dres_inst_tac [("x","xa")] spec 1); |
|
892 |
by (dres_inst_tac [("x","x")] spec 1); |
|
893 |
by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1); |
|
894 |
by Auto_tac; |
|
895 |
by (dres_inst_tac [("x","x")] spec 1); |
|
896 |
by (dres_inst_tac [("x","xa")] spec 1); |
|
897 |
by Auto_tac; |
|
898 |
by (Ultra_tac 1); |
|
899 |
by (auto_tac (claset() addIs [real_linear_less2],simpset())); |
|
900 |
qed "hypreal_trichotomy"; |
|
901 |
||
9055 | 902 |
val prems = Goal "[| (0::hypreal) < x ==> P; \ |
903 |
\ x = 0 ==> P; \ |
|
904 |
\ x < 0 ==> P |] ==> P"; |
|
7218 | 905 |
by (cut_inst_tac [("x","x")] hypreal_trichotomy 1); |
906 |
by (REPEAT (eresolve_tac (disjE::prems) 1)); |
|
907 |
qed "hypreal_trichotomyE"; |
|
908 |
||
909 |
(*---------------------------------------------------------------------------- |
|
910 |
More properties of < |
|
911 |
----------------------------------------------------------------------------*) |
|
912 |
||
9055 | 913 |
Goal "((x::hypreal) < y) = (0 < y + -x)"; |
10043 | 914 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
915 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
916 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
917 |
hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
918 |
by (ALLGOALS(Ultra_tac)); |
|
7218 | 919 |
qed "hypreal_less_minus_iff"; |
920 |
||
10043 | 921 |
Goal "((x::hypreal) < y) = (x + -y < 0)"; |
922 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
923 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
924 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
925 |
hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
926 |
by (ALLGOALS(Ultra_tac)); |
|
7218 | 927 |
qed "hypreal_less_minus_iff2"; |
928 |
||
9055 | 929 |
Goal "((x::hypreal) = y) = (0 = x + - y)"; |
7218 | 930 |
by Auto_tac; |
931 |
by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); |
|
932 |
by Auto_tac; |
|
933 |
qed "hypreal_eq_minus_iff"; |
|
934 |
||
9055 | 935 |
Goal "((x::hypreal) = y) = (0 = y + - x)"; |
7218 | 936 |
by Auto_tac; |
937 |
by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1); |
|
938 |
by Auto_tac; |
|
939 |
qed "hypreal_eq_minus_iff2"; |
|
940 |
||
10043 | 941 |
(* 07/00 *) |
942 |
Goal "(0::hypreal) - x = -x"; |
|
943 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
944 |
qed "hypreal_diff_zero"; |
|
945 |
||
946 |
Goal "x - (0::hypreal) = x"; |
|
947 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
948 |
qed "hypreal_diff_zero_right"; |
|
949 |
||
950 |
Goal "x - x = (0::hypreal)"; |
|
951 |
by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
952 |
qed "hypreal_diff_self"; |
|
953 |
||
954 |
Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self]; |
|
955 |
||
7218 | 956 |
Goal "(x = y + z) = (x + -z = (y::hypreal))"; |
957 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
958 |
qed "hypreal_eq_minus_iff3"; |
|
959 |
||
960 |
Goal "(x = z + y) = (x + -z = (y::hypreal))"; |
|
961 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
962 |
qed "hypreal_eq_minus_iff4"; |
|
963 |
||
9055 | 964 |
Goal "(x ~= a) = (x + -a ~= (0::hypreal))"; |
7218 | 965 |
by (auto_tac (claset() addDs [sym RS |
966 |
(hypreal_eq_minus_iff RS iffD2)],simpset())); |
|
967 |
qed "hypreal_not_eq_minus_iff"; |
|
968 |
||
969 |
(*** linearity ***) |
|
970 |
Goal "(x::hypreal) < y | x = y | y < x"; |
|
7322 | 971 |
by (stac hypreal_eq_minus_iff2 1); |
7218 | 972 |
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
973 |
by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1); |
|
974 |
by (rtac hypreal_trichotomyE 1); |
|
975 |
by Auto_tac; |
|
976 |
qed "hypreal_linear"; |
|
977 |
||
10043 | 978 |
Goal "((w::hypreal) ~= z) = (w<z | z<w)"; |
979 |
by (cut_facts_tac [hypreal_linear] 1); |
|
980 |
by (Blast_tac 1); |
|
981 |
qed "hypreal_neq_iff"; |
|
982 |
||
7218 | 983 |
Goal "!!(x::hypreal). [| x < y ==> P; x = y ==> P; \ |
984 |
\ y < x ==> P |] ==> P"; |
|
985 |
by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1); |
|
986 |
by Auto_tac; |
|
987 |
qed "hypreal_linear_less2"; |
|
988 |
||
989 |
(*------------------------------------------------------------------------------ |
|
990 |
Properties of <= |
|
991 |
------------------------------------------------------------------------------*) |
|
992 |
(*------ hypreal le iff reals le a.e ------*) |
|
993 |
||
994 |
Goalw [hypreal_le_def,real_le_def] |
|
995 |
"(Abs_hypreal(hyprel^^{%n. X n}) <= \ |
|
996 |
\ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
997 |
\ ({n. X n <= Y n} : FreeUltrafilterNat)"; |
|
998 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less])); |
|
999 |
by (ALLGOALS(Ultra_tac)); |
|
1000 |
qed "hypreal_le"; |
|
1001 |
||
1002 |
(*---------------------------------------------------------*) |
|
1003 |
(*---------------------------------------------------------*) |
|
1004 |
Goalw [hypreal_le_def] |
|
1005 |
"~(w < z) ==> z <= (w::hypreal)"; |
|
1006 |
by (assume_tac 1); |
|
1007 |
qed "hypreal_leI"; |
|
1008 |
||
1009 |
Goalw [hypreal_le_def] |
|
1010 |
"z<=w ==> ~(w<(z::hypreal))"; |
|
1011 |
by (assume_tac 1); |
|
1012 |
qed "hypreal_leD"; |
|
1013 |
||
9108 | 1014 |
bind_thm ("hypreal_leE", make_elim hypreal_leD); |
7218 | 1015 |
|
1016 |
Goal "(~(w < z)) = (z <= (w::hypreal))"; |
|
1017 |
by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1); |
|
1018 |
qed "hypreal_less_le_iff"; |
|
1019 |
||
1020 |
Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)"; |
|
1021 |
by (Fast_tac 1); |
|
1022 |
qed "not_hypreal_leE"; |
|
1023 |
||
1024 |
Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)"; |
|
1025 |
by (fast_tac (claset() addEs [hypreal_less_asym]) 1); |
|
1026 |
qed "hypreal_less_imp_le"; |
|
1027 |
||
1028 |
Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y"; |
|
1029 |
by (cut_facts_tac [hypreal_linear] 1); |
|
1030 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
1031 |
qed "hypreal_le_imp_less_or_eq"; |
|
1032 |
||
1033 |
Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)"; |
|
1034 |
by (cut_facts_tac [hypreal_linear] 1); |
|
1035 |
by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
1036 |
qed "hypreal_less_or_eq_imp_le"; |
|
1037 |
||
1038 |
Goal "(x <= (y::hypreal)) = (x < y | x=y)"; |
|
1039 |
by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1)); |
|
1040 |
qed "hypreal_le_eq_less_or_eq"; |
|
10043 | 1041 |
val hypreal_le_less = hypreal_le_eq_less_or_eq; |
7218 | 1042 |
|
1043 |
Goal "w <= (w::hypreal)"; |
|
1044 |
by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1); |
|
1045 |
qed "hypreal_le_refl"; |
|
1046 |
Addsimps [hypreal_le_refl]; |
|
1047 |
||
10043 | 1048 |
(* Axiom 'linorder_linear' of class 'linorder': *) |
1049 |
Goal "(z::hypreal) <= w | w <= z"; |
|
1050 |
by (simp_tac (simpset() addsimps [hypreal_le_less]) 1); |
|
1051 |
by (cut_facts_tac [hypreal_linear] 1); |
|
1052 |
by (Blast_tac 1); |
|
1053 |
qed "hypreal_le_linear"; |
|
1054 |
||
7218 | 1055 |
Goal "[| i <= j; j < k |] ==> i < (k::hypreal)"; |
1056 |
by (dtac hypreal_le_imp_less_or_eq 1); |
|
1057 |
by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1058 |
qed "hypreal_le_less_trans"; |
|
1059 |
||
1060 |
Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k"; |
|
1061 |
by (dtac hypreal_le_imp_less_or_eq 1); |
|
1062 |
by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1063 |
qed "hypreal_less_le_trans"; |
|
1064 |
||
1065 |
Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)"; |
|
1066 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1067 |
rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]); |
|
1068 |
qed "hypreal_le_trans"; |
|
1069 |
||
1070 |
Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; |
|
1071 |
by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1072 |
fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); |
|
1073 |
qed "hypreal_le_anti_sym"; |
|
1074 |
||
1075 |
Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; |
|
1076 |
by (rtac not_hypreal_leE 1); |
|
1077 |
by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); |
|
1078 |
qed "not_less_not_eq_hypreal_less"; |
|
1079 |
||
10043 | 1080 |
(* Axiom 'order_less_le' of class 'order': *) |
1081 |
Goal "(w::hypreal) < z = (w <= z & w ~= z)"; |
|
1082 |
by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1); |
|
1083 |
by (blast_tac (claset() addIs [hypreal_less_asym]) 1); |
|
1084 |
qed "hypreal_less_le"; |
|
1085 |
||
9055 | 1086 |
Goal "(0 < -R) = (R < (0::hypreal))"; |
10043 | 1087 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
1088 |
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
|
1089 |
hypreal_less,hypreal_minus])); |
|
7218 | 1090 |
qed "hypreal_minus_zero_less_iff"; |
10043 | 1091 |
Addsimps [hypreal_minus_zero_less_iff]; |
7218 | 1092 |
|
9055 | 1093 |
Goal "(-R < 0) = ((0::hypreal) < R)"; |
10043 | 1094 |
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
1095 |
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
|
1096 |
hypreal_less,hypreal_minus])); |
|
1097 |
by (ALLGOALS(Ultra_tac)); |
|
7218 | 1098 |
qed "hypreal_minus_zero_less_iff2"; |
1099 |
||
10043 | 1100 |
Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))"; |
1101 |
by (simp_tac (simpset() addsimps |
|
1102 |
[hypreal_minus_zero_less_iff2]) 1); |
|
1103 |
qed "hypreal_minus_zero_le_iff"; |
|
7218 | 1104 |
|
1105 |
(*---------------------------------------------------------- |
|
1106 |
hypreal_of_real preserves field and order properties |
|
1107 |
-----------------------------------------------------------*) |
|
1108 |
Goalw [hypreal_of_real_def] |
|
9071 | 1109 |
"hypreal_of_real (z1 + z2) = \ |
1110 |
\ hypreal_of_real z1 + hypreal_of_real z2"; |
|
7218 | 1111 |
by (asm_simp_tac (simpset() addsimps [hypreal_add, |
1112 |
hypreal_add_mult_distrib]) 1); |
|
1113 |
qed "hypreal_of_real_add"; |
|
1114 |
||
1115 |
Goalw [hypreal_of_real_def] |
|
9071 | 1116 |
"hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2"; |
7218 | 1117 |
by (full_simp_tac (simpset() addsimps [hypreal_mult, |
1118 |
hypreal_add_mult_distrib2]) 1); |
|
1119 |
qed "hypreal_of_real_mult"; |
|
1120 |
||
1121 |
Goalw [hypreal_less_def,hypreal_of_real_def] |
|
1122 |
"(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)"; |
|
1123 |
by Auto_tac; |
|
1124 |
by (res_inst_tac [("x","%n. z1")] exI 1); |
|
1125 |
by (Step_tac 1); |
|
1126 |
by (res_inst_tac [("x","%n. z2")] exI 2); |
|
1127 |
by Auto_tac; |
|
1128 |
by (rtac FreeUltrafilterNat_P 1); |
|
1129 |
by (Ultra_tac 1); |
|
1130 |
qed "hypreal_of_real_less_iff"; |
|
1131 |
||
1132 |
Addsimps [hypreal_of_real_less_iff RS sym]; |
|
1133 |
||
1134 |
Goalw [hypreal_le_def,real_le_def] |
|
1135 |
"(z1 <= z2) = (hypreal_of_real z1 <= hypreal_of_real z2)"; |
|
1136 |
by Auto_tac; |
|
1137 |
qed "hypreal_of_real_le_iff"; |
|
1138 |
||
1139 |
Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r"; |
|
1140 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus])); |
|
1141 |
qed "hypreal_of_real_minus"; |
|
1142 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
1143 |
Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real #1 = 1hr"; |
7218 | 1144 |
by (Step_tac 1); |
1145 |
qed "hypreal_of_real_one"; |
|
1146 |
||
9055 | 1147 |
Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0"; |
7218 | 1148 |
by (Step_tac 1); |
1149 |
qed "hypreal_of_real_zero"; |
|
1150 |
||
9055 | 1151 |
Goal "(hypreal_of_real r = 0) = (r = #0)"; |
7218 | 1152 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_P], |
1153 |
simpset() addsimps [hypreal_of_real_def, |
|
1154 |
hypreal_zero_def,FreeUltrafilterNat_Nat_set])); |
|
1155 |
qed "hypreal_of_real_zero_iff"; |
|
1156 |
||
9055 | 1157 |
Goal "(hypreal_of_real r ~= 0) = (r ~= #0)"; |
7218 | 1158 |
by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1); |
1159 |
qed "hypreal_of_real_not_zero_iff"; |
|
1160 |
||
10607 | 1161 |
Goal "r ~= #0 ==> inverse (hypreal_of_real r) = \ |
1162 |
\ hypreal_of_real (inverse r)"; |
|
7218 | 1163 |
by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1); |
1164 |
by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1); |
|
1165 |
by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1); |
|
1166 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one])); |
|
10607 | 1167 |
qed "hypreal_of_real_inverse"; |
7218 | 1168 |
|
10607 | 1169 |
Goal "hypreal_of_real r ~= 0 ==> inverse (hypreal_of_real r) = \ |
1170 |
\ hypreal_of_real (inverse r)"; |
|
1171 |
by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_inverse) 1); |
|
1172 |
qed "hypreal_of_real_inverse2"; |
|
7218 | 1173 |
|
1174 |
Goal "x+x=x*(1hr+1hr)"; |
|
1175 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); |
|
1176 |
qed "hypreal_add_self"; |
|
1177 |
||
10607 | 1178 |
Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)"; |
7218 | 1179 |
by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1); |
1180 |
qed "lemma_chain"; |
|
1181 |
||
10607 | 1182 |
Goal "[|(x::hypreal) ~= 0; y ~= 0 |] ==> \ |
1183 |
\ inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; |
|
1184 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib, |
|
7218 | 1185 |
hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); |
7322 | 1186 |
by (stac hypreal_mult_assoc 1); |
7218 | 1187 |
by (rtac (hypreal_mult_left_commute RS subst) 1); |
1188 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
10607 | 1189 |
qed "hypreal_inverse_add"; |
7218 | 1190 |
|
9055 | 1191 |
Goal "x = -x ==> x = (0::hypreal)"; |
10043 | 1192 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1193 |
by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
1194 |
hypreal_zero_def])); |
|
1195 |
by (Ultra_tac 1); |
|
7218 | 1196 |
qed "hypreal_self_eq_minus_self_zero"; |
1197 |
||
9055 | 1198 |
Goal "(x + x = 0) = (x = (0::hypreal))"; |
10043 | 1199 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1200 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
1201 |
hypreal_zero_def])); |
|
7218 | 1202 |
qed "hypreal_add_self_zero_cancel"; |
1203 |
Addsimps [hypreal_add_self_zero_cancel]; |
|
1204 |
||
9055 | 1205 |
Goal "(x + x + y = y) = (x = (0::hypreal))"; |
7218 | 1206 |
by Auto_tac; |
1207 |
by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1); |
|
1208 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1209 |
qed "hypreal_add_self_zero_cancel2"; |
|
1210 |
Addsimps [hypreal_add_self_zero_cancel2]; |
|
1211 |
||
9055 | 1212 |
Goal "(x + (x + y) = y) = (x = (0::hypreal))"; |
7218 | 1213 |
by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
1214 |
qed "hypreal_add_self_zero_cancel2a"; |
|
1215 |
Addsimps [hypreal_add_self_zero_cancel2a]; |
|
1216 |
||
1217 |
Goal "(b = -a) = (-b = (a::hypreal))"; |
|
1218 |
by Auto_tac; |
|
1219 |
qed "hypreal_minus_eq_swap"; |
|
1220 |
||
1221 |
Goal "(-b = -a) = (b = (a::hypreal))"; |
|
1222 |
by (asm_full_simp_tac (simpset() addsimps |
|
1223 |
[hypreal_minus_eq_swap]) 1); |
|
1224 |
qed "hypreal_minus_eq_cancel"; |
|
1225 |
Addsimps [hypreal_minus_eq_cancel]; |
|
1226 |
||
1227 |
Goal "x < x + 1hr"; |
|
10043 | 1228 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1229 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
1230 |
hypreal_one_def,hypreal_less])); |
|
7218 | 1231 |
qed "hypreal_less_self_add_one"; |
1232 |
Addsimps [hypreal_less_self_add_one]; |
|
1233 |
||
1234 |
Goal "((x::hypreal) + x = y + y) = (x = y)"; |
|
10043 | 1235 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1236 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1237 |
by (auto_tac (claset(),simpset() addsimps [hypreal_add])); |
|
1238 |
by (ALLGOALS(Ultra_tac)); |
|
7218 | 1239 |
qed "hypreal_add_self_cancel"; |
1240 |
Addsimps [hypreal_add_self_cancel]; |
|
1241 |
||
1242 |
Goal "(y = x + - y + x) = (y = (x::hypreal))"; |
|
1243 |
by Auto_tac; |
|
1244 |
by (dres_inst_tac [("x1","y")] |
|
1245 |
(hypreal_add_right_cancel RS iffD2) 1); |
|
1246 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1247 |
qed "hypreal_add_self_minus_cancel"; |
|
1248 |
Addsimps [hypreal_add_self_minus_cancel]; |
|
1249 |
||
1250 |
Goal "(y = x + (- y + x)) = (y = (x::hypreal))"; |
|
1251 |
by (asm_full_simp_tac (simpset() addsimps |
|
1252 |
[hypreal_add_assoc RS sym])1); |
|
1253 |
qed "hypreal_add_self_minus_cancel2"; |
|
1254 |
Addsimps [hypreal_add_self_minus_cancel2]; |
|
1255 |
||
10043 | 1256 |
(* of course, can prove this by "transfer" as well *) |
7218 | 1257 |
Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
1258 |
by Auto_tac; |
|
1259 |
by (dres_inst_tac [("x1","z")] |
|
1260 |
(hypreal_add_right_cancel RS iffD2) 1); |
|
1261 |
by (asm_full_simp_tac (simpset() addsimps |
|
10043 | 1262 |
[hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
1263 |
delsimps [hypreal_minus_add_distrib]) 1); |
|
7218 | 1264 |
by (asm_full_simp_tac (simpset() addsimps |
1265 |
[hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
|
1266 |
qed "hypreal_add_self_minus_cancel3"; |
|
1267 |
Addsimps [hypreal_add_self_minus_cancel3]; |
|
1268 |
||
9055 | 1269 |
Goal "(x * x = 0) = (x = (0::hypreal))"; |
7218 | 1270 |
by Auto_tac; |
1271 |
by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1); |
|
1272 |
qed "hypreal_mult_self_eq_zero_iff"; |
|
1273 |
Addsimps [hypreal_mult_self_eq_zero_iff]; |
|
1274 |
||
9055 | 1275 |
Goal "(0 = x * x) = (x = (0::hypreal))"; |
7218 | 1276 |
by (auto_tac (claset() addDs [sym],simpset())); |
1277 |
qed "hypreal_mult_self_eq_zero_iff2"; |
|
1278 |
Addsimps [hypreal_mult_self_eq_zero_iff2]; |
|
1279 |
||
10043 | 1280 |
Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))"; |
1281 |
by (rtac hypreal_less_minus_iff2 1); |
|
1282 |
qed "hypreal_less_eq_diff"; |
|
7218 | 1283 |
|
10043 | 1284 |
(*** Subtraction laws ***) |
7218 | 1285 |
|
10043 | 1286 |
Goal "x + (y - z) = (x + y) - (z::hypreal)"; |
1287 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1288 |
qed "hypreal_add_diff_eq"; |
|
7218 | 1289 |
|
10043 | 1290 |
Goal "(x - y) + z = (x + z) - (y::hypreal)"; |
1291 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1292 |
qed "hypreal_diff_add_eq"; |
|
7218 | 1293 |
|
10043 | 1294 |
Goal "(x - y) - z = x - (y + (z::hypreal))"; |
1295 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1296 |
qed "hypreal_diff_diff_eq"; |
|
7218 | 1297 |
|
10043 | 1298 |
Goal "x - (y - z) = (x + z) - (y::hypreal)"; |
1299 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1300 |
qed "hypreal_diff_diff_eq2"; |
|
7218 | 1301 |
|
10043 | 1302 |
Goal "(x-y < z) = (x < z + (y::hypreal))"; |
1303 |
by (stac hypreal_less_eq_diff 1); |
|
1304 |
by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1305 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1306 |
qed "hypreal_diff_less_eq"; |
|
7218 | 1307 |
|
10043 | 1308 |
Goal "(x < z-y) = (x + (y::hypreal) < z)"; |
1309 |
by (stac hypreal_less_eq_diff 1); |
|
1310 |
by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1311 |
by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1312 |
qed "hypreal_less_diff_eq"; |
|
7218 | 1313 |
|
10043 | 1314 |
Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))"; |
1315 |
by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1); |
|
1316 |
qed "hypreal_diff_le_eq"; |
|
7218 | 1317 |
|
10043 | 1318 |
Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)"; |
1319 |
by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); |
|
1320 |
qed "hypreal_le_diff_eq"; |
|
7218 | 1321 |
|
10043 | 1322 |
Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))"; |
1323 |
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
|
1324 |
qed "hypreal_diff_eq_eq"; |
|
7218 | 1325 |
|
10043 | 1326 |
Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)"; |
1327 |
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
|
1328 |
qed "hypreal_eq_diff_eq"; |
|
7218 | 1329 |
|
10043 | 1330 |
(*This list of rewrites simplifies (in)equalities by bringing subtractions |
1331 |
to the top and then moving negative terms to the other side. |
|
1332 |
Use with hypreal_add_ac*) |
|
1333 |
val hypreal_compare_rls = |
|
1334 |
[symmetric hypreal_diff_def, |
|
1335 |
hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, hypreal_diff_diff_eq2, |
|
1336 |
hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, hypreal_le_diff_eq, |
|
1337 |
hypreal_diff_eq_eq, hypreal_eq_diff_eq]; |
|
7218 | 1338 |
|
1339 |
||
10043 | 1340 |
(** For the cancellation simproc. |
1341 |
The idea is to cancel like terms on opposite sides by subtraction **) |
|
7218 | 1342 |
|
10043 | 1343 |
Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')"; |
1344 |
by (stac hypreal_less_eq_diff 1); |
|
1345 |
by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1346 |
by (Asm_simp_tac 1); |
|
1347 |
qed "hypreal_less_eqI"; |
|
7218 | 1348 |
|
10043 | 1349 |
Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')"; |
1350 |
by (dtac hypreal_less_eqI 1); |
|
1351 |
by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1); |
|
1352 |
qed "hypreal_le_eqI"; |
|
7218 | 1353 |
|
10043 | 1354 |
Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"; |
1355 |
by Safe_tac; |
|
1356 |
by (ALLGOALS |
|
1357 |
(asm_full_simp_tac |
|
1358 |
(simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq]))); |
|
1359 |
qed "hypreal_eq_eqI"; |
|
7218 | 1360 |