(*  Title:       Complex.thy

    Author:      Jacques D. Fleuriot

    Copyright:   2001 University of Edinburgh

    Description: Complex numbers

*)

theory Complex = HLog:

typedef complex = "{p::(real*real). True}"

  by blast

instance complex :: zero ..

instance complex :: one ..

instance complex :: plus ..

instance complex :: times ..

instance complex :: minus ..

instance complex :: inverse ..

instance complex :: power ..

consts

  "ii"    :: complex        ("ii")

constdefs

  (*--- real and Imaginary parts ---*)

  Re :: "complex => real"

  "Re(z) == fst(Rep_complex z)"

  Im :: "complex => real"

  "Im(z) == snd(Rep_complex z)"

  (*----------- modulus ------------*)

  cmod :: "complex => real"

  "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"

  (*----- injection from reals -----*)

  complex_of_real :: "real => complex"

  "complex_of_real r == Abs_complex(r,0::real)"

  (*------- complex conjugate ------*)

  cnj :: "complex => complex"

  "cnj z == Abs_complex(Re z, -Im z)"

  (*------------ Argand -------------*)

  sgn :: "complex => complex"

  "sgn z == z / complex_of_real(cmod z)"

  arg :: "complex => real"

  "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"

defs (overloaded)

  complex_zero_def:

  "0 == Abs_complex(0::real,0)"

  complex_one_def:

  "1 == Abs_complex(1,0::real)"

  (*------ imaginary unit ----------*)

  i_def:

  "ii == Abs_complex(0::real,1)"

  (*----------- negation -----------*)

  complex_minus_def:

  "- (z::complex) == Abs_complex(-Re z, -Im z)"

  (*----------- inverse -----------*)

  complex_inverse_def:

  "inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2),

                            -Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))"

  complex_add_def:

  "w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))"

  complex_diff_def:

  "w - (z::complex) == w + -(z::complex)"

  complex_mult_def:

  "w * (z::complex) == Abs_complex(Re(w) * Re(z) - Im(w) * Im(z),

			Re(w) * Im(z) + Im(w) * Re(z))"

  (*----------- division ----------*)

  complex_divide_def:

  "w / (z::complex) == w * inverse z"

constdefs

  (* abbreviation for (cos a + i sin a) *)

  cis :: "real => complex"

  "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"

  (* abbreviation for r*(cos a + i sin a) *)

  rcis :: "[real, real] => complex"

  "rcis r a == complex_of_real r * cis a"

  (* e ^ (x + iy) *)

  expi :: "complex => complex"

  "expi z == complex_of_real(exp (Re z)) * cis (Im z)"

lemma inj_Rep_complex: "inj Rep_complex"

apply (rule inj_on_inverseI)

apply (rule Rep_complex_inverse)

done

lemma inj_Abs_complex: "inj Abs_complex"

apply (rule inj_on_inverseI)

apply (rule Abs_complex_inverse)

apply (simp (no_asm) add: complex_def)

done

declare inj_Abs_complex [THEN injD, simp]

lemma Abs_complex_cancel_iff: "(Abs_complex x = Abs_complex y) = (x = y)"

by (auto dest: inj_Abs_complex [THEN injD])

declare Abs_complex_cancel_iff [simp]

lemma pair_mem_complex: "(x,y) : complex"

by (unfold complex_def, auto)

declare pair_mem_complex [simp]

lemma Abs_complex_inverse2: "Rep_complex (Abs_complex (x,y)) = (x,y)"

apply (simp (no_asm) add: Abs_complex_inverse)

done

declare Abs_complex_inverse2 [simp]

lemma eq_Abs_complex: "(!!x y. z = Abs_complex(x,y) ==> P) ==> P"

apply (rule_tac p = "Rep_complex z" in PairE)

apply (drule_tac f = Abs_complex in arg_cong)

apply (force simp add: Rep_complex_inverse)

done

lemma Re: "Re(Abs_complex(x,y)) = x"

apply (unfold Re_def)

apply (simp (no_asm))

done

declare Re [simp]

lemma Im: "Im(Abs_complex(x,y)) = y"

apply (unfold Im_def)

apply (simp (no_asm))

done

declare Im [simp]

lemma Abs_complex_cancel: "Abs_complex(Re(z),Im(z)) = z"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp))

done

declare Abs_complex_cancel [simp]

lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"

apply (rule_tac z = w in eq_Abs_complex)

