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