Theory NatStar

theory NatStar
imports Star
(*  Title:      HOL/Nonstandard_Analysis/NatStar.thy
    Author:     Jacques D. Fleuriot
    Copyright:  1998  University of Cambridge

Converted to Isar and polished by lcp
*)

section ‹Star-transforms for the Hypernaturals›

theory NatStar
  imports Star
begin

lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
  by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)

lemma starset_n_Un: "*sn* (λn. (A n) ∪ (B n)) = *sn* A ∪ *sn* B"
  apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
  apply (rule_tac x=whn in spec, transfer, simp)
  done

lemma InternalSets_Un: "X ∈ InternalSets ⟹ Y ∈ InternalSets ⟹ X ∪ Y ∈ InternalSets"
  by (auto simp add: InternalSets_def starset_n_Un [symmetric])

lemma starset_n_Int: "*sn* (λn. A n ∩ B n) = *sn* A ∩ *sn* B"
  apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
  apply (rule_tac x=whn in spec, transfer, simp)
  done

lemma InternalSets_Int: "X ∈ InternalSets ⟹ Y ∈ InternalSets ⟹ X ∩ Y ∈ InternalSets"
  by (auto simp add: InternalSets_def starset_n_Int [symmetric])

lemma starset_n_Compl: "*sn* ((λn. - A n)) = - ( *sn* A)"
  apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
  apply (rule_tac x=whn in spec, transfer, simp)
  done

lemma InternalSets_Compl: "X ∈ InternalSets ⟹ - X ∈ InternalSets"
  by (auto simp add: InternalSets_def starset_n_Compl [symmetric])

lemma starset_n_diff: "*sn* (λn. (A n) - (B n)) = *sn* A - *sn* B"
  apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
  apply (rule_tac x=whn in spec, transfer, simp)
  done

lemma InternalSets_diff: "X ∈ InternalSets ⟹ Y ∈ InternalSets ⟹ X - Y ∈ InternalSets"
  by (auto simp add: InternalSets_def starset_n_diff [symmetric])

lemma NatStar_SHNat_subset: "Nats ≤ *s* (UNIV:: nat set)"
  by simp

lemma NatStar_hypreal_of_real_Int: "*s* X Int Nats = hypnat_of_nat ` X"
  by (auto simp add: SHNat_eq)

lemma starset_starset_n_eq: "*s* X = *sn* (λn. X)"
  by (simp add: starset_n_starset)

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

lemma InternalSets_UNIV_diff: "X ∈ InternalSets ⟹ UNIV - X ∈ InternalSets"
  apply (subgoal_tac "UNIV - X = - X")
   apply (auto intro: InternalSets_Compl)
  done


subsection ‹Nonstandard Extensions of Functions›

text ‹Example of transfer of a property from reals to hyperreals
  --- used for limit comparison of sequences.›

lemma starfun_le_mono: "∀n. N ≤ n ⟶ f n ≤ g n ⟹
  ∀n. hypnat_of_nat N ≤ n ⟶ ( *f* f) n ≤ ( *f* g) n"
  by transfer

text ‹And another:›
lemma starfun_less_mono:
  "∀n. N ≤ n ⟶ f n < g n ⟹ ∀n. hypnat_of_nat N ≤ n ⟶ ( *f* f) n < ( *f* g) n"
  by transfer

text ‹Nonstandard extension when we increment the argument by one.›

lemma starfun_shift_one: "⋀N. ( *f* (λn. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
  by transfer simp

text ‹Nonstandard extension with absolute value.›
lemma starfun_abs: "⋀N. ( *f* (λn. ¦f n¦)) N = ¦( *f* f) N¦"
  by transfer (rule refl)

text ‹The ‹hyperpow› function as a nonstandard extension of ‹realpow›.›
lemma starfun_pow: "⋀N. ( *f* (λn. r ^ n)) N = hypreal_of_real r pow N"
  by transfer (rule refl)

lemma starfun_pow2: "⋀N. ( *f* (λn. X n ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
  by transfer (rule refl)

lemma starfun_pow3: "⋀R. ( *f* (λr. r ^ n)) R = R pow hypnat_of_nat n"
  by transfer (rule refl)

text ‹The @{term hypreal_of_hypnat} function as a nonstandard extension of
  @{term real_of_nat}.›
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
  by transfer (simp add: fun_eq_iff)

lemma starfun_inverse_real_of_nat_eq:
  "N ∈ HNatInfinite ⟹ ( *f* (λx::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
  apply (subgoal_tac "hypreal_of_hypnat N ≠ 0")
   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
  done

