src/HOL/Complex.thy
author paulson
Thu, 03 Sep 2015 20:27:53 +0100
changeset 61104 3c2d4636cebc
parent 61076 bdc1e2f0a86a
child 61531 ab2e862263e7
permissions -rw-r--r--
new lemmas about vector_derivative, complex numbers, paths, etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 37887
diff changeset
     1
(*  Title:       HOL/Complex.thy
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     2
    Author:      Jacques D. Fleuriot
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     3
    Copyright:   2001 University of Edinburgh
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14377
diff changeset
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     5
*)
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     6
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
     7
section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14354
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15085
diff changeset
     9
theory Complex
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
    10
imports Transcendental
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15085
diff changeset
    11
begin
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    12
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    13
text \<open>
58146
d91c1e50b36e codatatypes are not datatypes
blanchet
parents: 57512
diff changeset
    14
We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
d91c1e50b36e codatatypes are not datatypes
blanchet
parents: 57512
diff changeset
    15
@{text primcorec} to define complex functions by defining their real and imaginary result
d91c1e50b36e codatatypes are not datatypes
blanchet
parents: 57512
diff changeset
    16
separately.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    17
\<close>
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14354
diff changeset
    18
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    19
codatatype complex = Complex (Re: real) (Im: real)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    20
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    21
lemma complex_surj: "Complex (Re z) (Im z) = z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    22
  by (rule complex.collapse)
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    23
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
    24
lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    25
  by (rule complex.expand) simp
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    26
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
    27
lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    28
  by (auto intro: complex.expand)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    29
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    30
subsection \<open>Addition and Subtraction\<close>
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    31
25599
haftmann
parents: 25571
diff changeset
    32
instantiation complex :: ab_group_add
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
    33
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
    34
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    35
primcorec zero_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    36
  "Re 0 = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    37
| "Im 0 = 0"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
    38
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    39
primcorec plus_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    40
  "Re (x + y) = Re x + Re y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    41
| "Im (x + y) = Im x + Im y"
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    42
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    43
primcorec uminus_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    44
  "Re (- x) = - Re x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    45
| "Im (- x) = - Im x"
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    46
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    47
primcorec minus_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    48
  "Re (x - y) = Re x - Re y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    49
| "Im (x - y) = Im x - Im y"
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    50
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    51
instance
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    52
  by intro_classes (simp_all add: complex_eq_iff)
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    53
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    54
end
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    55
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    56
subsection \<open>Multiplication and Division\<close>
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    57
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59862
diff changeset
    58
instantiation complex :: field
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
    59
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
    60
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    61
primcorec one_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    62
  "Re 1 = 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    63
| "Im 1 = 0"
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
    64
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    65
primcorec times_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    66
  "Re (x * y) = Re x * Re y - Im x * Im y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    67
| "Im (x * y) = Re x * Im y + Im x * Re y"
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
    68
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    69
primcorec inverse_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    70
  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    71
| "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
14335
9c0b5e081037 conversion of Real/PReal to Isar script;
paulson
parents: 14334
diff changeset
    72
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
    73
definition "x div (y::complex) = x * inverse y"
14335
9c0b5e081037 conversion of Real/PReal to Isar script;
paulson
parents: 14334
diff changeset
    74
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    75
instance
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
    76
  by intro_classes
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    77
     (simp_all add: complex_eq_iff divide_complex_def
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    78
      distrib_left distrib_right right_diff_distrib left_diff_distrib
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    79
      power2_eq_square add_divide_distrib [symmetric])
14335
9c0b5e081037 conversion of Real/PReal to Isar script;
paulson
parents: 14334
diff changeset
    80
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
    81
end
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    82
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    83
lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    84
  unfolding divide_complex_def by (simp add: add_divide_distrib)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    85
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    86
lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    87
  unfolding divide_complex_def times_complex.sel inverse_complex.sel
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    88
  by (simp_all add: divide_simps)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    89
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    90
lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    91
  by (simp add: power2_eq_square)
20556
2e8227b81bf1 add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents: 20485
diff changeset
    92
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    93
lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    94
  by (simp add: power2_eq_square)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
    95
59862
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59746
diff changeset
    96
lemma Re_power_real [simp]: "Im x = 0 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
    97
  by (induct n) simp_all
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
    98
59862
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59746
diff changeset
    99
lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   100
  by (induct n) simp_all
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   101
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   102
subsection \<open>Scalar Multiplication\<close>
20556
2e8227b81bf1 add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents: 20485
diff changeset
   103
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   104
instantiation complex :: real_field
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   105
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   106
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   107
primcorec scaleR_complex where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   108
  "Re (scaleR r x) = r * Re x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   109
| "Im (scaleR r x) = r * Im x"
22972
3e96b98d37c6 generalized sgn function to work on any real normed vector space
huffman
parents: 22968
diff changeset
   110
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   111
instance
20556
2e8227b81bf1 add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents: 20485
diff changeset
   112
