src/HOL/Hyperreal/HyperPow.thy
author paulson
Sun Feb 15 10:46:37 2004 +0100 (2004-02-15)
changeset 14387 e96d5c42c4b0
parent 14378 69c4d5997669
child 14435 9e22eeccf129
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
paulson@10751
     1
(*  Title       : HyperPow.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot  
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@10751
     4
    Description : Powers theory for hyperreals
paulson@14387
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
paulson@10751
     6
*)
paulson@10751
     7
paulson@14348
     8
header{*Exponentials on the Hyperreals*}
paulson@14348
     9
paulson@14371
    10
theory HyperPow = HyperArith + HyperNat + RealPow:
paulson@10778
    11
paulson@14348
    12
instance hypreal :: power ..
paulson@10751
    13
paulson@10751
    14
consts hpowr :: "[hypreal,nat] => hypreal"  
paulson@10751
    15
primrec
paulson@14348
    16
   hpowr_0:   "r ^ 0       = (1::hypreal)"
paulson@14348
    17
   hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
paulson@14348
    18
paulson@14348
    19
paulson@14348
    20
instance hypreal :: ringpower
paulson@14348
    21
proof
paulson@14348
    22
  fix z :: hypreal
paulson@14348
    23
  fix n :: nat
paulson@14348
    24
  show "z^0 = 1" by simp
paulson@14348
    25
  show "z^(Suc n) = z * (z^n)" by simp
paulson@14348
    26
qed
paulson@14348
    27
paulson@10751
    28
paulson@10751
    29
consts
paulson@14348
    30
  "pow"  :: "[hypreal,hypnat] => hypreal"     (infixr 80)
paulson@10751
    31
paulson@10751
    32
defs
paulson@10751
    33
paulson@10751
    34
  (* hypernatural powers of hyperreals *)
paulson@14348
    35
  hyperpow_def:
paulson@14348
    36
  "(R::hypreal) pow (N::hypnat) ==
paulson@14348
    37
      Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
paulson@14348
    38
                        hyprel``{%n::nat. (X n) ^ (Y n)})"
paulson@14348
    39
paulson@14348
    40
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
paulson@14348
    41
apply (simp (no_asm))
paulson@14348
    42
done
paulson@14348
    43
paulson@14348
    44
lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
paulson@14371
    45
by (simp add: power_abs)
paulson@14348
    46
paulson@14348
    47
lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
paulson@14371
    48
by (auto simp add: zero_le_mult_iff)
paulson@14348
    49
declare hrealpow_two_le [simp]
paulson@14348
    50
paulson@14348
    51
lemma hrealpow_two_le_add_order:
paulson@14348
    52
     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
paulson@14348
    53
apply (simp only: hrealpow_two_le hypreal_le_add_order)
paulson@14348
    54
done
paulson@14348
    55
declare hrealpow_two_le_add_order [simp]
paulson@14348
    56
paulson@14348
    57
lemma hrealpow_two_le_add_order2:
paulson@14348
    58
     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
paulson@14348
    59
apply (simp only: hrealpow_two_le hypreal_le_add_order)
paulson@14348
    60
done
paulson@14348
    61
declare hrealpow_two_le_add_order2 [simp]
paulson@14348
    62
paulson@14348
    63
lemma hypreal_add_nonneg_eq_0_iff:
paulson@14348
    64
     "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
paulson@14348
    65
apply arith
paulson@14348
    66
done
paulson@14348
    67
paulson@14348
    68
text{*FIXME: DELETE THESE*}
paulson@14348
    69
lemma hypreal_three_squares_add_zero_iff:
paulson@14348
    70
     "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
paulson@14371
    71
apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
paulson@14348
    72
done
paulson@14348
    73
paulson@14348
    74
lemma hrealpow_three_squares_add_zero_iff [simp]:
paulson@14348
    75
     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
paulson@14348
    76
      (x = 0 & y = 0 & z = 0)"
paulson@14348
    77
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
paulson@14348
    78
paulson@14348
    79
paulson@14348
    80
lemma hrabs_hrealpow_two [simp]:
paulson@14348
    81
     "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
paulson@14348
    82
by (simp add: abs_mult)
paulson@14348
    83
paulson@14348
    84
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
paulson@14348
    85
