src/HOL/Complex/NSComplex.thy
author paulson
Mon Dec 22 18:29:20 2003 +0100 (2003-12-22)
changeset 14314 314da085adf3
parent 13957 10dbf16be15f
child 14318 7dbd3988b15b
permissions -rw-r--r--
converted Complex/NSComplex to Isar script
paulson@13957
     1
(*  Title:       NSComplex.thy
paulson@13957
     2
    Author:      Jacques D. Fleuriot
paulson@13957
     3
    Copyright:   2001  University of Edinburgh
paulson@13957
     4
    Description: Nonstandard Complex numbers
paulson@13957
     5
*)
paulson@13957
     6
paulson@14314
     7
theory NSComplex = NSInduct:
paulson@13957
     8
paulson@13957
     9
constdefs
paulson@13957
    10
    hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
paulson@14314
    11
    "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) &
paulson@13957
    12
                        {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
paulson@13957
    13
paulson@14314
    14
typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
paulson@14314
    15
  by (auto simp add: quotient_def)
paulson@13957
    16
paulson@14314
    17
instance hcomplex :: zero ..
paulson@14314
    18
instance hcomplex :: one ..
paulson@14314
    19
instance hcomplex :: plus ..
paulson@14314
    20
instance hcomplex :: times ..
paulson@14314
    21
instance hcomplex :: minus ..
paulson@14314
    22
instance hcomplex :: inverse ..
paulson@14314
    23
instance hcomplex :: power ..
paulson@14314
    24
paulson@14314
    25
defs (overloaded)
paulson@14314
    26
  hcomplex_zero_def:
paulson@13957
    27
  "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
paulson@14314
    28
paulson@14314
    29
  hcomplex_one_def:
paulson@13957
    30
  "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"
paulson@13957
    31
paulson@13957
    32
paulson@14314
    33
  hcomplex_minus_def:
paulson@14314
    34
  "- z == Abs_hcomplex(UN X: Rep_hcomplex(z).
paulson@14314
    35
                       hcomplexrel `` {%n::nat. - (X n)})"
paulson@13957
    36
paulson@14314
    37
  hcomplex_diff_def:
paulson@13957
    38
  "w - z == w + -(z::hcomplex)"
paulson@14314
    39
paulson@13957
    40
constdefs
paulson@13957
    41
paulson@14314
    42
  hcomplex_of_complex :: "complex => hcomplex"
paulson@13957
    43
  "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
paulson@14314
    44
paulson@14314
    45
  hcinv  :: "hcomplex => hcomplex"
paulson@14314
    46
  "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P).
paulson@13957
    47
                    hcomplexrel `` {%n. inverse(X n)})"
paulson@13957
    48
paulson@13957
    49
  (*--- real and Imaginary parts ---*)
paulson@14314
    50
paulson@14314
    51
  hRe :: "hcomplex => hypreal"
paulson@13957
    52
  "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
paulson@13957
    53
paulson@14314
    54
  hIm :: "hcomplex => hypreal"
paulson@14314
    55
  "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
paulson@13957
    56
paulson@13957
    57
paulson@13957
    58
  (*----------- modulus ------------*)
paulson@13957
    59
paulson@14314
    60
  hcmod :: "hcomplex => hypreal"
paulson@13957
    61
  "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
paulson@13957
    62
			  hyprel `` {%n. cmod (X n)})"
paulson@13957
    63
paulson@14314
    64
  (*------ imaginary unit ----------*)
paulson@14314
    65
paulson@14314
    66
  iii :: hcomplex
paulson@13957
    67
  "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"
paulson@13957
    68
paulson@13957
    69
  (*------- complex conjugate ------*)
paulson@13957
    70
paulson@14314
    71
  hcnj :: "hcomplex => hcomplex"
paulson@13957
    72
  "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"
paulson@13957
    73
paulson@14314
    74
  (*------------ Argand -------------*)
paulson@13957
    75
paulson@14314
    76
  hsgn :: "hcomplex => hcomplex"
paulson@13957
    77
  "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
paulson@13957
    78
paulson@14314
    79
  harg :: "hcomplex => hypreal"
paulson@13957
    80
  "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
paulson@13957
    81
paulson@13957
    82
  (* abbreviation for (cos a + i sin a) *)
paulson@14314
    83
  hcis :: "hypreal => hcomplex"
paulson@13957
    84
  "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
paulson@13957
    85
paulson@13957
    86
  (* abbreviation for r*(cos a + i sin a) *)
paulson@14314
    87
  hrcis :: "[hypreal, hypreal] => hcomplex"
paulson@13957
    88
  "hrcis r a == hcomplex_of_hypreal r * hcis a"
paulson@13957
    89
paulson@14314
    90
  (*----- injection from hyperreals -----*)
paulson@14314
    91
paulson@14314
    92
  hcomplex_of_hypreal :: "hypreal => hcomplex"
paulson@13957
    93
  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
paulson@13957
    94
			       hcomplexrel `` {%n. complex_of_real (X n)})"
paulson@13957
    95
paulson@13957
    96
  (*------------ e ^ (x + iy) ------------*)
paulson@13957
    97
paulson@14314
    98
  hexpi :: "hcomplex => hcomplex"
paulson@13957
    99
  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
paulson@14314
   100
paulson@13957
   101
paulson@14314
   102
defs (overloaded)
paulson@13957
   103
paulson@13957
   104
  (*----------- division ----------*)
paulson@13957
   105
paulson@14314
   106
  hcomplex_divide_def:
paulson@13957
   107
  "w / (z::hcomplex) == w * inverse z"
paulson@14314
   108
paulson@14314
   109
  hcomplex_add_def:
paulson@13957
   110
  "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@13957
   111
		      hcomplexrel `` {%n. X n + Y n})"
paulson@13957
   112
paulson@14314
   113
  hcomplex_mult_def:
paulson@13957
   114
  "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@14314
   115
		      hcomplexrel `` {%n. X n * Y n})"
paulson@13957
   116
paulson@13957
   117
paulson@13957
   118
primrec
paulson@14314
   119
     hcomplexpow_0:   "z ^ 0       = 1"
paulson@14314
   120
     hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
paulson@13957
   121
paulson@13957
   122
paulson@13957
   123
consts
paulson@14314
   124
  "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr 80)
paulson@13957
   125
paulson@13957
   126
defs
paulson@13957
   127
  (* hypernatural powers of nonstandard complex numbers *)
paulson@14314
   128
  hcpow_def:
paulson@14314
   129
  "(z::hcomplex) hcpow (n::hypnat)
paulson@13957
   130
      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
paulson@13957
   131
             hcomplexrel `` {%n. (X n) ^ (Y n)})"
paulson@13957
   132
paulson@14314
   133
paulson@14314
   134
lemma hcomplexrel_iff:
paulson@14314
   135
   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
paulson@14314
   136
apply (unfold hcomplexrel_def)
paulson@14314
   137
apply fast
paulson@14314
   138
done
paulson@14314
   139
paulson@14314
   140
lemma hcomplexrel_refl: "(x,x): hcomplexrel"
paulson@14314
   141
apply (simp add: hcomplexrel_iff) 
paulson@14314
   142
done
paulson@14314
   143
paulson@14314
   144
lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
paulson@14314
   145
apply (auto simp add: hcomplexrel_iff eq_commute)
paulson@14314
   146
done
paulson@14314
   147
paulson@14314
   148
lemma hcomplexrel_trans:
paulson@14314
   149
      "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
paulson@14314
   150
apply (simp add: hcomplexrel_iff) 
paulson@14314
   151
apply ultra
paulson@14314
   152
done
paulson@14314
   153
paulson@14314
   154
lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
paulson@14314
   155
apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) 
paulson@14314
   156
apply (blast intro: hcomplexrel_sym hcomplexrel_trans) 
paulson@14314
   157
done
paulson@14314
   158
paulson@14314
   159
lemmas equiv_hcomplexrel_iff =
paulson@14314
   160
    eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
paulson@14314
   161
paulson@14314
   162
lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
paulson@14314
   163
apply (unfold hcomplex_def hcomplexrel_def quotient_def)
paulson@14314
   164
apply blast
paulson@14314
   165
done
paulson@14314
   166
paulson@14314
   167
lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
paulson@14314
   168
apply (rule inj_on_inverseI)
paulson@14314
   169
apply (erule Abs_hcomplex_inverse)
paulson@14314
   170
done
paulson@14314
   171
paulson@14314
   172
declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp]
paulson@14314
   173
        Abs_hcomplex_inverse [simp]
paulson@14314
   174
paulson@14314
   175
declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
paulson@14314
   176
paulson@14314
   177
declare hcomplexrel_iff [iff]
paulson@14314
   178
paulson@14314
   179
lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
paulson@14314
   180
apply (rule inj_on_inverseI)
paulson@14314
   181
apply (rule Rep_hcomplex_inverse)
paulson@14314
   182
done
paulson@14314
   183
paulson@14314
   184
lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}"
paulson@14314
   185
apply (unfold hcomplexrel_def)
paulson@14314
   186
apply (safe)
paulson@14314
   187
apply auto
paulson@14314
   188
done
paulson@14314
   189
declare lemma_hcomplexrel_refl [simp]
paulson@14314
   190
paulson@14314
   191
lemma hcomplex_empty_not_mem: "{} ~: hcomplex"
paulson@14314
   192
apply (unfold hcomplex_def)
paulson@14314
   193
apply (auto elim!: quotientE)
paulson@14314
   194
done
paulson@14314
   195
declare hcomplex_empty_not_mem [simp]
paulson@14314
   196
paulson@14314
   197
lemma Rep_hcomplex_nonempty: "Rep_hcomplex x ~= {}"
paulson@14314
   198
apply (cut_tac x = "x" in Rep_hcomplex)
paulson@14314
   199
apply auto
paulson@14314
   200
done
paulson@14314
   201
declare Rep_hcomplex_nonempty [simp]
paulson@14314
   202
paulson@14314
   203
lemma eq_Abs_hcomplex:
paulson@14314
   204
    "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
paulson@14314
   205
apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
paulson@14314
   206
apply (drule_tac f = Abs_hcomplex in arg_cong)
paulson@14314
   207
apply (force simp add: Rep_hcomplex_inverse)
paulson@14314
   208
done
paulson@14314
   209
paulson@14314
   210
paulson@14314
   211
subsection{*Properties of Nonstandard Real and Imaginary Parts*}
paulson@14314
   212
paulson@14314
   213
lemma hRe:
paulson@14314
   214
     "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
paulson@14314
   215
      Abs_hypreal(hyprel `` {%n. Re(X n)})"
paulson@14314
   216
apply (unfold hRe_def)
paulson@14314
   217
apply (rule_tac f = "Abs_hypreal" in arg_cong)
paulson@14314
   218
apply (auto , ultra)
paulson@14314
   219
done
paulson@14314
   220
paulson@14314
   221
lemma hIm:
paulson@14314
   222
     "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
paulson@14314
   223
      Abs_hypreal(hyprel `` {%n. Im(X n)})"
paulson@14314
   224
apply (unfold hIm_def)
paulson@14314
   225
apply (rule_tac f = "Abs_hypreal" in arg_cong)
paulson@14314
   226
apply (auto , ultra)
paulson@14314
   227
done
paulson@14314
   228
paulson@14314
   229
lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
paulson@14314
   230
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   231
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   232
apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
paulson@14314
   233
apply (ultra+)
paulson@14314
   234
done
paulson@14314
   235
paulson@14314
   236
lemma hcomplex_hRe_zero: "hRe 0 = 0"
paulson@14314
   237
apply (unfold hcomplex_zero_def)
paulson@14314
   238
apply (simp (no_asm) add: hRe hypreal_zero_num)
paulson@14314
   239
done
paulson@14314
   240
declare hcomplex_hRe_zero [simp]
paulson@14314
   241
paulson@14314
   242
lemma hcomplex_hIm_zero: "hIm 0 = 0"
paulson@14314
   243
apply (unfold hcomplex_zero_def)
paulson@14314
   244
apply (simp (no_asm) add: hIm hypreal_zero_num)
paulson@14314
   245
done
paulson@14314
   246
declare hcomplex_hIm_zero [simp]
paulson@14314
   247
paulson@14314
   248
lemma hcomplex_hRe_one: "hRe 1 = 1"
paulson@14314
   249
apply (unfold hcomplex_one_def)
paulson@14314
   250
apply (simp (no_asm) add: hRe hypreal_one_num)
paulson@14314
   251
done
paulson@14314
   252
declare hcomplex_hRe_one [simp]
paulson@14314
   253
paulson@14314
   254
lemma hcomplex_hIm_one: "hIm 1 = 0"
paulson@14314
   255
apply (unfold hcomplex_one_def)
paulson@14314
   256
apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num)
paulson@14314
   257
done
paulson@14314
   258
declare hcomplex_hIm_one [simp]
paulson@14314
   259
paulson@14314
   260
(*-----------------------------------------------------------------------*)
paulson@14314
   261
(*   hcomplex_of_complex: the injection from complex to hcomplex         *)
paulson@14314
   262
(* ----------------------------------------------------------------------*)
paulson@14314
   263
paulson@14314
   264
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
paulson@14314
   265
apply (rule inj_onI , rule ccontr)
paulson@14314
   266
apply (auto simp add: hcomplex_of_complex_def)
paulson@14314
   267
done
paulson@14314
   268
paulson@14314
   269
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
paulson@14314
   270
apply (unfold iii_def hcomplex_of_complex_def)
paulson@14314
   271
apply (simp (no_asm))
paulson@14314
   272
done
paulson@14314
   273
paulson@14314
   274
(*-----------------------------------------------------------------------*)
paulson@14314
   275
(*   Addition for nonstandard complex numbers: hcomplex_add              *)
paulson@14314
   276
(* ----------------------------------------------------------------------*)
paulson@14314
   277
paulson@14314
   278
lemma hcomplex_add_congruent2:
paulson@14314
   279
    "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
paulson@14314
   280
apply (unfold congruent2_def)
paulson@14314
   281
apply safe
paulson@14314
   282
apply (ultra+)
paulson@14314
   283
done
paulson@14314
   284
paulson@14314
   285
lemma hcomplex_add:
paulson@14314
   286
  "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14314
   287
   Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
paulson@14314
   288
apply (unfold hcomplex_add_def)
paulson@14314
   289
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   290
apply auto
paulson@14314
   291
apply (ultra)
paulson@14314
   292
done
paulson@14314
   293
paulson@14314
   294
lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
paulson@14314
   295
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   296
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   297
apply (simp (no_asm_simp) add: complex_add_commute hcomplex_add)
paulson@14314
   298
done
paulson@14314
   299
paulson@14314
   300
lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
paulson@14314
   301