apply (rule_tac z = z in eq_Abs_complex)

apply (auto dest: inj_Abs_complex [THEN injD])

done

lemma complex_Re_zero: "Re 0 = 0"

apply (unfold complex_zero_def)

apply (simp (no_asm))

done

lemma complex_Im_zero: "Im 0 = 0"

apply (unfold complex_zero_def)

apply (simp (no_asm))

done

declare complex_Re_zero [simp] complex_Im_zero [simp]

lemma complex_Re_one: "Re 1 = 1"

apply (unfold complex_one_def)

apply (simp (no_asm))

done

declare complex_Re_one [simp]

lemma complex_Im_one: "Im 1 = 0"

apply (unfold complex_one_def)

apply (simp (no_asm))

done

declare complex_Im_one [simp]

lemma complex_Re_i: "Re(ii) = 0"

by (unfold i_def, auto)

declare complex_Re_i [simp]

lemma complex_Im_i: "Im(ii) = 1"

by (unfold i_def, auto)

declare complex_Im_i [simp]

lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0"

apply (unfold complex_of_real_def)

apply (simp (no_asm))

done

declare Re_complex_of_real_zero [simp]

lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0"

apply (unfold complex_of_real_def)

apply (simp (no_asm))

done

declare Im_complex_of_real_zero [simp]

lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1"

apply (unfold complex_of_real_def)

apply (simp (no_asm))

done

declare Re_complex_of_real_one [simp]

lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0"

apply (unfold complex_of_real_def)

apply (simp (no_asm))

done

declare Im_complex_of_real_one [simp]

lemma Re_complex_of_real: "Re(complex_of_real z) = z"

by (unfold complex_of_real_def, auto)

declare Re_complex_of_real [simp]

lemma Im_complex_of_real: "Im(complex_of_real z) = 0"

by (unfold complex_of_real_def, auto)

declare Im_complex_of_real [simp]

subsection{*Negation*}

lemma complex_minus: "- Abs_complex(x,y) = Abs_complex(-x,-y)"

apply (unfold complex_minus_def)

apply (simp (no_asm))

done

lemma complex_Re_minus: "Re (-z) = - Re z"

apply (unfold Re_def)

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_minus)

done

lemma complex_Im_minus: "Im (-z) = - Im z"

apply (unfold Im_def)

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_minus)

done

lemma complex_minus_minus: "- (- z) = (z::complex)"

apply (unfold complex_minus_def)

apply (simp (no_asm))

done

declare complex_minus_minus [simp]

lemma inj_complex_minus: "inj(%r::complex. -r)"

apply (rule inj_onI)

apply (drule_tac f = uminus in arg_cong, simp)

done

lemma complex_minus_zero: "-(0::complex) = 0"

apply (unfold complex_zero_def)

apply (simp (no_asm) add: complex_minus)

done

declare complex_minus_zero [simp]

lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))"

apply (rule_tac z = x in eq_Abs_complex)

apply (auto dest: inj_Abs_complex [THEN injD]

            simp add: complex_zero_def complex_minus)

done

declare complex_minus_zero_iff [simp]

lemma complex_minus_zero_iff2: "(0 = -x) = (x = (0::real))"

by (auto dest: sym)

declare complex_minus_zero_iff2 [simp]

lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))"

by auto

subsection{*Addition*}

lemma complex_add:

      "Abs_complex(x1,y1) + Abs_complex(x2,y2) = Abs_complex(x1+x2,y1+y2)"

apply (unfold complex_add_def)

apply (simp (no_asm))

done

lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)"

apply (unfold Re_def)

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_add)

done

lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)"

apply (unfold Im_def)

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_add)

done

lemma complex_add_commute: "(u::complex) + v = v + u"

apply (unfold complex_add_def)

apply (simp (no_asm) add: real_add_commute)

done

lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)"

apply (unfold complex_add_def)

apply (simp (no_asm) add: real_add_assoc)

done

lemma complex_add_left_commute: "(x::complex) + (y + z) = y + (x + z)"

apply (unfold complex_add_def)

apply (simp (no_asm) add: add_left_commute)

done

lemmas complex_add_ac = complex_add_assoc complex_add_commute

                      complex_add_left_commute

lemma complex_add_zero_left: "(0::complex) + z = z"

apply (unfold complex_add_def complex_zero_def)

apply (simp (no_asm))

done

declare complex_add_zero_left [simp]