by (insert power_increasing [of 0 n "2::hypreal"], simp)
paulson@14348
    86
paulson@14348
    87
lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
paulson@14348
    88
apply (induct_tac "n")
paulson@14348
    89
apply (auto simp add: hypreal_of_nat_Suc left_distrib)
paulson@14371
    90
apply (cut_tac n = n in two_hrealpow_ge_one, arith)
paulson@14348
    91
done
paulson@14348
    92
declare two_hrealpow_gt [simp] 
paulson@14348
    93
paulson@14348
    94
lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
paulson@14371
    95
by (induct_tac "n", auto)
paulson@14348
    96
paulson@14348
    97
lemma double_lemma: "n+n = (2*n::nat)"
paulson@14371
    98
by auto
paulson@14348
    99
paulson@14348
   100
(*ugh: need to get rid fo the n+n*)
paulson@14348
   101
lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
paulson@14371
   102
by (auto simp add: double_lemma hrealpow_minus_one)
paulson@14348
   103
declare hrealpow_minus_one2 [simp]
paulson@14348
   104
paulson@14348
   105
lemma hrealpow:
paulson@14348
   106
    "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
paulson@14348
   107
apply (induct_tac "m")
paulson@14348
   108
apply (auto simp add: hypreal_one_def hypreal_mult)
paulson@14348
   109
done
paulson@14348
   110
paulson@14348
   111
lemma hrealpow_sum_square_expand:
paulson@14348
   112
     "(x + (y::hypreal)) ^ Suc (Suc 0) =
paulson@14348
   113
      x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
paulson@14348
   114
by (simp add: right_distrib left_distrib hypreal_of_nat_Suc)
paulson@14348
   115
paulson@14348
   116
paulson@14348
   117
subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
paulson@14348
   118
paulson@14348
   119
lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
paulson@14348
   120
apply (induct_tac "n")
paulson@14348
   121
apply (simp_all add: nat_mult_distrib)
paulson@14348
   122
done
paulson@14348
   123
declare hypreal_of_real_power [simp]
paulson@14348
   124
paulson@14348
   125
lemma power_hypreal_of_real_number_of:
paulson@14348
   126
     "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
paulson@14387
   127
by (simp only: hypreal_number_of [symmetric] hypreal_of_real_power)
paulson@14348
   128
paulson@14348
   129
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
paulson@14348
   130
paulson@14348
   131
lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite"
paulson@14348
   132
apply (induct_tac "n")
paulson@14348
   133
apply (auto intro: HFinite_mult)
paulson@14348
   134
done
paulson@14348
   135
paulson@14348
   136
paulson@14348
   137
subsection{*Powers with Hypernatural Exponents*}
paulson@14348
   138
paulson@14348
   139
lemma hyperpow_congruent:
paulson@14348
   140
     "congruent hyprel
