1 (* Title : NatStar.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 |
|
5 Converted to Isar and polished by lcp |
|
6 *) |
|
7 |
|
8 header{*Star-transforms for the Hypernaturals*} |
|
9 |
|
10 theory NatStar |
|
11 imports Star |
|
12 begin |
|
13 |
|
14 lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn" |
|
15 by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n) |
|
16 |
|
17 lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B" |
|
18 apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def) |
|
19 apply (rule_tac x=whn in spec, transfer, simp) |
|
20 done |
|
21 |
|
22 lemma InternalSets_Un: |
|
23 "[| X \<in> InternalSets; Y \<in> InternalSets |] |
|
24 ==> (X Un Y) \<in> InternalSets" |
|
25 by (auto simp add: InternalSets_def starset_n_Un [symmetric]) |
|
26 |
|
27 lemma starset_n_Int: |
|
28 "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B" |
|
29 apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def) |
|
30 apply (rule_tac x=whn in spec, transfer, simp) |
|
31 done |
|
32 |
|
33 lemma InternalSets_Int: |
|
34 "[| X \<in> InternalSets; Y \<in> InternalSets |] |
|
35 ==> (X Int Y) \<in> InternalSets" |
|
36 by (auto simp add: InternalSets_def starset_n_Int [symmetric]) |
|
37 |
|
38 lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)" |
|
39 apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq) |
|
40 apply (rule_tac x=whn in spec, transfer, simp) |
|
41 done |
|
42 |
|
43 lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets" |
|
44 by (auto simp add: InternalSets_def starset_n_Compl [symmetric]) |
|
45 |
|
46 lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B" |
|
47 apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq) |
|
48 apply (rule_tac x=whn in spec, transfer, simp) |
|
49 done |
|
50 |
|
51 lemma InternalSets_diff: |
|
52 "[| X \<in> InternalSets; Y \<in> InternalSets |] |
|
53 ==> (X - Y) \<in> InternalSets" |
|
54 by (auto simp add: InternalSets_def starset_n_diff [symmetric]) |
|
55 |
|
56 lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)" |
|
57 by simp |
|
58 |
|
59 lemma NatStar_hypreal_of_real_Int: |
|
60 "*s* X Int Nats = hypnat_of_nat ` X" |
|
61 by (auto simp add: SHNat_eq) |
|
62 |
|
63 lemma starset_starset_n_eq: "*s* X = *sn* (%n. X)" |
|
64 by (simp add: starset_n_starset) |
|
65 |
|
66 lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets" |
|
67 by (auto simp add: InternalSets_def starset_starset_n_eq) |
|
68 |
|
69 lemma InternalSets_UNIV_diff: |
|
70 "X \<in> InternalSets ==> UNIV - X \<in> InternalSets" |
|
71 apply (subgoal_tac "UNIV - X = - X") |
|
72 by (auto intro: InternalSets_Compl) |
|
73 |
|
74 |
|
75 subsection{*Nonstandard Extensions of Functions*} |
|
76 |
|
77 text{* Example of transfer of a property from reals to hyperreals |
|
78 --- used for limit comparison of sequences*} |
|
79 |
|
80 lemma starfun_le_mono: |
|
81 "\<forall>n. N \<le> n --> f n \<le> g n |
|
82 ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n" |
|
83 by transfer |
|
84 |
|
85 (*****----- and another -----*****) |
|
86 lemma starfun_less_mono: |
|
87 "\<forall>n. N \<le> n --> f n < g n |
|
88 ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n" |
|
89 by transfer |
|
90 |
|
91 text{*Nonstandard extension when we increment the argument by one*} |
|
92 |
|
93 lemma starfun_shift_one: |
|
94 "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))" |
|
95 by (transfer, simp) |
|
96 |
|
97 text{*Nonstandard extension with absolute value*} |
|
98 |
|
99 lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)" |
|
100 by (transfer, rule refl) |
|
101 |
|
102 text{*The hyperpow function as a nonstandard extension of realpow*} |
|
103 |
|
104 lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N" |
|
105 by (transfer, rule refl) |
|
106 |
|
107 lemma starfun_pow2: |
|
108 "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m" |
|
109 by (transfer, rule refl) |
|
110 |
|
111 lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n" |
|
112 by (transfer, rule refl) |
|
113 |
|
114 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of |
|
115 @{term real_of_nat} *} |
|
116 |
|
117 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" |
|
118 by transfer (simp add: expand_fun_eq real_of_nat_def) |
|
119 |
|
120 lemma starfun_inverse_real_of_nat_eq: |
|
121 "N \<in> HNatInfinite |
|
122 ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)" |
|
123 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |
|
124 apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
125 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse) |
|
126 done |
|
127 |
|
128 text{*Internal functions - some redundancy with *f* now*} |
|
129 |
|
130 lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))" |
|
131 by (simp add: starfun_n_def Ifun_star_n) |
|
132 |
|
133 text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*} |
|
134 |
|
135 lemma starfun_n_mult: |
|
136 "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z" |
|
137 apply (cases z) |
|
138 apply (simp add: starfun_n star_n_mult) |
|
139 done |
|
140 |
|
141 text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*} |
|
142 |
|
143 lemma starfun_n_add: |
|
144 "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z" |
|
145 apply (cases z) |
|
146 apply (simp add: starfun_n star_n_add) |
|
147 done |
|
148 |
|
149 text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*} |
|
150 |
|
151 lemma starfun_n_add_minus: |
|
152 "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z" |
|
153 apply (cases z) |
|
154 apply (simp add: starfun_n star_n_minus star_n_add) |
|
155 done |
|
156 |
|
157 |
|
158 text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*} |
|
159 |
|
160 lemma starfun_n_const_fun [simp]: |
|
161 "( *fn* (%i x. k)) z = star_of k" |
|
162 apply (cases z) |
|
163 apply (simp add: starfun_n star_of_def) |
|
164 done |
|
165 |
|
166 lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (%i x. - (f i) x)) x" |
|
167 apply (cases x) |
|
168 apply (simp add: starfun_n star_n_minus) |
|
169 done |
|
170 |
|
171 lemma starfun_n_eq [simp]: |
|
172 "( *fn* f) (star_of n) = star_n (%i. f i n)" |
|
173 by (simp add: starfun_n star_of_def) |
|
174 |
|
175 lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) = (f = g)" |
|
176 by (transfer, rule refl) |
|
177 |
|
178 lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]: |
|
179 "N \<in> HNatInfinite ==> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal" |
|
180 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |
|
181 apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
182 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat) |
|
183 done |
|
184 |
|
185 |
|
186 subsection{*Nonstandard Characterization of Induction*} |
|
187 |
|
188 lemma hypnat_induct_obj: |
|
189 "!!n. (( *p* P) (0::hypnat) & |
|
190 (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1))) |
|
191 --> ( *p* P)(n)" |
|
192 by (transfer, induct_tac n, auto) |
|
193 |
|
194 lemma hypnat_induct: |
|
195 "!!n. [| ( *p* P) (0::hypnat); |
|
196 !!n. ( *p* P)(n) ==> ( *p* P)(n + 1)|] |
|
197 ==> ( *p* P)(n)" |
|
198 by (transfer, induct_tac n, auto) |
|
199 |
|
200 lemma starP2_eq_iff: "( *p2* (op =)) = (op =)" |
|
201 by transfer (rule refl) |
|
202 |
|
203 lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)" |
|
204 by (simp add: starP2_eq_iff) |
|
205 |
|
206 lemma nonempty_nat_set_Least_mem: |
|
207 "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S" |
|
208 by (erule LeastI) |
|
209 |
|
210 lemma nonempty_set_star_has_least: |
|
211 "!!S::nat set star. Iset S \<noteq> {} ==> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m" |
|
212 apply (transfer empty_def) |
|
213 apply (rule_tac x="LEAST n. n \<in> S" in bexI) |
|
214 apply (simp add: Least_le) |
|
215 apply (rule LeastI_ex, auto) |
|
216 done |
|
217 |
|
218 lemma nonempty_InternalNatSet_has_least: |
|
219 "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m" |
|
220 apply (clarsimp simp add: InternalSets_def starset_n_def) |
|
221 apply (erule nonempty_set_star_has_least) |
|
222 done |
|
223 |
|
224 text{* Goldblatt page 129 Thm 11.3.2*} |
|
225 lemma internal_induct_lemma: |
|
226 "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |] |
|
227 ==> Iset X = (UNIV:: hypnat set)" |
|
228 apply (transfer UNIV_def) |
|
229 apply (rule equalityI [OF subset_UNIV subsetI]) |
|
230 apply (induct_tac x, auto) |
|
231 done |
|
232 |
|
233 lemma internal_induct: |
|
234 "[| X \<in> InternalSets; (0::hypnat) \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |] |
|
235 ==> X = (UNIV:: hypnat set)" |
|
236 apply (clarsimp simp add: InternalSets_def starset_n_def) |
|
237 apply (erule (1) internal_induct_lemma) |
|
238 done |
|
239 |
|
240 |
|
241 end |
|