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