src/HOL/NSA/NatStar.thy
author huffman
Thu Jul 03 17:47:22 2008 +0200 (2008-07-03)
changeset 27468 0783dd1dc13d
child 39198 f967a16dfcdd
permissions -rw-r--r--
move nonstandard analysis theories to NSA directory
     1 (*  Title       : NatStar.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4 
     5 Converted to Isar and polished by lcp
     6 *)
     7 
     8 header{*Star-transforms for the Hypernaturals*}
     9 
    10 theory NatStar
    11 imports Star
    12 begin
    13 
    14 lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
    15 by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
    16 
    17 lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
    18 apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
    19 apply (rule_tac x=whn in spec, transfer, simp)
    20 done
    21 
    22 lemma InternalSets_Un:
    23      "[| X \<in> InternalSets; Y \<in> InternalSets |]
    24       ==> (X Un Y) \<in> InternalSets"
    25 by (auto simp add: InternalSets_def starset_n_Un [symmetric])
    26 
    27 lemma starset_n_Int:
    28       "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
    29 apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
    30 apply (rule_tac x=whn in spec, transfer, simp)
    31 done
    32 
    33 lemma InternalSets_Int:
    34      "[| X \<in> InternalSets; Y \<in> InternalSets |]
    35       ==> (X Int Y) \<in> InternalSets"
    36 by (auto simp add: InternalSets_def starset_n_Int [symmetric])
    37 
    38 lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
    39 apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
    40 apply (rule_tac x=whn in spec, transfer, simp)
    41 done
    42 
    43 lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
    44 by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
    45 
    46 lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
    47 apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
    48 apply (rule_tac x=whn in spec, transfer, simp)
    49 done
    50 
    51 lemma InternalSets_diff:
    52      "[| X \<in> InternalSets; Y \<in> InternalSets |]
    53       ==> (X - Y) \<in> InternalSets"
    54 by (auto simp add: InternalSets_def starset_n_diff [symmetric])
    55 
    56 lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)"
    57 by simp
    58 
    59 lemma NatStar_hypreal_of_real_Int:
    60      "*s* X Int Nats = hypnat_of_nat ` X"
    61 by (auto simp add: SHNat_eq)
    62 
    63 lemma starset_starset_n_eq: "*s* X = *sn* (%n. X)"
    64 by (simp add: starset_n_starset)
    65 
    66 lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets"
    67 by (auto simp add: InternalSets_def starset_starset_n_eq)
    68 
    69 lemma InternalSets_UNIV_diff:
    70      "X \<in> InternalSets ==> UNIV - X \<in> InternalSets"
    71 apply (subgoal_tac "UNIV - X = - X")
    72 by (auto intro: InternalSets_Compl)
    73 
    74 
    75 subsection{*Nonstandard Extensions of Functions*}
    76 
    77 text{* Example of transfer of a property from reals to hyperreals
    78     --- used for limit comparison of sequences*}
    79 
    80 lemma starfun_le_mono:
    81      "\<forall>n. N \<le> n --> f n \<le> g n
    82       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n"
    83 by transfer
    84 
    85 (*****----- and another -----*****)
    86 lemma starfun_less_mono:
    87      "\<forall>n. N \<le> n --> f n < g n
    88       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
    89 by transfer
    90 
    91 text{*Nonstandard extension when we increment the argument by one*}
    92 
    93 lemma starfun_shift_one:
    94      "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
    95 by (transfer, simp)
    96 
    97 text{*Nonstandard extension with absolute value*}
    98 
    99 lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)"
   100 by (transfer, rule refl)
   101 
   102 text{*The hyperpow function as a nonstandard extension of realpow*}
   103 
   104 lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
   105 by (transfer, rule refl)
   106 
   107 lemma starfun_pow2:
   108      "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
   109 by (transfer, rule refl)
   110 
   111 lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
   112 by (transfer, rule refl)
   113 
   114 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
   115   @{term real_of_nat} *}
   116 
   117 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
   118 by transfer (simp add: expand_fun_eq real_of_nat_def)
   119 
   120 lemma starfun_inverse_real_of_nat_eq:
   121      "N \<in> HNatInfinite
   122    ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
   123 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   124 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   125 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
   126 done
   127 
   128 text{*Internal functions - some redundancy with *f* now*}
   129 
   130 lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
   131 by (simp add: starfun_n_def Ifun_star_n)
   132 
   133 text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
   134 
   135 lemma starfun_n_mult:
   136      "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
   137 apply (cases z)
   138 apply (simp add: starfun_n star_n_mult)
   139 done
   140 
   141 text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
   142 
   143 lemma starfun_n_add:
   144      "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
   145 apply (cases z)
   146 apply (simp add: starfun_n star_n_add)
   147 done
   148 
   149 text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
   150 
   151 lemma starfun_n_add_minus:
   152      "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
   153 apply (cases z)
   154 apply (simp add: starfun_n star_n_minus star_n_add)
   155 done
   156 
   157 
   158 text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
   159 
   160 lemma starfun_n_const_fun [simp]:
   161      "( *fn* (%i x. k)) z = star_of k"
   162 apply (cases z)
   163 apply (simp add: starfun_n star_of_def)
   164 done
   165 
   166 lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (%i x. - (f i) x)) x"
   167 apply (cases x)
   168 apply (simp add: starfun_n star_n_minus)
   169 done
   170 
   171 lemma starfun_n_eq [simp]:
   172      "( *fn* f) (star_of n) = star_n (%i. f i n)"
   173 by (simp add: starfun_n star_of_def)
   174 
   175 lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) = (f = g)"
   176 by (transfer, rule refl)
   177 
   178 lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
   179      "N \<in> HNatInfinite ==> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
   180 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   181 apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   182 apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
   183 done
   184 
   185 
   186 subsection{*Nonstandard Characterization of Induction*}
   187 
   188 lemma hypnat_induct_obj:
   189     "!!n. (( *p* P) (0::hypnat) &
   190             (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
   191        --> ( *p* P)(n)"
   192 by (transfer, induct_tac n, auto)
   193 
   194 lemma hypnat_induct:
   195   "!!n. [| ( *p* P) (0::hypnat);
   196       !!n. ( *p* P)(n) ==> ( *p* P)(n + 1)|]
   197      ==> ( *p* P)(n)"
   198 by (transfer, induct_tac n, auto)
   199 
   200 lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
   201 by transfer (rule refl)
   202 
   203 lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
   204 by (simp add: starP2_eq_iff)
   205 
   206 lemma nonempty_nat_set_Least_mem:
   207   "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
   208 by (erule LeastI)
   209 
   210 lemma nonempty_set_star_has_least:
   211     "!!S::nat set star. Iset S \<noteq> {} ==> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
   212 apply (transfer empty_def)
   213 apply (rule_tac x="LEAST n. n \<in> S" in bexI)
   214 apply (simp add: Least_le)
   215 apply (rule LeastI_ex, auto)
   216 done
   217 
   218 lemma nonempty_InternalNatSet_has_least:
   219     "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
   220 apply (clarsimp simp add: InternalSets_def starset_n_def)
   221 apply (erule nonempty_set_star_has_least)
   222 done
   223 
   224 text{* Goldblatt page 129 Thm 11.3.2*}
   225 lemma internal_induct_lemma:
   226      "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
   227       ==> Iset X = (UNIV:: hypnat set)"
   228 apply (transfer UNIV_def)
   229 apply (rule equalityI [OF subset_UNIV subsetI])
   230 apply (induct_tac x, auto)
   231 done
   232 
   233 lemma internal_induct:
   234      "[| X \<in> InternalSets; (0::hypnat) \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
   235       ==> X = (UNIV:: hypnat set)"
   236 apply (clarsimp simp add: InternalSets_def starset_n_def)
   237 apply (erule (1) internal_induct_lemma)
   238 done
   239 
   240 
   241 end