paulson@14348
   141
     (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
paulson@14348
   142
apply (unfold congruent_def)
paulson@14371
   143
apply (auto intro!: ext, fuf+)
paulson@14348
   144
done
paulson@14348
   145
paulson@14348
   146
lemma hyperpow:
paulson@14348
   147
  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
paulson@14348
   148
   Abs_hypreal(hyprel``{%n. X n ^ Y n})"
paulson@14348
   149
apply (unfold hyperpow_def)
paulson@14371
   150
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14348
   151
apply (auto intro!: lemma_hyprel_refl bexI 
paulson@14348
   152
           simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
paulson@14371
   153
                     hyperpow_congruent, fuf)
paulson@14348
   154
done
paulson@14348
   155
paulson@14348
   156
lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
paulson@14348
   157
apply (unfold hypnat_one_def)
paulson@14348
   158
apply (simp (no_asm) add: hypreal_zero_def)
paulson@14371
   159
apply (rule_tac z = n in eq_Abs_hypnat)
paulson@14348
   160
apply (auto simp add: hyperpow hypnat_add)
paulson@14348
   161
done
paulson@14348
   162
declare hyperpow_zero [simp]
paulson@14348
   163
paulson@14348
   164
lemma hyperpow_not_zero [rule_format (no_asm)]:
paulson@14348
   165
     "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
paulson@14348
   166
apply (simp (no_asm) add: hypreal_zero_def)
paulson@14378
   167
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   168
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   169
apply (auto simp add: hyperpow)
paulson@14371
   170
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
paulson@14348
   171
done
paulson@14348
   172
paulson@14348
   173
lemma hyperpow_inverse:
paulson@14348
   174
     "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
paulson@14348
   175
apply (simp (no_asm) add: hypreal_zero_def)
paulson@14378
   176
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   177
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   178
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
paulson@14348
   179
apply (rule FreeUltrafilterNat_subset)
paulson@14348
   180
apply (auto dest: realpow_not_zero intro: power_inverse)
paulson@14348
   181
done
paulson@14348
   182
paulson@14348
   183
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
paulson@14378
   184
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   185
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   186
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
paulson@14348
   187
done
paulson@14348
   188
paulson@14348
   189
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
paulson@14378
   190
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   191
apply (rule eq_Abs_hypnat [of m])
paulson@14378
   192
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   193
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
paulson@14348
   194
done
paulson@14348
   195
paulson@14348
   196
lemma hyperpow_one: "r pow (1::hypnat) = r"
paulson@14348
   197
apply (unfold hypnat_one_def)
paulson@14378
   198
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   199
apply (auto simp add: hyperpow)
paulson@14348
   200
done
paulson@14348
   201
declare hyperpow_one [simp]
paulson@14348
   202
paulson@14348
   203
lemma hyperpow_two:
paulson@14348
   204
     "r pow ((1::hypnat) + (1::hypnat)) = r * r"
paulson@14348
   205
apply (unfold hypnat_one_def)
paulson@14378
   206
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   207
apply (auto simp add: hyperpow hypnat_add hypreal_mult)
paulson@14348
   208
done
paulson@14348
   209
paulson@14348
   210
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
paulson@14348
   211
apply (simp add: hypreal_zero_def)
paulson@14378
   212
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   213
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   214
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
paulson@14348
   215
                   simp add: hyperpow hypreal_less hypreal_le)
paulson@14348
   216
done
paulson@14348
   217
paulson@14348
   218
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
paulson@14348
   219
apply (simp add: hypreal_zero_def)
paulson@14378
   220
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   221
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   222
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
paulson@14348
   223
            simp add: hyperpow hypreal_le)
paulson@14348
   224
done
paulson@14348
   225
paulson@14348
   226
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
paulson@14348
   227
apply (simp add: hypreal_zero_def)
paulson@14378
   228
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   229
apply (rule eq_Abs_hypreal [of x])
paulson@14378
   230
apply (rule eq_Abs_hypreal [of y])
paulson@14348
   231
apply (auto simp add: hyperpow hypreal_le hypreal_less)
paulson@14371
   232
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
paulson@14348
   233
apply (auto intro: power_mono)
paulson@14348
   234
done
paulson@14348
   235
paulson@14348
   236
lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
paulson@14378
   237
apply (rule eq_Abs_hypnat [of n])
paulson@14348
   238
apply (auto simp add: hypreal_one_def hyperpow)
paulson@14348
   239
done
paulson@14348
   240
declare hyperpow_eq_one [simp]
paulson@14348
   241
paulson@14348
   242
lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
paulson@14348
   243
apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
paulson@14348
   244
apply simp
paulson@14378
   245
apply (rule eq_Abs_hypnat [of n])
paulson@14348
   246
apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
paulson@14348
   247
done
paulson@14348
   248
declare hrabs_hyperpow_minus_one [simp]
paulson@14348
   249
paulson@14348
   250
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
paulson@14378
   251
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   252
apply (rule eq_Abs_hypreal [of r])
paulson@14378
   253
apply (rule eq_Abs_hypreal [of s])
paulson@14348
   254
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
paulson@14348
   255
done
paulson@14348
   256
paulson@14348
   257
lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
paulson@14371
   258
by (auto simp add: hyperpow_two zero_le_mult_iff)
paulson@14348
   259
declare hyperpow_two_le [simp]
paulson@14348
   260
paulson@14371
   261
lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
paulson@14371
   262
by (simp add: hrabs_def hyperpow_two_le)
paulson@14348
   263
paulson@14348
   264
lemma hyperpow_two_hrabs:
paulson@14348
   265
     "abs(x) pow (1 + 1)  = x pow (1 + 1)"
paulson@14348
   266