apply (rule_tac z = "z1" in eq_Abs_hcomplex)
paulson@14314
   302
apply (rule_tac z = "z2" in eq_Abs_hcomplex)
paulson@14314
   303
apply (rule_tac z = "z3" in eq_Abs_hcomplex)
paulson@14314
   304
apply (simp (no_asm_simp) add: hcomplex_add complex_add_assoc)
paulson@14314
   305
done
paulson@14314
   306
paulson@14314
   307
(*For AC rewriting*)
paulson@14314
   308
lemma hcomplex_add_left_commute: "(x::hcomplex)+(y+z)=y+(x+z)"
paulson@14314
   309
apply (rule hcomplex_add_commute [THEN trans])
paulson@14314
   310
apply (rule hcomplex_add_assoc [THEN trans])
paulson@14314
   311
apply (rule hcomplex_add_commute [THEN arg_cong])
paulson@14314
   312
done
paulson@14314
   313
paulson@14314
   314
(* hcomplex addition is an AC operator *)
paulson@14314
   315
lemmas hcomplex_add_ac = hcomplex_add_assoc hcomplex_add_commute
paulson@14314
   316
                      hcomplex_add_left_commute 
paulson@14314
   317
paulson@14314
   318
lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
paulson@14314
   319
apply (unfold hcomplex_zero_def)
paulson@14314
   320
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   321
apply (simp add: hcomplex_add)
paulson@14314
   322
done
paulson@14314
   323
paulson@14314
   324
lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
paulson@14314
   325
apply (simp (no_asm) add: hcomplex_add_zero_left hcomplex_add_commute)
paulson@14314
   326
done
paulson@14314
   327
declare hcomplex_add_zero_left [simp] hcomplex_add_zero_right [simp]
paulson@14314
   328
paulson@14314
   329
lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
paulson@14314
   330
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   331
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   332
apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add)
paulson@14314
   333
done
paulson@14314
   334
paulson@14314
   335
lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
paulson@14314
   336
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   337
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   338
apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
paulson@14314
   339
done
paulson@14314
   340
paulson@14314
   341
(*-----------------------------------------------------------------------*)
paulson@14314
   342
(* hypreal_minus: additive inverse on nonstandard complex                *)
paulson@14314
   343
(* ----------------------------------------------------------------------*)
paulson@14314
   344
paulson@14314
   345
lemma hcomplex_minus_congruent:
paulson@14314
   346
  "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
paulson@14314
   347
paulson@14314
   348
apply (unfold congruent_def)
paulson@14314
   349
apply safe
paulson@14314
   350
apply (ultra+)
paulson@14314
   351
done
paulson@14314
   352
paulson@14314
   353
lemma hcomplex_minus:
paulson@14314
   354
  "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   355
      Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
paulson@14314
   356
apply (unfold hcomplex_minus_def)
paulson@14314
   357
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   358
apply (auto , ultra)
paulson@14314
   359
done
paulson@14314
   360
paulson@14314
   361
lemma hcomplex_minus_minus: "- (- z) = (z::hcomplex)"
paulson@14314
   362
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   363
apply (simp (no_asm_simp) add: hcomplex_minus)
paulson@14314
   364
done
paulson@14314
   365
declare hcomplex_minus_minus [simp]
paulson@14314
   366
paulson@14314
   367
lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)"
paulson@14314
   368
apply (rule inj_onI)
paulson@14314
   369
apply (drule_tac f = "uminus" in arg_cong)
paulson@14314
   370
apply simp
paulson@14314
   371
done
paulson@14314
   372
paulson@14314
   373
lemma hcomplex_minus_zero: "- 0 = (0::hcomplex)"
paulson@14314
   374
apply (unfold hcomplex_zero_def)
paulson@14314
   375
apply (simp (no_asm) add: hcomplex_minus)
paulson@14314
   376
done
paulson@14314
   377
declare hcomplex_minus_zero [simp]
paulson@14314
   378
paulson@14314
   379
lemma hcomplex_minus_zero_iff: "(-x = 0) = (x = (0::hcomplex))"
paulson@14314
   380
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   381
apply (auto simp add: hcomplex_zero_def hcomplex_minus)
paulson@14314
   382
done
paulson@14314
   383
declare hcomplex_minus_zero_iff [simp]
paulson@14314
   384
paulson@14314
   385
lemma hcomplex_minus_zero_iff2: "(0 = -x) = (x = (0::hcomplex))"
paulson@14314
   386
apply (auto dest: sym)
paulson@14314
   387
done
paulson@14314
   388
declare hcomplex_minus_zero_iff2 [simp]
paulson@14314
   389
paulson@14314
   390
lemma hcomplex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::hcomplex))"
paulson@14314
   391
apply auto
paulson@14314
   392
done
paulson@14314
   393
paulson@14314
   394
lemma hcomplex_add_minus_right: "z + - z = (0::hcomplex)"
paulson@14314
   395
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   396
apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
paulson@14314
   397
done
paulson@14314
   398
declare hcomplex_add_minus_right [simp]
paulson@14314
   399
paulson@14314
   400
lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
paulson@14314
   401
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   402
apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
paulson@14314
   403
done
paulson@14314
   404
declare hcomplex_add_minus_left [simp]
paulson@14314
   405
paulson@14314
   406
lemma hcomplex_add_minus_cancel: "z + (- z + w) = (w::hcomplex)"
paulson@14314
   407
apply (simp (no_asm) add: hcomplex_add_assoc [symmetric])
paulson@14314
   408
done
paulson@14314
   409
paulson@14314
   410
lemma hcomplex_minus_add_cancel: "(-z) + (z + w) = (w::hcomplex)"
paulson@14314
   411
apply (simp (no_asm) add: hcomplex_add_assoc [symmetric])
paulson@14314
   412
done
paulson@14314
   413
paulson@14314
   414
lemma hRe_minus: "hRe(-z) = - hRe(z)"
paulson@14314
   415
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   416
apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
paulson@14314
   417
done
paulson@14314
   418
paulson@14314
   419
lemma hIm_minus: "hIm(-z) = - hIm(z)"
paulson@14314
   420
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   421
apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
paulson@14314
   422
done
paulson@14314
   423
paulson@14314
   424
lemma hcomplex_add_minus_eq_minus:
paulson@14314
   425
      "x + y = (0::hcomplex) ==> x = -y"
paulson@14314
   426
apply (unfold hcomplex_zero_def)
paulson@14314
   427
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   428
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   429
apply (auto simp add: hcomplex_add hcomplex_minus)
paulson@14314
   430
apply ultra
paulson@14314
   431
done
paulson@14314
   432
paulson@14314
   433
lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)"
paulson@14314
   434
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   435
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   436
apply (auto simp add: hcomplex_add hcomplex_minus)
paulson@14314
   437
done
paulson@14314
   438
declare hcomplex_minus_add_distrib [simp]
paulson@14314
   439
paulson@14314
   440
lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)"
paulson@14314
   441
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   442
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   443
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   444
apply (auto simp add: hcomplex_add)
paulson@14314
   445
done
paulson@14314
   446
declare hcomplex_add_left_cancel [iff]
paulson@14314
   447
paulson@14314
   448
lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)"
paulson@14314
   449
apply (simp (no_asm) add: hcomplex_add_commute)
paulson@14314
   450
done
paulson@14314
   451
declare hcomplex_add_right_cancel [iff]
paulson@14314
   452
paulson@14314
   453
lemma hcomplex_eq_minus_iff: "((x::hcomplex) = y) = ((0::hcomplex) = x + - y)"
paulson@14314
   454
apply (safe)
paulson@14314
   455
apply (rule_tac [2] x1 = "-y" in hcomplex_add_right_cancel [THEN iffD1])
paulson@14314
   456
apply auto
paulson@14314
   457
done
paulson@14314
   458
paulson@14314
   459
lemma hcomplex_eq_minus_iff2: "((x::hcomplex) = y) = (x + - y = (0::hcomplex))"
paulson@14314
   460
apply (safe)
paulson@14314
   461
apply (rule_tac [2] x1 = "-y" in hcomplex_add_right_cancel [THEN iffD1])
paulson@14314
   462
apply auto
paulson@14314
   463
done
paulson@14314
   464
paulson@14314
   465
subsection{*Subraction for Nonstandard Complex Numbers*}
paulson@14314
   466
paulson@14314
   467
lemma hcomplex_diff:
paulson@14314
   468
  "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14314
   469
   Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
paulson@14314
   470
paulson@14314
   471
apply (unfold hcomplex_diff_def)
paulson@14314
   472
apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def)
paulson@14314
   473
done
paulson@14314
   474
paulson@14314
   475
lemma hcomplex_diff_zero: "(z::hcomplex) - z = (0::hcomplex)"
paulson@14314
   476
apply (unfold hcomplex_diff_def)
paulson@14314
   477
apply (simp (no_asm))
paulson@14314
   478
done
paulson@14314
   479
declare hcomplex_diff_zero [simp]
paulson@14314
   480
paulson@14314
   481
lemma hcomplex_diff_0: "(0::hcomplex) - x = -x"
paulson@14314
   482
apply (simp (no_asm) add: hcomplex_diff_def)
paulson@14314
   483
done
paulson@14314
   484
paulson@14314
   485
lemma hcomplex_diff_0_right: "x - (0::hcomplex) = x"
paulson@14314
   486
apply (simp (no_asm) add: hcomplex_diff_def)
paulson@14314
   487
done
paulson@14314
   488
paulson@14314
   489
lemma hcomplex_diff_self: "x - x = (0::hcomplex)"
paulson@14314
   490
apply (simp (no_asm) add: hcomplex_diff_def)
paulson@14314
   491
done
paulson@14314
   492
paulson@14314
   493
declare hcomplex_diff_0 [simp] hcomplex_diff_0_right [simp] hcomplex_diff_self [simp]
paulson@14314
   494
paulson@14314
   495
lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)"
paulson@14314
   496
apply (auto simp add: hcomplex_diff_def hcomplex_add_assoc)
paulson@14314
   497
done
paulson@14314
   498
paulson@14314
   499
subsection{*Multiplication for Nonstandard Complex Numbers*}
paulson@14314
   500
paulson@14314
   501
lemma hcomplex_mult:
paulson@14314
   502
  "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14314
   503
   Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
paulson@14314
   504
paulson@14314
   505
apply (unfold hcomplex_mult_def)
paulson@14314
   506
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   507
apply (auto , ultra)
paulson@14314
   508
done
paulson@14314
   509
paulson@14314
   510
lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
paulson@14314
   511
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   512
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   513
apply (auto simp add: hcomplex_mult complex_mult_commute)
paulson@14314
   514
done
paulson@14314
   515
paulson@14314
   516
lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
paulson@14314
   517
apply (rule_tac z = "u" in eq_Abs_hcomplex)
paulson@14314
   518
apply (rule_tac z = "v" in eq_Abs_hcomplex)
paulson@14314
   519
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   520
apply (auto simp add: hcomplex_mult complex_mult_assoc)
paulson@14314
   521
done
paulson@14314
   522
paulson@14314
   523
lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)"
paulson@14314
   524
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   525
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   526
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   527
apply (auto simp add: hcomplex_mult complex_mult_left_commute)
paulson@14314
   528
done
paulson@14314
   529
paulson@14314
   530
lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute
paulson@14314
   531
                        hcomplex_mult_left_commute
paulson@14314
   532
paulson@14314
   533
lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
paulson@14314
   534
apply (unfold hcomplex_one_def)
paulson@14314
   535
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   536
apply (auto simp add: hcomplex_mult)
paulson@14314
   537
done
paulson@14314
   538
declare hcomplex_mult_one_left [simp]
paulson@14314
   539
paulson@14314
   540
lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
paulson@14314
   541
apply (simp (no_asm) add: hcomplex_mult_commute)
paulson@14314
   542
done
paulson@14314
   543
declare hcomplex_mult_one_right [simp]
paulson@14314
   544
paulson@14314
   545
lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
paulson@14314
   546
apply (unfold hcomplex_zero_def)
paulson@14314
   547
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   548
apply (auto simp add: hcomplex_mult)
paulson@14314
   549
done
paulson@14314
   550
declare hcomplex_mult_zero_left [simp]
paulson@14314
   551
paulson@14314
   552
lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0"
paulson@14314
   553
apply (simp (no_asm) add: hcomplex_mult_commute)
paulson@14314
   554
done
paulson@14314
   555
declare hcomplex_mult_zero_right [simp]
paulson@14314
   556
paulson@14314
   557
lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)"
paulson@14314
   558
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   559
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   560
apply (auto simp add: hcomplex_mult hcomplex_minus)
paulson@14314
   561
done
paulson@14314
   562
paulson@14314
   563
lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)"
paulson@14314
   564
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   565
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   566
apply (auto simp add: hcomplex_mult hcomplex_minus)
paulson@14314
   567
done
paulson@14314
   568
paulson@14314
   569
declare hcomplex_minus_mult_eq1 [symmetric, simp] hcomplex_minus_mult_eq2 [symmetric, simp]
paulson@14314
   570
paulson@14314
   571
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
paulson@14314
   572
apply (simp (no_asm))
paulson@14314
   573
done
paulson@14314
   574
declare hcomplex_mult_minus_one [simp]
paulson@14314
   575
paulson@14314
   576
lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
paulson@14314
   577
apply (subst hcomplex_mult_commute)
paulson@14314
   578
apply (simp (no_asm))
paulson@14314
   579
done
paulson@14314
   580
declare hcomplex_mult_minus_one_right [simp]
paulson@14314
   581
paulson@14314
   582
lemma hcomplex_minus_mult_cancel: "-x * -y = x * (y::hcomplex)"
paulson@14314
   583
apply auto
paulson@14314
   584
done
paulson@14314
   585
declare hcomplex_minus_mult_cancel [simp]
paulson@14314
   586
paulson@14314
   587
lemma hcomplex_minus_mult_commute: "-x * y = x * -(y::hcomplex)"
paulson@14314
   588
apply auto
paulson@14314
   589
done
paulson@14314
   590
paulson@14314
   591
lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
paulson@14314
   592
apply (rule_tac z = "z1" in eq_Abs_hcomplex)
paulson@14314
   593
apply (rule_tac z = "z2" in eq_Abs_hcomplex)
paulson@14314
   594
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   595
apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
paulson@14314
   596
done
paulson@14314
   597
paulson@14314
   598
lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)"
paulson@14314
   599
apply (rule_tac z1 = "z1 + z2" in hcomplex_mult_commute [THEN ssubst])
paulson@14314
   600
apply (simp (no_asm) add: hcomplex_add_mult_distrib)
paulson@14314
   601
apply (simp (no_asm) add: hcomplex_mult_commute)
paulson@14314
   602