proof
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   113
  fix a b :: real and x y :: complex
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   114
  show "scaleR a (x + y) = scaleR a x + scaleR a y"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 47108
diff changeset
   115
    by (simp add: complex_eq_iff distrib_left)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   116
  show "scaleR (a + b) x = scaleR a x + scaleR b x"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 47108
diff changeset
   117
    by (simp add: complex_eq_iff distrib_right)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   118
  show "scaleR a (scaleR b x) = scaleR (a * b) x"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57259
diff changeset
   119
    by (simp add: complex_eq_iff mult.assoc)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   120
  show "scaleR 1 x = x"
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   121
    by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   122
  show "scaleR a x * y = scaleR a (x * y)"
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   123
    by (simp add: complex_eq_iff algebra_simps)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   124
  show "x * scaleR a y = scaleR a (x * y)"
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   125
    by (simp add: complex_eq_iff algebra_simps)
20556
2e8227b81bf1 add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents: 20485
diff changeset
   126
qed
2e8227b81bf1 add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents: 20485
diff changeset
   127
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   128
end
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   129
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   130
subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   131
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   132
abbreviation complex_of_real :: "real \<Rightarrow> complex"
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   133
  where "complex_of_real \<equiv> of_real"
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   134
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
   135
declare [[coercion "of_real :: real \<Rightarrow> complex"]]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
   136
declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   137
declare [[coercion "of_int :: int \<Rightarrow> complex"]]
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   138
declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]
56331
bea2196627cb add complex_of_real coercion
hoelzl
parents: 56238
diff changeset
   139
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   140
lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   141
  by (induct n) simp_all
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   142
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   143
lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   144
  by (induct n) simp_all
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   145
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   146
lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   147
  by (cases z rule: int_diff_cases) simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   148
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   149
lemma complex_Im_of_int [simp]: "Im (of_int z) = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   150
  by (cases z rule: int_diff_cases) simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   151
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   152
lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   153
  using complex_Re_of_int [of "numeral v"] by simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   154
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   155
lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   156
  using complex_Im_of_int [of "numeral v"] by simp
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   157
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   158
lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   159
  by (simp add: of_real_def)
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   160
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   161
lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   162
  by (simp add: of_real_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   163
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   164
lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   165
  by (simp add: Re_divide sqr_conv_mult)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   166
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   167
lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   168
  by (simp add: Im_divide sqr_conv_mult)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   169
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   170
lemma of_real_Re [simp]:
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   171
    "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   172
  by (auto simp: Reals_def)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   173
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   174
subsection \<open>The Complex Number $i$\<close>
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   175
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   176
primcorec "ii" :: complex  ("\<i>") where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   177
  "Re ii = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   178
| "Im ii = 1"
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   179
57259
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   180
lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   181
  by (simp add: complex_eq_iff)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   182
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   183
lemma complex_eq: "a = Re a + \<i> * Im a"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   184
  by (simp add: complex_eq_iff)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   185
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   186
lemma fun_complex_eq: "f = (\<lambda>x. Re (f x) + \<i> * Im (f x))"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   187
  by (simp add: fun_eq_iff complex_eq)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   188
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   189
lemma i_squared [simp]: "ii * ii = -1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   190
  by (simp add: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   191
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   192
lemma power2_i [simp]: "ii\<^sup>2 = -1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   193
  by (simp add: power2_eq_square)
14377
f454b3004f8f tidying up, especially the Complex numbers
paulson
parents: 14374
diff changeset
   194
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   195
lemma inverse_i [simp]: "inverse ii = - ii"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   196
  by (rule inverse_unique) simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   197
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   198
lemma divide_i [simp]: "x / ii = - ii * x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   199
  by (simp add: divide_complex_def)
14377
f454b3004f8f tidying up, especially the Complex numbers
paulson
parents: 14374
diff changeset
   200
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   201
lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57259
diff changeset
   202
  by (simp add: mult.assoc [symmetric])
14377
f454b3004f8f tidying up, especially the Complex numbers
paulson
parents: 14374
diff changeset
   203
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   204
lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   205
  by (simp add: complex_eq_iff)
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   206
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   207
lemma complex_i_not_one [simp]: "ii \<noteq> 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   208
  by (simp add: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   209
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   210
lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   211
  by (simp add: complex_eq_iff)
44841
huffman
parents: 44828
diff changeset
   212
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   213
lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   214
  by (simp add: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   215
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   216
lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   217
  by (simp add: complex_eq_iff polar_Ex)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   218
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   219
lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   220
  by (metis mult.commute power2_i power_mult)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   221
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   222
lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   223
  by simp
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   224
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   225
lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   226
  by simp
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   227
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   228
lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   229
  by auto
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   230
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   231
lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   232
  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   233
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   234
subsection \<open>Vector Norm\<close>
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   235
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   236
instantiation complex :: real_normed_field
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   237
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   238
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   239
definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   240
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   241
abbreviation cmod :: "complex \<Rightarrow> real"
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   242
  where "cmod \<equiv> norm"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   243
31413
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   244
definition complex_sgn_def:
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   245
  "sgn x = x /\<^sub>R cmod x"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25502
diff changeset
   246
31413
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   247
definition dist_complex_def:
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   248
  "dist x y = cmod (x - y)"
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   249
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 36825
diff changeset
   250
definition open_complex_def:
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31419
diff changeset
   251
  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
31292
d24b2692562f definition of dist for complex
huffman
parents: 31021
diff changeset
   252
31413
729d90a531e4 introduce class topological_space as a superclass of metric_space
huffman
parents: 31292
diff changeset
   253
instance proof
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31419
diff changeset
   254
  fix r :: real and x y :: complex and S :: "complex set"
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   255
  show "(norm x = 0) = (x = 0)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   256
    by (simp add: norm_complex_def complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   257
  show "norm (x + y) \<le> norm x + norm y"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   258
    by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   259
  show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   260
    by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   261
  show "norm (x * y) = norm x * norm y"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   262
    by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   263
qed (rule complex_sgn_def dist_complex_def open_complex_def)+
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   264
25712
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   265
end
f488a37cfad4 instantiation target
haftmann
parents: 25599
diff changeset
   266
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   267
lemma norm_ii [simp]: "norm ii = 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   268
  by (simp add: norm_complex_def)
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   269
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   270
lemma cmod_unit_one: "cmod (cos a + \<i> * sin a) = 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   271
  by (simp add: norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   272
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   273
lemma cmod_complex_polar: "cmod (r * (cos a + \<i> * sin a)) = \<bar>r\<bar>"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   274
  by (simp add: norm_mult cmod_unit_one)
22861
8ec47039614e clean up complex norm proofs, remove redundant lemmas
huffman
parents: 22852
diff changeset
   275
8ec47039614e clean up complex norm proofs, remove redundant lemmas
huffman
parents: 22852
diff changeset
   276
lemma complex_Re_le_cmod: "Re x \<le> cmod x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   277
  unfolding norm_complex_def
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   278
  by (rule real_sqrt_sum_squares_ge1)
22861
8ec47039614e clean up complex norm proofs, remove redundant lemmas
huffman
parents: 22852
diff changeset
   279
44761
0694fc3248fd remove some unnecessary simp rules from simpset
huffman
parents: 44749
diff changeset
   280
lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   281
  by (rule order_trans [OF _ norm_ge_zero]) simp
22861
8ec47039614e clean up complex norm proofs, remove redundant lemmas
huffman
parents: 22852
diff changeset
   282
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   283
lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \<le> cmod a"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   284
  by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   285
26117
ca578d3b9f8c Added trivial theorems aboud cmod
chaieb
parents: 25712
diff changeset
   286
lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   287
  by (simp add: norm_complex_def)
26117
ca578d3b9f8c Added trivial theorems aboud cmod
chaieb
parents: 25712
diff changeset
   288
ca578d3b9f8c Added trivial theorems aboud cmod
chaieb
parents: 25712
diff changeset
   289
lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   290
  by (simp add: norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   291
57259
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   292
lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   293
  apply (subst complex_eq)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   294
  apply (rule order_trans)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   295
  apply (rule norm_triangle_ineq)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   296
  apply (simp add: norm_mult)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   297
  done
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   298
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   299
lemma cmod_eq_Re: "Im z = 0 \<Longrightarrow> cmod z = \<bar>Re z\<bar>"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   300
  by (simp add: norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   301
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   302
lemma cmod_eq_Im: "Re z = 0 \<Longrightarrow> cmod z = \<bar>Im z\<bar>"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   303
  by (simp add: norm_complex_def)
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   304
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   305
lemma cmod_power2: "cmod z ^ 2 = (Re z)^2 + (Im z)^2"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   306
  by (simp add: norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   307
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   308
lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \<le> 0 \<longleftrightarrow> Re z = - cmod z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   309
  using abs_Re_le_cmod[of z] by auto
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   310
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   311
lemma Im_eq_0: "\<bar>Re z\<bar> = cmod z \<Longrightarrow> Im z = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   312
  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2])
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   313
     (auto simp add: norm_complex_def)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   314
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   315
lemma abs_sqrt_wlog:
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   316
  fixes x::"'a::linordered_idom"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   317
  assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   318
by (metis abs_ge_zero assms power2_abs)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   319
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   320
lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   321
  unfolding norm_complex_def
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   322
  apply (rule abs_sqrt_wlog [where x="Re z"])
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   323
  apply (rule abs_sqrt_wlog [where x="Im z"])
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   324
  apply (rule power2_le_imp_le)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57259
diff changeset
   325
  apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   326
  done
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   327
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   328
lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   329
  by (simp add: norm_complex_def divide_simps complex_eq_iff)
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   330
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   331
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   332
text \<open>Properties of complex signum.\<close>
44843
huffman
parents: 44842
diff changeset
   333
huffman
parents: 44842
diff changeset
   334
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57259
diff changeset
   335
  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)
44843
huffman
parents: 44842
diff changeset
   336
huffman
parents: 44842
diff changeset
   337
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
huffman
parents: 44842
diff changeset
   338
  by (simp add: complex_sgn_def divide_inverse)
huffman
parents: 44842
diff changeset
   339
huffman
parents: 44842
diff changeset
   340
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
huffman
parents: 44842
diff changeset
   341
  by (simp add: complex_sgn_def divide_inverse)
huffman
parents: 44842
diff changeset
   342
14354
988aa4648597 types complex and hcomplex are now instances of class ringpower:
paulson
parents: 14353
diff changeset
   343
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   344
subsection \<open>Completeness of the Complexes\<close>
23123
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   345
44290
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   346
lemma bounded_linear_Re: "bounded_linear Re"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   347
  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
44290
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   348
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   349
lemma bounded_linear_Im: "bounded_linear Im"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   350
  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
23123
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   351
44290
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   352
lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   353
lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   354
lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   355
lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   356
lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   357
lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   358
lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   359
lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   360
lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   361
lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   362
lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   363
lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   364
lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   365
lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   366
36825
d9320cdcde73 add lemma tendsto_Complex
huffman
parents: 36777
diff changeset
   367
lemma tendsto_Complex [tendsto_intros]:
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   368
  "(f ---> a) F \<Longrightarrow> (g ---> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   369
  by (auto intro!: tendsto_intros)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   370
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   371
lemma tendsto_complex_iff:
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   372
  "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   373
proof safe
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   374
  assume "((\<lambda>x. Re (f x)) ---> Re x) F" "((\<lambda>x. Im (f x)) ---> Im x) F"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   375
  from tendsto_Complex[OF this] show "(f ---> x) F"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   376
    unfolding complex.collapse .
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   377
qed (auto intro: tendsto_intros)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   378
57259
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   379
lemma continuous_complex_iff: "continuous F f \<longleftrightarrow>
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   380
    continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   381
  unfolding continuous_def tendsto_complex_iff ..
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   382
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   383
lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   384
    ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   385
    ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   386
  unfolding has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   387
  by (simp add: field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   388
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   389
lemma has_field_derivative_Re[derivative_intros]:
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   390
  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   391
  unfolding has_vector_derivative_complex_iff by safe
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   392
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   393
lemma has_field_derivative_Im[derivative_intros]:
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   394
  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_field_derivative (Im D)) F"
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   395
  unfolding has_vector_derivative_complex_iff by safe
3a448982a74a add more derivative and continuity rules for complex-values functions
hoelzl
parents: 56889
diff changeset
   396
23123
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   397
instance complex :: banach
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   398
proof
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   399
  fix X :: "nat \<Rightarrow> complex"
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   400
  assume X: "Cauchy X"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   401
  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   402
    by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   403
  then show "convergent X"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   404
    unfolding complex.collapse by (rule convergentI)
23123
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   405
qed
e2e370bccde1 instance complex :: banach
huffman
parents: 22972
diff changeset
   406
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56217
diff changeset
   407
declare
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   408
  DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56217
diff changeset
   409
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   410
subsection \<open>Complex Conjugation\<close>
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   411
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   412
primcorec cnj :: "complex \<Rightarrow> complex" where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   413
  "Re (cnj z) = Re z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   414
| "Im (cnj z) = - Im z"
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   415
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   416
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   417
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   418
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   419
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   420
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   421
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   422
lemma complex_cnj_zero [simp]: "cnj 0 = 0"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   423
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   424
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   425
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   426
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   427
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   428
lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   429
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   430
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   431
lemma cnj_setsum [simp]: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   432
  by (induct s rule: infinite_finite_induct) auto
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   433
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   434
lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   435
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   436
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   437
lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   438
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   439
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   440
lemma complex_cnj_one [simp]: "cnj 1 = 1"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   441
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   442
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   443
lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   444
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   445
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   446
lemma cnj_setprod [simp]: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   447
  by (induct s rule: infinite_finite_induct) auto
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   448
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   449
lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   450
  by (simp add: complex_eq_iff)
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   451
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   452
lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   453
  by (simp add: divide_complex_def)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   454
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   455
lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   456
  by (induct n) simp_all
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   457
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   458
lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   459
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   460
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   461
lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   462
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   463
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44902
diff changeset
   464
lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44902
diff changeset
   465
  by (simp add: complex_eq_iff)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44902
diff changeset
   466
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54230
diff changeset
   467
lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   468
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   469
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   470
lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   471
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   472
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   473
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   474
  by (simp add: norm_complex_def)
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   475
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   476
lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   477
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   478
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   479
lemma complex_cnj_i [simp]: "cnj ii = - ii"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   480
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   481
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   482
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   483
  by (simp add: complex_eq_iff)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   484
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   485
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   486
  by (simp add: complex_eq_iff)
14354
988aa4648597 types complex and hcomplex are now instances of class ringpower:
paulson
parents: 14353
diff changeset
   487
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51002
diff changeset
   488
lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   489
  by (simp add: complex_eq_iff power2_eq_square)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   490
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51002
diff changeset
   491
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"
44724
0b900a9d8023 tuned indentation
huffman
parents: 44715
diff changeset
   492
  by (simp add: norm_mult power2_eq_square)
23125
6f7b5b96241f cleaned up proofs; reorganized sections; removed redundant lemmas
huffman
parents: 23124
diff changeset
   493
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   494
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   495
  by (simp add: norm_complex_def power2_eq_square)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   496
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   497
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   498
  by simp
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   499
44290
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   500
lemma bounded_linear_cnj: "bounded_linear cnj"
44127
7b57b9295d98 lemma bounded_linear_intro
huffman
parents: 44065
diff changeset
   501
  using complex_cnj_add complex_cnj_scaleR
7b57b9295d98 lemma bounded_linear_intro
huffman
parents: 44065
diff changeset
   502
  by (rule bounded_linear_intro [where K=1], simp)
14354
988aa4648597 types complex and hcomplex are now instances of class ringpower:
paulson
parents: 14353
diff changeset
   503
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   504
lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   505
lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   506
lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   507
lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56369
diff changeset
   508
lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
44290
23a5137162ea remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman
parents: 44127
diff changeset
   509
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   510
lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   511
  by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   512
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   513
lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   514
  by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   515
14354
988aa4648597 types complex and hcomplex are now instances of class ringpower:
paulson
parents: 14353
diff changeset
   516
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   517
subsection\<open>Basic Lemmas\<close>
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   518
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   519
lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   520
  by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   521
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   522
lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   523
  by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   524
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   525
lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   526
by (cases z)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   527
   (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   528
         simp del: of_real_power)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   529
61104
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   530
lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)^2"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   531
  using complex_norm_square by auto
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   532
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   533
lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   534
  by (auto simp add: Re_divide)
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   535
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   536
lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   537
  by (auto simp add: Im_divide)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   538
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   539
lemma complex_div_gt_0:
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   540
  "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   541
proof cases
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   542
  assume "b = 0" then show ?thesis by auto
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   543
next
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   544
  assume "b \<noteq> 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   545
  then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   546
    by (simp add: complex_eq_iff sum_power2_gt_zero_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   547
  then show ?thesis
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   548
    by (simp add: Re_divide Im_divide zero_less_divide_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   549
qed
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   550
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   551
lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   552
  and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   553
  using complex_div_gt_0 by auto
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   554
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   555
lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   556
  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   557
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   558
lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   559
  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   560
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   561
lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   562
  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   563
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   564
lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   565
  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   566
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   567
lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   568
  by (metis not_le Re_complex_div_gt_0)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   569
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   570
lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   571
  by (metis Im_complex_div_gt_0 not_le)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   572
61104
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   573
lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   574
  by (simp add: Re_divide power2_eq_square)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   575
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   576
lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   577
  by (simp add: Im_divide power2_eq_square)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   578
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   579
lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   580
  by (metis Re_divide_of_real of_real_Re)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   581
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   582
lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   583
  by (metis Im_divide_of_real of_real_Re)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   584
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   585
lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   586
  by (induct s rule: infinite_finite_induct) auto
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   587
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   588
lemma Im_setsum[simp]: "Im (setsum f s) = (\<Sum>x\<in>s. Im(f x))"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   589
  by (induct s rule: infinite_finite_induct) auto
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   590
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   591
lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   592
  unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   593
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   594
lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   595
  unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   596
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   597
lemma summable_complex_of_real [simp]: "summable (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   598
  unfolding summable_complex_iff by simp
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   599
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   600
lemma summable_Re: "summable f \<Longrightarrow> summable (\<lambda>x. Re (f x))"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   601
  unfolding summable_complex_iff by blast
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   602
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   603
lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   604
  unfolding summable_complex_iff by blast
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55759
diff changeset
   605
61104
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   606
lemma complex_is_Nat_iff: "z \<in> \<nat> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_nat i)"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   607
  by (auto simp: Nats_def complex_eq_iff)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   608
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   609
lemma complex_is_Int_iff: "z \<in> \<int> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_int i)"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   610
  by (auto simp: Ints_def complex_eq_iff)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   611
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   612
lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   613
  by (auto simp: Reals_def complex_eq_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   614
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   615
lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   616
  by (auto simp: complex_is_Real_iff complex_eq_iff)
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   617
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   618
lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   619
  by (simp add: complex_is_Real_iff norm_complex_def)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   620
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   621
lemma series_comparison_complex:
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   622
  fixes f:: "nat \<Rightarrow> 'a::banach"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   623
  assumes sg: "summable g"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   624
     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   625
     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   626
  shows "summable f"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   627
proof -
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   628
  have g: "\<And>n. cmod (g n) = Re (g n)" using assms
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   629
    by (metis abs_of_nonneg in_Reals_norm)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   630
  show ?thesis
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   631
    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   632
    using sg
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   633
    apply (auto simp: summable_def)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   634
    apply (rule_tac x="Re s" in exI)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   635
    apply (auto simp: g sums_Re)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   636
    apply (metis fg g)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   637
    done
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56331
diff changeset
   638
qed
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   639
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   640
subsection\<open>Polar Form for Complex Numbers\<close>
59746
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   641
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   642
lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   643
  using sincos_total_2pi [of "Re z" "Im z"]
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   644
  by auto (metis cmod_power2 complex_eq power_one)
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   645
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   646
subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   647
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   648
primcorec cis :: "real \<Rightarrow> complex" where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   649
  "Re (cis a) = cos a"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   650
| "Im (cis a) = sin a"
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   651
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   652
lemma cis_zero [simp]: "cis 0 = 1"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   653
  by (simp add: complex_eq_iff)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   654
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   655
lemma norm_cis [simp]: "norm (cis a) = 1"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   656
  by (simp add: norm_complex_def)
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   657
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   658
lemma sgn_cis [simp]: "sgn (cis a) = cis a"
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   659
  by (simp add: sgn_div_norm)
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   660
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   661
lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   662
  by (metis norm_cis norm_zero zero_neq_one)
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   663
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   664
lemma cis_mult: "cis a * cis b = cis (a + b)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   665
  by (simp add: complex_eq_iff cos_add sin_add)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   666
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   667
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   668
  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   669
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   670
lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   671
  by (simp add: complex_eq_iff)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   672
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   673
lemma cis_divide: "cis a / cis b = cis (a - b)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   674
  by (simp add: divide_complex_def cis_mult)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   675
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   676
lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   677
  by (auto simp add: DeMoivre)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   678
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   679
lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   680
  by (auto simp add: DeMoivre)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   681
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   682
lemma cis_pi: "cis pi = -1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   683
  by (simp add: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   684
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   685
subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
44715
1a17d8913976 tuned comments
huffman
parents: 44712
diff changeset
   686
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   687
definition rcis :: "real \<Rightarrow> real \<Rightarrow> complex" where
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   688
  "rcis r a = complex_of_real r * cis a"
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   689
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   690
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   691
  by (simp add: rcis_def)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   692
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   693
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   694
  by (simp add: rcis_def)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   695
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   696
lemma rcis_Ex: "\<exists>r a. z = rcis r a"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   697
  by (simp add: complex_eq_iff polar_Ex)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   698
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   699
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   700
  by (simp add: rcis_def norm_mult)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   701
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   702
lemma cis_rcis_eq: "cis a = rcis 1 a"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   703
  by (simp add: rcis_def)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   704
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   705
lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   706
  by (simp add: rcis_def cis_mult)
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   707
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   708
lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   709
  by (simp add: rcis_def)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   710
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   711
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   712
  by (simp add: rcis_def)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   713
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   714
lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \<longleftrightarrow> r = 0"
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   715
  by (simp add: rcis_def)
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   716
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   717
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   718
  by (simp add: rcis_def power_mult_distrib DeMoivre)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   719
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   720
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   721
  by (simp add: divide_inverse rcis_def)
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   722
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   723
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   724
  by (simp add: rcis_def cis_divide [symmetric])
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   725
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   726
subsubsection \<open>Complex exponential\<close>
44827
4d1384a1fc82 Complex.thy: move theorems into appropriate subsections
huffman
parents: 44825
diff changeset
   727
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   728
abbreviation Exp :: "complex \<Rightarrow> complex"
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   729
  where "Exp \<equiv> exp"
44291
dbd9965745fd define complex exponential 'expi' as abbreviation for 'exp'
huffman
parents: 44290
diff changeset
   730
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   731
lemma cis_conv_exp: "cis b = exp (\<i> * b)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   732
proof -
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   733
  { fix n :: nat
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   734
    have "\<i> ^ n = fact n *\<^sub>R (cos_coeff n + \<i> * sin_coeff n)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   735
      by (induct n)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   736
         (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   737
                        power2_eq_square real_of_nat_Suc add_nonneg_eq_0_iff
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   738
                        real_of_nat_def[symmetric])
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   739
    then have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   740
        of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   741
      by (simp add: field_simps) }
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   742
  then show ?thesis using sin_converges [of b] cos_converges [of b]
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   743
    by (auto simp add: cis.ctr exp_def simp del: of_real_mult
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   744
             intro!: sums_unique sums_add sums_mult sums_of_real)
44291
dbd9965745fd define complex exponential 'expi' as abbreviation for 'exp'
huffman
parents: 44290
diff changeset
   745
qed
dbd9965745fd define complex exponential 'expi' as abbreviation for 'exp'
huffman
parents: 44290
diff changeset
   746
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   747
lemma Exp_eq_polar: "Exp z = exp (Re z) * cis (Im z)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   748
  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
20557
81dd3679f92c complex_of_real abbreviates of_real::real=>complex;
huffman
parents: 20556
diff changeset
   749
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   750
lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   751
  unfolding Exp_eq_polar by simp
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   752
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   753
lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   754
  unfolding Exp_eq_polar by simp
44828
3d6a79e0e1d0 add some new lemmas about cis and rcis;
huffman
parents: 44827
diff changeset
   755
59746
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   756
lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   757
  by (simp add: norm_complex_def)
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   758
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   759
lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   760
  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   761
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   762
lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
59746
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   763
  apply (insert rcis_Ex [of z])
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   764
  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   765
  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   766
  done
14323
27724f528f82 converting Complex/Complex.ML to Isar
paulson
parents: 13957
diff changeset
   767
59658
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   768
lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
0cc388370041 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents: 59613
diff changeset
   769
  by (simp add: Exp_eq_polar complex_eq_iff)
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14377
diff changeset
   770
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   771
subsubsection \<open>Complex argument\<close>
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   772
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   773
definition arg :: "complex \<Rightarrow> real" where
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   774
  "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi))"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   775
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   776
lemma arg_zero: "arg 0 = 0"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   777
  by (simp add: arg_def)
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   778
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   779
lemma arg_unique:
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   780
  assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   781
  shows "arg z = x"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   782
proof -
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   783
  from assms have "z \<noteq> 0" by auto
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   784
  have "(SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi) = x"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   785
  proof
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   786
    fix a def d \<equiv> "a - x"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   787
    assume a: "sgn z = cis a \<and> - pi < a \<and> a \<le> pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   788
    from a assms have "- (2*pi) < d \<and> d < 2*pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   789
      unfolding d_def by simp
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   790
    moreover from a assms have "cos a = cos x" and "sin a = sin x"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   791
      by (simp_all add: complex_eq_iff)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   792
    hence cos: "cos d = 1" unfolding d_def cos_diff by simp
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53015
diff changeset
   793
    moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   794
    ultimately have "d = 0"
58709
efdc6c533bd3 prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents: 58146
diff changeset
   795
      unfolding sin_zero_iff
58740
cb9d84d3e7f2 turn even into an abbreviation
haftmann
parents: 58709
diff changeset
   796
      by (auto elim!: evenE dest!: less_2_cases)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   797
    thus "a = x" unfolding d_def by simp
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   798
  qed (simp add: assms del: Re_sgn Im_sgn)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   799
  with \<open>z \<noteq> 0\<close> show "arg z = x"
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   800
    unfolding arg_def by simp
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   801
qed
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   802
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   803
lemma arg_correct:
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   804
  assumes "z \<noteq> 0" shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   805
proof (simp add: arg_def assms, rule someI_ex)
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   806
  obtain r a where z: "z = rcis r a" using rcis_Ex by fast
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   807
  with assms have "r \<noteq> 0" by auto
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   808
  def b \<equiv> "if 0 < r then a else a + pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   809
  have b: "sgn z = cis b"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   810
    unfolding z b_def rcis_def using \<open>r \<noteq> 0\<close>
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   811
    by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   812
  have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   813
    by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   814
  have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   815
    by (case_tac x rule: int_diff_cases)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   816
       (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   817
  def c \<equiv> "b - 2*pi * of_int \<lceil>(b - pi) / (2*pi)\<rceil>"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   818
  have "sgn z = cis c"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   819
    unfolding b c_def
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   820
    by (simp add: cis_divide [symmetric] cis_2pi_int)
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   821
  moreover have "- pi < c \<and> c \<le> pi"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   822
    using ceiling_correct [of "(b - pi) / (2*pi)"]
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   823
    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   824
  ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   825
qed
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   826
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   827
lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   828
  by (cases "z = 0") (simp_all add: arg_zero arg_correct)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   829
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   830
lemma cis_arg: "z \<noteq> 0 \<Longrightarrow> cis (arg z) = sgn z"
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   831
  by (simp add: arg_correct)
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   832
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   833
lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   834
  by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   835
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   836
lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   837
  using cis_arg [of y] by (simp add: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   838
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   839
subsection \<open>Square root of complex numbers\<close>
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   840
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   841
primcorec csqrt :: "complex \<Rightarrow> complex" where
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   842
  "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   843
| "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   844
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   845
lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \<Longrightarrow> Re x \<ge> 0 \<Longrightarrow> csqrt x = sqrt (Re x)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   846
  by (simp add: complex_eq_iff norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   847
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   848
lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \<Longrightarrow> Re x \<le> 0 \<Longrightarrow> csqrt x = \<i> * sqrt \<bar>Re x\<bar>"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   849
  by (simp add: complex_eq_iff norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   850
59862
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59746
diff changeset
   851
lemma of_real_sqrt: "x \<ge> 0 \<Longrightarrow> of_real (sqrt x) = csqrt (of_real x)"
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59746
diff changeset
   852
  by (simp add: complex_eq_iff norm_complex_def)
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59746
diff changeset
   853
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   854
lemma csqrt_0 [simp]: "csqrt 0 = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   855
  by simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   856
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   857
lemma csqrt_1 [simp]: "csqrt 1 = 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   858
  by simp
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   859
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   860
lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   861
  by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   862
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   863
lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   864
proof cases
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   865
  assume "Im z = 0" then show ?thesis
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   866
    using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   867
    by (cases "0::real" "Re z" rule: linorder_cases)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   868
       (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   869
next
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   870
  assume "Im z \<noteq> 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   871
  moreover
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   872
  have "cmod z * cmod z - Re z * Re z = Im z * Im z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   873
    by (simp add: norm_complex_def power2_eq_square)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   874
  moreover
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   875
  have "\<bar>Re z\<bar> \<le> cmod z"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   876
    by (simp add: norm_complex_def)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   877
  ultimately show ?thesis
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   878
    by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   879
                  field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   880
qed
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   881
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   882
lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   883
  by auto (metis power2_csqrt power_eq_0_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   884
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   885
lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   886
  by auto (metis power2_csqrt power2_eq_1_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   887
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   888
lemma csqrt_principal: "0 < Re (csqrt z) \<or> Re (csqrt z) = 0 \<and> 0 \<le> Im (csqrt z)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   889
  by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   890
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   891
lemma Re_csqrt: "0 \<le> Re (csqrt z)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   892
  by (metis csqrt_principal le_less)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   893
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   894
lemma csqrt_square:
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   895
  assumes "0 < Re b \<or> (Re b = 0 \<and> 0 \<le> Im b)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   896
  shows "csqrt (b^2) = b"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   897
proof -
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   898
  have "csqrt (b^2) = b \<or> csqrt (b^2) = - b"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   899
    unfolding power2_eq_iff[symmetric] by (simp add: power2_csqrt)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   900
  moreover have "csqrt (b^2) \<noteq> -b \<or> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   901
    using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   902
  ultimately show ?thesis
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   903
    by auto
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   904
qed
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   905
59746
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   906
lemma csqrt_unique:
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   907
    "w^2 = z \<Longrightarrow> (0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w) \<Longrightarrow> csqrt z = w"
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   908
  by (auto simp: csqrt_square)
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   909
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59000
diff changeset
   910
lemma csqrt_minus [simp]:
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   911
  assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   912
  shows "csqrt (- x) = \<i> * csqrt x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   913
proof -
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   914
  have "csqrt ((\<i> * csqrt x)^2) = \<i> * csqrt x"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   915
  proof (rule csqrt_square)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   916
    have "Im (csqrt x) \<le> 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   917
      using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   918
    then show "0 < Re (\<i> * csqrt x) \<or> Re (\<i> * csqrt x) = 0 \<and> 0 \<le> Im (\<i> * csqrt x)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   919
      by (auto simp add: Re_csqrt simp del: csqrt.simps)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   920
  qed
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   921
  also have "(\<i> * csqrt x)^2 = - x"
59746
ddae5727c5a9 new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents: 59741
diff changeset
   922
    by (simp add: power_mult_distrib)
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   923
  finally show ?thesis .
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   924
qed
44844
f74a4175a3a8 prove existence, uniqueness, and other properties of complex arg function
huffman
parents: 44843
diff changeset
   925
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   926
text \<open>Legacy theorem names\<close>
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   927
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   928
lemmas expand_complex_eq = complex_eq_iff
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   929
lemmas complex_Re_Im_cancel_iff = complex_eq_iff
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   930
lemmas complex_equality = complex_eqI
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   931
lemmas cmod_def = norm_complex_def
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   932
lemmas complex_norm_def = norm_complex_def
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   933
lemmas complex_divide_def = divide_complex_def
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   934
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   935
lemma legacy_Complex_simps:
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   936
  shows Complex_eq_0: "Complex a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   937
    and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   938
    and complex_minus: "- (Complex a b) = Complex (- a) (- b)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   939
    and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   940
    and Complex_eq_1: "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   941
    and Complex_eq_neg_1: "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   942
    and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   943
    and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   944
    and Complex_eq_numeral: "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   945
    and Complex_eq_neg_numeral: "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   946
    and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   947
    and Complex_eq_i: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   948
    and i_mult_Complex: "ii * Complex a b = Complex (- b) a"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   949
    and Complex_mult_i: "Complex a b * ii = Complex (- b) a"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   950
    and i_complex_of_real: "ii * complex_of_real r = Complex 0 r"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   951
    and complex_of_real_i: "complex_of_real r * ii = Complex 0 r"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   952
    and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   953
    and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   954
    and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   955
    and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   956
    and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   957
    and complex_cn: "cnj (Complex a b) = Complex a (- b)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   958
    and Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   959
    and Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   960
    and complex_of_real_def: "complex_of_real r = Complex r 0"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   961
    and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   962
  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   963
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   964
lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56541
diff changeset
   965
  by (metis Reals_of_real complex_of_real_def)
44065
eb64ffccfc75 standard theorem naming scheme: complex_eqI, complex_eq_iff
huffman
parents: 41959
diff changeset
   966
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   967
end