apply (simp add: hyperpow_hrabs)
paulson@14348
   267
done
paulson@14348
   268
declare hyperpow_two_hrabs [simp]
paulson@14348
   269
paulson@14348
   270
lemma hyperpow_two_gt_one:
paulson@14348
   271
     "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
paulson@14348
   272
apply (auto simp add: hyperpow_two)
paulson@14348
   273
apply (rule_tac y = "1*1" in order_le_less_trans)
paulson@14371
   274
apply (rule_tac [2] hypreal_mult_less_mono, auto)
paulson@14348
   275
done
paulson@14348
   276
paulson@14348
   277
lemma hyperpow_two_ge_one:
paulson@14348
   278
     "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
paulson@14348
   279
apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
paulson@14348
   280
done
paulson@14348
   281
paulson@14348
   282
lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
paulson@14348
   283
apply (rule_tac y = "1 pow n" in order_trans)
paulson@14371
   284
apply (rule_tac [2] hyperpow_le, auto)
paulson@14348
   285
done
paulson@14348
   286
declare two_hyperpow_ge_one [simp]
paulson@14348
   287
paulson@14348
   288
lemma hyperpow_minus_one2:
paulson@14348
   289
     "-1 pow ((1 + 1)*n) = (1::hypreal)"
paulson@14348
   290
apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
paulson@14348
   291
apply simp
paulson@14348
   292
apply (simp only: hypreal_one_def)
paulson@14371
   293
apply (rule eq_Abs_hypnat [of n])
paulson@14371
   294
apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus
paulson@14371
   295
                      left_distrib)
paulson@14348
   296
done
paulson@14348
   297
declare hyperpow_minus_one2 [simp]
paulson@14348
   298
paulson@14348
   299
lemma hyperpow_less_le:
paulson@14348
   300
     "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
paulson@14378
   301
apply (rule eq_Abs_hypnat [of n])
paulson@14378
   302
apply (rule eq_Abs_hypnat [of N])
paulson@14378
   303
apply (rule eq_Abs_hypreal [of r])
paulson@14348
   304
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
paulson@14348
   305
            hypreal_zero_def hypreal_one_def)
paulson@14348
   306
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
paulson@14371
   307
apply (erule FreeUltrafilterNat_Int, assumption)
paulson@14348
   308
apply (auto intro: power_decreasing)
paulson@14348
   309
done
paulson@14348
   310
paulson@14348
   311
lemma hyperpow_SHNat_le:
paulson@14348
   312
     "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
paulson@14348
   313
      ==> ALL n: Nats. r pow N \<le> r pow n"
paulson@14348
   314
by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
paulson@14348
   315
paulson@14348
   316
lemma hyperpow_realpow:
paulson@14348
   317
      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
paulson@14378
   318
apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
paulson@14348
   319
done
paulson@14348
   320
paulson@14348
   321
lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
paulson@14348
   322
apply (unfold SReal_def)
paulson@14348
   323
apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
paulson@14348
   324
done
paulson@14348
   325
declare hyperpow_SReal [simp]
paulson@14348
   326
paulson@14348
   327
lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
paulson@14371
   328
by (drule HNatInfinite_is_Suc, auto)
paulson@14348
   329
declare hyperpow_zero_HNatInfinite [simp]
paulson@14348
   330
paulson@14348
   331
lemma hyperpow_le_le:
paulson@14348
   332
     "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
paulson@14371
   333
apply (drule order_le_less [of n, THEN iffD1])
paulson@14348
   334
apply (auto intro: hyperpow_less_le)
paulson@14348
   335
done
paulson@14348
   336
paulson@14348
   337
lemma hyperpow_Suc_le_self2:
paulson@14348
   338
     "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
paulson@14348
   339
apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
paulson@14348
   340
apply auto
paulson@14348
   341
done
paulson@14348
   342
paulson@14348
   343
lemma lemma_Infinitesimal_hyperpow:
paulson@14348
   344
     "[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
paulson@14348
   345
apply (unfold Infinitesimal_def)
paulson@14348
   346