done
paulson@14314
   603
paulson@14314
   604
lemma hcomplex_zero_not_eq_one: "(0::hcomplex) ~= (1::hcomplex)"
paulson@14314
   605
apply (unfold hcomplex_zero_def hcomplex_one_def)
paulson@14314
   606
apply auto
paulson@14314
   607
done
paulson@14314
   608
declare hcomplex_zero_not_eq_one [simp]
paulson@14314
   609
declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
paulson@14314
   610
paulson@14314
   611
paulson@14314
   612
subsection{*Inverse of Nonstandard Complex Number*}
paulson@14314
   613
paulson@14314
   614
lemma hcomplex_inverse:
paulson@14314
   615
  "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   616
      Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
paulson@14314
   617
apply (unfold hcinv_def)
paulson@14314
   618
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   619
apply (auto , ultra)
paulson@14314
   620
done
paulson@14314
   621
paulson@14314
   622
lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0"
paulson@14314
   623
apply (unfold hcomplex_zero_def)
paulson@14314
   624
apply (auto simp add: hcomplex_inverse)
paulson@14314
   625
done
paulson@14314
   626
paulson@14314
   627
lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0"
paulson@14314
   628
apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
paulson@14314
   629
done
paulson@14314
   630
paulson@14314
   631
lemma hcomplex_mult_inv_left:
paulson@14314
   632
      "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
paulson@14314
   633
apply (unfold hcomplex_zero_def hcomplex_one_def)
paulson@14314
   634
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   635
apply (auto simp add: hcomplex_inverse hcomplex_mult)
paulson@14314
   636
apply (ultra)
paulson@14314
   637
apply (rule ccontr)
paulson@14314
   638
apply (drule complex_mult_inv_left)
paulson@14314
   639
apply auto
paulson@14314
   640
done
paulson@14314
   641
declare hcomplex_mult_inv_left [simp]
paulson@14314
   642
paulson@14314
   643
lemma hcomplex_mult_inv_right: "z ~= (0::hcomplex) ==> z * inverse(z) = (1::hcomplex)"
paulson@14314
   644
apply (auto intro: hcomplex_mult_commute [THEN subst])
paulson@14314
   645
done
paulson@14314
   646
declare hcomplex_mult_inv_right [simp]
paulson@14314
   647
paulson@14314
   648
lemma hcomplex_mult_left_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
paulson@14314
   649
apply auto
paulson@14314
   650
apply (drule_tac f = "%x. x*inverse c" in arg_cong)
paulson@14314
   651
apply (simp add: hcomplex_mult_ac)
paulson@14314
   652
done
paulson@14314
   653
paulson@14314
   654
lemma hcomplex_mult_right_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
paulson@14314
   655
apply (safe)
paulson@14314
   656
apply (drule_tac f = "%x. x*inverse c" in arg_cong)
paulson@14314
   657
apply (simp add: hcomplex_mult_ac)
paulson@14314
   658
done
paulson@14314
   659
paulson@14314
   660
lemma hcomplex_inverse_not_zero: "z ~= (0::hcomplex) ==> inverse(z) ~= 0"
paulson@14314
   661
apply (safe)
paulson@14314
   662
apply (frule hcomplex_mult_right_cancel [THEN iffD2])
paulson@14314
   663
apply (erule_tac [2] V = "inverse z = 0" in thin_rl)
paulson@14314
   664
apply (assumption , auto)
paulson@14314
   665
done
paulson@14314
   666
declare hcomplex_inverse_not_zero [simp]
paulson@14314
   667
paulson@14314
   668
lemma hcomplex_mult_not_zero: "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0"
paulson@14314
   669
apply (safe)
paulson@14314
   670
apply (drule_tac f = "%z. inverse x*z" in arg_cong)
paulson@14314
   671
apply (simp add: hcomplex_mult_assoc [symmetric])
paulson@14314
   672
done
paulson@14314
   673
paulson@14314
   674
lemmas hcomplex_mult_not_zeroE = hcomplex_mult_not_zero [THEN notE, standard]
paulson@14314
   675
paulson@14314
   676
lemma hcomplex_inverse_inverse: "inverse(inverse x) = (x::hcomplex)"
paulson@14314
   677
apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
paulson@14314
   678
apply (rule_tac c1 = "inverse x" in hcomplex_mult_right_cancel [THEN iffD1])
paulson@14314
   679
apply (erule hcomplex_inverse_not_zero)
paulson@14314
   680
apply (auto dest: hcomplex_inverse_not_zero)
paulson@14314
   681
done
paulson@14314
   682
declare hcomplex_inverse_inverse [simp]
paulson@14314
   683
paulson@14314
   684
lemma hcomplex_inverse_one: "inverse((1::hcomplex)) = 1"
paulson@14314
   685
apply (unfold hcomplex_one_def)
paulson@14314
   686
apply (simp (no_asm) add: hcomplex_inverse)
paulson@14314
   687
done
paulson@14314
   688
declare hcomplex_inverse_one [simp]
paulson@14314
   689
paulson@14314
   690
lemma hcomplex_minus_inverse: "inverse(-x) = -inverse(x::hcomplex)"
paulson@14314
   691
apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
paulson@14314
   692
apply (rule_tac c1 = "-x" in hcomplex_mult_right_cancel [THEN iffD1])
paulson@14314
   693
apply (force ); 
paulson@14314
   694
apply (subst hcomplex_mult_inv_left)
paulson@14314
   695
apply auto
paulson@14314
   696
done
paulson@14314
   697
paulson@14314
   698
lemma hcomplex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::hcomplex)"
paulson@14314
   699
apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
paulson@14314
   700
apply (case_tac "y = 0", simp add: HCOMPLEX_INVERSE_ZERO)
paulson@14314
   701
apply (rule_tac c1 = "x*y" in hcomplex_mult_left_cancel [THEN iffD1])
paulson@14314
   702
apply (auto simp add: hcomplex_mult_not_zero hcomplex_mult_ac)
paulson@14314
   703
apply (auto simp add: hcomplex_mult_not_zero hcomplex_mult_assoc [symmetric])
paulson@14314
   704
done
paulson@14314
   705
paulson@14314
   706
subsection{*Division*}
paulson@14314
   707
paulson@14314
   708
lemma hcomplex_times_divide1_eq: "(x::hcomplex) * (y/z) = (x*y)/z"
paulson@14314
   709
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_mult_assoc)
paulson@14314
   710
done
paulson@14314
   711
paulson@14314
   712
lemma hcomplex_times_divide2_eq: "(y/z) * (x::hcomplex) = (y*x)/z"
paulson@14314
   713
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_mult_ac)
paulson@14314
   714
done
paulson@14314
   715
paulson@14314
   716
declare hcomplex_times_divide1_eq [simp] hcomplex_times_divide2_eq [simp]
paulson@14314
   717
paulson@14314
   718
lemma hcomplex_divide_divide1_eq: "(x::hcomplex) / (y/z) = (x*z)/y"
paulson@14314
   719
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_inverse_distrib hcomplex_mult_ac)
paulson@14314
   720
done
paulson@14314
   721
paulson@14314
   722
lemma hcomplex_divide_divide2_eq: "((x::hcomplex) / y) / z = x/(y*z)"
paulson@14314
   723
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_inverse_distrib hcomplex_mult_assoc)
paulson@14314
   724
done
paulson@14314
   725
paulson@14314
   726
declare hcomplex_divide_divide1_eq [simp] hcomplex_divide_divide2_eq [simp]
paulson@14314
   727
paulson@14314
   728
(** As with multiplication, pull minus signs OUT of the / operator **)
paulson@14314
   729
paulson@14314
   730
lemma hcomplex_minus_divide_eq: "(-x) / (y::hcomplex) = - (x/y)"
paulson@14314
   731
apply (simp (no_asm) add: hcomplex_divide_def)
paulson@14314
   732
done
paulson@14314
   733
declare hcomplex_minus_divide_eq [simp]
paulson@14314
   734
paulson@14314
   735
lemma hcomplex_divide_minus_eq: "(x / -(y::hcomplex)) = - (x/y)"
paulson@14314
   736
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_minus_inverse)
paulson@14314
   737
done
paulson@14314
   738
declare hcomplex_divide_minus_eq [simp]
paulson@14314
   739
paulson@14314
   740
lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
paulson@14314
   741
apply (simp (no_asm) add: hcomplex_divide_def hcomplex_add_mult_distrib)
paulson@14314
   742
done
paulson@14314
   743
paulson@14314
   744
paulson@14314
   745
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
paulson@14314
   746
paulson@14314
   747
lemma hcomplex_of_hypreal:
paulson@14314
   748
  "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
paulson@14314
   749
      Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
paulson@14314
   750
apply (unfold hcomplex_of_hypreal_def)
paulson@14314
   751
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   752
apply auto
paulson@14314
   753
apply (ultra)
paulson@14314
   754
done
paulson@14314
   755
paulson@14314
   756
lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal"
paulson@14314
   757
apply (rule inj_onI)
paulson@14314
   758
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   759
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
   760
apply (auto simp add: hcomplex_of_hypreal)
paulson@14314
   761
done
paulson@14314
   762
paulson@14314
   763
lemma hcomplex_of_hypreal_cancel_iff: "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
paulson@14314
   764
apply (auto dest: inj_hcomplex_of_hypreal [THEN injD])
paulson@14314
   765
done
paulson@14314
   766
declare hcomplex_of_hypreal_cancel_iff [iff]
paulson@14314
   767
paulson@14314
   768
lemma hcomplex_of_hypreal_minus: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
paulson@14314
   769
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   770
apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
paulson@14314
   771
done
paulson@14314
   772
paulson@14314
   773
lemma hcomplex_of_hypreal_inverse: "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
paulson@14314
   774
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   775
apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
paulson@14314
   776
done
paulson@14314
   777
paulson@14314
   778
lemma hcomplex_of_hypreal_add: "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
paulson@14314
   779
      hcomplex_of_hypreal (x + y)"
paulson@14314
   780
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   781
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
   782
apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
paulson@14314
   783
done
paulson@14314
   784
paulson@14314
   785
lemma hcomplex_of_hypreal_diff:
paulson@14314
   786
     "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
paulson@14314
   787
      hcomplex_of_hypreal (x - y)"
paulson@14314
   788
apply (unfold hcomplex_diff_def)
paulson@14314
   789
apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
paulson@14314
   790
done
paulson@14314
   791
paulson@14314
   792
lemma hcomplex_of_hypreal_mult: "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
paulson@14314
   793
      hcomplex_of_hypreal (x * y)"
paulson@14314
   794
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   795
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
   796
apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
paulson@14314
   797
done
paulson@14314
   798
paulson@14314
   799
lemma hcomplex_of_hypreal_divide:
paulson@14314
   800
  "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
paulson@14314
   801
apply (unfold hcomplex_divide_def)
paulson@14314
   802
apply (case_tac "y=0")
paulson@14314
   803
apply (simp (no_asm_simp) add: HYPREAL_DIVISION_BY_ZERO HYPREAL_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO)
paulson@14314
   804
apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
paulson@14314
   805
apply (simp (no_asm) add: hypreal_divide_def)
paulson@14314
   806
done
paulson@14314
   807
paulson@14314
   808
lemma hcomplex_of_hypreal_one [simp]:
paulson@14314
   809
      "hcomplex_of_hypreal 1 = 1"
paulson@14314
   810
apply (unfold hcomplex_one_def)
paulson@14314
   811
apply (auto simp add: hcomplex_of_hypreal hypreal_one_num)
paulson@14314
   812
done
paulson@14314
   813
paulson@14314
   814
lemma hcomplex_of_hypreal_zero [simp]:
paulson@14314
   815
      "hcomplex_of_hypreal 0 = 0"
paulson@14314
   816
apply (unfold hcomplex_zero_def hypreal_zero_def)
paulson@14314
   817
apply (auto simp add: hcomplex_of_hypreal)
paulson@14314
   818
done
paulson@14314
   819
paulson@14314
   820
lemma hcomplex_of_hypreal_pow:
paulson@14314
   821
     "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
paulson@14314
   822
apply (induct_tac "n")
paulson@14314
   823
apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
paulson@14314
   824
done
paulson@14314
   825
paulson@14314
   826
lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
paulson@14314
   827
apply (rule_tac z = "z" in eq_Abs_hypreal)
paulson@14314
   828
apply (auto simp add: hcomplex_of_hypreal hRe)
paulson@14314
   829
done
paulson@14314
   830
declare hRe_hcomplex_of_hypreal [simp]
paulson@14314
   831
paulson@14314
   832
lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0"
paulson@14314
   833
apply (rule_tac z = "z" in eq_Abs_hypreal)
paulson@14314
   834
apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
paulson@14314
   835
done
paulson@14314
   836
declare hIm_hcomplex_of_hypreal [simp]
paulson@14314
   837
paulson@14314
   838
lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon ~= 0"
paulson@14314
   839
apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
paulson@14314
   840
done
paulson@14314
   841
declare hcomplex_of_hypreal_epsilon_not_zero [simp]
paulson@14314
   842
paulson@14314
   843
(*---------------------------------------------------------------------------*)
paulson@14314
   844
(*  Modulus (absolute value) of nonstandard complex number                   *)
paulson@14314
   845
(*---------------------------------------------------------------------------*)
paulson@14314
   846
paulson@14314
   847
lemma hcmod:
paulson@14314
   848
  "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   849
      Abs_hypreal(hyprel `` {%n. cmod (X n)})"
paulson@14314
   850
paulson@14314
   851
apply (unfold hcmod_def)
paulson@14314
   852
apply (rule_tac f = "Abs_hypreal" in arg_cong)
paulson@14314
   853
apply (auto , ultra)
paulson@14314
   854
done
paulson@14314
   855
paulson@14314
   856
lemma hcmod_zero [simp]:
paulson@14314
   857
      "hcmod(0) = 0"
paulson@14314
   858
apply (unfold hcomplex_zero_def hypreal_zero_def)
paulson@14314
   859
apply (auto simp add: hcmod)
paulson@14314
   860
done
paulson@14314
   861
paulson@14314
   862
lemma hcmod_one:
paulson@14314
   863
      "hcmod(1) = 1"
paulson@14314
   864
apply (unfold hcomplex_one_def)
paulson@14314
   865
apply (auto simp add: hcmod hypreal_one_num)
paulson@14314
   866
done
paulson@14314
   867
declare hcmod_one [simp]
paulson@14314
   868
paulson@14314
   869
lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x"
paulson@14314
   870
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   871
apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
paulson@14314
   872
done
paulson@14314
   873
declare hcmod_hcomplex_of_hypreal [simp]
paulson@14314
   874
paulson@14314
   875
lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) =
paulson@14314
   876
      hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
paulson@14314
   877
apply (simp (no_asm))
paulson@14314
   878
done
paulson@14314
   879
paulson@14314
   880
paulson@14314
   881
subsection{*Conjugation*}
paulson@14314
   882
paulson@14314
   883
lemma hcnj:
paulson@14314
   884
  "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
   885
      Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
paulson@14314
   886
paulson@14314
   887
apply (unfold hcnj_def)
paulson@14314
   888
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
   889
apply (auto , ultra)
paulson@14314
   890
done
paulson@14314
   891
paulson@14314
   892
lemma inj_hcnj: "inj hcnj"
paulson@14314
   893
apply (rule inj_onI)
paulson@14314
   894
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
   895
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
   896
apply (auto simp add: hcnj)
paulson@14314
   897
done
paulson@14314
   898
paulson@14314
   899
lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)"
paulson@14314
   900
apply (auto dest: inj_hcnj [THEN injD])
paulson@14314
   901
done
paulson@14314
   902
declare hcomplex_hcnj_cancel_iff [simp]
paulson@14314
   903
paulson@14314
   904
lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z"
paulson@14314
   905
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   906
apply (auto simp add: hcnj)
paulson@14314
   907
done
paulson@14314
   908
declare hcomplex_hcnj_hcnj [simp]
paulson@14314
   909
paulson@14314
   910
lemma hcomplex_hcnj_hcomplex_of_hypreal: "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
paulson@14314
   911
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
   912
apply (auto simp add: hcnj hcomplex_of_hypreal)
paulson@14314
   913
done
paulson@14314
   914
declare hcomplex_hcnj_hcomplex_of_hypreal [simp]
paulson@14314
   915
paulson@14314
   916
lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z"
paulson@14314
   917
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   918
apply (auto simp add: hcnj hcmod)
paulson@14314
   919
done
paulson@14314
   920
declare hcomplex_hmod_hcnj [simp]
paulson@14314
   921
paulson@14314
   922
lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
paulson@14314
   923
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   924
apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus)
paulson@14314
   925
done
paulson@14314
   926
paulson@14314
   927
lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
paulson@14314
   928
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   929
apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse)
paulson@14314
   930
done
paulson@14314
   931
paulson@14314
   932
lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
paulson@14314
   933
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   934
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   935
apply (auto simp add: hcnj hcomplex_add complex_cnj_add)
paulson@14314
   936
done
paulson@14314
   937
paulson@14314
   938
lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
paulson@14314
   939
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   940
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   941
apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff)
paulson@14314
   942
done
paulson@14314
   943
paulson@14314
   944
lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
paulson@14314
   945
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   946
apply (rule_tac z = "w" in eq_Abs_hcomplex)
paulson@14314
   947
apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult)
paulson@14314
   948
done
paulson@14314
   949
paulson@14314
   950
lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
paulson@14314
   951
apply (unfold hcomplex_divide_def)
paulson@14314
   952
apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse)
paulson@14314
   953
done
paulson@14314
   954
paulson@14314
   955
lemma hcnj_one: "hcnj 1 = 1"
paulson@14314
   956
apply (unfold hcomplex_one_def)
paulson@14314
   957
apply (simp (no_asm) add: hcnj)
paulson@14314
   958
done
paulson@14314
   959
declare hcnj_one [simp]
paulson@14314
   960
paulson@14314
   961
lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
paulson@14314
   962
apply (induct_tac "n")
paulson@14314
   963
apply (auto simp add: hcomplex_hcnj_mult)
paulson@14314
   964
done
paulson@14314
   965
paulson@14314
   966
(* MOVE to NSComplexBin
paulson@14314
   967
Goal "z + hcnj z =
paulson@14314
   968
      hcomplex_of_hypreal (2 * hRe(z))"
paulson@14314
   969
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
paulson@14314
   970
by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
paulson@14314
   971
    hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
paulson@14314
   972
qed "hcomplex_add_hcnj";
paulson@14314
   973
paulson@14314
   974
Goal "z - hcnj z = \
paulson@14314
   975
\     hcomplex_of_hypreal (hypreal_of_real 2 * hIm(z)) * iii";
paulson@14314
   976
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
paulson@14314
   977
by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
paulson@14314
   978
    hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
paulson@14314
   979
    complex_diff_cnj,iii_def,hcomplex_mult]));
paulson@14314
   980
qed "hcomplex_diff_hcnj";
paulson@14314
   981
*)
paulson@14314
   982
paulson@14314
   983
lemma hcomplex_hcnj_zero:
paulson@14314
   984
      "hcnj 0 = 0"
paulson@14314
   985
apply (unfold hcomplex_zero_def)
paulson@14314
   986
apply (auto simp add: hcnj)
paulson@14314
   987
done
paulson@14314
   988
declare hcomplex_hcnj_zero [simp]
paulson@14314
   989
paulson@14314
   990
lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)"
paulson@14314
   991
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   992
apply (auto simp add: hcomplex_zero_def hcnj)
paulson@14314
   993
done
paulson@14314
   994
declare hcomplex_hcnj_zero_iff [iff]
paulson@14314
   995
paulson@14314
   996
lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
paulson@14314
   997
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
   998
apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj two_eq_Suc_Suc)
paulson@14314
   999
done
paulson@14314
  1000
paulson@14314
  1001
paulson@14314
  1002
(*---------------------------------------------------------------------------*)
paulson@14314
  1003
(*  some algebra etc.                                                        *)
paulson@14314
  1004
(*---------------------------------------------------------------------------*)
paulson@14314
  1005
paulson@14314
  1006
lemma hcomplex_mult_zero_iff: "(x*y = (0::hcomplex)) = (x = 0 | y = 0)"
paulson@14314
  1007
apply auto
paulson@14314
  1008
apply (auto intro: ccontr dest: hcomplex_mult_not_zero)
paulson@14314
  1009
done
paulson@14314
  1010
declare hcomplex_mult_zero_iff [simp]
paulson@14314
  1011
paulson@14314
  1012
lemma hcomplex_add_left_cancel_zero: "(x + y = x) = (y = (0::hcomplex))"
paulson@14314
  1013
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1014
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1015
apply (auto simp add: hcomplex_add hcomplex_zero_def)
paulson@14314
  1016
done
paulson@14314
  1017
declare hcomplex_add_left_cancel_zero [simp]
paulson@14314
  1018
paulson@14314
  1019
lemma hcomplex_diff_mult_distrib:
paulson@14314
  1020
      "((z1::hcomplex) - z2) * w = (z1 * w) - (z2 * w)"
paulson@14314
  1021
apply (unfold hcomplex_diff_def)
paulson@14314
  1022
apply (simp (no_asm) add: hcomplex_add_mult_distrib)
paulson@14314
  1023
done
paulson@14314
  1024
paulson@14314
  1025
lemma hcomplex_diff_mult_distrib2:
paulson@14314
  1026
      "(w::hcomplex) * (z1 - z2) = (w * z1) - (w * z2)"
paulson@14314
  1027
apply (unfold hcomplex_diff_def)
paulson@14314
  1028
apply (simp (no_asm) add: hcomplex_add_mult_distrib2)
paulson@14314
  1029
done
paulson@14314
  1030
paulson@14314
  1031
(*---------------------------------------------------------------------------*)
paulson@14314
  1032
(*  More theorems about hcmod                                                *)
paulson@14314
  1033
(*---------------------------------------------------------------------------*)
paulson@14314
  1034
paulson@14314
  1035
lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
paulson@14314
  1036
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1037
apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num)
paulson@14314
  1038
done
paulson@14314
  1039
declare hcomplex_hcmod_eq_zero_cancel [simp]
paulson@14314
  1040
paulson@14314
  1041
(* not proved already? strange! *)
paulson@14314
  1042
lemma hypreal_of_nat_le_iff:
paulson@14314
  1043
      "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
paulson@14314
  1044
apply (unfold hypreal_le_def)
paulson@14314
  1045
apply auto
paulson@14314
  1046
done
paulson@14314
  1047
declare hypreal_of_nat_le_iff [simp]
paulson@14314
  1048
paulson@14314
  1049
lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
paulson@14314
  1050
apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
paulson@14314
  1051
         del: hypreal_of_nat_zero)
paulson@14314
  1052
done
paulson@14314
  1053
declare hypreal_of_nat_ge_zero [simp]
paulson@14314
  1054
paulson@14314
  1055
declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
paulson@14314
  1056
paulson@14314
  1057
lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
paulson@14314
  1058
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1059
apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
paulson@14314
  1060
done
paulson@14314
  1061
declare hypreal_of_hypnat_ge_zero [simp]
paulson@14314
  1062
paulson@14314
  1063
declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
paulson@14314
  1064
paulson@14314
  1065
lemma hcmod_hcomplex_of_hypreal_of_nat: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
paulson@14314
  1066
apply auto
paulson@14314
  1067
done
paulson@14314
  1068
declare hcmod_hcomplex_of_hypreal_of_nat [simp]
paulson@14314
  1069
paulson@14314
  1070
lemma hcmod_hcomplex_of_hypreal_of_hypnat: "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
paulson@14314
  1071
apply auto
paulson@14314
  1072
done
paulson@14314
  1073
declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
paulson@14314
  1074
paulson@14314
  1075
lemma hcmod_minus: "hcmod (-x) = hcmod(x)"
paulson@14314
  1076
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1077
apply (auto simp add: hcmod hcomplex_minus)
paulson@14314
  1078
done
paulson@14314
  1079
declare hcmod_minus [simp]
paulson@14314
  1080
paulson@14314
  1081
lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
paulson@14314
  1082
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1083
apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj two_eq_Suc_Suc)
paulson@14314
  1084
done
paulson@14314
  1085
paulson@14314
  1086
lemma hcmod_ge_zero: "(0::hypreal) <= hcmod x"
paulson@14314
  1087
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1088
apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
paulson@14314
  1089
done
paulson@14314
  1090
declare hcmod_ge_zero [simp]
paulson@14314
  1091
paulson@14314
  1092
lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x"
paulson@14314
  1093
apply (auto intro: hrabs_eqI1)
paulson@14314
  1094
done
paulson@14314
  1095
declare hrabs_hcmod_cancel [simp]
paulson@14314
  1096
paulson@14314
  1097
lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
paulson@14314
  1098
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1099
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1100
apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
paulson@14314
  1101
done
paulson@14314
  1102
paulson@14314
  1103
lemma hcmod_add_squared_eq:
paulson@14314
  1104
     "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
paulson@14314
  1105
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1106
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1107
apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
paulson@14314
  1108
                      two_eq_Suc_Suc realpow_two [symmetric] 
paulson@14314
  1109
                 simp del: realpow_Suc)
paulson@14314
  1110
apply (auto simp add: two_eq_Suc_Suc [symmetric] complex_mod_add_squared_eq
paulson@14314
  1111
                 hypreal_add [symmetric] hypreal_mult [symmetric] 
paulson@14314
  1112
                 hypreal_of_real_def [symmetric])
paulson@14314
  1113
done
paulson@14314
  1114
paulson@14314
  1115
lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) <= hcmod(x * hcnj y)"
paulson@14314
  1116
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1117
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1118
apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
paulson@14314
  1119
done
paulson@14314
  1120
declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
paulson@14314
  1121
paulson@14314
  1122
lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) <= hcmod(x * y)"
paulson@14314
  1123
apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
paulson@14314
  1124
apply (simp add: hcmod_mult)
paulson@14314
  1125
done
paulson@14314
  1126
declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
paulson@14314
  1127
paulson@14314
  1128
lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 <= (hcmod(x) + hcmod(y)) ^ 2"
paulson@14314
  1129
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1130
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1131
apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
paulson@14314
  1132
                      hypreal_le realpow_two [symmetric] two_eq_Suc_Suc
paulson@14314
  1133
            simp del: realpow_Suc)
paulson@14314
  1134
apply (simp (no_asm) add: two_eq_Suc_Suc [symmetric])
paulson@14314
  1135
done
paulson@14314
  1136
declare hcmod_triangle_squared [simp]
paulson@14314
  1137
paulson@14314
  1138
lemma hcmod_triangle_ineq: "hcmod (x + y) <= hcmod(x) + hcmod(y)"
paulson@14314
  1139
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1140
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1141
apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
paulson@14314
  1142
done
paulson@14314
  1143
declare hcmod_triangle_ineq [simp]
paulson@14314
  1144
paulson@14314
  1145
lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a"
paulson@14314
  1146
apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
paulson@14314
  1147
apply (simp add: hypreal_add_ac)
paulson@14314
  1148
done
paulson@14314
  1149
declare hcmod_triangle_ineq2 [simp]
paulson@14314
  1150
paulson@14314
  1151
lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
paulson@14314
  1152
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1153
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1154
apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute)
paulson@14314
  1155
done
paulson@14314
  1156
paulson@14314
  1157
lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
paulson@14314
  1158
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1159
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1160
apply (rule_tac z = "r" in eq_Abs_hypreal)
paulson@14314
  1161
apply (rule_tac z = "s" in eq_Abs_hypreal)
paulson@14314
  1162
apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less)
paulson@14314
  1163
apply ultra
paulson@14314
  1164
apply (auto intro: complex_mod_add_less)
paulson@14314
  1165
done
paulson@14314
  1166
paulson@14314
  1167
lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
paulson@14314
  1168
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1169
apply (rule_tac z = "y" in eq_Abs_hcomplex)
paulson@14314
  1170
apply (rule_tac z = "r" in eq_Abs_hypreal)
paulson@14314
  1171
apply (rule_tac z = "s" in eq_Abs_hypreal)
paulson@14314
  1172
apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult)
paulson@14314
  1173
apply ultra
paulson@14314
  1174
apply (auto intro: complex_mod_mult_less)
paulson@14314
  1175
done
paulson@14314
  1176
paulson@14314
  1177
lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) <= hcmod(a + b)"
paulson@14314
  1178
apply (rule_tac z = "a" in eq_Abs_hcomplex)
paulson@14314
  1179
apply (rule_tac z = "b" in eq_Abs_hcomplex)
paulson@14314
  1180
apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
paulson@14314
  1181
done
paulson@14314
  1182
declare hcmod_diff_ineq [simp]
paulson@14314
  1183
paulson@14314
  1184
paulson@14314
  1185
paulson@14314
  1186
subsection{*A Few Nonlinear Theorems*}
paulson@14314
  1187
paulson@14314
  1188
lemma hcpow:
paulson@14314
  1189
  "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
paulson@14314
  1190
   Abs_hypnat(hypnatrel``{%n. Y n}) =
paulson@14314
  1191
   Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
paulson@14314
  1192
