# Theory NatStar

Up to index of Isabelle/HOL/HOL-Complex

theory NatStar
imports HyperPow
begin

    (*  Title       : NatStar.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 1998  University of Cambridge

    Converted to Isar and polished by lcp
    *)

    header{*Star-transforms for the Hypernaturals*}

    theory NatStar
    imports HyperPow
    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) Un (B n)) = *sn* A Un *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 Un Y) ∈ InternalSets"
    by (auto simp add: InternalSets_def starset_n_Un [symmetric])

    lemma starset_n_Int:
          "*sn* (%n. (A n) Int (B n)) = *sn* A Int *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 Int 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_def)
    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_def)
    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 STAR_mem_iff)

    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")
    by (auto intro: InternalSets_Compl)

    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

    (*****----- 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. abs (f n))) N = abs(( *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, rule refl)

    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: HNatInfinite_not_eq_zero starfunNat_real_of_nat starfun_inverse_inverse)
    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: @{text "( *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"
    apply (cases z)
    apply (simp add: starfun_n star_n_mult)
    done

    text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}

    lemma starfun_n_add:
         "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
    apply (cases z)
    apply (simp add: starfun_n star_n_add)
    done

    text{*Subtraction: @{text "( *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"
    apply (cases z)
    apply (simp add: starfun_n star_n_minus star_n_add)
    done

    text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}

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

    lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (%i x. - (f i) x)) x"
    apply (cases x)
    apply (simp add: starfun_n star_n_minus)
    done

    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: HNatInfinite_not_eq_zero starfunNat_real_of_nat)
    done

    ML
    {*
    val starset_n_Un = thm "starset_n_Un";
    val InternalSets_Un = thm "InternalSets_Un";
    val starset_n_Int = thm "starset_n_Int";
    val InternalSets_Int = thm "InternalSets_Int";
    val starset_n_Compl = thm "starset_n_Compl";
    val InternalSets_Compl = thm "InternalSets_Compl";
    val starset_n_diff = thm "starset_n_diff";
    val InternalSets_diff = thm "InternalSets_diff";
    val NatStar_SHNat_subset = thm "NatStar_SHNat_subset";
    val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int";
    val starset_starset_n_eq = thm "starset_starset_n_eq";
    val InternalSets_starset_n = thm "InternalSets_starset_n";
    val InternalSets_UNIV_diff = thm "InternalSets_UNIV_diff";
    val starset_n_starset = thm "starset_n_starset";
    val starfun_const_fun = thm "starfun_const_fun";
    val starfun_le_mono = thm "starfun_le_mono";
    val starfun_less_mono = thm "starfun_less_mono";
    val starfun_shift_one = thm "starfun_shift_one";
    val starfun_abs = thm "starfun_abs";
    val starfun_pow = thm "starfun_pow";
    val starfun_pow2 = thm "starfun_pow2";
    val starfun_pow3 = thm "starfun_pow3";
    val starfunNat_real_of_nat = thm "starfunNat_real_of_nat";
    val starfun_inverse_real_of_nat_eq = thm "starfun_inverse_real_of_nat_eq";
    val starfun_n = thm "starfun_n";
    val starfun_n_mult = thm "starfun_n_mult";
    val starfun_n_add = thm "starfun_n_add";
    val starfun_n_add_minus = thm "starfun_n_add_minus";
    val starfun_n_const_fun = thm "starfun_n_const_fun";
    val starfun_n_minus = thm "starfun_n_minus";
    val starfun_n_eq = thm "starfun_n_eq";
    val starfun_eq_iff = thm "starfun_eq_iff";
    val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
    *}

    subsection{*Nonstandard Characterization of Induction*}

    constdefs
      hSuc :: "hypnat => hypnat"
      "hSuc n == n + 1"

    lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} ∈ FreeUltrafilterNat)"
    by (rule starP_star_n)

    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:
    "(( *p2* P) (star_n X) (star_n Y)) =
          ({n. P (X n) (Y n)} ∈ FreeUltrafilterNat)"
    by (rule starP2_star_n)

    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 hSuc_not_zero [iff]: "hSuc m ≠ 0"
    by (simp add: hSuc_def)

    lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]

    lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
    by (simp add: hSuc_def star_n_one_num)

    lemma nonempty_nat_set_Least_mem: "c ∈ (S :: nat set) ==> (LEAST n. n  ∈ S)  ∈ S"
    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::hypnat set) ∈ InternalSets; S ≠ {} |] ==> ∃n ∈ S. ∀m ∈ S. n ≤ m"
    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

lemma star_n_eq_starfun_whn:

      star_n X = (*f* X) whn

lemma starset_n_Un:

      *sn* (%n. A n ∪ B n) = *sn* A ∪ *sn* B

lemma InternalSets_Un:

      [| X ∈ InternalSets; Y ∈ InternalSets |] ==> X ∪ Y ∈ InternalSets

lemma starset_n_Int:

      *sn* (%n. A n ∩ B n) = *sn* A ∩ *sn* B

