# Theory Star

theory Star
imports NSA
```(*  Title:      HOL/Nonstandard_Analysis/Star.thy
Author:     Jacques D. Fleuriot
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"

lemma STAR_star_of_Int: "*s* X ∩ Standard = star_of ` X"

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 (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)
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)

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)

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 (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 (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"

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)

"*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])
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])