src/HOL/Complex/NSComplex.thy
author paulson
Mon Mar 08 11:12:06 2004 +0100 (2004-03-08)
changeset 14443 75910c7557c5
parent 14430 5cb24165a2e1
child 14469 c7674b7034f5
permissions -rw-r--r--
generic theorems about exponentials; general tidying up
paulson@13957
     1
(*  Title:       NSComplex.thy
paulson@14430
     2
    ID:      $Id$
paulson@13957
     3
    Author:      Jacques D. Fleuriot
paulson@13957
     4
    Copyright:   2001  University of Edinburgh
paulson@14430
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
paulson@13957
     6
*)
paulson@13957
     7
paulson@14430
     8
header{*Nonstandard Complex Numbers*}
paulson@14430
     9
paulson@14314
    10
theory NSComplex = NSInduct:
paulson@13957
    11
paulson@13957
    12
constdefs
paulson@13957
    13
    hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
paulson@14354
    14
    "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
paulson@13957
    15
                        {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
paulson@13957
    16
paulson@14314
    17
typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
paulson@14314
    18
  by (auto simp add: quotient_def)
paulson@13957
    19
paulson@14314
    20
instance hcomplex :: zero ..
paulson@14314
    21
instance hcomplex :: one ..
paulson@14314
    22
instance hcomplex :: plus ..
paulson@14314
    23
instance hcomplex :: times ..
paulson@14314
    24
instance hcomplex :: minus ..
paulson@14314
    25
instance hcomplex :: inverse ..
paulson@14314
    26
instance hcomplex :: power ..
paulson@14314
    27
paulson@14314
    28
defs (overloaded)
paulson@14314
    29
  hcomplex_zero_def:
paulson@13957
    30
  "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
paulson@14314
    31
paulson@14314
    32
  hcomplex_one_def:
paulson@13957
    33
  "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"
paulson@13957
    34
paulson@13957
    35
paulson@14314
    36
  hcomplex_minus_def:
paulson@14314
    37
  "- z == Abs_hcomplex(UN X: Rep_hcomplex(z).
paulson@14314
    38
                       hcomplexrel `` {%n::nat. - (X n)})"
paulson@13957
    39
paulson@14314
    40
  hcomplex_diff_def:
paulson@13957
    41
  "w - z == w + -(z::hcomplex)"
paulson@14314
    42
paulson@14377
    43
  hcinv_def:
paulson@14377
    44
  "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
paulson@14377
    45
                    hcomplexrel `` {%n. inverse(X n)})"
paulson@14377
    46
paulson@13957
    47
constdefs
paulson@13957
    48
paulson@14314
    49
  hcomplex_of_complex :: "complex => hcomplex"
paulson@13957
    50
  "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
paulson@14314
    51
paulson@13957
    52
  (*--- real and Imaginary parts ---*)
paulson@14314
    53
paulson@14314
    54
  hRe :: "hcomplex => hypreal"
paulson@13957
    55
  "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
paulson@13957
    56
paulson@14314
    57
  hIm :: "hcomplex => hypreal"
paulson@14314
    58
  "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
paulson@13957
    59
paulson@13957
    60
paulson@13957
    61
  (*----------- modulus ------------*)
paulson@13957
    62
paulson@14314
    63
  hcmod :: "hcomplex => hypreal"
paulson@13957
    64
  "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
paulson@13957
    65
			  hyprel `` {%n. cmod (X n)})"
paulson@13957
    66
paulson@14314
    67
  (*------ imaginary unit ----------*)
paulson@14314
    68
paulson@14314
    69
  iii :: hcomplex
paulson@13957
    70
  "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"
paulson@13957
    71
paulson@13957
    72
  (*------- complex conjugate ------*)
paulson@13957
    73
paulson@14314
    74
  hcnj :: "hcomplex => hcomplex"
paulson@13957
    75
  "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"
paulson@13957
    76
paulson@14314
    77
  (*------------ Argand -------------*)
paulson@13957
    78
paulson@14314
    79
  hsgn :: "hcomplex => hcomplex"
paulson@13957
    80
  "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
paulson@13957
    81
paulson@14314
    82
  harg :: "hcomplex => hypreal"
paulson@13957
    83
  "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
paulson@13957
    84
paulson@13957
    85
  (* abbreviation for (cos a + i sin a) *)
paulson@14314
    86
  hcis :: "hypreal => hcomplex"
paulson@13957
    87
  "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
paulson@13957
    88
paulson@13957
    89
  (* abbreviation for r*(cos a + i sin a) *)
paulson@14314
    90
  hrcis :: "[hypreal, hypreal] => hcomplex"
paulson@13957
    91
  "hrcis r a == hcomplex_of_hypreal r * hcis a"
paulson@13957
    92
paulson@14314
    93
  (*----- injection from hyperreals -----*)
paulson@14314
    94
paulson@14314
    95
  hcomplex_of_hypreal :: "hypreal => hcomplex"
paulson@13957
    96
  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
paulson@13957
    97
			       hcomplexrel `` {%n. complex_of_real (X n)})"
paulson@13957
    98
paulson@13957
    99
  (*------------ e ^ (x + iy) ------------*)
paulson@13957
   100
paulson@14314
   101
  hexpi :: "hcomplex => hcomplex"
paulson@13957
   102
  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
paulson@14314
   103
paulson@13957
   104
paulson@14377
   105
constdefs
paulson@14377
   106
  HComplex :: "[hypreal,hypreal] => hcomplex"
paulson@14377
   107
   "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"
paulson@14377
   108
paulson@14377
   109
paulson@14314
   110
defs (overloaded)
paulson@13957
   111
paulson@13957
   112
  (*----------- division ----------*)
paulson@13957
   113
paulson@14314
   114
  hcomplex_divide_def:
paulson@13957
   115
  "w / (z::hcomplex) == w * inverse z"
paulson@14314
   116
paulson@14314
   117
  hcomplex_add_def:
paulson@13957
   118
  "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@13957
   119
		      hcomplexrel `` {%n. X n + Y n})"
paulson@13957
   120
paulson@14314
   121
  hcomplex_mult_def:
paulson@13957
   122
  "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@14314
   123
		      hcomplexrel `` {%n. X n * Y n})"
paulson@13957
   124
paulson@13957
   125
paulson@13957
   126
paulson@13957
   127
consts
paulson@14314
   128
  "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr 80)
paulson@13957
   129
paulson@13957
   130
defs
paulson@13957
   131
  (* hypernatural powers of nonstandard complex numbers *)
paulson@14314
   132
  hcpow_def:
paulson@14314
   133
  "(z::hcomplex) hcpow (n::hypnat)
paulson@13957
   134
      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
paulson@13957
   135
             hcomplexrel `` {%n. (X n) ^ (Y n)})"
paulson@13957
   136
paulson@14314
   137
paulson@14314
   138
lemma hcomplexrel_refl: "(x,x): hcomplexrel"
paulson@14374
   139
by (simp add: hcomplexrel_def)
paulson@14314
   140
paulson@14314
   141
lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
paulson@14374
   142
by (auto simp add: hcomplexrel_def eq_commute)
paulson@14314
   143
paulson@14314
   144
lemma hcomplexrel_trans:
paulson@14314
   145
      "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
paulson@14374
   146
by (simp add: hcomplexrel_def, ultra)
paulson@14314
   147
paulson@14314
   148
lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
paulson@14374
   149
apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl)
paulson@14374
   150
apply (blast intro: hcomplexrel_sym hcomplexrel_trans)
paulson@14314
   151
done
paulson@14314
   152
paulson@14314
   153
lemmas equiv_hcomplexrel_iff =
paulson@14314
   154
    eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
paulson@14314
   155
paulson@14314
   156
lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
paulson@14374
   157
by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast)
paulson@14314
   158
paulson@14314
   159
lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
paulson@14314
   160
apply (rule inj_on_inverseI)
paulson@14314
   161
apply (erule Abs_hcomplex_inverse)
paulson@14314
   162
done
paulson@14314
   163
paulson@14314
   164
declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp]
paulson@14314
   165
        Abs_hcomplex_inverse [simp]
paulson@14314
   166
paulson@14314
   167
declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
paulson@14314
   168
paulson@14314
   169
paulson@14314
   170
lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
paulson@14314
   171
apply (rule inj_on_inverseI)
paulson@14314
   172
apply (rule Rep_hcomplex_inverse)
paulson@14314
   173
done
paulson@14314
   174
paulson@14374
   175
lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}"
paulson@14374
   176
by (simp add: hcomplexrel_def)
paulson@14314
   177
paulson@14374
   178
lemma hcomplex_empty_not_mem [simp]: "{} \<notin> hcomplex"
paulson@14374
   179
apply (simp add: hcomplex_def hcomplexrel_def)
paulson@14314
   180
apply (auto elim!: quotientE)
paulson@14314
   181
done
paulson@14314
   182
paulson@14374
   183
lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \<noteq> {}"
paulson@14374
   184
by (cut_tac x = x in Rep_hcomplex, auto)
paulson@14314
   185
paulson@14314
   186
lemma eq_Abs_hcomplex:
paulson@14314
   187
    "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
paulson@14314
   188
apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
paulson@14314
   189
apply (drule_tac f = Abs_hcomplex in arg_cong)
paulson@14374
   190
apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
paulson@14314
   191
done
paulson@14314
   192
paulson@14377
   193
lemma hcomplexrel_iff [simp]:
paulson@14374
   194
   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
paulson@14374
   195
by (simp add: hcomplexrel_def)
paulson@14374
   196
paulson@14314
   197
paulson@14314
   198
subsection{*Properties of Nonstandard Real and Imaginary Parts*}
paulson@14314
   199
paulson@14314
   200
lemma hRe:
paulson@14314
   201
     "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
paulson@14314
   202
      Abs_hypreal(hyprel `` {%n. Re(X n)})"
paulson@14374
   203
apply (simp add: hRe_def)
paulson@14374
   204
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14377
   205
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   206
done
paulson@14314
   207
paulson@14314
   208
lemma hIm:
paulson@14314
   209
     "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
paulson@14314
   210
      Abs_hypreal(hyprel `` {%n. Im(X n)})"
paulson@14374
   211
apply (simp add: hIm_def)
paulson@14374
   212
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14377
   213
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   214
done
paulson@14314
   215
paulson@14335
   216
lemma hcomplex_hRe_hIm_cancel_iff:
paulson@14335
   217
     "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
paulson@14374
   218
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   219
apply (rule eq_Abs_hcomplex [of w])
paulson@14377
   220
apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
paulson@14314
   221
apply (ultra+)
paulson@14314
   222
done
paulson@14314
   223
paulson@14377
   224
lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
paulson@14377
   225
by (simp add: hcomplex_hRe_hIm_cancel_iff) 
paulson@14377
   226
paulson@14374
   227
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
paulson@14374
   228
by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
paulson@14314
   229
paulson@14374
   230
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
paulson@14374
   231
