src/HOL/NSA/HyperDef.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47195 836bf25fb70f
child 49962 a8cc904a6820
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title       : HOL/NSA/HyperDef.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{*Construction of Hyperreals Using Ultrafilters*}
     8 
     9 theory HyperDef
    10 imports HyperNat Real
    11 begin
    12 
    13 type_synonym hypreal = "real star"
    14 
    15 abbreviation
    16   hypreal_of_real :: "real => real star" where
    17   "hypreal_of_real == star_of"
    18 
    19 abbreviation
    20   hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" where
    21   "hypreal_of_hypnat \<equiv> of_hypnat"
    22 
    23 definition
    24   omega :: hypreal where
    25    -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
    26   "omega = star_n (\<lambda>n. real (Suc n))"
    27 
    28 definition
    29   epsilon :: hypreal where
    30    -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
    31   "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
    32 
    33 notation (xsymbols)
    34   omega  ("\<omega>") and
    35   epsilon  ("\<epsilon>")
    36 
    37 notation (HTML output)
    38   omega  ("\<omega>") and
    39   epsilon  ("\<epsilon>")
    40 
    41 
    42 subsection {* Real vector class instances *}
    43 
    44 instantiation star :: (scaleR) scaleR
    45 begin
    46 
    47 definition
    48   star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
    49 
    50 instance ..
    51 
    52 end
    53 
    54 lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
    55 by (simp add: star_scaleR_def)
    56 
    57 lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
    58 by transfer (rule refl)
    59 
    60 instance star :: (real_vector) real_vector
    61 proof
    62   fix a b :: real
    63   show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
    64     by transfer (rule scaleR_right_distrib)
    65   show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
    66     by transfer (rule scaleR_left_distrib)
    67   show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
    68     by transfer (rule scaleR_scaleR)
    69   show "\<And>x::'a star. scaleR 1 x = x"
    70     by transfer (rule scaleR_one)
    71 qed
    72 
    73 instance star :: (real_algebra) real_algebra
    74 proof
    75   fix a :: real
    76   show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)"
    77     by transfer (rule mult_scaleR_left)
    78   show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)"
    79     by transfer (rule mult_scaleR_right)
    80 qed
    81 
    82 instance star :: (real_algebra_1) real_algebra_1 ..
    83 
    84 instance star :: (real_div_algebra) real_div_algebra ..
    85 
    86 instance star :: (field_char_0) field_char_0 ..
    87 
    88 instance star :: (real_field) real_field ..
    89 
    90 lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
    91 by (unfold of_real_def, transfer, rule refl)
    92 
    93 lemma Standard_of_real [simp]: "of_real r \<in> Standard"
    94 by (simp add: star_of_real_def)
    95 
    96 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
    97 by transfer (rule refl)
    98 
    99 lemma of_real_eq_star_of [simp]: "of_real = star_of"
   100 proof
   101   fix r :: real
   102   show "of_real r = star_of r"
   103     by transfer simp
   104 qed
   105 
   106 lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
   107 by (simp add: Reals_def Standard_def)
   108 
   109 
   110 subsection {* Injection from @{typ hypreal} *}
   111 
   112 definition
   113   of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
   114   [transfer_unfold]: "of_hypreal = *f* of_real"
   115 
   116 lemma Standard_of_hypreal [simp]:
   117   "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
   118 by (simp add: of_hypreal_def)
   119 
   120 lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0"
   121 by transfer (rule of_real_0)
   122 
   123 lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1"
   124 by transfer (rule of_real_1)
   125 
   126 lemma of_hypreal_add [simp]:
   127   "\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y"
   128 by transfer (rule of_real_add)
   129 
   130 lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x"
   131 by transfer (rule of_real_minus)
   132 
   133 lemma of_hypreal_diff [simp]:
   134   "\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y"
   135 by transfer (rule of_real_diff)
   136 
   137 lemma of_hypreal_mult [simp]:
   138   "\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y"
   139 by transfer (rule of_real_mult)
   140 
   141 lemma of_hypreal_inverse [simp]:
   142   "\<And>x. of_hypreal (inverse x) =
   143    inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
   144 by transfer (rule of_real_inverse)
   145 
   146 lemma of_hypreal_divide [simp]:
   147   "\<And>x y. of_hypreal (x / y) =
   148    (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
   149 by transfer (rule of_real_divide)
   150 
   151 lemma of_hypreal_eq_iff [simp]:
   152   "\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)"
   153 by transfer (rule of_real_eq_iff)
   154 
   155 lemma of_hypreal_eq_0_iff [simp]:
   156   "\<And>x. (of_hypreal x = 0) = (x = 0)"
   157 by transfer (rule of_real_eq_0_iff)
   158 
   159 
   160 subsection{*Properties of @{term starrel}*}
   161 
   162 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
   163 by (simp add: starrel_def)
   164 
   165 lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
   166 by (simp add: star_def starrel_def quotient_def, blast)
   167 
   168 declare Abs_star_inject [simp] Abs_star_inverse [simp]
   169 declare equiv_starrel [THEN eq_equiv_class_iff, simp]
   170 
   171 subsection{*@{term hypreal_of_real}: 
   172             the Injection from @{typ real} to @{typ hypreal}*}
   173 
   174 lemma inj_star_of: "inj star_of"
   175 by (rule inj_onI, simp)
   176 
   177 lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)"
   178 by (cases x, simp add: star_n_def)
   179 
   180 lemma Rep_star_star_n_iff [simp]:
   181   "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
   182 by (simp add: star_n_def)
   183 
   184 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
   185 by simp
   186 
   187 subsection{* Properties of @{term star_n} *}
   188 
   189 lemma star_n_add:
   190   "star_n X + star_n Y = star_n (%n. X n + Y n)"
   191 by (simp only: star_add_def starfun2_star_n)
   192 
   193 lemma star_n_minus:
   194    "- star_n X = star_n (%n. -(X n))"
   195 by (simp only: star_minus_def starfun_star_n)
   196 
   197 lemma star_n_diff:
   198      "star_n X - star_n Y = star_n (%n. X n - Y n)"
   199 by (simp only: star_diff_def starfun2_star_n)
   200 
   201 lemma star_n_mult:
   202   "star_n X * star_n Y = star_n (%n. X n * Y n)"
   203 by (simp only: star_mult_def starfun2_star_n)
   204 
   205 lemma star_n_inverse:
   206       "inverse (star_n X) = star_n (%n. inverse(X n))"
   207 by (simp only: star_inverse_def starfun_star_n)
   208 
   209 lemma star_n_le:
   210       "star_n X \<le> star_n Y =  
   211        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
   212 by (simp only: star_le_def starP2_star_n)
   213 
   214 lemma star_n_less:
   215       "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   216 by (simp only: star_less_def starP2_star_n)
   217 
   218 lemma star_n_zero_num: "0 = star_n (%n. 0)"
   219 by (simp only: star_zero_def star_of_def)
   220 
   221 lemma star_n_one_num: "1 = star_n (%n. 1)"
   222 by (simp only: star_one_def star_of_def)
   223 
   224 lemma star_n_abs:
   225      "abs (star_n X) = star_n (%n. abs (X n))"
   226 by (simp only: star_abs_def starfun_star_n)
   227 
   228 subsection{*Misc Others*}
   229 
   230 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
   231 by (auto)
   232 
   233 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
   234 by auto
   235 
   236 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
   237 by auto
   238     
   239 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
   240 by auto
   241 
   242 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
   243 by (simp add: omega_def star_n_zero_num star_n_less)
   244 
   245 subsection{*Existence of Infinite Hyperreal Number*}
   246 
   247 text{*Existence of infinite number not corresponding to any real number.
   248 Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
   249 
   250 
   251 text{*A few lemmas first*}
   252 
   253 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
   254       (\<exists>y. {n::nat. x = real n} = {y})"
   255 by force
   256 
   257 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
   258 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
   259 
   260 lemma not_ex_hypreal_of_real_eq_omega: 
   261       "~ (\<exists>x. hypreal_of_real x = omega)"
   262 apply (simp add: omega_def)
   263 apply (simp add: star_of_def star_n_eq_iff)
   264 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
   265             lemma_finite_omega_set [THEN FreeUltrafilterNat.finite])
   266 done
   267 
   268 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
   269 by (insert not_ex_hypreal_of_real_eq_omega, auto)
   270 
   271 text{*Existence of infinitesimal number also not corresponding to any
   272  real number*}
   273 
   274 lemma lemma_epsilon_empty_singleton_disj:
   275      "{n::nat. x = inverse(real(Suc n))} = {} |  
   276       (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
   277 by auto
   278 
   279 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
   280 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
   281 
   282 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
   283 by (auto simp add: epsilon_def star_of_def star_n_eq_iff
   284                    lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite])
   285 
   286 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
   287 by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
   288 
   289 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
   290 by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
   291          del: star_of_zero)
   292 
   293 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
   294 by (simp add: epsilon_def omega_def star_n_inverse)
   295 
   296 lemma hypreal_epsilon_gt_zero: "0 < epsilon"
   297 by (simp add: hypreal_epsilon_inverse_omega)
   298 
   299 subsection{*Absolute Value Function for the Hyperreals*}
   300 
   301 lemma hrabs_add_less:
   302      "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
   303 by (simp add: abs_if split: split_if_asm)
   304 
   305 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
   306 by (blast intro!: order_le_less_trans abs_ge_zero)
   307 
   308 lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x"
   309 by (simp add: abs_if)
   310 
   311 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
   312 by (simp add: abs_if split add: split_if_asm)
   313 
   314 
   315 subsection{*Embedding the Naturals into the Hyperreals*}
   316 
   317 abbreviation
   318   hypreal_of_nat :: "nat => hypreal" where
   319   "hypreal_of_nat == of_nat"
   320 
   321 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
   322 by (simp add: Nats_def image_def)
   323 
   324 (*------------------------------------------------------------*)
   325 (* naturals embedded in hyperreals                            *)
   326 (* is a hyperreal c.f. NS extension                           *)
   327 (*------------------------------------------------------------*)
   328 
   329 lemma hypreal_of_nat_eq:
   330      "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
   331 by (simp add: real_of_nat_def)
   332 
   333 lemma hypreal_of_nat:
   334      "hypreal_of_nat m = star_n (%n. real m)"
   335 apply (fold star_of_def)
   336 apply (simp add: real_of_nat_def)
   337 done
   338 
   339 (*
   340 FIXME: we should declare this, as for type int, but many proofs would break.
   341 It replaces x+-y by x-y.
   342 Addsimps [symmetric hypreal_diff_def]
   343 *)
   344 
   345 declaration {*
   346   K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
   347     @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
   348   #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
   349       @{thm star_of_numeral}, @{thm star_of_neg_numeral}, @{thm star_of_add},
   350       @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
   351   #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
   352 *}
   353 
   354 simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
   355   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
   356 
   357 
   358 subsection {* Exponentials on the Hyperreals *}
   359 
   360 lemma hpowr_0 [simp]:   "r ^ 0       = (1::hypreal)"
   361 by (rule power_0)
   362 
   363 lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
   364 by (rule power_Suc)
   365 
   366 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
   367 by simp
   368 
   369 lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
   370 by (auto simp add: zero_le_mult_iff)
   371 
   372 lemma hrealpow_two_le_add_order [simp]:
   373      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
   374 by (simp only: hrealpow_two_le add_nonneg_nonneg)
   375 
   376 lemma hrealpow_two_le_add_order2 [simp]:
   377      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
   378 by (simp only: hrealpow_two_le add_nonneg_nonneg)
   379 
   380 lemma hypreal_add_nonneg_eq_0_iff:
   381      "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
   382 by arith
   383 
   384 
   385 text{*FIXME: DELETE THESE*}
   386 lemma hypreal_three_squares_add_zero_iff:
   387      "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
   388 apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
   389 done
   390 
   391 lemma hrealpow_three_squares_add_zero_iff [simp]:
   392      "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
   393       (x = 0 & y = 0 & z = 0)"
   394 by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
   395 
   396 (*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
   397   result proved in Rings or Fields*)
   398 lemma hrabs_hrealpow_two [simp]:
   399      "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
   400 by (simp add: abs_mult)
   401 
   402 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
   403 by (insert power_increasing [of 0 n "2::hypreal"], simp)
   404 
   405 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
   406 apply (induct n)
   407 apply (auto simp add: left_distrib)
   408 apply (cut_tac n = n in two_hrealpow_ge_one, arith)
   409 done
   410 
   411 lemma hrealpow:
   412     "star_n X ^ m = star_n (%n. (X n::real) ^ m)"
   413 apply (induct_tac "m")
   414 apply (auto simp add: star_n_one_num star_n_mult power_0)
   415 done
   416 
   417 lemma hrealpow_sum_square_expand:
   418      "(x + (y::hypreal)) ^ Suc (Suc 0) =
   419       x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
   420 by (simp add: right_distrib left_distrib)
   421 
   422 lemma power_hypreal_of_real_numeral:
   423      "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
   424 by simp
   425 declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w
   426 
   427 lemma power_hypreal_of_real_neg_numeral:
   428      "(neg_numeral v :: hypreal) ^ n = hypreal_of_real ((neg_numeral v) ^ n)"
   429 by simp
   430 declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
   431 (*
   432 lemma hrealpow_HFinite:
   433   fixes x :: "'a::{real_normed_algebra,power} star"
   434   shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
   435 apply (induct_tac "n")
   436 apply (auto simp add: power_Suc intro: HFinite_mult)
   437 done
   438 *)
   439 
   440 subsection{*Powers with Hypernatural Exponents*}
   441 
   442 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
   443   hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
   444   (* hypernatural powers of hyperreals *)
   445 
   446 lemma Standard_hyperpow [simp]:
   447   "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
   448 unfolding hyperpow_def by simp
   449 
   450 lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
   451 by (simp add: hyperpow_def starfun2_star_n)
   452 
   453 lemma hyperpow_zero [simp]:
   454   "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
   455 by transfer simp
   456 
   457 lemma hyperpow_not_zero:
   458   "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
   459 by transfer (rule field_power_not_zero)
   460 
   461 lemma hyperpow_inverse:
   462   "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
   463    \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
   464 by transfer (rule power_inverse)
   465   
   466 lemma hyperpow_hrabs:
   467   "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
   468 by transfer (rule power_abs [symmetric])
   469 
   470 lemma hyperpow_add:
   471   "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
   472 by transfer (rule power_add)
   473 
   474 lemma hyperpow_one [simp]:
   475   "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
   476 by transfer (rule power_one_right)
   477 
   478 lemma hyperpow_two:
   479   "\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
   480 by transfer (rule power2_eq_square)
   481 
   482 lemma hyperpow_gt_zero:
   483   "\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
   484 by transfer (rule zero_less_power)
   485 
   486 lemma hyperpow_ge_zero:
   487   "\<And>r n. (0::'a::{linordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
   488 by transfer (rule zero_le_power)
   489 
   490 lemma hyperpow_le:
   491   "\<And>x y n. \<lbrakk>(0::'a::{linordered_semidom} star) < x; x \<le> y\<rbrakk>
   492    \<Longrightarrow> x pow n \<le> y pow n"
   493 by transfer (rule power_mono [OF _ order_less_imp_le])
   494 
   495 lemma hyperpow_eq_one [simp]:
   496   "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
   497 by transfer (rule power_one)
   498 
   499 lemma hrabs_hyperpow_minus_one [simp]:
   500   "\<And>n. abs(-1 pow n) = (1::'a::{linordered_idom} star)"
   501 by transfer (rule abs_power_minus_one)
   502 
   503 lemma hyperpow_mult:
   504   "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
   505    = (r pow n) * (s pow n)"
   506 by transfer (rule power_mult_distrib)
   507 
   508 lemma hyperpow_two_le [simp]:
   509   "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
   510 by (auto simp add: hyperpow_two zero_le_mult_iff)
   511 
   512 lemma hrabs_hyperpow_two [simp]:
   513   "abs(x pow 2) =
   514    (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
   515 by (simp only: abs_of_nonneg hyperpow_two_le)
   516 
   517 lemma hyperpow_two_hrabs [simp]:
   518   "abs(x::'a::{linordered_idom} star) pow 2 = x pow 2"
   519 by (simp add: hyperpow_hrabs)
   520 
   521 text{*The precondition could be weakened to @{term "0\<le>x"}*}
   522 lemma hypreal_mult_less_mono:
   523      "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
   524  by (simp add: mult_strict_mono order_less_imp_le)
   525 
   526 lemma hyperpow_two_gt_one:
   527   "\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow 2"
   528 by transfer simp
   529 
   530 lemma hyperpow_two_ge_one:
   531   "\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2"
   532 by transfer (rule one_le_power)
   533 
   534 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   535 apply (rule_tac y = "1 pow n" in order_trans)
   536 apply (rule_tac [2] hyperpow_le, auto)
   537 done
   538 
   539 lemma hyperpow_minus_one2 [simp]:
   540      "\<And>n. -1 pow (2*n) = (1::hypreal)"
   541 by transfer (rule power_minus1_even)
   542 
   543 lemma hyperpow_less_le:
   544      "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
   545 by transfer (rule power_decreasing [OF order_less_imp_le])
   546 
   547 lemma hyperpow_SHNat_le:
   548      "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
   549       ==> ALL n: Nats. r pow N \<le> r pow n"
   550 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
   551 
   552 lemma hyperpow_realpow:
   553       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   554 by transfer (rule refl)
   555 
   556 lemma hyperpow_SReal [simp]:
   557      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   558 by (simp add: Reals_eq_Standard)
   559 
   560 lemma hyperpow_zero_HNatInfinite [simp]:
   561      "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
   562 by (drule HNatInfinite_is_Suc, auto)
   563 
   564 lemma hyperpow_le_le:
   565      "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
   566 apply (drule order_le_less [of n, THEN iffD1])
   567 apply (auto intro: hyperpow_less_le)
   568 done
   569 
   570 lemma hyperpow_Suc_le_self2:
   571      "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
   572 apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
   573 apply auto
   574 done
   575 
   576 lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
   577 by transfer (rule refl)
   578 
   579 lemma of_hypreal_hyperpow:
   580   "\<And>x n. of_hypreal (x pow n) =
   581    (of_hypreal x::'a::{real_algebra_1} star) pow n"
   582 by transfer (rule of_real_power)
   583 
   584 end