lemma InternalSets_Int:

      [| X ∈ InternalSets; Y ∈ InternalSets |] ==> X ∩ Y ∈ InternalSets

lemma starset_n_Compl:

      *sn* (%n. - A n) = - (*sn* A)

lemma InternalSets_Compl:

      X ∈ InternalSets ==> - X ∈ InternalSets

lemma starset_n_diff:

      *sn* (%n. A n - B n) = *sn* A - *sn* B

lemma InternalSets_diff:

      [| X ∈ InternalSets; Y ∈ InternalSets |] ==> X - Y ∈ InternalSets

lemma NatStar_SHNat_subset:

      Nats ⊆ *s* UNIV

lemma NatStar_hypreal_of_real_Int:

      *s* X ∩ Nats = star_of ` X

lemma starset_starset_n_eq:

      *s* X = *sn* (%n. X)

lemma InternalSets_starset_n:

      *s* X ∈ InternalSets

lemma InternalSets_UNIV_diff:

      X ∈ InternalSets ==> UNIV - X ∈ InternalSets

### Nonstandard Extensions of Functions

lemma starfun_le_mono:

      ∀n≥N. f n ≤ g n ==> ∀n≥star_of N. (*f* f) n ≤ (*f* g) n

lemma starfun_less_mono:

      ∀n≥N. f n < g n ==> ∀n≥star_of N. (*f* f) n < (*f* g) n

lemma starfun_shift_one:

      (*f* (%n. f (Suc n))) N = (*f* f) (N + 1)

lemma starfun_abs:

      (*f* (%n. ¦f n¦)) N = ¦(*f* f) N¦

lemma starfun_pow:

      (*f* op ^ r) N = star_of r pow N

lemma starfun_pow2:

      (*f* (%n. X n ^ m)) N = (*f* X) N pow star_of m

lemma starfun_pow3:

      (*f* (%r. r ^ n)) R = R pow star_of n

lemma starfunNat_real_of_nat:

      *f* real = hypreal_of_hypnat

lemma starfun_inverse_real_of_nat_eq:

      N ∈ HNatInfinite
      ==> (*f* (%x. inverse (real x))) N = inverse (hypreal_of_hypnat N)

lemma starfun_n:

      (*fn* f) (star_n X) = star_n (%n. f n (X n))

lemma starfun_n_mult:

      (*fn* f) z * (*fn* g) z = (*fn* (%i x. f i x * g i x)) z

lemma starfun_n_add:

      (*fn* f) z + (*fn* g) z = (*fn* (%i x. f i x + g i x)) z

lemma starfun_n_add_minus:

      (*fn* f) z + - (*fn* g) z = (*fn* (%i x. f i x + - g i x)) z

lemma starfun_n_const_fun:

      (*fn* (%i x. k)) z = star_of k

lemma starfun_n_minus:

      - (*fn* f) x = (*fn* (%i x. - f i x)) x

lemma starfun_n_eq:

      (*fn* f) (star_of n) = star_n (%i. f i n)

lemma starfun_eq_iff:

      (*f* f = *f* g) = (f = g)

lemma starfunNat_inverse_real_of_nat_Infinitesimal:

      N ∈ HNatInfinite ==> (*f* (%x. inverse (real x))) N ∈ Infinitesimal

### Nonstandard Characterization of Induction

lemma starP:

      (*p* P) (star_n X) = ({n. P (X n)} ∈ \<U>)

lemma hypnat_induct_obj:

      (*p* P) 0 ∧ (∀n. (*p* P) n --> (*p* P) (n + 1)) --> (*p* P) n

lemma hypnat_induct:

      [| (*p* P) 0; !!n. (*p* P) n ==> (*p* P) (n + 1) |] ==> (*p* P) n

lemma starP2:

      (*p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} ∈ \<U>)

lemma starP2_eq_iff:

      *p2* op = = op =

lemma starP2_eq_iff2:

      (*p2* op =) X Y = (X = Y)

lemma hSuc_not_zero:

      hSuc m ≠ 0

lemmas zero_not_hSuc:

      0 ≠ hSuc m

lemmas zero_not_hSuc:

      0 ≠ hSuc m

lemma hSuc_hSuc_eq:

      (hSuc m = hSuc n) = (m = n)

lemma nonempty_nat_set_Least_mem:

      c ∈ S ==> (LEAST n. n ∈ S) ∈ S

lemma nonempty_set_star_has_least:

      Iset S ≠ {} ==> ∃n∈Iset S. ∀m∈Iset S. n ≤ m

lemma nonempty_InternalNatSet_has_least:

      [| S ∈ InternalSets; S ≠ {} |] ==> ∃n∈S. ∀m∈S. n ≤ m

lemma internal_induct_lemma:

      [| 0 ∈ Iset X; ∀n. n ∈ Iset X --> n + 1 ∈ Iset X |] ==> Iset X = UNIV

lemma internal_induct:

      [| X ∈ InternalSets; 0 ∈ X; ∀n. n ∈ X --> n + 1 ∈ X |] ==> X = UNIV