Quelle  Star.thy

(*  Title:      HOL/Nonstandard_Analysis/Star.thy
  Author: Jacques D. Fleuriot
  Copyright: 1998 University of Cambridge
  Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)

section ‹Star-Transforms in Non-Standard Analysis›

theory Star
  imports NSA
begin

definition  🍋 ‹internal sets›
  starset_n :: "(nat ==> 'a set) ==> 'a star set"
    (‹(‹open_block notation=‹prefix starset_n›\›*sn* _)› [80] 80)
  where "*sn* As = Iset (star_n As)"

definition InternalSets :: "'a star set set"
  where "InternalSets = {X. ∃As. X = *sn* As}"

definition  🍋 ‹nonstandard extension of function›
  is_starext :: "('a star ==> 'a star) ==> ('a ==> 'a) ==> bool"
  where "is_starext F f ⟷
    (∀x y. ∃X ∈ Rep_star x. ∃Y ∈ Rep_star y. y = F x ⟷ eventually (λn. Y n = f(X n)) U)"

definition  🍋 ‹internal functions›
  starfun_n :: "(nat ==> 'a ==> 'b) ==> 'a star ==> 'b star"
    (‹(‹open_block notation=‹prefix starfun_n›\›*fn* _)› [80] 80)
  where "*fn* F = Ifun (star_n F)"

definition InternalFuns :: "('a star => 'b star) set"
  where "InternalFuns = {X. ∃F. X = *fn* F}"


subsection ‹Preamble - Pulling ‹∃› over ‹∀›\›

text ‹This proof does not need AC and was suggested by the
  referee for the JCM Paper: let ‹f x› be least ‹y› such
  that ‹Q x y›.›
lemma no_choice: "∀x. ∃y. Q x y ==> ∃f :: 'a ==> nat. ∀x. Q x (f x)"
  by (rule exI [where x = "λx. LEAST y. Q x y"]) (blast intro: LeastI)


subsection ‹Properties of the Star-transform Applied to Sets of Reals›

lemma STAR_star_of_image_subset: "star_of ` A ⊆ *s* A"
  by auto

lemma STAR_hypreal_of_real_Int: "*s* X ∩ ℝ = hypreal_of_real ` X"
  by (auto simp add: SReal_def)

lemma STAR_star_of_Int: "*s* X ∩ Standard = star_of ` X"
  by (auto simp add: Standard_def)

lemma lemma_not_hyprealA: "x ∉ hypreal_of_real ` A ==> ∀y ∈ A. x ≠ hypreal_of_real y"
  by auto

lemma lemma_not_starA: "x ∉ star_of ` A ==> ∀y ∈ A. x ≠ star_of y"
  by auto

lemma STAR_real_seq_to_hypreal: "∀n. (X n) ∉ M ==> star_n X ∉ *s* M"
  by (simp add: starset_def star_of_def Iset_star_n FreeUltrafilterNat.proper)

lemma STAR_singleton: "*s* {x} = {star_of x}"
  by simp

lemma STAR_not_mem: "x ∉ F ==> star_of x ∉ *s* F"
  by transfer

lemma STAR_subset_closed: "x ∈ *s* A ==> A ⊆ B ==> x ∈ *s* B"
  by (erule rev_subsetD) simp

text ‹Nonstandard extension of a set (defined using a constant
  sequence) as a special case of an internal set.›
lemma starset_n_starset: "∀n. As n = A ==> *sn* As = *s* A"
  by (drule fun_eq_iff [THEN iffD2]) (simp add: starset_n_def starset_def star_of_def)


subsection ‹Theorems about nonstandard extensions of functions›

text ‹Nonstandard extension of a function (defined using a
  constant sequence) as a special case of an internal function.›

lemma starfun_n_starfun: "F = (λn. f) ==> *fn* F = *f* f"
  by (simp add: starfun_n_def starfun_def star_of_def)

text ‹Prove that ‹abs› for hypreal is a nonstandard extension of abs for real w/o
  use of congruence property (proved after this for general
  nonstandard extensions of real valued functions).
 
  Proof now Uses the ultrafilter tactic!›

lemma hrabs_is_starext_rabs: "is_starext abs abs"
  proof -
  have "∃f∈Rep_star (star_n h). ∃g∈Rep_star (star_n k). (star_n k = ∣star_n h∣) = (∀🪙F n in U. (g n::'a) = ∣f n∣)"
    for x y :: "'a star" and h k
    by (metis (full_types) Rep_star_star_n star_n_abs star_n_eq_iff)
  then show ?thesis
    unfolding is_starext_def by (metis star_cases)
qed


text ‹Nonstandard extension of functions.›

