Theory HyperDef

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

section ‹Construction of Hyperreals Using Ultrafilters›

theory HyperDef
  imports Complex_Main HyperNat
begin

type_synonym hypreal = "real star"

abbreviation hypreal_of_real :: "real ⇒ real star"
  where "hypreal_of_real ≡ star_of"

abbreviation hypreal_of_hypnat :: "hypnat ⇒ hypreal"
  where "hypreal_of_hypnat ≡ of_hypnat"

definition omega :: hypreal  ("ω")
  where "ω = star_n (λn. real (Suc n))"
    ― ‹an infinite number ‹= [<1, 2, 3, …>]››

definition epsilon :: hypreal  ("ε")
  where "ε = star_n (λn. inverse (real (Suc n)))"
    ― ‹an infinitesimal number ‹= [<1, 1/2, 1/3, …>]››


subsection ‹Real vector class instances›

instantiation star :: (scaleR) scaleR
begin
  definition star_scaleR_def [transfer_unfold]: "scaleR r ≡ *f* (scaleR r)"
  instance ..
end

lemma Standard_scaleR [simp]: "x ∈ Standard ⟹ scaleR r x ∈ Standard"
  by (simp add: star_scaleR_def)

lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
  by transfer (rule refl)

instance star :: (real_vector) real_vector
proof
  fix a b :: real
  show "⋀x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
    by transfer (rule scaleR_right_distrib)
  show "⋀x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
    by transfer (rule scaleR_left_distrib)
  show "⋀x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
    by transfer (rule scaleR_scaleR)
  show "⋀x::'a star. scaleR 1 x = x"
    by transfer (rule scaleR_one)
qed

instance star :: (real_algebra) real_algebra
proof
  fix a :: real
  show "⋀x y::'a star. scaleR a x * y = scaleR a (x * y)"
    by transfer (rule mult_scaleR_left)
  show "⋀x y::'a star. x * scaleR a y = scaleR a (x * y)"
    by transfer (rule mult_scaleR_right)
qed

instance star :: (real_algebra_1) real_algebra_1 ..

instance star :: (real_div_algebra) real_div_algebra ..

instance star :: (field_char_0) field_char_0 ..

instance star :: (real_field) real_field ..

lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
  by (unfold of_real_def, transfer, rule refl)

lemma Standard_of_real [simp]: "of_real r ∈ Standard"
  by (simp add: star_of_real_def)

lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
  by transfer (rule refl)

lemma of_real_eq_star_of [simp]: "of_real = star_of"
proof
  show "of_real r = star_of r" for r :: real
    by transfer simp
qed

lemma Reals_eq_Standard: "(ℝ :: hypreal set) = Standard"
  by (simp add: Reals_def Standard_def)


subsection ‹Injection from \<^typ>‹hypreal››

definition of_hypreal :: "hypreal ⇒ 'a::real_algebra_1 star"
  where [transfer_unfold]: "of_hypreal = *f* of_real"

lemma Standard_of_hypreal [simp]: "r ∈ Standard ⟹ of_hypreal r ∈ Standard"
  by (simp add: of_hypreal_def)

lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0"
  by transfer (rule of_real_0)

lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1"
  by transfer (rule of_real_1)

lemma of_hypreal_add [simp]: "⋀x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y"
  by transfer (rule of_real_add)

lemma of_hypreal_minus [simp]: "⋀x. of_hypreal (- x) = - of_hypreal x"
  by transfer (rule of_real_minus)

lemma of_hypreal_diff [simp]: "⋀x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y"
  by transfer (rule of_real_diff)

lemma of_hypreal_mult [simp]: "⋀x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y"
  by transfer (rule of_real_mult)

lemma of_hypreal_inverse [simp]:
  "⋀x. of_hypreal (inverse x) =
    inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)"
  by transfer (rule of_real_inverse)

lemma of_hypreal_divide [simp]:
  "⋀x y. of_hypreal (x / y) =
    (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)"
  by transfer (rule of_real_divide)

lemma of_hypreal_eq_iff [simp]: "⋀x y. (of_hypreal x = of_hypreal y) = (x = y)"
  by transfer (rule of_real_eq_iff)