lemma complex_add_zero_right: "z + (0::complex) = z"

apply (unfold complex_add_def complex_zero_def)

apply (simp (no_asm))

done

declare complex_add_zero_right [simp]

lemma complex_add_minus_right_zero:

      "z + -z = (0::complex)"

apply (unfold complex_add_def complex_minus_def complex_zero_def)

apply (simp (no_asm))

done

declare complex_add_minus_right_zero [simp]

lemma complex_add_minus_left:

      "-z + z = (0::complex)"

apply (unfold complex_add_def complex_minus_def complex_zero_def)

apply (simp (no_asm))

done

lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"

apply (simp (no_asm) add: complex_add_assoc [symmetric])

done

lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"

by (simp add: complex_add_minus_left complex_add_assoc [symmetric])

declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]

lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y"

by (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus)

lemma complex_minus_add_distrib: "-(x + y) = -x + -(y::complex)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_minus complex_add)

done

declare complex_minus_add_distrib [simp]

lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"

apply safe

apply (drule_tac f = "%t.-x + t" in arg_cong)

apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])

done

declare complex_add_left_cancel [iff]

lemma complex_add_right_cancel: "(y + (x::complex)= z + x) = (y = z)"

apply (simp (no_asm) add: complex_add_commute)

done

declare complex_add_right_cancel [simp]

lemma complex_eq_minus_iff: "((x::complex) = y) = (0 = x + - y)"

apply safe

apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)

done

lemma complex_eq_minus_iff2: "((x::complex) = y) = (x + - y = 0)"

apply safe

apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)

done

lemma complex_diff_0: "(0::complex) - x = -x"

apply (simp (no_asm) add: complex_diff_def)

done

lemma complex_diff_0_right: "x - (0::complex) = x"

apply (simp (no_asm) add: complex_diff_def)

done

lemma complex_diff_self: "x - x = (0::complex)"

apply (simp (no_asm) add: complex_diff_def)

done

declare complex_diff_0 [simp] complex_diff_0_right [simp] complex_diff_self [simp]

lemma complex_diff:

      "Abs_complex(x1,y1) - Abs_complex(x2,y2) = Abs_complex(x1-x2,y1-y2)"

apply (unfold complex_diff_def)

apply (simp (no_asm) add: complex_add complex_minus)

done

lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"

by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)

subsection{*Multiplication*}

lemma complex_mult:

      "Abs_complex(x1,y1) * Abs_complex(x2,y2) =

       Abs_complex(x1*x2 - y1*y2,x1*y2 + y1*x2)"

apply (unfold complex_mult_def)

apply (simp (no_asm))

done

lemma complex_mult_commute: "(w::complex) * z = z * w"

apply (unfold complex_mult_def)

apply (simp (no_asm) add: real_mult_commute real_add_commute)

done

lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"

apply (unfold complex_mult_def)

apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc right_diff_distrib right_distrib left_diff_distrib left_distrib mult_left_commute)

done

lemma complex_mult_left_commute: "(x::complex) * (y * z) = y * (x * z)"

apply (unfold complex_mult_def)

apply (simp (no_asm) add: complex_Re_Im_cancel_iff mult_left_commute right_diff_distrib right_distrib)

done

lemmas complex_mult_ac = complex_mult_assoc complex_mult_commute

                      complex_mult_left_commute

lemma complex_mult_one_left: "(1::complex) * z = z"

apply (unfold complex_one_def)

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_mult)

done

declare complex_mult_one_left [simp]

lemma complex_mult_one_right: "z * (1::complex) = z"

apply (simp (no_asm) add: complex_mult_commute)

done

declare complex_mult_one_right [simp]

lemma complex_mult_zero_left: "(0::complex) * z = 0"

apply (unfold complex_zero_def)

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_mult)

done

declare complex_mult_zero_left [simp]

lemma complex_mult_zero_right: "z * 0 = (0::complex)"

apply (simp (no_asm) add: complex_mult_commute)

done

declare complex_mult_zero_right [simp]

lemma complex_divide_zero: "0 / z = (0::complex)"

by (unfold complex_divide_def, auto)

declare complex_divide_zero [simp]

lemma complex_minus_mult_eq1: "-(x * y) = -x * (y::complex)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_mult complex_minus real_diff_def)

done

lemma complex_minus_mult_eq2: "-(x * y) = x * -(y::complex)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_mult complex_minus real_diff_def)

done

lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)"

