src/HOL/NSA/NSComplex.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47108 2a1953f0d20d
child 49962 a8cc904a6820
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
wenzelm@41959
     1
(*  Title:      HOL/NSA/NSComplex.thy
wenzelm@41959
     2
    Author:     Jacques D. Fleuriot, University of Edinburgh
wenzelm@41959
     3
    Author:     Lawrence C Paulson
huffman@27468
     4
*)
huffman@27468
     5
huffman@27468
     6
header{*Nonstandard Complex Numbers*}
huffman@27468
     7
huffman@27468
     8
theory NSComplex
wenzelm@41413
     9
imports Complex NSA
huffman@27468
    10
begin
huffman@27468
    11
wenzelm@42463
    12
type_synonym hcomplex = "complex star"
huffman@27468
    13
huffman@27468
    14
abbreviation
huffman@27468
    15
  hcomplex_of_complex :: "complex => complex star" where
huffman@27468
    16
  "hcomplex_of_complex == star_of"
huffman@27468
    17
huffman@27468
    18
abbreviation
huffman@27468
    19
  hcmod :: "complex star => real star" where
huffman@27468
    20
  "hcmod == hnorm"
huffman@27468
    21
huffman@27468
    22
huffman@27468
    23
  (*--- real and Imaginary parts ---*)
huffman@27468
    24
huffman@27468
    25
definition
huffman@27468
    26
  hRe :: "hcomplex => hypreal" where
haftmann@37765
    27
  "hRe = *f* Re"
huffman@27468
    28
huffman@27468
    29
definition
huffman@27468
    30
  hIm :: "hcomplex => hypreal" where
haftmann@37765
    31
  "hIm = *f* Im"
huffman@27468
    32
huffman@27468
    33
huffman@27468
    34
  (*------ imaginary unit ----------*)
huffman@27468
    35
huffman@27468
    36
definition
huffman@27468
    37
  iii :: hcomplex where
huffman@27468
    38
  "iii = star_of ii"
huffman@27468
    39
huffman@27468
    40
  (*------- complex conjugate ------*)
huffman@27468
    41
huffman@27468
    42
definition
huffman@27468
    43
  hcnj :: "hcomplex => hcomplex" where
haftmann@37765
    44
  "hcnj = *f* cnj"
huffman@27468
    45
huffman@27468
    46
  (*------------ Argand -------------*)
huffman@27468
    47
huffman@27468
    48
definition
huffman@27468
    49
  hsgn :: "hcomplex => hcomplex" where
haftmann@37765
    50
  "hsgn = *f* sgn"
huffman@27468
    51
huffman@27468
    52
definition
huffman@27468
    53
  harg :: "hcomplex => hypreal" where
haftmann@37765
    54
  "harg = *f* arg"
huffman@27468
    55
huffman@27468
    56
definition
huffman@27468
    57
  (* abbreviation for (cos a + i sin a) *)
huffman@27468
    58
  hcis :: "hypreal => hcomplex" where
haftmann@37765
    59
  "hcis = *f* cis"
huffman@27468
    60
huffman@27468
    61
  (*----- injection from hyperreals -----*)
huffman@27468
    62
huffman@27468
    63
abbreviation
huffman@27468
    64
  hcomplex_of_hypreal :: "hypreal \<Rightarrow> hcomplex" where
huffman@27468
    65
  "hcomplex_of_hypreal \<equiv> of_hypreal"
huffman@27468
    66
huffman@27468
    67
definition
huffman@27468
    68
  (* abbreviation for r*(cos a + i sin a) *)
huffman@27468
    69
  hrcis :: "[hypreal, hypreal] => hcomplex" where
haftmann@37765
    70
  "hrcis = *f2* rcis"
huffman@27468
    71
huffman@27468
    72
  (*------------ e ^ (x + iy) ------------*)
huffman@27468
    73
definition
huffman@27468
    74
  hexpi :: "hcomplex => hcomplex" where
haftmann@37765
    75
  "hexpi = *f* expi"
huffman@27468
    76
huffman@27468
    77
