1(* Title: HOL/Nonstandard_Analysis/Star.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 1998 University of Cambridge 4 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 5*) 6 7section \<open>Star-Transforms in Non-Standard Analysis\<close> 8 9theory Star 10 imports NSA 11begin 12 13definition \<comment> \<open>internal sets\<close> 14 starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set" ("*sn* _" [80] 80) 15 where "*sn* As = Iset (star_n As)" 16 17definition InternalSets :: "'a star set set" 18 where "InternalSets = {X. \<exists>As. X = *sn* As}" 19 20definition \<comment> \<open>nonstandard extension of function\<close> 21 is_starext :: "('a star \<Rightarrow> 'a star) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" 22 where "is_starext F f \<longleftrightarrow> 23 (\<forall>x y. \<exists>X \<in> Rep_star x. \<exists>Y \<in> Rep_star y. y = F x \<longleftrightarrow> eventually (\<lambda>n. Y n = f(X n)) \<U>)" 24 25definition \<comment> \<open>internal functions\<close> 26 starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star" ("*fn* _" [80] 80) 27 where "*fn* F = Ifun (star_n F)" 28 29definition InternalFuns :: "('a star => 'b star) set" 30 where "InternalFuns = {X. \<exists>F. X = *fn* F}" 31 32 33subsection \<open>Preamble - Pulling \<open>\<exists>\<close> over \<open>\<forall>\<close>\<close> 34 35text \<open>This proof does not need AC and was suggested by the 36 referee for the JCM Paper: let \<open>f x\<close> be least \<open>y\<close> such 37 that \<open>Q x y\<close>.\<close> 38lemma no_choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f :: 'a \<Rightarrow> nat. \<forall>x. Q x (f x)" 39 by (rule exI [where x = "\<lambda>x. LEAST y. Q x y"]) (blast intro: LeastI) 40 41 42subsection \<open>Properties of the Star-transform Applied to Sets of Reals\<close> 43 44lemma STAR_star_of_image_subset: "star_of ` A \<subseteq> *s* A" 45 by auto 46 47lemma STAR_hypreal_of_real_Int: "*s* X \<inter> \<real> = hypreal_of_real ` X" 48 by (auto simp add: SReal_def) 49 50lemma STAR_star_of_Int: "*s* X \<inter> Standard = star_of ` X" 51 by (auto simp add: Standard_def) 52 53lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> hypreal_of_real y" 54 by auto 55 56lemma lemma_not_starA: "x \<notin> star_of ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> star_of y" 57 by auto 58 59lemma STAR_real_seq_to_hypreal: "\<forall>n. (X n) \<notin> M \<Longrightarrow> star_n X \<notin> *s* M" 60 by (simp add: starset_def star_of_def Iset_star_n FreeUltrafilterNat.proper) 61 62lemma STAR_singleton: "*s* {x} = {star_of x}" 63 by simp 64 65lemma STAR_not_mem: "x \<notin> F \<Longrightarrow> star_of x \<notin> *s* F" 66 by transfer 67 68lemma STAR_subset_closed: "x \<in> *s* A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<in> *s* B" 69 by (erule rev_subsetD) simp 70 71text \<open>Nonstandard extension of a set (defined using a constant 72 sequence) as a special case of an internal set.\<close> 73lemma starset_n_starset: "\<forall>n. As n = A \<Longrightarrow> *sn* As = *s* A" 74 by (drule fun_eq_iff [THEN iffD2]) (simp add: starset_n_def starset_def star_of_def) 75 76 77subsection \<open>Theorems about nonstandard extensions of functions\<close> 78 79text \<open>Nonstandard extension of a function (defined using a 80 constant sequence) as a special case of an internal function.\<close> 81 82lemma starfun_n_starfun: "F = (\<lambda>n. f) \<Longrightarrow> *fn* F = *f* f" 83 by (simp add: starfun_n_def starfun_def star_of_def) 84 85text \<open>Prove that \<open>abs\<close> for hypreal is a nonstandard extension of abs for real w/o 86 use of congruence property (proved after this for general 87 nonstandard extensions of real valued functions). 88 89 Proof now Uses the ultrafilter tactic!\<close> 90 91lemma hrabs_is_starext_rabs: "is_starext abs abs" 92 proof - 93 have "\<exists>f\<in>Rep_star (star_n h). \<exists>g\<in>Rep_star (star_n k). (star_n k = \<bar>star_n h\<bar>) = (\<forall>\<^sub>F n in \<U>. (g n::'a) = \<bar>f n\<bar>)" 94 for x y :: "'a star" and h k 95 by (metis (full_types) Rep_star_star_n star_n_abs star_n_eq_iff) 96 then show ?thesis 97 unfolding is_starext_def by (metis star_cases) 98qed 99 100 101text \<open>Nonstandard extension of functions.\<close> 102 103lemma starfun: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))" 104 by (rule starfun_star_n) 105 106lemma starfun_if_eq: "\<And>w. w \<noteq> star_of x \<Longrightarrow> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w" 107 by transfer simp 108 109text \<open>Multiplication: \<open>( *f) x ( *g) = *(f x g)\<close>\<close> 110lemma starfun_mult: "\<And>x. ( *f* f) x * ( *f* g) x = ( *f* (\<lambda>x. f x * g x)) x" 111 by transfer (rule refl) 112declare starfun_mult [symmetric, simp] 113 114text \<open>Addition: \<open>( *f) + ( *g) = *(f + g)\<close>\<close> 115lemma starfun_add: "\<And>x. ( *f* f) x + ( *f* g) x = ( *f* (\<lambda>x. f x + g x)) x" 116 by transfer (rule refl) 117declare starfun_add [symmetric, simp] 118 119text \<open>Subtraction: \<open>( *f) + -( *g) = *(f + -g)\<close>\<close> 120lemma starfun_minus: "\<And>x. - ( *f* f) x = ( *f* (\<lambda>x. - f x)) x" 121 by transfer (rule refl) 122declare starfun_minus [symmetric, simp] 123 124(*FIXME: delete*) 125lemma starfun_add_minus: "\<And>x. ( *f* f) x + -( *f* g) x = ( *f* (\<lambda>x. f x + -g x)) x" 126 by transfer (rule refl) 127declare starfun_add_minus [symmetric, simp] 128 129lemma starfun_diff: "\<And>x. ( *f* f) x - ( *f* g) x = ( *f* (\<lambda>x. f x - g x)) x" 130 by transfer (rule refl) 131declare starfun_diff [symmetric, simp] 132 133text \<open>Composition: \<open>( *f) \<circ> ( *g) = *(f \<circ> g)\<close>\<close> 134lemma starfun_o2: "(\<lambda>x. ( *f* f) (( *f* g) x)) = *f* (\<lambda>x. f (g x))" 135 by transfer (rule refl) 136 137lemma starfun_o: "( *f* f) \<circ> ( *f* g) = ( *f* (f \<circ> g))" 138 by (transfer o_def) (rule refl) 139 140text \<open>NS extension of constant function.\<close> 141lemma starfun_const_fun [simp]: "\<And>x. ( *f* (\<lambda>x. k)) x = star_of k" 142 by transfer (rule refl) 143 144text \<open>The NS extension of the identity function.\<close> 145lemma starfun_Id [simp]: "\<And>x. ( *f* (\<lambda>x. x)) x = x" 146 by transfer (rule refl) 147 148text \<open>The Star-function is a (nonstandard) extension of the function.\<close> 149lemma is_starext_starfun: "is_starext ( *f* f) f" 150proof - 151 have "\<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = (*f* f) x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))" 152 for x y 153 by (metis (mono_tags) Rep_star_star_n star_cases star_n_eq_iff starfun_star_n) 154 then show ?thesis 155 by (auto simp: is_starext_def) 156qed 157 158text \<open>Any nonstandard extension is in fact the Star-function.\<close> 159lemma is_starfun_starext: 160 assumes "is_starext F f" 161 shows "F = *f* f" 162 proof - 163 have "F x = (*f* f) x" 164 if "\<forall>x y. \<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = F x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))" for x 165 by (metis that mem_Rep_star_iff star_n_eq_iff starfun_star_n) 166 with assms show ?thesis 167 by (force simp add: is_starext_def) 168qed 169 170lemma is_starext_starfun_iff: "is_starext F f \<longleftrightarrow> F = *f* f" 171 by (blast intro: is_starfun_starext is_starext_starfun) 172 173text \<open>Extended function has same solution as its standard version 174 for real arguments. i.e they are the same for all real arguments.\<close> 175lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)" 176 by (rule starfun_star_of) 177 178lemma starfun_approx: "( *f* f) (star_of a) \<approx> star_of (f a)" 179 by simp 180 181text \<open>Useful for NS definition of derivatives.\<close> 182lemma starfun_lambda_cancel: "\<And>x'. ( *f* (\<lambda>h. f (x + h))) x' = ( *f* f) (star_of x + x')" 183 by transfer (rule refl) 184 185lemma starfun_lambda_cancel2: "( *f* (\<lambda>h. f (g (x + h)))) x' = ( *f* (f \<circ> g)) (star_of x + x')" 186 unfolding o_def by (rule starfun_lambda_cancel) 187 188lemma starfun_mult_HFinite_approx: 189 "( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> l \<in> HFinite \<Longrightarrow> m \<in> HFinite \<Longrightarrow> 190 ( *f* (\<lambda>x. f x * g x)) x \<approx> l * m" 191 for l m :: "'a::real_normed_algebra star" 192 using approx_mult_HFinite by auto 193 194lemma starfun_add_approx: "( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> ( *f* (%x. f x + g x)) x \<approx> l + m" 195 by (auto intro: approx_add) 196 197text \<open>Examples: \<open>hrabs\<close> is nonstandard extension of \<open>rabs\<close>, 198 \<open>inverse\<close> is nonstandard extension of \<open>inverse\<close>.\<close> 199 200text \<open>Can be proved easily using theorem \<open>starfun\<close> and 201 properties of ultrafilter as for inverse below we 202 use the theorem we proved above instead.\<close> 203 204lemma starfun_rabs_hrabs: "*f* abs = abs" 205 by (simp only: star_abs_def) 206 207lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse x" 208 by (simp only: star_inverse_def) 209 210lemma starfun_inverse: "\<And>x. inverse (( *f* f) x) = ( *f* (\<lambda>x. inverse (f x))) x" 211 by transfer (rule refl) 212declare starfun_inverse [symmetric, simp] 213 214lemma starfun_divide: "\<And>x. ( *f* f) x / ( *f* g) x = ( *f* (\<lambda>x. f x / g x)) x" 215 by transfer (rule refl) 216declare starfun_divide [symmetric, simp] 217 218lemma starfun_inverse2: "\<And>x. inverse (( *f* f) x) = ( *f* (\<lambda>x. inverse (f x))) x" 219 by transfer (rule refl) 220 221text \<open>General lemma/theorem needed for proofs in elementary topology of the reals.\<close> 222lemma starfun_mem_starset: "\<And>x. ( *f* f) x \<in> *s* A \<Longrightarrow> x \<in> *s* {x. f x \<in> A}" 223 by transfer simp 224 225text \<open>Alternative definition for \<open>hrabs\<close> with \<open>rabs\<close> function applied 226 entrywise to equivalence class representative. 227 This is easily proved using @{thm [source] starfun} and ns extension thm.\<close> 228lemma hypreal_hrabs: "\<bar>star_n X\<bar> = star_n (\<lambda>n. \<bar>X n\<bar>)" 229 by (simp only: starfun_rabs_hrabs [symmetric] starfun) 230 231text \<open>Nonstandard extension of set through nonstandard extension 232 of \<open>rabs\<close> function i.e. \<open>hrabs\<close>. A more general result should be 233 where we replace \<open>rabs\<close> by some arbitrary function \<open>f\<close> and \<open>hrabs\<close> 234 by its NS extenson. See second NS set extension below.\<close> 235lemma STAR_rabs_add_minus: "*s* {x. \<bar>x + - y\<bar> < r} = {x. \<bar>x + -star_of y\<bar> < star_of r}" 236 by transfer (rule refl) 237 238lemma STAR_starfun_rabs_add_minus: 239 "*s* {x. \<bar>f x + - y\<bar> < r} = {x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}" 240 by transfer (rule refl) 241 242text \<open>Another characterization of Infinitesimal and one of \<open>\<approx>\<close> relation. 243 In this theory since \<open>hypreal_hrabs\<close> proved here. Maybe move both theorems??\<close> 244lemma Infinitesimal_FreeUltrafilterNat_iff2: 245 "star_n X \<in> Infinitesimal \<longleftrightarrow> (\<forall>m. eventually (\<lambda>n. norm (X n) < inverse (real (Suc m))) \<U>)" 246 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def hnorm_def 247 star_of_nat_def starfun_star_n star_n_inverse star_n_less) 248 249lemma HNatInfinite_inverse_Infinitesimal [simp]: 250 assumes "n \<in> HNatInfinite" 251 shows "inverse (hypreal_of_hypnat n) \<in> Infinitesimal" 252proof (cases n) 253 case (star_n X) 254 then have *: "\<And>k. \<forall>\<^sub>F n in \<U>. k < X n" 255 using HNatInfinite_FreeUltrafilterNat assms by blast 256 have "\<forall>\<^sub>F n in \<U>. inverse (real (X n)) < inverse (1 + real m)" for m 257 using * [of "Suc m"] by (auto elim!: eventually_mono) 258 then show ?thesis 259 using star_n by (auto simp: of_hypnat_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff2) 260qed 261 262lemma approx_FreeUltrafilterNat_iff: 263 "star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)" 264 (is "?lhs = ?rhs") 265proof - 266 have "?lhs = (star_n X - star_n Y \<approx> 0)" 267 using approx_minus_iff by blast 268 also have "... = ?rhs" 269 by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff mem_infmal_iff star_n_diff) 270 finally show ?thesis . 271qed 272 273lemma approx_FreeUltrafilterNat_iff2: 274 "star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse (real (Suc m))) \<U>)" 275 (is "?lhs = ?rhs") 276proof - 277 have "?lhs = (star_n X - star_n Y \<approx> 0)" 278 using approx_minus_iff by blast 279 also have "... = ?rhs" 280 by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff2 mem_infmal_iff star_n_diff) 281 finally show ?thesis . 282qed 283 284lemma inj_starfun: "inj starfun" 285proof (rule inj_onI) 286 show "\<phi> = \<psi>" if eq: "*f* \<phi> = *f* \<psi>" for \<phi> \<psi> :: "'a \<Rightarrow> 'b" 287 proof (rule ext, rule ccontr) 288 show False 289 if "\<phi> x \<noteq> \<psi> x" for x 290 by (metis eq that star_of_inject starfun_eq) 291 qed 292qed 293 294end 295