lemma starfun: "( *f* f) (star_n X) = star_n (λn. f (X n))"
  by (rule starfun_star_n)

lemma starfun_if_eq: "∧w. w ≠ star_of x ==> ( *f* (λz. if z = x then a else g z)) w = ( *f* g) w"
  by transfer simp

text ‹Multiplication: ‹( *f) x ( *g) = *(f x g)›\›
lemma starfun_mult: "∧x. ( *f* f) x * ( *f* g) x = ( *f* (λx. f x * g x)) x"
  by transfer (rule refl)
declare starfun_mult [symmetric, simp]

text ‹Addition: ‹( *f) + ( *g) = *(f + g)›\›
lemma starfun_add: "∧x. ( *f* f) x + ( *f* g) x = ( *f* (λx. f x + g x)) x"
  by transfer (rule refl)
declare starfun_add [symmetric, simp]

text ‹Subtraction: ‹( *f) + -( *g) = *(f + -g)›\›
lemma starfun_minus: "∧x. - ( *f* f) x = ( *f* (λx. - f x)) x"
  by transfer (rule refl)
declare starfun_minus [symmetric, simp]

(*FIXME: delete*)
lemma starfun_add_minus: "∧x. ( *f* f) x + -( *f* g) x = ( *f* (λx. f x + -g x)) x"
  by transfer (rule refl)
declare starfun_add_minus [symmetric, simp]

lemma starfun_diff: "∧x. ( *f* f) x - ( *f* g) x = ( *f* (λx. f x - g x)) x"
  by transfer (rule refl)
declare starfun_diff [symmetric, simp]

text ‹Composition: ‹( *f) ∘ ( *g) = *(f ∘ g)›\ lemma starfun_o2: "(λx. ( *f* f) (( *f* g) x)) = *f* (λx. f (g x))"
  by transfer (rule refl)

lemma starfun_o: "( *f* f) ∘ ( *f* g) = ( *f* (f ∘ g))"
  by (transfer o_def) (rule refl)

text ‹NS extension of constant function.›
lemma starfun_const_fun [simp]: "∧x. ( *f* (λx. k)) x = star_of k"
  by transfer (rule refl)

text ‹The NS extension of the identity function.›
lemma starfun_Id [simp]: "∧x. ( *f* (λx. x)) x = x"
  by transfer (rule refl)

text ‹The Star-function is a (nonstandard) extension of the function.›
lemma is_starext_starfun: "is_starext ( *f* f) f"
proof -
  have "∃X∈Rep_star x. ∃Y∈Rep_star y. (y = (*f* f) x) = (∀🪙F n in U. Y n = f (X n))"
    for x y
    by (metis (mono_tags) Rep_star_star_n star_cases star_n_eq_iff starfun_star_n)
  then show ?thesis
    by (auto simp: is_starext_def)
qed

text ‹Any nonstandard extension is in fact the Star-function.›
lemma is_starfun_starext:
  assumes "is_starext F f"
  shows "F = *f* f"
  proof -
  have "F x = (*f* f) x"
    if "∀x y. ∃X∈Rep_star x. ∃Y∈Rep_star y. (y = F x) = (∀🪙F n in U. Y n = f (X n))" for x
    by (metis that mem_Rep_star_iff star_n_eq_iff starfun_star_n)
  with assms show ?thesis
    by (force simp add: is_starext_def)
qed

lemma is_starext_starfun_iff: "is_starext F f ⟷ F = *f* f"
  by (blast intro: is_starfun_starext is_starext_starfun)

text ‹Extended function has same solution as its standard version
  for real arguments. i.e they are the same for all real arguments.›
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
  by (rule starfun_star_of)

lemma starfun_approx: "( *f* f) (star_of a) ≈ star_of (f a)"
  by simp

text ‹Useful for NS definition of derivatives.›
lemma starfun_lambda_cancel: "∧x'. ( *f* (λh. f (x + h))) x' = ( *f* f) (star_of x + x')"
  by transfer (rule refl)

lemma starfun_lambda_cancel2: "( *f* (λh. f (g (x + h)))) x' = ( *f* (f ∘ g)) (star_of x + x')"
  unfolding o_def by (rule starfun_lambda_cancel)

lemma starfun_mult_HFinite_approx:
  "( *f* f) x ≈ l ==> ( *f* g) x ≈ m ==> l ∈ HFinite ==> m ∈ HFinite ==>
    ( *f* (λx. f x * g x)) x ≈ l * m"
  for l m :: "'a::real_normed_algebra star"
  using approx_mult_HFinite by auto

lemma starfun_add_approx: "( *f* f) x ≈ l ==> ( *f* g) x ≈ m ==> ( *f* (%x. f x + g x)) x ≈ l + m"
  by (auto intro: approx_add)

