src/HOL/NSA/NatStar.thy
changeset 27468 0783dd1dc13d
child 39198 f967a16dfcdd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NSA/NatStar.thy	Thu Jul 03 17:47:22 2008 +0200
     1.3 @@ -0,0 +1,241 @@
     1.4 +(*  Title       : NatStar.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +
     1.8 +Converted to Isar and polished by lcp
     1.9 +*)
    1.10 +
    1.11 +header{*Star-transforms for the Hypernaturals*}
    1.12 +
    1.13 +theory NatStar
    1.14 +imports Star
    1.15 +begin
    1.16 +
    1.17 +lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
    1.18 +by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
    1.19 +
    1.20 +lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
    1.21 +apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
    1.22 +apply (rule_tac x=whn in spec, transfer, simp)
    1.23 +done
    1.24 +
    1.25 +lemma InternalSets_Un:
    1.26 +     "[| X \<in> InternalSets; Y \<in> InternalSets |]
    1.27 +      ==> (X Un Y) \<in> InternalSets"
    1.28 +by (auto simp add: InternalSets_def starset_n_Un [symmetric])
    1.29 +
    1.30 +lemma starset_n_Int:
    1.31 +      "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
    1.32 +apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
    1.33 +apply (rule_tac x=whn in spec, transfer, simp)
    1.34 +done
    1.35 +
    1.36 +lemma InternalSets_Int:
    1.37 +     "[| X \<in> InternalSets; Y \<in> InternalSets |]
    1.38 +      ==> (X Int Y) \<in> InternalSets"
    1.39 +by (auto simp add: InternalSets_def starset_n_Int [symmetric])
    1.40 +
    1.41 +lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
    1.42 +apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
    1.43 +apply (rule_tac x=whn in spec, transfer, simp)
    1.44 +done
    1.45 +
    1.46 +lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
    1.47 +by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
    1.48 +
    1.49 +lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
    1.50 +apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
    1.51 +apply (rule_tac x=whn in spec, transfer, simp)
    1.52 +done
    1.53 +
    1.54 +lemma InternalSets_diff:
    1.55 +     "[| X \<in> InternalSets; Y \<in> InternalSets |]
    1.56 +      ==> (X - Y) \<in> InternalSets"
    1.57 +by (auto simp add: InternalSets_def starset_n_diff [symmetric])
    1.58 +
    1.59 +lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)"
    1.60 +by simp
    1.61 +
    1.62 +lemma NatStar_hypreal_of_real_Int:
    1.63 +     "*s* X Int Nats = hypnat_of_nat ` X"
    1.64 +by (auto simp add: SHNat_eq)
    1.65 +
    1.66 +lemma starset_starset_n_eq: "*s* X = *sn* (%n. X)"
    1.67 +by (simp add: starset_n_starset)
    1.68 +
    1.69 +lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets"
    1.70 +by (auto simp add: InternalSets_def starset_starset_n_eq)
    1.71 +
    1.72 +lemma InternalSets_UNIV_diff:
    1.73 +     "X \<in> InternalSets ==> UNIV - X \<in> InternalSets"
    1.74 +apply (subgoal_tac "UNIV - X = - X")
    1.75 +by (auto intro: InternalSets_Compl)
    1.76 +
    1.77 +
    1.78 +subsection{*Nonstandard Extensions of Functions*}
    1.79 +
    1.80 +text{* Example of transfer of a property from reals to hyperreals
    1.81 +    --- used for limit comparison of sequences*}
    1.82 +
    1.83 +lemma starfun_le_mono:
    1.84 +     "\<forall>n. N \<le> n --> f n \<le> g n
    1.85 +      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n"
    1.86 +by transfer
    1.87 +
    1.88 +(*****----- and another -----*****)
    1.89 +lemma starfun_less_mono:
    1.90 +     "\<forall>n. N \<le> n --> f n < g n
    1.91 +      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
    1.92 +by transfer
    1.93 +
    1.94 +text{*Nonstandard extension when we increment the argument by one*}
    1.95 +
    1.96 +lemma starfun_shift_one:
    1.97 +     "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
    1.98 +by (transfer, simp)
    1.99 +
   1.100 +text{*Nonstandard extension with absolute value*}
   1.101 +
   1.102 +lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)"
   1.103 +by (transfer, rule refl)
   1.104 +
   1.105 +text{*The hyperpow function as a nonstandard extension of realpow*}
   1.106 +
   1.107 +lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
   1.108 +by (transfer, rule refl)
   1.109 +
   1.110 +lemma starfun_pow2:
   1.111 +     "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
   1.112 +by (transfer, rule refl)
   1.113 +
   1.114 +lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
   1.115 +by (transfer, rule refl)
   1.116 +
   1.117 +text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
   1.118 +  @{term real_of_nat} *}
   1.119 +
   1.120 +lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
   1.121 +by transfer (simp add: expand_fun_eq real_of_nat_def)
   1.122 +
   1.123 +lemma starfun_inverse_real_of_nat_eq:
   1.124 +     "N \<in> HNatInfinite
   1.125 +   ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
   1.126 +apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   1.127 +apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   1.128 +apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
   1.129 +done
   1.130 +
   1.131 +text{*Internal functions - some redundancy with *f* now*}
   1.132 +
   1.133 +lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
   1.134 +by (simp add: starfun_n_def Ifun_star_n)
   1.135 +
   1.136 +text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
   1.137 +
   1.138 +lemma starfun_n_mult:
   1.139 +     "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
   1.140 +apply (cases z)
   1.141 +apply (simp add: starfun_n star_n_mult)
   1.142 +done
   1.143 +
   1.144 +text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
   1.145 +
   1.146 +lemma starfun_n_add:
   1.147 +     "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
   1.148 +apply (cases z)
   1.149 +apply (simp add: starfun_n star_n_add)
   1.150 +done
   1.151 +
   1.152 +text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
   1.153 +
   1.154 +lemma starfun_n_add_minus:
   1.155 +     "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
   1.156 +apply (cases z)
   1.157 +apply (simp add: starfun_n star_n_minus star_n_add)
   1.158 +done
   1.159 +
   1.160 +
   1.161 +text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
   1.162 +
   1.163 +lemma starfun_n_const_fun [simp]:
   1.164 +     "( *fn* (%i x. k)) z = star_of k"
   1.165 +apply (cases z)
   1.166 +apply (simp add: starfun_n star_of_def)
   1.167 +done
   1.168 +
   1.169 +lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (%i x. - (f i) x)) x"
   1.170 +apply (cases x)
   1.171 +apply (simp add: starfun_n star_n_minus)
   1.172 +done
   1.173 +
   1.174 +lemma starfun_n_eq [simp]:
   1.175 +     "( *fn* f) (star_of n) = star_n (%i. f i n)"
   1.176 +by (simp add: starfun_n star_of_def)
   1.177 +
   1.178 +lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) = (f = g)"
   1.179 +by (transfer, rule refl)
   1.180 +
   1.181 +lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
   1.182 +     "N \<in> HNatInfinite ==> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
   1.183 +apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
   1.184 +apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
   1.185 +apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
   1.186 +done
   1.187 +
   1.188 +
   1.189 +subsection{*Nonstandard Characterization of Induction*}
   1.190 +
   1.191 +lemma hypnat_induct_obj:
   1.192 +    "!!n. (( *p* P) (0::hypnat) &
   1.193 +            (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
   1.194 +       --> ( *p* P)(n)"
   1.195 +by (transfer, induct_tac n, auto)
   1.196 +
   1.197 +lemma hypnat_induct:
   1.198 +  "!!n. [| ( *p* P) (0::hypnat);
   1.199 +      !!n. ( *p* P)(n) ==> ( *p* P)(n + 1)|]
   1.200 +     ==> ( *p* P)(n)"
   1.201 +by (transfer, induct_tac n, auto)
   1.202 +
   1.203 +lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
   1.204 +by transfer (rule refl)
   1.205 +
   1.206 +lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
   1.207 +by (simp add: starP2_eq_iff)
   1.208 +
   1.209 +lemma nonempty_nat_set_Least_mem:
   1.210 +  "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
   1.211 +by (erule LeastI)
   1.212 +
   1.213 +lemma nonempty_set_star_has_least:
   1.214 +    "!!S::nat set star. Iset S \<noteq> {} ==> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
   1.215 +apply (transfer empty_def)
   1.216 +apply (rule_tac x="LEAST n. n \<in> S" in bexI)
   1.217 +apply (simp add: Least_le)
   1.218 +apply (rule LeastI_ex, auto)
   1.219 +done
   1.220 +
   1.221 +lemma nonempty_InternalNatSet_has_least:
   1.222 +    "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
   1.223 +apply (clarsimp simp add: InternalSets_def starset_n_def)
   1.224 +apply (erule nonempty_set_star_has_least)
   1.225 +done
   1.226 +
   1.227 +text{* Goldblatt page 129 Thm 11.3.2*}
   1.228 +lemma internal_induct_lemma:
   1.229 +     "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
   1.230 +      ==> Iset X = (UNIV:: hypnat set)"
   1.231 +apply (transfer UNIV_def)
   1.232 +apply (rule equalityI [OF subset_UNIV subsetI])
   1.233 +apply (induct_tac x, auto)
   1.234 +done
   1.235 +
   1.236 +lemma internal_induct:
   1.237 +     "[| X \<in> InternalSets; (0::hypnat) \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
   1.238 +      ==> X = (UNIV:: hypnat set)"
   1.239 +apply (clarsimp simp add: InternalSets_def starset_n_def)
   1.240 +apply (erule (1) internal_induct_lemma)
   1.241 +done
   1.242 +
   1.243 +
   1.244 +end