apply (rule_tac z = z1 in eq_Abs_complex)

apply (rule_tac z = z2 in eq_Abs_complex)

apply (rule_tac z = w in eq_Abs_complex)

apply (auto simp add: complex_mult complex_add left_distrib real_diff_def add_ac)

done

lemma complex_add_mult_distrib2: "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)"

apply (rule_tac z1 = "z1 + z2" in complex_mult_commute [THEN ssubst])

apply (simp (no_asm) add: complex_add_mult_distrib)

apply (simp (no_asm) add: complex_mult_commute)

done

lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1"

apply (unfold complex_zero_def complex_one_def)

apply (simp (no_asm) add: complex_Re_Im_cancel_iff)

done

declare complex_zero_not_eq_one [simp]

declare complex_zero_not_eq_one [THEN not_sym, simp]

subsection{*Inverse*}

lemma complex_inverse:

     "inverse (Abs_complex(x,y)) =

      Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"

apply (unfold complex_inverse_def)

apply (simp (no_asm))

done

lemma COMPLEX_INVERSE_ZERO: "inverse 0 = (0::complex)"

by (unfold complex_inverse_def complex_zero_def, auto)

lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0"

apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO)

done

instance complex :: division_by_zero

proof

  fix x :: complex

  show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO)

  show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 

qed

lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_mult complex_inverse complex_one_def 

       complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)

apply (drule_tac y = y in real_sum_squares_not_zero)

apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)

done

declare complex_mult_inv_left [simp]

lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1"

by (auto intro: complex_mult_commute [THEN subst])

declare complex_mult_inv_right [simp]

subsection {* The field of complex numbers *}

instance complex :: field

proof

  fix z u v w :: complex

  show "(u + v) + w = u + (v + w)"

    by (rule complex_add_assoc) 

  show "z + w = w + z"

    by (rule complex_add_commute) 

  show "0 + z = z"

    by (rule complex_add_zero_left) 

  show "-z + z = 0"

    by (rule complex_add_minus_left) 

  show "z - w = z + -w"

    by (simp add: complex_diff_def)

  show "(u * v) * w = u * (v * w)"

    by (rule complex_mult_assoc) 

  show "z * w = w * z"

    by (rule complex_mult_commute) 

  show "1 * z = z"

    by (rule complex_mult_one_left) 

  show "0 \<noteq> (1::complex)"

    by (rule complex_zero_not_eq_one) 

  show "(u + v) * w = u * w + v * w"

    by (rule complex_add_mult_distrib) 

  show "z+u = z+v ==> u=v"

    proof -

      assume eq: "z+u = z+v" 

      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)

      thus "u = v" by (simp add: complex_add_minus_left)

    qed

  assume neq: "w \<noteq> 0"

  thus "z / w = z * inverse w"

    by (simp add: complex_divide_def)

  show "inverse w * w = 1"

    by (simp add: neq complex_mult_inv_left) 

qed

lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"

apply (simp)

done

subsection{*Embedding Properties for @{term complex_of_real} Map*}

lemma inj_complex_of_real: "inj complex_of_real"

apply (rule inj_onI)

apply (auto dest: inj_Abs_complex [THEN injD] simp add: complex_of_real_def)

done

lemma complex_of_real_one:

      "complex_of_real 1 = 1"

apply (unfold complex_one_def complex_of_real_def)

apply (rule refl)

done

declare complex_of_real_one [simp]

lemma complex_of_real_zero:

      "complex_of_real 0 = 0"

apply (unfold complex_zero_def complex_of_real_def)

apply (rule refl)

done

declare complex_of_real_zero [simp]

lemma complex_of_real_eq_iff:

     "(complex_of_real x = complex_of_real y) = (x = y)"

by (auto dest: inj_complex_of_real [THEN injD])

declare complex_of_real_eq_iff [iff]

lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"

apply (simp (no_asm) add: complex_of_real_def complex_minus)

done

lemma complex_of_real_inverse:

 "complex_of_real(inverse x) = inverse(complex_of_real x)"

apply (case_tac "x=0", simp)

apply (simp add: complex_inverse complex_of_real_def real_divide_def 

                 inverse_mult_distrib power2_eq_square)

done

lemma complex_of_real_add:

 "complex_of_real x + complex_of_real y = complex_of_real (x + y)"

apply (simp (no_asm) add: complex_add complex_of_real_def)

done