by (simp add: hcomplex_zero_def hIm hypreal_zero_num)
paulson@14314
   232
paulson@14374
   233
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
paulson@14374
   234
by (simp add: hcomplex_one_def hRe hypreal_one_num)
paulson@14314
   235
paulson@14374
   236
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
paulson@14374
   237
by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num)
paulson@14314
   238
paulson@14314
   239
paulson@14354
   240
subsection{*Addition for Nonstandard Complex Numbers*}
paulson@14314
   241
paulson@14314
   242
lemma hcomplex_add_congruent2:
paulson@14314
   243
    "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
paulson@14377
   244
by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) 
paulson@14314
   245
paulson@14314
   246
lemma hcomplex_add:
paulson@14377
   247
  "Abs_hcomplex(hcomplexrel``{%n. X n}) + 
paulson@14377
   248
   Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14377
   249
     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
paulson@14374
   250
apply (simp add: hcomplex_add_def)
paulson@14374
   251
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   252
apply (auto simp add: iff: hcomplexrel_iff, ultra) 
paulson@14314
   253
done
paulson@14314
   254
paulson@14314
   255
lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
paulson@14374
   256
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   257
apply (rule eq_Abs_hcomplex [of w])
paulson@14335
   258
apply (simp add: complex_add_commute hcomplex_add)
paulson@14314
   259
done
paulson@14314
   260
paulson@14314
   261
lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
paulson@14374
   262
apply (rule eq_Abs_hcomplex [of z1])
paulson@14374
   263
apply (rule eq_Abs_hcomplex [of z2])
paulson@14374
   264
apply (rule eq_Abs_hcomplex [of z3])
paulson@14335
   265
apply (simp add: hcomplex_add complex_add_assoc)
paulson@14314
   266
done
paulson@14314
   267
paulson@14314
   268
lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
paulson@14374
   269
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   270
apply (simp add: hcomplex_zero_def hcomplex_add)
paulson@14314
   271
done
paulson@14314
   272
paulson@14314
   273
lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
paulson@14374
   274
by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
paulson@14314
   275
paulson@14314
   276
lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
paulson@14374
   277
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   278
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   279
apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
paulson@14314
   280
done
paulson@14314
   281
paulson@14314
   282
lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
paulson@14374
   283
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   284
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   285
apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
paulson@14314
   286
done
paulson@14314
   287
paulson@14354
   288
paulson@14354
   289
subsection{*Additive Inverse on Nonstandard Complex Numbers*}
paulson@14314
   290
paulson@14314
   291
lemma hcomplex_minus_congruent:
paulson@14374
   292
     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
paulson@14374
   293
by (simp add: congruent_def)
paulson@14314
   294
paulson@14314
   295
lemma hcomplex_minus:
paulson@14314
   296
  "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   297
      Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
paulson@14374
   298
apply (simp add: hcomplex_minus_def)
paulson@14374
   299
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   300
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   301
done
paulson@14314
   302
paulson@14314
   303
lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
paulson@14374
   304
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   305
apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
paulson@14314
   306
done
paulson@14335
   307
paulson@14314
   308
paulson@14314
   309
subsection{*Multiplication for Nonstandard Complex Numbers*}
paulson@14314
   310
paulson@14314
   311
lemma hcomplex_mult:
paulson@14374
   312
  "Abs_hcomplex(hcomplexrel``{%n. X n}) *
paulson@14335
   313
     Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14374
   314
     Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
paulson@14374
   315
apply (simp add: hcomplex_mult_def)
paulson@14374
   316
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   317
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   318
done
paulson@14314
   319
paulson@14314
   320
lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
paulson@14374
   321
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   322
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   323
apply (simp add: hcomplex_mult complex_mult_commute)
paulson@14314
   324
done
paulson@14314
   325
paulson@14314
   326
lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
paulson@14374
   327
apply (rule eq_Abs_hcomplex [of u])
paulson@14374
   328
apply (rule eq_Abs_hcomplex [of v])
paulson@14374
   329
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   330
apply (simp add: hcomplex_mult complex_mult_assoc)
paulson@14314
   331
done
paulson@14314
   332
paulson@14314
   333
lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
paulson@14374
   334
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   335
apply (simp add: hcomplex_one_def hcomplex_mult)
paulson@14314
   336
done
paulson@14314
   337
paulson@14314
   338
lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
paulson@14374
   339
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   340
apply (simp add: hcomplex_zero_def hcomplex_mult)
paulson@14314
   341
done
paulson@14314
   342
paulson@14335
   343
lemma hcomplex_add_mult_distrib:
paulson@14335
   344
     "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
paulson@14374
   345
apply (rule eq_Abs_hcomplex [of z1])
paulson@14374
   346
apply (rule eq_Abs_hcomplex [of z2])
paulson@14374
   347
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   348
apply (simp add: hcomplex_mult hcomplex_add left_distrib)
paulson@14314
   349
done
paulson@14314
   350
paulson@14354
   351
lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
paulson@14374
   352
by (simp add: hcomplex_zero_def hcomplex_one_def)
paulson@14374
   353
paulson@14314
   354
declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
paulson@14314
   355
paulson@14314
   356
paulson@14314
   357
subsection{*Inverse of Nonstandard Complex Number*}
paulson@14314
   358
paulson@14314
   359
lemma hcomplex_inverse:
paulson@14314
   360
  "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   361
      Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
paulson@14374
   362
apply (simp add: hcinv_def)
paulson@14374
   363
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   364
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   365
done
paulson@14314
   366
paulson@14314
   367
lemma hcomplex_mult_inv_left:
paulson@14354
   368
      "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
paulson@14374
   369
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   370
apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
paulson@14314
   371
apply (rule ccontr)
paulson@14374
   372
apply (drule left_inverse, auto)
paulson@14314
   373
done
paulson@14314
   374
paulson@14318
   375
subsection {* The Field of Nonstandard Complex Numbers *}
paulson@14318
   376
paulson@14318
   377
instance hcomplex :: field
paulson@14318
   378
proof
paulson@14318
   379
  fix z u v w :: hcomplex
paulson@14318
   380
  show "(u + v) + w = u + (v + w)"
paulson@14318
   381
    by (simp add: hcomplex_add_assoc)
paulson@14318
   382
  show "z + w = w + z"
paulson@14318
   383
    by (simp add: hcomplex_add_commute)
paulson@14318
   384
  show "0 + z = z"
paulson@14335
   385
    by (simp add: hcomplex_add_zero_left)
paulson@14318
   386
  show "-z + z = 0"
paulson@14335
   387
    by (simp add: hcomplex_add_minus_left)
paulson@14318
   388
  show "z - w = z + -w"
paulson@14318
   389
    by (simp add: hcomplex_diff_def)
paulson@14318
   390
  show "(u * v) * w = u * (v * w)"
paulson@14318
   391
    by (simp add: hcomplex_mult_assoc)
paulson@14318
   392
  show "z * w = w * z"
paulson@14318
   393
    by (simp add: hcomplex_mult_commute)
paulson@14318
   394
  show "1 * z = z"
paulson@14335
   395
    by (simp add: hcomplex_mult_one_left)
paulson@14318
   396
  show "0 \<noteq> (1::hcomplex)"
paulson@14318
   397
    by (rule hcomplex_zero_not_eq_one)
paulson@14318
   398
  show "(u + v) * w = u * w + v * w"
paulson@14318
   399
    by (simp add: hcomplex_add_mult_distrib)
paulson@14430
   400
  show "z / w = z * inverse w"
paulson@14318
   401
    by (simp add: hcomplex_divide_def)
paulson@14430
   402
  assume "w \<noteq> 0"
paulson@14430
   403
  thus "inverse w * w = 1"
paulson@14318
   404
    by (rule hcomplex_mult_inv_left)
paulson@14318
   405
qed
paulson@14318
   406
paulson@14318
   407
instance hcomplex :: division_by_zero
paulson@14318
   408
proof
paulson@14430
   409
  show "inverse 0 = (0::hcomplex)"
paulson@14374
   410
    by (simp add: hcomplex_inverse hcomplex_zero_def)
paulson@14318
   411
qed
paulson@14314
   412
paulson@14374
   413
paulson@14318
   414
subsection{*More Minus Laws*}
paulson@14318
   415
paulson@14318
   416
lemma hRe_minus: "hRe(-z) = - hRe(z)"
paulson@14374
   417
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   418
apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
paulson@14318
   419
done
paulson@14318
   420
paulson@14318
   421
lemma hIm_minus: "hIm(-z) = - hIm(z)"
paulson@14374
   422
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   423
apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
paulson@14318
   424
done
paulson@14318
   425
paulson@14318
   426
lemma hcomplex_add_minus_eq_minus:
paulson@14318
   427
      "x + y = (0::hcomplex) ==> x = -y"
paulson@14374
   428
apply (drule Ring_and_Field.equals_zero_I)
paulson@14374
   429
apply (simp add: minus_equation_iff [of x y])
paulson@14318
   430
done
paulson@14318
   431
paulson@14377
   432
lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
paulson@14377
   433
by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
paulson@14377
   434
paulson@14377
   435
lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
paulson@14377
   436
by (simp add: mult_assoc [symmetric])
paulson@14377
   437
paulson@14377
   438
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
paulson@14377
   439
by (simp add: iii_def hcomplex_zero_def)
paulson@14377
   440
paulson@14318
   441
paulson@14318
   442
subsection{*More Multiplication Laws*}
paulson@14318
   443
paulson@14318
   444
lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
paulson@14374
   445
by (rule Ring_and_Field.mult_1_right)
paulson@14318
   446
paulson@14374
   447
lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
paulson@14374
   448
by simp
paulson@14318
   449
paulson@14374
   450
lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z"
paulson@14374
   451
by (subst hcomplex_mult_commute, simp)
paulson@14318
   452
paulson@14335
   453
lemma hcomplex_mult_left_cancel:
paulson@14354
   454
     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
paulson@14374
   455
by (simp add: field_mult_cancel_left)
paulson@14314
   456
paulson@14335
   457
lemma hcomplex_mult_right_cancel:
paulson@14354
   458
     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
paulson@14374
   459
by (simp add: Ring_and_Field.field_mult_cancel_right)
paulson@14314
   460
paulson@14314
   461
paulson@14318
   462
subsection{*Subraction and Division*}
paulson@14314
   463
paulson@14318
   464
lemma hcomplex_diff:
paulson@14318
   465
 "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14318
   466
  Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
paulson@14374
   467
by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def)
paulson@14314
   468
paulson@14374
   469
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
paulson@14374
   470
by (rule Ring_and_Field.diff_eq_eq)
paulson@14314
   471
paulson@14314
   472
lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
paulson@14374
   473
by (rule Ring_and_Field.add_divide_distrib)
paulson@14314
   474
paulson@14314
   475
paulson@14314
   476
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
paulson@14314
   477
paulson@14314
   478
lemma hcomplex_of_hypreal:
paulson@14314
   479
  "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
paulson@14314
   480
      Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