lemma of_hypreal_eq_0_iff [simp]: "⋀x. (of_hypreal x = 0) = (x = 0)"
  by transfer (rule of_real_eq_0_iff)


subsection ‹Properties of \<^term>‹starrel››

lemma lemma_starrel_refl [simp]: "x ∈ starrel `` {x}"
  by (simp add: starrel_def)

lemma starrel_in_hypreal [simp]: "starrel``{x}∈star"
  by (simp add: star_def starrel_def quotient_def, blast)

declare Abs_star_inject [simp] Abs_star_inverse [simp]
declare equiv_starrel [THEN eq_equiv_class_iff, simp]


subsection ‹\<^term>‹hypreal_of_real›: the Injection from \<^typ>‹real› to \<^typ>‹hypreal››

lemma inj_star_of: "inj star_of"
  by (rule inj_onI) simp

lemma mem_Rep_star_iff: "X ∈ Rep_star x ⟷ x = star_n X"
  by (cases x) (simp add: star_n_def)

lemma Rep_star_star_n_iff [simp]: "X ∈ Rep_star (star_n Y) ⟷ eventually (λn. Y n = X n) 𝒰"
  by (simp add: star_n_def)

lemma Rep_star_star_n: "X ∈ Rep_star (star_n X)"
  by simp


subsection ‹Properties of \<^term>‹star_n››

lemma star_n_add: "star_n X + star_n Y = star_n (λn. X n + Y n)"
  by (simp only: star_add_def starfun2_star_n)

lemma star_n_minus: "- star_n X = star_n (λn. -(X n))"
  by (simp only: star_minus_def starfun_star_n)

lemma star_n_diff: "star_n X - star_n Y = star_n (λn. X n - Y n)"
  by (simp only: star_diff_def starfun2_star_n)

lemma star_n_mult: "star_n X * star_n Y = star_n (λn. X n * Y n)"
  by (simp only: star_mult_def starfun2_star_n)

lemma star_n_inverse: "inverse (star_n X) = star_n (λn. inverse (X n))"
  by (simp only: star_inverse_def starfun_star_n)

lemma star_n_le: "star_n X ≤ star_n Y = eventually (λn. X n ≤ Y n) 𝒰"
  by (simp only: star_le_def starP2_star_n)

lemma star_n_less: "star_n X < star_n Y = eventually (λn. X n < Y n) 𝒰"
  by (simp only: star_less_def starP2_star_n)

lemma star_n_zero_num: "0 = star_n (λn. 0)"
  by (simp only: star_zero_def star_of_def)

lemma star_n_one_num: "1 = star_n (λn. 1)"
  by (simp only: star_one_def star_of_def)

lemma star_n_abs: "¦star_n X¦ = star_n (λn. ¦X n¦)"
  by (simp only: star_abs_def starfun_star_n)

lemma hypreal_omega_gt_zero [simp]: "0 < ω"
  by (simp add: omega_def star_n_zero_num star_n_less)


subsection ‹Existence of Infinite Hyperreal Number›

text ‹Existence of infinite number not corresponding to any real number.
  Use assumption that member \<^term>‹𝒰› is not finite.›

lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ≠ ω"
proof -
  have False if "∀⇩F n in 𝒰. x = 1 + real n" for x
  proof -
    have "finite {n::nat. x = 1 + real n}"
      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute nat_le_linear nat_le_real_less)
    then show False
      using FreeUltrafilterNat.finite that by blast
  qed
  then show ?thesis
    by (auto simp add: omega_def star_of_def star_n_eq_iff)
qed

text ‹Existence of infinitesimal number also not corresponding to any real number.›

lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ≠ ε"
proof -
  have False if "∀⇩F n in 𝒰. x = inverse (1 + real n)" for x
  proof -
    have "finite {n::nat. x = inverse (1 + real n)}"
      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute inverse_inverse_eq linear nat_le_real_less of_nat_Suc) 
    then show False
      using FreeUltrafilterNat.finite that by blast
  qed
  then show ?thesis
    by (auto simp: epsilon_def star_of_def star_n_eq_iff)