lemma complex_of_real_diff:

 "complex_of_real x - complex_of_real y = complex_of_real (x - y)"

apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)

done

lemma complex_of_real_mult:

 "complex_of_real x * complex_of_real y = complex_of_real (x * y)"

apply (simp (no_asm) add: complex_mult complex_of_real_def)

done

lemma complex_of_real_divide:

      "complex_of_real x / complex_of_real y = complex_of_real(x/y)"

apply (unfold complex_divide_def)

apply (case_tac "y=0")

apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)

apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)

done

lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)"

apply (unfold cmod_def)

apply (simp (no_asm))

done

lemma complex_mod_zero: "cmod(0) = 0"

apply (unfold cmod_def)

apply (simp (no_asm))

done

declare complex_mod_zero [simp]

lemma complex_mod_one [simp]: "cmod(1) = 1"

by (simp add: cmod_def power2_eq_square)

lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"

apply (simp add: complex_of_real_def power2_eq_square complex_mod)

done

declare complex_mod_complex_of_real [simp]

lemma complex_of_real_abs:

     "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"

by (simp)

subsection{*Conjugation is an Automorphism*}

lemma complex_cnj: "cnj (Abs_complex(x,y)) = Abs_complex(x,-y)"

apply (unfold cnj_def)

apply (simp (no_asm))

done

lemma inj_cnj: "inj cnj"

apply (rule inj_onI)

apply (auto simp add: cnj_def Abs_complex_cancel_iff complex_Re_Im_cancel_iff)

done

lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)"

by (auto dest: inj_cnj [THEN injD])

declare complex_cnj_cancel_iff [simp]

lemma complex_cnj_cnj: "cnj (cnj z) = z"

apply (unfold cnj_def)

apply (simp (no_asm))

done

declare complex_cnj_cnj [simp]

lemma complex_cnj_complex_of_real:

 "cnj (complex_of_real x) = complex_of_real x"

apply (unfold complex_of_real_def)

apply (simp (no_asm) add: complex_cnj)

done

declare complex_cnj_complex_of_real [simp]

lemma complex_mod_cnj: "cmod (cnj z) = cmod z"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square)

done

declare complex_mod_cnj [simp]

lemma complex_cnj_minus: "cnj (-z) = - cnj z"

apply (unfold cnj_def)

apply (simp (no_asm) add: complex_minus complex_Re_minus complex_Im_minus)

done

lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square)

done

lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"

apply (rule_tac z = w in eq_Abs_complex)

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_cnj complex_add)

done

lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"

apply (unfold complex_diff_def)

apply (simp (no_asm) add: complex_cnj_add complex_cnj_minus)

done

lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"

apply (rule_tac z = w in eq_Abs_complex)

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_cnj complex_mult)

done

lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"

apply (unfold complex_divide_def)

apply (simp (no_asm) add: complex_cnj_mult complex_cnj_inverse)

done

lemma complex_cnj_one: "cnj 1 = 1"

apply (unfold cnj_def complex_one_def)

apply (simp (no_asm))

done

declare complex_cnj_one [simp]

lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def)

done

lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def 

                 complex_minus i_def complex_mult)

done

lemma complex_cnj_zero [simp]: "cnj 0 = 0"

by (simp add: cnj_def complex_zero_def)

lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_zero_def complex_cnj)

done

declare complex_cnj_zero_iff [iff]

lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)

done

subsection{*Algebra*}

lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"

apply (unfold complex_zero_def)

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_add)

done

declare complex_add_left_cancel_zero [simp]

lemma complex_diff_mult_distrib:

      "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)"

apply (unfold complex_diff_def)

apply (simp (no_asm) add: complex_add_mult_distrib)

done

lemma complex_diff_mult_distrib2:

      "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)"

apply (unfold complex_diff_def)

apply (simp (no_asm) add: complex_add_mult_distrib2)

done

subsection{*Modulus*}

lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"

apply (rule_tac z = x in eq_Abs_complex)

apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square)

done

declare complex_mod_eq_zero_cancel [simp]

lemma complex_mod_complex_of_real_of_nat: "cmod (complex_of_real(real (n::nat))) = real n"

apply (simp (no_asm))

done

declare complex_mod_complex_of_real_of_nat [simp]

lemma complex_mod_minus: "cmod (-x) = cmod(x)"

apply (rule_tac z = x in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square)

done

declare complex_mod_minus [simp]

lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"