definition
huffman@27468
    78
  HComplex :: "[hypreal,hypreal] => hcomplex" where
haftmann@37765
    79
  "HComplex = *f2* Complex"
huffman@27468
    80
huffman@27468
    81
lemmas hcomplex_defs [transfer_unfold] =
huffman@27468
    82
  hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
huffman@27468
    83
  hrcis_def hexpi_def HComplex_def
huffman@27468
    84
huffman@27468
    85
lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard"
huffman@27468
    86
by (simp add: hcomplex_defs)
huffman@27468
    87
huffman@27468
    88
lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard"
huffman@27468
    89
by (simp add: hcomplex_defs)
huffman@27468
    90
huffman@27468
    91
lemma Standard_iii [simp]: "iii \<in> Standard"
huffman@27468
    92
by (simp add: hcomplex_defs)
huffman@27468
    93
huffman@27468
    94
lemma Standard_hcnj [simp]: "x \<in> Standard \<Longrightarrow> hcnj x \<in> Standard"
huffman@27468
    95
by (simp add: hcomplex_defs)
huffman@27468
    96
huffman@27468
    97
lemma Standard_hsgn [simp]: "x \<in> Standard \<Longrightarrow> hsgn x \<in> Standard"
huffman@27468
    98
by (simp add: hcomplex_defs)
huffman@27468
    99
huffman@27468
   100
lemma Standard_harg [simp]: "x \<in> Standard \<Longrightarrow> harg x \<in> Standard"
huffman@27468
   101
by (simp add: hcomplex_defs)
huffman@27468
   102
huffman@27468
   103
lemma Standard_hcis [simp]: "r \<in> Standard \<Longrightarrow> hcis r \<in> Standard"
huffman@27468
   104
by (simp add: hcomplex_defs)
huffman@27468
   105
huffman@27468
   106
lemma Standard_hexpi [simp]: "x \<in> Standard \<Longrightarrow> hexpi x \<in> Standard"
huffman@27468
   107
by (simp add: hcomplex_defs)
huffman@27468
   108
huffman@27468
   109
lemma Standard_hrcis [simp]:
huffman@27468
   110
  "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> hrcis r s \<in> Standard"
huffman@27468
   111
by (simp add: hcomplex_defs)
huffman@27468
   112
huffman@27468
   113
lemma Standard_HComplex [simp]:
huffman@27468
   114
  "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard"
huffman@27468
   115
by (simp add: hcomplex_defs)
huffman@27468
   116
huffman@27468
   117
lemma hcmod_def: "hcmod = *f* cmod"
huffman@27468
   118
by (rule hnorm_def)
huffman@27468
   119
huffman@27468
   120
huffman@27468
   121
subsection{*Properties of Nonstandard Real and Imaginary Parts*}
huffman@27468
   122
huffman@27468
   123
lemma hcomplex_hRe_hIm_cancel_iff:
huffman@27468
   124
     "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
huffman@27468
   125
by transfer (rule complex_Re_Im_cancel_iff)
huffman@27468
   126
huffman@27468
   127
lemma hcomplex_equality [intro?]:
huffman@27468
   128
  "!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w"
huffman@27468
   129
by transfer (rule complex_equality)
huffman@27468
   130
huffman@27468
   131
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
huffman@27468
   132
by transfer (rule complex_Re_zero)
huffman@27468
   133
huffman@27468
   134
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
huffman@27468
   135
by transfer (rule complex_Im_zero)
huffman@27468
   136
huffman@27468
   137
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
huffman@27468
   138
by transfer (rule complex_Re_one)
huffman@27468
   139
huffman@27468
   140
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
huffman@27468
   141
by transfer (rule complex_Im_one)
huffman@27468
   142
huffman@27468
   143
huffman@27468
   144
subsection{*Addition for Nonstandard Complex Numbers*}
huffman@27468
   145
huffman@27468
   146
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
huffman@27468
   147
by transfer (rule complex_Re_add)
huffman@27468
   148
huffman@27468
   149
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
huffman@27468
   150
by transfer (rule complex_Im_add)
huffman@27468
   151