paulson@14374
   481
apply (simp add: hcomplex_of_hypreal_def)
paulson@14377
   482
apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
paulson@14314
   483
done
paulson@14314
   484
paulson@14374
   485
lemma hcomplex_of_hypreal_cancel_iff [iff]:
paulson@14374
   486
     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
paulson@14374
   487
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   488
apply (rule eq_Abs_hypreal [of y])
paulson@14374
   489
apply (simp add: hcomplex_of_hypreal)
paulson@14314
   490
done
paulson@14314
   491
paulson@14335
   492
lemma hcomplex_of_hypreal_minus:
paulson@14335
   493
     "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
paulson@14374
   494
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   495
apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
paulson@14314
   496
done
paulson@14314
   497
paulson@14335
   498
lemma hcomplex_of_hypreal_inverse:
paulson@14335
   499
     "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
paulson@14374
   500
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   501
apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
paulson@14314
   502
done
paulson@14314
   503
paulson@14335
   504
lemma hcomplex_of_hypreal_add:
paulson@14335
   505
     "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
paulson@14314
   506
      hcomplex_of_hypreal (x + y)"
paulson@14374
   507
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   508
apply (rule eq_Abs_hypreal [of y])
paulson@14374
   509
apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
paulson@14314
   510
done
paulson@14314
   511
paulson@14314
   512
lemma hcomplex_of_hypreal_diff:
paulson@14314
   513
     "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
paulson@14314
   514
      hcomplex_of_hypreal (x - y)"
paulson@14374
   515
by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
paulson@14314
   516
paulson@14335
   517
lemma hcomplex_of_hypreal_mult:
paulson@14335
   518
     "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
paulson@14314
   519
      hcomplex_of_hypreal (x * y)"
paulson@14374
   520
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   521
apply (rule eq_Abs_hypreal [of y])
paulson@14374
   522
apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
paulson@14314
   523
done
paulson@14314
   524
paulson@14314
   525
lemma hcomplex_of_hypreal_divide:
paulson@14314
   526
  "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
paulson@14374
   527
apply (simp add: hcomplex_divide_def)
paulson@14374
   528
apply (case_tac "y=0", simp)
paulson@14314
   529
apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
paulson@14374
   530
apply (simp add: hypreal_divide_def)
paulson@14314
   531
done
paulson@14314
   532
paulson@14374
   533
lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
paulson@14374
   534
by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
paulson@14314
   535
paulson@14374
   536
lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
paulson@14374
   537
by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
paulson@14374
   538
paulson@14374
   539
lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
paulson@14374
   540
apply (rule eq_Abs_hypreal [of z])
paulson@14314
   541
apply (auto simp add: hcomplex_of_hypreal hRe)
paulson@14314
   542
done
paulson@14314
   543
paulson@14374
   544
lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
paulson@14374
   545
apply (rule eq_Abs_hypreal [of z])
paulson@14314
   546
apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
paulson@14314
   547
done
paulson@14314
   548
paulson@14374
   549
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
paulson@14374
   550
     "hcomplex_of_hypreal epsilon \<noteq> 0"
paulson@14374
   551
by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
paulson@14314
   552
paulson@14318
   553
paulson@14377
   554
subsection{*HComplex theorems*}
paulson@14377
   555
paulson@14377
   556
lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
paulson@14377
   557
apply (rule eq_Abs_hypreal [of x])
paulson@14377
   558
apply (rule eq_Abs_hypreal [of y])
paulson@14377
   559
apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
paulson@14377
   560
done
paulson@14377
   561
paulson@14377
   562
lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
paulson@14377
   563
apply (rule eq_Abs_hypreal [of x])
paulson@14377
   564
apply (rule eq_Abs_hypreal [of y])
paulson@14377
   565
apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
paulson@14377
   566
done
paulson@14377
   567
paulson@14377
   568
text{*Relates the two nonstandard constructions*}
paulson@14377
   569
lemma HComplex_eq_Abs_hcomplex_Complex:
paulson@14377
   570
     "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
paulson@14377
   571
      Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
paulson@14377
   572
by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) 
paulson@14377
   573
paulson@14377
   574
lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
paulson@14377
   575
by (simp add: hcomplex_equality) 
paulson@14377
   576
paulson@14377
   577
lemma hcomplex_induct [case_names rect, induct type: hcomplex]:
paulson@14377
   578
     "(\<And>x y. P (HComplex x y)) ==> P z"
paulson@14377
   579
by (rule hcomplex_surj [THEN subst], blast)
paulson@14377
   580
paulson@14377
   581
paulson@14318
   582
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
paulson@14314
   583
paulson@14314
   584
lemma hcmod:
paulson@14314
   585
  "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   586
      Abs_hypreal(hyprel `` {%n. cmod (X n)})"
paulson@14314
   587
paulson@14374
   588
apply (simp add: hcmod_def)
paulson@14374
   589
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14377
   590
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   591
done
paulson@14314
   592
paulson@14374
   593
lemma hcmod_zero [simp]: "hcmod(0) = 0"
paulson@14377
   594
by (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
paulson@14314
   595
paulson@14374
   596
lemma hcmod_one [simp]: "hcmod(1) = 1"
paulson@14374
   597
by (simp add: hcomplex_one_def hcmod hypreal_one_num)
paulson@14314
   598
paulson@14374
   599
lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
paulson@14374
   600
apply (rule eq_Abs_hypreal [of x])
paulson@14314
   601
apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
paulson@14314
   602
done
paulson@14314
   603
paulson@14335
   604
lemma hcomplex_of_hypreal_abs:
paulson@14335
   605
     "hcomplex_of_hypreal (abs x) =
paulson@14314
   606
      hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
paulson@14374
   607
by simp
paulson@14314
   608
paulson@14377
   609
lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')"
paulson@14377
   610
apply (rule iffI) 
paulson@14377
   611
 prefer 2 apply simp 
paulson@14377
   612
apply (simp add: HComplex_def iii_def) 
paulson@14377
   613
apply (rule eq_Abs_hypreal [of x])
paulson@14377
   614
apply (rule eq_Abs_hypreal [of y])
paulson@14377
   615
apply (rule eq_Abs_hypreal [of x'])
paulson@14377
   616
apply (rule eq_Abs_hypreal [of y'])
paulson@14377
   617
apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
paulson@14377
   618
apply (ultra+) 
paulson@14377
   619
done
paulson@14377
   620
paulson@14377
   621
lemma HComplex_add [simp]:
paulson@14377
   622
     "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
paulson@14377
   623
by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib) 
paulson@14377
   624
paulson@14377
   625
lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
paulson@14377
   626
by (simp add: HComplex_def hcomplex_of_hypreal_minus) 
paulson@14377
   627
paulson@14377
   628
lemma HComplex_diff [simp]:
paulson@14377
   629
     "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
paulson@14377
   630
by (simp add: diff_minus)
paulson@14377
   631
paulson@14377
   632
lemma HComplex_mult [simp]:
paulson@14377
   633
  "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
paulson@14377
   634
by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus 
paulson@14377
   635
       hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
paulson@14377
   636
       add_ac mult_ac right_distrib)
paulson@14377
   637
paulson@14377
   638
(*HComplex_inverse is proved below*)
paulson@14377
   639
paulson@14377
   640
lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0"
paulson@14377
   641
by (simp add: HComplex_def)
paulson@14377
   642
paulson@14377
   643
lemma HComplex_add_hcomplex_of_hypreal [simp]:
paulson@14377
   644
     "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
paulson@14377
   645
by (simp add: hcomplex_of_hypreal_eq)
paulson@14377
   646
paulson@14377
   647
lemma hcomplex_of_hypreal_add_HComplex [simp]:
paulson@14377
   648
     "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
paulson@14377
   649
by (simp add: i_def hcomplex_of_hypreal_eq)
paulson@14377
   650
paulson@14377
   651
lemma HComplex_mult_hcomplex_of_hypreal:
paulson@14377
   652
     "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
paulson@14377
   653
by (simp add: hcomplex_of_hypreal_eq)
paulson@14377
   654
paulson@14377
   655
lemma hcomplex_of_hypreal_mult_HComplex:
paulson@14377
   656
     "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
paulson@14377
   657
by (simp add: i_def hcomplex_of_hypreal_eq)
paulson@14377
   658
paulson@14377
   659
lemma i_hcomplex_of_hypreal [simp]:
paulson@14377
   660
     "iii * hcomplex_of_hypreal r = HComplex 0 r"
paulson@14377
   661
by (simp add: HComplex_def)
paulson@14377
   662
paulson@14377
   663
lemma hcomplex_of_hypreal_i [simp]:
paulson@14377
   664
     "hcomplex_of_hypreal r * iii = HComplex 0 r"
paulson@14377
   665
by (simp add: mult_commute) 
paulson@14377
   666
paulson@14314
   667
paulson@14314
   668
subsection{*Conjugation*}
paulson@14314
   669
paulson@14314
   670
lemma hcnj:
paulson@14314
   671
  "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14318
   672
   Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
paulson@14374
   673
apply (simp add: hcnj_def)
paulson@14374
   674
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   675
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   676
done
paulson@14314
   677
paulson@14374
   678
lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
paulson@14374
   679
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   680
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   681
apply (simp add: hcnj)
paulson@14374
   682
done
paulson@14374
   683
paulson@14374
   684
lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
paulson@14374
   685
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   686
apply (simp add: hcnj)
paulson@14314
   687
done
paulson@14314
   688
paulson@14374
   689
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
paulson@14374
   690
     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
paulson@14374
   691
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   692
apply (simp add: hcnj hcomplex_of_hypreal)
paulson@14314
   693
done
paulson@14314
   694
paulson@14374
   695
lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
paulson@14374
   696
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   697
apply (simp add: hcnj hcmod)
paulson@14314
   698
done
paulson@14314
   699
paulson@14314
   700
lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
paulson@14374
   701
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   702
apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
paulson@14314
   703
done
paulson@14314
   704
paulson@14314
   705
lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
paulson@14374
   706
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   707
apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
paulson@14314
   708
done
paulson@14314
   709
paulson@14314
   710
lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
paulson@14374
   711
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   712
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   713
apply (simp add: hcnj hcomplex_add complex_cnj_add)
paulson@14314
   714
done
paulson@14314
   715
paulson@14314
   716
lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
paulson@14374
   717
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   718
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   719
apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
paulson@14314
   720
done
paulson@14314
   721
paulson@14314
   722
lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
paulson@14374
   723
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   724
apply (rule eq_Abs_hcomplex [of w])
paulson@14374
   725
apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
paulson@14314
   726
done
paulson@14314
   727
paulson@14314
   728
lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
paulson@14374
   729
by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse)
paulson@14314
   730
paulson@14374
   731
lemma hcnj_one [simp]: "hcnj 1 = 1"
paulson@14374
   732
by (simp add: hcomplex_one_def hcnj)
paulson@14314
   733
paulson@14374
   734
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
paulson@14374
   735
by (simp add: hcomplex_zero_def hcnj)
paulson@14374
   736
paulson@14374
   737
lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
paulson@14374
   738
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   739
apply (simp add: hcomplex_zero_def hcnj)
paulson@14314
   740
done
paulson@14314
   741
paulson@14335
   742
lemma hcomplex_mult_hcnj:
paulson@14335
   743
     "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
paulson@14374
   744
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   745
apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
paulson@14374
   746
                      hypreal_mult complex_mult_cnj numeral_2_eq_2)
paulson@14314
   747
done
paulson@14314
   748
paulson@14314
   749
paulson@14354
   750
subsection{*More Theorems about the Function @{term hcmod}*}
paulson@14314
   751
paulson@14374
   752
lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
paulson@14374
   753
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   754
apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
paulson@14314
   755
done
paulson@14314
   756
paulson@14374
   757
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
paulson@14335
   758
     "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
paulson@14374
   759
apply (simp add: abs_if linorder_not_less)
paulson@14314
   760
done
paulson@14314
   761
paulson@14374
   762
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
paulson@14335
   763
     "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
paulson@14374
   764
apply (simp add: abs_if linorder_not_less)
paulson@14314
   765
done
paulson@14314
   766
paulson@14374
   767
lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
paulson@14374
   768
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   769
apply (simp add: hcmod hcomplex_minus)
paulson@14314
   770
done
paulson@14314
   771
paulson@14314
   772
lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
paulson@14374
   773
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   774
apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
paulson@14314
   775
done
paulson@14314
   776
paulson@14374
   777
lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
paulson@14374
   778
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   779
apply (simp add: hcmod hypreal_zero_num hypreal_le)
paulson@14314
   780
done
paulson@14314
   781
paulson@14374
   782
lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
paulson@14374
   783
by (simp add: abs_if linorder_not_less)
paulson@14314
   784
paulson@14314
   785
lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
paulson@14374
   786
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   787
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   788
apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
paulson@14314
   789
done
paulson@14314
   790
paulson@14314
   791
lemma hcmod_add_squared_eq:
paulson@14314
   792
     "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
paulson@14374
   793
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   794
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   795
apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
paulson@14374
   796
                      numeral_2_eq_2 realpow_two [symmetric]
paulson@14374
   797
                  del: realpow_Suc)