qed

lemma epsilon_ge_zero [simp]: "0 ≤ ε"
  by (simp add: epsilon_def star_n_zero_num star_n_le)

lemma epsilon_not_zero: "ε ≠ 0"
  using hypreal_of_real_not_eq_epsilon by force

lemma epsilon_inverse_omega: "ε = inverse ω"
  by (simp add: epsilon_def omega_def star_n_inverse)

lemma epsilon_gt_zero: "0 < ε"
  by (simp add: epsilon_inverse_omega)


subsection ‹Embedding the Naturals into the Hyperreals›

abbreviation hypreal_of_nat :: "nat ⇒ hypreal"
  where "hypreal_of_nat ≡ of_nat"

lemma SNat_eq: "Nats = {n. ∃N. n = hypreal_of_nat N}"
  by (simp add: Nats_def image_def)

text ‹Naturals embedded in hyperreals: is a hyperreal c.f. NS extension.›

lemma hypreal_of_nat: "hypreal_of_nat m = star_n (λn. real m)"
  by (simp add: star_of_def [symmetric])

declaration ‹
  K (Lin_Arith.add_simps @{thms star_of_zero star_of_one
      star_of_numeral star_of_add
      star_of_minus star_of_diff star_of_mult}
  #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2]
      star_of_less [THEN iffD2] star_of_eq [THEN iffD2]}
  #> Lin_Arith.add_inj_const (\<^const_name>‹StarDef.star_of›, \<^typ>‹real ⇒ hypreal›))
›

simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) ≤ n" | "(m::hypreal) = n") =
  ‹K Lin_Arith.simproc›


subsection ‹Exponentials on the Hyperreals›

lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
  for r :: hypreal
  by (rule power_0)

lemma hpowr_Suc [simp]: "r ^ (Suc n) = r * (r ^ n)"
  for r :: hypreal
  by (rule power_Suc)

lemma hrealpow: "star_n X ^ m = star_n (λn. (X n::real) ^ m)"
  by (induct m) (auto simp: star_n_one_num star_n_mult)

lemma hrealpow_sum_square_expand:
  "(x + y) ^ Suc (Suc 0) =
    x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0))) * x * y"
  for x y :: hypreal
  by (simp add: distrib_left distrib_right)

lemma power_hypreal_of_real_numeral:
  "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
  by simp
declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w

lemma power_hypreal_of_real_neg_numeral:
  "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
  by simp
declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w


subsection ‹Powers with Hypernatural Exponents›

text ‹Hypernatural powers of hyperreals.›
definition pow :: "'a::power star ⇒ nat star ⇒ 'a star"  (infixr "pow" 80)
  where hyperpow_def [transfer_unfold]: "R pow N = ( *f2* (^)) R N"

lemma Standard_hyperpow [simp]: "r ∈ Standard ⟹ n ∈ Standard ⟹ r pow n ∈ Standard"
  by (simp add: hyperpow_def)

lemma hyperpow: "star_n X pow star_n Y = star_n (λn. X n ^ Y n)"
  by (simp add: hyperpow_def starfun2_star_n)

lemma hyperpow_zero [simp]: "⋀n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
  by transfer simp

lemma hyperpow_not_zero: "⋀r n. r ≠ (0::'a::{field} star) ⟹ r pow n ≠ 0"
  by transfer (rule power_not_zero)

lemma hyperpow_inverse: "⋀r n. r ≠ (0::'a::field star) ⟹ inverse (r pow n) = (inverse r) pow n"
  by transfer (rule power_inverse [symmetric])

lemma hyperpow_hrabs: "⋀r n. ¦r::'a::{linordered_idom} star¦ pow n = ¦r pow n¦"
  by transfer (rule power_abs [symmetric])

lemma hyperpow_add: "⋀r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
  by transfer (rule power_add)

lemma hyperpow_one [simp]: "⋀r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
  by transfer (rule power_one_right)

lemma hyperpow_two: "⋀r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
  by transfer (rule power2_eq_square)

