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