paulson@14374
   798
apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
paulson@14374
   799
                 hypreal_add [symmetric] hypreal_mult [symmetric]
paulson@14314
   800
                 hypreal_of_real_def [symmetric])
paulson@14314
   801
done
paulson@14314
   802
paulson@14374
   803
lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
paulson@14374
   804
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   805
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   806
apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
paulson@14314
   807
done
paulson@14314
   808
paulson@14374
   809
lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \<le> hcmod(x * y)"
paulson@14374
   810
apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod)
paulson@14314
   811
apply (simp add: hcmod_mult)
paulson@14314
   812
done
paulson@14314
   813
paulson@14374
   814
lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
paulson@14374
   815
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   816
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   817
apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
paulson@14323
   818
                      hypreal_le realpow_two [symmetric] numeral_2_eq_2
paulson@14374
   819
            del: realpow_Suc)
paulson@14374
   820
apply (simp add: numeral_2_eq_2 [symmetric])
paulson@14314
   821
done
paulson@14314
   822
paulson@14374
   823
lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
paulson@14374
   824
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   825
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   826
apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
paulson@14314
   827
done
paulson@14314
   828
paulson@14374
   829
lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \<le> hcmod a"
paulson@14374
   830
apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
paulson@14331
   831
apply (simp add: add_ac)
paulson@14314
   832
done
paulson@14314
   833
paulson@14314
   834
lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
paulson@14374
   835
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   836
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   837
apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
paulson@14314
   838
done
paulson@14314
   839
paulson@14335
   840
lemma hcmod_add_less:
paulson@14335
   841
     "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
paulson@14374
   842
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   843
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   844
apply (rule eq_Abs_hypreal [of r])
paulson@14374
   845
apply (rule eq_Abs_hypreal [of s])
paulson@14374
   846
apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
paulson@14314
   847
apply (auto intro: complex_mod_add_less)
paulson@14314
   848
done
paulson@14314
   849
paulson@14335
   850
lemma hcmod_mult_less:
paulson@14335
   851
     "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
paulson@14374
   852
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   853
apply (rule eq_Abs_hcomplex [of y])
paulson@14374
   854
apply (rule eq_Abs_hypreal [of r])
paulson@14374
   855
apply (rule eq_Abs_hypreal [of s])
paulson@14374
   856
apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
paulson@14314
   857
apply (auto intro: complex_mod_mult_less)
paulson@14314
   858
done
paulson@14314
   859
paulson@14374
   860
lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
paulson@14374
   861
apply (rule eq_Abs_hcomplex [of a])
paulson@14374
   862
apply (rule eq_Abs_hcomplex [of b])
paulson@14374
   863
apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
paulson@14314
   864
done
paulson@14314
   865
paulson@14314
   866
paulson@14314
   867
subsection{*A Few Nonlinear Theorems*}
paulson@14314
   868
paulson@14314
   869
lemma hcpow:
paulson@14314
   870
  "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
paulson@14314
   871
   Abs_hypnat(hypnatrel``{%n. Y n}) =
paulson@14314
   872
   Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
paulson@14374
   873
apply (simp add: hcpow_def)
paulson@14374
   874
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   875
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   876
done
paulson@14314
   877
paulson@14335
   878
lemma hcomplex_of_hypreal_hyperpow:
paulson@14335
   879
     "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
paulson@14374
   880
apply (rule eq_Abs_hypreal [of x])
paulson@14374
   881
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   882
apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
paulson@14314
   883
done
paulson@14314
   884
paulson@14314
   885
lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
paulson@14374
   886
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   887
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   888
apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
paulson@14314
   889
done
paulson@14314
   890
paulson@14314
   891
lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
paulson@14374
   892
apply (case_tac "x = 0", simp)
paulson@14314
   893
apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
paulson@14314
   894
apply (auto simp add: hcmod_mult [symmetric])
paulson@14314
   895
done
paulson@14314
   896
paulson@14374
   897
lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
paulson@14374
   898
by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse)
paulson@14314
   899
paulson@14354
   900
paulson@14354
   901
subsection{*Exponentiation*}
paulson@14354
   902
paulson@14354
   903
primrec
paulson@14354
   904
     hcomplexpow_0:   "z ^ 0       = 1"
paulson@14354
   905
     hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
paulson@14354
   906
paulson@14354
   907
instance hcomplex :: ringpower
paulson@14354
   908
proof
paulson@14354
   909
  fix z :: hcomplex
paulson@14354
   910
  fix n :: nat
paulson@14354
   911
  show "z^0 = 1" by simp
paulson@14354
   912
  show "z^(Suc n) = z * (z^n)" by simp
paulson@14354
   913
qed
paulson@14354
   914
paulson@14377
   915
lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
paulson@14377
   916
by (simp add: power2_eq_square)
paulson@14377
   917
paulson@14354
   918
paulson@14354
   919
lemma hcomplex_of_hypreal_pow:
paulson@14354
   920
     "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
paulson@14354
   921
apply (induct_tac "n")
paulson@14354
   922
apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
paulson@14354
   923
done
paulson@14354
   924
paulson@14354
   925
lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
paulson@14314
   926
apply (induct_tac "n")
paulson@14354
   927
apply (auto simp add: hcomplex_hcnj_mult)
paulson@14354
   928
done
paulson@14354
   929
paulson@14354
   930
lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
paulson@14354
   931
apply (induct_tac "n")
paulson@14354
   932
apply (auto simp add: hcmod_mult)
paulson@14354
   933
done
paulson@14354
   934
paulson@14354
   935
lemma hcpow_minus:
paulson@14354
   936
     "(-x::hcomplex) hcpow n =
paulson@14354
   937
      (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
paulson@14374
   938
apply (rule eq_Abs_hcomplex [of x])
paulson@14374
   939
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   940
apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
paulson@14443
   941
apply (auto simp add: neg_power_if, ultra)
paulson@14314
   942
done
paulson@14314
   943
paulson@14314
   944
lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
paulson@14374
   945
apply (rule eq_Abs_hcomplex [of r])
paulson@14374
   946
apply (rule eq_Abs_hcomplex [of s])
paulson@14374
   947
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   948
apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
paulson@14314
   949
done
paulson@14314
   950
paulson@14354
   951
lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
paulson@14374
   952
apply (simp add: hcomplex_zero_def hypnat_one_def)
paulson@14374
   953
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   954
apply (simp add: hcpow hypnat_add)
paulson@14314
   955
done
paulson@14314
   956
paulson@14354
   957
lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
paulson@14374
   958
by (simp add: hSuc_def)
paulson@14314
   959
paulson@14354
   960
lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
paulson@14374
   961
apply (rule eq_Abs_hcomplex [of r])
paulson@14374
   962
apply (rule eq_Abs_hypnat [of n])
paulson@14374
   963
apply (auto simp add: hcpow hcomplex_zero_def, ultra)
paulson@14314
   964
done
paulson@14314
   965
paulson@14314
   966
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
paulson@14374
   967
by (blast intro: ccontr dest: hcpow_not_zero)
paulson@14314
   968
paulson@14314
   969
lemma hcomplex_divide:
paulson@14314
   970
  "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14314
   971
   Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
paulson@14374
   972
by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult)
paulson@14374
   973
paulson@14314
   974
paulson@14314
   975
paulson@14377
   976
paulson@14314
   977
subsection{*The Function @{term hsgn}*}
paulson@14314
   978
paulson@14314
   979
lemma hsgn:
paulson@14314
   980
  "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   981
      Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
paulson@14374
   982
apply (simp add: hsgn_def)
paulson@14374
   983
apply (rule_tac f = Abs_hcomplex in arg_cong)
paulson@14377
   984
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
   985
done
paulson@14314
   986
paulson@14374
   987
lemma hsgn_zero [simp]: "hsgn 0 = 0"
paulson@14374
   988
by (simp add: hcomplex_zero_def hsgn)
paulson@14314
   989
paulson@14374
   990
lemma hsgn_one [simp]: "hsgn 1 = 1"
paulson@14374
   991
by (simp add: hcomplex_one_def hsgn)
paulson@14314
   992
paulson@14314
   993
lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
paulson@14374
   994
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
   995
apply (simp add: hsgn hcomplex_minus sgn_minus)
paulson@14314
   996
done
paulson@14314
   997
paulson@14314
   998
lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
paulson@14374
   999
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
  1000
apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
paulson@14314
  1001
done
paulson@14314
  1002
paulson@14314
  1003
paulson@14377
  1004
lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
paulson@14374
  1005
apply (rule eq_Abs_hypreal [of x])
paulson@14377
  1006
apply (rule eq_Abs_hypreal [of y]) 
paulson@14377
  1007
apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
paulson@14377
  1008
                 hypreal_mult hypreal_add hcmod numeral_2_eq_2)
paulson@14314
  1009
done
paulson@14314
  1010
paulson@14377
  1011
lemma hcomplex_eq_cancel_iff1 [simp]:
paulson@14377
  1012
     "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
paulson@14377
  1013
by (simp add: hcomplex_of_hypreal_eq)
paulson@14314
  1014
paulson@14374
  1015
lemma hcomplex_eq_cancel_iff2 [simp]:
paulson@14377
  1016
     "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
paulson@14377
  1017
by (simp add: hcomplex_of_hypreal_eq)
paulson@14314
  1018
paulson@14377
  1019
lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
paulson@14377
  1020
by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
paulson@14314
  1021
paulson@14377
  1022
lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
paulson@14377
  1023
by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
paulson@14314
  1024
paulson@14377
  1025
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
paulson@14377
  1026
by (insert hcomplex_of_hypreal_i [of 1], simp)
paulson@14314
  1027
paulson@14377
  1028
lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
paulson@14377
  1029
by (simp add: i_eq_HComplex_0_1) 
paulson@14314
  1030
paulson@14374
  1031
lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
paulson@14374
  1032
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
  1033
apply (simp add: hsgn hcmod hRe hypreal_divide)
paulson@14314
  1034
done
paulson@14314
  1035
paulson@14374
  1036
lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
paulson@14374
  1037
apply (rule eq_Abs_hcomplex [of z])
paulson@14374
  1038
apply (simp add: hsgn hcmod hIm hypreal_divide)
paulson@14314
  1039
done
paulson@14314
  1040
paulson@14374
  1041
lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
paulson@14377
  1042
by (auto intro: real_sum_squares_cancel)
paulson@14314
  1043
paulson@14335
  1044
lemma hcomplex_inverse_complex_split:
paulson@14335
  1045
     "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
paulson@14314
  1046
      hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
paulson@14314
  1047
      iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
paulson@14374
  1048
apply (rule eq_Abs_hypreal [of x])
paulson@14374
  1049
apply (rule eq_Abs_hypreal [of y])
paulson@14374
  1050
apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
paulson@14377
  1051
apply (simp add: diff_minus) 
paulson@14374
  1052
done
paulson@14374
  1053
paulson@14377
  1054
lemma HComplex_inverse:
paulson@14377
  1055
     "inverse (HComplex x y) =
paulson@14377
  1056
      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
paulson@14377
  1057
by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
paulson@14377
  1058
paulson@14377
  1059
paulson@14377
  1060
paulson@14374
  1061
lemma hRe_mult_i_eq[simp]:
paulson@14374
  1062
    "hRe (iii * hcomplex_of_hypreal y) = 0"
paulson@14374
  1063
apply (simp add: iii_def)
paulson@14374
  1064
apply (rule eq_Abs_hypreal [of y])
paulson@14374
  1065
apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
paulson@14314
  1066
done
paulson@14314
  1067
paulson@14374
  1068
lemma hIm_mult_i_eq [simp]:
paulson@14314
  1069
    "hIm (iii * hcomplex_of_hypreal y) = y"
paulson@14374
  1070
apply (simp add: iii_def)
paulson@14374
  1071
apply (rule eq_Abs_hypreal [of y])
paulson@14374
  1072
apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
paulson@14314
  1073
done
paulson@14314
  1074
paulson@14374
  1075
lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
paulson@14374
  1076
apply (rule eq_Abs_hypreal [of y])
paulson@14374
  1077
apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
paulson@14314
  1078
done
paulson@14314
  1079
paulson@14374
  1080
lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
paulson@14377
  1081
by (simp only: hcmod_mult_i hcomplex_mult_commute)
paulson@14314
  1082
paulson@14314
  1083
(*---------------------------------------------------------------------------*)
paulson@14314
  1084
(*  harg                                                                     *)
paulson@14314
  1085
(*---------------------------------------------------------------------------*)
paulson@14314
  1086
paulson@14314
  1087
lemma harg:
paulson@14314
  1088
  "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
  1089
      Abs_hypreal(hyprel `` {%n. arg (X n)})"
paulson@14374
  1090
apply (simp add: harg_def)
paulson@14374
  1091
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14377
  1092
apply (auto iff: hcomplexrel_iff, ultra)
paulson@14314
  1093
done
paulson@14314
  1094
paulson@14354
  1095
lemma cos_harg_i_mult_zero_pos:
paulson@14377
  1096
     "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
paulson@14374
  1097
apply (rule eq_Abs_hypreal [of y])
paulson@14377
  1098
apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
paulson@14377
  1099
                hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
paulson@14314
  1100
done
paulson@14314
  1101
paulson@14354
  1102
lemma cos_harg_i_mult_zero_neg:
paulson@14377
  1103
     "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
paulson@14374
  1104
apply (rule eq_Abs_hypreal [of y])
paulson@14377
  1105
apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
paulson@14377
  1106
                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
paulson@14314
  1107
done
paulson@14314
  1108
paulson@14354
  1109
lemma cos_harg_i_mult_zero [simp]:
paulson@14377
  1110
     "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
paulson@14377
  1111
by (auto simp add: linorder_neq_iff
paulson@14377
  1112
                   cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
paulson@14354
  1113
paulson@14354
  1114
lemma hcomplex_of_hypreal_zero_iff [simp]:
paulson@14354
  1115
     "(hcomplex_of_hypreal y = 0) = (y = 0)"
paulson@14374
  1116
apply (rule eq_Abs_hypreal [of y])
paulson@14374
  1117
apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
paulson@14314
  1118
done
paulson@14314
  1119
paulson@14314
  1120
paulson@14354
  1121
subsection{*Polar Form for Nonstandard Complex Numbers*}
paulson@14314
  1122
paulson@14335
  1123
lemma complex_split_polar2:
paulson@14377
  1124
     "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
paulson@14377
  1125
by (blast intro: complex_split_polar)
paulson@14377
  1126
paulson@14377
  1127
lemma lemma_hypreal_P_EX2:
paulson@14377
  1128
     "(\<exists>(x::hypreal) y. P x y) =
paulson@14377
  1129
      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
paulson@14377
  1130
apply auto
paulson@14377
  1131
apply (rule_tac z = x in eq_Abs_hypreal)
paulson@14377
  1132
apply (rule_tac z = y in eq_Abs_hypreal, auto)
paulson@14314
  1133
done
paulson@14314
  1134
paulson@14314
  1135
lemma hcomplex_split_polar:
paulson@14377
  1136
  "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
paulson@14374
  1137
apply (rule eq_Abs_hcomplex [of z])
paulson@14377
  1138
apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
paulson@14374
  1139
apply (cut_tac z = x in complex_split_polar2)
paulson@14335
  1140
apply (drule choice, safe)+
paulson@14374
  1141
apply (rule_tac x = f in exI)
paulson@14374
  1142
apply (rule_tac x = fa in exI, auto)
paulson@14314
  1143
done
paulson@14314
  1144
paulson@14314
  1145
lemma hcis:
paulson@14314
  1146
  "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
paulson@14314
  1147
      Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
paulson@14374
  1148
apply (simp add: hcis_def)
paulson@14377
  1149
apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
paulson@14314
  1150
done
paulson@14314
  1151
paulson@14314
  1152
lemma hcis_eq:
paulson@14314
  1153
   "hcis a =
paulson@14314
  1154
    (hcomplex_of_hypreal(( *f* cos) a) +
paulson@14314
  1155
    iii * hcomplex_of_hypreal(( *f* sin) a))"
paulson@14374
  1156
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1157
apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
paulson@14314
  1158
done
paulson@14314
  1159
paulson@14314
  1160
lemma hrcis:
paulson@14314
  1161
  "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
paulson@14314
  1162
      Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
paulson@14374
  1163
by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
paulson@14314
  1164
paulson@14354
  1165
lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
paulson@14377
  1166
apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
paulson@14314
  1167
apply (rule hcomplex_split_polar)
paulson@14314
  1168
done
paulson@14314
  1169
paulson@14374
  1170
lemma hRe_hcomplex_polar [simp]:
paulson@14377
  1171
     "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
paulson@14377
  1172
      r * ( *f* cos) a"
paulson@14377
  1173
by (simp add: hcomplex_of_hypreal_mult_HComplex)
paulson@14314
  1174
paulson@14374
  1175
lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
paulson@14374
  1176
by (simp add: hrcis_def hcis_eq)
paulson@14314
  1177
paulson@14374
  1178
lemma hIm_hcomplex_polar [simp]:
paulson@14377
  1179
     "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
paulson@14377
  1180
      r * ( *f* sin) a"
paulson@14377
  1181
by (simp add: hcomplex_of_hypreal_mult_HComplex)
paulson@14314
  1182
paulson@14374
  1183
lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
paulson@14374
  1184
by (simp add: hrcis_def hcis_eq)
paulson@14314
  1185
paulson@14377
  1186
paulson@14377
  1187
lemma hcmod_unit_one [simp]:
paulson@14377
  1188
     "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
paulson@14377
  1189
apply (rule eq_Abs_hypreal [of a]) 
paulson@14377
  1190
apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
paulson@14377
  1191
                 hcomplex_mult hcmod hcomplex_add hypreal_one_def)
paulson@14377
  1192
done
paulson@14377
  1193
paulson@14374
  1194
lemma hcmod_complex_polar [simp]:
paulson@14377
  1195
     "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
paulson@14377
  1196
      abs r"
paulson@14377
  1197
apply (simp only: hcmod_mult hcmod_unit_one, simp)  
paulson@14314
  1198
done
paulson@14314
  1199
paulson@14374
  1200
lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
paulson@14374
  1201
by (simp add: hrcis_def hcis_eq)
paulson@14314
  1202
paulson@14314
  1203
(*---------------------------------------------------------------------------*)
paulson@14314
  1204
(*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
paulson@14314
  1205
(*---------------------------------------------------------------------------*)
paulson@14314
  1206
paulson@14314
  1207
lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
paulson@14374
  1208
by (simp add: hrcis_def)
paulson@14314
  1209
declare hcis_hrcis_eq [symmetric, simp]
paulson@14314
  1210
paulson@14314
  1211
lemma hrcis_mult:
paulson@14314
  1212
  "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
paulson@14374
  1213
apply (simp add: hrcis_def)
paulson@14374
  1214
apply (rule eq_Abs_hypreal [of r1])
paulson@14374
  1215
apply (rule eq_Abs_hypreal [of r2])
paulson@14374
  1216
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1217
apply (rule eq_Abs_hypreal [of b])
paulson@14374
  1218
apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
paulson@14374
  1219
                      hcomplex_mult cis_mult [symmetric]
paulson@14314
  1220
                      complex_of_real_mult [symmetric])
paulson@14314
  1221
done
paulson@14314
  1222
paulson@14314
  1223
lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
paulson@14374
  1224
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1225
apply (rule eq_Abs_hypreal [of b])
paulson@14374
  1226
apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
paulson@14314
  1227
done
paulson@14314
  1228
paulson@14374
  1229
lemma hcis_zero [simp]: "hcis 0 = 1"
paulson@14374
  1230
by (simp add: hcomplex_one_def hcis hypreal_zero_num)
paulson@14314
  1231
paulson@14374
  1232
lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
paulson@14374
  1233
apply (simp add: hcomplex_zero_def)
paulson@14374
  1234
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1235
apply (simp add: hrcis hypreal_zero_num)
paulson@14314
  1236
done
paulson@14314
  1237
paulson@14374
  1238
lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
paulson@14374
  1239
apply (rule eq_Abs_hypreal [of r])
paulson@14374
  1240
apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
paulson@14314
  1241
done
paulson@14314
  1242
paulson@14374
  1243
lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
paulson@14374
  1244
by (simp add: hcomplex_mult_assoc [symmetric])
paulson@14314
  1245
paulson@14374
  1246
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
paulson@14374
  1247
by simp
paulson@14314
  1248
paulson@14314
  1249
lemma hcis_hypreal_of_nat_Suc_mult:
paulson@14314
  1250
   "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
paulson@14374
  1251
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1252
apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
paulson@14314
  1253
done
paulson@14314
  1254
paulson@14314
  1255
lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
paulson@14314
  1256
apply (induct_tac "n")
paulson@14374
  1257
apply (simp_all add: hcis_hypreal_of_nat_Suc_mult)
paulson@14314
  1258
done
paulson@14314
  1259
paulson@14335
  1260
lemma hcis_hypreal_of_hypnat_Suc_mult:
paulson@14335
  1261
     "hcis (hypreal_of_hypnat (n + 1) * a) =
paulson@14314
  1262
      hcis a * hcis (hypreal_of_hypnat n * a)"
paulson@14374
  1263
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1264
apply (rule eq_Abs_hypnat [of n])
paulson@14374
  1265
apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
paulson@14314
  1266
done
paulson@14314
  1267
paulson@14314
  1268
lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
paulson@14374
  1269
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1270
apply (rule eq_Abs_hypnat [of n])
paulson@14374
  1271
apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
paulson@14314
  1272
done
paulson@14314
  1273
paulson@14314
  1274
lemma DeMoivre2:
paulson@14314
  1275
  "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
paulson@14374
  1276
apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
paulson@14314
  1277
done
paulson@14314
  1278
paulson@14314
  1279
lemma DeMoivre2_ext:
paulson@14314
  1280
  "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
paulson@14374
  1281
apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
paulson@14374
  1282
done
paulson@14374
  1283
paulson@14374
  1284
lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
paulson@14374
  1285
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1286
apply (simp add: hcomplex_inverse hcis hypreal_minus)
paulson@14314
  1287
done
paulson@14314
  1288
paulson@14374
  1289
lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
paulson@14374
  1290
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1291
apply (rule eq_Abs_hypreal [of r])
paulson@14374
  1292
apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
paulson@14374
  1293
apply (simp add: real_divide_def)
paulson@14314
  1294
done
paulson@14314
  1295
paulson@14374
  1296
lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
paulson@14374
  1297
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1298
apply (simp add: hcis starfun hRe)
paulson@14314
  1299
done
paulson@14314
  1300
paulson@14374
  1301
lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
paulson@14374
  1302
apply (rule eq_Abs_hypreal [of a])
paulson@14374
  1303
apply (simp add: hcis starfun hIm)
paulson@14314
  1304
done
paulson@14314
  1305
paulson@14374
  1306
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
paulson@14377
  1307
by (simp add: NSDeMoivre)
paulson@14314
  1308
paulson@14374
  1309
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
paulson@14377
  1310
by (simp add: NSDeMoivre)
paulson@14314
  1311
paulson@14374
  1312
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
paulson@14377
  1313
by (simp add: NSDeMoivre_ext)
paulson@14314
  1314
paulson@14374
  1315
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
paulson@14377
  1316
by (simp add: NSDeMoivre_ext)
paulson@14314
  1317
paulson@14314
  1318
lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
paulson@14374
  1319
apply (simp add: hexpi_def)
paulson@14374
  1320
apply (rule eq_Abs_hcomplex [of a])
paulson@14374
  1321
apply (rule eq_Abs_hcomplex [of b])
paulson@14374
  1322
apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
paulson@14314
  1323
done
paulson@14314
  1324
paulson@14314
  1325
paulson@14374
  1326
subsection{*@{term hcomplex_of_complex}: the Injection from
paulson@14354
  1327
  type @{typ complex} to to @{typ hcomplex}*}
paulson@14354
  1328
paulson@14354
  1329
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
paulson@14374
  1330
apply (rule inj_onI, rule ccontr)
paulson@14374
  1331
apply (simp add: hcomplex_of_complex_def)
paulson@14354
  1332
done
paulson@14354
  1333
paulson@14354
  1334
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
paulson@14374
  1335
by (simp add: iii_def hcomplex_of_complex_def)
paulson@14314
  1336
paulson@14374
  1337
lemma hcomplex_of_complex_add [simp]:
paulson@14314
  1338
     "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
paulson@14374
  1339
by (simp add: hcomplex_of_complex_def hcomplex_add)
paulson@14314
  1340
paulson@14374
  1341
lemma hcomplex_of_complex_mult [simp]:
paulson@14314
  1342
     "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
paulson@14374
  1343
by (simp add: hcomplex_of_complex_def hcomplex_mult)
paulson@14314
  1344
paulson@14374
  1345
lemma hcomplex_of_complex_eq_iff [simp]:
paulson@14374
  1346
     "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
paulson@14374
  1347
by (simp add: hcomplex_of_complex_def)
paulson@14314
  1348
paulson@14374
  1349
paulson@14374
  1350
lemma hcomplex_of_complex_minus [simp]:
paulson@14335
  1351
     "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
paulson@14374
  1352
by (simp add: hcomplex_of_complex_def hcomplex_minus)
paulson@14314
  1353
paulson@14374
  1354
lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1"
paulson@14374
  1355
by (simp add: hcomplex_of_complex_def hcomplex_one_def)
paulson@14314
  1356
paulson@14374
  1357
lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
paulson@14374
  1358
by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
paulson@14314
  1359
paulson@14387
  1360
lemma hcomplex_of_complex_zero_iff [simp]:
paulson@14387
  1361
     "(hcomplex_of_complex r = 0) = (r = 0)"
paulson@14387
  1362
by (auto intro: FreeUltrafilterNat_P 
paulson@14387
  1363
         simp add: hcomplex_of_complex_def hcomplex_zero_def)
paulson@14314
  1364
paulson@14374
  1365
lemma hcomplex_of_complex_inverse [simp]:
paulson@14335
  1366
     "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
paulson@14314
  1367
apply (case_tac "r=0")
paulson@14336
  1368
apply (simp add: hcomplex_of_complex_zero)
paulson@14374
  1369
apply (rule_tac c1 = "hcomplex_of_complex r"
paulson@14336
  1370
       in hcomplex_mult_left_cancel [THEN iffD1])
paulson@14314
  1371
apply (force simp add: hcomplex_of_complex_zero_iff)
paulson@14314
  1372
apply (subst hcomplex_of_complex_mult [symmetric])
paulson@14374
  1373
apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
paulson@14314
  1374
done
paulson@14314
  1375
paulson@14374
  1376
lemma hcomplex_of_complex_divide [simp]:
paulson@14335
  1377
     "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
paulson@14374
  1378
by (simp add: hcomplex_divide_def complex_divide_def)
paulson@14314
  1379
paulson@14314
  1380
lemma hRe_hcomplex_of_complex:
paulson@14314
  1381
   "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
paulson@14374
  1382
by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
paulson@14314
  1383
paulson@14314
  1384
lemma hIm_hcomplex_of_complex:
paulson@14314
  1385
   "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
paulson@14374
  1386
by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
paulson@14314
  1387
paulson@14314
  1388
lemma hcmod_hcomplex_of_complex:
paulson@14314
  1389
     "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
paulson@14374
  1390
by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
paulson@14314
  1391
paulson@14387
  1392
paulson@14387
  1393
subsection{*Numerals and Arithmetic*}
paulson@14387
  1394
paulson@14387
  1395
instance hcomplex :: number ..
paulson@14387
  1396
paulson@14387
  1397
primrec (*the type constraint is essential!*)
paulson@14387
  1398
  number_of_Pls: "number_of bin.Pls = 0"
paulson@14387
  1399
  number_of_Min: "number_of bin.Min = - (1::hcomplex)"
paulson@14387
  1400
  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
paulson@14387
  1401
	                               (number_of w) + (number_of w)"
paulson@14387
  1402
paulson@14387
  1403
declare number_of_Pls [simp del]
paulson@14387
  1404
        number_of_Min [simp del]
paulson@14387
  1405
        number_of_BIT [simp del]
paulson@14387
  1406
paulson@14387
  1407
instance hcomplex :: number_ring
paulson@14387
  1408
proof
paulson@14387
  1409
  show "Numeral0 = (0::hcomplex)" by (rule number_of_Pls)
paulson@14387
  1410
  show "-1 = - (1::hcomplex)" by (rule number_of_Min)
paulson@14387
  1411
  fix w :: bin and x :: bool
paulson@14387
  1412
  show "(number_of (w BIT x) :: hcomplex) =
paulson@14387
  1413
        (if x then 1 else 0) + number_of w + number_of w"
paulson@14387
  1414
    by (rule number_of_BIT)
paulson@14387
  1415
qed
paulson@14387
  1416
paulson@14387
  1417
paulson@14387
  1418
text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
paulson@14387
  1419
lemma hcomplex_number_of [simp]:
paulson@14387
  1420
     "hcomplex_of_complex (number_of w) = number_of w"
paulson@14387
  1421
apply (induct w) 
paulson@14387
  1422
apply (simp_all only: number_of hcomplex_of_complex_add 
paulson@14387
  1423
                      hcomplex_of_complex_minus, simp_all) 
paulson@14387
  1424
done
paulson@14387
  1425
paulson@14387
  1426
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
paulson@14387
  1427
     "hcomplex_of_hypreal (hypreal_of_real x) =  
paulson@14387
  1428
      hcomplex_of_complex(complex_of_real x)"
paulson@14387
  1429
by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def 
paulson@14387
  1430
              complex_of_real_def)
paulson@14387
  1431
paulson@14387
  1432
lemma hcomplex_hypreal_number_of: 
paulson@14387
  1433
  "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
paulson@14387
  1434
by (simp only: complex_number_of [symmetric] hypreal_number_of [symmetric] 
paulson@14387
  1435
               hcomplex_of_hypreal_eq_hcomplex_of_complex)
paulson@14387
  1436
paulson@14387
  1437
