Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Hyperreal/HyperPow.thy
changeset 14371 c78c7da09519
parent 14348 744c868ee0b7
child 14378 69c4d5997669
equal deleted inserted replaced
14370:b0064703967b 14371:c78c7da09519 
     4     Description : Powers theory for hyperreals
 
     4     Description : Powers theory for hyperreals
 
     5 *)
 
     5 *)
 
     6 
     6 
     7 header{*Exponentials on the Hyperreals*}
 
     7 header{*Exponentials on the Hyperreals*}
 
     8 
     8 
     9 theory HyperPow = HRealAbs + HyperNat + RealPow:
 
     9 theory HyperPow = HyperArith + HyperNat + RealPow:
 
    10 
       
    11 instance hypnat :: order
 
       
    12   by (intro_classes,
 
       
    13       (assumption | 
       
    14        rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+)
 
       
    15 
       
    16                           
       
    17 text{*Type @{typ hypnat} is linearly ordered*}
 
       
    18 instance hypnat :: linorder 
       
    19   by (intro_classes, rule hypnat_le_linear)
 
       
    20 
       
    21 instance hypnat :: plus_ac0
 
       
    22   by (intro_classes,
 
       
    23       (assumption | 
       
    24        rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
 
       
    25 
       
    26 
    10 
    27 instance hypreal :: power ..
 
    11 instance hypreal :: power ..
 
    28 
    12 
    29 consts hpowr :: "[hypreal,nat] => hypreal"  
    13 consts hpowr :: "[hypreal,nat] => hypreal"  
    30 primrec
 
    14 primrec
 
    55 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
 
    39 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
 
    56 apply (simp (no_asm))
 
    40 apply (simp (no_asm))
 
    57 done
 
    41 done
 
    58 
    42 
    59 lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
 
    43 lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
 
    60 apply (simp add: power_abs); 
    44 by (simp add: power_abs)
 
    61 done
 
       
    62 
    45 
    63 lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
 
    46 lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
 
    64 apply (auto simp add: zero_le_mult_iff)
 
    47 by (auto simp add: zero_le_mult_iff)
 
    65 done
 
       
    66 declare hrealpow_two_le [simp]
 
    48 declare hrealpow_two_le [simp]
 
    67 
    49 
    68 lemma hrealpow_two_le_add_order:
 
    50 lemma hrealpow_two_le_add_order:
 
    69      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
 
    51      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
 
    70 apply (simp only: hrealpow_two_le hypreal_le_add_order)
 
    52 apply (simp only: hrealpow_two_le hypreal_le_add_order)
 
    83 done
 
    65 done
 
    84 
    66 
    85 text{*FIXME: DELETE THESE*}
 
    67 text{*FIXME: DELETE THESE*}
 
    86 lemma hypreal_three_squares_add_zero_iff:
 
    68 lemma hypreal_three_squares_add_zero_iff:
 
    87      "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
 
    69      "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
 
    88 apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff)
 
    70 apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
 
    89 apply auto
 
       
    90 done
 
    71 done
 
    91 
    72 
    92 lemma hrealpow_three_squares_add_zero_iff [simp]:
 
    73 lemma hrealpow_three_squares_add_zero_iff [simp]:
 
    93      "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
    74      "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
    94       (x = 0 & y = 0 & z = 0)"
 
    75       (x = 0 & y = 0 & z = 0)"
 
   103 by (insert power_increasing [of 0 n "2::hypreal"], simp)
 
    84 by (insert power_increasing [of 0 n "2::hypreal"], simp)
 
   104 
    85 
   105 lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
 
    86 lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
 
   106 apply (induct_tac "n")
 
    87 apply (induct_tac "n")
 
   107 apply (auto simp add: hypreal_of_nat_Suc left_distrib)
 
    88 apply (auto simp add: hypreal_of_nat_Suc left_distrib)
 
   108 apply (cut_tac n = "n" in two_hrealpow_ge_one)
 
    89 apply (cut_tac n = n in two_hrealpow_ge_one, arith)
 
   109 apply arith
 
       
   110 done
 
    90 done
 
   111 declare two_hrealpow_gt [simp] 
    91 declare two_hrealpow_gt [simp] 
   112 
    92 
   113 lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
 
    93 lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
 
   114 apply (induct_tac "n")
 
    94 by (induct_tac "n", auto)
 
   115 apply auto
 
       
   116 done
 
       
   117 
    95 
   118 lemma double_lemma: "n+n = (2*n::nat)"
 
    96 lemma double_lemma: "n+n = (2*n::nat)"
 
   119 apply auto
 
    97 by auto
 
   120 done
 
       
   121 
    98 
   122 (*ugh: need to get rid fo the n+n*)
 
    99 (*ugh: need to get rid fo the n+n*)
 
   123 lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
 
   100 lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
 
   124 apply (auto simp add: double_lemma hrealpow_minus_one)
 
   101 by (auto simp add: double_lemma hrealpow_minus_one)
 
   125 done
 
       
   126 declare hrealpow_minus_one2 [simp]
 
   102 declare hrealpow_minus_one2 [simp]
 
   127 
   103 
   128 lemma hrealpow:
 
   104 lemma hrealpow:
 
   129     "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
 
   105     "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
 
   130 apply (induct_tac "m")
 
   106 apply (induct_tac "m")
 
   161 
   137 
   162 lemma hyperpow_congruent:
 
   138 lemma hyperpow_congruent:
 
   163      "congruent hyprel
 
   139      "congruent hyprel
 
   164      (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
 
   140      (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
 
   165 apply (unfold congruent_def)
 
   141 apply (unfold congruent_def)
 
   166 apply (auto intro!: ext)
 
   142 apply (auto intro!: ext, fuf+)
 
   167 apply fuf+
 
       
   168 done
 
   143 done
 
   169 
   144 
   170 lemma hyperpow:
 
   145 lemma hyperpow:
 
   171   "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
 
   146   "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
 
   172    Abs_hypreal(hyprel``{%n. X n ^ Y n})"
 
   147    Abs_hypreal(hyprel``{%n. X n ^ Y n})"
 
   173 apply (unfold hyperpow_def)
 
   148 apply (unfold hyperpow_def)
 
   174 apply (rule_tac f = "Abs_hypreal" in arg_cong)
 
   149 apply (rule_tac f = Abs_hypreal in arg_cong)
 
   175 apply (auto intro!: lemma_hyprel_refl bexI 
   150 apply (auto intro!: lemma_hyprel_refl bexI 
   176            simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
   151            simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
   177                      hyperpow_congruent)
 
   152                      hyperpow_congruent, fuf)
 
   178 apply fuf
 
       
   179 done
 
   153 done
 
   180 
   154 
   181 lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
 
   155 lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
 
   182 apply (unfold hypnat_one_def)
 
   156 apply (unfold hypnat_one_def)
 
   183 apply (simp (no_asm) add: hypreal_zero_def)
 
   157 apply (simp (no_asm) add: hypreal_zero_def)
 
   184 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   158 apply (rule_tac z = n in eq_Abs_hypnat)
 
   185 apply (auto simp add: hyperpow hypnat_add)
 
   159 apply (auto simp add: hyperpow hypnat_add)
 
   186 done
 
   160 done
 
   187 declare hyperpow_zero [simp]
 
   161 declare hyperpow_zero [simp]
 
   188 
   162 
   189 lemma hyperpow_not_zero [rule_format (no_asm)]:
 
   163 lemma hyperpow_not_zero [rule_format (no_asm)]:
 
   190      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
 
   164      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
 
   191 apply (simp (no_asm) add: hypreal_zero_def)
 
   165 apply (simp (no_asm) add: hypreal_zero_def)
 
   192 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   166 apply (rule_tac z = n in eq_Abs_hypnat)
 
   193 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   167 apply (rule_tac z = r in eq_Abs_hypreal)
 
   194 apply (auto simp add: hyperpow)
 
   168 apply (auto simp add: hyperpow)
 
   195 apply (drule FreeUltrafilterNat_Compl_mem)
 
   169 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 
   196 apply ultra
 
       
   197 done
 
   170 done
 
   198 
   171 
   199 lemma hyperpow_inverse:
 
   172 lemma hyperpow_inverse:
 
   200      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
 
   173      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
 
   201 apply (simp (no_asm) add: hypreal_zero_def)
 
   174 apply (simp (no_asm) add: hypreal_zero_def)
 
   202 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   175 apply (rule_tac z = n in eq_Abs_hypnat)
 
   203 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   176 apply (rule_tac z = r in eq_Abs_hypreal)
 
   204 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 
   177 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 
   205 apply (rule FreeUltrafilterNat_subset)
 
   178 apply (rule FreeUltrafilterNat_subset)
 
   206 apply (auto dest: realpow_not_zero intro: power_inverse)
 
   179 apply (auto dest: realpow_not_zero intro: power_inverse)
 
   207 done
 
   180 done
 
   208 
   181 
   209 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
 
   182 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
 
   210 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   183 apply (rule_tac z = n in eq_Abs_hypnat)
 
   211 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   184 apply (rule_tac z = r in eq_Abs_hypreal)
 
   212 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 
   185 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 
   213 done
 
   186 done
 
   214 
   187 
   215 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
 
   188 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
 
   216 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   189 apply (rule_tac z = n in eq_Abs_hypnat)
 
   217 apply (rule_tac z = "m" in eq_Abs_hypnat)
 
   190 apply (rule_tac z = m in eq_Abs_hypnat)
 
   218 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   191 apply (rule_tac z = r in eq_Abs_hypreal)
 
   219 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 
   192 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 
   220 done
 
   193 done
 
   221 
   194 
   222 lemma hyperpow_one: "r pow (1::hypnat) = r"
 
   195 lemma hyperpow_one: "r pow (1::hypnat) = r"
 
   223 apply (unfold hypnat_one_def)
 
   196 apply (unfold hypnat_one_def)
 
   224 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   197 apply (rule_tac z = r in eq_Abs_hypreal)
 
   225 apply (auto simp add: hyperpow)
 
   198 apply (auto simp add: hyperpow)
 
   226 done
 
   199 done
 
   227 declare hyperpow_one [simp]
 
   200 declare hyperpow_one [simp]
 
   228 
   201 
   229 lemma hyperpow_two:
 
   202 lemma hyperpow_two:
 
   230      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
 
   203      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
 
   231 apply (unfold hypnat_one_def)
 
   204 apply (unfold hypnat_one_def)
 
   232 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   205 apply (rule_tac z = r in eq_Abs_hypreal)
 
   233 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 
   206 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 
   234 done
 
   207 done
 
   235 
   208 
   236 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
 
   209 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
 
   237 apply (simp add: hypreal_zero_def)
 
   210 apply (simp add: hypreal_zero_def)
 
   238 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   211 apply (rule_tac z = n in eq_Abs_hypnat)
 
   239 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   212 apply (rule_tac z = r in eq_Abs_hypreal)
 
   240 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
 
   213 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
 
   241                    simp add: hyperpow hypreal_less hypreal_le)
 
   214                    simp add: hyperpow hypreal_less hypreal_le)
 
   242 done
 
   215 done
 
   243 
   216 
   244 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
 
   217 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
 
   245 apply (simp add: hypreal_zero_def)
 
   218 apply (simp add: hypreal_zero_def)
 
   246 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   219 apply (rule_tac z = n in eq_Abs_hypnat)
 
   247 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   220 apply (rule_tac z = r in eq_Abs_hypreal)
 
   248 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   221 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   249             simp add: hyperpow hypreal_le)
 
   222             simp add: hyperpow hypreal_le)
 
   250 done
 
   223 done
 
   251 
   224 
   252 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
 
   225 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
 
   253 apply (simp add: hypreal_zero_def)
 
   226 apply (simp add: hypreal_zero_def)
 
   254 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   227 apply (rule_tac z = n in eq_Abs_hypnat)
 
   255 apply (rule_tac z = "x" in eq_Abs_hypreal)
 
   228 apply (rule_tac z = x in eq_Abs_hypreal)
 
   256 apply (rule_tac z = "y" in eq_Abs_hypreal)
 
   229 apply (rule_tac z = y in eq_Abs_hypreal)
 
   257 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 
   230 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 
   258 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption)
 
   231 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 
   259 apply (auto intro: power_mono)
 
   232 apply (auto intro: power_mono)
 
   260 done
 
   233 done
 
   261 
   234 
   262 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
 
   235 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
 
   263 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   236 apply (rule_tac z = n in eq_Abs_hypnat)
 
   264 apply (auto simp add: hypreal_one_def hyperpow)
 
   237 apply (auto simp add: hypreal_one_def hyperpow)
 
   265 done
 
   238 done
 
   266 declare hyperpow_eq_one [simp]
 
   239 declare hyperpow_eq_one [simp]
 
   267 
   240 
   268 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 
   241 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 
   269 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 
   242 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 
   270 apply simp
 
   243 apply simp
 
   271 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   244 apply (rule_tac z = n in eq_Abs_hypnat)
 
   272 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 
   245 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 
   273 done
 
   246 done
 
   274 declare hrabs_hyperpow_minus_one [simp]
 
   247 declare hrabs_hyperpow_minus_one [simp]
 
   275 
   248 
   276 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
 
   249 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
 
   277 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   250 apply (rule_tac z = n in eq_Abs_hypnat)
 
   278 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   251 apply (rule_tac z = r in eq_Abs_hypreal)
 
   279 apply (rule_tac z = "s" in eq_Abs_hypreal)
 
   252 apply (rule_tac z = s in eq_Abs_hypreal)
 
   280 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 
   253 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 
   281 done
 
   254 done
 
   282 
   255 
   283 lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
 
   256 lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
 
   284 apply (auto simp add: hyperpow_two zero_le_mult_iff)
 
   257 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
   285 done
 
       
   286 declare hyperpow_two_le [simp]
 
   258 declare hyperpow_two_le [simp]
 
   287 
   259 
   288 lemma hrabs_hyperpow_two:
 
   260 lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
 
   289      "abs(x pow (1 + 1)) = x pow (1 + 1)"
 
   261 by (simp add: hrabs_def hyperpow_two_le)
 
   290 apply (simp (no_asm) add: hrabs_eqI1)
 
       
   291 done
 
       
   292 declare hrabs_hyperpow_two [simp]
 
       
   293 
   262 
   294 lemma hyperpow_two_hrabs:
 
   263 lemma hyperpow_two_hrabs:
 
   295      "abs(x) pow (1 + 1)  = x pow (1 + 1)"
 
   264      "abs(x) pow (1 + 1)  = x pow (1 + 1)"
 
   296 apply (simp add: hyperpow_hrabs)
 
   265 apply (simp add: hyperpow_hrabs)
 
   297 done
 
   266 done
 
   299 
   268 
   300 lemma hyperpow_two_gt_one:
 
   269 lemma hyperpow_two_gt_one:
 
   301      "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
 
   270      "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
 
   302 apply (auto simp add: hyperpow_two)
 
   271 apply (auto simp add: hyperpow_two)
 
   303 apply (rule_tac y = "1*1" in order_le_less_trans)
 
   272 apply (rule_tac y = "1*1" in order_le_less_trans)
 
   304 apply (rule_tac [2] hypreal_mult_less_mono)
 
   273 apply (rule_tac [2] hypreal_mult_less_mono, auto)
 
   305 apply auto
 
       
   306 done
 
   274 done
 
   307 
   275 
   308 lemma hyperpow_two_ge_one:
 
   276 lemma hyperpow_two_ge_one:
 
   309      "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
 
   277      "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
 
   310 apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
 
   278 apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
 
   311 done
 
   279 done
 
   312 
   280 
   313 lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
 
   281 lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
 
   314 apply (rule_tac y = "1 pow n" in order_trans)
 
   282 apply (rule_tac y = "1 pow n" in order_trans)
 
   315 apply (rule_tac [2] hyperpow_le)
 
   283 apply (rule_tac [2] hyperpow_le, auto)
 
   316 apply auto
 
       
   317 done
 
   284 done
 
   318 declare two_hyperpow_ge_one [simp]
 
   285 declare two_hyperpow_ge_one [simp]
 
   319 
   286 
   320 lemma hyperpow_minus_one2:
 
   287 lemma hyperpow_minus_one2:
 
   321      "-1 pow ((1 + 1)*n) = (1::hypreal)"
 
   288      "-1 pow ((1 + 1)*n) = (1::hypreal)"
 
   322 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
 
   289 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
 
   323 apply simp
 
   290 apply simp
 
   324 apply (simp only: hypreal_one_def)
 
   291 apply (simp only: hypreal_one_def)
 
   325 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   292 apply (rule eq_Abs_hypnat [of n])
 
   326 apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus)
 
   293 apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus
 
       
   294                       left_distrib)
 
   327 done
 
   295 done
 
   328 declare hyperpow_minus_one2 [simp]
 
   296 declare hyperpow_minus_one2 [simp]
 
   329 
   297 
   330 lemma hyperpow_less_le:
 
   298 lemma hyperpow_less_le:
 
   331      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
 
   299      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
 
   332 apply (rule_tac z = "n" in eq_Abs_hypnat)
 
   300 apply (rule_tac z = n in eq_Abs_hypnat)
 
   333 apply (rule_tac z = "N" in eq_Abs_hypnat)
 
   301 apply (rule_tac z = N in eq_Abs_hypnat)
 
   334 apply (rule_tac z = "r" in eq_Abs_hypreal)
 
   302 apply (rule_tac z = r in eq_Abs_hypreal)
 
   335 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   303 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   336             hypreal_zero_def hypreal_one_def)
 
   304             hypreal_zero_def hypreal_one_def)
 
   337 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
 
   305 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
 
   338 apply (erule FreeUltrafilterNat_Int)
 
   306 apply (erule FreeUltrafilterNat_Int, assumption)
 
   339 apply assumption; 
       
   340 apply (auto intro: power_decreasing)
 
   307 apply (auto intro: power_decreasing)
 
   341 done
 
   308 done
 
   342 
   309 
   343 lemma hyperpow_SHNat_le:
 
   310 lemma hyperpow_SHNat_le:
 
   344      "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
 
   311      "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
 
   356 apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
 
   323 apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
 
   357 done
 
   324 done
 
   358 declare hyperpow_SReal [simp]
 
   325 declare hyperpow_SReal [simp]
 
   359 
   326 
   360 lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
 
   327 lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
 
   361 apply (drule HNatInfinite_is_Suc)
 
   328 by (drule HNatInfinite_is_Suc, auto)
 
   362 apply auto
 
       
   363 done
 
       
   364 declare hyperpow_zero_HNatInfinite [simp]
 
   329 declare hyperpow_zero_HNatInfinite [simp]
 
   365 
   330 
   366 lemma hyperpow_le_le:
 
   331 lemma hyperpow_le_le:
 
   367      "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
 
   332      "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
 
   368 apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq)
 
   333 apply (drule order_le_less [of n, THEN iffD1])
 
   369 apply (auto intro: hyperpow_less_le)
 
   334 apply (auto intro: hyperpow_less_le)
 
   370 done
 
   335 done
 
   371 
   336 
   372 lemma hyperpow_Suc_le_self2:
 
   337 lemma hyperpow_Suc_le_self2:
 
   373      "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
 
   338      "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
 
   383 done
 
   348 done
 
   384 
   349 
   385 lemma Infinitesimal_hyperpow:
 
   350 lemma Infinitesimal_hyperpow:
 
   386      "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
 
   351      "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
 
   387 apply (rule hrabs_le_Infinitesimal)
 
   352 apply (rule hrabs_le_Infinitesimal)
 
   388 apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
 
   353 apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
 
   389 apply auto
 
       
   390 done
 
   354 done
 
   391 
   355 
   392 lemma hrealpow_hyperpow_Infinitesimal_iff:
 
   356 lemma hrealpow_hyperpow_Infinitesimal_iff:
 
   393      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
 
   357      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
 
   394 apply (unfold hypnat_of_nat_def)
 
   358 apply (unfold hypnat_of_nat_def)
 
   395 apply (rule_tac z = "x" in eq_Abs_hypreal)
 
   359 apply (rule_tac z = x in eq_Abs_hypreal)
 
   396 apply (auto simp add: hrealpow hyperpow)
 
   360 apply (auto simp add: hrealpow hyperpow)
 
   397 done
 
   361 done
 
   398 
   362 
   399 lemma Infinitesimal_hrealpow:
 
   363 lemma Infinitesimal_hrealpow:
 
   400      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 
   364      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 
   401 by (force intro!: Infinitesimal_hyperpow
 
   365 by (force intro!: Infinitesimal_hyperpow
 
   402           simp add: hrealpow_hyperpow_Infinitesimal_iff 
   366           simp add: hrealpow_hyperpow_Infinitesimal_iff 
   403                     hypnat_of_nat_less_iff hypnat_of_nat_zero
 
   367                     hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
 
   404           simp del: hypnat_of_nat_less_iff [symmetric])
 
   368           simp del: hypnat_of_nat_less_iff)
 
   405 
   369 
   406 ML
 
   370 ML
 
   407 {*
 
   371 {*
 
   408 val hrealpow_two = thm "hrealpow_two";
 
   372 val hrealpow_two = thm "hrealpow_two";
 
   409 val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
 
   373 val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
wneuper/isa