lemma hyperpow_gt_zero: "⋀r n. (0::'a::{linordered_semidom} star) < r ⟹ 0 < r pow n"
  by transfer (rule zero_less_power)

lemma hyperpow_ge_zero: "⋀r n. (0::'a::{linordered_semidom} star) ≤ r ⟹ 0 ≤ r pow n"
  by transfer (rule zero_le_power)

lemma hyperpow_le: "⋀x y n. (0::'a::{linordered_semidom} star) < x ⟹ x ≤ y ⟹ x pow n ≤ y pow n"
  by transfer (rule power_mono [OF _ order_less_imp_le])

lemma hyperpow_eq_one [simp]: "⋀n. 1 pow n = (1::'a::monoid_mult star)"
  by transfer (rule power_one)

lemma hrabs_hyperpow_minus [simp]: "⋀(a::'a::linordered_idom star) n. ¦(-a) pow n¦ = ¦a pow n¦"
  by transfer (rule abs_power_minus)

lemma hyperpow_mult: "⋀r s n. (r * s::'a::comm_monoid_mult star) pow n = (r pow n) * (s pow n)"
  by transfer (rule power_mult_distrib)

lemma hyperpow_two_le [simp]: "⋀r. (0::'a::{monoid_mult,linordered_ring_strict} star) ≤ r pow 2"
  by (auto simp add: hyperpow_two zero_le_mult_iff)

lemma hyperpow_two_hrabs [simp]: "¦x::'a::linordered_idom star¦ pow 2 = x pow 2"
  by (simp add: hyperpow_hrabs)

lemma hyperpow_two_gt_one: "⋀r::'a::linordered_semidom star. 1 < r ⟹ 1 < r pow 2"
  by transfer simp

lemma hyperpow_two_ge_one: "⋀r::'a::linordered_semidom star. 1 ≤ r ⟹ 1 ≤ r pow 2"
  by transfer (rule one_le_power)

lemma two_hyperpow_ge_one [simp]: "(1::hypreal) ≤ 2 pow n"
  by (metis hyperpow_eq_one hyperpow_le one_le_numeral zero_less_one)

lemma hyperpow_minus_one2 [simp]: "⋀n. (- 1) pow (2 * n) = (1::hypreal)"
  by transfer (rule power_minus1_even)

lemma hyperpow_less_le: "⋀r n N. (0::hypreal) ≤ r ⟹ r ≤ 1 ⟹ n < N ⟹ r pow N ≤ r pow n"
  by transfer (rule power_decreasing [OF order_less_imp_le])

lemma hyperpow_SHNat_le:
  "0 ≤ r ⟹ r ≤ (1::hypreal) ⟹ N ∈ HNatInfinite ⟹ ∀n∈Nats. r pow N ≤ r pow n"
  by (auto intro!: hyperpow_less_le simp: HNatInfinite_iff)

lemma hyperpow_realpow: "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
  by transfer (rule refl)

lemma hyperpow_SReal [simp]: "(hypreal_of_real r) pow (hypnat_of_nat n) ∈ ℝ"
  by (simp add: Reals_eq_Standard)

lemma hyperpow_zero_HNatInfinite [simp]: "N ∈ HNatInfinite ⟹ (0::hypreal) pow N = 0"
  by (drule HNatInfinite_is_Suc, auto)

lemma hyperpow_le_le: "(0::hypreal) ≤ r ⟹ r ≤ 1 ⟹ n ≤ N ⟹ r pow N ≤ r pow n"
  by (metis hyperpow_less_le le_less)

lemma hyperpow_Suc_le_self2: "(0::hypreal) ≤ r ⟹ r < 1 ⟹ r pow (n + (1::hypnat)) ≤ r"
  by (metis hyperpow_less_le hyperpow_one hypnat_add_self_le le_less)

lemma hyperpow_hypnat_of_nat: "⋀x. x pow hypnat_of_nat n = x ^ n"
  by transfer (rule refl)

lemma of_hypreal_hyperpow:
  "⋀x n. of_hypreal (x pow n) = (of_hypreal x::'a::{real_algebra_1} star) pow n"
  by transfer (rule of_real_power)

end