huffman@27468
   152
subsection{*More Minus Laws*}
huffman@27468
   153
huffman@27468
   154
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
huffman@27468
   155
by transfer (rule complex_Re_minus)
huffman@27468
   156
huffman@27468
   157
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
huffman@27468
   158
by transfer (rule complex_Im_minus)
huffman@27468
   159
huffman@27468
   160
lemma hcomplex_add_minus_eq_minus:
huffman@27468
   161
      "x + y = (0::hcomplex) ==> x = -y"
haftmann@35050
   162
apply (drule minus_unique)
huffman@27468
   163
apply (simp add: minus_equation_iff [of x y])
huffman@27468
   164
done
huffman@27468
   165
huffman@44764
   166
lemma hcomplex_i_mult_eq [simp]: "iii * iii = -1"
huffman@44764
   167
by transfer (rule i_squared)
huffman@27468
   168
huffman@27468
   169
lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
huffman@27468
   170
by transfer (rule complex_i_mult_minus)
huffman@27468
   171
huffman@27468
   172
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
huffman@27468
   173
by transfer (rule complex_i_not_zero)
huffman@27468
   174
huffman@27468
   175
huffman@27468
   176
subsection{*More Multiplication Laws*}
huffman@27468
   177
huffman@27468
   178
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
huffman@27468
   179
by simp
huffman@27468
   180
huffman@27468
   181
lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
huffman@27468
   182
by simp
huffman@27468
   183
huffman@27468
   184
lemma hcomplex_mult_left_cancel:
huffman@27468
   185
     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
huffman@27468
   186
by simp
huffman@27468
   187
huffman@27468
   188
lemma hcomplex_mult_right_cancel:
huffman@27468
   189
     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
huffman@27468
   190
by simp
huffman@27468
   191
huffman@27468
   192
huffman@27468
   193
subsection{*Subraction and Division*}
huffman@27468
   194
huffman@27468
   195
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
huffman@27468
   196
(* TODO: delete *)
haftmann@35050
   197
by (rule diff_eq_eq)
huffman@27468
   198
huffman@27468
   199
huffman@27468
   200
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
huffman@27468
   201
huffman@27468
   202
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
huffman@27468
   203
by transfer (rule Re_complex_of_real)
huffman@27468
   204
huffman@27468
   205
lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0"
huffman@27468
   206
by transfer (rule Im_complex_of_real)
huffman@27468
   207
huffman@27468
   208
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
huffman@27468
   209
     "hcomplex_of_hypreal epsilon \<noteq> 0"
huffman@27468
   210
by (simp add: hypreal_epsilon_not_zero)
huffman@27468
   211
huffman@27468
   212
subsection{*HComplex theorems*}
huffman@27468
   213
huffman@27468
   214
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
huffman@27468
   215
by transfer (rule Re)
huffman@27468
   216
huffman@27468
   217
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
huffman@27468
   218
by transfer (rule Im)
huffman@27468
   219
huffman@27468
   220
lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z"
huffman@27468
   221
by transfer (rule complex_surj)
huffman@27468
   222
huffman@27468
   223
lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]:
huffman@27468
   224
     "(\<And>x y. P (HComplex x y)) ==> P z"
huffman@27468
   225
by (rule hcomplex_surj [THEN subst], blast)
huffman@27468
   226
huffman@27468
   227
huffman@27468
   228
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
huffman@27468
   229
huffman@27468
   230
lemma hcomplex_of_hypreal_abs:
huffman@27468
   231
     "hcomplex_of_hypreal (abs x) =
huffman@27468
   232
      hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
huffman@27468
   233
by simp
huffman@27468
   234
huffman@27468
   235
lemma HComplex_inject [simp]:
huffman@27468
   236
  "!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
huffman@27468
   237
by transfer (rule complex.inject)
huffman@27468
   238
huffman@27468
   239
lemma HComplex_add [simp]:
huffman@27468
   240
  "!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
huffman@27468
   241
by transfer (rule complex_add)
huffman@27468
   242
huffman@27468
   243
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
huffman@27468
   244
