author | huffman |
Tue, 06 Sep 2005 23:16:48 +0200 | |
changeset 17298 | ad73fb6144cf |
parent 17290 | a39d1430d271 |
child 17299 | c6eecde058e4 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : NatStar.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14415 | 4 |
|
5 |
Converted to Isar and polished by lcp |
|
6 |
*) |
|
7 |
||
8 |
header{*Star-transforms for the Hypernaturals*} |
|
10751 | 9 |
|
15131 | 10 |
theory NatStar |
15360 | 11 |
imports HyperPow |
15131 | 12 |
begin |
14415 | 13 |
|
14 |
text{*Extends sets of nats, and functions from the nats to nats or reals*} |
|
15 |
||
10751 | 16 |
|
17 |
constdefs |
|
18 |
||
19 |
(* internal sets and nonstandard extensions -- see Star.thy as well *) |
|
20 |
||
14415 | 21 |
starsetNat :: "nat set => hypnat set" ("*sNat* _" [80] 80) |
22 |
"*sNat* A == |
|
23 |
{x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}" |
|
10751 | 24 |
|
14415 | 25 |
starsetNat_n :: "(nat => nat set) => hypnat set" ("*sNatn* _" [80] 80) |
26 |
"*sNatn* As == |
|
27 |
{x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}" |
|
10751 | 28 |
|
14415 | 29 |
InternalNatSets :: "hypnat set set" |
30 |
"InternalNatSets == {X. \<exists>As. X = *sNatn* As}" |
|
10751 | 31 |
|
32 |
(* star transform of functions f:Nat --> Real *) |
|
33 |
||
14415 | 34 |
starfunNat :: "(nat => real) => hypnat => hypreal" |
35 |
("*fNat* _" [80] 80) |
|
17298 | 36 |
"*fNat* f == (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. f (X n)}))" |
10751 | 37 |
|
14415 | 38 |
starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal" |
39 |
("*fNatn* _" [80] 80) |
|
40 |
"*fNatn* F == |
|
17298 | 41 |
(%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. (F n)(X n)}))" |
10751 | 42 |
|
14415 | 43 |
InternalNatFuns :: "(hypnat => hypreal) set" |
44 |
"InternalNatFuns == {X. \<exists>F. X = *fNatn* F}" |
|
10751 | 45 |
|
46 |
(* star transform of functions f:Nat --> Nat *) |
|
47 |
||
14415 | 48 |
starfunNat2 :: "(nat => nat) => hypnat => hypnat" |
49 |
("*fNat2* _" [80] 80) |
|
50 |
"*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})" |
|
51 |
||
52 |
starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat" |
|
53 |
("*fNat2n* _" [80] 80) |
|
54 |
"*fNat2n* F == |
|
55 |
%x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})" |
|
56 |
||
57 |
InternalNatFuns2 :: "(hypnat => hypnat) set" |
|
58 |
"InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}" |
|
59 |
||
60 |
||
61 |
lemma NatStar_real_set: "*sNat*(UNIV::nat set) = (UNIV::hypnat set)" |
|
62 |
by (simp add: starsetNat_def) |
|
63 |
||
64 |
lemma NatStar_empty_set [simp]: "*sNat* {} = {}" |
|
65 |
by (simp add: starsetNat_def) |
|
66 |
||
67 |
lemma NatStar_Un: "*sNat* (A Un B) = *sNat* A Un *sNat* B" |
|
68 |
apply (auto simp add: starsetNat_def) |
|
69 |
prefer 2 apply (blast intro: FreeUltrafilterNat_subset) |
|
70 |
prefer 2 apply (blast intro: FreeUltrafilterNat_subset) |
|
71 |
apply (drule FreeUltrafilterNat_Compl_mem) |
|
72 |
apply (drule bspec, assumption) |
|
73 |
apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra) |
|
74 |
done |
|
75 |
||
76 |
lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B" |
|
77 |
apply (auto simp add: starsetNat_n_def) |
|
78 |
apply (drule_tac x = Xa in bspec) |
|
79 |
apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
80 |
apply (auto dest!: bspec, ultra+) |
|
81 |
done |
|
82 |
||
83 |
lemma InternalNatSets_Un: |
|
84 |
"[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
85 |
==> (X Un Y) \<in> InternalNatSets" |
|
86 |
by (auto simp add: InternalNatSets_def starsetNat_n_Un [symmetric]) |
|
87 |
||
88 |
lemma NatStar_Int: "*sNat* (A Int B) = *sNat* A Int *sNat* B" |
|
89 |
apply (auto simp add: starsetNat_def) |
|
90 |
prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset) |
|
91 |
apply (blast intro: FreeUltrafilterNat_subset)+ |
|
92 |
done |
|
93 |
||
94 |
lemma starsetNat_n_Int: |
|
95 |
"*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B" |
|
96 |
apply (auto simp add: starsetNat_n_def) |
|
97 |
apply (auto dest!: bspec, ultra+) |
|
98 |
done |
|
99 |
||
100 |
lemma InternalNatSets_Int: |
|
101 |
"[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
102 |
==> (X Int Y) \<in> InternalNatSets" |
|
103 |
by (auto simp add: InternalNatSets_def starsetNat_n_Int [symmetric]) |
|
104 |
||
105 |
lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)" |
|
106 |
apply (auto simp add: starsetNat_def) |
|
107 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
108 |
apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
109 |
apply (auto dest!: bspec, ultra+) |
|
110 |
done |
|
111 |
||
112 |
lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)" |
|
113 |
apply (auto simp add: starsetNat_n_def) |
|
114 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
115 |
apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
116 |
apply (auto dest!: bspec, ultra+) |
|
117 |
done |
|
118 |
||
119 |
lemma InternalNatSets_Compl: "X \<in> InternalNatSets ==> -X \<in> InternalNatSets" |
|
120 |
by (auto simp add: InternalNatSets_def starsetNat_n_Compl [symmetric]) |
|
121 |
||
122 |
lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B" |
|
123 |
apply (auto simp add: starsetNat_n_def) |
|
124 |
apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
125 |
apply (rule_tac [3] z = x in eq_Abs_hypnat) |
|
126 |
apply (auto dest!: bspec, ultra+) |
|
127 |
done |
|
128 |
||
129 |
lemma InternalNatSets_diff: |
|
130 |
"[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
131 |
==> (X - Y) \<in> InternalNatSets" |
|
132 |
by (auto simp add: InternalNatSets_def starsetNat_n_diff [symmetric]) |
|
133 |
||
134 |
lemma NatStar_subset: "A \<le> B ==> *sNat* A \<le> *sNat* B" |
|
135 |
apply (simp add: starsetNat_def) |
|
136 |
apply (blast intro: FreeUltrafilterNat_subset) |
|
137 |
done |
|
138 |
||
139 |
lemma NatStar_mem: "a \<in> A ==> hypnat_of_nat a \<in> *sNat* A" |
|
140 |
by (auto intro: FreeUltrafilterNat_subset |
|
141 |
simp add: starsetNat_def hypnat_of_nat_eq) |
|
142 |
||
143 |
lemma NatStar_hypreal_of_real_image_subset: "hypnat_of_nat ` A \<le> *sNat* A" |
|
144 |
apply (auto simp add: starsetNat_def hypnat_of_nat_eq) |
|
145 |
apply (blast intro: FreeUltrafilterNat_subset) |
|
146 |
done |
|
147 |
||
148 |
lemma NatStar_SHNat_subset: "Nats \<le> *sNat* (UNIV:: nat set)" |
|
149 |
by (simp add: starsetNat_def SHNat_eq hypnat_of_nat_eq) |
|
150 |
||
151 |
lemma NatStar_hypreal_of_real_Int: |
|
152 |
"*sNat* X Int Nats = hypnat_of_nat ` X" |
|
153 |
apply (auto simp add: starsetNat_def hypnat_of_nat_eq SHNat_eq) |
|
154 |
apply (simp add: hypnat_of_nat_eq [symmetric]) |
|
155 |
apply (rule imageI, rule ccontr) |
|
156 |
apply (drule bspec) |
|
157 |
apply (rule lemma_hypnatrel_refl) |
|
158 |
prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto) |
|
159 |
done |
|
160 |
||
161 |
lemma starsetNat_starsetNat_n_eq: "*sNat* X = *sNatn* (%n. X)" |
|
162 |
by (simp add: starsetNat_n_def starsetNat_def) |
|
163 |
||
164 |
lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets" |
|
165 |
by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq) |
|
166 |
||
167 |
lemma InternalNatSets_UNIV_diff: |
|
168 |
"X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets" |
|
17290 | 169 |
apply (subgoal_tac "UNIV - X = - X") |
14415 | 170 |
by (auto intro: InternalNatSets_Compl) |
171 |
||
172 |
text{*Nonstandard extension of a set (defined using a constant |
|
173 |
sequence) as a special case of an internal set*} |
|
174 |
lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A" |
|
175 |
by (simp add: starsetNat_n_def starsetNat_def) |
|
176 |
||
177 |
||
178 |
subsection{*Nonstandard Extensions of Functions*} |
|
179 |
||
180 |
text{* Nonstandard extension of a function (defined using a constant |
|
181 |
sequence) as a special case of an internal function*} |
|
182 |
||
183 |
lemma starfunNat_n_starfunNat: "\<forall>n. (F n = f) ==> *fNatn* F = *fNat* f" |
|
184 |
by (simp add: starfunNat_n_def starfunNat_def) |
|
185 |
||
186 |
lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f" |
|
187 |
by (simp add: starfunNat2_n_def starfunNat2_def) |
|
188 |
||
15169 | 189 |
lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel" |
14415 | 190 |
apply (simp add: congruent_def, safe) |
191 |
apply (ultra+) |
|
192 |
done |
|
193 |
||
194 |
(* f::nat=>real *) |
|
195 |
lemma starfunNat: |
|
196 |
"( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
17298 | 197 |
Abs_star(starrel `` {%n. f (X n)})" |
14415 | 198 |
apply (simp add: starfunNat_def) |
17298 | 199 |
apply (rule arg_cong [where f = Abs_star]) |
14415 | 200 |
apply (auto, ultra) |
201 |
done |
|
202 |
||
203 |
(* f::nat=>nat *) |
|
204 |
lemma starfunNat2: |
|
205 |
"( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
206 |
Abs_hypnat(hypnatrel `` {%n. f (X n)})" |
|
207 |
apply (simp add: starfunNat2_def) |
|
208 |
apply (rule arg_cong [where f = Abs_hypnat]) |
|
209 |
apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse] |
|
210 |
UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent]) |
|
211 |
done |
|
212 |
||
213 |
subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*} |
|
214 |
||
215 |
lemma starfunNat_mult: |
|
216 |
"( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z" |
|
14468 | 217 |
apply (cases z) |
14415 | 218 |
apply (simp add: starfunNat hypreal_mult) |
219 |
done |
|
220 |
||
221 |
lemma starfunNat2_mult: |
|
222 |
"( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z" |
|
14468 | 223 |
apply (cases z) |
14415 | 224 |
apply (simp add: starfunNat2 hypnat_mult) |
225 |
done |
|
226 |
||
227 |
subsubsection{*Addition: @{text "( *f) + ( *g) = *(f + g)"}*} |
|
228 |
||
229 |
lemma starfunNat_add: |
|
230 |
"( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z" |
|
14468 | 231 |
apply (cases z) |
14415 | 232 |
apply (simp add: starfunNat hypreal_add) |
233 |
done |
|
234 |
||
235 |
lemma starfunNat2_add: |
|
236 |
"( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z" |
|
14468 | 237 |
apply (cases z) |
14415 | 238 |
apply (simp add: starfunNat2 hypnat_add) |
239 |
done |
|
240 |
||
241 |
lemma starfunNat2_minus: |
|
242 |
"( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z" |
|
14468 | 243 |
apply (cases z) |
14415 | 244 |
apply (simp add: starfunNat2 hypnat_minus) |
245 |
done |
|
246 |
||
247 |
subsubsection{*Composition: @{text "( *f) o ( *g) = *(f o g)"}*} |
|
248 |
||
249 |
(***** ( *f::nat=>real) o ( *g::nat=>nat) = *(f o g) *****) |
|
250 |
||
251 |
lemma starfunNatNat2_o: |
|
252 |
"( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))" |
|
253 |
apply (rule ext) |
|
254 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
255 |
apply (simp add: starfunNat2 starfunNat) |
|
256 |
done |
|
257 |
||
258 |
lemma starfunNatNat2_o2: |
|
259 |
"(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))" |
|
260 |
apply (insert starfunNatNat2_o [of f g]) |
|
261 |
apply (simp add: o_def) |
|
262 |
done |
|
263 |
||
264 |
(***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****) |
|
265 |
lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))" |
|
266 |
apply (rule ext) |
|
267 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
268 |
apply (simp add: starfunNat2) |
|
269 |
done |
|
270 |
||
271 |
(***** ( *f::real=>real) o ( *g::nat=>real) = *(f o g) *****) |
|
272 |
||
273 |
lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))" |
|
274 |
apply (rule ext) |
|
275 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
276 |
apply (simp add: starfunNat starfun) |
|
277 |
done |
|
278 |
||
279 |
lemma starfun_stafunNat_o2: |
|
280 |
"(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))" |
|
281 |
apply (insert starfun_stafunNat_o [of f g]) |
|
282 |
apply (simp add: o_def) |
|
283 |
done |
|
284 |
||
285 |
||
286 |
text{*NS extension of constant function*} |
|
287 |
||
288 |
lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k" |
|
14468 | 289 |
apply (cases z) |
17298 | 290 |
apply (simp add: starfunNat hypreal_of_real_def star_of_def star_n_def) |
14415 | 291 |
done |
10751 | 292 |
|
14415 | 293 |
lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat k" |
14468 | 294 |
apply (cases z) |
14415 | 295 |
apply (simp add: starfunNat2 hypnat_of_nat_eq) |
296 |
done |
|
297 |
||
298 |
lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x" |
|
14468 | 299 |
apply (cases x) |
14415 | 300 |
apply (simp add: starfunNat hypreal_minus) |
301 |
done |
|
302 |
||
303 |
lemma starfunNat_inverse: |
|
304 |
"inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x" |
|
14468 | 305 |
apply (cases x) |
14415 | 306 |
apply (simp add: starfunNat hypreal_inverse) |
307 |
done |
|
308 |
||
309 |
text{* Extended function has same solution as its standard |
|
310 |
version for natural arguments. i.e they are the same |
|
311 |
for all natural arguments (c.f. Hoskins pg. 107- SEQ)*} |
|
312 |
||
313 |
lemma starfunNat_eq [simp]: |
|
314 |
"( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)" |
|
17298 | 315 |
by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def star_of_def star_n_def) |
14415 | 316 |
|
317 |
lemma starfunNat2_eq [simp]: |
|
318 |
"( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)" |
|
319 |
by (simp add: starfunNat2 hypnat_of_nat_eq) |
|
320 |
||
321 |
lemma starfunNat_approx: |
|
322 |
"( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)" |
|
323 |
by auto |
|
324 |
||
325 |
||
326 |
text{* Example of transfer of a property from reals to hyperreals |
|
327 |
--- used for limit comparison of sequences*} |
|
328 |
||
329 |
lemma starfun_le_mono: |
|
330 |
"\<forall>n. N \<le> n --> f n \<le> g n |
|
331 |
==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n" |
|
332 |
apply safe |
|
333 |
apply (rule_tac z = n in eq_Abs_hypnat) |
|
334 |
apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto) |
|
335 |
done |
|
336 |
||
337 |
(*****----- and another -----*****) |
|
338 |
lemma starfun_less_mono: |
|
339 |
"\<forall>n. N \<le> n --> f n < g n |
|
340 |
==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n" |
|
341 |
apply safe |
|
342 |
apply (rule_tac z = n in eq_Abs_hypnat) |
|
343 |
apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto) |
|
344 |
done |
|
345 |
||
346 |
text{*Nonstandard extension when we increment the argument by one*} |
|
347 |
||
348 |
lemma starfunNat_shift_one: |
|
349 |
"( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))" |
|
14468 | 350 |
apply (cases N) |
14415 | 351 |
apply (simp add: starfunNat hypnat_one_def hypnat_add) |
352 |
done |
|
353 |
||
354 |
text{*Nonstandard extension with absolute value*} |
|
355 |
||
356 |
lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)" |
|
14468 | 357 |
apply (cases N) |
14415 | 358 |
apply (simp add: starfunNat hypreal_hrabs) |
359 |
done |
|
360 |
||
361 |
text{*The hyperpow function as a nonstandard extension of realpow*} |
|
362 |
||
363 |
lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N" |
|
14468 | 364 |
apply (cases N) |
17298 | 365 |
apply (simp add: hyperpow hypreal_of_real_def star_of_def star_n_def starfunNat) |
14415 | 366 |
done |
367 |
||
368 |
lemma starfunNat_pow2: |
|
369 |
"( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m" |
|
14468 | 370 |
apply (cases N) |
14415 | 371 |
apply (simp add: hyperpow hypnat_of_nat_eq starfunNat) |
372 |
done |
|
373 |
||
374 |
lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n" |
|
17298 | 375 |
apply (rule_tac z = R in eq_Abs_star) |
14415 | 376 |
apply (simp add: hyperpow starfun hypnat_of_nat_eq) |
377 |
done |
|
378 |
||
379 |
text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of |
|
380 |
@{term real_of_nat} *} |
|
381 |
||
382 |
lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat" |
|
383 |
apply (rule ext) |
|
384 |
apply (rule_tac z = x in eq_Abs_hypnat) |
|
385 |
apply (simp add: hypreal_of_hypnat starfunNat) |
|
386 |
done |
|
387 |
||
388 |
lemma starfunNat_inverse_real_of_nat_eq: |
|
389 |
"N \<in> HNatInfinite |
|
390 |
==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)" |
|
391 |
apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst]) |
|
392 |
apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
393 |
apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat starfun_inverse_inverse) |
|
394 |
done |
|
395 |
||
396 |
text{*Internal functions - some redundancy with *fNat* now*} |
|
397 |
||
398 |
lemma starfunNat_n_congruent: |
|
15169 | 399 |
"(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel" |
400 |
by (auto simp add: congruent_def, ultra+) |
|
14415 | 401 |
|
402 |
lemma starfunNat_n: |
|
403 |
"( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
17298 | 404 |
Abs_star(starrel `` {%n. f n (X n)})" |
14415 | 405 |
apply (simp add: starfunNat_n_def) |
17298 | 406 |
apply (rule_tac f = Abs_star in arg_cong, auto, ultra) |
14415 | 407 |
done |
408 |
||
409 |
text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*} |
|
10751 | 410 |
|
14415 | 411 |
lemma starfunNat_n_mult: |
412 |
"( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z" |
|
14468 | 413 |
apply (cases z) |
14415 | 414 |
apply (simp add: starfunNat_n hypreal_mult) |
415 |
done |
|
416 |
||
417 |
text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*} |
|
418 |
||
419 |
lemma starfunNat_n_add: |
|
420 |
"( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z" |
|
14468 | 421 |
apply (cases z) |
14415 | 422 |
apply (simp add: starfunNat_n hypreal_add) |
423 |
done |
|
424 |
||
425 |
text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*} |
|
426 |
||
427 |
lemma starfunNat_n_add_minus: |
|
428 |
"( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z" |
|
14468 | 429 |
apply (cases z) |
14415 | 430 |
apply (simp add: starfunNat_n hypreal_minus hypreal_add) |
431 |
done |
|
432 |
||
433 |
||
434 |
text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*} |
|
435 |
||
436 |
lemma starfunNat_n_const_fun [simp]: |
|
437 |
"( *fNatn* (%i x. k)) z = hypreal_of_real k" |
|
14468 | 438 |
apply (cases z) |
17298 | 439 |
apply (simp add: starfunNat_n hypreal_of_real_def star_of_def star_n_def) |
14415 | 440 |
done |
441 |
||
442 |
lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x" |
|
14468 | 443 |
apply (cases x) |
14415 | 444 |
apply (simp add: starfunNat_n hypreal_minus) |
445 |
done |
|
446 |
||
447 |
lemma starfunNat_n_eq [simp]: |
|
17298 | 448 |
"( *fNatn* f) (hypnat_of_nat n) = Abs_star(starrel `` {%i. f i n})" |
14415 | 449 |
by (simp add: starfunNat_n hypnat_of_nat_eq) |
450 |
||
451 |
lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)" |
|
452 |
apply auto |
|
453 |
apply (rule ext, rule ccontr) |
|
454 |
apply (drule_tac x = "hypnat_of_nat (x) " in fun_cong) |
|
455 |
apply (simp add: starfunNat hypnat_of_nat_eq) |
|
456 |
done |
|
457 |
||
458 |
||
459 |
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]: |
|
460 |
"N \<in> HNatInfinite ==> ( *fNat* (%x. inverse (real x))) N \<in> Infinitesimal" |
|
461 |
apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst]) |
|
462 |
apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
463 |
apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat) |
|
464 |
done |
|
465 |
||
466 |
ML |
|
467 |
{* |
|
468 |
val starsetNat_def = thm "starsetNat_def"; |
|
469 |
||
470 |
val NatStar_real_set = thm "NatStar_real_set"; |
|
471 |
val NatStar_empty_set = thm "NatStar_empty_set"; |
|
472 |
val NatStar_Un = thm "NatStar_Un"; |
|
473 |
val starsetNat_n_Un = thm "starsetNat_n_Un"; |
|
474 |
val InternalNatSets_Un = thm "InternalNatSets_Un"; |
|
475 |
val NatStar_Int = thm "NatStar_Int"; |
|
476 |
val starsetNat_n_Int = thm "starsetNat_n_Int"; |
|
477 |
val InternalNatSets_Int = thm "InternalNatSets_Int"; |
|
478 |
val NatStar_Compl = thm "NatStar_Compl"; |
|
479 |
val starsetNat_n_Compl = thm "starsetNat_n_Compl"; |
|
480 |
val InternalNatSets_Compl = thm "InternalNatSets_Compl"; |
|
481 |
val starsetNat_n_diff = thm "starsetNat_n_diff"; |
|
482 |
val InternalNatSets_diff = thm "InternalNatSets_diff"; |
|
483 |
val NatStar_subset = thm "NatStar_subset"; |
|
484 |
val NatStar_mem = thm "NatStar_mem"; |
|
485 |
val NatStar_hypreal_of_real_image_subset = thm "NatStar_hypreal_of_real_image_subset"; |
|
486 |
val NatStar_SHNat_subset = thm "NatStar_SHNat_subset"; |
|
487 |
val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int"; |
|
488 |
val starsetNat_starsetNat_n_eq = thm "starsetNat_starsetNat_n_eq"; |
|
489 |
val InternalNatSets_starsetNat_n = thm "InternalNatSets_starsetNat_n"; |
|
490 |
val InternalNatSets_UNIV_diff = thm "InternalNatSets_UNIV_diff"; |
|
491 |
val starsetNat_n_starsetNat = thm "starsetNat_n_starsetNat"; |
|
492 |
val starfunNat_n_starfunNat = thm "starfunNat_n_starfunNat"; |
|
493 |
val starfunNat2_n_starfunNat2 = thm "starfunNat2_n_starfunNat2"; |
|
494 |
val starfunNat_congruent = thm "starfunNat_congruent"; |
|
495 |
val starfunNat = thm "starfunNat"; |
|
496 |
val starfunNat2 = thm "starfunNat2"; |
|
497 |
val starfunNat_mult = thm "starfunNat_mult"; |
|
498 |
val starfunNat2_mult = thm "starfunNat2_mult"; |
|
499 |
val starfunNat_add = thm "starfunNat_add"; |
|
500 |
val starfunNat2_add = thm "starfunNat2_add"; |
|
501 |
val starfunNat2_minus = thm "starfunNat2_minus"; |
|
502 |
val starfunNatNat2_o = thm "starfunNatNat2_o"; |
|
503 |
val starfunNatNat2_o2 = thm "starfunNatNat2_o2"; |
|
504 |
val starfunNat2_o = thm "starfunNat2_o"; |
|
505 |
val starfun_stafunNat_o = thm "starfun_stafunNat_o"; |
|
506 |
val starfun_stafunNat_o2 = thm "starfun_stafunNat_o2"; |
|
507 |
val starfunNat_const_fun = thm "starfunNat_const_fun"; |
|
508 |
val starfunNat2_const_fun = thm "starfunNat2_const_fun"; |
|
509 |
val starfunNat_minus = thm "starfunNat_minus"; |
|
510 |
val starfunNat_inverse = thm "starfunNat_inverse"; |
|
511 |
val starfunNat_eq = thm "starfunNat_eq"; |
|
512 |
val starfunNat2_eq = thm "starfunNat2_eq"; |
|
513 |
val starfunNat_approx = thm "starfunNat_approx"; |
|
514 |
val starfun_le_mono = thm "starfun_le_mono"; |
|
515 |
val starfun_less_mono = thm "starfun_less_mono"; |
|
516 |
val starfunNat_shift_one = thm "starfunNat_shift_one"; |
|
517 |
val starfunNat_rabs = thm "starfunNat_rabs"; |
|
518 |
val starfunNat_pow = thm "starfunNat_pow"; |
|
519 |
val starfunNat_pow2 = thm "starfunNat_pow2"; |
|
520 |
val starfun_pow = thm "starfun_pow"; |
|
521 |
val starfunNat_real_of_nat = thm "starfunNat_real_of_nat"; |
|
522 |
val starfunNat_inverse_real_of_nat_eq = thm "starfunNat_inverse_real_of_nat_eq"; |
|
523 |
val starfunNat_n_congruent = thm "starfunNat_n_congruent"; |
|
524 |
val starfunNat_n = thm "starfunNat_n"; |
|
525 |
val starfunNat_n_mult = thm "starfunNat_n_mult"; |
|
526 |
val starfunNat_n_add = thm "starfunNat_n_add"; |
|
527 |
val starfunNat_n_add_minus = thm "starfunNat_n_add_minus"; |
|
528 |
val starfunNat_n_const_fun = thm "starfunNat_n_const_fun"; |
|
529 |
val starfunNat_n_minus = thm "starfunNat_n_minus"; |
|
530 |
val starfunNat_n_eq = thm "starfunNat_n_eq"; |
|
531 |
val starfun_eq_iff = thm "starfun_eq_iff"; |
|
532 |
val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal"; |
|
533 |
*} |
|
534 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
535 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
536 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
537 |
subsection{*Nonstandard Characterization of Induction*} |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
538 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
539 |
constdefs |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
540 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
541 |
starPNat :: "(nat => bool) => hypnat => bool" ("*pNat* _" [80] 80) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
542 |
"*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) & |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
543 |
{n. P(X n)} \<in> FreeUltrafilterNat))" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
544 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
545 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
546 |
starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
547 |
("*pNat2* _" [80] 80) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
548 |
"*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) & |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
549 |
{n. P(X n) (Y n)} \<in> FreeUltrafilterNat))" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
550 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
551 |
hSuc :: "hypnat => hypnat" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
552 |
"hSuc n == n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
553 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
554 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
555 |
lemma starPNat: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
556 |
"(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
557 |
({n. P (X n)} \<in> FreeUltrafilterNat)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
558 |
by (auto simp add: starPNat_def, ultra) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
559 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
560 |
lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
561 |
by (auto simp add: starPNat hypnat_of_nat_eq) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
562 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
563 |
lemma hypnat_induct_obj: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
564 |
"(( *pNat* P) 0 & |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
565 |
(\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
566 |
--> ( *pNat* P)(n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
567 |
apply (cases n) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
568 |
apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
569 |
apply (erule nat_induct) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
570 |
apply (drule_tac x = "hypnat_of_nat n" in spec) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
571 |
apply (rule ccontr) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
572 |
apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
573 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
574 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
575 |
lemma hypnat_induct: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
576 |
"[| ( *pNat* P) 0; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
577 |
!!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
578 |
==> ( *pNat* P)(n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
579 |
by (insert hypnat_induct_obj [of P n], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
580 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
581 |
lemma starPNat2: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
582 |
"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
583 |
(Abs_hypnat(hypnatrel``{%n. Y n}))) = |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
584 |
({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
585 |
by (auto simp add: starPNat2_def, ultra) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
586 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
587 |
lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
588 |
apply (simp add: starPNat2_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
589 |
apply (rule ext) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
590 |
apply (rule ext) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
591 |
apply (rule_tac z = x in eq_Abs_hypnat) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
592 |
apply (rule_tac z = y in eq_Abs_hypnat) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
593 |
apply (auto, ultra) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
594 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
595 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
596 |
lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
597 |
by (simp add: starPNat2_eq_iff) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
598 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
599 |
lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
600 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
601 |
apply (rule_tac z = h in eq_Abs_hypnat, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
602 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
603 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
604 |
lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
605 |
by (simp add: hSuc_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
606 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
607 |
lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff] |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
608 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
609 |
lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
610 |
by (simp add: hSuc_def hypnat_one_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
611 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
612 |
lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
613 |
by (erule LeastI) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
614 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
615 |
lemma nonempty_InternalNatSet_has_least: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
616 |
"[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
617 |
apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
618 |
apply (rule_tac z = x in eq_Abs_hypnat) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
619 |
apply (auto dest!: bspec simp add: hypnat_le) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
620 |
apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
621 |
apply (ultra, force dest: nonempty_nat_set_Least_mem) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
622 |
apply (drule_tac x = x in bspec, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
623 |
apply (ultra, auto intro: Least_le) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
624 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
625 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
626 |
text{* Goldblatt page 129 Thm 11.3.2*} |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
627 |
lemma internal_induct: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
628 |
"[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |] |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
629 |
==> X = (UNIV:: hypnat set)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
630 |
apply (rule ccontr) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
631 |
apply (frule InternalNatSets_Compl) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
632 |
apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
633 |
apply (subgoal_tac "1 \<le> n") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
634 |
apply (drule_tac x = "n - 1" in bspec, safe) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
635 |
apply (drule_tac x = "n - 1" in spec) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
636 |
apply (drule_tac [2] c = 1 and a = n in add_right_mono) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
637 |
apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
638 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
639 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14468
diff
changeset
|
640 |
|
10751 | 641 |
end |