text{*This theorem is necessary because theorems such as
paulson@14387
  1438
   @{text iszero_number_of_0} only hold for ordered rings. They cannot
paulson@14387
  1439
   be generalized to fields in general because they fail for finite fields.
paulson@14387
  1440
   They work for type complex because the reals can be embedded in them.*}
paulson@14387
  1441
lemma iszero_hcomplex_number_of [simp]:
paulson@14387
  1442
     "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
paulson@14387
  1443
apply (simp only: iszero_complex_number_of [symmetric])  
paulson@14387
  1444
apply (simp only: hcomplex_of_complex_zero_iff hcomplex_number_of [symmetric] 
paulson@14387
  1445
                  iszero_def)  
paulson@14387
  1446
done
paulson@14387
  1447
paulson@14387
  1448
paulson@14387
  1449
(*
paulson@14387
  1450
Goal "z + hcnj z =  
paulson@14387
  1451
      hcomplex_of_hypreal (2 * hRe(z))"
paulson@14387
  1452
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
paulson@14387
  1453
by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
paulson@14387
  1454
    hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
paulson@14387
  1455
qed "hcomplex_add_hcnj";
paulson@14387
  1456
paulson@14387
  1457
Goal "z - hcnj z = \
paulson@14387
  1458
\     hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
paulson@14387
  1459
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
paulson@14387
  1460
by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
paulson@14387
  1461
    hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
paulson@14387
  1462
    complex_diff_cnj,iii_def,hcomplex_mult]));
paulson@14387
  1463
qed "hcomplex_diff_hcnj";
paulson@14387
  1464
*)
paulson@14387
  1465
paulson@14387
  1466
paulson@14387
  1467
lemma hcomplex_hcnj_num_zero_iff: "(hcnj z = 0) = (z = 0)"
paulson@14387
  1468
apply (auto simp add: hcomplex_hcnj_zero_iff)
paulson@14387
  1469
done
paulson@14387
  1470
declare hcomplex_hcnj_num_zero_iff [simp]
paulson@14387
  1471
paulson@14387
  1472
lemma hcomplex_zero_num: "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})"
paulson@14387
  1473
apply (simp add: hcomplex_zero_def)
paulson@14387
  1474
done
paulson@14387
  1475
paulson@14387
  1476
lemma hcomplex_one_num: "1 =  Abs_hcomplex (hcomplexrel `` {%n. 1})"
paulson@14387
  1477
apply (simp add: hcomplex_one_def)
paulson@14387
  1478
done
paulson@14387
  1479
paulson@14387
  1480
(*** Real and imaginary stuff ***)
paulson@14387
  1481
paulson@14387
  1482
(*Convert???
paulson@14387
  1483
Goalw [hcomplex_number_of_def] 
paulson@14387
  1484
  "((number_of xa :: hcomplex) + iii * number_of ya =  
paulson@14387
  1485
        number_of xb + iii * number_of yb) =  
paulson@14387
  1486
   (((number_of xa :: hcomplex) = number_of xb) &  
paulson@14387
  1487
    ((number_of ya :: hcomplex) = number_of yb))"
paulson@14387
  1488
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
paulson@14387
  1489
     hcomplex_hypreal_number_of]));
paulson@14387
  1490
qed "hcomplex_number_of_eq_cancel_iff";
paulson@14387
  1491
Addsimps [hcomplex_number_of_eq_cancel_iff];
paulson@14387
  1492
paulson@14387
  1493
Goalw [hcomplex_number_of_def] 
paulson@14387
  1494
  "((number_of xa :: hcomplex) + number_of ya * iii = \
paulson@14387
  1495
\       number_of xb + number_of yb * iii) = \
paulson@14387
  1496
\  (((number_of xa :: hcomplex) = number_of xb) & \
paulson@14387
  1497
\   ((number_of ya :: hcomplex) = number_of yb))";
paulson@14387
  1498
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
paulson@14387
  1499
    hcomplex_hypreal_number_of]));
paulson@14387
  1500
qed "hcomplex_number_of_eq_cancel_iffA";
paulson@14387
  1501
Addsimps [hcomplex_number_of_eq_cancel_iffA];
paulson@14387
  1502
paulson@14387
  1503
Goalw [hcomplex_number_of_def] 
paulson@14387
  1504
  "((number_of xa :: hcomplex) + number_of ya * iii = \
paulson@14387
  1505
\       number_of xb + iii * number_of yb) = \
paulson@14387
  1506
\  (((number_of xa :: hcomplex) = number_of xb) & \
paulson@14387
  1507
\   ((number_of ya :: hcomplex) = number_of yb))";
paulson@14387
  1508
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
paulson@14387
  1509
    hcomplex_hypreal_number_of]));
paulson@14387
  1510
qed "hcomplex_number_of_eq_cancel_iffB";
paulson@14387
  1511
Addsimps [hcomplex_number_of_eq_cancel_iffB];
paulson@14387
  1512
paulson@14387
  1513
Goalw [hcomplex_number_of_def] 
paulson@14387
  1514
  "((number_of xa :: hcomplex) + iii * number_of ya = \
paulson@14387
  1515
\       number_of xb + number_of yb * iii) = \
paulson@14387
  1516
\  (((number_of xa :: hcomplex) = number_of xb) & \
paulson@14387
  1517
\   ((number_of ya :: hcomplex) = number_of yb))";
paulson@14387
  1518
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
paulson@14387
  1519
     hcomplex_hypreal_number_of]));
paulson@14387
  1520
qed "hcomplex_number_of_eq_cancel_iffC";
paulson@14387
  1521
Addsimps [hcomplex_number_of_eq_cancel_iffC];
paulson@14387
  1522
paulson@14387
  1523
Goalw [hcomplex_number_of_def] 
paulson@14387
  1524
  "((number_of xa :: hcomplex) + iii * number_of ya = \
paulson@14387
  1525
\       number_of xb) = \
paulson@14387
  1526
\  (((number_of xa :: hcomplex) = number_of xb) & \
paulson@14387
  1527
\   ((number_of ya :: hcomplex) = 0))";
paulson@14387
  1528
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
paulson@14387
  1529
    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
paulson@14387
  1530
qed "hcomplex_number_of_eq_cancel_iff2";
paulson@14387
  1531
Addsimps [hcomplex_number_of_eq_cancel_iff2];
paulson@14387
  1532
paulson@14387
  1533
Goalw [hcomplex_number_of_def] 
paulson@14387
  1534
  "((number_of xa :: hcomplex) + number_of ya * iii = \
paulson@14387
  1535
\       number_of xb) = \
paulson@14387
  1536
\  (((number_of xa :: hcomplex) = number_of xb) & \
paulson@14387
  1537
\   ((number_of ya :: hcomplex) = 0))";
paulson@14387
  1538
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
paulson@14387
  1539
    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
paulson@14387
  1540
qed "hcomplex_number_of_eq_cancel_iff2a";
paulson@14387
  1541
Addsimps [hcomplex_number_of_eq_cancel_iff2a];
paulson@14387
  1542
paulson@14387
  1543
Goalw [hcomplex_number_of_def] 
paulson@14387
  1544
  "((number_of xa :: hcomplex) + iii * number_of ya = \
paulson@14387
  1545
\    iii * number_of yb) = \
paulson@14387
  1546
\  (((number_of xa :: hcomplex) = 0) & \
paulson@14387
  1547
\   ((number_of ya :: hcomplex) = number_of yb))";
paulson@14387
  1548
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
paulson@14387
  1549
    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
paulson@14387
  1550
qed "hcomplex_number_of_eq_cancel_iff3";
paulson@14387
  1551
Addsimps [hcomplex_number_of_eq_cancel_iff3];
paulson@14387
  1552
paulson@14387
  1553
Goalw [hcomplex_number_of_def] 
paulson@14387
  1554
  "((number_of xa :: hcomplex) + number_of ya * iii= \
paulson@14387
  1555
\    iii * number_of yb) = \
paulson@14387
  1556
\  (((number_of xa :: hcomplex) = 0) & \
paulson@14387
  1557
\   ((number_of ya :: hcomplex) = number_of yb))";
paulson@14387
  1558
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
paulson@14387
  1559
    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
paulson@14387
  1560
qed "hcomplex_number_of_eq_cancel_iff3a";
paulson@14387
  1561
Addsimps [hcomplex_number_of_eq_cancel_iff3a];
paulson@14387
  1562
*)
paulson@14387
  1563
paulson@14387
  1564
lemma hcomplex_number_of_hcnj [simp]:
paulson@14387
  1565
     "hcnj (number_of v :: hcomplex) = number_of v"
paulson@14387
  1566
by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
paulson@14387
  1567
               hcomplex_hcnj_hcomplex_of_hypreal)
paulson@14387
  1568
paulson@14387
  1569
lemma hcomplex_number_of_hcmod [simp]: 
paulson@14387
  1570
      "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
paulson@14387
  1571
by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
paulson@14387
  1572
               hcmod_hcomplex_of_hypreal)
paulson@14387
  1573
paulson@14387
  1574
lemma hcomplex_number_of_hRe [simp]: 
paulson@14387
  1575
      "hRe(number_of v :: hcomplex) = number_of v"
paulson@14387
  1576
by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
paulson@14387
  1577
               hRe_hcomplex_of_hypreal)
paulson@14387
  1578
paulson@14387
  1579
lemma hcomplex_number_of_hIm [simp]: 
paulson@14387
  1580
      "hIm(number_of v :: hcomplex) = 0"
paulson@14387
  1581
by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
paulson@14387
  1582
               hIm_hcomplex_of_hypreal)
paulson@14387
  1583
paulson@14387
  1584
paulson@14314
  1585
