src/HOL/Real/Hyperreal/HyperPow.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/HyperPow.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,585 @@
     1.4 +(*  Title       : HyperPow.ML
     1.5 +    Author      : Jacques D. Fleuriot  
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Natural Powers of hyperreals theory
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +Goal "(0::hypreal) ^ (Suc n) = 0";
    1.12 +by (Auto_tac);
    1.13 +qed "hrealpow_zero";
    1.14 +Addsimps [hrealpow_zero];
    1.15 +
    1.16 +Goal "r ~= (0::hypreal) --> r ^ n ~= 0";
    1.17 +by (induct_tac "n" 1);
    1.18 +by (auto_tac (claset() addIs [hypreal_mult_not_0E],
    1.19 +    simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
    1.20 +qed_spec_mp "hrealpow_not_zero";
    1.21 +
    1.22 +Goal "r ~= (0::hypreal) --> hrinv(r ^ n) = (hrinv r) ^ n";
    1.23 +by (induct_tac "n" 1);
    1.24 +by (Auto_tac);
    1.25 +by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
    1.26 +by (auto_tac (claset() addDs [hrinv_mult_eq],
    1.27 +    simpset()));
    1.28 +qed_spec_mp "hrealpow_hrinv";
    1.29 +
    1.30 +Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
    1.31 +by (induct_tac "n" 1);
    1.32 +by (auto_tac (claset(),simpset() addsimps [hrabs_mult,hrabs_one]));
    1.33 +qed "hrealpow_hrabs";
    1.34 +
    1.35 +Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
    1.36 +by (induct_tac "n" 1);
    1.37 +by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
    1.38 +qed "hrealpow_add";
    1.39 +
    1.40 +Goal "(r::hypreal) ^ 1 = r";
    1.41 +by (Simp_tac 1);
    1.42 +qed "hrealpow_one";
    1.43 +Addsimps [hrealpow_one];
    1.44 +
    1.45 +Goal "(r::hypreal) ^ 2 = r * r";
    1.46 +by (Simp_tac 1);
    1.47 +qed "hrealpow_two";
    1.48 +
    1.49 +Goal "(0::hypreal) < r --> 0 <= r ^ n";
    1.50 +by (induct_tac "n" 1);
    1.51 +by (auto_tac (claset() addDs [hypreal_less_imp_le] 
    1.52 +    addIs [hypreal_le_mult_order],simpset() addsimps 
    1.53 +    [hypreal_zero_less_one RS hypreal_less_imp_le]));
    1.54 +qed_spec_mp "hrealpow_ge_zero";
    1.55 +
    1.56 +Goal "(0::hypreal) < r --> 0 < r ^ n";
    1.57 +by (induct_tac "n" 1);
    1.58 +by (auto_tac (claset() addIs [hypreal_mult_order],
    1.59 +    simpset() addsimps [hypreal_zero_less_one]));
    1.60 +qed_spec_mp "hrealpow_gt_zero";
    1.61 +
    1.62 +Goal "(0::hypreal) <= r --> 0 <= r ^ n";
    1.63 +by (induct_tac "n" 1);
    1.64 +by (auto_tac (claset() addIs [hypreal_le_mult_order],simpset() 
    1.65 +    addsimps [hypreal_zero_less_one RS hypreal_less_imp_le]));
    1.66 +qed_spec_mp "hrealpow_ge_zero2";
    1.67 +
    1.68 +Goal "(0::hypreal) < x & x <= y --> x ^ n <= y ^ n";
    1.69 +by (induct_tac "n" 1);
    1.70 +by (auto_tac (claset() addSIs [hypreal_mult_le_mono],
    1.71 +    simpset() addsimps [hypreal_le_refl]));
    1.72 +by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
    1.73 +qed_spec_mp "hrealpow_le";
    1.74 +
    1.75 +Goal "(0::hypreal) < x & x < y & 0 < n --> x ^ n < y ^ n";
    1.76 +by (induct_tac "n" 1);
    1.77 +by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I] 
    1.78 +    addDs [hrealpow_gt_zero],simpset()));
    1.79 +qed "hrealpow_less";
    1.80 +
    1.81 +Goal "1hr ^ n = 1hr";
    1.82 +by (induct_tac "n" 1);
    1.83 +by (Auto_tac);
    1.84 +qed "hrealpow_eq_one";
    1.85 +Addsimps [hrealpow_eq_one];
    1.86 +
    1.87 +Goal "abs(-(1hr ^ n)) = 1hr";
    1.88 +by (simp_tac (simpset() addsimps 
    1.89 +    [hrabs_minus_cancel,hrabs_one]) 1);
    1.90 +qed "hrabs_minus_hrealpow_one";
    1.91 +Addsimps [hrabs_minus_hrealpow_one];
    1.92 +
    1.93 +Goal "abs((-1hr) ^ n) = 1hr";
    1.94 +by (induct_tac "n" 1);
    1.95 +by (auto_tac (claset(),simpset() addsimps [hrabs_mult,
    1.96 +         hrabs_minus_cancel,hrabs_one]));
    1.97 +qed "hrabs_hrealpow_minus_one";
    1.98 +Addsimps [hrabs_hrealpow_minus_one];
    1.99 +
   1.100 +Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
   1.101 +by (induct_tac "n" 1);
   1.102 +by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac));
   1.103 +qed "hrealpow_mult";
   1.104 +
   1.105 +Goal "(0::hypreal) <= r ^ 2";
   1.106 +by (simp_tac (simpset() addsimps [hrealpow_two]) 1);
   1.107 +qed "hrealpow_two_le";
   1.108 +Addsimps [hrealpow_two_le];
   1.109 +
   1.110 +Goal "(0::hypreal) <= u ^ 2 + v ^ 2";
   1.111 +by (auto_tac (claset() addIs [hypreal_le_add_order],simpset()));
   1.112 +qed "hrealpow_two_le_add_order";
   1.113 +Addsimps [hrealpow_two_le_add_order];
   1.114 +
   1.115 +Goal "(0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2";
   1.116 +by (auto_tac (claset() addSIs [hypreal_le_add_order],simpset()));
   1.117 +qed "hrealpow_two_le_add_order2";
   1.118 +Addsimps [hrealpow_two_le_add_order2];
   1.119 +
   1.120 +(* See HYPER.ML *)
   1.121 +Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = \ 
   1.122 +\               (x = 0 & y = 0 & z = 0)";
   1.123 +by (simp_tac (simpset() addsimps [hrealpow_two]) 1);
   1.124 +qed "hrealpow_three_squares_add_zero_iff";
   1.125 +Addsimps [hrealpow_three_squares_add_zero_iff];
   1.126 +
   1.127 +Goal "abs(x ^ 2) = (x::hypreal) ^ 2";
   1.128 +by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
   1.129 +qed "hrabs_hrealpow_two";
   1.130 +Addsimps [hrabs_hrealpow_two];
   1.131 +
   1.132 +Goal "abs(x) ^ 2 = (x::hypreal) ^ 2";
   1.133 +by (simp_tac (simpset() addsimps [hrealpow_hrabs,
   1.134 +    hrabs_eqI1] delsimps [hpowr_Suc]) 1);
   1.135 +qed "hrealpow_two_hrabs";
   1.136 +Addsimps [hrealpow_two_hrabs];
   1.137 +
   1.138 +Goal "!!r. 1hr < r ==> 1hr < r ^ 2";
   1.139 +by (auto_tac (claset(),simpset() addsimps [hrealpow_two]));
   1.140 +by (cut_facts_tac [hypreal_zero_less_one] 1);
   1.141 +by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
   1.142 +by (assume_tac 1);
   1.143 +by (dres_inst_tac [("z","r"),("x","1hr")] hypreal_mult_less_mono1 1);
   1.144 +by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
   1.145 +qed "hrealpow_two_gt_one";
   1.146 +
   1.147 +Goal "!!r. 1hr <= r ==> 1hr <= r ^ 2";
   1.148 +by (etac (hypreal_le_imp_less_or_eq RS disjE) 1);
   1.149 +by (etac (hrealpow_two_gt_one RS hypreal_less_imp_le) 1);
   1.150 +by (asm_simp_tac (simpset() addsimps [hypreal_le_refl]) 1);
   1.151 +qed "hrealpow_two_ge_one";
   1.152 +
   1.153 +Goal "!!r. (0::hypreal) < r ==> 0 < r ^ Suc n";
   1.154 +by (forw_inst_tac [("n","n")] hrealpow_ge_zero 1);
   1.155 +by (forw_inst_tac [("n1","n")]
   1.156 +    ((hypreal_not_refl2 RS not_sym) RS hrealpow_not_zero RS not_sym) 1);
   1.157 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq]
   1.158 +     addIs [hypreal_mult_order],simpset()));
   1.159 +qed "hrealpow_Suc_gt_zero";
   1.160 +
   1.161 +Goal "!!r. (0::hypreal) <= r ==> 0 <= r ^ Suc n";
   1.162 +by (etac (hypreal_le_imp_less_or_eq RS disjE) 1);
   1.163 +by (etac (hrealpow_ge_zero) 1);
   1.164 +by (asm_simp_tac (simpset() addsimps [hypreal_le_refl]) 1);
   1.165 +qed "hrealpow_Suc_ge_zero";
   1.166 +
   1.167 +Goal "1hr <= (1hr +1hr) ^ n";
   1.168 +by (res_inst_tac [("j","1hr ^ n")] hypreal_le_trans 1);
   1.169 +by (rtac hrealpow_le 2);
   1.170 +by (auto_tac (claset() addIs [hypreal_less_imp_le],
   1.171 +    simpset() addsimps [hypreal_zero_less_one,
   1.172 +    hypreal_one_less_two,hypreal_le_refl]));
   1.173 +qed "two_hrealpow_ge_one";
   1.174 +
   1.175 +Goal "hypreal_of_nat n < (1hr + 1hr) ^ n";
   1.176 +by (induct_tac "n" 1);
   1.177 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
   1.178 +    hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
   1.179 +by (blast_tac (claset() addSIs [hypreal_add_less_le_mono,
   1.180 +    two_hrealpow_ge_one]) 1);
   1.181 +qed "two_hrealpow_gt";
   1.182 +Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
   1.183 +
   1.184 +Goal "(-1hr) ^ (2*n) = 1hr";
   1.185 +by (induct_tac "n" 1);
   1.186 +by (Auto_tac);
   1.187 +qed "hrealpow_minus_one";
   1.188 +
   1.189 +Goal "(-1hr) ^ (n + n) = 1hr";
   1.190 +by (induct_tac "n" 1);
   1.191 +by (Auto_tac);
   1.192 +qed "hrealpow_minus_one2";
   1.193 +Addsimps [hrealpow_minus_one2];
   1.194 +
   1.195 +Goal "(-(x::hypreal)) ^ 2 = x ^ 2";
   1.196 +by (Auto_tac);
   1.197 +qed "hrealpow_minus_two";
   1.198 +Addsimps [hrealpow_minus_two];
   1.199 +
   1.200 +Goal "(0::hypreal) < r & r < 1hr --> r ^ Suc n < r ^ n";
   1.201 +by (induct_tac "n" 1);
   1.202 +by (auto_tac (claset(),simpset() addsimps 
   1.203 +        [hypreal_mult_less_mono2]));
   1.204 +qed_spec_mp "hrealpow_Suc_less";
   1.205 +
   1.206 +Goal "(0::hypreal) <= r & r < 1hr --> r ^ Suc n <= r ^ n";
   1.207 +by (induct_tac "n" 1);
   1.208 +by (auto_tac (claset() addIs [hypreal_less_imp_le] addSDs
   1.209 +     [hypreal_le_imp_less_or_eq,hrealpow_Suc_less],simpset()
   1.210 +     addsimps [hypreal_le_refl,hypreal_mult_less_mono2]));
   1.211 +qed_spec_mp "hrealpow_Suc_le";
   1.212 +
   1.213 +(* a few more theorems needed here *)
   1.214 +Goal "1hr <= r --> r ^ n <= r ^ Suc n";
   1.215 +by (induct_tac "n" 1);
   1.216 +by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1],simpset()));
   1.217 +by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
   1.218 +by (dtac hypreal_le_less_trans 1 THEN assume_tac 1);
   1.219 +by (etac (hypreal_zero_less_one RS hypreal_less_asym) 1);
   1.220 +qed "hrealpow_less_Suc";
   1.221 +
   1.222 +Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})";
   1.223 +by (nat_ind_tac "m" 1);
   1.224 +by (auto_tac (claset(),simpset() addsimps 
   1.225 +    [hypreal_one_def,hypreal_mult]));
   1.226 +qed "hrealpow";
   1.227 +
   1.228 +Goal "(x + (y::hypreal)) ^ 2 = \
   1.229 +\     x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y";
   1.230 +by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
   1.231 +    hypreal_add_mult_distrib,hypreal_of_nat_two] 
   1.232 +    @ hypreal_add_ac @ hypreal_mult_ac) 1);
   1.233 +qed "hrealpow_sum_square_expand";
   1.234 +
   1.235 +(*---------------------------------------------------------------
   1.236 +   we'll prove the following theorem by going down to the
   1.237 +   level of the ultrafilter and relying on the analogous
   1.238 +   property for the real rather than prove it directly 
   1.239 +   using induction: proof is much simpler this way!
   1.240 + ---------------------------------------------------------------*)
   1.241 +Goalw [hypreal_zero_def] 
   1.242 +  "[|(0::hypreal) <= x;0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
   1.243 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.244 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.245 +by (auto_tac (claset(),simpset() addsimps 
   1.246 +    [hrealpow,hypreal_le,hypreal_mult]));
   1.247 +by (ultra_tac (claset() addIs [realpow_increasing],simpset()) 1);
   1.248 +qed "hrealpow_increasing";
   1.249 +
   1.250 +goalw HyperPow.thy [hypreal_zero_def] 
   1.251 +  "!!x. [|(0::hypreal) <= x;0 <= y;x ^ Suc n = y ^ Suc n |] ==> x = y";
   1.252 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.253 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.254 +by (auto_tac (claset(),simpset() addsimps 
   1.255 +    [hrealpow,hypreal_mult,hypreal_le]));
   1.256 +by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
   1.257 +    simpset()) 1);
   1.258 +qed "hrealpow_Suc_cancel_eq";
   1.259 +
   1.260 +Goal "x : HFinite --> x ^ n : HFinite";
   1.261 +by (induct_tac "n" 1);
   1.262 +by (auto_tac (claset() addIs [HFinite_mult],simpset()));
   1.263 +qed_spec_mp "hrealpow_HFinite";
   1.264 +
   1.265 +(*---------------------------------------------------------------
   1.266 +                  Hypernaturals Powers
   1.267 + --------------------------------------------------------------*)
   1.268 +Goalw [congruent_def]
   1.269 +     "congruent hyprel \
   1.270 +\    (%X Y. hyprel^^{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
   1.271 +by (safe_tac (claset() addSIs [ext]));
   1.272 +by (ALLGOALS(Fuf_tac));
   1.273 +qed "hyperpow_congruent";
   1.274 +
   1.275 +Goalw [hyperpow_def]
   1.276 +  "Abs_hypreal(hyprel^^{%n. X n}) pow Abs_hypnat(hypnatrel^^{%n. Y n}) = \
   1.277 +\  Abs_hypreal(hyprel^^{%n. X n ^ Y n})";
   1.278 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   1.279 +by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
   1.280 +    simpset() addsimps [hyprel_in_hypreal RS 
   1.281 +    Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent]));
   1.282 +by (Fuf_tac 1);
   1.283 +qed "hyperpow";
   1.284 +
   1.285 +Goalw [hypreal_zero_def,hypnat_one_def]
   1.286 +      "(0::hypreal) pow (n + 1hn) = 0";
   1.287 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.288 +by (auto_tac (claset(),simpset() addsimps 
   1.289 +    [hyperpow,hypnat_add]));
   1.290 +qed "hyperpow_zero";
   1.291 +Addsimps [hyperpow_zero];
   1.292 +
   1.293 +Goalw [hypreal_zero_def]
   1.294 +      "r ~= (0::hypreal) --> r pow n ~= 0";
   1.295 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.296 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.297 +by (auto_tac (claset(),simpset() addsimps [hyperpow]));
   1.298 +by (dtac FreeUltrafilterNat_Compl_mem 1);
   1.299 +by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
   1.300 +    simpset()) 1);
   1.301 +qed_spec_mp "hyperpow_not_zero";
   1.302 +
   1.303 +Goalw [hypreal_zero_def] 
   1.304 +      "r ~= (0::hypreal) --> hrinv(r pow n) = (hrinv r) pow n";
   1.305 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.306 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.307 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   1.308 +    simpset() addsimps [hypreal_hrinv,hyperpow]));
   1.309 +by (rtac FreeUltrafilterNat_subset 1);
   1.310 +by (auto_tac (claset() addDs [realpow_not_zero] 
   1.311 +    addIs [realpow_rinv],simpset()));
   1.312 +qed "hyperpow_hrinv";
   1.313 +
   1.314 +Goal "abs r pow n = abs (r pow n)";
   1.315 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.316 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.317 +by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
   1.318 +    hyperpow,realpow_abs]));
   1.319 +qed "hyperpow_hrabs";
   1.320 +
   1.321 +Goal "r pow (n + m) = (r pow n) * (r pow m)";
   1.322 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.323 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.324 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.325 +by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
   1.326 +     hypreal_mult,realpow_add]));
   1.327 +qed "hyperpow_add";
   1.328 +
   1.329 +Goalw [hypnat_one_def] "r pow 1hn = r";
   1.330 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.331 +by (auto_tac (claset(),simpset() addsimps [hyperpow]));
   1.332 +qed "hyperpow_one";
   1.333 +Addsimps [hyperpow_one];
   1.334 +
   1.335 +Goalw [hypnat_one_def] 
   1.336 +      "r pow (1hn + 1hn) = r * r";
   1.337 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.338 +by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add,
   1.339 +     hypreal_mult,realpow_two]));
   1.340 +qed "hyperpow_two";
   1.341 +
   1.342 +Goalw [hypreal_zero_def]
   1.343 +      "(0::hypreal) < r --> 0 < r pow n";
   1.344 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.345 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.346 +by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
   1.347 +    realpow_gt_zero],simpset() addsimps [hyperpow,hypreal_less,
   1.348 +    hypreal_le]));
   1.349 +qed_spec_mp "hyperpow_gt_zero";
   1.350 +
   1.351 +Goal "(0::hypreal) < r --> 0 <= r pow n";
   1.352 +by (blast_tac (claset() addSIs [hyperpow_gt_zero,
   1.353 +    hypreal_less_imp_le]) 1);
   1.354 +qed_spec_mp "hyperpow_ge_zero";
   1.355 +
   1.356 +Goalw [hypreal_zero_def]
   1.357 +      "(0::hypreal) <= r --> 0 <= r pow n";
   1.358 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.359 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.360 +by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset,
   1.361 +    realpow_ge_zero2],simpset() addsimps [hyperpow,hypreal_le]));
   1.362 +qed "hyperpow_ge_zero2";
   1.363 +
   1.364 +Goalw [hypreal_zero_def]
   1.365 +      "(0::hypreal) < x & x <= y --> x pow n <= y pow n";
   1.366 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.367 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.368 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.369 +by (auto_tac (claset() addIs [realpow_le,
   1.370 +    (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset)],
   1.371 +    simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
   1.372 +qed_spec_mp "hyperpow_le";
   1.373 +
   1.374 +Goalw [hypreal_one_def] "1hr pow n = 1hr";
   1.375 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.376 +by (auto_tac (claset(),simpset() addsimps [hyperpow]));
   1.377 +qed "hyperpow_eq_one";
   1.378 +Addsimps [hyperpow_eq_one];
   1.379 +
   1.380 +Goalw [hypreal_one_def]
   1.381 +      "abs(-(1hr pow n)) = 1hr";
   1.382 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.383 +by (auto_tac (claset(),simpset() addsimps [abs_one,
   1.384 +    hrabs_minus_cancel,hyperpow,hypreal_hrabs]));
   1.385 +qed "hrabs_minus_hyperpow_one";
   1.386 +Addsimps [hrabs_minus_hyperpow_one];
   1.387 +
   1.388 +Goalw [hypreal_one_def]
   1.389 +      "abs((-1hr) pow n) = 1hr";
   1.390 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.391 +by (auto_tac (claset(),simpset() addsimps 
   1.392 +    [hyperpow,hypreal_minus,hypreal_hrabs]));
   1.393 +qed "hrabs_hyperpow_minus_one";
   1.394 +Addsimps [hrabs_hyperpow_minus_one];
   1.395 +
   1.396 +Goal "(r * s) pow n = (r pow n) * (s pow n)";
   1.397 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.398 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.399 +by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
   1.400 +by (auto_tac (claset(),simpset() addsimps [hyperpow,
   1.401 +    hypreal_mult,realpow_mult]));
   1.402 +qed "hyperpow_mult";
   1.403 +
   1.404 +Goal "(0::hypreal) <= r pow (1hn + 1hn)";
   1.405 +by (simp_tac (simpset() addsimps [hyperpow_two]) 1);
   1.406 +qed "hyperpow_two_le";
   1.407 +Addsimps [hyperpow_two_le];
   1.408 +
   1.409 +Goal "abs(x pow (1hn + 1hn)) = x pow (1hn + 1hn)";
   1.410 +by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
   1.411 +qed "hrabs_hyperpow_two";
   1.412 +Addsimps [hrabs_hyperpow_two];
   1.413 +
   1.414 +Goal "abs(x) pow (1hn + 1hn)  = x pow (1hn + 1hn)";
   1.415 +by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
   1.416 +qed "hyperpow_two_hrabs";
   1.417 +Addsimps [hyperpow_two_hrabs];
   1.418 +
   1.419 +Goal "!!r. 1hr < r ==> 1hr < r pow (1hn + 1hn)";
   1.420 +by (auto_tac (claset(),simpset() addsimps [hyperpow_two]));
   1.421 +by (cut_facts_tac [hypreal_zero_less_one] 1);
   1.422 +by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1);
   1.423 +by (assume_tac 1);
   1.424 +by (dres_inst_tac [("z","r"),("x","1hr")] 
   1.425 +    hypreal_mult_less_mono1 1);
   1.426 +by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
   1.427 +qed "hyperpow_two_gt_one";
   1.428 +
   1.429 +Goal "!!r. 1hr <= r ==> 1hr <= r pow (1hn + 1hn)";
   1.430 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.431 +     addIs [hyperpow_two_gt_one,hypreal_less_imp_le],
   1.432 +     simpset() addsimps [hypreal_le_refl]));
   1.433 +qed "hyperpow_two_ge_one";
   1.434 +
   1.435 +Goalw [hypnat_one_def,hypreal_zero_def]
   1.436 +      "!!r. (0::hypreal) < r ==> 0 < r pow (n + 1hn)";
   1.437 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.438 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.439 +by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset]
   1.440 +    addDs [realpow_Suc_gt_zero],simpset() addsimps [hyperpow,
   1.441 +    hypreal_less,hypnat_add]));
   1.442 +qed "hyperpow_Suc_gt_zero";
   1.443 +
   1.444 +Goal "!!r. (0::hypreal) <= r ==> 0 <= r pow (n + 1hn)";
   1.445 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.446 +    addIs [hyperpow_ge_zero,hypreal_less_imp_le], 
   1.447 +    simpset() addsimps [hypreal_le_refl]));
   1.448 +qed "hyperpow_Suc_ge_zero";
   1.449 +
   1.450 +Goal "1hr <= (1hr +1hr) pow n";
   1.451 +by (res_inst_tac [("j","1hr pow n")] hypreal_le_trans 1);
   1.452 +by (rtac hyperpow_le 2);
   1.453 +by (auto_tac (claset() addIs [hypreal_less_imp_le],
   1.454 +    simpset() addsimps [hypreal_zero_less_one,
   1.455 +    hypreal_one_less_two,hypreal_le_refl]));
   1.456 +qed "two_hyperpow_ge_one";
   1.457 +Addsimps [two_hyperpow_ge_one];
   1.458 +
   1.459 +Addsimps [simplify (simpset()) realpow_minus_one];
   1.460 +Goalw [hypreal_one_def]
   1.461 +      "(-1hr) pow ((1hn + 1hn)*n) = 1hr";
   1.462 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.463 +by (auto_tac (claset(),simpset() addsimps [hyperpow,
   1.464 +    hypnat_add,hypreal_minus]));
   1.465 +qed "hyperpow_minus_one2";
   1.466 +Addsimps [hyperpow_minus_one2];
   1.467 +
   1.468 +Goalw [hypreal_zero_def,
   1.469 +      hypreal_one_def,hypnat_one_def]
   1.470 +     "(0::hypreal) < r & r < 1hr --> r pow (n + 1hn) < r pow n";
   1.471 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.472 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.473 +by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] addEs
   1.474 +    [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ],
   1.475 +    simpset() addsimps [hyperpow,hypreal_less,hypnat_add]));
   1.476 +qed_spec_mp "hyperpow_Suc_less";
   1.477 +
   1.478 +Goalw [hypreal_zero_def,
   1.479 +      hypreal_one_def,hypnat_one_def]
   1.480 +     "0 <= r & r < 1hr --> r pow (n + 1hn) <= r pow n";
   1.481 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.482 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.483 +by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] addEs
   1.484 +    [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ],
   1.485 +    simpset() addsimps [hyperpow,hypreal_le,hypnat_add,
   1.486 +    hypreal_less]));
   1.487 +qed_spec_mp "hyperpow_Suc_le";
   1.488 +
   1.489 +Goalw [hypreal_zero_def,
   1.490 +      hypreal_one_def,hypnat_one_def]
   1.491 +     "(0::hypreal) <= r & r < 1hr & n < N --> r pow N <= r pow n";
   1.492 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.493 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.494 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.495 +by (auto_tac (claset(),simpset() addsimps [hyperpow,
   1.496 +    hypreal_le,hypreal_less,hypnat_less]));
   1.497 +by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
   1.498 +by (etac FreeUltrafilterNat_Int 1);
   1.499 +by (auto_tac (claset() addSDs [conjI RS realpow_less_le],
   1.500 +    simpset()));
   1.501 +qed_spec_mp "hyperpow_less_le";
   1.502 +
   1.503 +Goal "!!r. [| (0::hypreal) <= r; r < 1hr |] ==> \
   1.504 +\          ALL N n. n < N --> r pow N <= r pow n";
   1.505 +by (blast_tac (claset() addSIs [hyperpow_less_le]) 1);
   1.506 +qed "hyperpow_less_le2";
   1.507 +
   1.508 +Goal "!!r. [| 0 <= r; r < 1hr; \
   1.509 +\             N : HNatInfinite \
   1.510 +\          |] ==> ALL n:SHNat. r pow N <= r pow n";
   1.511 +by (auto_tac (claset() addSIs [hyperpow_less_le],
   1.512 +              simpset() addsimps [HNatInfinite_iff]));
   1.513 +qed "hyperpow_SHNat_le";
   1.514 +
   1.515 +Goalw [hypreal_of_real_def,hypnat_of_nat_def] 
   1.516 +      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
   1.517 +by (auto_tac (claset(),simpset() addsimps [hyperpow]));
   1.518 +qed "hyperpow_realpow";
   1.519 +
   1.520 +Goalw [SReal_def]
   1.521 +     "(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
   1.522 +by (auto_tac (claset(),simpset() addsimps [hyperpow_realpow]));
   1.523 +qed "hyperpow_SReal";
   1.524 +Addsimps [hyperpow_SReal];
   1.525 +
   1.526 +Goal "!!N. N : HNatInfinite ==> (0::hypreal) pow N = 0";
   1.527 +by (dtac HNatInfinite_is_Suc 1);
   1.528 +by (Auto_tac);
   1.529 +qed "hyperpow_zero_HNatInfinite";
   1.530 +Addsimps [hyperpow_zero_HNatInfinite];
   1.531 +
   1.532 +Goal "!!r. [| (0::hypreal) <= r; r < 1hr; n <= N |] ==> r pow N <= r pow n";
   1.533 +by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1);
   1.534 +by (auto_tac (claset() addIs [hyperpow_less_le],
   1.535 +    simpset() addsimps [hypreal_le_refl]));
   1.536 +qed "hyperpow_le_le";
   1.537 +
   1.538 +Goal "!!r. [| (0::hypreal) < r; r < 1hr |] ==> r pow (n + 1hn) <= r";
   1.539 +by (dres_inst_tac [("n","1hn")] (hypreal_less_imp_le RS 
   1.540 +    hyperpow_le_le) 1);
   1.541 +by (Auto_tac);
   1.542 +qed "hyperpow_Suc_le_self";
   1.543 +
   1.544 +Goal "!!r. [| (0::hypreal) <= r; r < 1hr |] ==> r pow (n + 1hn) <= r";
   1.545 +by (dres_inst_tac [("n","1hn")] hyperpow_le_le 1);
   1.546 +by (Auto_tac);
   1.547 +qed "hyperpow_Suc_le_self2";
   1.548 +
   1.549 +Goalw [Infinitesimal_def]
   1.550 +     "!!x. [| x : Infinitesimal; 0 < N |] \
   1.551 +\          ==> (abs x) pow N <= abs x";
   1.552 +by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
   1.553 +    simpset() addsimps [hyperpow_hrabs RS sym,
   1.554 +    hypnat_gt_zero_iff2,hrabs_ge_zero,SReal_one,
   1.555 +    hypreal_zero_less_one]));
   1.556 +qed "lemma_Infinitesimal_hyperpow";
   1.557 +
   1.558 +Goal "!!x. [| x : Infinitesimal; 0 < N |] \
   1.559 +\           ==> x pow N : Infinitesimal";
   1.560 +by (rtac hrabs_le_Infinitesimal 1);
   1.561 +by (dtac Infinitesimal_hrabs 1);
   1.562 +by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow],
   1.563 +    simpset() addsimps [hyperpow_hrabs RS sym]));
   1.564 +qed "Infinitesimal_hyperpow";
   1.565 +
   1.566 +goalw HyperPow.thy [hypnat_of_nat_def] 
   1.567 +     "(x ^ n : Infinitesimal) = \
   1.568 +\     (x pow (hypnat_of_nat n) : Infinitesimal)";
   1.569 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.570 +by (auto_tac (claset(),simpset() addsimps [hrealpow,
   1.571 +    hyperpow]));
   1.572 +qed "hrealpow_hyperpow_Infinitesimal_iff";
   1.573 +
   1.574 +goal HyperPow.thy 
   1.575 +     "!!x. [| x : Infinitesimal; 0 < n |] \
   1.576 +\           ==> x ^ n : Infinitesimal";
   1.577 +by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
   1.578 +    simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
   1.579 +    hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
   1.580 +    delsimps [hypnat_of_nat_less_iff RS sym]));
   1.581 +qed "Infinitesimal_hrealpow";
   1.582 +
   1.583 +
   1.584 +
   1.585 +
   1.586 +
   1.587 +
   1.588 +