text ‹Examples: ‹hrabs› is nonstandard extension of ‹rabs›,
  ‹inverse› is nonstandard extension of ‹inverse›.›

text ‹Can be proved easily using theorem ‹starfun› and
  properties of ultrafilter as for inverse below we
  use the theorem we proved above instead.›

lemma starfun_rabs_hrabs: "*f* abs = abs"
  by (simp only: star_abs_def)

lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse x"
  by (simp only: star_inverse_def)

lemma starfun_inverse: "∧x. inverse (( *f* f) x) = ( *f* (λx. inverse (f x))) x"
  by transfer (rule refl)
declare starfun_inverse [symmetric, simp]

lemma starfun_divide: "∧x. ( *f* f) x / ( *f* g) x = ( *f* (λx. f x / g x)) x"
  by transfer (rule refl)
declare starfun_divide [symmetric, simp]

lemma starfun_inverse2: "∧x. inverse (( *f* f) x) = ( *f* (λx. inverse (f x))) x"
  by transfer (rule refl)

text ‹General lemma/theorem needed for proofs in elementary topology of the reals.›
lemma starfun_mem_starset: "∧x. ( *f* f) x ∈ *s* A ==> x ∈ *s* {x. f x ∈ A}"
  by transfer simp

text ‹Alternative definition for ‹hrabs› with ‹rabs› function applied
  entrywise to equivalence class representative.
  This is easily proved using @{thm [source] starfun} and ns extension thm.›
lemma hypreal_hrabs: "∣star_n X∣ = star_n (λn. ∣X n∣)"
  by (simp only: starfun_rabs_hrabs [symmetric] starfun)

text ‹Nonstandard extension of set through nonstandard extension
  of ‹rabs› function i.e. ‹hrabs›. A more general result should be
  where we replace ‹rabs› by some arbitrary function ‹f› and ‹hrabs›
  by its NS extenson. See second NS set extension below.›
lemma STAR_rabs_add_minus: "*s* {x. ∣x + - y∣ < r} = {x. ∣x + -star_of y∣ < star_of r}"
  by transfer (rule refl)

lemma STAR_starfun_rabs_add_minus:
  "*s* {x. ∣f x + - y∣ < r} = {x. ∣( *f* f) x + -star_of y∣ < star_of r}"
  by transfer (rule refl)

text ‹Another characterization of Infinitesimal and one of ‹≈› relation.
  In this theory since ‹hypreal_hrabs› proved here. Maybe move both theorems??›
lemma Infinitesimal_FreeUltrafilterNat_iff2:
  "star_n X ∈ Infinitesimal ⟷ (∀m. eventually (λn. norm (X n) < inverse (real (Suc m))) U)"
  by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def hnorm_def
      star_of_nat_def starfun_star_n star_n_inverse star_n_less)

lemma HNatInfinite_inverse_Infinitesimal [simp]:
  assumes "n ∈ HNatInfinite"
  shows "inverse (hypreal_of_hypnat n) ∈ Infinitesimal"
proof (cases n)
  case (star_n X)
  then have *: "∧k. ∀🪙F n in U. k < X n"
    using HNatInfinite_FreeUltrafilterNat assms by blast
  have "∀🪙F n in U. inverse (real (X n)) < inverse (1 + real m)" for m
    using * [of "Suc m"] by (auto elim!: eventually_mono)
  then show ?thesis
    using star_n by (auto simp: of_hypnat_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff2)
qed

lemma approx_FreeUltrafilterNat_iff:
  "star_n X ≈ star_n Y ⟷ (∀r>0. eventually (λn. norm (X n - Y n) < r) U)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (star_n X - star_n Y ≈ 0)"
    using approx_minus_iff by blast
  also have "... = ?rhs"
    by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff mem_infmal_iff star_n_diff)
  finally show ?thesis .
qed

lemma approx_FreeUltrafilterNat_iff2:
  "star_n X ≈ star_n Y ⟷ (∀m. eventually (λn. norm (X n - Y n) < inverse (real (Suc m))) U)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (star_n X - star_n Y ≈ 0)"
    using approx_minus_iff by blast
  also have "... = ?rhs"
    by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff2 mem_infmal_iff star_n_diff)
  finally show ?thesis .
qed

lemma inj_starfun: "inj starfun"
proof (rule inj_onI)
  show "φ = ψ" if eq: "*f* φ = *f* ψ" for φ ψ :: "'a ==> 'b"
  proof (rule ext, rule ccontr)
    show False
      if "φ x ≠ ψ x" for x
      by (metis eq that star_of_inject starfun_eq)
  qed
qed

end