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