by transfer (rule complex_minus)
huffman@27468
   245
huffman@27468
   246
lemma HComplex_diff [simp]:
huffman@27468
   247
  "!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
huffman@27468
   248
by transfer (rule complex_diff)
huffman@27468
   249
huffman@27468
   250
lemma HComplex_mult [simp]:
huffman@27468
   251
  "!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
huffman@27468
   252
   HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
huffman@27468
   253
by transfer (rule complex_mult)
huffman@27468
   254
huffman@27468
   255
(*HComplex_inverse is proved below*)
huffman@27468
   256
huffman@27468
   257
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
huffman@27468
   258
by transfer (rule complex_of_real_def)
huffman@27468
   259
huffman@27468
   260
lemma HComplex_add_hcomplex_of_hypreal [simp]:
huffman@27468
   261
     "!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
huffman@27468
   262
by transfer (rule Complex_add_complex_of_real)
huffman@27468
   263
huffman@27468
   264
lemma hcomplex_of_hypreal_add_HComplex [simp]:
huffman@27468
   265
     "!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
huffman@27468
   266
by transfer (rule complex_of_real_add_Complex)
huffman@27468
   267
huffman@27468
   268
lemma HComplex_mult_hcomplex_of_hypreal:
huffman@27468
   269
     "!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
huffman@27468
   270
by transfer (rule Complex_mult_complex_of_real)
huffman@27468
   271
huffman@27468
   272
lemma hcomplex_of_hypreal_mult_HComplex:
huffman@27468
   273
     "!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
huffman@27468
   274
by transfer (rule complex_of_real_mult_Complex)
huffman@27468
   275
huffman@27468
   276
lemma i_hcomplex_of_hypreal [simp]:
huffman@27468
   277
     "!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
huffman@27468
   278
by transfer (rule i_complex_of_real)
huffman@27468
   279
huffman@27468
   280
lemma hcomplex_of_hypreal_i [simp]:
huffman@27468
   281
     "!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
huffman@27468
   282
by transfer (rule complex_of_real_i)
huffman@27468
   283
huffman@27468
   284
huffman@27468
   285
subsection{*Conjugation*}
huffman@27468
   286
huffman@27468
   287
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
huffman@27468
   288
by transfer (rule complex_cnj_cancel_iff)
huffman@27468
   289
huffman@27468
   290
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
huffman@27468
   291
by transfer (rule complex_cnj_cnj)
huffman@27468
   292
huffman@27468
   293
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
huffman@27468
   294
     "!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
huffman@27468
   295
by transfer (rule complex_cnj_complex_of_real)
huffman@27468
   296
huffman@27468
   297
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
huffman@27468
   298
by transfer (rule complex_mod_cnj)
huffman@27468
   299
huffman@27468
   300
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
huffman@27468
   301
by transfer (rule complex_cnj_minus)
huffman@27468
   302
huffman@27468
   303
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
huffman@27468
   304
by transfer (rule complex_cnj_inverse)
huffman@27468
   305
huffman@27468
   306
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
huffman@27468
   307
by transfer (rule complex_cnj_add)
huffman@27468
   308
huffman@27468
   309
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
huffman@27468
   310
by transfer (rule complex_cnj_diff)
huffman@27468
   311
huffman@27468
   312
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
huffman@27468
   313
by transfer (rule complex_cnj_mult)
huffman@27468
   314
huffman@27468
   315
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
huffman@27468
   316
by transfer (rule complex_cnj_divide)
huffman@27468
   317
huffman@27468
   318
lemma hcnj_one [simp]: "hcnj 1 = 1"
huffman@27468
   319
by transfer (rule complex_cnj_one)
huffman@27468
   320
huffman@27468
   321
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
huffman@27468
   322
by transfer (rule complex_cnj_zero)
huffman@27468
   323
huffman@27468
   324
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
huffman@27468
   325
by transfer (rule complex_cnj_zero_iff)
huffman@27468
   326
huffman@27468
   327
lemma hcomplex_mult_hcnj:
huffman@27468
   328
     "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
huffman@27468
   329
