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