src/HOL/Real/Hyperreal/NatStar.ML
changeset 10045 c76b73e16711
child 10607 352f6f209775
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/NatStar.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,541 @@
     1.4 +(*  Title       : NatStar.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : *-transforms in NSA which extends 
     1.8 +                  sets of reals, and nat=>real, 
     1.9 +                  nat=>nat functions
    1.10 +*) 
    1.11 +
    1.12 +Goalw [starsetNat_def] 
    1.13 +      "*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
    1.14 +by (auto_tac (claset(),simpset() addsimps 
    1.15 +    [FreeUltrafilterNat_Nat_set]));
    1.16 +qed "NatStar_real_set";
    1.17 +
    1.18 +Goalw [starsetNat_def] "*sNat* {} = {}";
    1.19 +by (Step_tac 1);
    1.20 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.21 +by (dres_inst_tac [("x","%n. xa n")] bspec 1);
    1.22 +by (auto_tac (claset(),simpset() addsimps 
    1.23 +    [FreeUltrafilterNat_empty]));
    1.24 +qed "NatStar_empty_set";
    1.25 +
    1.26 +Addsimps [NatStar_empty_set];
    1.27 +
    1.28 +Goalw [starsetNat_def] 
    1.29 +      "*sNat* (A Un B) = *sNat* A Un *sNat* B";
    1.30 +by (Auto_tac);
    1.31 +by (REPEAT(blast_tac (claset() addIs 
    1.32 +   [FreeUltrafilterNat_subset]) 2));
    1.33 +by (dtac FreeUltrafilterNat_Compl_mem 1);
    1.34 +by (dtac bspec 1 THEN assume_tac 1);
    1.35 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.36 +by (Auto_tac);
    1.37 +by (Fuf_tac 1);
    1.38 +qed "NatStar_Un";
    1.39 +
    1.40 +Goalw [starsetNat_n_def] 
    1.41 +      "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B";
    1.42 +by Auto_tac;
    1.43 +by (dres_inst_tac [("x","Xa")] bspec 1);
    1.44 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    1.45 +by (auto_tac (claset() addSDs [bspec],simpset()));
    1.46 +by (TRYALL(Ultra_tac));
    1.47 +qed "starsetNat_n_Un";
    1.48 +
    1.49 +Goalw [InternalNatSets_def]
    1.50 +     "[| X : InternalNatSets; Y : InternalNatSets |] \
    1.51 +\     ==> (X Un Y) : InternalNatSets";
    1.52 +by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Un RS sym]));
    1.53 +qed "InternalNatSets_Un";
    1.54 +
    1.55 +Goalw [starsetNat_def] "*sNat* (A Int B) = *sNat* A Int *sNat* B";
    1.56 +by (Auto_tac);
    1.57 +by (blast_tac (claset() addIs [FreeUltrafilterNat_Int,
    1.58 +    FreeUltrafilterNat_subset]) 3);
    1.59 +by (REPEAT(blast_tac (claset() addIs 
    1.60 +    [FreeUltrafilterNat_subset]) 1));
    1.61 +qed "NatStar_Int";
    1.62 +
    1.63 +Goalw [starsetNat_n_def] 
    1.64 +      "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B";
    1.65 +by (Auto_tac);
    1.66 +by (auto_tac (claset() addSDs [bspec],simpset()));
    1.67 +by (TRYALL(Ultra_tac));
    1.68 +qed "starsetNat_n_Int";
    1.69 +
    1.70 +Goalw [InternalNatSets_def]
    1.71 +     "[| X : InternalNatSets; Y : InternalNatSets |] \
    1.72 +\     ==> (X Int Y) : InternalNatSets";
    1.73 +by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Int RS sym]));
    1.74 +qed "InternalNatSets_Int";
    1.75 +
    1.76 +Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
    1.77 +by (Auto_tac);
    1.78 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.79 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    1.80 +by (REPEAT(Step_tac 1) THEN Auto_tac);
    1.81 +by (TRYALL(Ultra_tac));
    1.82 +qed "NatStar_Compl";
    1.83 +
    1.84 +Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)";
    1.85 +by (Auto_tac);
    1.86 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.87 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    1.88 +by (REPEAT(Step_tac 1) THEN Auto_tac);
    1.89 +by (TRYALL(Ultra_tac));
    1.90 +qed "starsetNat_n_Compl";
    1.91 +
    1.92 +Goalw [InternalNatSets_def]
    1.93 +     "X :InternalNatSets ==> -X : InternalNatSets";
    1.94 +by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Compl RS sym]));
    1.95 +qed "InternalNatSets_Compl";
    1.96 +
    1.97 +Goalw [starsetNat_n_def] 
    1.98 +      "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B";
    1.99 +by (Auto_tac);
   1.100 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
   1.101 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 3);
   1.102 +by (auto_tac (claset() addSDs [bspec],simpset()));
   1.103 +by (TRYALL(Ultra_tac));
   1.104 +qed "starsetNat_n_diff";
   1.105 +
   1.106 +Goalw [InternalNatSets_def]
   1.107 +     "[| X : InternalNatSets; Y : InternalNatSets |] \
   1.108 +\     ==> (X - Y) : InternalNatSets";
   1.109 +by (auto_tac (claset(),simpset() addsimps [starsetNat_n_diff RS sym]));
   1.110 +qed "InternalNatSets_diff";
   1.111 +
   1.112 +Goalw [starsetNat_def] "!!A. A <= B ==> *sNat* A <= *sNat* B";
   1.113 +by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
   1.114 +qed "NatStar_subset";
   1.115 +
   1.116 +Goalw [starsetNat_def,hypnat_of_nat_def] 
   1.117 +          "!!A. a : A ==> hypnat_of_nat a : *sNat* A";
   1.118 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
   1.119 +qed "NatStar_mem";
   1.120 +
   1.121 +Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
   1.122 +by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def]));
   1.123 +by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
   1.124 +qed "NatStar_hypreal_of_real_image_subset";
   1.125 +
   1.126 +Goal "SHNat <= *sNat* (UNIV:: nat set)";
   1.127 +by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
   1.128 +    NatStar_hypreal_of_real_image_subset]) 1);
   1.129 +qed "NatStar_SHNat_subset";
   1.130 +
   1.131 +Goalw [starsetNat_def] 
   1.132 +      "*sNat* X Int SHNat = hypnat_of_nat `` X";
   1.133 +by (auto_tac (claset(),simpset() addsimps 
   1.134 +           [hypnat_of_nat_def,SHNat_def]));
   1.135 +by (fold_tac [hypnat_of_nat_def]);
   1.136 +by (rtac imageI 1 THEN rtac ccontr 1);
   1.137 +by (dtac bspec 1);
   1.138 +by (rtac lemma_hypnatrel_refl 1);
   1.139 +by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
   1.140 +by (Auto_tac);
   1.141 +qed "NatStar_hypreal_of_real_Int";
   1.142 +
   1.143 +Goal "!!x. x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
   1.144 +by (Auto_tac);
   1.145 +qed "lemma_not_hypnatA";
   1.146 +
   1.147 +Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)";
   1.148 +by Auto_tac;
   1.149 +qed "starsetNat_starsetNat_n_eq";
   1.150 +
   1.151 +Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
   1.152 +by (auto_tac (claset(),simpset() addsimps [starsetNat_starsetNat_n_eq]));
   1.153 +qed "InternalNatSets_starsetNat_n";
   1.154 +Addsimps [InternalNatSets_starsetNat_n];
   1.155 +
   1.156 +Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets";
   1.157 +by (auto_tac (claset() addIs [InternalNatSets_Compl],simpset()));
   1.158 +qed "InternalNatSets_UNIV_diff";
   1.159 +
   1.160 +(*------------------------------------------------------------------ 
   1.161 +   Nonstandard extension of a set (defined using a constant 
   1.162 +   sequence) as a special case of an internal set
   1.163 + -----------------------------------------------------------------*)
   1.164 +
   1.165 +Goalw [starsetNat_n_def,starsetNat_def] 
   1.166 +     "!!A. ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
   1.167 +by (Auto_tac);
   1.168 +qed "starsetNat_n_starsetNat";
   1.169 +
   1.170 +(*------------------------------------------------------
   1.171 +   Theorems about nonstandard extensions of functions
   1.172 + ------------------------------------------------------*)
   1.173 +
   1.174 +(*------------------------------------------------------------------ 
   1.175 +   Nonstandard extension of a function (defined using a constant 
   1.176 +   sequence) as a special case of an internal function
   1.177 + -----------------------------------------------------------------*)
   1.178 +
   1.179 +Goalw [starfunNat_n_def,starfunNat_def] 
   1.180 +     "!!A. ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
   1.181 +by (Auto_tac);
   1.182 +qed "starfunNat_n_starfunNat";
   1.183 +
   1.184 +Goalw [starfunNat2_n_def,starfunNat2_def] 
   1.185 +     "!!A. ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
   1.186 +by (Auto_tac);
   1.187 +qed "starfunNat2_n_starfunNat2";
   1.188 +
   1.189 +Goalw [congruent_def] 
   1.190 +      "congruent hypnatrel (%X. hypnatrel^^{%n. f (X n)})";
   1.191 +by (safe_tac (claset()));
   1.192 +by (ALLGOALS(Fuf_tac));
   1.193 +qed "starfunNat_congruent";
   1.194 +
   1.195 +(* f::nat=>real *)
   1.196 +Goalw [starfunNat_def]
   1.197 +      "(*fNat* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   1.198 +\      Abs_hypreal(hyprel ^^ {%n. f (X n)})";
   1.199 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   1.200 +by (simp_tac (simpset() addsimps 
   1.201 +   [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1);
   1.202 +by (Auto_tac THEN Fuf_tac 1);
   1.203 +qed "starfunNat";
   1.204 +
   1.205 +(* f::nat=>nat *)
   1.206 +Goalw [starfunNat2_def]
   1.207 +      "(*fNat2* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   1.208 +\      Abs_hypnat(hypnatrel ^^ {%n. f (X n)})";
   1.209 +by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
   1.210 +by (simp_tac (simpset() addsimps 
   1.211 +   [hypnatrel_in_hypnat RS Abs_hypnat_inverse,
   1.212 +    [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
   1.213 +qed "starfunNat2";
   1.214 +
   1.215 +(*---------------------------------------------
   1.216 +  multiplication: ( *f ) x ( *g ) = *(f x g)  
   1.217 + ---------------------------------------------*)
   1.218 +Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa";
   1.219 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.220 +by (auto_tac (claset(),simpset() addsimps 
   1.221 +    [starfunNat,hypreal_mult]));
   1.222 +qed "starfunNat_mult";
   1.223 +
   1.224 +Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa";
   1.225 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.226 +by (auto_tac (claset(),simpset() addsimps 
   1.227 +    [starfunNat2,hypnat_mult]));
   1.228 +qed "starfunNat2_mult";
   1.229 +
   1.230 +(*---------------------------------------
   1.231 +  addition: ( *f ) + ( *g ) = *(f + g)  
   1.232 + ---------------------------------------*)
   1.233 +Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa";
   1.234 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.235 +by (auto_tac (claset(),simpset() addsimps 
   1.236 +    [starfunNat,hypreal_add]));
   1.237 +qed "starfunNat_add";
   1.238 +
   1.239 +Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa";
   1.240 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.241 +by (auto_tac (claset(),simpset() addsimps 
   1.242 +    [starfunNat2,hypnat_add]));
   1.243 +qed "starfunNat2_add";
   1.244 +
   1.245 +(*--------------------------------------------
   1.246 +  subtraction: ( *f ) + -( *g ) = *(f + -g)  
   1.247 + --------------------------------------------*)
   1.248 +Goal "(*fNat* f) xa + -(*fNat* g) xa = (*fNat* (%x. f x + -g x)) xa";
   1.249 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.250 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.251 +    hypreal_minus,hypreal_add]));
   1.252 +qed "starfunNat_add_minus";
   1.253 +
   1.254 +Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa";
   1.255 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.256 +by (auto_tac (claset(),simpset() addsimps [starfunNat2,
   1.257 +    hypnat_minus]));
   1.258 +qed "starfunNat2_minus";
   1.259 +
   1.260 +(*--------------------------------------
   1.261 +  composition: ( *f ) o ( *g ) = *(f o g)  
   1.262 + ---------------------------------------*)
   1.263 +(***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
   1.264 + 
   1.265 +Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
   1.266 +by (rtac ext 1);
   1.267 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.268 +by (auto_tac (claset(),simpset() addsimps [starfunNat2,
   1.269 +    starfunNat]));
   1.270 +qed "starfunNatNat2_o";
   1.271 +
   1.272 +Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
   1.273 +by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
   1.274 +qed "starfunNatNat2_o2";
   1.275 +
   1.276 +(***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
   1.277 +Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
   1.278 +by (rtac ext 1);
   1.279 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.280 +by (auto_tac (claset(),simpset() addsimps [starfunNat2]));
   1.281 +qed "starfunNat2_o";
   1.282 +
   1.283 +(***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
   1.284 +
   1.285 +Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; 
   1.286 +by (rtac ext 1);
   1.287 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.288 +by (auto_tac (claset(),simpset() addsimps [starfunNat,starfun]));
   1.289 +qed "starfun_stafunNat_o";
   1.290 +
   1.291 +Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; 
   1.292 +by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
   1.293 +qed "starfun_stafunNat_o2";
   1.294 +
   1.295 +(*--------------------------------------
   1.296 +  NS extension of constant function
   1.297 + --------------------------------------*)
   1.298 +Goal "(*fNat* (%x. k)) xa = hypreal_of_real k";
   1.299 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.300 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.301 +    hypreal_of_real_def]));
   1.302 +qed "starfunNat_const_fun";
   1.303 +Addsimps [starfunNat_const_fun];
   1.304 +
   1.305 +Goal "(*fNat2* (%x. k)) xa = hypnat_of_nat  k";
   1.306 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.307 +by (auto_tac (claset(),simpset() addsimps [starfunNat2,
   1.308 +    hypnat_of_nat_def]));
   1.309 +qed "starfunNat2_const_fun";
   1.310 +
   1.311 +Addsimps [starfunNat2_const_fun];
   1.312 +
   1.313 +Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
   1.314 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.315 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.316 +              hypreal_minus]));
   1.317 +qed "starfunNat_minus";
   1.318 +
   1.319 +Goal "ALL x. f x ~= 0 ==> \
   1.320 +\     hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
   1.321 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.322 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.323 +              hypreal_hrinv]));
   1.324 +qed "starfunNat_hrinv";
   1.325 +
   1.326 +(*--------------------------------------------------------
   1.327 +   extented function has same solution as its standard
   1.328 +   version for natural arguments. i.e they are the same
   1.329 +   for all natural arguments (c.f. Hoskins pg. 107- SEQ)
   1.330 + -------------------------------------------------------*)
   1.331 +
   1.332 +Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
   1.333 +by (auto_tac (claset(),simpset() addsimps 
   1.334 +     [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
   1.335 +qed "starfunNat_eq";
   1.336 +
   1.337 +Addsimps [starfunNat_eq];
   1.338 +
   1.339 +Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
   1.340 +by (auto_tac (claset(),simpset() addsimps 
   1.341 +     [starfunNat2,hypnat_of_nat_def]));
   1.342 +qed "starfunNat2_eq";
   1.343 +
   1.344 +Addsimps [starfunNat2_eq];
   1.345 +
   1.346 +Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
   1.347 +by (Auto_tac);
   1.348 +qed "starfunNat_inf_close";
   1.349 +
   1.350 +Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m; \
   1.351 +\                 l: HFinite; m: HFinite  \
   1.352 +\              |] ==>  (*fNat* (%x. f x * g x)) xa @= l * m";
   1.353 +by (dtac inf_close_mult_HFinite 1);
   1.354 +by (REPEAT(assume_tac 1));
   1.355 +by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
   1.356 +              simpset() addsimps [starfunNat_mult]));
   1.357 +qed "starfunNat_mult_HFinite_inf_close";
   1.358 +
   1.359 +Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m \
   1.360 +\              |] ==>  (*fNat* (%x. f x + g x)) xa @= l + m";
   1.361 +by (auto_tac (claset() addIs [inf_close_add],
   1.362 +              simpset() addsimps [starfunNat_add RS sym]));
   1.363 +qed "starfunNat_add_inf_close";
   1.364 +
   1.365 +(*-------------------------------------------------------------------
   1.366 +  A few more theorems involving NS extension of real sequences
   1.367 +  See analogous theorems for starfun- NS extension of f::real=>real
   1.368 + ------------------------------------------------------------------*)
   1.369 +Goal 
   1.370 +     "!!f. (*fNat* f) x ~= 0 ==> \
   1.371 +\     hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
   1.372 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.373 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   1.374 +    addSDs [FreeUltrafilterNat_Compl_mem],
   1.375 +    simpset() addsimps [starfunNat,hypreal_hrinv,
   1.376 +    hypreal_zero_def]));
   1.377 +qed "starfunNat_hrinv2";
   1.378 +
   1.379 +(*-----------------------------------------------------------------
   1.380 +    Example of transfer of a property from reals to hyperreals
   1.381 +    --- used for limit comparison of sequences
   1.382 + ----------------------------------------------------------------*)
   1.383 +Goal "!!f. ALL n. N <= n --> f n <= g n \
   1.384 +\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
   1.385 +by (Step_tac 1);
   1.386 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.387 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.388 +        hypnat_of_nat_def,hypreal_le,hypreal_less,
   1.389 +        hypnat_le,hypnat_less]));
   1.390 +by (Ultra_tac 1);
   1.391 +by Auto_tac;
   1.392 +qed "starfun_le_mono";
   1.393 +
   1.394 +(*****----- and another -----*****) 
   1.395 +goal NatStar.thy 
   1.396 +     "!!f. ALL n. N <= n --> f n < g n \
   1.397 +\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
   1.398 +by (Step_tac 1);
   1.399 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.400 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.401 +        hypnat_of_nat_def,hypreal_le,hypreal_less,
   1.402 +        hypnat_le,hypnat_less]));
   1.403 +by (Ultra_tac 1);
   1.404 +by Auto_tac;
   1.405 +qed "starfun_less_mono";
   1.406 +
   1.407 +(*----------------------------------------------------------------
   1.408 +            NS extension when we displace argument by one
   1.409 + ---------------------------------------------------------------*)
   1.410 +Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)";
   1.411 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.412 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.413 +    hypnat_one_def,hypnat_add]));
   1.414 +qed "starfunNat_shift_one";
   1.415 +
   1.416 +(*----------------------------------------------------------------
   1.417 +                 NS extension with rabs    
   1.418 + ---------------------------------------------------------------*)
   1.419 +Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
   1.420 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.421 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.422 +    hypreal_hrabs]));
   1.423 +qed "starfunNat_rabs";
   1.424 +
   1.425 +(*----------------------------------------------------------------
   1.426 +       The hyperpow function as a NS extension of realpow
   1.427 + ----------------------------------------------------------------*)
   1.428 +Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
   1.429 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.430 +by (auto_tac (claset(),simpset() addsimps [hyperpow,
   1.431 +    hypreal_of_real_def,starfunNat]));
   1.432 +qed "starfunNat_pow";
   1.433 +
   1.434 +Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
   1.435 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.436 +by (auto_tac (claset(),simpset() addsimps [hyperpow,
   1.437 +    hypnat_of_nat_def,starfunNat]));
   1.438 +qed "starfunNat_pow2";
   1.439 +
   1.440 +Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   1.441 +by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   1.442 +by (auto_tac (claset(),simpset() addsimps [hyperpow,starfun]));
   1.443 +qed "starfun_pow";
   1.444 +
   1.445 +(*----------------------------------------------------- 
   1.446 +   hypreal_of_hypnat as NS extension of real_of_nat! 
   1.447 +-------------------------------------------------------*)
   1.448 +Goal "(*fNat* real_of_nat) = hypreal_of_hypnat";
   1.449 +by (rtac ext 1);
   1.450 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.451 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,starfunNat]));
   1.452 +qed "starfunNat_real_of_nat";
   1.453 +
   1.454 +Goal "N : HNatInfinite \
   1.455 +\     ==> (*fNat* (%x. rinv (real_of_nat x))) N = hrinv(hypreal_of_hypnat N)";
   1.456 +by (res_inst_tac [("f1","rinv")]  (starfun_stafunNat_o2 RS subst) 1);
   1.457 +by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   1.458 +by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat, 
   1.459 +    starfun_rinv_hrinv]));
   1.460 +qed "starfunNat_rinv_real_of_nat_eq";
   1.461 +
   1.462 +(*----------------------------------------------------------
   1.463 +     Internal functions - some redundancy with *fNat* now
   1.464 + ---------------------------------------------------------*)
   1.465 +Goalw [congruent_def] 
   1.466 +      "congruent hypnatrel (%X. hypnatrel^^{%n. f n (X n)})";
   1.467 +by (safe_tac (claset()));
   1.468 +by (ALLGOALS(Fuf_tac));
   1.469 +qed "starfunNat_n_congruent";
   1.470 +
   1.471 +Goalw [starfunNat_n_def]
   1.472 +      "(*fNatn* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \
   1.473 +\      Abs_hypreal(hyprel ^^ {%n. f n (X n)})";
   1.474 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   1.475 +by Auto_tac;
   1.476 +by (Ultra_tac 1);
   1.477 +qed "starfunNat_n";
   1.478 +
   1.479 +(*-------------------------------------------------
   1.480 +  multiplication: ( *fn ) x ( *gn ) = *(fn x gn)  
   1.481 + -------------------------------------------------*)
   1.482 +Goal "(*fNatn* f) xa * (*fNatn* g) xa = \
   1.483 +\         (*fNatn* (% i x. f i x * g i x)) xa";
   1.484 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.485 +by (auto_tac (claset(),simpset() addsimps 
   1.486 +    [starfunNat_n,hypreal_mult]));
   1.487 +qed "starfunNat_n_mult";
   1.488 +
   1.489 +(*-----------------------------------------------
   1.490 +  addition: ( *fn ) + ( *gn ) = *(fn + gn)  
   1.491 + -----------------------------------------------*)
   1.492 +Goal "(*fNatn* f) xa + (*fNatn* g) xa = \
   1.493 +\         (*fNatn* (%i x. f i x + g i x)) xa";
   1.494 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.495 +by (auto_tac (claset(),simpset() addsimps 
   1.496 +    [starfunNat_n,hypreal_add]));
   1.497 +qed "starfunNat_n_add";
   1.498 +
   1.499 +(*-------------------------------------------------
   1.500 +  subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)  
   1.501 + -------------------------------------------------*)
   1.502 +Goal "(*fNatn* f) xa + -(*fNatn* g) xa = \
   1.503 +\         (*fNatn* (%i x. f i x + -g i x)) xa";
   1.504 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.505 +by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
   1.506 +    hypreal_minus,hypreal_add]));
   1.507 +qed "starfunNat_n_add_minus";
   1.508 +
   1.509 +(*--------------------------------------------------
   1.510 +  composition: ( *fn ) o ( *gn ) = *(fn o gn)  
   1.511 + -------------------------------------------------*)
   1.512 + 
   1.513 +Goal "(*fNatn* (%i x. k)) xa = hypreal_of_real  k";
   1.514 +by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
   1.515 +by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
   1.516 +    hypreal_of_real_def]));
   1.517 +qed "starfunNat_n_const_fun";
   1.518 +
   1.519 +Addsimps [starfunNat_n_const_fun];
   1.520 +
   1.521 +Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
   1.522 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.523 +by (auto_tac (claset(),simpset() addsimps [starfunNat_n,
   1.524 +              hypreal_minus]));
   1.525 +qed "starfunNat_n_minus";
   1.526 +
   1.527 +Goal "(*fNatn* f) (hypnat_of_nat n) = \
   1.528 +\         Abs_hypreal(hyprel ^^ {%i. f i n})";
   1.529 +by (auto_tac (claset(),simpset() addsimps 
   1.530 +     [starfunNat_n,hypnat_of_nat_def]));
   1.531 +qed "starfunNat_n_eq";
   1.532 +Addsimps [starfunNat_n_eq];
   1.533 +
   1.534 +Goal "((*fNat* f) = (*fNat* g)) = (f = g)";
   1.535 +by Auto_tac;
   1.536 +by (rtac ext 1 THEN rtac ccontr 1);
   1.537 +by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
   1.538 +by (auto_tac (claset(),simpset() addsimps [starfunNat,hypnat_of_nat_def]));
   1.539 +qed "starfun_eq_iff";
   1.540 +
   1.541 +
   1.542 +
   1.543 +
   1.544 +