by transfer (rule complex_mult_cnj)
huffman@27468
   330
huffman@27468
   331
huffman@27468
   332
subsection{*More Theorems about the Function @{term hcmod}*}
huffman@27468
   333
huffman@27468
   334
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
huffman@27468
   335
     "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
huffman@27468
   336
by simp
huffman@27468
   337
huffman@27468
   338
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
huffman@27468
   339
     "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
huffman@27468
   340
by simp
huffman@27468
   341
huffman@27468
   342
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
huffman@27468
   343
by transfer (rule complex_mod_mult_cnj)
huffman@27468
   344
huffman@27468
   345
lemma hcmod_triangle_ineq2 [simp]:
huffman@27468
   346
  "!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
huffman@27468
   347
by transfer (rule complex_mod_triangle_ineq2)
huffman@27468
   348
huffman@27468
   349
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
huffman@27468
   350
by transfer (rule norm_diff_ineq)
huffman@27468
   351
huffman@27468
   352
huffman@27468
   353
subsection{*Exponentiation*}
huffman@27468
   354
huffman@27468
   355
lemma hcomplexpow_0 [simp]:   "z ^ 0       = (1::hcomplex)"
huffman@27468
   356
by (rule power_0)
huffman@27468
   357
huffman@27468
   358
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
huffman@27468
   359
by (rule power_Suc)
huffman@27468
   360
huffman@27468
   361
lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
huffman@27468
   362
by transfer (rule power2_i)
huffman@27468
   363
huffman@27468
   364
lemma hcomplex_of_hypreal_pow:
huffman@27468
   365
     "!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
huffman@27468
   366
by transfer (rule of_real_power)
huffman@27468
   367
huffman@27468
   368
lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n"
huffman@27468
   369
by transfer (rule complex_cnj_power)
huffman@27468
   370
huffman@27468
   371
lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n"
huffman@27468
   372
by transfer (rule norm_power)
huffman@27468
   373
huffman@27468
   374
lemma hcpow_minus:
huffman@27468
   375
     "!!x n. (-x::hcomplex) pow n =
huffman@27468
   376
      (if ( *p* even) n then (x pow n) else -(x pow n))"
huffman@27468
   377
by transfer (rule neg_power_if)
huffman@27468
   378
huffman@27468
   379
lemma hcpow_mult:
huffman@27468
   380
  "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
huffman@27468
   381
by transfer (rule power_mult_distrib)
huffman@27468
   382
huffman@27468
   383
lemma hcpow_zero2 [simp]:
haftmann@31019
   384
  "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
huffman@27468
   385
by transfer (rule power_0_Suc)
huffman@27468
   386
huffman@27468
   387
lemma hcpow_not_zero [simp,intro]:
huffman@27468
   388
  "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
huffman@27468
   389
by (rule hyperpow_not_zero)
huffman@27468
   390
huffman@27468
   391
lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
huffman@27468
   392
by (blast intro: ccontr dest: hcpow_not_zero)
huffman@27468
   393
huffman@27468
   394
subsection{*The Function @{term hsgn}*}
huffman@27468
   395
huffman@27468
   396
lemma hsgn_zero [simp]: "hsgn 0 = 0"
huffman@27468
   397
by transfer (rule sgn_zero)
huffman@27468
   398
huffman@27468
   399
lemma hsgn_one [simp]: "hsgn 1 = 1"
huffman@27468
   400
by transfer (rule sgn_one)
huffman@27468
   401
huffman@27468
   402
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)"
huffman@27468
   403
by transfer (rule sgn_minus)
huffman@27468
   404
huffman@27468
   405
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
huffman@27468
   406
by transfer (rule sgn_eq)
huffman@27468
   407
huffman@27468
   408
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
huffman@27468
   409
by transfer (rule complex_norm)
huffman@27468
   410
huffman@27468
   411
lemma hcomplex_eq_cancel_iff1 [simp]:
huffman@27468
   412
     "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
huffman@27468
   413
by (simp add: hcomplex_of_hypreal_eq)
huffman@27468
   414
huffman@27468
   415
