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