apply (rule_tac z = z in eq_Abs_complex)

apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult);

apply (simp (no_asm) add: power2_eq_square real_abs_def)

done

lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"

by (unfold cmod_def, auto)

lemma complex_mod_ge_zero: "0 \<le> cmod x"

apply (unfold cmod_def)

apply (auto intro: real_sqrt_ge_zero)

done

declare complex_mod_ge_zero [simp]

lemma abs_cmod_cancel: "abs(cmod x) = cmod x"

by (auto intro: abs_eqI1)

declare abs_cmod_cancel [simp]

lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)

apply (rule_tac n = 1 in power_inject_base)

apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)

apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac)

done

lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)

apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)

done

lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)

done

declare complex_Re_mult_cnj_le_cmod [simp]

lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"

apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod)

apply (simp add: complex_mod_mult)

done

declare complex_Re_mult_cnj_le_cmod2 [simp]

lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"

apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)

done

lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"

apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])

done

declare complex_mod_triangle_squared [simp]

lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"

apply (rule order_trans [OF _ complex_mod_ge_zero]) 

apply (simp (no_asm))

done

declare complex_mod_minus_le_complex_mod [simp]

lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"

apply (rule_tac n = 1 in realpow_increasing)

apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]

            simp add: power2_eq_square [symmetric])

done

declare complex_mod_triangle_ineq [simp]

lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"

apply (cut_tac x1 = b and y1 = a and c = "-cmod b" 

       in complex_mod_triangle_ineq [THEN add_right_mono])

apply (simp (no_asm))

done

declare complex_mod_triangle_ineq2 [simp]

lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"

apply (rule_tac z = x in eq_Abs_complex)

apply (rule_tac z = y in eq_Abs_complex)

apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)

done

lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"

by (auto intro: order_le_less_trans complex_mod_triangle_ineq)

lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"

by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)

lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)"

apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])

apply auto

apply (rule order_trans [of _ 0], rule order_less_imp_le)

apply (simp add: compare_rls, simp)  

apply (simp add: compare_rls)

apply (rule complex_mod_minus [THEN subst])

apply (rule order_trans)

apply (rule_tac [2] complex_mod_triangle_ineq)

apply (auto simp add: complex_add_ac)

done

declare complex_mod_diff_ineq [simp]

lemma complex_Re_le_cmod: "Re z \<le> cmod z"

apply (rule_tac z = z in eq_Abs_complex)

apply (auto simp add: complex_mod simp del: realpow_Suc)

done

declare complex_Re_le_cmod [simp]

lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"

apply (cut_tac x = z in complex_mod_ge_zero)

apply (drule order_le_imp_less_or_eq, auto)

done

subsection{*A Few More Theorems*}

lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"

apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO)

apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])

apply (auto simp add: complex_mod_mult [symmetric])

done

lemma complex_mod_divide:

      "cmod(x/y) = cmod(x)/(cmod y)"

apply (unfold complex_divide_def real_divide_def)

apply (auto simp add: complex_mod_mult complex_mod_inverse)

done

lemma complex_inverse_divide:

      "inverse(x/y) = y/(x::complex)"

apply (unfold complex_divide_def)

apply (auto simp add: inverse_mult_distrib complex_mult_commute)

done

declare complex_inverse_divide [simp]

subsection{*Exponentiation*}

primrec

     complexpow_0:   "z ^ 0       = 1"

     complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"

instance complex :: ringpower

proof

  fix z :: complex

  fix n :: nat

  show "z^0 = 1" by simp

  show "z^(Suc n) = z * (z^n)" by simp

qed

lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"

apply (induct_tac "n")

apply (auto simp add: complex_of_real_mult [symmetric])

done

lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"

apply (induct_tac "n")

apply (auto simp add: complex_cnj_mult)

done

lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"

apply (induct_tac "n")

apply (auto simp add: complex_mod_mult)

done

lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"

by (induct_tac "n", auto)

lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"

by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)

lemma complex_i_not_zero [simp]: "ii \<noteq> 0"

by (unfold i_def complex_zero_def, auto)

subsection{*The Function @{term sgn}*}

lemma sgn_zero: "sgn 0 = 0"

apply (unfold sgn_def)

apply (simp (no_asm))

done

declare sgn_zero [simp]

lemma sgn_one: "sgn 1 = 1"

apply (unfold sgn_def)

apply (simp (no_asm))

done