lemma hcomplex_eq_cancel_iff2 [simp]:
huffman@27468
   416
     "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
huffman@27468
   417
by (simp add: hcomplex_of_hypreal_eq)
huffman@27468
   418
huffman@27468
   419
lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)"
huffman@27468
   420
by transfer (rule Complex_eq_0)
huffman@27468
   421
huffman@27468
   422
lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)"
huffman@27468
   423
by transfer (rule Complex_eq_1)
huffman@27468
   424
huffman@27468
   425
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
huffman@27468
   426
by transfer (rule i_def [THEN meta_eq_to_obj_eq])
huffman@27468
   427
huffman@27468
   428
lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)"
huffman@27468
   429
by transfer (rule Complex_eq_i)
huffman@27468
   430
huffman@27468
   431
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z"
huffman@27468
   432
by transfer (rule Re_sgn)
huffman@27468
   433
huffman@27468
   434
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
huffman@27468
   435
by transfer (rule Im_sgn)
huffman@27468
   436
huffman@27468
   437
lemma HComplex_inverse:
huffman@27468
   438
     "!!x y. inverse (HComplex x y) =
huffman@27468
   439
      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
huffman@27468
   440
by transfer (rule complex_inverse)
huffman@27468
   441
huffman@27468
   442
lemma hRe_mult_i_eq[simp]:
huffman@27468
   443
    "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
huffman@27468
   444
by transfer simp
huffman@27468
   445
huffman@27468
   446
lemma hIm_mult_i_eq [simp]:
huffman@27468
   447
    "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
huffman@27468
   448
by transfer simp
huffman@27468
   449
huffman@27468
   450
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
huffman@27468
   451
by transfer simp
huffman@27468
   452
huffman@27468
   453
lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
huffman@27468
   454
by transfer simp
huffman@27468
   455
huffman@27468
   456
(*---------------------------------------------------------------------------*)
huffman@27468
   457
(*  harg                                                                     *)
huffman@27468
   458
(*---------------------------------------------------------------------------*)
huffman@27468
   459
huffman@27468
   460
lemma cos_harg_i_mult_zero [simp]:
huffman@27468
   461
     "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
huffman@27468
   462
by transfer (rule cos_arg_i_mult_zero)
huffman@27468
   463
huffman@27468
   464
lemma hcomplex_of_hypreal_zero_iff [simp]:
huffman@27468
   465
     "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
huffman@27468
   466
by transfer (rule of_real_eq_0_iff)
huffman@27468
   467
huffman@27468
   468
huffman@27468
   469
subsection{*Polar Form for Nonstandard Complex Numbers*}
huffman@27468
   470
huffman@27468
   471
lemma complex_split_polar2:
huffman@27468
   472
     "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
huffman@27468
   473
by (blast intro: complex_split_polar)
huffman@27468
   474
huffman@27468
   475
lemma hcomplex_split_polar:
huffman@27468
   476
  "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
huffman@27468
   477
by transfer (rule complex_split_polar)
huffman@27468
   478
huffman@27468
   479
lemma hcis_eq:
huffman@27468
   480
   "!!a. hcis a =
huffman@27468
   481
    (hcomplex_of_hypreal(( *f* cos) a) +
huffman@27468
   482
    iii * hcomplex_of_hypreal(( *f* sin) a))"
huffman@27468
   483
by transfer (simp add: cis_def)
huffman@27468
   484
huffman@27468
   485
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
huffman@27468
   486
by transfer (rule rcis_Ex)
huffman@27468
   487
huffman@27468
   488
lemma hRe_hcomplex_polar [simp]:
huffman@27468
   489
  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
huffman@27468
   490
      r * ( *f* cos) a"
huffman@27468
   491
by transfer simp
huffman@27468
   492
huffman@27468
   493
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a"
huffman@27468
   494
by transfer (rule Re_rcis)
huffman@27468
   495
huffman@27468
   496
lemma hIm_hcomplex_polar [simp]:
huffman@27468
   497
  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
huffman@27468
   498
      r * ( *f* sin) a"
huffman@27468
   499
by transfer simp
huffman@27468
   500