apply (unfold hcpow_def)
paulson@14314
  1193
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
  1194
apply (auto , ultra)
paulson@14314
  1195
done
paulson@14314
  1196
paulson@14314
  1197
lemma hcomplex_of_hypreal_hyperpow: "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
paulson@14314
  1198
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1199
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1200
apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
paulson@14314
  1201
done
paulson@14314
  1202
paulson@14314
  1203
lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
paulson@14314
  1204
apply (induct_tac "n")
paulson@14314
  1205
apply (auto simp add: hcmod_mult)
paulson@14314
  1206
done
paulson@14314
  1207
paulson@14314
  1208
lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
paulson@14314
  1209
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1210
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1211
apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
paulson@14314
  1212
done
paulson@14314
  1213
paulson@14314
  1214
lemma hcomplexpow_minus: "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
paulson@14314
  1215
apply (induct_tac "n")
paulson@14314
  1216
apply auto
paulson@14314
  1217
done
paulson@14314
  1218
paulson@14314
  1219
lemma hcpow_minus: "(-x::hcomplex) hcpow n =
paulson@14314
  1220
      (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
paulson@14314
  1221
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1222
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1223
apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
paulson@14314
  1224
apply ultra
paulson@14314
  1225
apply (auto simp add: complexpow_minus) 
paulson@14314
  1226
apply ultra
paulson@14314
  1227
done
paulson@14314
  1228
paulson@14314
  1229
lemma hccomplex_inverse_minus: "inverse(-x) = - inverse (x::hcomplex)"
paulson@14314
  1230
apply (rule_tac z = "x" in eq_Abs_hcomplex)
paulson@14314
  1231
apply (auto simp add: hcomplex_inverse hcomplex_minus complex_inverse_minus)
paulson@14314
  1232
done
paulson@14314
  1233
paulson@14314
  1234
lemma hcomplex_div_one: "x / (1::hcomplex) = x"
paulson@14314
  1235
apply (unfold hcomplex_divide_def)
paulson@14314
  1236
apply (simp (no_asm))
paulson@14314
  1237
done
paulson@14314
  1238
declare hcomplex_div_one [simp]
paulson@14314
  1239
paulson@14314
  1240
lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
paulson@14314
  1241
apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
paulson@14314
  1242
apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
paulson@14314
  1243
apply (auto simp add: hcmod_mult [symmetric])
paulson@14314
  1244
done
paulson@14314
  1245
paulson@14314
  1246
lemma hcmod_divide:
paulson@14314
  1247
      "hcmod(x/y) = hcmod(x)/(hcmod y)"
paulson@14314
  1248
apply (unfold hcomplex_divide_def hypreal_divide_def)
paulson@14314
  1249
apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse)
paulson@14314
  1250
done
paulson@14314
  1251
paulson@14314
  1252
lemma hcomplex_inverse_divide:
paulson@14314
  1253
      "inverse(x/y) = y/(x::hcomplex)"
paulson@14314
  1254
apply (unfold hcomplex_divide_def)
paulson@14314
  1255
apply (auto simp add: hcomplex_inverse_distrib hcomplex_mult_commute)
paulson@14314
  1256
done
paulson@14314
  1257
declare hcomplex_inverse_divide [simp]
paulson@14314
  1258
paulson@14314
  1259
lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"
paulson@14314
  1260
apply (induct_tac "n")
paulson@14314
  1261
apply (auto simp add: hcomplex_mult_ac)
paulson@14314
  1262
done
paulson@14314
  1263
paulson@14314
  1264
lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
paulson@14314
  1265
apply (rule_tac z = "r" in eq_Abs_hcomplex)
paulson@14314
  1266
apply (rule_tac z = "s" in eq_Abs_hcomplex)
paulson@14314
  1267
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1268
apply (auto simp add: hcpow hypreal_mult hcomplex_mult complexpow_mult)
paulson@14314
  1269
done
paulson@14314
  1270
paulson@14314
  1271
lemma hcomplexpow_zero: "(0::hcomplex) ^ (Suc n) = 0"
paulson@14314
  1272
apply auto
paulson@14314
  1273
done
paulson@14314
  1274
declare hcomplexpow_zero [simp]
paulson@14314
  1275
paulson@14314
  1276
lemma hcpow_zero:
paulson@14314
  1277
   "0 hcpow (n + 1) = 0"
paulson@14314
  1278
apply (unfold hcomplex_zero_def hypnat_one_def)
paulson@14314
  1279
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1280
apply (auto simp add: hcpow hypnat_add)
paulson@14314
  1281
done
paulson@14314
  1282
declare hcpow_zero [simp]
paulson@14314
  1283
paulson@14314
  1284
lemma hcpow_zero2:
paulson@14314
  1285
   "0 hcpow (hSuc n) = 0"
paulson@14314
  1286
apply (unfold hSuc_def)
paulson@14314
  1287
apply (simp (no_asm))
paulson@14314
  1288
done
paulson@14314
  1289
declare hcpow_zero2 [simp]
paulson@14314
  1290
paulson@14314
  1291
lemma hcomplexpow_not_zero [rule_format (no_asm)]: "r ~= (0::hcomplex) --> r ^ n ~= 0"
paulson@14314
  1292
apply (induct_tac "n")
paulson@14314
  1293
apply (auto simp add: hcomplex_mult_not_zero)
paulson@14314
  1294
done
paulson@14314
  1295
declare hcomplexpow_not_zero [simp]
paulson@14314
  1296
declare hcomplexpow_not_zero [intro]
paulson@14314
  1297
paulson@14314
  1298
lemma hcpow_not_zero: "r ~= 0 ==> r hcpow n ~= (0::hcomplex)"
paulson@14314
  1299
apply (rule_tac z = "r" in eq_Abs_hcomplex)
paulson@14314
  1300
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1301
apply (auto simp add: hcpow hcomplex_zero_def)
paulson@14314
  1302
apply ultra
paulson@14314
  1303
apply (auto dest: complexpow_zero_zero)
paulson@14314
  1304
done
paulson@14314
  1305
declare hcpow_not_zero [simp]
paulson@14314
  1306
declare hcpow_not_zero [intro]
paulson@14314
  1307
paulson@14314
  1308
lemma hcomplexpow_zero_zero: "r ^ n = (0::hcomplex) ==> r = 0"
paulson@14314
  1309
apply (blast intro: ccontr dest: hcomplexpow_not_zero)
paulson@14314
  1310
done
paulson@14314
  1311
paulson@14314
  1312
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
paulson@14314
  1313
apply (blast intro: ccontr dest: hcpow_not_zero)
paulson@14314
  1314
done
paulson@14314
  1315
paulson@14314
  1316
lemma hcomplex_i_mult_eq: "iii * iii = - 1"
paulson@14314
  1317
apply (unfold iii_def)
paulson@14314
  1318
apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus)
paulson@14314
  1319
done
paulson@14314
  1320
declare hcomplex_i_mult_eq [simp]
paulson@14314
  1321
paulson@14314
  1322
lemma hcomplexpow_i_squared: "iii ^ 2 = - 1"
paulson@14314
  1323
apply (simp (no_asm) add: two_eq_Suc_Suc)
paulson@14314
  1324
done
paulson@14314
  1325
declare hcomplexpow_i_squared [simp]
paulson@14314
  1326
paulson@14314
  1327
lemma hcomplex_i_not_zero: "iii ~= 0"
paulson@14314
  1328
apply (unfold iii_def hcomplex_zero_def)
paulson@14314
  1329
apply auto
paulson@14314
  1330
done
paulson@14314
  1331
declare hcomplex_i_not_zero [simp]
paulson@14314
  1332
paulson@14314
  1333
lemma hcomplex_mult_eq_zero_cancel1: "x * y ~= (0::hcomplex) ==> x ~= 0"
paulson@14314
  1334
apply auto
paulson@14314
  1335
done
paulson@14314
  1336
paulson@14314
  1337
lemma hcomplex_mult_eq_zero_cancel2: "x * y ~= (0::hcomplex) ==> y ~= 0"
paulson@14314
  1338
apply auto
paulson@14314
  1339
done
paulson@14314
  1340
paulson@14314
  1341
lemma hcomplex_mult_not_eq_zero_iff: "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
paulson@14314
  1342
apply auto
paulson@14314
  1343
done
paulson@14314
  1344
declare hcomplex_mult_not_eq_zero_iff [iff]
paulson@14314
  1345
paulson@14314
  1346
lemma hcomplex_divide:
paulson@14314
  1347
  "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
paulson@14314
  1348
   Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
paulson@14314
  1349
apply (unfold hcomplex_divide_def complex_divide_def)
paulson@14314
  1350
apply (auto simp add: hcomplex_inverse hcomplex_mult)
paulson@14314
  1351
done
paulson@14314
  1352
paulson@14314
  1353
paulson@14314
  1354
subsection{*The Function @{term hsgn}*}
paulson@14314
  1355
paulson@14314
  1356
lemma hsgn:
paulson@14314
  1357
  "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
  1358
      Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
paulson@14314
  1359
apply (unfold hsgn_def)
paulson@14314
  1360
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
  1361
apply (auto , ultra)
paulson@14314
  1362
done
paulson@14314
  1363
paulson@14314
  1364
lemma hsgn_zero: "hsgn 0 = 0"
paulson@14314
  1365
apply (unfold hcomplex_zero_def)
paulson@14314
  1366
apply (simp (no_asm) add: hsgn)
paulson@14314
  1367
done
paulson@14314
  1368
declare hsgn_zero [simp]
paulson@14314
  1369
paulson@14314
  1370
paulson@14314
  1371
lemma hsgn_one: "hsgn 1 = 1"
paulson@14314
  1372
apply (unfold hcomplex_one_def)
paulson@14314
  1373
apply (simp (no_asm) add: hsgn)
paulson@14314
  1374
done
paulson@14314
  1375
declare hsgn_one [simp]
paulson@14314
  1376
paulson@14314
  1377
lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
paulson@14314
  1378
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1379
apply (auto simp add: hsgn hcomplex_minus sgn_minus)
paulson@14314
  1380
done
paulson@14314
  1381
paulson@14314
  1382
lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
paulson@14314
  1383
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1384
apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
paulson@14314
  1385
done
paulson@14314
  1386
paulson@14314
  1387
lemma lemma_hypreal_P_EX2: "(EX (x::hypreal) y. P x y) =
paulson@14314
  1388
      (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
paulson@14314
  1389
apply auto
paulson@14314
  1390
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1391
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1392
apply auto
paulson@14314
  1393
done
paulson@14314
  1394
paulson@14314
  1395
lemma complex_split2: "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
paulson@14314
  1396
apply (blast intro: complex_split)
paulson@14314
  1397
done
paulson@14314
  1398
paulson@14314
  1399
(* Interesting proof! *)
paulson@14314
  1400
lemma hcomplex_split: "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
paulson@14314
  1401
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1402
apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
paulson@14314
  1403
apply (cut_tac z = "x" in complex_split2)
paulson@14314
  1404
apply (drule choice , safe)+
paulson@14314
  1405
apply (rule_tac x = "f" in exI)
paulson@14314
  1406
apply (rule_tac x = "fa" in exI)
paulson@14314
  1407
apply auto
paulson@14314
  1408
done
paulson@14314
  1409
paulson@14314
  1410
lemma hRe_hcomplex_i: "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
paulson@14314
  1411
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1412
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1413
apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
paulson@14314
  1414
done
paulson@14314
  1415
declare hRe_hcomplex_i [simp]
paulson@14314
  1416
paulson@14314
  1417
lemma hIm_hcomplex_i: "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
paulson@14314
  1418
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1419
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1420
apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
paulson@14314
  1421
done
paulson@14314
  1422
declare hIm_hcomplex_i [simp]
paulson@14314
  1423
paulson@14314
  1424
lemma hcmod_i: "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
paulson@14314
  1425
      ( *f* sqrt) (x ^ 2 + y ^ 2)"
paulson@14314
  1426
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1427
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1428
apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i two_eq_Suc_Suc)
paulson@14314
  1429
done
paulson@14314
  1430
paulson@14314
  1431
lemma hcomplex_eq_hRe_eq:
paulson@14314
  1432
     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
paulson@14314
  1433
      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
paulson@14314
  1434
       ==> xa = xb"
paulson@14314
  1435
apply (unfold iii_def)
paulson@14314
  1436
apply (rule_tac z = "xa" in eq_Abs_hypreal)
paulson@14314
  1437
apply (rule_tac z = "ya" in eq_Abs_hypreal)
paulson@14314
  1438
apply (rule_tac z = "xb" in eq_Abs_hypreal)
paulson@14314
  1439
apply (rule_tac z = "yb" in eq_Abs_hypreal)
paulson@14314
  1440
apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
paulson@14314
  1441
apply (ultra)
paulson@14314
  1442
done
paulson@14314
  1443
paulson@14314
  1444
lemma hcomplex_eq_hIm_eq:
paulson@14314
  1445
     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
paulson@14314
  1446
      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
paulson@14314
  1447
       ==> ya = yb"
paulson@14314
  1448
apply (unfold iii_def)
paulson@14314
  1449
apply (rule_tac z = "xa" in eq_Abs_hypreal)
paulson@14314
  1450
apply (rule_tac z = "ya" in eq_Abs_hypreal)
paulson@14314
  1451
apply (rule_tac z = "xb" in eq_Abs_hypreal)
paulson@14314
  1452
apply (rule_tac z = "yb" in eq_Abs_hypreal)
paulson@14314
  1453
apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
paulson@14314
  1454
apply (ultra)
paulson@14314
  1455
done
paulson@14314
  1456
paulson@14314
  1457
lemma hcomplex_eq_cancel_iff: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
paulson@14314
  1458
       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
paulson@14314
  1459
      ((xa = xb) & (ya = yb))"
paulson@14314
  1460
apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
paulson@14314
  1461
done
paulson@14314
  1462
declare hcomplex_eq_cancel_iff [simp]
paulson@14314
  1463
paulson@14314
  1464
lemma hcomplex_eq_cancel_iffA: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
paulson@14314
  1465
       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"
paulson@14314
  1466
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1467
done
paulson@14314
  1468
declare hcomplex_eq_cancel_iffA [iff]
paulson@14314
  1469
paulson@14314
  1470
lemma hcomplex_eq_cancel_iffB: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
paulson@14314
  1471
       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
paulson@14314
  1472
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1473
done
paulson@14314
  1474
declare hcomplex_eq_cancel_iffB [iff]
paulson@14314
  1475
paulson@14314
  1476
lemma hcomplex_eq_cancel_iffC: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
paulson@14314
  1477
       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
paulson@14314
  1478
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1479
done
paulson@14314
  1480
