author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 21210 | c17fd2df4e9e |
child 21588 | cd0dc678a205 |
permissions | -rw-r--r-- |
20245 | 1 |
(* Title : HOL/Hyperreal/HyperDef.thy |
10751 | 2 |
ID : $Id$ |
3 |
Author : Jacques D. Fleuriot |
|
4 |
Copyright : 1998 University of Cambridge |
|
14468 | 5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13487 | 6 |
*) |
10751 | 7 |
|
14468 | 8 |
header{*Construction of Hyperreals Using Ultrafilters*} |
9 |
||
15131 | 10 |
theory HyperDef |
17298 | 11 |
imports StarClasses "../Real/Real" |
16417 | 12 |
uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*) |
15131 | 13 |
begin |
10751 | 14 |
|
17298 | 15 |
types hypreal = "real star" |
14299 | 16 |
|
19380 | 17 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
18 |
hypreal_of_real :: "real => real star" where |
19380 | 19 |
"hypreal_of_real == star_of" |
10751 | 20 |
|
19765 | 21 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
22 |
omega :: hypreal where -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
19765 | 23 |
"omega = star_n (%n. real (Suc n))" |
13487 | 24 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
25 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
26 |
epsilon :: hypreal where -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
19765 | 27 |
"epsilon = star_n (%n. inverse (real (Suc n)))" |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
28 |
|
21210 | 29 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
30 |
omega ("\<omega>") and |
19765 | 31 |
epsilon ("\<epsilon>") |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
32 |
|
21210 | 33 |
notation (HTML output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
34 |
omega ("\<omega>") and |
19765 | 35 |
epsilon ("\<epsilon>") |
14565 | 36 |
|
14329 | 37 |
|
20555 | 38 |
subsection {* Real vector class instances *} |
39 |
||
40 |
instance star :: (scaleR) scaleR .. |
|
41 |
||
42 |
defs (overloaded) |
|
43 |
star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)" |
|
44 |
||
20726 | 45 |
lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> r *# x \<in> Standard" |
46 |
by (simp add: star_scaleR_def) |
|
47 |
||
48 |
lemma star_of_scaleR [simp]: "star_of (r *# x) = r *# star_of x" |
|
49 |
by transfer (rule refl) |
|
50 |
||
20555 | 51 |
instance star :: (real_vector) real_vector |
52 |
proof |
|
53 |
fix a b :: real |
|
54 |
show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y" |
|
55 |
by transfer (rule scaleR_right_distrib) |
|
56 |
show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x" |
|
57 |
by transfer (rule scaleR_left_distrib) |
|
20765 | 58 |
show "\<And>x::'a star. a *# b *# x = (a * b) *# x" |
59 |
by transfer (rule scaleR_scaleR) |
|
20555 | 60 |
show "\<And>x::'a star. 1 *# x = x" |
61 |
by transfer (rule scaleR_one) |
|
62 |
qed |
|
63 |
||
64 |
instance star :: (real_algebra) real_algebra |
|
65 |
proof |
|
66 |
fix a :: real |
|
67 |
show "\<And>x y::'a star. a *# x * y = a *# (x * y)" |
|
68 |
by transfer (rule mult_scaleR_left) |
|
69 |
show "\<And>x y::'a star. x * a *# y = a *# (x * y)" |
|
70 |
by transfer (rule mult_scaleR_right) |
|
71 |
qed |
|
72 |
||
73 |
instance star :: (real_algebra_1) real_algebra_1 .. |
|
74 |
||
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
75 |
instance star :: (real_div_algebra) real_div_algebra .. |
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
76 |
|
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
77 |
instance star :: (real_field) real_field .. |
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
78 |
|
20726 | 79 |
lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)" |
80 |
by (unfold of_real_def, transfer, rule refl) |
|
81 |
||
82 |
lemma Standard_of_real [simp]: "of_real r \<in> Standard" |
|
83 |
by (simp add: star_of_real_def) |
|
20555 | 84 |
|
85 |
lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
|
86 |
by transfer (rule refl) |
|
87 |
||
20729 | 88 |
lemma of_real_eq_star_of [simp]: "of_real = star_of" |
89 |
proof |
|
90 |
fix r :: real |
|
91 |
show "of_real r = star_of r" |
|
92 |
by transfer simp |
|
93 |
qed |
|
94 |
||
95 |
lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard" |
|
20765 | 96 |
by (simp add: Reals_def Standard_def) |
20729 | 97 |
|
20555 | 98 |
|
14329 | 99 |
subsection{*Existence of Free Ultrafilter over the Naturals*} |
100 |
||
101 |
text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
|
102 |
an arbitrary free ultrafilter*} |
|
14299 | 103 |
|
17290 | 104 |
lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
105 |
by (rule nat_infinite [THEN freeultrafilter_Ex]) |
14299 | 106 |
|
17298 | 107 |
lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat" |
14299 | 108 |
apply (unfold FreeUltrafilterNat_def) |
17290 | 109 |
apply (rule someI_ex) |
110 |
apply (rule FreeUltrafilterNat_Ex) |
|
14299 | 111 |
done |
112 |
||
17290 | 113 |
lemma UltrafilterNat_mem: "ultrafilter FreeUltrafilterNat" |
114 |
by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.ultrafilter]) |
|
115 |
||
116 |
lemma FilterNat_mem: "filter FreeUltrafilterNat" |
|
117 |
by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter]) |
|
118 |
||
14299 | 119 |
lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat" |
17290 | 120 |
by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite]) |
14299 | 121 |
|
14705 | 122 |
lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x" |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19765
diff
changeset
|
123 |
thm FreeUltrafilterNat_mem |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19765
diff
changeset
|
124 |
thm freeultrafilter.infinite |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19765
diff
changeset
|
125 |
thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite] |
17290 | 126 |
by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]) |
14299 | 127 |
|
14301 | 128 |
lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat" |
17290 | 129 |
by (rule FilterNat_mem [THEN filter.empty]) |
14299 | 130 |
|
14329 | 131 |
lemma FreeUltrafilterNat_Int: |
14705 | 132 |
"[| X \<in> FreeUltrafilterNat; Y \<in> FreeUltrafilterNat |] |
14299 | 133 |
==> X Int Y \<in> FreeUltrafilterNat" |
17290 | 134 |
by (rule FilterNat_mem [THEN filter.Int]) |
14299 | 135 |
|
14329 | 136 |
lemma FreeUltrafilterNat_subset: |
14705 | 137 |
"[| X \<in> FreeUltrafilterNat; X \<subseteq> Y |] |
14299 | 138 |
==> Y \<in> FreeUltrafilterNat" |
17290 | 139 |
by (rule FilterNat_mem [THEN filter.subset]) |
14299 | 140 |
|
14329 | 141 |
lemma FreeUltrafilterNat_Compl: |
14705 | 142 |
"X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
17290 | 143 |
apply (erule contrapos_pn) |
144 |
apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2]) |
|
145 |
done |
|
14299 | 146 |
|
14329 | 147 |
lemma FreeUltrafilterNat_Compl_mem: |
148 |
"X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
|
17290 | 149 |
by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1]) |
14299 | 150 |
|
14329 | 151 |
lemma FreeUltrafilterNat_Compl_iff1: |
14705 | 152 |
"(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)" |
17290 | 153 |
by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff]) |
14299 | 154 |
|
14329 | 155 |
lemma FreeUltrafilterNat_Compl_iff2: |
14705 | 156 |
"(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
14301 | 157 |
by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
14299 | 158 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
159 |
lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
160 |
apply (drule FreeUltrafilterNat_finite) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
161 |
apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric]) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
162 |
done |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
163 |
|
15539 | 164 |
lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat" |
17290 | 165 |
by (rule FilterNat_mem [THEN filter.UNIV]) |
14299 | 166 |
|
14329 | 167 |
lemma FreeUltrafilterNat_Nat_set_refl [intro]: |
168 |
"{n. P(n) = P(n)} \<in> FreeUltrafilterNat" |
|
14301 | 169 |
by simp |
14299 | 170 |
|
171 |
lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P" |
|
14301 | 172 |
by (rule ccontr, simp) |
14299 | 173 |
|
174 |
lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)" |
|
14301 | 175 |
by (rule ccontr, simp) |
14299 | 176 |
|
177 |
lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat" |
|
15539 | 178 |
by (auto) |
14299 | 179 |
|
14329 | 180 |
|
181 |
text{*Define and use Ultrafilter tactics*} |
|
14299 | 182 |
use "fuf.ML" |
183 |
||
184 |
method_setup fuf = {* |
|
185 |
Method.ctxt_args (fn ctxt => |
|
186 |
Method.METHOD (fn facts => |
|
15032 | 187 |
fuf_tac (local_clasimpset_of ctxt) 1)) *} |
14299 | 188 |
"free ultrafilter tactic" |
189 |
||
190 |
method_setup ultra = {* |
|
191 |
Method.ctxt_args (fn ctxt => |
|
192 |
Method.METHOD (fn facts => |
|
15032 | 193 |
ultra_tac (local_clasimpset_of ctxt) 1)) *} |
14299 | 194 |
"ultrafilter tactic" |
195 |
||
196 |
||
14329 | 197 |
text{*One further property of our free ultrafilter*} |
198 |
lemma FreeUltrafilterNat_Un: |
|
14705 | 199 |
"X Un Y \<in> FreeUltrafilterNat |
200 |
==> X \<in> FreeUltrafilterNat | Y \<in> FreeUltrafilterNat" |
|
201 |
by (auto, ultra) |
|
14299 | 202 |
|
203 |
||
17298 | 204 |
subsection{*Properties of @{term starrel}*} |
14329 | 205 |
|
17298 | 206 |
text{*Proving that @{term starrel} is an equivalence relation*} |
14299 | 207 |
|
17298 | 208 |
lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
209 |
by (rule StarDef.starrel_iff) |
14299 | 210 |
|
17298 | 211 |
lemma starrel_refl: "(x,x) \<in> starrel" |
212 |
by (simp add: starrel_def) |
|
14299 | 213 |
|
17298 | 214 |
lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel" |
215 |
by (simp add: starrel_def eq_commute) |
|
14299 | 216 |
|
17298 | 217 |
lemma starrel_trans: |
218 |
"[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel" |
|
219 |
by (simp add: starrel_def, ultra) |
|
14299 | 220 |
|
17298 | 221 |
lemma equiv_starrel: "equiv UNIV starrel" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
222 |
by (rule StarDef.equiv_starrel) |
14299 | 223 |
|
17298 | 224 |
(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *) |
225 |
lemmas equiv_starrel_iff = |
|
226 |
eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] |
|
14299 | 227 |
|
17298 | 228 |
lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
229 |
by (simp add: star_def starrel_def quotient_def, blast) |
|
14299 | 230 |
|
17298 | 231 |
declare Abs_star_inject [simp] Abs_star_inverse [simp] |
232 |
declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
|
14299 | 233 |
|
17298 | 234 |
lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel] |
14299 | 235 |
|
17298 | 236 |
lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
237 |
by (simp add: starrel_def) |
|
14299 | 238 |
|
17298 | 239 |
lemma hypreal_empty_not_mem [simp]: "{} \<notin> star" |
240 |
apply (simp add: star_def) |
|
14299 | 241 |
apply (auto elim!: quotientE equalityCE) |
242 |
done |
|
243 |
||
17298 | 244 |
lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}" |
245 |
by (insert Rep_star [of x], auto) |
|
14299 | 246 |
|
14329 | 247 |
subsection{*@{term hypreal_of_real}: |
248 |
the Injection from @{typ real} to @{typ hypreal}*} |
|
14299 | 249 |
|
250 |
lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
251 |
by (rule inj_onI, simp) |
14299 | 252 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
253 |
lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
254 |
by (cases x, simp add: star_n_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
255 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
256 |
lemma Rep_star_star_n_iff [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
257 |
"(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
258 |
by (simp add: star_n_def) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
259 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
260 |
lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
261 |
by simp |
14329 | 262 |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
263 |
subsection{* Properties of @{term star_n} *} |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
264 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
265 |
lemma star_n_add: |
17298 | 266 |
"star_n X + star_n Y = star_n (%n. X n + Y n)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
267 |
by (simp only: star_add_def starfun2_star_n) |
14329 | 268 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
269 |
lemma star_n_minus: |
17298 | 270 |
"- star_n X = star_n (%n. -(X n))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
271 |
by (simp only: star_minus_def starfun_star_n) |
14299 | 272 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
273 |
lemma star_n_diff: |
17298 | 274 |
"star_n X - star_n Y = star_n (%n. X n - Y n)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
275 |
by (simp only: star_diff_def starfun2_star_n) |
14299 | 276 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
277 |
lemma star_n_mult: |
17298 | 278 |
"star_n X * star_n Y = star_n (%n. X n * Y n)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
279 |
by (simp only: star_mult_def starfun2_star_n) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
280 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
281 |
lemma star_n_inverse: |
17301 | 282 |
"inverse (star_n X) = star_n (%n. inverse(X n))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
283 |
by (simp only: star_inverse_def starfun_star_n) |
14299 | 284 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
285 |
lemma star_n_le: |
17298 | 286 |
"star_n X \<le> star_n Y = |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14361
diff
changeset
|
287 |
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
288 |
by (simp only: star_le_def starP2_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
289 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
290 |
lemma star_n_less: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
291 |
"star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
292 |
by (simp only: star_less_def starP2_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
293 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
294 |
lemma star_n_zero_num: "0 = star_n (%n. 0)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
295 |
by (simp only: star_zero_def star_of_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
296 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
297 |
lemma star_n_one_num: "1 = star_n (%n. 1)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
298 |
by (simp only: star_one_def star_of_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
299 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
300 |
lemma star_n_abs: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
301 |
"abs (star_n X) = star_n (%n. abs (X n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
302 |
by (simp only: star_abs_def starfun_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
303 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
304 |
subsection{*Misc Others*} |
14299 | 305 |
|
14370 | 306 |
lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
15539 | 307 |
by (auto) |
14329 | 308 |
|
14331 | 309 |
lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
310 |
by auto |
14331 | 311 |
|
14329 | 312 |
lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
313 |
by auto |
14329 | 314 |
|
315 |
lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
316 |
by auto |
14329 | 317 |
|
14301 | 318 |
lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
319 |
by (simp add: omega_def star_n_zero_num star_n_less) |
14370 | 320 |
|
321 |
subsection{*Existence of Infinite Hyperreal Number*} |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
322 |
|
14370 | 323 |
text{*Existence of infinite number not corresponding to any real number. |
324 |
Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
|
325 |
||
326 |
||
327 |
text{*A few lemmas first*} |
|
328 |
||
329 |
lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
|
330 |
(\<exists>y. {n::nat. x = real n} = {y})" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
331 |
by force |
14370 | 332 |
|
333 |
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
334 |
by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
|
335 |
||
336 |
lemma not_ex_hypreal_of_real_eq_omega: |
|
337 |
"~ (\<exists>x. hypreal_of_real x = omega)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
338 |
apply (simp add: omega_def) |
17298 | 339 |
apply (simp add: star_of_def star_n_eq_iff) |
14370 | 340 |
apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] |
341 |
lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) |
|
342 |
done |
|
343 |
||
344 |
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega" |
|
14705 | 345 |
by (insert not_ex_hypreal_of_real_eq_omega, auto) |
14370 | 346 |
|
347 |
text{*Existence of infinitesimal number also not corresponding to any |
|
348 |
real number*} |
|
349 |
||
350 |
lemma lemma_epsilon_empty_singleton_disj: |
|
351 |
"{n::nat. x = inverse(real(Suc n))} = {} | |
|
352 |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
353 |
by auto |
14370 | 354 |
|
355 |
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
356 |
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
357 |
||
14705 | 358 |
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
359 |
by (auto simp add: epsilon_def star_of_def star_n_eq_iff |
14705 | 360 |
lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) |
14370 | 361 |
|
362 |
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon" |
|
14705 | 363 |
by (insert not_ex_hypreal_of_real_eq_epsilon, auto) |
14370 | 364 |
|
365 |
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
|
17298 | 366 |
by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff |
367 |
del: star_of_zero) |
|
14370 | 368 |
|
369 |
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
370 |
by (simp add: epsilon_def omega_def star_n_inverse) |
14370 | 371 |
|
20753 | 372 |
lemma hypreal_epsilon_gt_zero: "0 < epsilon" |
373 |
by (simp add: hypreal_epsilon_inverse_omega) |
|
374 |
||
10751 | 375 |
end |