Theory AuxiliaryNSA

(*  Title:  AuxiliaryNSA.thy
    Author: Jacques D. Fleuriot, University of Edinburgh, 2026
*)

section‹Various supporting lemmas›

theory  AuxiliaryNSA
imports "HOL-Nonstandard_Analysis.HSeries" "Real_Power.Log" 
begin

text‹These results can be moved to the indicated theories.›

text‹StarDef.thy lemmas›
lemma Iset_star_of_empty [simp]: "Iset(star_of {}) = {}"
by (transfer empty_def) simp

lemma Iset_star_n_empty [simp]: "Iset (star_n (λn. {})) = {}"
  by (simp add: star_of_def [symmetric])

lemma Iset_eq_cancel:
  "(Iset (star_n X) = Iset (star_n Y)) = (eventually (λn. X n = Y n) 𝒰)"
  by (simp add: transfer_set_eq)

lemma Collect_starP_starset_eq: "{x. (*p* P) x} = *s* {x. P x}"
by transfer simp

text‹Hypernat.thy lemmas›

lemma Nats_hypnat_of_nat_iff: "(n ∈ Nats) = (∃m. n = hypnat_of_nat m)"
  by (auto simp add: Nats_def)

lemma HNatInfinite_add_one_cancel:
   "N + 1 ∈ HNatInfinite ⟹ N ∈ HNatInfinite"
  by (drule HNatInfinite_diff [of _ 1], auto)

lemma of_hypnat_of_nat [simp]: "of_hypnat(hypnat_of_nat n) = of_nat n"
  by (metis of_hypnat_def star_of_nat_def starfun_star_of)

lemma of_nat_hypreal_of_hypnat:
     "of_nat n = of_hypnat (hypnat_of_nat n)"
  by simp

lemma hSuc_eq_add_one:
  "⋀n. hSuc n = n + 1"
by transfer simp

lemma HNatInfinite_hSuc_diff_one [simp]: 
  "N ∈ HNatInfinite ⟹ hSuc (N - 1) = N"
by (metis hSuc_eq_add_one hypnat_le_add_diff_inverse2 one_le_HNatInfinite)

lemma HNatInfinite_atLeastAtMost_hSuc:
  "N ∈ HNatInfinite ⟹ {M..<N} = {M..<hSuc(N - 1)}"
by (metis HNatInfinite_hSuc_diff_one)

text‹HyperDef.thy lemmas›

lemma hypreal_of_nat_less_hypreal_of_hypnat_iff:
      "⋀a b.(hypreal_of_nat a < of_hypnat b) = (hypnat_of_nat a < b)"
by (auto simp only: of_nat_hypreal_of_hypnat of_hypnat_less_iff)

lemma hypreal_of_nat_le_hypreal_of_hypnat_iff:
      "⋀a b.(hypreal_of_nat a ≤ hypreal_of_hypnat b) = (hypnat_of_nat a ≤  b)"
  by (auto simp only: of_nat_hypreal_of_hypnat of_hypnat_le_iff)

lemma hyperpow_zero [simp]: "x pow 0 = 1"
by (metis hyperpow_hypnat_of_nat power_0 star_of_simps(9))

lemma hyperpow_of_nat: "⋀x. x pow of_nat n = x ^ n"
by transfer simp

lemma hyperpow_hSuc_zero [simp]:
  "⋀N. (0::'a::{power, semiring_0} star) pow hSuc N = 0"
by transfer simp

lemma starfun_power: "⋀n. (*f* (^) x) n = star_of x pow n"
by transfer simp

lemma hyperpow_diff:
  "⋀x n k. n ≥ k ⟹ x ≠ 0 ⟹ ((x::'a::field star) pow n)/(x pow k) = x pow (n - k)"
  by transfer (metis power_diff)

lemma hyperpow_divide:
  "⋀x y n. ((x::'a::field star)/y) pow n = (x pow n)/(y pow n)"
by transfer (metis power_divide)

lemma hyperpow_diff_cancel:
  "k ≤ n ⟹ x pow k * (x::'a::monoid_mult star) pow (n - k) = x pow n"
  by (simp add: hyperpow_add [symmetric])

lemma hyperpow_0_left:
  "⋀n. 0 pow n = (if n = 0 then 1 else (0::'a::{power, semiring_1} star))"
by transfer (simp add: power_0_left)