declare hcomplex_eq_cancel_iffC [iff]
paulson@14314
  1481
paulson@14314
  1482
lemma hcomplex_eq_cancel_iff2: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
paulson@14314
  1483
      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
paulson@14314
  1484
apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff)
paulson@14314
  1485
apply (simp del: hcomplex_eq_cancel_iff)
paulson@14314
  1486
done
paulson@14314
  1487
declare hcomplex_eq_cancel_iff2 [simp]
paulson@14314
  1488
paulson@14314
  1489
lemma hcomplex_eq_cancel_iff2a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
paulson@14314
  1490
      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
paulson@14314
  1491
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1492
done
paulson@14314
  1493
declare hcomplex_eq_cancel_iff2a [simp]
paulson@14314
  1494
paulson@14314
  1495
lemma hcomplex_eq_cancel_iff3: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
paulson@14314
  1496
      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
paulson@14314
  1497
apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff)
paulson@14314
  1498
apply (simp del: hcomplex_eq_cancel_iff)
paulson@14314
  1499
done
paulson@14314
  1500
declare hcomplex_eq_cancel_iff3 [simp]
paulson@14314
  1501
paulson@14314
  1502
lemma hcomplex_eq_cancel_iff3a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
paulson@14314
  1503
      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
paulson@14314
  1504
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1505
done
paulson@14314
  1506
declare hcomplex_eq_cancel_iff3a [simp]
paulson@14314
  1507
paulson@14314
  1508
lemma hcomplex_split_hRe_zero:
paulson@14314
  1509
     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
paulson@14314
  1510
      ==> x = 0"
paulson@14314
  1511
apply (unfold iii_def)
paulson@14314
  1512
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1513
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1514
apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
paulson@14314
  1515
apply ultra
paulson@14314
  1516
apply (auto simp add: complex_split_Re_zero)
paulson@14314
  1517
done
paulson@14314
  1518
paulson@14314
  1519
lemma hcomplex_split_hIm_zero:
paulson@14314
  1520
     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
paulson@14314
  1521
      ==> y = 0"
paulson@14314
  1522
apply (unfold iii_def)
paulson@14314
  1523
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1524
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1525
apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
paulson@14314
  1526
apply ultra
paulson@14314
  1527
apply (auto simp add: complex_split_Im_zero)
paulson@14314
  1528
done
paulson@14314
  1529
paulson@14314
  1530
lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z"
paulson@14314
  1531
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1532
apply (auto simp add: hsgn hcmod hRe hypreal_divide)
paulson@14314
  1533
done
paulson@14314
  1534
declare hRe_hsgn [simp]
paulson@14314
  1535
paulson@14314
  1536
lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z"
paulson@14314
  1537
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1538
apply (auto simp add: hsgn hcmod hIm hypreal_divide)
paulson@14314
  1539
done
paulson@14314
  1540
declare hIm_hsgn [simp]
paulson@14314
  1541
paulson@14314
  1542
lemma real_two_squares_add_zero_iff: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
paulson@14314
  1543
apply (auto intro: real_sum_squares_cancel)
paulson@14314
  1544
done
paulson@14314
  1545
declare real_two_squares_add_zero_iff [simp]
paulson@14314
  1546
paulson@14314
  1547
lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
paulson@14314
  1548
      hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
paulson@14314
  1549
      iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
paulson@14314
  1550
apply (rule_tac z = "x" in eq_Abs_hypreal)
paulson@14314
  1551
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1552
apply (auto 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 two_eq_Suc_Suc)
paulson@14314
  1553
done
paulson@14314
  1554
paulson@14314
  1555
lemma hRe_mult_i_eq:
paulson@14314
  1556
    "hRe (iii * hcomplex_of_hypreal y) = 0"
paulson@14314
  1557
apply (unfold iii_def)
paulson@14314
  1558
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1559
apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
paulson@14314
  1560
done
paulson@14314
  1561
declare hRe_mult_i_eq [simp]
paulson@14314
  1562
paulson@14314
  1563
lemma hIm_mult_i_eq:
paulson@14314
  1564
    "hIm (iii * hcomplex_of_hypreal y) = y"
paulson@14314
  1565
apply (unfold iii_def)
paulson@14314
  1566
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1567
apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
paulson@14314
  1568
done
paulson@14314
  1569
declare hIm_mult_i_eq [simp]
paulson@14314
  1570
paulson@14314
  1571
lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
paulson@14314
  1572
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1573
apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
paulson@14314
  1574
done
paulson@14314
  1575
declare hcmod_mult_i [simp]
paulson@14314
  1576
paulson@14314
  1577
lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
paulson@14314
  1578
apply (auto simp add: hcomplex_mult_commute)
paulson@14314
  1579
done
paulson@14314
  1580
declare hcmod_mult_i2 [simp]
paulson@14314
  1581
paulson@14314
  1582
(*---------------------------------------------------------------------------*)
paulson@14314
  1583
(*  harg                                                                     *)
paulson@14314
  1584
(*---------------------------------------------------------------------------*)
paulson@14314
  1585
paulson@14314
  1586
lemma harg:
paulson@14314
  1587
  "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
paulson@14314
  1588
      Abs_hypreal(hyprel `` {%n. arg (X n)})"
paulson@14314
  1589
paulson@14314
  1590
apply (unfold harg_def)
paulson@14314
  1591
apply (rule_tac f = "Abs_hypreal" in arg_cong)
paulson@14314
  1592
apply (auto , ultra)
paulson@14314
  1593
done
paulson@14314
  1594
paulson@14314
  1595
lemma cos_harg_i_mult_zero: "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
paulson@14314
  1596
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1597
apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
paulson@14314
  1598
apply (ultra)
paulson@14314
  1599
done
paulson@14314
  1600
declare cos_harg_i_mult_zero [simp]
paulson@14314
  1601
paulson@14314
  1602
lemma cos_harg_i_mult_zero2: "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
paulson@14314
  1603
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1604
apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
paulson@14314
  1605
apply (ultra)
paulson@14314
  1606
done
paulson@14314
  1607
declare cos_harg_i_mult_zero2 [simp]
paulson@14314
  1608
paulson@14314
  1609
lemma hcomplex_of_hypreal_not_zero_iff: "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
paulson@14314
  1610
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1611
apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
paulson@14314
  1612
done
paulson@14314
  1613
declare hcomplex_of_hypreal_not_zero_iff [simp]
paulson@14314
  1614
paulson@14314
  1615
lemma hcomplex_of_hypreal_zero_iff: "(hcomplex_of_hypreal y = 0) = (y = 0)"
paulson@14314
  1616
apply (rule_tac z = "y" in eq_Abs_hypreal)
paulson@14314
  1617
apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
paulson@14314
  1618
done
paulson@14314
  1619
declare hcomplex_of_hypreal_zero_iff [simp]
paulson@14314
  1620
paulson@14314
  1621
lemma cos_harg_i_mult_zero3: "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
paulson@14314
  1622
apply (cut_tac x = "y" and y = "0" in hypreal_linear)
paulson@14314
  1623
apply auto
paulson@14314
  1624
done
paulson@14314
  1625
declare cos_harg_i_mult_zero3 [simp]
paulson@14314
  1626
paulson@14314
  1627
(*---------------------------------------------------------------------------*)
paulson@14314
  1628
(* Polar form for nonstandard complex numbers                                 *)
paulson@14314
  1629
(*---------------------------------------------------------------------------*)
paulson@14314
  1630
paulson@14314
  1631
lemma complex_split_polar2: "ALL n. EX r a. (z n) = complex_of_real r *
paulson@14314
  1632
      (complex_of_real(cos a) + ii * complex_of_real(sin a))"
paulson@14314
  1633
apply (blast intro: complex_split_polar)
paulson@14314
  1634
done
paulson@14314
  1635
paulson@14314
  1636
lemma hcomplex_split_polar:
paulson@14314
  1637
  "EX r a. z = hcomplex_of_hypreal r *
paulson@14314
  1638
   (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
paulson@14314
  1639
apply (rule_tac z = "z" in eq_Abs_hcomplex)
paulson@14314
  1640
apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
paulson@14314
  1641
apply (cut_tac z = "x" in complex_split_polar2)
paulson@14314
  1642
apply (drule choice , safe)+
paulson@14314
  1643
apply (rule_tac x = "f" in exI)
paulson@14314
  1644
apply (rule_tac x = "fa" in exI)
paulson@14314
  1645
apply auto
paulson@14314
  1646
done
paulson@14314
  1647
paulson@14314
  1648
lemma hcis:
paulson@14314
  1649
  "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
paulson@14314
  1650
      Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
paulson@14314
  1651
apply (unfold hcis_def)
paulson@14314
  1652
apply (rule_tac f = "Abs_hcomplex" in arg_cong)
paulson@14314
  1653
apply auto
paulson@14314
  1654
apply (ultra)
paulson@14314
  1655
done
paulson@14314
  1656
paulson@14314
  1657
lemma hcis_eq:
paulson@14314
  1658
   "hcis a =
paulson@14314
  1659
    (hcomplex_of_hypreal(( *f* cos) a) +
paulson@14314
  1660
    iii * hcomplex_of_hypreal(( *f* sin) a))"
paulson@14314
  1661
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1662
apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
paulson@14314
  1663
done
paulson@14314
  1664
paulson@14314
  1665
lemma hrcis:
paulson@14314
  1666
  "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
paulson@14314
  1667
      Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
paulson@14314
  1668
apply (unfold hrcis_def)
paulson@14314
  1669
apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
paulson@14314
  1670
done
paulson@14314
  1671
paulson@14314
  1672
lemma hrcis_Ex: "EX r a. z = hrcis r a"
paulson@14314
  1673
apply (simp (no_asm) add: hrcis_def hcis_eq)
paulson@14314
  1674
apply (rule hcomplex_split_polar)
paulson@14314
  1675
done
paulson@14314
  1676
paulson@14314
  1677
lemma hRe_hcomplex_polar: "hRe(hcomplex_of_hypreal r *
paulson@14314
  1678
      (hcomplex_of_hypreal(( *f* cos) a) +
paulson@14314
  1679
       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
paulson@14314
  1680
apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
paulson@14314
  1681
done
paulson@14314
  1682
declare hRe_hcomplex_polar [simp]
paulson@14314
  1683
paulson@14314
  1684
lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a"
paulson@14314
  1685
apply (unfold hrcis_def)
paulson@14314
  1686
apply (auto simp add: hcis_eq)
paulson@14314
  1687
done
paulson@14314
  1688
declare hRe_hrcis [simp]
paulson@14314
  1689
paulson@14314
  1690
lemma hIm_hcomplex_polar: "hIm(hcomplex_of_hypreal r *
paulson@14314
  1691
      (hcomplex_of_hypreal(( *f* cos) a) +
paulson@14314
  1692
       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
paulson@14314
  1693
apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
paulson@14314
  1694
done
paulson@14314
  1695
declare hIm_hcomplex_polar [simp]
paulson@14314
  1696
paulson@14314
  1697
lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a"
paulson@14314
  1698
apply (unfold hrcis_def)
paulson@14314
  1699
apply (auto simp add: hcis_eq)
paulson@14314
  1700
done
paulson@14314
  1701
declare hIm_hrcis [simp]
paulson@14314
  1702
paulson@14314
  1703
lemma hcmod_complex_polar: "hcmod (hcomplex_of_hypreal r *
paulson@14314
  1704
      (hcomplex_of_hypreal(( *f* cos) a) +
paulson@14314
  1705
       iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
paulson@14314
  1706
apply (rule_tac z = "r" in eq_Abs_hypreal)
paulson@14314
  1707
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1708
apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
paulson@14314
  1709
done
paulson@14314
  1710
declare hcmod_complex_polar [simp]
paulson@14314
  1711
paulson@14314
  1712
lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r"
paulson@14314
  1713
apply (unfold hrcis_def)
paulson@14314
  1714
apply (auto simp add: hcis_eq)
paulson@14314
  1715
done
paulson@14314
  1716
declare hcmod_hrcis [simp]
paulson@14314
  1717
paulson@14314
  1718
(*---------------------------------------------------------------------------*)
paulson@14314
  1719
(*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
paulson@14314
  1720
(*---------------------------------------------------------------------------*)
paulson@14314
  1721
paulson@14314
  1722
lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
paulson@14314
  1723
paulson@14314
  1724
apply (unfold hrcis_def)
paulson@14314
  1725
apply (simp (no_asm))
paulson@14314
  1726
done
paulson@14314
  1727
declare hcis_hrcis_eq [symmetric, simp]
paulson@14314
  1728
paulson@14314
  1729
lemma hrcis_mult:
paulson@14314
  1730
  "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
paulson@14314
  1731
apply (unfold hrcis_def)
paulson@14314
  1732
apply (rule_tac z = "r1" in eq_Abs_hypreal)
paulson@14314
  1733
apply (rule_tac z = "r2" in eq_Abs_hypreal)
paulson@14314
  1734
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1735
apply (rule_tac z = "b" in eq_Abs_hypreal)
paulson@14314
  1736
apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
paulson@14314
  1737
                      hcomplex_mult cis_mult [symmetric] 
paulson@14314
  1738
                      complex_of_real_mult [symmetric])
paulson@14314
  1739
done
paulson@14314
  1740
paulson@14314
  1741
lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
paulson@14314
  1742
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1743
apply (rule_tac z = "b" in eq_Abs_hypreal)
paulson@14314
  1744
apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult)
paulson@14314
  1745
done
paulson@14314
  1746
paulson@14314
  1747
lemma hcis_zero:
paulson@14314
  1748
  "hcis 0 = 1"
paulson@14314
  1749
apply (unfold hcomplex_one_def)
paulson@14314
  1750
apply (auto simp add: hcis hypreal_zero_num)
paulson@14314
  1751
done
paulson@14314
  1752
declare hcis_zero [simp]
paulson@14314
  1753
paulson@14314
  1754
lemma hrcis_zero_mod:
paulson@14314
  1755
  "hrcis 0 a = 0"
paulson@14314
  1756
apply (unfold hcomplex_zero_def)
paulson@14314
  1757
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1758
apply (auto simp add: hrcis hypreal_zero_num)
paulson@14314
  1759
done
paulson@14314
  1760
declare hrcis_zero_mod [simp]
paulson@14314
  1761
paulson@14314
  1762
lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r"
paulson@14314
  1763
apply (rule_tac z = "r" in eq_Abs_hypreal)
paulson@14314
  1764
apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
paulson@14314
  1765
done
paulson@14314
  1766
declare hrcis_zero_arg [simp]
paulson@14314
  1767
paulson@14314
  1768
lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x"
paulson@14314
  1769
apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric])
paulson@14314
  1770
done
paulson@14314
  1771
declare hcomplex_i_mult_minus [simp]
paulson@14314
  1772
paulson@14314
  1773
lemma hcomplex_i_mult_minus2: "iii * iii * x = - x"
paulson@14314
  1774
apply (simp (no_asm))
paulson@14314
  1775
done
paulson@14314
  1776
declare hcomplex_i_mult_minus2 [simp]
paulson@14314
  1777
paulson@14314
  1778
(* Move to one of the hyperreal theories *)
paulson@14314
  1779
lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
paulson@14314
  1780
apply (induct_tac "m")
paulson@14314
  1781
apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
paulson@14314
  1782
done
paulson@14314
  1783
paulson@14314
  1784
lemma hcis_hypreal_of_nat_Suc_mult:
paulson@14314
  1785
   "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
paulson@14314
  1786
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1787
apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
paulson@14314
  1788
done
paulson@14314
  1789
paulson@14314
  1790
lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
paulson@14314
  1791
apply (induct_tac "n")
paulson@14314
  1792
apply (auto simp add: hcis_hypreal_of_nat_Suc_mult)
paulson@14314
  1793
done
paulson@14314
  1794
paulson@14314
  1795
lemma hcis_hypreal_of_hypnat_Suc_mult: "hcis (hypreal_of_hypnat (n + 1) * a) =
paulson@14314
  1796
      hcis a * hcis (hypreal_of_hypnat n * a)"
paulson@14314
  1797
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1798
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1799
apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
paulson@14314
  1800
done
paulson@14314
  1801
paulson@14314
  1802
lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
paulson@14314
  1803
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1804
apply (rule_tac z = "n" in eq_Abs_hypnat)
paulson@14314
  1805
apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
paulson@14314
  1806
done
paulson@14314
  1807
paulson@14314
  1808
lemma DeMoivre2:
paulson@14314
  1809
  "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
paulson@14314
  1810
apply (unfold hrcis_def)
paulson@14314
  1811
apply (auto simp add: hcomplexpow_mult NSDeMoivre hcomplex_of_hypreal_pow)
paulson@14314
  1812
done
paulson@14314
  1813
paulson@14314
  1814
lemma DeMoivre2_ext:
paulson@14314
  1815
  "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
paulson@14314
  1816
apply (unfold hrcis_def)
paulson@14314
  1817
apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
paulson@14314
  1818
done
paulson@14314
  1819
paulson@14314
  1820
lemma hcis_inverse: "inverse(hcis a) = hcis (-a)"
paulson@14314
  1821
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1822
apply (auto simp add: hcomplex_inverse hcis hypreal_minus)
paulson@14314
  1823
done
paulson@14314
  1824
declare hcis_inverse [simp]
paulson@14314
  1825
paulson@14314
  1826
lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
paulson@14314
  1827
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1828
apply (rule_tac z = "r" in eq_Abs_hypreal)
paulson@14314
  1829
apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse)
paulson@14314
  1830
