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