ML
paulson@14314
  1586
{*
paulson@14314
  1587
val hcomplex_zero_def = thm"hcomplex_zero_def";
paulson@14314
  1588
val hcomplex_one_def = thm"hcomplex_one_def";
paulson@14314
  1589
val hcomplex_minus_def = thm"hcomplex_minus_def";
paulson@14314
  1590
val hcomplex_diff_def = thm"hcomplex_diff_def";
paulson@14314
  1591
val hcomplex_divide_def = thm"hcomplex_divide_def";
paulson@14314
  1592
val hcomplex_mult_def = thm"hcomplex_mult_def";
paulson@14314
  1593
val hcomplex_add_def = thm"hcomplex_add_def";
paulson@14314
  1594
val hcomplex_of_complex_def = thm"hcomplex_of_complex_def";
paulson@14314
  1595
val iii_def = thm"iii_def";
paulson@14314
  1596
paulson@14314
  1597
val hcomplexrel_iff = thm"hcomplexrel_iff";
paulson@14314
  1598
val hcomplexrel_refl = thm"hcomplexrel_refl";
paulson@14314
  1599
val hcomplexrel_sym = thm"hcomplexrel_sym";
paulson@14314
  1600
val hcomplexrel_trans = thm"hcomplexrel_trans";
paulson@14314
  1601
val equiv_hcomplexrel = thm"equiv_hcomplexrel";
paulson@14314
  1602
val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff";
paulson@14314
  1603
val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex";
paulson@14314
  1604
val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex";
paulson@14314
  1605
val inj_Rep_hcomplex = thm"inj_Rep_hcomplex";
paulson@14314
  1606
val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl";
paulson@14314
  1607
val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem";
paulson@14314
  1608
val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty";
paulson@14314
  1609
val eq_Abs_hcomplex = thm"eq_Abs_hcomplex";
paulson@14314
  1610
val hRe = thm"hRe";
paulson@14314
  1611
val hIm = thm"hIm";
paulson@14314
  1612
val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
paulson@14314
  1613
val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
paulson@14314
  1614
val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
paulson@14314
  1615
val hcomplex_hRe_one = thm"hcomplex_hRe_one";
paulson@14314
  1616
val hcomplex_hIm_one = thm"hcomplex_hIm_one";
paulson@14314
  1617
val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
paulson@14314
  1618
val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
paulson@14314
  1619
val hcomplex_add_congruent2 = thm"hcomplex_add_congruent2";
paulson@14314
  1620
val hcomplex_add = thm"hcomplex_add";
paulson@14314
  1621
val hcomplex_add_commute = thm"hcomplex_add_commute";
paulson@14314
  1622
val hcomplex_add_assoc = thm"hcomplex_add_assoc";
paulson@14314
  1623
val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
paulson@14314
  1624
val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
paulson@14314
  1625
val hRe_add = thm"hRe_add";
paulson@14314
  1626
val hIm_add = thm"hIm_add";
paulson@14314
  1627
val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
paulson@14314
  1628
val hcomplex_minus = thm"hcomplex_minus";
paulson@14314
  1629
val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
paulson@14314
  1630
val hRe_minus = thm"hRe_minus";
paulson@14314
  1631
val hIm_minus = thm"hIm_minus";
paulson@14314
  1632
val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
paulson@14314
  1633
val hcomplex_diff = thm"hcomplex_diff";
paulson@14314
  1634
val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
paulson@14314
  1635
val hcomplex_mult = thm"hcomplex_mult";
paulson@14314
  1636
val hcomplex_mult_commute = thm"hcomplex_mult_commute";
paulson@14314
  1637
val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
paulson@14314
  1638
val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
paulson@14314
  1639
val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
paulson@14314
  1640
val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
paulson@14314
  1641
val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
paulson@14314
  1642
val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
paulson@14314
  1643
val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
paulson@14314
  1644
val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
paulson@14314
  1645
val hcomplex_inverse = thm"hcomplex_inverse";
paulson@14314
  1646
val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
paulson@14314
  1647
val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
paulson@14314
  1648
val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
paulson@14314
  1649
val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
paulson@14314
  1650
val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
paulson@14314
  1651
val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
paulson@14314
  1652
val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
paulson@14314
  1653
val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
paulson@14314
  1654
val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
paulson@14314
  1655
val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
paulson@14314
  1656
val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
paulson@14314
  1657
val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
paulson@14314
  1658
val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
paulson@14314
  1659
val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
paulson@14314
  1660
val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
paulson@14314
  1661
val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
paulson@14314
  1662
val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
paulson@14314
  1663
val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
paulson@14314
  1664
val hcmod = thm"hcmod";
paulson@14314
  1665
val hcmod_zero = thm"hcmod_zero";
paulson@14314
  1666
val hcmod_one = thm"hcmod_one";
paulson@14314
  1667
val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
paulson@14314
  1668
val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
paulson@14314
  1669
val hcnj = thm"hcnj";
paulson@14314
  1670
val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
paulson@14314
  1671
val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
paulson@14314
  1672
val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
paulson@14314
  1673
val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
paulson@14314
  1674
val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
paulson@14314
  1675
val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
paulson@14314
  1676
val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
paulson@14314
  1677
val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
paulson@14314
  1678
val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
paulson@14314
  1679
val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
paulson@14314
  1680
val hcnj_one = thm"hcnj_one";
paulson@14314
  1681
val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
paulson@14314
  1682
val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
paulson@14314
  1683
val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
paulson@14314
  1684
val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
paulson@14314
  1685
val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
paulson@14371
  1686
paulson@14314
  1687
val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
paulson@14314
  1688
val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
paulson@14314
  1689
val hcmod_minus = thm"hcmod_minus";
paulson@14314
  1690
val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
paulson@14314
  1691
val hcmod_ge_zero = thm"hcmod_ge_zero";
paulson@14314
  1692
val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
paulson@14314
  1693
val hcmod_mult = thm"hcmod_mult";
paulson@14314
  1694
val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
paulson@14314
  1695
val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
paulson@14314
  1696
val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
paulson@14314
  1697
val hcmod_triangle_squared = thm"hcmod_triangle_squared";
paulson@14314
  1698
val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
paulson@14314
  1699
val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
paulson@14314
  1700
val hcmod_diff_commute = thm"hcmod_diff_commute";
paulson@14314
  1701
val hcmod_add_less = thm"hcmod_add_less";
paulson@14314
  1702
val hcmod_mult_less = thm"hcmod_mult_less";
paulson@14314
  1703
val hcmod_diff_ineq = thm"hcmod_diff_ineq";
paulson@14314
  1704
val hcpow = thm"hcpow";
paulson@14314
  1705
val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
paulson@14314
  1706
val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
paulson@14314
  1707
val hcmod_hcpow = thm"hcmod_hcpow";
paulson@14314
  1708
val hcpow_minus = thm"hcpow_minus";
paulson@14314
  1709
val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
paulson@14314
  1710
val hcmod_divide = thm"hcmod_divide";
paulson@14314
  1711
val hcpow_mult = thm"hcpow_mult";
paulson@14314
  1712
val hcpow_zero = thm"hcpow_zero";
paulson@14314
  1713
val hcpow_zero2 = thm"hcpow_zero2";
paulson@14314
  1714
val hcpow_not_zero = thm"hcpow_not_zero";
paulson@14314
  1715
val hcpow_zero_zero = thm"hcpow_zero_zero";
paulson@14314
  1716
val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
paulson@14314
  1717
val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
paulson@14314
  1718
val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
paulson@14314
  1719
val hcomplex_divide = thm"hcomplex_divide";
paulson@14314
  1720
val hsgn = thm"hsgn";
paulson@14314
  1721
val hsgn_zero = thm"hsgn_zero";
paulson@14314
  1722
val hsgn_one = thm"hsgn_one";
paulson@14314
  1723
val hsgn_minus = thm"hsgn_minus";
paulson@14314
  1724
val hsgn_eq = thm"hsgn_eq";
paulson@14314
  1725
val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
paulson@14314
  1726
val hcmod_i = thm"hcmod_i";
paulson@14314
  1727
val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
paulson@14314
  1728
val hRe_hsgn = thm"hRe_hsgn";
paulson@14314
  1729
val hIm_hsgn = thm"hIm_hsgn";
paulson@14314
  1730
val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
paulson@14314
  1731
val hRe_mult_i_eq = thm"hRe_mult_i_eq";
paulson@14314
  1732
val hIm_mult_i_eq = thm"hIm_mult_i_eq";
paulson@14314
  1733
val hcmod_mult_i = thm"hcmod_mult_i";
paulson@14314
  1734
val hcmod_mult_i2 = thm"hcmod_mult_i2";
paulson@14314
  1735
val harg = thm"harg";
paulson@14314
  1736
val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
paulson@14314
  1737
val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
paulson@14314
  1738
val complex_split_polar2 = thm"complex_split_polar2";
paulson@14314
  1739
val hcomplex_split_polar = thm"hcomplex_split_polar";
paulson@14314
  1740
val hcis = thm"hcis";
paulson@14314
  1741
val hcis_eq = thm"hcis_eq";
paulson@14314
  1742
val hrcis = thm"hrcis";
paulson@14314
  1743
val hrcis_Ex = thm"hrcis_Ex";
paulson@14314
  1744
val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
paulson@14314
  1745
val hRe_hrcis = thm"hRe_hrcis";
paulson@14314
  1746
val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
paulson@14314
  1747
val hIm_hrcis = thm"hIm_hrcis";
paulson@14314
  1748
val hcmod_complex_polar = thm"hcmod_complex_polar";
paulson@14314
  1749
val hcmod_hrcis = thm"hcmod_hrcis";
paulson@14314
  1750
val hcis_hrcis_eq = thm"hcis_hrcis_eq";
paulson@14314
  1751
val hrcis_mult = thm"hrcis_mult";
paulson@14314
  1752
val hcis_mult = thm"hcis_mult";
paulson@14314
  1753
val hcis_zero = thm"hcis_zero";
paulson@14314
  1754
val hrcis_zero_mod = thm"hrcis_zero_mod";
paulson@14314
  1755
val hrcis_zero_arg = thm"hrcis_zero_arg";
paulson@14314
  1756
val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
paulson@14314
  1757
val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
paulson@14314
  1758
val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
paulson@14314
  1759
val NSDeMoivre = thm"NSDeMoivre";
paulson@14314
  1760
val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
paulson@14314
  1761
val NSDeMoivre_ext = thm"NSDeMoivre_ext";
paulson@14314
  1762
val DeMoivre2 = thm"DeMoivre2";
paulson@14314
  1763
val DeMoivre2_ext = thm"DeMoivre2_ext";
paulson@14314
  1764
val hcis_inverse = thm"hcis_inverse";
paulson@14314
  1765
val hrcis_inverse = thm"hrcis_inverse";
paulson@14314
  1766
val hRe_hcis = thm"hRe_hcis";
paulson@14314
  1767
val hIm_hcis = thm"hIm_hcis";
paulson@14314
  1768
val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
paulson@14314
  1769
val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
paulson@14314
  1770
val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
paulson@14314
  1771
val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
paulson@14314
  1772
val hexpi_add = thm"hexpi_add";
paulson@14314
  1773
val hcomplex_of_complex_add = thm"hcomplex_of_complex_add";
paulson@14314
  1774
val hcomplex_of_complex_mult = thm"hcomplex_of_complex_mult";
paulson@14314
  1775
val hcomplex_of_complex_eq_iff = thm"hcomplex_of_complex_eq_iff";
paulson@14314
  1776
val hcomplex_of_complex_minus = thm"hcomplex_of_complex_minus";
paulson@14314
  1777
val hcomplex_of_complex_one = thm"hcomplex_of_complex_one";
paulson@14314
  1778
val hcomplex_of_complex_zero = thm"hcomplex_of_complex_zero";
paulson@14314
  1779
val hcomplex_of_complex_zero_iff = thm"hcomplex_of_complex_zero_iff";
paulson@14314
  1780
val hcomplex_of_complex_inverse = thm"hcomplex_of_complex_inverse";
paulson@14314
  1781
val hcomplex_of_complex_divide = thm"hcomplex_of_complex_divide";
paulson@14314
  1782
val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
paulson@14314
  1783
val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
paulson@14314
  1784
val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
paulson@14314
  1785
*}
paulson@14314
  1786
paulson@13957
  1787
end