huffman@27468
   501
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a"
huffman@27468
   502
by transfer (rule Im_rcis)
huffman@27468
   503
huffman@27468
   504
lemma hcmod_unit_one [simp]:
huffman@27468
   505
     "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
huffman@27468
   506
by transfer (rule cmod_unit_one)
huffman@27468
   507
huffman@27468
   508
lemma hcmod_complex_polar [simp]:
huffman@27468
   509
  "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
huffman@27468
   510
      abs r"
huffman@27468
   511
by transfer (rule cmod_complex_polar)
huffman@27468
   512
huffman@27468
   513
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
huffman@27468
   514
by transfer (rule complex_mod_rcis)
huffman@27468
   515
huffman@27468
   516
(*---------------------------------------------------------------------------*)
huffman@27468
   517
(*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
huffman@27468
   518
(*---------------------------------------------------------------------------*)
huffman@27468
   519
huffman@27468
   520
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a"
huffman@27468
   521
by transfer (rule cis_rcis_eq)
huffman@27468
   522
declare hcis_hrcis_eq [symmetric, simp]
huffman@27468
   523
huffman@27468
   524
lemma hrcis_mult:
huffman@27468
   525
  "!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
huffman@27468
   526
by transfer (rule rcis_mult)
huffman@27468
   527
huffman@27468
   528
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)"
huffman@27468
   529
by transfer (rule cis_mult)
huffman@27468
   530
huffman@27468
   531
lemma hcis_zero [simp]: "hcis 0 = 1"
huffman@27468
   532
by transfer (rule cis_zero)
huffman@27468
   533
huffman@27468
   534
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0"
huffman@27468
   535
by transfer (rule rcis_zero_mod)
huffman@27468
   536
huffman@27468
   537
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r"
huffman@27468
   538
by transfer (rule rcis_zero_arg)
huffman@27468
   539
huffman@27468
   540
lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x"
huffman@27468
   541
by transfer (rule complex_i_mult_minus)
huffman@27468
   542
huffman@27468
   543
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
huffman@27468
   544
by simp
huffman@27468
   545
huffman@27468
   546
lemma hcis_hypreal_of_nat_Suc_mult:
huffman@27468
   547
   "!!a. hcis (hypreal_of_nat (Suc n) * a) =
huffman@27468
   548
     hcis a * hcis (hypreal_of_nat n * a)"
huffman@27468
   549
apply transfer
huffman@44824
   550
apply (simp add: left_distrib cis_mult)
huffman@27468
   551
done
huffman@27468
   552
huffman@27468
   553
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
huffman@27468
   554
apply transfer
huffman@27468
   555
apply (fold real_of_nat_def)
huffman@27468
   556
apply (rule DeMoivre)
huffman@27468
   557
done
huffman@27468
   558
huffman@27468
   559
lemma hcis_hypreal_of_hypnat_Suc_mult:
huffman@27468
   560
     "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
huffman@27468
   561
      hcis a * hcis (hypreal_of_hypnat n * a)"
huffman@44824
   562
by transfer (simp add: left_distrib cis_mult)
huffman@27468
   563
huffman@27468
   564
lemma NSDeMoivre_ext:
huffman@27468
   565
  "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
huffman@27468
   566
by transfer (fold real_of_nat_def, rule DeMoivre)
huffman@27468
   567
huffman@27468
   568
lemma NSDeMoivre2:
huffman@27468
   569
  "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
huffman@27468
   570
by transfer (fold real_of_nat_def, rule DeMoivre2)
huffman@27468
   571
huffman@27468
   572
lemma DeMoivre2_ext:
huffman@27468
   573
  "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
huffman@27468
   574
by transfer (fold real_of_nat_def, rule DeMoivre2)
huffman@27468
   575
huffman@27468
   576
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
huffman@27468
   577
by transfer (rule cis_inverse)
huffman@27468
   578
huffman@27468
   579
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
huffman@27468
   580
by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
huffman@27468
   581
huffman@27468
   582
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
huffman@27468
   583
by transfer (rule Re_cis)
huffman@27468
   584
