src/HOL/Nonstandard_Analysis/HyperDef.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64438 f91cae6c1d74
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/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 section \<open>Construction of Hyperreals Using Ultrafilters\<close>
     8 
     9 theory HyperDef
    10   imports Complex_Main HyperNat
    11 begin
    12 
    13 type_synonym hypreal = "real star"
    14 
    15 abbreviation hypreal_of_real :: "real \<Rightarrow> real star"
    16   where "hypreal_of_real \<equiv> star_of"
    17 
    18 abbreviation hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal"
    19   where "hypreal_of_hypnat \<equiv> of_hypnat"
    20 
    21 definition omega :: hypreal  ("\<omega>")
    22   where "\<omega> = star_n (\<lambda>n. real (Suc n))"
    23     \<comment> \<open>an infinite number \<open>= [<1, 2, 3, \<dots>>]\<close>\<close>
    24 
    25 definition epsilon :: hypreal  ("\<epsilon>")
    26   where "\<epsilon> = star_n (\<lambda>n. inverse (real (Suc n)))"
    27     \<comment> \<open>an infinitesimal number \<open>= [<1, 1/2, 1/3, \<dots>>]\<close>\<close>
    28 
    29 
    30 subsection \<open>Real vector class instances\<close>
    31 
    32 instantiation star :: (scaleR) scaleR
    33 begin
    34   definition star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
    35   instance ..
    36 end
    37 
    38 lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
    39   by (simp add: star_scaleR_def)
    40 
    41 lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
    42   by transfer (rule refl)
    43 
    44 instance star :: (real_vector) real_vector
    45 proof
    46   fix a b :: real
    47   show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
    48     by transfer (rule scaleR_right_distrib)
    49   show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
    50     by transfer (rule scaleR_left_distrib)
    51   show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
    52     by transfer (rule scaleR_scaleR)
    53   show "\<And>x::'a star. scaleR 1 x = x"
    54     by transfer (rule scaleR_one)
    55 qed
    56 
    57 instance star :: (real_algebra) real_algebra
    58 proof
    59   fix a :: real
    60   show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)"
    61     by transfer (rule mult_scaleR_left)
    62   show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)"
    63     by transfer (rule mult_scaleR_right)
    64 qed
    65 
    66 instance star :: (real_algebra_1) real_algebra_1 ..
    67 
    68 instance star :: (real_div_algebra) real_div_algebra ..
    69 
    70 instance star :: (field_char_0) field_char_0 ..
    71 
    72 instance star :: (real_field) real_field ..
    73 
    74 lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
    75   by (unfold of_real_def, transfer, rule refl)
    76 
    77 lemma Standard_of_real [simp]: "of_real r \<in> Standard"
    78   by (simp add: star_of_real_def)
    79 
    80 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
    81   by transfer (rule refl)
    82 
    83 lemma of_real_eq_star_of [simp]: "of_real = star_of"
    84 proof
    85   show "of_real r = star_of r" for r :: real
    86     by transfer simp
    87 qed
    88 
    89 lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard"
    90   by (simp add: Reals_def Standard_def)
    91 
    92 
    93 subsection \<open>Injection from @{typ hypreal}\<close>
    94 
    95 definition of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star"
    96   where [transfer_unfold]: "of_hypreal = *f* of_real"
    97 
    98 lemma Standard_of_hypreal [simp]: "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
    99   by (simp add: of_hypreal_def)
   100 
   101 lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0"
   102   by transfer (rule of_real_0)
   103 
   104 lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1"
   105   by transfer (rule of_real_1)
   106 
   107 lemma of_hypreal_add [simp]: "\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y"
   108   by transfer (rule of_real_add)
   109 
   110 lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x"
   111   by transfer (rule of_real_minus)
   112 
   113 lemma of_hypreal_diff [simp]: "\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y"
   114   by transfer (rule of_real_diff)
   115 
   116 lemma of_hypreal_mult [simp]: "\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y"
   117   by transfer (rule of_real_mult)
   118 
   119 lemma of_hypreal_inverse [simp]:
   120   "\<And>x. of_hypreal (inverse x) =
   121     inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)"
   122   by transfer (rule of_real_inverse)
   123 
   124 lemma of_hypreal_divide [simp]:
   125   "\<And>x y. of_hypreal (x / y) =
   126     (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)"
   127   by transfer (rule of_real_divide)
   128 
   129 lemma of_hypreal_eq_iff [simp]: "\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)"
   130   by transfer (rule of_real_eq_iff)
   131 
   132 lemma of_hypreal_eq_0_iff [simp]: "\<And>x. (of_hypreal x = 0) = (x = 0)"
   133   by transfer (rule of_real_eq_0_iff)
   134 
   135 
   136 subsection \<open>Properties of @{term starrel}\<close>
   137 
   138 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
   139   by (simp add: starrel_def)
   140 
   141 lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
   142   by (simp add: star_def starrel_def quotient_def, blast)
   143 
   144 declare Abs_star_inject [simp] Abs_star_inverse [simp]
   145 declare equiv_starrel [THEN eq_equiv_class_iff, simp]
   146 
   147 
   148 subsection \<open>@{term hypreal_of_real}: the Injection from @{typ real} to @{typ hypreal}\<close>
   149 
   150 lemma inj_star_of: "inj star_of"
   151   by (rule inj_onI) simp
   152 
   153 lemma mem_Rep_star_iff: "X \<in> Rep_star x \<longleftrightarrow> x = star_n X"
   154   by (cases x) (simp add: star_n_def)
   155 
   156 lemma Rep_star_star_n_iff [simp]: "X \<in> Rep_star (star_n Y) \<longleftrightarrow> eventually (\<lambda>n. Y n = X n) \<U>"
   157   by (simp add: star_n_def)
   158 
   159 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
   160   by simp
   161 
   162 
   163 subsection \<open>Properties of @{term star_n}\<close>
   164 
   165 lemma star_n_add: "star_n X + star_n Y = star_n (\<lambda>n. X n + Y n)"
   166   by (simp only: star_add_def starfun2_star_n)
   167 
   168 lemma star_n_minus: "- star_n X = star_n (\<lambda>n. -(X n))"
   169   by (simp only: star_minus_def starfun_star_n)
   170 
   171 lemma star_n_diff: "star_n X - star_n Y = star_n (\<lambda>n. X n - Y n)"
   172   by (simp only: star_diff_def starfun2_star_n)
   173 
   174 lemma star_n_mult: "star_n X * star_n Y = star_n (\<lambda>n. X n * Y n)"
   175   by (simp only: star_mult_def starfun2_star_n)
   176 
   177 lemma star_n_inverse: "inverse (star_n X) = star_n (\<lambda>n. inverse (X n))"
   178   by (simp only: star_inverse_def starfun_star_n)
   179 
   180 lemma star_n_le: "star_n X \<le> star_n Y = eventually (\<lambda>n. X n \<le> Y n) \<U>"
   181   by (simp only: star_le_def starP2_star_n)
   182 
   183 lemma star_n_less: "star_n X < star_n Y = eventually (\<lambda>n. X n < Y n) \<U>"
   184   by (simp only: star_less_def starP2_star_n)
   185 
   186 lemma star_n_zero_num: "0 = star_n (\<lambda>n. 0)"
   187   by (simp only: star_zero_def star_of_def)
   188 
   189 lemma star_n_one_num: "1 = star_n (\<lambda>n. 1)"
   190   by (simp only: star_one_def star_of_def)
   191 
   192 lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (\<lambda>n. \<bar>X n\<bar>)"
   193   by (simp only: star_abs_def starfun_star_n)
   194 
   195 lemma hypreal_omega_gt_zero [simp]: "0 < \<omega>"
   196   by (simp add: omega_def star_n_zero_num star_n_less)
   197 
   198 
   199 subsection \<open>Existence of Infinite Hyperreal Number\<close>
   200 
   201 text \<open>Existence of infinite number not corresponding to any real number.
   202   Use assumption that member @{term \<U>} is not finite.\<close>
   203 
   204 text \<open>A few lemmas first.\<close>
   205 
   206 lemma lemma_omega_empty_singleton_disj:
   207   "{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
   208   by force
   209 
   210 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
   211   using lemma_omega_empty_singleton_disj [of x] by auto
   212 
   213 lemma not_ex_hypreal_of_real_eq_omega: "\<nexists>x. hypreal_of_real x = \<omega>"
   214   apply (simp add: omega_def star_of_def star_n_eq_iff)
   215   apply clarify
   216   apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
   217   apply (erule eventually_mono)
   218   apply auto
   219   done
   220 
   221 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>"
   222   using not_ex_hypreal_of_real_eq_omega by auto
   223 
   224 text \<open>Existence of infinitesimal number also not corresponding to any real number.\<close>
   225 
   226 lemma lemma_epsilon_empty_singleton_disj:
   227   "{n::nat. x = inverse(real(Suc n))} = {} \<or> (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
   228   by auto
   229 
   230 lemma lemma_finite_epsilon_set: "finite {n. x = inverse (real (Suc n))}"
   231   using lemma_epsilon_empty_singleton_disj [of x] by auto
   232 
   233 lemma not_ex_hypreal_of_real_eq_epsilon: "\<nexists>x. hypreal_of_real x = \<epsilon>"
   234   by (auto simp: epsilon_def star_of_def star_n_eq_iff
   235       lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: of_nat_Suc)
   236 
   237 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>"
   238   using not_ex_hypreal_of_real_eq_epsilon by auto
   239 
   240 lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
   241   by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
   242       del: star_of_zero)
   243 
   244 lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
   245   by (simp add: epsilon_def omega_def star_n_inverse)
   246 
   247 lemma hypreal_epsilon_gt_zero: "0 < \<epsilon>"
   248   by (simp add: hypreal_epsilon_inverse_omega)
   249 
   250 
   251 subsection \<open>Absolute Value Function for the Hyperreals\<close>
   252 
   253 lemma hrabs_add_less: "\<bar>x\<bar> < r \<Longrightarrow> \<bar>y\<bar> < s \<Longrightarrow> \<bar>x + y\<bar> < r + s"
   254   for x y r s :: hypreal
   255   by (simp add: abs_if split: if_split_asm)
   256 
   257 lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r \<Longrightarrow> 0 < r"
   258   for x r :: hypreal
   259   by (blast intro!: order_le_less_trans abs_ge_zero)
   260 
   261 lemma hrabs_disj: "\<bar>x\<bar> = x \<or> \<bar>x\<bar> = -x"
   262   for x :: "'a::abs_if"
   263   by (simp add: abs_if)
   264 
   265 lemma hrabs_add_lemma_disj: "y + - x + (y + - z) = \<bar>x + - z\<bar> \<Longrightarrow> y = z \<or> x = y"
   266   for x y z :: hypreal
   267   by (simp add: abs_if split: if_split_asm)
   268 
   269 
   270 subsection \<open>Embedding the Naturals into the Hyperreals\<close>
   271 
   272 abbreviation hypreal_of_nat :: "nat \<Rightarrow> hypreal"
   273   where "hypreal_of_nat \<equiv> of_nat"
   274 
   275 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
   276   by (simp add: Nats_def image_def)
   277 
   278 text \<open>Naturals embedded in hyperreals: is a hyperreal c.f. NS extension.\<close>
   279 
   280 lemma hypreal_of_nat: "hypreal_of_nat m = star_n (\<lambda>n. real m)"
   281   by (simp add: star_of_def [symmetric])
   282 
   283 declaration \<open>
   284   K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
   285     @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
   286   #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
   287       @{thm star_of_numeral}, @{thm star_of_add},
   288       @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
   289   #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
   290 \<close>
   291 
   292 simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) \<le> n" | "(m::hypreal) = n") =
   293   \<open>K Lin_Arith.simproc\<close>
   294 
   295 
   296 subsection \<open>Exponentials on the Hyperreals\<close>
   297 
   298 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
   299   for r :: hypreal
   300   by (rule power_0)
   301 
   302 lemma hpowr_Suc [simp]: "r ^ (Suc n) = r * (r ^ n)"
   303   for r :: hypreal
   304   by (rule power_Suc)
   305 
   306 lemma hrealpow_two: "r ^ Suc (Suc 0) = r * r"
   307   for r :: hypreal
   308   by simp
   309 
   310 lemma hrealpow_two_le [simp]: "0 \<le> r ^ Suc (Suc 0)"
   311   for r :: hypreal
   312   by (auto simp add: zero_le_mult_iff)
   313 
   314 lemma hrealpow_two_le_add_order [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
   315   for u v :: hypreal
   316   by (simp only: hrealpow_two_le add_nonneg_nonneg)
   317 
   318 lemma hrealpow_two_le_add_order2 [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
   319   for u v w :: hypreal
   320   by (simp only: hrealpow_two_le add_nonneg_nonneg)
   321 
   322 lemma hypreal_add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   323   for x y :: hypreal
   324   by arith
   325 
   326 
   327 (* FIXME: DELETE THESE *)
   328 lemma hypreal_three_squares_add_zero_iff: "x * x + y * y + z * z = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0"
   329   for x y z :: hypreal
   330   by (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff) auto
   331 
   332 lemma hrealpow_three_squares_add_zero_iff [simp]:
   333   "x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0"
   334   for x y z :: hypreal
   335   by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
   336 
   337 (*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
   338   result proved in Rings or Fields*)
   339 lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = x ^ Suc (Suc 0)"
   340   for x :: hypreal
   341   by (simp add: abs_mult)
   342 
   343 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
   344   using power_increasing [of 0 n "2::hypreal"] by simp
   345 
   346 lemma hrealpow: "star_n X ^ m = star_n (\<lambda>n. (X n::real) ^ m)"
   347   by (induct m) (auto simp: star_n_one_num star_n_mult)
   348 
   349 lemma hrealpow_sum_square_expand:
   350   "(x + y) ^ Suc (Suc 0) =
   351     x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0))) * x * y"
   352   for x y :: hypreal
   353   by (simp add: distrib_left distrib_right)
   354 
   355 lemma power_hypreal_of_real_numeral:
   356   "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
   357   by simp
   358 declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w
   359 
   360 lemma power_hypreal_of_real_neg_numeral:
   361   "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
   362   by simp
   363 declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
   364 (*
   365 lemma hrealpow_HFinite:
   366   fixes x :: "'a::{real_normed_algebra,power} star"
   367   shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
   368 apply (induct_tac "n")
   369 apply (auto simp add: power_Suc intro: HFinite_mult)
   370 done
   371 *)
   372 
   373 
   374 subsection \<open>Powers with Hypernatural Exponents\<close>
   375 
   376 text \<open>Hypernatural powers of hyperreals.\<close>
   377 definition pow :: "'a::power star \<Rightarrow> nat star \<Rightarrow> 'a star"  (infixr "pow" 80)
   378   where hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
   379 
   380 lemma Standard_hyperpow [simp]: "r \<in> Standard \<Longrightarrow> n \<in> Standard \<Longrightarrow> r pow n \<in> Standard"
   381   by (simp add: hyperpow_def)
   382 
   383 lemma hyperpow: "star_n X pow star_n Y = star_n (\<lambda>n. X n ^ Y n)"
   384   by (simp add: hyperpow_def starfun2_star_n)
   385 
   386 lemma hyperpow_zero [simp]: "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
   387   by transfer simp
   388 
   389 lemma hyperpow_not_zero: "\<And>r n. r \<noteq> (0::'a::{field} star) \<Longrightarrow> r pow n \<noteq> 0"
   390   by transfer (rule power_not_zero)
   391 
   392 lemma hyperpow_inverse: "\<And>r n. r \<noteq> (0::'a::field star) \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
   393   by transfer (rule power_inverse [symmetric])
   394 
   395 lemma hyperpow_hrabs: "\<And>r n. \<bar>r::'a::{linordered_idom} star\<bar> pow n = \<bar>r pow n\<bar>"
   396   by transfer (rule power_abs [symmetric])
   397 
   398 lemma hyperpow_add: "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
   399   by transfer (rule power_add)
   400 
   401 lemma hyperpow_one [simp]: "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
   402   by transfer (rule power_one_right)
   403 
   404 lemma hyperpow_two: "\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
   405   by transfer (rule power2_eq_square)
   406 
   407 lemma hyperpow_gt_zero: "\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
   408   by transfer (rule zero_less_power)
   409 
   410 lemma hyperpow_ge_zero: "\<And>r n. (0::'a::{linordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
   411   by transfer (rule zero_le_power)
   412 
   413 lemma hyperpow_le: "\<And>x y n. (0::'a::{linordered_semidom} star) < x \<Longrightarrow> x \<le> y \<Longrightarrow> x pow n \<le> y pow n"
   414   by transfer (rule power_mono [OF _ order_less_imp_le])
   415 
   416 lemma hyperpow_eq_one [simp]: "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
   417   by transfer (rule power_one)
   418 
   419 lemma hrabs_hyperpow_minus [simp]: "\<And>(a::'a::linordered_idom star) n. \<bar>(-a) pow n\<bar> = \<bar>a pow n\<bar>"
   420   by transfer (rule abs_power_minus)
   421 
   422 lemma hyperpow_mult: "\<And>r s n. (r * s::'a::comm_monoid_mult star) pow n = (r pow n) * (s pow n)"
   423   by transfer (rule power_mult_distrib)
   424 
   425 lemma hyperpow_two_le [simp]: "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
   426   by (auto simp add: hyperpow_two zero_le_mult_iff)
   427 
   428 lemma hrabs_hyperpow_two [simp]:
   429   "\<bar>x pow 2\<bar> = (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
   430   by (simp only: abs_of_nonneg hyperpow_two_le)
   431 
   432 lemma hyperpow_two_hrabs [simp]: "\<bar>x::'a::linordered_idom star\<bar> pow 2 = x pow 2"
   433   by (simp add: hyperpow_hrabs)
   434 
   435 text \<open>The precondition could be weakened to @{term "0\<le>x"}.\<close>
   436 lemma hypreal_mult_less_mono: "u < v \<Longrightarrow> x < y \<Longrightarrow> 0 < v \<Longrightarrow> 0 < x \<Longrightarrow> u * x < v * y"
   437   for u v x y :: hypreal
   438   by (simp add: mult_strict_mono order_less_imp_le)
   439 
   440 lemma hyperpow_two_gt_one: "\<And>r::'a::linordered_semidom star. 1 < r \<Longrightarrow> 1 < r pow 2"
   441   by transfer simp
   442 
   443 lemma hyperpow_two_ge_one: "\<And>r::'a::linordered_semidom star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2"
   444   by transfer (rule one_le_power)
   445 
   446 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   447   apply (rule_tac y = "1 pow n" in order_trans)
   448    apply (rule_tac [2] hyperpow_le)
   449     apply auto
   450   done
   451 
   452 lemma hyperpow_minus_one2 [simp]: "\<And>n. (- 1) pow (2 * n) = (1::hypreal)"
   453   by transfer (rule power_minus1_even)
   454 
   455 lemma hyperpow_less_le: "\<And>r n N. (0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n < N \<Longrightarrow> r pow N \<le> r pow n"
   456   by transfer (rule power_decreasing [OF order_less_imp_le])
   457 
   458 lemma hyperpow_SHNat_le:
   459   "0 \<le> r \<Longrightarrow> r \<le> (1::hypreal) \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> \<forall>n\<in>Nats. r pow N \<le> r pow n"
   460   by (auto intro!: hyperpow_less_le simp: HNatInfinite_iff)
   461 
   462 lemma hyperpow_realpow: "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   463   by transfer (rule refl)
   464 
   465 lemma hyperpow_SReal [simp]: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>"
   466   by (simp add: Reals_eq_Standard)
   467 
   468 lemma hyperpow_zero_HNatInfinite [simp]: "N \<in> HNatInfinite \<Longrightarrow> (0::hypreal) pow N = 0"
   469   by (drule HNatInfinite_is_Suc, auto)
   470 
   471 lemma hyperpow_le_le: "(0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n \<le> N \<Longrightarrow> r pow N \<le> r pow n"
   472   apply (drule order_le_less [of n, THEN iffD1])
   473   apply (auto intro: hyperpow_less_le)
   474   done
   475 
   476 lemma hyperpow_Suc_le_self2: "(0::hypreal) \<le> r \<Longrightarrow> r < 1 \<Longrightarrow> r pow (n + (1::hypnat)) \<le> r"
   477   apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
   478     apply auto
   479   done
   480 
   481 lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
   482   by transfer (rule refl)
   483 
   484 lemma of_hypreal_hyperpow:
   485   "\<And>x n. of_hypreal (x pow n) = (of_hypreal x::'a::{real_algebra_1} star) pow n"
   486   by transfer (rule of_real_power)
   487 
   488 end