Theory Star

theory Star
imports NSA
(*  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"  ("*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)) 𝒰)"

definition   ‹internal functions›
  starfun_n :: "(nat ⇒ 'a ⇒ 'b) ⇒ 'a star ⇒ 'b star"  ("*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 lemma_Compl_eq: "- {n. X n = xa} = {n. X n ≠ xa}"
  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: "∀n. F n = f ⟹ *fn* F = *f* f"
  apply (drule fun_eq_iff [THEN iffD2])
  apply (simp add: starfun_n_def starfun_def star_of_def)
  done

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"
  apply (simp add: is_starext_def, safe)
  apply (rule_tac x=x in star_cases)
  apply (rule_tac x=y in star_cases)
  apply (unfold star_n_def, auto)
  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
  apply (fold star_n_def)
  apply (unfold star_abs_def starfun_def star_of_def)
  apply (simp add: Ifun_star_n star_n_eq_iff)
  done


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 ‹This is trivial, given ‹starfun_Id›.›
lemma starfun_Idfun_approx: "x ≈ star_of a ⟹ ( *f* (λx. x)) x ≈ star_of a"
  by (simp only: starfun_Id)

text ‹The Star-function is a (nonstandard) extension of the function.›
lemma is_starext_starfun: "is_starext ( *f* f) f"
  apply (auto simp: is_starext_def)
  apply (rule_tac x = x in star_cases)
  apply (rule_tac x = y in star_cases)
  apply (auto intro!: bexI [OF _ Rep_star_star_n] simp: starfun star_n_eq_iff)
  done

text ‹Any nonstandard extension is in fact the Star-function.›
lemma is_starfun_starext: "is_starext F f ⟹ F = *f* f"
  apply (simp add: is_starext_def)
  apply (rule ext)
  apply (rule_tac x = x in star_cases)
  apply (drule_tac x = x in spec)
  apply (drule_tac x = "( *f* f) x" in spec)
  apply (auto simp add: starfun_star_n)
  apply (simp add: star_n_eq_iff [symmetric])
  apply (simp add: starfun_star_n [of f, symmetric])
  done

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

text ‹Extented 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"
  apply (drule (3) approx_mult_HFinite)
  apply (auto intro: approx_HFinite [OF _ approx_sym])
  done

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))) 𝒰)"
  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]:
  "n ∈ HNatInfinite ⟹ inverse (hypreal_of_hypnat n) ∈ Infinitesimal"
  apply (cases n)
  apply (auto simp: of_hypnat_def starfun_star_n star_n_inverse
    HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
  apply (drule_tac x = "Suc m" in spec)
  apply (auto elim!: eventually_mono)
  done

lemma approx_FreeUltrafilterNat_iff:
  "star_n X ≈ star_n Y ⟷ (∀r>0. eventually (λn. norm (X n - Y n) < r) 𝒰)"
  apply (subst approx_minus_iff)
  apply (rule mem_infmal_iff [THEN subst])
  apply (simp add: star_n_diff)
  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
  done

lemma approx_FreeUltrafilterNat_iff2:
  "star_n X ≈ star_n Y ⟷ (∀m. eventually (λn. norm (X n - Y n) < inverse (real (Suc m))) 𝒰)"
  apply (subst approx_minus_iff)
  apply (rule mem_infmal_iff [THEN subst])
  apply (simp add: star_n_diff)
  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
  done

lemma inj_starfun: "inj starfun"
  apply (rule inj_onI)
  apply (rule ext, rule ccontr)
  apply (drule_tac x = "star_n (λn. xa)" in fun_cong)
  apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
  done

end