huffman@27468
   585
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
huffman@27468
   586
by transfer (rule Im_cis)
huffman@27468
   587
huffman@27468
   588
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
huffman@27468
   589
by (simp add: NSDeMoivre)
huffman@27468
   590
huffman@27468
   591
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
huffman@27468
   592
by (simp add: NSDeMoivre)
huffman@27468
   593
huffman@27468
   594
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
huffman@27468
   595
by (simp add: NSDeMoivre_ext)
huffman@27468
   596
huffman@27468
   597
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
huffman@27468
   598
by (simp add: NSDeMoivre_ext)
huffman@27468
   599
huffman@27468
   600
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
huffman@44711
   601
by transfer (rule exp_add)
huffman@27468
   602
huffman@27468
   603
huffman@27468
   604
subsection{*@{term hcomplex_of_complex}: the Injection from
huffman@27468
   605
  type @{typ complex} to to @{typ hcomplex}*}
huffman@27468
   606
huffman@27468
   607
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
huffman@27468
   608
(* TODO: delete *)
huffman@27468
   609
by (rule inj_star_of)
huffman@27468
   610
huffman@27468
   611
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
huffman@27468
   612
by (rule iii_def)
huffman@27468
   613
huffman@27468
   614
lemma hRe_hcomplex_of_complex:
huffman@27468
   615
   "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
huffman@27468
   616
by transfer (rule refl)
huffman@27468
   617
huffman@27468
   618
lemma hIm_hcomplex_of_complex:
huffman@27468
   619
   "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
huffman@27468
   620
by transfer (rule refl)
huffman@27468
   621
huffman@27468
   622
lemma hcmod_hcomplex_of_complex:
huffman@27468
   623
     "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
huffman@27468
   624
by transfer (rule refl)
huffman@27468
   625
huffman@27468
   626
huffman@27468
   627
subsection{*Numerals and Arithmetic*}
huffman@27468
   628
huffman@27468
   629
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
huffman@27468
   630
     "hcomplex_of_hypreal (hypreal_of_real x) =  
huffman@27468
   631
      hcomplex_of_complex (complex_of_real x)"
huffman@27468
   632
by transfer (rule refl)
huffman@27468
   633
huffman@47108
   634
lemma hcomplex_hypreal_numeral:
huffman@47108
   635
  "hcomplex_of_complex (numeral w) = hcomplex_of_hypreal(numeral w)"
huffman@47108
   636
by transfer (rule of_real_numeral [symmetric])
huffman@27468
   637
huffman@47108
   638
lemma hcomplex_hypreal_neg_numeral:
huffman@47108
   639
  "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
huffman@47108
   640
by transfer (rule of_real_neg_numeral [symmetric])
huffman@47108
   641
huffman@47108
   642
lemma hcomplex_numeral_hcnj [simp]:
huffman@47108
   643
     "hcnj (numeral v :: hcomplex) = numeral v"
huffman@47108
   644
by transfer (rule complex_cnj_numeral)
huffman@27468
   645
huffman@47108
   646
lemma hcomplex_numeral_hcmod [simp]:
huffman@47108
   647
      "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
huffman@47108
   648
by transfer (rule norm_numeral)
huffman@47108
   649
huffman@47108
   650
lemma hcomplex_neg_numeral_hcmod [simp]: 
huffman@47108
   651
      "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
huffman@47108
   652
by transfer (rule norm_neg_numeral)
huffman@27468
   653
huffman@47108
   654
lemma hcomplex_numeral_hRe [simp]: 
huffman@47108
   655
      "hRe(numeral v :: hcomplex) = numeral v"
huffman@47108
   656
by transfer (rule complex_Re_numeral)
huffman@27468
   657
huffman@47108
   658
lemma hcomplex_numeral_hIm [simp]: 
huffman@47108
   659
      "hIm(numeral v :: hcomplex) = 0"
huffman@47108
   660
by transfer (rule complex_Im_numeral)
huffman@27468
   661
huffman@47108
   662
(* TODO: add neg_numeral rules above *)
huffman@27468
   663
end