apply (ultra)
paulson@14314
  1831
apply (unfold real_divide_def)
paulson@14314
  1832
apply (auto simp add: INVERSE_ZERO)
paulson@14314
  1833
done
paulson@14314
  1834
paulson@14314
  1835
lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a"
paulson@14314
  1836
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1837
apply (auto simp add: hcis starfun hRe)
paulson@14314
  1838
done
paulson@14314
  1839
declare hRe_hcis [simp]
paulson@14314
  1840
paulson@14314
  1841
lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a"
paulson@14314
  1842
apply (rule_tac z = "a" in eq_Abs_hypreal)
paulson@14314
  1843
apply (auto simp add: hcis starfun hIm)
paulson@14314
  1844
done
paulson@14314
  1845
declare hIm_hcis [simp]
paulson@14314
  1846
paulson@14314
  1847
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
paulson@14314
  1848
apply (auto simp add: NSDeMoivre)
paulson@14314
  1849
done
paulson@14314
  1850
paulson@14314
  1851
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
paulson@14314
  1852
apply (auto simp add: NSDeMoivre)
paulson@14314
  1853
done
paulson@14314
  1854
paulson@14314
  1855
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
paulson@14314
  1856
apply (auto simp add: NSDeMoivre_ext)
paulson@14314
  1857
done
paulson@14314
  1858
paulson@14314
  1859
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
paulson@14314
  1860
apply (auto simp add: NSDeMoivre_ext)
paulson@14314
  1861
done
paulson@14314
  1862
paulson@14314
  1863
lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
paulson@14314
  1864
apply (unfold hexpi_def)
paulson@14314
  1865
apply (rule_tac z = "a" in eq_Abs_hcomplex)
paulson@14314
  1866
apply (rule_tac z = "b" in eq_Abs_hcomplex)
paulson@14314
  1867
apply (auto 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
  1868
done
paulson@14314
  1869
paulson@14314
  1870
paulson@14314
  1871
subsection{*@{term hcomplex_of_complex} Preserves Field Properties*}
paulson@14314
  1872
paulson@14314
  1873
lemma hcomplex_of_complex_add:
paulson@14314
  1874
     "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
paulson@14314
  1875
apply (unfold hcomplex_of_complex_def)
paulson@14314
  1876
apply (simp (no_asm) add: hcomplex_add)
paulson@14314
  1877
done
paulson@14314
  1878
declare hcomplex_of_complex_add [simp]
paulson@14314
  1879
paulson@14314
  1880
lemma hcomplex_of_complex_mult:
paulson@14314
  1881
     "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
paulson@14314
  1882
apply (unfold hcomplex_of_complex_def)
paulson@14314
  1883
apply (simp (no_asm) add: hcomplex_mult)
paulson@14314
  1884
done
paulson@14314
  1885
declare hcomplex_of_complex_mult [simp]
paulson@14314
  1886
paulson@14314
  1887
lemma hcomplex_of_complex_eq_iff:
paulson@14314
  1888
 "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
paulson@14314
  1889
apply (unfold hcomplex_of_complex_def)
paulson@14314
  1890
apply auto
paulson@14314
  1891
done
paulson@14314
  1892
declare hcomplex_of_complex_eq_iff [simp]
paulson@14314
  1893
paulson@14314
  1894
lemma hcomplex_of_complex_minus: "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
paulson@14314
  1895
apply (unfold hcomplex_of_complex_def)
paulson@14314
  1896
apply (auto simp add: hcomplex_minus)
paulson@14314
  1897
done
paulson@14314
  1898
declare hcomplex_of_complex_minus [simp]
paulson@14314
  1899
paulson@14314
  1900
lemma hcomplex_of_complex_one:
paulson@14314
  1901
      "hcomplex_of_complex 1 = 1"
paulson@14314
  1902
apply (unfold hcomplex_of_complex_def hcomplex_one_def)
paulson@14314
  1903
apply auto
paulson@14314
  1904
done
paulson@14314
  1905
paulson@14314
  1906
lemma hcomplex_of_complex_zero:
paulson@14314
  1907
      "hcomplex_of_complex 0 = 0"
paulson@14314
  1908
apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
paulson@14314
  1909
apply (simp (no_asm))
paulson@14314
  1910
done
paulson@14314
  1911
paulson@14314
  1912
lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)"
paulson@14314
  1913
apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
paulson@14314
  1914
done
paulson@14314
  1915
paulson@14314
  1916
lemma hcomplex_of_complex_inverse: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
paulson@14314
  1917
apply (case_tac "r=0")
paulson@14314
  1918
apply (simp (no_asm_simp) add: COMPLEX_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO hcomplex_of_complex_zero COMPLEX_DIVIDE_ZERO)
paulson@14314
  1919
apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1])
paulson@14314
  1920
apply (force simp add: hcomplex_of_complex_zero_iff)
paulson@14314
  1921
apply (subst hcomplex_of_complex_mult [symmetric])
paulson@14314
  1922
apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff); 
paulson@14314
  1923
done
paulson@14314
  1924
declare hcomplex_of_complex_inverse [simp]
paulson@14314
  1925
paulson@14314
  1926
lemma hcomplex_of_complex_divide: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
paulson@14314
  1927
apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def)
paulson@14314
  1928
done
paulson@14314
  1929
declare hcomplex_of_complex_divide [simp]
paulson@14314
  1930
paulson@14314
  1931
lemma hRe_hcomplex_of_complex:
paulson@14314
  1932
   "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
paulson@14314
  1933
apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
paulson@14314
  1934
apply (auto simp add: hRe)
paulson@14314
  1935
done
paulson@14314
  1936
paulson@14314
  1937
lemma hIm_hcomplex_of_complex:
paulson@14314
  1938
   "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
paulson@14314
  1939
apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
paulson@14314
  1940
apply (auto simp add: hIm)
paulson@14314
  1941
done
paulson@14314
  1942
paulson@14314
  1943
lemma hcmod_hcomplex_of_complex:
paulson@14314
  1944
     "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
paulson@14314
  1945
apply (unfold hypreal_of_real_def hcomplex_of_complex_def)
paulson@14314
  1946
apply (auto simp add: hcmod)
paulson@14314
  1947
done
paulson@14314
  1948
paulson@14314
  1949
