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