apply (auto intro!: hyperpow_Suc_le_self2 
paulson@14348
   347
          simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
paulson@14348
   348
done
paulson@14348
   349
paulson@14348
   350
lemma Infinitesimal_hyperpow:
paulson@14348
   351
     "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
paulson@14348
   352
apply (rule hrabs_le_Infinitesimal)
paulson@14371
   353
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
paulson@14348
   354
done
paulson@14348
   355
paulson@14348
   356
lemma hrealpow_hyperpow_Infinitesimal_iff:
paulson@14348
   357
     "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
paulson@14378
   358
apply (rule eq_Abs_hypreal [of x])
paulson@14378
   359
apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
paulson@14348
   360
done
paulson@14348
   361
paulson@14348
   362
lemma Infinitesimal_hrealpow:
paulson@14348
   363
     "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
paulson@14348
   364
by (force intro!: Infinitesimal_hyperpow
paulson@14348
   365
          simp add: hrealpow_hyperpow_Infinitesimal_iff 
paulson@14371
   366
                    hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
paulson@14371
   367
          simp del: hypnat_of_nat_less_iff)
paulson@14348
   368
paulson@14348
   369
ML
paulson@14348
   370
{*
paulson@14348
   371
val hrealpow_two = thm "hrealpow_two";
paulson@14348
   372
val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
paulson@14348
   373
val hrealpow_two_le = thm "hrealpow_two_le";
paulson@14348
   374
val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
paulson@14348
   375
val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
paulson@14348
   376
val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
paulson@14348
   377
val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
paulson@14348
   378
val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
paulson@14348
   379
val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
paulson@14348
   380
val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
paulson@14348
   381
val two_hrealpow_gt = thm "two_hrealpow_gt";
paulson@14348
   382
val hrealpow_minus_one = thm "hrealpow_minus_one";
paulson@14348
   383
val double_lemma = thm "double_lemma";
paulson@14348
   384
val hrealpow_minus_one2 = thm "hrealpow_minus_one2";
paulson@14348
   385
val hrealpow = thm "hrealpow";
paulson@14348
   386
val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
paulson@14348
   387
val hypreal_of_real_power = thm "hypreal_of_real_power";
paulson@14348
   388
val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
paulson@14348
   389
val hrealpow_HFinite = thm "hrealpow_HFinite";
paulson@14348
   390
val hyperpow_congruent = thm "hyperpow_congruent";
paulson@14348
   391
val hyperpow = thm "hyperpow";
paulson@14348
   392
val hyperpow_zero = thm "hyperpow_zero";
paulson@14348
   393
val hyperpow_not_zero = thm "hyperpow_not_zero";
paulson@14348
   394
val hyperpow_inverse = thm "hyperpow_inverse";
paulson@14348
   395
val hyperpow_hrabs = thm "hyperpow_hrabs";
paulson@14348
   396
val hyperpow_add = thm "hyperpow_add";
paulson@14348
   397
val hyperpow_one = thm "hyperpow_one";
paulson@14348
   398
val hyperpow_two = thm "hyperpow_two";
paulson@14348
   399
val hyperpow_gt_zero = thm "hyperpow_gt_zero";
paulson@14348
   400
val hyperpow_ge_zero = thm "hyperpow_ge_zero";
paulson@14348
   401
val hyperpow_le = thm "hyperpow_le";
paulson@14348
   402
val hyperpow_eq_one = thm "hyperpow_eq_one";
paulson@14348
   403
val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
paulson@14348
   404
val hyperpow_mult = thm "hyperpow_mult";
paulson@14348
   405
val hyperpow_two_le = thm "hyperpow_two_le";
paulson@14348
   406
val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
paulson@14348
   407
val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
paulson@14348
   408
val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
paulson@14348
   409
val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
paulson@14348
   410
val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
paulson@14348
   411
val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
paulson@14348
   412
val hyperpow_less_le = thm "hyperpow_less_le";
paulson@14348
   413
val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
paulson@14348
   414
val hyperpow_realpow = thm "hyperpow_realpow";
paulson@14348
   415
val hyperpow_SReal = thm "hyperpow_SReal";
paulson@14348
   416
val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
paulson@14348
   417
val hyperpow_le_le = thm "hyperpow_le_le";
paulson@14348
   418
val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
paulson@14348
   419
val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
paulson@14348
   420
val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
paulson@14348
   421
val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
paulson@14348
   422
val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
paulson@14348
   423
*}
paulson@14348
   424
paulson@10751
   425
end