ML
paulson@14314
  1950
{*
paulson@14314
  1951
val hcomplex_zero_def = thm"hcomplex_zero_def";
paulson@14314
  1952
val hcomplex_one_def = thm"hcomplex_one_def";
paulson@14314
  1953
val hcomplex_minus_def = thm"hcomplex_minus_def";
paulson@14314
  1954
val hcomplex_diff_def = thm"hcomplex_diff_def";
paulson@14314
  1955
val hcomplex_divide_def = thm"hcomplex_divide_def";
paulson@14314
  1956
val hcomplex_mult_def = thm"hcomplex_mult_def";
paulson@14314
  1957
val hcomplex_add_def = thm"hcomplex_add_def";
paulson@14314
  1958
val hcomplex_of_complex_def = thm"hcomplex_of_complex_def";
paulson@14314
  1959
val iii_def = thm"iii_def";
paulson@14314
  1960
paulson@14314
  1961
val hcomplexrel_iff = thm"hcomplexrel_iff";
paulson@14314
  1962
val hcomplexrel_refl = thm"hcomplexrel_refl";
paulson@14314
  1963
val hcomplexrel_sym = thm"hcomplexrel_sym";
paulson@14314
  1964
val hcomplexrel_trans = thm"hcomplexrel_trans";
paulson@14314
  1965
val equiv_hcomplexrel = thm"equiv_hcomplexrel";
paulson@14314
  1966
val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff";
paulson@14314
  1967
val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex";
paulson@14314
  1968
val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex";
paulson@14314
  1969
val inj_Rep_hcomplex = thm"inj_Rep_hcomplex";
paulson@14314
  1970
val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl";
paulson@14314
  1971
val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem";
paulson@14314
  1972
val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty";
paulson@14314
  1973
val eq_Abs_hcomplex = thm"eq_Abs_hcomplex";
paulson@14314
  1974
val hRe = thm"hRe";
paulson@14314
  1975
val hIm = thm"hIm";
paulson@14314
  1976
val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
paulson@14314
  1977
val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
paulson@14314
  1978
val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
paulson@14314
  1979
val hcomplex_hRe_one = thm"hcomplex_hRe_one";
paulson@14314
  1980
val hcomplex_hIm_one = thm"hcomplex_hIm_one";
paulson@14314
  1981
val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
paulson@14314
  1982
val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
paulson@14314
  1983
val hcomplex_add_congruent2 = thm"hcomplex_add_congruent2";
paulson@14314
  1984
val hcomplex_add = thm"hcomplex_add";
paulson@14314
  1985
val hcomplex_add_commute = thm"hcomplex_add_commute";
paulson@14314
  1986
val hcomplex_add_assoc = thm"hcomplex_add_assoc";
paulson@14314
  1987
val hcomplex_add_left_commute = thm"hcomplex_add_left_commute";
paulson@14314
  1988
val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
paulson@14314
  1989
val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
paulson@14314
  1990
val hRe_add = thm"hRe_add";
paulson@14314
  1991
val hIm_add = thm"hIm_add";
paulson@14314
  1992
val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
paulson@14314
  1993
val hcomplex_minus = thm"hcomplex_minus";
paulson@14314
  1994
val hcomplex_minus_minus = thm"hcomplex_minus_minus";
paulson@14314
  1995
val inj_hcomplex_minus = thm"inj_hcomplex_minus";
paulson@14314
  1996
val hcomplex_minus_zero = thm"hcomplex_minus_zero";
paulson@14314
  1997
val hcomplex_minus_zero_iff = thm"hcomplex_minus_zero_iff";
paulson@14314
  1998
val hcomplex_minus_zero_iff2 = thm"hcomplex_minus_zero_iff2";
paulson@14314
  1999
val hcomplex_minus_not_zero_iff = thm"hcomplex_minus_not_zero_iff";
paulson@14314
  2000
val hcomplex_add_minus_right = thm"hcomplex_add_minus_right";
paulson@14314
  2001
val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
paulson@14314
  2002
val hcomplex_add_minus_cancel = thm"hcomplex_add_minus_cancel";
paulson@14314
  2003
val hcomplex_minus_add_cancel = thm"hcomplex_minus_add_cancel";
paulson@14314
  2004
val hRe_minus = thm"hRe_minus";
paulson@14314
  2005
val hIm_minus = thm"hIm_minus";
paulson@14314
  2006
val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
paulson@14314
  2007
val hcomplex_minus_add_distrib = thm"hcomplex_minus_add_distrib";
paulson@14314
  2008
val hcomplex_add_left_cancel = thm"hcomplex_add_left_cancel";
paulson@14314
  2009
val hcomplex_add_right_cancel = thm"hcomplex_add_right_cancel";
paulson@14314
  2010
val hcomplex_eq_minus_iff = thm"hcomplex_eq_minus_iff";
paulson@14314
  2011
val hcomplex_eq_minus_iff2 = thm"hcomplex_eq_minus_iff2";
paulson@14314
  2012
val hcomplex_diff = thm"hcomplex_diff";
paulson@14314
  2013
val hcomplex_diff_zero = thm"hcomplex_diff_zero";
paulson@14314
  2014
val hcomplex_diff_0 = thm"hcomplex_diff_0";
paulson@14314
  2015
val hcomplex_diff_0_right = thm"hcomplex_diff_0_right";
paulson@14314
  2016
val hcomplex_diff_self = thm"hcomplex_diff_self";
paulson@14314
  2017
val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
paulson@14314
  2018
val hcomplex_mult = thm"hcomplex_mult";
paulson@14314
  2019
val hcomplex_mult_commute = thm"hcomplex_mult_commute";
paulson@14314
  2020
val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
paulson@14314
  2021
val hcomplex_mult_left_commute = thm"hcomplex_mult_left_commute";
paulson@14314
  2022
val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
paulson@14314
  2023
val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
paulson@14314
  2024
val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
paulson@14314
  2025
val hcomplex_mult_zero_right = thm"hcomplex_mult_zero_right";
paulson@14314
  2026
val hcomplex_minus_mult_eq1 = thm"hcomplex_minus_mult_eq1";
paulson@14314
  2027
val hcomplex_minus_mult_eq2 = thm"hcomplex_minus_mult_eq2";
paulson@14314
  2028
val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
paulson@14314
  2029
val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
paulson@14314
  2030
val hcomplex_minus_mult_cancel = thm"hcomplex_minus_mult_cancel";
paulson@14314
  2031
val hcomplex_minus_mult_commute = thm"hcomplex_minus_mult_commute";
paulson@14314
  2032
val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
paulson@14314
  2033
val hcomplex_add_mult_distrib2 = thm"hcomplex_add_mult_distrib2";
paulson@14314
  2034
val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
paulson@14314
  2035
val hcomplex_inverse = thm"hcomplex_inverse";
paulson@14314
  2036
val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO";
paulson@14314
  2037
val HCOMPLEX_DIVISION_BY_ZERO = thm"HCOMPLEX_DIVISION_BY_ZERO";
paulson@14314
  2038
val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
paulson@14314
  2039
val hcomplex_mult_inv_right = thm"hcomplex_mult_inv_right";
paulson@14314
  2040
val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
paulson@14314
  2041
val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
paulson@14314
  2042
val hcomplex_inverse_not_zero = thm"hcomplex_inverse_not_zero";
paulson@14314
  2043
val hcomplex_mult_not_zero = thm"hcomplex_mult_not_zero";
paulson@14314
  2044
val hcomplex_mult_not_zeroE = thm"hcomplex_mult_not_zeroE";
paulson@14314
  2045
val hcomplex_inverse_inverse = thm"hcomplex_inverse_inverse";
paulson@14314
  2046
val hcomplex_inverse_one = thm"hcomplex_inverse_one";
paulson@14314
  2047
val hcomplex_minus_inverse = thm"hcomplex_minus_inverse";
paulson@14314
  2048
val hcomplex_inverse_distrib = thm"hcomplex_inverse_distrib";
paulson@14314
  2049
val hcomplex_times_divide1_eq = thm"hcomplex_times_divide1_eq";
paulson@14314
  2050
val hcomplex_times_divide2_eq = thm"hcomplex_times_divide2_eq";
paulson@14314
  2051
val hcomplex_divide_divide1_eq = thm"hcomplex_divide_divide1_eq";
paulson@14314
  2052
val hcomplex_divide_divide2_eq = thm"hcomplex_divide_divide2_eq";
paulson@14314
  2053
val hcomplex_minus_divide_eq = thm"hcomplex_minus_divide_eq";
paulson@14314
  2054
val hcomplex_divide_minus_eq = thm"hcomplex_divide_minus_eq";
paulson@14314
  2055
val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
paulson@14314
  2056
val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
paulson@14314
  2057
val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal";
paulson@14314
  2058
val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
paulson@14314
  2059
val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
paulson@14314
  2060
val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
paulson@14314
  2061
val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
paulson@14314
  2062
val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
paulson@14314
  2063
val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
paulson@14314
  2064
val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
paulson@14314
  2065
val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
paulson@14314
  2066
val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
paulson@14314
  2067
val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
paulson@14314
  2068
val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
paulson@14314
  2069
val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
paulson@14314
  2070
val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
paulson@14314
  2071
val hcmod = thm"hcmod";
paulson@14314
  2072
val hcmod_zero = thm"hcmod_zero";
paulson@14314
  2073
val hcmod_one = thm"hcmod_one";
paulson@14314
  2074
val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
paulson@14314
  2075
val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
paulson@14314
  2076
val hcnj = thm"hcnj";
paulson@14314
  2077
val inj_hcnj = thm"inj_hcnj";
paulson@14314
  2078
val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
paulson@14314
  2079
val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
paulson@14314
  2080
val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
paulson@14314
  2081
val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
paulson@14314
  2082
val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
paulson@14314
  2083
val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
paulson@14314
  2084
val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
paulson@14314
  2085
val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
paulson@14314
  2086
val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
paulson@14314
  2087
val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
paulson@14314
  2088
val hcnj_one = thm"hcnj_one";
paulson@14314
  2089
val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
paulson@14314
  2090
val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
paulson@14314
  2091
val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
paulson@14314
  2092
val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
paulson@14314
  2093
val hcomplex_mult_zero_iff = thm"hcomplex_mult_zero_iff";
paulson@14314
  2094
val hcomplex_add_left_cancel_zero = thm"hcomplex_add_left_cancel_zero";
paulson@14314
  2095
val hcomplex_diff_mult_distrib = thm"hcomplex_diff_mult_distrib";
paulson@14314
  2096
val hcomplex_diff_mult_distrib2 = thm"hcomplex_diff_mult_distrib2";
paulson@14314
  2097
val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
paulson@14314
  2098
val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
paulson@14314
  2099
val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
paulson@14314
  2100
val hypreal_of_hypnat_ge_zero = thm"hypreal_of_hypnat_ge_zero";
paulson@14314
  2101
val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
paulson@14314
  2102
val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
paulson@14314
  2103
val hcmod_minus = thm"hcmod_minus";
paulson@14314
  2104
val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
paulson@14314
  2105
val hcmod_ge_zero = thm"hcmod_ge_zero";
paulson@14314
  2106
val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
paulson@14314
  2107
val hcmod_mult = thm"hcmod_mult";
paulson@14314
  2108
val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
paulson@14314
  2109
val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
paulson@14314
  2110
val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
paulson@14314
  2111
val hcmod_triangle_squared = thm"hcmod_triangle_squared";
paulson@14314
  2112
val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
paulson@14314
  2113
val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
paulson@14314
  2114
val hcmod_diff_commute = thm"hcmod_diff_commute";
paulson@14314
  2115
val hcmod_add_less = thm"hcmod_add_less";
paulson@14314
  2116
val hcmod_mult_less = thm"hcmod_mult_less";
paulson@14314
  2117
val hcmod_diff_ineq = thm"hcmod_diff_ineq";
paulson@14314
  2118
val hcpow = thm"hcpow";
paulson@14314
  2119
val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
paulson@14314
  2120
val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
paulson@14314
  2121
val hcmod_hcpow = thm"hcmod_hcpow";
paulson@14314
  2122
val hcomplexpow_minus = thm"hcomplexpow_minus";
paulson@14314
  2123
val hcpow_minus = thm"hcpow_minus";
paulson@14314
  2124
val hccomplex_inverse_minus = thm"hccomplex_inverse_minus";
paulson@14314
  2125
val hcomplex_div_one = thm"hcomplex_div_one";
paulson@14314
  2126
val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
paulson@14314
  2127
val hcmod_divide = thm"hcmod_divide";
paulson@14314
  2128
val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
paulson@14314
  2129
val hcomplexpow_mult = thm"hcomplexpow_mult";
paulson@14314
  2130
val hcpow_mult = thm"hcpow_mult";
paulson@14314
  2131
val hcomplexpow_zero = thm"hcomplexpow_zero";
paulson@14314
  2132
val hcpow_zero = thm"hcpow_zero";
paulson@14314
  2133
val hcpow_zero2 = thm"hcpow_zero2";
paulson@14314
  2134
val hcomplexpow_not_zero = thm"hcomplexpow_not_zero";
paulson@14314
  2135
val hcpow_not_zero = thm"hcpow_not_zero";
paulson@14314
  2136
val hcomplexpow_zero_zero = thm"hcomplexpow_zero_zero";
paulson@14314
  2137
val hcpow_zero_zero = thm"hcpow_zero_zero";
paulson@14314
  2138
val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
paulson@14314
  2139
val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
paulson@14314
  2140
val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
paulson@14314
  2141
val hcomplex_mult_eq_zero_cancel1 = thm"hcomplex_mult_eq_zero_cancel1";
paulson@14314
  2142
val hcomplex_mult_eq_zero_cancel2 = thm"hcomplex_mult_eq_zero_cancel2";
paulson@14314
  2143
val hcomplex_mult_not_eq_zero_iff = thm"hcomplex_mult_not_eq_zero_iff";
paulson@14314
  2144
val hcomplex_divide = thm"hcomplex_divide";
paulson@14314
  2145
val hsgn = thm"hsgn";
paulson@14314
  2146
val hsgn_zero = thm"hsgn_zero";
paulson@14314
  2147
val hsgn_one = thm"hsgn_one";
paulson@14314
  2148
val hsgn_minus = thm"hsgn_minus";
paulson@14314
  2149
val hsgn_eq = thm"hsgn_eq";
paulson@14314
  2150
val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
paulson@14314
  2151
val complex_split2 = thm"complex_split2";
paulson@14314
  2152
val hcomplex_split = thm"hcomplex_split";
paulson@14314
  2153
val hRe_hcomplex_i = thm"hRe_hcomplex_i";
paulson@14314
  2154
val hIm_hcomplex_i = thm"hIm_hcomplex_i";
paulson@14314
  2155
val hcmod_i = thm"hcmod_i";
paulson@14314
  2156
val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq";
paulson@14314
  2157
val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq";
paulson@14314
  2158
val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff";
paulson@14314
  2159
val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA";
paulson@14314
  2160
val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB";
paulson@14314
  2161
val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC";
paulson@14314
  2162
val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
paulson@14314
  2163
val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a";
paulson@14314
  2164
val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3";
paulson@14314
  2165
val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a";
paulson@14314
  2166
val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero";
paulson@14314
  2167
val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero";
paulson@14314
  2168
val hRe_hsgn = thm"hRe_hsgn";
paulson@14314
  2169
val hIm_hsgn = thm"hIm_hsgn";
paulson@14314
  2170
val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
paulson@14314
  2171
val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split";
paulson@14314
  2172
val hRe_mult_i_eq = thm"hRe_mult_i_eq";
paulson@14314
  2173
val hIm_mult_i_eq = thm"hIm_mult_i_eq";
paulson@14314
  2174
val hcmod_mult_i = thm"hcmod_mult_i";
paulson@14314
  2175
val hcmod_mult_i2 = thm"hcmod_mult_i2";
paulson@14314
  2176
val harg = thm"harg";
paulson@14314
  2177
val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
paulson@14314
  2178
val cos_harg_i_mult_zero2 = thm"cos_harg_i_mult_zero2";
paulson@14314
  2179
val hcomplex_of_hypreal_not_zero_iff = thm"hcomplex_of_hypreal_not_zero_iff";
paulson@14314
  2180
val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
paulson@14314
  2181
val cos_harg_i_mult_zero3 = thm"cos_harg_i_mult_zero3";
paulson@14314
  2182
val complex_split_polar2 = thm"complex_split_polar2";
paulson@14314
  2183
val hcomplex_split_polar = thm"hcomplex_split_polar";
paulson@14314
  2184
val hcis = thm"hcis";
paulson@14314
  2185
val hcis_eq = thm"hcis_eq";
paulson@14314
  2186
val hrcis = thm"hrcis";
paulson@14314
  2187
val hrcis_Ex = thm"hrcis_Ex";
paulson@14314
  2188
val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
paulson@14314
  2189
val hRe_hrcis = thm"hRe_hrcis";
paulson@14314
  2190
val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
paulson@14314
  2191
val hIm_hrcis = thm"hIm_hrcis";
paulson@14314
  2192
val hcmod_complex_polar = thm"hcmod_complex_polar";
paulson@14314
  2193
val hcmod_hrcis = thm"hcmod_hrcis";
paulson@14314
  2194
val hcis_hrcis_eq = thm"hcis_hrcis_eq";
paulson@14314
  2195
val hrcis_mult = thm"hrcis_mult";
paulson@14314
  2196
val hcis_mult = thm"hcis_mult";
paulson@14314
  2197
val hcis_zero = thm"hcis_zero";
paulson@14314
  2198
val hrcis_zero_mod = thm"hrcis_zero_mod";
paulson@14314
  2199
val hrcis_zero_arg = thm"hrcis_zero_arg";
paulson@14314
  2200
val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
paulson@14314
  2201
val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
paulson@14314
  2202
val hypreal_of_nat = thm"hypreal_of_nat";
paulson@14314
  2203
val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
paulson@14314
  2204
val NSDeMoivre = thm"NSDeMoivre";
paulson@14314
  2205
val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
paulson@14314
  2206
val NSDeMoivre_ext = thm"NSDeMoivre_ext";
paulson@14314
  2207
val DeMoivre2 = thm"DeMoivre2";
paulson@14314
  2208
val DeMoivre2_ext = thm"DeMoivre2_ext";
paulson@14314
  2209
val hcis_inverse = thm"hcis_inverse";
paulson@14314
  2210
val hrcis_inverse = thm"hrcis_inverse";
paulson@14314
  2211
val hRe_hcis = thm"hRe_hcis";
paulson@14314
  2212
val hIm_hcis = thm"hIm_hcis";
paulson@14314
  2213
val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
paulson@14314
  2214
val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
paulson@14314
  2215
val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
paulson@14314
  2216
val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
paulson@14314
  2217
val hexpi_add = thm"hexpi_add";
paulson@14314
  2218
val hcomplex_of_complex_add = thm"hcomplex_of_complex_add";
paulson@14314
  2219
val hcomplex_of_complex_mult = thm"hcomplex_of_complex_mult";
paulson@14314
  2220
val hcomplex_of_complex_eq_iff = thm"hcomplex_of_complex_eq_iff";
paulson@14314
  2221
val hcomplex_of_complex_minus = thm"hcomplex_of_complex_minus";
paulson@14314
  2222
val hcomplex_of_complex_one = thm"hcomplex_of_complex_one";
paulson@14314
  2223
val hcomplex_of_complex_zero = thm"hcomplex_of_complex_zero";
paulson@14314
  2224
val hcomplex_of_complex_zero_iff = thm"hcomplex_of_complex_zero_iff";
paulson@14314
  2225
val hcomplex_of_complex_inverse = thm"hcomplex_of_complex_inverse";
paulson@14314
  2226
val hcomplex_of_complex_divide = thm"hcomplex_of_complex_divide";
paulson@14314
  2227
val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
paulson@14314
  2228
val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
paulson@14314
  2229
val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
paulson@14314
  2230
paulson@14314
  2231
val hcomplex_add_ac = thms"hcomplex_add_ac";
paulson@14314
  2232
val hcomplex_mult_ac = thms"hcomplex_mult_ac";
paulson@14314
  2233
*}
paulson@14314
  2234
paulson@13957
  2235
end