lemma hyperpow_eq_0_iff [simp]:
  "⋀x n. (x pow n = 0) ⟷ 
           (x = (0::'a::{mult_zero,zero_neq_one,semiring_1_no_zero_divisors,power} star) ∧ n ≠ 0)"
  by transfer simp

lemma hyperpow_less_zero_eq:
  "⋀x n. (x pow n < (0::'a::{linordered_idom} star)) = (¬ 2 dvd n ∧ x < 0)"
by transfer (metis power_less_zero_eq)

lemma star_n_divide: "star_n X / star_n Y = star_n (λn. X n / Y n)"
  by (simp add: star_divide_def starfun2_star_n)

text‹NSA.thy lemmas›

lemma approx_zero_abs_zero_iff [iff]:
  "(abs x ≈ 0) = ((x::hypreal) ≈ 0)"
by (metis Infinitesimal_hrabs_iff mem_infmal_iff)

lemma Infinitesimal_divide_HFinite:
  "⟦ (x::'a::real_normed_div_algebra star) ∈ Infinitesimal; y ∈ HFinite - Infinitesimal ⟧ 
       ⟹ x/y ∈ Infinitesimal"
by (metis HFinite_inverse2 Infinitesimal_HFinite_mult divide_inverse)

lemma approx_1_not_Infinitesimal:
  "x ≈ (1 ::'a::real_normed_div_algebra star) ⟹ x ∉ Infinitesimal"
  using approx_sym approx_trans mem_infmal_iff one_not_Infinitesimal 
  by blast

lemma HFinite_add_imp_HFinite:
  "⟦ x ≥ (0::hypreal); y ≥ 0; x + y ∈ HFinite ⟧ ⟹ y ∈ HFinite"
  using HFinite_not_HInfinite HInfinite_add_ge_zero2 not_HFinite_HInfinite 
  by blast

lemma Infinitesimal_hrealpow_cancel [simp]:
  assumes "n > 0" 
  shows "(x ^ n ∈ Infinitesimal) = ((x::'a::real_normed_div_algebra star) ∈ Infinitesimal)"
proof (insert assms, induct n)
  case 0
  then show ?case 
    by simp
next
  case (Suc n)
  then show ?case
    using Infinitesimal_mult not_Infinitesimal_mult 
    by force 
qed

lemma hrealpow_approx:
   "⟦ (x::'a::{real_normed_algebra, one, monoid_mult} star) ≈ b;  b ∈ HFinite ⟧ ⟹ x ^ n ≈ b ^ n"
by (induct n, auto dest: hrealpow_HFinite approx_mult_HFinite [of x])

lemma hrealpow_approx_one:
   "(x::'a::{real_normed_algebra, one, monoid_mult} star) ≈ 1 ⟹ x ^ n ≈ 1"
by (auto dest: hrealpow_approx)

lemma zero_not_HInfinite [simp]: "0 ∉ HInfinite"
by (simp add: HFinite_not_HInfinite)

lemma HInfinite_hyperpow_not_zero:
  "(x::'a::{real_normed_field} star) ∈ HInfinite ⟹ x pow n ≠ 0"
  by (metis hyperpow_not_zero zero_not_HInfinite)

lemma HFinite_divide:
  "⟦ (x::'a::real_normed_div_algebra star) ∈ HFinite; y ∉ Infinitesimal ⟧ ⟹ x/y ∈ HFinite"
by (metis HFinite_mult Infinitesimal_inverse_HFinite divide_inverse)

lemma HFinite_hyperpow_HFinite:
  "⟦ (x::'a::{monoid_mult, real_normed_algebra} star) ∈ HFinite; n ∈ ℕ ⟧ ⟹ x pow n ∈ HFinite"
  by (metis Nats_cases hrealpow_HFinite hyperpow_hypnat_of_nat of_nat_eq_star_of)

lemma hyperpow_approx:
      assumes HFinite_a: "a ∈ HFinite" 
      and approx_ab: "(a::hypreal) ≈ b"
      shows "a pow of_nat n ≈ b pow of_nat n"
by (metis HFinite_a approx_HFinite approx_ab hrealpow_approx hyperpow_of_nat)

lemma Infinitesimal_approx_hyperpow:
      assumes Infinitesimal_a: "a ∈ Infinitesimal" 
      and approx_ab: "(a::hypreal) ≈ b"
      shows "a pow n ≈ b pow n"
  by (metis Infinitesimal_a Infinitesimal_approx Infinitesimal_hyperpow Infinitesimal_monad_zero_iff 
      approx_ab approx_mem_monad_zero approx_monad_iff hyperpow_zero hypnat_neq0_conv)

lemma hnorm_hypreal_of_hypnat [simp]: 
  "⋀n. hnorm (of_hypnat n::'a::real_normed_algebra_1 star) = of_hypnat n"
  by transfer simp

lemma HFinite_of_nat [simp]: "of_nat n ∈ HFinite"
by (metis HFinite_star_of star_of_nat_def)

lemma HInfinite_def2: "HInfinite = {x. ∀n ∈ Nats. hypreal_of_hypnat n < hnorm x}"
proof (auto simp add: HInfinite_def SHNat_eq SReal_def)
   fix x::"'a :: real_normed_vector star" and N
   assume "∀r. (∃ra. r = hypreal_of_real ra) ⟶ r < hnorm x" 
   then show "hypreal_of_nat N < hnorm x"
     using star_of_nat_def by blast
next
   fix x::"'a :: real_normed_vector star" and ra 
   assume "∀n. (∃N. n = hypnat_of_nat N) ⟶ hypreal_of_hypnat n < hnorm x"
   then show "hypreal_of_real ra < hnorm x"
     by (metis of_nat_hypreal_of_hypnat less_trans reals_Archimedean2 
          star_of_less star_of_nat_def)
 qed

lemma HFinite_def2: "HFinite = {x. ∃n ∈ Nats. hnorm x < hypreal_of_hypnat n}"
proof (auto simp add: HFinite_def)
  fix x::"'a :: real_normed_vector star" and r
  assume r: "r ∈ ℝ" and hnormx: "hnorm x < r"
  then obtain s where "r = of_real s"
    using Reals_cases by blast
  moreover obtain n where "s < of_nat n"
    using reals_Archimedean2 by blast
  ultimately have "hnorm x < hypreal_of_hypnat (of_nat n)"
    using hnormx
    by (metis dual_order.strict_trans of_hypnat_def of_nat_eq_star_of of_real_eq_star_of star_of_less
        starfun_star_of) 
  then show "∃n∈ℕ. hnorm x < hypreal_of_hypnat n"
    by fastforce
next
  fix x::"'a :: real_normed_vector star" and n
  assume n: "n ∈ ℕ" and "hnorm x < hypreal_of_hypnat n"
  then have "hnorm x < hypreal_of_hypnat n"
    by blast
  moreover have "hypreal_of_hypnat n ∈ ℝ"
    using n by (auto simp add: SHNat_eq)
  ultimately show "∃r∈ℝ. hnorm x < r"
    by fastforce
qed

lemma HFinite_less_Nat_Ex:
  "(x::hypreal) ∈ HFinite ⟹ ∃n∈Nats. x < n"
  unfolding Nats_def HFinite_def2
  by simp (metis abs_ge_self order_less_le xt1(10))

lemma HNatInfinite_of_hypnat_HInfinite: 
  "x ∈ HNatInfinite ⟹ (of_hypnat x :: 'a::real_normed_algebra_1 star) ∈ HInfinite"
proof (auto simp add: HInfinite_def2 Nats_def)
  fix n
  assume "x ∈ HNatInfinite" 
  then show "hypreal_of_nat n < hypreal_of_hypnat x"
    by (metis hypreal_of_nat_less_hypreal_of_hypnat_iff star_of_less_HNatInfinite)
qed

lemma HInfinite_ge_HNatInfinite:
  "⟦ n ∈ HNatInfinite; hypreal_of_hypnat n ≤ x ⟧ ⟹ x ∈ HInfinite"
  using HInfinite_ge_HInfinite HNatInfinite_of_hypnat_HInfinite of_hypnat_0_le_iff 
  by blast

lemma HNatInfinite_of_hypnat_HInfinite_iff:
  "(of_hypnat n :: 'a::real_normed_algebra_1 star) ∈ HInfinite = (n ∈ HNatInfinite)"
proof 
  assume "(of_hypnat n :: 'a::real_normed_algebra_1 star) ∈ HInfinite" 
  then show "n ∈ HNatInfinite" 
    by (auto simp add: HInfinite_def2 HNatInfinite_def)
next 
  assume "n ∈ HNatInfinite" 
  then show "(of_hypnat n :: 'a::real_normed_algebra_1 star) ∈ HInfinite" 
    using HNatInfinite_of_hypnat_HInfinite by blast
qed

lemma HNatInfinite_inverse_of_hypnat_Infinitesimal_iff:
  "N ≠ 0 ⟹ (1/hypreal_of_hypnat N ∈ Infinitesimal) = (N ∈ HNatInfinite)"
  by (simp add: HNatInfinite_of_hypnat_HInfinite_iff divide_inverse inverse_Infinitesimal_iff_HInfinite)

lemma Nats_hypreal_of_hypnat_HFinite:
  "n ∈ Nats ⟹ of_hypnat n ∈ HFinite"
  using Nats_hypnat_of_nat_iff by auto

lemma approx_divide_HFinite_diff_Infinitesimal: 
   "⟦(x :: 'a::{real_normed_div_algebra, field} star) ≈ y; 
     z ∈ HFinite - Infinitesimal
    ⟧ ⟹ x/z ≈ y/z"
by (metis HFinite_inverse2 approx_mult1 divide_inverse)

lemma HFinite_diff:
  "⟦ x ∈ HFinite; y ∈ HFinite ⟧ ⟹ x - y ∈ HFinite"
by (metis HFinite_add HFinite_minus_iff add_uminus_conv_diff)

lemma Infinitesimal_interval2a:
     "⟦ e ∈ Infinitesimal; e' ∈ Infinitesimal;
        hnorm e' ≤ hnorm x ; hnorm x ≤ hnorm e ⟧ ⟹ x ∈ Infinitesimal"
  by (auto simp add: Infinitesimal_def)

lemma Infinitesimal_HInfinite_divide:
  "⟦ (x::'a::{real_normed_div_algebra, field} star) ∈ HFinite; y ∈ HInfinite ⟧ ⟹ x/y ∈ Infinitesimal"
by (simp add: HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse)

lemma approx_divide_HInfinite: 
  "⟦(x :: 'a::{real_normed_div_algebra, field} star) ≈ y; z ∈ HInfinite⟧ ⟹ x/z ≈ y/z"
by (metis Infinitesimal_HInfinite_divide approx_minus_iff approx_star_of_HFinite 
          diff_divide_distrib mem_infmal_iff star_zero_def)

lemma approx_1_mult_HFinite_HFinite:
      assumes approx_1: "x ≈ (1 ::'a::real_normed_div_algebra star)" 
      and HFinite_prod: "x*y ∈ HFinite"
      shows "y ∈ HFinite"
proof (rule ccontr)
  assume "y ∉ HFinite" 
  then have HInfinite_y: "y ∈ HInfinite" 
    using HFinite_HInfinite_iff 
    by blast 
  have HFinite_x: "x ∈ HFinite" 
    by (metis approx_1 approx_star_of_HFinite star_one_def) 
  have "x ∉ Infinitesimal" 
    using approx_1 approx_1_not_Infinitesimal 
    by blast
  then have "x * y ∈ HInfinite" 
    using  HInfinite_y HFinite_x HInfinite_HFinite_not_Infinitesimal_mult2 
           HInfinite_diff_HFinite_Infinitesimal_disj  
    by blast 
  thus "False" 
    using HFinite_not_HInfinite HFinite_prod 
    by blast 
qed

text‹Star.thy lemmas›

instance star :: (semiring_modulo) semiring_modulo
  by (intro_classes, transfer) (simp add: div_mult_mod_eq)

declare of_bool_def [transfer_unfold] 

instance star :: (semiring_parity) semiring_parity
proof
  show "⋀a ::'a :: semiring_parity star. a mod 2 = of_bool (¬ 2 dvd a)"
    by transfer (simp add: mod2_eq_if)
next
  show "¬ (2::'a :: semiring_parity star) dvd 1"
    by transfer simp
next 
  show "⋀a ::'a :: semiring_parity star. 2 dvd a ⟹ (1 + a) div 2 = a div 2"
    by transfer simp
qed

lemma starfun_starfun_n_eq:
  "*f* f = *fn* (λn. f)"
  by (metis starfun_n_starfun)

lemma starfun_n_zero:
  "(*fn* (λm n::'b. 0::'a::zero)) = (λn. star_of 0)"
  by (metis starfun_const_fun starfun_starfun_n_eq)

lemma InternalFuns_starfun_n [simp]: "*fn* f ∈ InternalFuns"
by (force simp add: InternalFuns_def)

lemma InternalFuns_starfun [simp]: "*f* f ∈ InternalFuns"
by (simp add: starfun_starfun_n_eq)

lemma InternalFuns_starfun2 [simp]: "(*f2* f) a ∈ InternalFuns"
  by (metis InternalFuns_starfun_n star_cases starfun2_def starfun_n_def)

lemma starfun_n_hyperpow: "(λn. (*f2* (^)) ((*fn* f) n) ((*fn* g) n)) z = (*fn* (λ i x. (f i x) ^ (g i x))) z"
proof (cases z)
  case (star_n X)
   assume Z: "z = star_n X"
   then have "(λn. (*f2* (^)) ((*fn* f) n) ((*fn* g) n)) z = (*f2* (^)) ((*fn* f) (star_n X)) ((*fn* g) (star_n X))"
     by simp
   also have "… = (*f2* (^)) (star_n (λn. f n (X n))) (star_n (λn. g n (X n)))"
     by (simp add: Ifun_star_n starfun_n_def)
   also have "… = star_n (λn. f n (X n) ^ g n (X n))"
     by (simp add: starfun2_star_n)
   also have "… =  (*fn* (λi x. f i x ^ g i x)) (star_n X)"
     by (simp add: Ifun_star_n starfun_n_def)
   finally show ?thesis using Z [symmetric] by simp
 qed

lemma InternalFuns_hSuc [simp]: "hSuc ∈ InternalFuns"
by (simp add: hSuc_def)

lemma InternalSets_starset_n [simp]: "*sn* X ∈ InternalSets"
by (auto simp add: InternalSets_def)

lemma InternalSets_singleton [simp]: "{x} ∈ InternalSets"
proof -
  {fix X assume "x = star_n X" 
    have "{star_n X} = Iset (star_n (λn. {X n}))"
    proof
       show "{star_n X} ⊆ Iset (star_n (λn. {X n}))"
         by (simp add: Iset_star_n) 
    next 
      show "Iset (star_n (λn. {X n})) ⊆ {star_n X}" 
      proof 
        fix y
        assume yin: "y ∈ Iset (star_n (λn. {X n}))" 
        then show  "y ∈ {star_n X}"
          using yin 
          by (auto intro: star_cases [of y] 
                   simp add: Iset_def starP2_star_n star_n_eq_iff)
        qed
      qed
   }
   then show ?thesis
     by (force intro: star_cases simp add: InternalSets_def starset_n_def)
 qed

lemma starset_n_singleton [simp]: "*sn* (λn. {X n}) =  {star_n X}"
proof  (auto simp add: starset_n_def)
  fix x
  assume xinX: "x ∈ Iset (star_n (λn. {X n}))"
  then show "x = star_n X"
  proof (cases x)
    case (star_n Y)
    then show ?thesis 
      using xinX by (auto simp add: Iset_star_n star_n_eq_iff)
  qed  
next
  show "star_n X ∈ Iset (star_n (λn. {X n}))"
    by (simp add: Iset_star_n)
qed

lemma starset_n_singleton2:"*sn* (λn. {X n}) = {x. x = star_n X}"
by simp

lemma starset_n_empty [simp]: "*sn* (λn. {}) = {}"
by (simp add: starset_n_def )

lemma InternalSets_empty [simp]: "{} ∈ InternalSets"
  by (metis InternalSets_starset_n starset_n_empty)

lemma starset_n_subset: 
   "(*sn* X ⊆ *sn* Y) = (eventually (λn. X n ⊆ Y n) 𝒰)"
proof 
  assume "*sn* X ⊆ *sn* Y" 
  then have "∀x∈Iset (star_n X). x ∈ Iset (star_n Y)"
    by (simp add: set_mp starset_n_def)
  moreover 
   have "∀Xa. star_n Xa ∈ Iset (star_n Y) = (∀⇩F n in 𝒰. Xa n ∈ Y n)"
     by (simp add: Iset_star_n)
   ultimately have "∀⇩F n in 𝒰. ∀x∈X n. x ∈ Y n" 
     by (force intro: transfer_ball [THEN meta_eq_to_obj_eq, THEN iffD1])
   then show "∀⇩F n in 𝒰. X n ⊆ Y n" 
     by (simp add: subset_eq)
 next
   assume  subsetF: "∀⇩F n in 𝒰. X n ⊆ Y n" 
   show "*sn* X ⊆ *sn* Y"
   proof 
     fix x
     assume xX: "x ∈ *sn* X"
     show "x ∈ *sn* Y"
     proof (cases x)
       case (star_n X)
       then show ?thesis 
         using xX subsetF by (auto elim: eventually_elim2 simp add: Iset_star_n starset_n_def)
     qed
   qed
 qed

lemma starfun_n_mult_star_n_right:
  "(*fn* F) n * star_n X = (*fn* (λn m. F n m * X n)) n"
  by (cases n, simp add: Ifun_star_n star_n_mult starfun_n_def)

lemma starfun_n_mult_star_n_left:
  "star_n X  * (*fn* F) n = (*fn* (λn m. X n * F n m)) n"
  by (cases n, simp add: Ifun_star_n star_n_mult starfun_n_def)

lemma starfun_n_diff:
     "(*fn* f) z - (*fn* g) z = (*fn* (λi x. f i x - g i x)) z"
  by (cases z, simp add:  Ifun_star_n star_n_minus star_n_diff starfun_n_def)

lemma starfun_n_inverse: "inverse ((*fn* f) x) = (*fn* (λi x. inverse ((f i) x))) x"
  by (cases x, simp add:  Ifun_star_n star_n_minus star_n_inverse starfun_n_def)

lemma InternalFuns_const_fun [simp]:
  "(λn. c) ∈ InternalFuns"
proof (cases c, simp add: InternalFuns_def)
  case (star_n X)
  have "(λn. c) = *fn* (λm n. X m)" 
  proof 
    fix n :: "'c star"
    obtain N where "n = star_n N"
      using star_cases by blast 
    then show "c = (*fn* (λm n. X m)) n"
      by (simp add: star_n starfun_n_def transfer_Ifun) 
  qed
  then show "∃F. (λn. star_n X) = *fn* F"
    using star_n by blast 
qed

lemma starfun_n_divide:
     "((*fn* f) z ::'a::division_ring star)/ (*fn* g) z = (*fn* (λi x. f i x / g i x)) z"
  by (cases z, simp add: Ifun_star_n divide_inverse starfun_n_def star_n_inverse star_n_mult)

lemma InternalFuns_divide:
  "⟦ f ∈ InternalFuns; g ∈ InternalFuns ⟧ 
       ⟹ (λn. (f n ::'a::division_ring star)/g n) ∈ InternalFuns"
by (auto simp add: InternalFuns_def starfun_n_divide)

lemma InternalFuns_id_fun [simp]: "(λn. n) ∈ InternalFuns"
proof -
   have id: "(λn. n) = (*fn* (λn m. m))" 
     by (metis ext starfun_Id starfun_starfun_n_eq)
   then show ?thesis
     using InternalFuns_def by blast
 qed

(* This proof could be nicer, I guess *)
lemma FreeUltrafilterNat_star_n_Infinitesimal:
  assumes "eventually (λn. norm (X n) < inverse(Suc n)) 𝒰" 
  shows "star_n X ∈ Infinitesimal"
proof (auto simp add: Infinitesimal_def hnorm_def starfun Reals_def 
       star_of_def star_less_def starP2_star_n star_n_zero_num)
  fix r
  assume "∀⇩F n in 𝒰. 0 < (r::real)" 
  moreover have "eventually (λn. inverse (real (Suc n)) < r) 𝒰" 
    using FreeUltrafilterNat_inverse_real_of_posnat calculation transfer_bool by blast 
  ultimately show "∀⇩F n in 𝒰. norm (X n) < r" using assms 
    by (force elim: eventually_elim2)
qed

lemma starset_n_atLeastLessThan_eq:
  "*sn* (λn. {(X n)..<(Y n)}) = {star_n X..<star_n Y}"
proof (auto simp add: starset_n_def)
  fix x
  assume x: "x ∈ Iset (star_n (λn. {X n..<Y n}))" 
  then show "star_n X ≤ x"
  proof (cases x)
    case (star_n X)
    then show ?thesis 
      using x by (simp add: Iset_star_n eventually_mono star_n star_n_le)  
  qed
next
  fix x
  assume x: "x ∈ Iset (star_n (λn. {X n..<Y n}))" 
  then show "x < star_n Y"
  proof (cases x)
    case (star_n X)
    then show ?thesis 
      using x by (simp add: Iset_star_n eventually_mono star_n_less) 
  qed
next
  fix x
  assume x: "star_n X ≤ x" "x < star_n Y"
  then show "x ∈ Iset (star_n (λn. {X n..<Y n}))"
  proof (cases x)
    case (star_n X)
    then show ?thesis 
      using x by (simp add: Iset_star_n starP2_star_n star_n_less 
           star_le_def eventually_conj_iff) 
  qed
qed

lemma starset_n_atLeast_zero_LessThan_eq:
  "*sn* (λn. {0..<(X n)}) = {0..<star_n X}"
by (simp add: starset_n_atLeastLessThan_eq [of "λn. 0"] star_n_zero_num)

lemma starset_atLeastAtMost:
  "{of_nat m .. of_nat n} = *s* {m .. n}"
proof
  show "{of_nat m..of_nat n} ⊆ *s* {m..n}"
  proof 
    have "⋀x. hypnat_of_nat m ≤ x ∧ x ≤ hypnat_of_nat n ⟶ x ∈ *s* {m..n}"
      by (transfer, simp)
    then
    show "⋀x. x ∈ {of_nat m..of_nat n} ⟹ x ∈ *s* {m..n}"
      by simp
  qed
next
  show "*s* {m..n} ⊆ {of_nat m..of_nat n}"
  proof 
    have "⋀x. x ∈ *s* {m..n} ⟹ hypnat_of_nat m ≤ x"
      by (transfer, simp)
    moreover have "⋀x. x ∈ *s* {m..n} ⟹ x ≤ hypnat_of_nat n"
      by (transfer, simp)
    ultimately show "⋀x. x ∈ *s* {m..n} ⟹ x ∈ {of_nat m..of_nat n}"
      by simp
  qed
qed

lemma starset_n_atLeastAtMost:
  "*sn* (λn. {(X n)..(Y n)}) = {star_n X..star_n Y}"
proof (auto simp add: starset_n_def)
  fix x
  assume x_in_ISet: "x ∈ Iset (star_n (λn. {X n..Y n}))"
  have "star_n X ≤ x ∧ x ≤ star_n Y"  
  proof (cases x)
    case (star_n X)
    then show ?thesis 
      using x_in_ISet 
      by (auto simp add: star_le_def starP2_star_n Iset_star_n
             eventually_conj_iff)
  qed
  then show "star_n X ≤ x" and "x ≤ star_n Y"
    by auto
next
  fix x
  assume x_bounds: "star_n X ≤ x" "x ≤ star_n Y"
  then show "x ∈ Iset (star_n (λn. {X n..Y n}))"
  proof (cases x)
    case (star_n X)
    then show ?thesis 
      using x_bounds 
      by (auto simp add: star_le_def starP2_star_n Iset_star_n
             eventually_conj_iff)
  qed
qed

lemma starset_n_atLeast_zero_AtMost:
  "*sn* (λn. {0..(X n)}) = {0..star_n X}"
by (simp add: starset_n_atLeastAtMost [of "λn. 0"] star_n_zero_num)

lemma InternalSets_atLeastLessThan [simp]: "{M..<N} ∈ InternalSets"
  by (metis InternalSets_starset_n star_cases starset_n_atLeastLessThan_eq)


lemma InternalSets_atLeastAtMost [simp]: "{M..N} ∈ InternalSets"
proof -
  have "∃f. {M..N} = *sn* f"
    by (metis star_cases starset_n_atLeastAtMost)
  then show ?thesis
    by (simp add: InternalSets_def)
qed

lemma le_inverse_HNatInfinite_Infinitesimal:
      "⟦n ∈ HNatInfinite; hnorm x ≤ inverse (hypreal_of_hypnat n)⟧ ⟹ x ∈ Infinitesimal"
by (metis HNatInfinite_inverse_Infinitesimal hnorm_le_Infinitesimal)

(* Adapted from a proof by Jessika Rockel*)
lemma InternalFuns_hyperpow: 
    "f ∈ InternalFuns ⟹ (g:: 'a star ⇒ nat star) ∈ InternalFuns  
     ⟹ (λn. f n pow g n) ∈ InternalFuns"
proof (unfold hyperpow_def)
  assume "f ∈ InternalFuns" 
  then obtain f' where F':"f = *fn* f'"
    using InternalFuns_def by auto
  moreover assume"(g:: 'a star ⇒ nat star) ∈ InternalFuns"
  moreover then obtain g' where G':"g = *fn* g'"
    using InternalFuns_def by auto
  ultimately have "(λn. (*f2* (^)) ((*fn* f') n) ((*fn* g') n)) 
                      = (*fn* (λ i x. (f' i x) ^ (g' i x)))" 
    using starfun_n_hyperpow by auto
  thus "(λn. (*f2* (^)) (f n) (g n)) ∈ InternalFuns" 
    using F' G' InternalFuns_starfun_n by auto
qed

lemma InternalFuns_hyperpowf [simp]: 
  "f ∈ InternalFuns ⟹ (λn. x pow (f n)) ∈ InternalFuns"
  by (simp add: InternalFuns_hyperpow)

lemma InternalFuns_hyperpow_simple [simp]: "(λn. x pow n) ∈ InternalFuns"
  by simp

text‹NatStar.thy lemmas›

lemma InternalFuns_add:
  "⟦ f ∈ InternalFuns; g ∈ InternalFuns ⟧ ⟹ (λn. f n + g n) ∈ InternalFuns"
by (auto simp add: InternalFuns_def starfun_n_add)

lemma InternalFuns_mult:
  "⟦ f ∈ InternalFuns; g ∈ InternalFuns ⟧ ⟹ (λn. f n * g n) ∈ InternalFuns"
by (auto simp add: InternalFuns_def starfun_n_mult)

lemma InternalFuns_diff:
  "⟦ f ∈ InternalFuns; g ∈ InternalFuns ⟧ ⟹ (λn. f n - g n) ∈ InternalFuns"
  by (auto simp add: InternalFuns_def starfun_n_diff)

lemma InternalFuns_minus:
  "f ∈ InternalFuns  ⟹ (λn. - f n ) ∈ InternalFuns"
by (auto simp add: InternalFuns_def starfun_n_minus)

lemma InternalFuns_mult_const_left:
  "f ∈ InternalFuns ⟹ (λn. c * f n) ∈ InternalFuns"
by (force dest: InternalFuns_mult [OF InternalFuns_const_fun])

lemma InternalFuns_mult_const_right:
  "f ∈ InternalFuns ⟹ (λn. f n * c) ∈ InternalFuns"
by (force dest: InternalFuns_mult [OF _ InternalFuns_const_fun])

lemma InternalFuns_mult_of_hypnat [simp]:
      "X ∈ InternalFuns ⟹ (λn. of_hypnat n * X n) ∈ InternalFuns"
by (auto simp add: InternalFuns_def of_hypnat_def starfun_starfun_n_eq starfun_n_mult)

lemma finite_InternalSets: 
  assumes "finite X" 
  shows "X ∈ InternalSets"
proof (insert assms, induct set: finite)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case 
    by (auto intro: insert_def [THEN ssubst] intro!: InternalSets_Un)
qed

lemma InternalFuns_of_hypnat: 
  assumes "f ∈ InternalFuns"
  shows "(λn. of_hypnat (f n)) ∈ InternalFuns"
proof (insert assms, auto simp add: InternalFuns_def)
  fix F 
  have "(λn. of_hypnat ((*fn* (F::nat ⇒ 'a ⇒ nat)) n)) = *fn* (λn m. of_nat(F n m))"
  proof 
    fix n
    obtain N where "(n::'a star) = star_n N"
      using star_cases by blast  
    then show " of_hypnat ((*fn* F) n) = (*fn* (λn m. of_nat (F n m))) n"
      by (simp add: starfun_n of_hypnat_def starfun)
  qed
  then show "∃Fa. (λn. of_hypnat ((*fn* F) n)) = *fn* Fa"
    by blast
qed

lemma insert_star_n_starset_n:
  "insert (star_n X) (*sn* A) = *sn* (λn. insert (X n) (A n))"
proof (unfold insert_def)
  have "{x. x = star_n X} ∪ *sn* A = *sn* (λn. {X n} ∪ A n)"
    by (simp only: starset_n_singleton2 [symmetric] starset_n_Un [symmetric])
  then show "{x. x = star_n X} ∪ *sn* A = *sn* (λn. {x. x = X n} ∪ A n)"
    by simp
qed

lemma inj_starfun_n:
  "inj (*fn* f) =  (∀⇩F n in 𝒰. inj (f n))"
proof  
  assume "inj (*fn* f)"
  then have "∀x y. (*fn* f) x = (*fn* f) y ⟶ x = y "
    by (simp add: inj_eq)
  then have "∀Y Ya. ∀⇩F n in 𝒰. f n (Y n) = f n (Ya n) ⟶ Y n = Ya n"
    by (metis  FreeUltrafilterNat.eventually_imp_iff star_n_eq_iff starfun_n)
  then show "∀⇩F n in 𝒰. inj (f n)"
    by (auto simp add: inj_def FreeUltrafilterNat.eventually_all_iff)
next
  assume "∀⇩F n in 𝒰. inj (f n)" 
  then have eventually_inj: "∀Y Ya. ∀⇩F n in 𝒰. f n (Y n) = f n (Ya n) ⟶ Y n = Ya n"
    by (simp add: eventually_mono inj_def) 
  then show "inj (*fn* f)"
  proof(auto simp add: inj_def)
    fix x y
    assume "(*fn* f) x = (*fn* f) y"
    then show "x = y"
      using eventually_inj 
      by (metis not_eventually_impI star_cases star_n_eq_iff starfun_n)
  qed
qed


lemma surj_starfun_n:
  "surj (*fn* f) =  (∀⇩F n in 𝒰. surj (f n))"
proof  
  assume "surj (*fn* f)"
  then have "∀y. ∃x. y = (*fn* f) x"
    by (simp add: surjD)
  then have "∀Y. ∃Ya. ∀⇩F n in 𝒰. Y n = f n (Ya n)"
    by (metis Ifun_star_n star_cases star_n_eq_iff starfun_n_def)
  then have "∀Y. ∀⇩F n in 𝒰. ∃x. Y n = f n x"
    by (simp add: eventually_ex)
  then show "∀⇩F n in 𝒰. surj (f n)"
    by (auto simp add: surj_def FreeUltrafilterNat.eventually_all_iff)
next
  assume "∀⇩F n in 𝒰. surj (f n)" 
  then have eventually_surj: "∀Y. ∃Ya. ∀⇩F n in 𝒰. Y n = f n (Ya n)"
    by (simp add: surj_def FreeUltrafilterNat.eventually_all_iff eventually_ex)
  then show "surj (*fn* f)"
  proof(auto simp add: surj_def)
    fix y 
    show "∃x. y = (*fn* f) x"
      by (metis eventually_surj star_cases star_n_eq_iff starfun_n)
  qed
qed

lemma bij_starfun_n:
  "bij (*fn* f) =  (∀⇩F n in 𝒰. bij (f n))"
  unfolding bij_def by (simp add: eventually_conj_iff inj_starfun_n surj_starfun_n)

lemma
  assumes "bij (*fn* f)" 
  shows "(inv (*fn* f)) = *fn* (λn. inv (f n))"
proof
  have inj_fn: "inj (*fn* f)" 
    using assms bij_betw_def by blast 
  have surj_fn: "surj (*fn* f)" 
    using assms
    by (simp add: bij_betw_def)
  fix x
  have "(*fn* f) ((*fn* (λn. inv (f n))) x) = x"
  proof (cases x)
    case (star_n X)
    then have " ∀⇩F n in 𝒰. f n (inv (f n) (X n)) = X n"
      using surj_fn 
      by (auto simp add:  surj_starfun_n eventually_mono surj_f_inv_f)
    then show ?thesis
      by (simp add: star_n star_n_eq_iff starfun_n) 
  qed
  then show "inv (*fn* f) x = (*fn* (λn. inv (f n))) x"
    by (metis inj_fn inv_f_eq)
qed

lemma starfun_n_o:
  "(λi. (*fn* F) ((*fn* G) i)) = (*fn* (λi m. F i (G i m)))"
proof (rule ext)
  fix i
  show "(*fn* F) ((*fn* G) i) = (*fn* (λi m. F i (G i m))) i"
    by (case_tac i, auto simp add: starfun_n)
qed

lemma starfun_starfun_n_o:
  "(λi. (*f* f) ((*fn* F) i)) = (*fn* (λi m. f (F i m)))"
by (simp add: starfun_starfun_n_eq starfun_n_o)

lemma InternalFuns_o2:
  "f ∈ InternalFuns ⟹ g ∈ InternalFuns ⟹ (λn. f (g n)) ∈ InternalFuns"
  unfolding InternalFuns_def using starfun_n_o by blast

lemma InternalFuns_abs_starfun_n [simp]: 
  "(λi. abs ((*fn* F) i)) ∈ InternalFuns"
by (metis InternalFuns_starfun_n starfun_rabs_hrabs starfun_starfun_n_o)

lemma InternalFuns_abs: 
  "f ∈ InternalFuns ⟹ (λi. abs (f i)) ∈ InternalFuns"
  by (metis InternalFuns_o2 InternalFuns_starfun starfun_rabs_hrabs)

text‹HSEQ.thy lemmas›

(* Move to NSA.thy - not used?*)
lemma LIMSEQ_0_Infinitesimal:
  assumes "X ⇢ 0" 
  shows "star_n X ∈ Infinitesimal"
proof -
  have "∀N∈HNatInfinite. (*f* X) N ≈ 0" 
    using assms LIMSEQ_NSLIMSEQ NSLIMSEQ_D by fastforce 
  then have "∀N∈HNatInfinite.
            ∀n. hnorm ((*f* X) N) < inverse (1 + hypreal_of_nat n)"
    using mem_infmal_iff [symmetric] Infinitesimal_hypreal_of_nat_iff by auto
  then have "∀n. hnorm ((*f* X) whn) < inverse (1 + hypreal_of_nat n)" by force
  then show ?thesis 
    by (auto simp add: hypnat_omega_def starfun Infinitesimal_hypreal_of_nat_iff)
qed

text‹Alternative definitions for exponential and real powers 
     to replace the one in the AFP session eventually.›

lemma powrat_def2: "x pow⇩ℚ r = root (nat (snd(quotient_of r))) (x powi (fst(quotient_of r)))"
proof (cases "r > 0")
  case True
  then have "x ^ nat (fst (quotient_of r)) = x powi fst (quotient_of r)"
    by (metis Fract_quotient_of order_less_le power_int_nonneg_exp quotient_of_denom_pos' zero_le_Fract_iff)
  then show ?thesis
    by (simp add: True powrat_def)
next
  case False
  then have "1 / x ^ nat (- fst (quotient_of r)) = x powi fst (quotient_of r)"
    by (metis Rat_cases add.inverse_inverse linorder_not_le nat_eq_iff2 neg_less_0_iff_less normalize_stable
        power_int_minus_divide power_int_of_nat prod.sel(1) quotient_of_Fract zero_less_Fract_iff)
  then show ?thesis
    by (simp add: False powrat_def)
qed

lemma powrat_powi: "x pow⇩ℚ (of_int n) = x powi n"
  by (simp add: powrat_def2)

lemma real_root_eq_powrat_inverse': "n > 0 ⟹ x pow⇩ℚ (1 / of_nat n) = root n x"
  by (simp add: inverse_eq_divide real_root_eq_powrat_inverse)

lemma "a powa x = lim (λn. a pow⇩ℚ (incseq_of x n))"
  by (simp add: Lim_def powa_def)


text‹Next two proofs by Zuzana Frankovska› 
lemma HNatInfinite_pow_real_Infinitesimal:
  assumes "0 ≤ (x::real)" and "x < 1" and "N ∈ HNatInfinite"
  shows "(star_of x) pow N ≈ 0"
proof -
  have "(*f* (λn. x ^ n)) N ≈ 0" 
    using NSLIMSEQ_def LIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff assms by force
  thus ?thesis using starfun_pow assms by simp
qed

lemma HNatInfinite_pow_Infinitesimal:
  assumes "0 < (x::hypreal)" and "x < 1" and "¬(x ≈ 1)" and "N ∈ HNatInfinite"
  shows "x pow N ≈ 0"
proof -
  from assms have "x ∈ HFinite"
    using HInfinite_gt_zero_gt_one not_HFinite_HInfinite order.asym by blast
  then obtain x' where st_x: "star_of x' ≈ x" 
    using st_SReal st_approx_self SReal_iff by fastforce
  then have "x' ≠ 1" using assms(3) by auto
  then have "x' < 1" using st_x assms(2)
    by (metis star_of_1_le star_of_approx_one_iff approx_le_bound less_imp_le not_less)
  then  obtain y where y: "x' < y ∧ y < 1" 
    using dense by blast
  then have x_less_y: "x < star_of y"
    using st_x 
    by (metis Infinitesimal_add_hypreal_of_real_less approx_sym bex_Infinitesimal_iff2) 
  then have "x pow N ≤ star_of y pow N"
    by (simp add: assms(1) hyperpow_le less_imp_le)
  moreover have "0 < x pow N"
    by (simp add: assms(1) hyperpow_gt_zero)
  moreover have "star_of y pow N ≈ 0"
    using assms(1,4) HNatInfinite_pow_real_Infinitesimal x_less_y y by auto
  ultimately show ?thesis
    using approx_le_bound approx_trans3 less_imp_le by blast 
qed 

lemma Infinitesimal_hyperpow_HNatInfinite:
  assumes "hnorm (x::'a::real_normed_div_algebra star) < 1"
  and "N ∈ HNatInfinite"
  and "¬(hnorm x ≈ 1)"
shows "x pow N ∈ Infinitesimal"
proof -
  have "hnorm x pow N ≈ 0" 
    using HNatInfinite_pow_Infinitesimal assms
    by force
  then show ?thesis
    by (metis Infinitesimal_hnorm_iff hnorm_hyperpow mem_infmal_iff) 
qed

text‹HSeries.thy lemmas›

lemma NSsums_sumhr_HNatInfinite_approx_iff:
  "(f NSsums s) = (∀N∈HNatInfinite. sumhr(0, N, f) ≈ of_real s)"
by (simp add: NSsums_def sumhr_app NSLIMSEQ_def star_of_zero [symmetric] 
       atLeast0LessThan del: star_of_zero)

lemma sumhr_approx: 
  "sumhr (0, M, f) ≈ sumhr (0, N, f) ⟹ sumhr (M, N, f) ≈ 0"
by (metis approx_zero_abs_zero_iff sumhr_hrabs_approx)

end