text ‹Internal functions -- some redundancy with ‹*f*› now.›

lemma starfun_n: "( *fn* f) (star_n X) = star_n (λn. f n (X n))"
  by (simp add: starfun_n_def Ifun_star_n)

text ‹Multiplication: ‹( *fn) x ( *gn) = *(fn x gn)››

lemma starfun_n_mult: "( *fn* f) z * ( *fn* g) z = ( *fn* (λi x. f i x * g i x)) z"
  by (cases z) (simp add: starfun_n star_n_mult)

text ‹Addition: ‹( *fn) + ( *gn) = *(fn + gn)››
lemma starfun_n_add: "( *fn* f) z + ( *fn* g) z = ( *fn* (λi x. f i x + g i x)) z"
  by (cases z) (simp add: starfun_n star_n_add)

text ‹Subtraction: ‹( *fn) - ( *gn) = *(fn + - gn)››
lemma starfun_n_add_minus: "( *fn* f) z + -( *fn* g) z = ( *fn* (λi x. f i x + -g i x)) z"
  by (cases z) (simp add: starfun_n star_n_minus star_n_add)


text ‹Composition: ‹( *fn) ∘ ( *gn) = *(fn ∘ gn)››

lemma starfun_n_const_fun [simp]: "( *fn* (λi x. k)) z = star_of k"
  by (cases z) (simp add: starfun_n star_of_def)

lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (λi x. - (f i) x)) x"
  by (cases x) (simp add: starfun_n star_n_minus)

lemma starfun_n_eq [simp]: "( *fn* f) (star_of n) = star_n (λi. f i n)"
  by (simp add: starfun_n star_of_def)

lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) ⟷ f = g"
  by transfer (rule refl)

lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
  "N ∈ HNatInfinite ⟹ ( *f* (%x. inverse (real x))) N ∈ Infinitesimal"
  apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
  apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
  done


subsection ‹Nonstandard Characterization of Induction›

lemma hypnat_induct_obj:
  "⋀n. (( *p* P) (0::hypnat) ∧ (∀n. ( *p* P) n ⟶ ( *p* P) (n + 1))) ⟶ ( *p* P) n"
  by transfer (induct_tac n, auto)

lemma hypnat_induct:
  "⋀n. ( *p* P) (0::hypnat) ⟹ (⋀n. ( *p* P) n ⟹ ( *p* P) (n + 1)) ⟹ ( *p* P) n"
  by transfer (induct_tac n, auto)

lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
  by transfer (rule refl)

lemma starP2_eq_iff2: "( *p2* (λx y. x = y)) X Y ⟷ X = Y"
  by (simp add: starP2_eq_iff)

lemma nonempty_nat_set_Least_mem: "c ∈ S ⟹ (LEAST n. n ∈ S) ∈ S"
  for S :: "nat set"
  by (erule LeastI)

lemma nonempty_set_star_has_least:
  "⋀S::nat set star. Iset S ≠ {} ⟹ ∃n ∈ Iset S. ∀m ∈ Iset S. n ≤ m"
  apply (transfer empty_def)
  apply (rule_tac x="LEAST n. n ∈ S" in bexI)
   apply (simp add: Least_le)
  apply (rule LeastI_ex, auto)
  done

lemma nonempty_InternalNatSet_has_least: "S ∈ InternalSets ⟹ S ≠ {} ⟹ ∃n ∈ S. ∀m ∈ S. n ≤ m"
  for S :: "hypnat set"
  apply (clarsimp simp add: InternalSets_def starset_n_def)
  apply (erule nonempty_set_star_has_least)
  done

text ‹Goldblatt, page 129 Thm 11.3.2.›
lemma internal_induct_lemma:
  "⋀X::nat set star.
    (0::hypnat) ∈ Iset X ⟹ ∀n. n ∈ Iset X ⟶ n + 1 ∈ Iset X ⟹ Iset X = (UNIV:: hypnat set)"
  apply (transfer UNIV_def)
  apply (rule equalityI [OF subset_UNIV subsetI])
  apply (induct_tac x, auto)
  done

lemma internal_induct:
  "X ∈ InternalSets ⟹ (0::hypnat) ∈ X ⟹ ∀n. n ∈ X ⟶ n + 1 ∈ X ⟹ X = (UNIV:: hypnat set)"
  apply (clarsimp simp add: InternalSets_def starset_n_def)
  apply (erule (1) internal_induct_lemma)
  done

end