src/HOL/Complex/Complex.ML

HOL-Real -> HOL-Complex

(*  Title:       Complex.ML
    Author:      Jacques D. Fleuriot
    Copyright:   2001  University of Edinburgh
    Description: Complex numbers
*)

Goal "inj Rep_complex";
by (rtac inj_inverseI 1);
by (rtac Rep_complex_inverse 1);
qed "inj_Rep_complex";

Goal "inj Abs_complex";
by (rtac inj_inverseI 1);
by (rtac Abs_complex_inverse 1);
by (simp_tac (simpset() addsimps [complex_def]) 1);
qed "inj_Abs_complex";
Addsimps [inj_Abs_complex RS injD];

Goal "(Abs_complex x = Abs_complex y) = (x = y)";
by (auto_tac (claset() addDs [inj_Abs_complex RS injD],simpset()));
qed "Abs_complex_cancel_iff";
Addsimps [Abs_complex_cancel_iff]; 

Goalw [complex_def] "(x,y) : complex";
by (Auto_tac);
qed "pair_mem_complex";
Addsimps [pair_mem_complex];

Goal "Rep_complex (Abs_complex (x,y)) = (x,y)";
by (simp_tac (simpset() addsimps [Abs_complex_inverse]) 1);
qed "Abs_complex_inverse2";
Addsimps [Abs_complex_inverse2];

val [prem] = goal Complex.thy
    "(!!x y. z = Abs_complex(x,y) ==> P) ==> P";
by (res_inst_tac [("p","Rep_complex z")] PairE 1);
by (dres_inst_tac [("f","Abs_complex")] arg_cong 1);
by (res_inst_tac [("x","x"),("y","y")] prem 1);
by (asm_full_simp_tac (simpset() addsimps [Rep_complex_inverse]) 1);
qed "eq_Abs_complex";

Goalw [Re_def] "Re(Abs_complex(x,y)) = x";
by (Simp_tac 1);
qed "Re";
Addsimps [Re];

Goalw [Im_def] "Im(Abs_complex(x,y)) = y";
by (Simp_tac 1);
qed "Im";
Addsimps [Im];

Goal "Abs_complex(Re(z),Im(z)) = z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (Asm_simp_tac 1);
qed "Abs_complex_cancel";
Addsimps [Abs_complex_cancel];

Goal "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))";
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset() addDs [inj_Abs_complex RS injD],simpset()));
qed "complex_Re_Im_cancel_iff";

Goalw [complex_zero_def] "Re 0 = 0";
by (Simp_tac 1);
qed "complex_Re_zero";

Goalw [complex_zero_def] "Im 0 = 0";
by (Simp_tac 1);
qed "complex_Im_zero";
Addsimps [complex_Re_zero,complex_Im_zero];

Goalw [complex_one_def] "Re 1 = 1";
by (Simp_tac 1);
qed "complex_Re_one";
Addsimps [complex_Re_one];

Goalw [complex_one_def] "Im 1 = 0";
by (Simp_tac 1);
qed "complex_Im_one";
Addsimps [complex_Im_one];

Goalw [i_def] "Re(ii) = 0";
by Auto_tac;
qed "complex_Re_i";
Addsimps [complex_Re_i];

Goalw [i_def] "Im(ii) = 1";
by Auto_tac;
qed "complex_Im_i";
Addsimps [complex_Im_i];

Goalw [complex_of_real_def] "Re(complex_of_real 0) = 0";
by (Simp_tac 1);
qed "Re_complex_of_real_zero";
Addsimps [Re_complex_of_real_zero];

Goalw [complex_of_real_def] "Im(complex_of_real 0) = 0";
by (Simp_tac 1);
qed "Im_complex_of_real_zero";
Addsimps [Im_complex_of_real_zero];

Goalw [complex_of_real_def] "Re(complex_of_real 1) = 1";
by (Simp_tac 1);
qed "Re_complex_of_real_one";
Addsimps [Re_complex_of_real_one];

Goalw [complex_of_real_def] "Im(complex_of_real 1) = 0";
by (Simp_tac 1);
qed "Im_complex_of_real_one";
Addsimps [Im_complex_of_real_one];

Goalw [complex_of_real_def] "Re(complex_of_real z) = z";
by Auto_tac;
qed "Re_complex_of_real";
Addsimps [Re_complex_of_real];

Goalw [complex_of_real_def] "Im(complex_of_real z) = 0";
by Auto_tac;
qed "Im_complex_of_real";
Addsimps [Im_complex_of_real];

(*** negation ***)

Goalw [complex_minus_def] "- Abs_complex(x,y) = Abs_complex(-x,-y)";
by (Simp_tac 1);
qed "complex_minus";

Goalw [Re_def] "Re (-z) = - Re z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_minus]));
qed "complex_Re_minus";

Goalw [Im_def] "Im (-z) = - Im z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_minus]));
qed "complex_Im_minus";

Goalw [complex_minus_def] "- (- z) = (z::complex)";
by (Simp_tac 1);
qed "complex_minus_minus";
Addsimps [complex_minus_minus];

Goal "inj(%r::complex. -r)";
by (rtac injI 1);
by (dres_inst_tac [("f","uminus")] arg_cong 1);
by (Asm_full_simp_tac 1);
qed "inj_complex_minus";

Goalw [complex_zero_def] "-(0::complex) = 0";
by (simp_tac (simpset() addsimps [complex_minus]) 1);
qed "complex_minus_zero";
Addsimps [complex_minus_zero];

Goal "(-x = 0) = (x = (0::complex))"; 
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (auto_tac (claset() addDs [inj_Abs_complex RS injD],simpset() 
    addsimps [complex_zero_def,complex_minus]));
qed "complex_minus_zero_iff";
Addsimps [complex_minus_zero_iff];

Goal "(0 = -x) = (x = (0::real))"; 
by (auto_tac (claset() addDs [sym],simpset()));
qed "complex_minus_zero_iff2";
Addsimps [complex_minus_zero_iff2];

Goal "(-x ~= 0) = (x ~= (0::complex))"; 
by Auto_tac;
qed "complex_minus_not_zero_iff";

(*** addition ***)

Goalw [complex_add_def]
      "Abs_complex(x1,y1) + Abs_complex(x2,y2) = Abs_complex(x1+x2,y1+y2)";
by (Simp_tac 1);
qed "complex_add";

Goalw [Re_def] "Re(x + y) = Re(x) + Re(y)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_add]));
qed "complex_Re_add";

Goalw [Im_def] "Im(x + y) = Im(x) + Im(y)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_add]));
qed "complex_Im_add";

Goalw [complex_add_def] "(u::complex) + v = v + u";
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "complex_add_commute";

Goalw [complex_add_def] "((u::complex) + v) + w = u + (v + w)";
by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
qed "complex_add_assoc";

Goalw [complex_add_def] "(x::complex) + (y + z) = y + (x + z)";
by (simp_tac (simpset() addsimps [real_add_left_commute]) 1);
qed "complex_add_left_commute";

val complex_add_ac = [complex_add_assoc,complex_add_commute,
                      complex_add_left_commute];

Goalw [complex_add_def,complex_zero_def] "(0::complex) + z = z";
by (Simp_tac 1);
qed "complex_add_zero_left";
Addsimps [complex_add_zero_left];

Goalw [complex_add_def,complex_zero_def] "z + (0::complex) = z";
by (Simp_tac 1);
qed "complex_add_zero_right";
Addsimps [complex_add_zero_right];

Goalw [complex_add_def,complex_minus_def,complex_zero_def] 
      "z + -z = (0::complex)";
by (Simp_tac 1);
qed "complex_add_minus_right_zero";
Addsimps [complex_add_minus_right_zero];

Goalw [complex_add_def,complex_minus_def,complex_zero_def] 
      "-z + z = (0::complex)";
by (Simp_tac 1);
qed "complex_add_minus_left_zero";
Addsimps [complex_add_minus_left_zero];

Goal "z + (- z + w) = (w::complex)";
by (simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1);
qed "complex_add_minus_cancel";

Goal "(-z) + (z + w) = (w::complex)";
by (simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1);
qed "complex_minus_add_cancel";

Addsimps [complex_add_minus_cancel, complex_minus_add_cancel];

Goal "x + y = (0::complex) ==> x = -y";
by (auto_tac (claset(),simpset() addsimps [complex_Re_Im_cancel_iff,
    complex_Re_add,complex_Im_add,complex_Re_minus,complex_Im_minus]));
qed "complex_add_minus_eq_minus";

Goal "-(x + y) = -x + -(y::complex)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add]));
qed "complex_minus_add_distrib";
Addsimps [complex_minus_add_distrib];

Goal "((x::complex) + y = x + z) = (y = z)";
by (Step_tac 1);
by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1);
qed "complex_add_left_cancel";
AddIffs [complex_add_left_cancel];

Goal "(y + (x::complex)= z + x) = (y = z)";
by (simp_tac (simpset() addsimps [complex_add_commute]) 1);
qed "complex_add_right_cancel";
Addsimps [complex_add_right_cancel];

Goal "((x::complex) = y) = (0 = x + - y)";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")] 
      (complex_add_right_cancel RS iffD1) 2);
by (Auto_tac);
qed "complex_eq_minus_iff"; 

Goal "((x::complex) = y) = (x + - y = 0)";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")] 
      (complex_add_right_cancel RS iffD1) 2);
by (Auto_tac);
qed "complex_eq_minus_iff2"; 

Goal "(0::complex) - x = -x";
by (simp_tac (simpset() addsimps [complex_diff_def]) 1);
qed "complex_diff_0";

Goal "x - (0::complex) = x";
by (simp_tac (simpset() addsimps [complex_diff_def]) 1);
qed "complex_diff_0_right";

Goal "x - x = (0::complex)";
by (simp_tac (simpset() addsimps [complex_diff_def]) 1);
qed "complex_diff_self";

Addsimps [complex_diff_0, complex_diff_0_right, complex_diff_self];

Goalw [complex_diff_def]
      "Abs_complex(x1,y1) - Abs_complex(x2,y2) = Abs_complex(x1-x2,y1-y2)";
by (simp_tac (simpset() addsimps [complex_add,complex_minus]) 1);
qed "complex_diff";

Goal "((x::complex) - y = z) = (x = z + y)";
by (auto_tac (claset(),simpset() addsimps [complex_diff_def,complex_add_assoc]));
qed "complex_diff_eq_eq";

(*** complex multiplication ***)

Goalw [complex_mult_def]
      "Abs_complex(x1,y1) * Abs_complex(x2,y2) = \
\      Abs_complex(x1*x2 - y1*y2,x1*y2 + y1*x2)";
by (Simp_tac 1);
qed "complex_mult";

Goalw [complex_mult_def] "(w::complex) * z = z * w";
by (simp_tac (simpset() addsimps [real_mult_commute,real_add_commute]) 1);
qed "complex_mult_commute";

Goalw [complex_mult_def] "((u::complex) * v) * w = u * (v * w)";
by (simp_tac (simpset() addsimps [complex_Re_Im_cancel_iff,
    real_mult_assoc,real_diff_mult_distrib2,
    real_add_mult_distrib2,real_diff_mult_distrib,
    real_add_mult_distrib,real_mult_left_commute]) 1);
qed "complex_mult_assoc";

Goalw [complex_mult_def] "(x::complex) * (y * z) = y * (x * z)";
by (simp_tac (simpset() addsimps [complex_Re_Im_cancel_iff,
    real_mult_left_commute,real_diff_mult_distrib2,
    real_add_mult_distrib2]) 1);
qed "complex_mult_left_commute";

val complex_mult_ac = [complex_mult_assoc,complex_mult_commute,
                      complex_mult_left_commute];

Goalw [complex_one_def] "(1::complex) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_mult]) 1);
qed "complex_mult_one_left";
Addsimps [complex_mult_one_left];

Goal "z * (1::complex) = z";
by (simp_tac (simpset() addsimps [complex_mult_commute]) 1);
qed "complex_mult_one_right";
Addsimps [complex_mult_one_right];

Goalw [complex_zero_def] "(0::complex) * z = 0";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_mult]) 1);
qed "complex_mult_zero_left";
Addsimps [complex_mult_zero_left];

Goal "z * 0 = (0::complex)";
by (simp_tac (simpset() addsimps [complex_mult_commute]) 1);
qed "complex_mult_zero_right";
Addsimps [complex_mult_zero_right];

Goalw [complex_divide_def] "0 / z = (0::complex)";
by Auto_tac;
qed "complex_divide_zero";
Addsimps [complex_divide_zero];

Goal "-(x * y) = -x * (y::complex)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_minus,
    real_diff_def]));
qed "complex_minus_mult_eq1";

Goal "-(x * y) = x * -(y::complex)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_minus,
    real_diff_def]));
qed "complex_minus_mult_eq2";

Addsimps [ complex_minus_mult_eq1 RS sym, complex_minus_mult_eq2 RS sym];

Goal "-(1::complex) * z = -z";
by (Simp_tac 1);
qed "complex_mult_minus_one";
Addsimps [complex_mult_minus_one];

Goal "z * -(1::complex) = -z";
by (stac complex_mult_commute 1);
by (Simp_tac 1);
qed "complex_mult_minus_one_right";
Addsimps [complex_mult_minus_one_right];

Goal "-x * -y = x * (y::complex)";
by (Simp_tac 1);
qed "complex_minus_mult_cancel";
Addsimps [complex_minus_mult_cancel];

Goal "-x * y = x * -(y::complex)";
by (Simp_tac 1);
qed "complex_minus_mult_commute";

qed_goal "complex_add_assoc_cong" thy
    "!!z. (z::complex) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
 (fn _ => [(asm_simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1)]);

qed_goal "complex_add_assoc_swap" thy "(z::complex) + (v + w) = v + (z + w)"
 (fn _ => [(REPEAT (ares_tac [complex_add_commute RS complex_add_assoc_cong] 1))]);

Goal "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)";
by (res_inst_tac [("z","z1")] eq_Abs_complex 1);
by (res_inst_tac [("z","z2")] eq_Abs_complex 1);
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add,
    real_add_mult_distrib,real_diff_def] @ real_add_ac));
qed "complex_add_mult_distrib";

Goal "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)";
by (res_inst_tac [("z1","z1 + z2")] (complex_mult_commute RS ssubst) 1);
by (simp_tac (simpset() addsimps [complex_add_mult_distrib]) 1);
by (simp_tac (simpset() addsimps [complex_mult_commute]) 1);
qed "complex_add_mult_distrib2";

Goalw [complex_zero_def,complex_one_def] "(0::complex) ~= 1";
by (simp_tac (simpset() addsimps [complex_Re_Im_cancel_iff]) 1);
qed "complex_zero_not_eq_one";
Addsimps [complex_zero_not_eq_one];
Addsimps [complex_zero_not_eq_one RS not_sym];

(*** inverse ***)
Goalw [complex_inverse_def] "inverse (Abs_complex(x,y)) = \
\    Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))";
by (Simp_tac 1);
qed "complex_inverse";

Goalw [complex_inverse_def,complex_zero_def] "inverse 0 = (0::complex)";
by Auto_tac;
qed "COMPLEX_INVERSE_ZERO";

Goal "a / (0::complex) = 0";
by (simp_tac (simpset() addsimps [complex_divide_def, COMPLEX_INVERSE_ZERO]) 1);
qed "COMPLEX_DIVISION_BY_ZERO";  (*NOT for adding to default simpset*)

fun complex_div_undefined_case_tac s i =
  case_tac s i THEN 
  asm_simp_tac (simpset() addsimps [COMPLEX_DIVISION_BY_ZERO, COMPLEX_INVERSE_ZERO]) i;

(*REMOVE?:
lemmas:replace previous versions to accommodate new behaviour of simplification
Goal "x ^ 2 + y ^ 2 = 0 ==> x = (0::real)";
by (auto_tac (claset() addIs [real_sum_squares_cancel],
    simpset() addsimps [CLAIM "2 = Suc(Suc 0)"]));
qed "real_sum_squares_cancel";

Goal "x ^ 2 + y ^ 2 = 0 ==> y = (0::real)";
by (auto_tac (claset() addIs [real_sum_squares_cancel2],
    simpset() addsimps [CLAIM "2 = Suc(Suc 0)"]));
qed "real_sum_squares_cancel2";
*)

Goal "z ~= (0::complex) ==> inverse(z) * z = 1";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_inverse,
    complex_one_def,complex_zero_def,real_add_divide_distrib RS sym,
    realpow_two_eq_mult] @ real_mult_ac));
by (dres_inst_tac [("y","y")] real_sum_squares_not_zero 1);
by (dres_inst_tac [("x","x")] real_sum_squares_not_zero2 2);
by Auto_tac;
qed "complex_mult_inv_left";
Addsimps [complex_mult_inv_left];

Goal "z ~= (0::complex) ==> z * inverse(z) = 1";
by (auto_tac (claset() addIs [complex_mult_commute RS subst],simpset()));
qed "complex_mult_inv_right";
Addsimps [complex_mult_inv_right];

Goal "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)";
by Auto_tac;
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps complex_mult_ac)  1);
qed "complex_mult_left_cancel";
    
Goal "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)";
by (Step_tac 1);
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps complex_mult_ac)  1);
qed "complex_mult_right_cancel";

Goal "z ~= 0 ==> inverse(z::complex) ~= 0";
by (Step_tac 1);
by (ftac (complex_mult_right_cancel RS iffD2) 1);
by (thin_tac "inverse z = 0" 2);
by (assume_tac 1 THEN Auto_tac);
qed "complex_inverse_not_zero";
Addsimps [complex_inverse_not_zero];

Goal "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0";
by (Step_tac 1);
by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [complex_mult_assoc RS sym]) 1);
qed "complex_mult_not_zero";

bind_thm ("complex_mult_not_zeroE",complex_mult_not_zero RS notE);

Goal "inverse(inverse (x::complex)) = x";
by (complex_div_undefined_case_tac "x = 0" 1);
by (res_inst_tac [("c1","inverse x")] (complex_mult_right_cancel RS iffD1) 1);
by (etac complex_inverse_not_zero 1);
by (auto_tac (claset() addDs [complex_inverse_not_zero],simpset()));
qed "complex_inverse_inverse";
Addsimps [complex_inverse_inverse];

Goalw [complex_one_def] "inverse(1::complex) = 1";
by (simp_tac (simpset() addsimps [complex_inverse,realpow_num_two]) 1);
qed "complex_inverse_one";
Addsimps [complex_inverse_one];

Goal "inverse(-x) = -inverse(x::complex)";
by (complex_div_undefined_case_tac "x = 0" 1);
by (res_inst_tac [("c1","-x")] (complex_mult_right_cancel RS iffD1) 1);
by (stac complex_mult_inv_left 2);
by Auto_tac;
qed "complex_minus_inverse";

Goal "inverse(x*y) = inverse x * inverse (y::complex)";
by (complex_div_undefined_case_tac "x = 0" 1);
by (complex_div_undefined_case_tac "y = 0" 1);
by (res_inst_tac [("c1","x*y")] (complex_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult_not_zero]
    @ complex_mult_ac));
by (auto_tac (claset(),simpset() addsimps [complex_mult_not_zero,
    complex_mult_assoc RS sym]));
qed "complex_inverse_distrib";


(*** division ***)

(*adding some of these theorems to simpset as for reals: 
  not 100% convinced for some*)

Goal "(x::complex) * (y/z) = (x*y)/z";
by (simp_tac (simpset() addsimps [complex_divide_def, complex_mult_assoc]) 1); 
qed "complex_times_divide1_eq";

Goal "(y/z) * (x::complex) = (y*x)/z";
by (simp_tac (simpset() addsimps [complex_divide_def]@complex_mult_ac) 1); 
qed "complex_times_divide2_eq";

Addsimps [complex_times_divide1_eq, complex_times_divide2_eq];

Goal "(x::complex) / (y/z) = (x*z)/y";
by (simp_tac (simpset() addsimps [complex_divide_def, complex_inverse_distrib]@
                                  complex_mult_ac) 1); 
qed "complex_divide_divide1_eq";

Goal "((x::complex) / y) / z = x/(y*z)";
by (simp_tac (simpset() addsimps [complex_divide_def, complex_inverse_distrib, 
                                  complex_mult_assoc]) 1); 
qed "complex_divide_divide2_eq";

Addsimps [complex_divide_divide1_eq, complex_divide_divide2_eq];

(** As with multiplication, pull minus signs OUT of the / operator **)

Goal "(-x) / (y::complex) = - (x/y)";
by (simp_tac (simpset() addsimps [complex_divide_def]) 1); 
qed "complex_minus_divide_eq";
Addsimps [complex_minus_divide_eq];

Goal "(x / -(y::complex)) = - (x/y)";
by (simp_tac (simpset() addsimps [complex_divide_def, complex_minus_inverse]) 1); 
qed "complex_divide_minus_eq";
Addsimps [complex_divide_minus_eq];

Goal "(x+y)/(z::complex) = x/z + y/z";
by (simp_tac (simpset() addsimps [complex_divide_def, complex_add_mult_distrib]) 1); 
qed "complex_add_divide_distrib";

(*---------------------------------------------------------------------------*)
(*          Embedding properties for complex_of_real map                     *)
(*---------------------------------------------------------------------------*)

Goal "inj complex_of_real";
by (rtac injI 1);
by (auto_tac (claset() addDs [inj_Abs_complex RS injD],
    simpset() addsimps [complex_of_real_def]));
qed "inj_complex_of_real";

Goalw [complex_one_def,complex_of_real_def]
      "complex_of_real 1 = 1";
by (rtac refl 1);
qed "complex_of_real_one";
Addsimps [complex_of_real_one];

Goalw [complex_zero_def,complex_of_real_def]
      "complex_of_real 0 = 0";
by (rtac refl 1);
qed "complex_of_real_zero";
Addsimps [complex_of_real_zero];

Goal "(complex_of_real x = complex_of_real y) = (x = y)";
by (auto_tac (claset() addDs [inj_complex_of_real RS injD],simpset()));
qed "complex_of_real_eq_iff";
AddIffs [complex_of_real_eq_iff];

Goal "complex_of_real(-x) = - complex_of_real x";
by (simp_tac (simpset() addsimps [complex_of_real_def,complex_minus]) 1);
qed "complex_of_real_minus";

Goal "complex_of_real(inverse x) = inverse(complex_of_real x)";
by (real_div_undefined_case_tac "x=0" 1);
by (simp_tac (simpset() addsimps [DIVISION_BY_ZERO,COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [complex_inverse,
    complex_of_real_def,realpow_num_two,real_divide_def,
    real_inverse_distrib]));
qed "complex_of_real_inverse";

Goal "complex_of_real x + complex_of_real y = complex_of_real (x + y)";
by (simp_tac (simpset() addsimps [complex_add,complex_of_real_def]) 1);
qed "complex_of_real_add";

Goal "complex_of_real x - complex_of_real y = complex_of_real (x - y)";
by (simp_tac (simpset() addsimps [complex_of_real_minus RS sym,
    complex_diff_def,complex_of_real_add]) 1);
qed "complex_of_real_diff";

Goal "complex_of_real x * complex_of_real y = complex_of_real (x * y)";
by (simp_tac (simpset() addsimps [complex_mult,complex_of_real_def]) 1);
qed "complex_of_real_mult";

Goalw [complex_divide_def] 
      "complex_of_real x / complex_of_real y = complex_of_real(x/y)";
by (real_div_undefined_case_tac "y=0" 1);
by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
    COMPLEX_INVERSE_ZERO]) 1);
by (asm_simp_tac (simpset() addsimps [complex_of_real_mult RS sym,
    complex_of_real_inverse,real_divide_def]) 1);
qed "complex_of_real_divide";

Goal "complex_of_real (x ^ n) = (complex_of_real x) ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [complex_of_real_mult RS sym]));
qed "complex_of_real_pow";

Goalw [cmod_def] "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)";
by (Simp_tac 1);
qed "complex_mod";

Goalw [cmod_def] "cmod(0) = 0";
by (Simp_tac 1);
qed "complex_mod_zero";
Addsimps [complex_mod_zero];

Goalw [cmod_def] "cmod(1) = 1";
by (simp_tac (simpset() addsimps [realpow_num_two]) 1);
qed "complex_mod_one";
Addsimps [complex_mod_one];

Goalw [complex_of_real_def] "cmod(complex_of_real x) = abs x";
by (simp_tac (simpset() addsimps [complex_mod,realpow_num_two]) 1);
qed "complex_mod_complex_of_real";
Addsimps [complex_mod_complex_of_real];

Goal "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))";
by (Simp_tac 1);
qed "complex_of_real_abs";

(*---------------------------------------------------------------------------*)
(*                   conjugation is an automorphism                          *)
(*---------------------------------------------------------------------------*)

Goalw [cnj_def] "cnj (Abs_complex(x,y)) = Abs_complex(x,-y)";
by (Simp_tac 1);
qed "complex_cnj";

Goal "inj cnj";
by (rtac injI 1);
by (auto_tac (claset(),simpset() addsimps [cnj_def,
    Abs_complex_cancel_iff,complex_Re_Im_cancel_iff]));
qed "inj_cnj";

Goal "(cnj x = cnj y) = (x = y)";
by (auto_tac (claset() addDs [inj_cnj RS injD],simpset()));
qed "complex_cnj_cancel_iff";
Addsimps [complex_cnj_cancel_iff];

Goalw [cnj_def] "cnj (cnj z) = z";
by (Simp_tac 1);
qed "complex_cnj_cnj";
Addsimps [complex_cnj_cnj];

Goalw [complex_of_real_def] "cnj (complex_of_real x) = complex_of_real x";
by (simp_tac (simpset() addsimps [complex_cnj]) 1);
qed "complex_cnj_complex_of_real";
Addsimps [complex_cnj_complex_of_real];

Goal "cmod (cnj z) = cmod z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_cnj,complex_mod,realpow_num_two]) 1);
qed "complex_mod_cnj";
Addsimps [complex_mod_cnj];

Goalw [cnj_def] "cnj (-z) = - cnj z";
by (simp_tac (simpset() addsimps [complex_minus,
    complex_Re_minus,complex_Im_minus]) 1);
qed "complex_cnj_minus";

Goal "cnj(inverse z) = inverse(cnj z)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_cnj,complex_inverse,
    realpow_num_two]) 1);
qed "complex_cnj_inverse";

Goal "cnj(w + z) = cnj(w) + cnj(z)";
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_cnj,complex_add]) 1);
qed "complex_cnj_add";

Goalw [complex_diff_def] "cnj(w - z) = cnj(w) - cnj(z)";
by (simp_tac (simpset() addsimps [complex_cnj_add,complex_cnj_minus]) 1);
qed "complex_cnj_diff";

Goal "cnj(w * z) = cnj(w) * cnj(z)";
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_cnj,complex_mult]) 1);
qed "complex_cnj_mult";

Goalw [complex_divide_def] "cnj(w / z) = (cnj w)/(cnj z)";
by (simp_tac (simpset() addsimps [complex_cnj_mult,complex_cnj_inverse]) 1);
qed "complex_cnj_divide";

Goalw [cnj_def,complex_one_def] "cnj 1 = 1";
by (Simp_tac 1);
qed "complex_cnj_one";
Addsimps [complex_cnj_one];

Goal "cnj(z ^ n) = cnj(z) ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [complex_cnj_mult]));
qed "complex_cnj_pow";

Goal "z + cnj z = complex_of_real (2 * Re(z))";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_add,complex_cnj,
    complex_of_real_def]) 1);
qed "complex_add_cnj";

Goal "z - cnj z = complex_of_real (2 * Im(z)) * ii";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_add,complex_cnj,
    complex_of_real_def,complex_diff_def,complex_minus,
    i_def,complex_mult]) 1);
qed "complex_diff_cnj";

goalw Complex.thy  [cnj_def,complex_zero_def] 
      "cnj 0 = 0";
by Auto_tac;
qed "complex_cnj_zero";
Addsimps [complex_cnj_zero];

goal Complex.thy "(cnj z = 0) = (z = 0)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_zero_def,
    complex_cnj]));
qed "complex_cnj_zero_iff";
AddIffs [complex_cnj_zero_iff];

Goal "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_cnj,complex_mult,
    complex_of_real_def,realpow_num_two]));
qed "complex_mult_cnj";

(*---------------------------------------------------------------------------*)
(*                              algebra                                      *)
(*---------------------------------------------------------------------------*)

Goal "(x*y = (0::complex)) = (x = 0 | y = 0)";
by Auto_tac;
by (auto_tac (claset() addIs [ccontr] addDs 
    [complex_mult_not_zero],simpset()));
qed "complex_mult_zero_iff";
AddIffs [complex_mult_zero_iff];

Goalw [complex_zero_def] "(x + y = x) = (y = (0::complex))";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_add]));
qed "complex_add_left_cancel_zero";
Addsimps [complex_add_left_cancel_zero];

Goalw [complex_diff_def] 
      "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)";
by (simp_tac (simpset() addsimps [complex_add_mult_distrib]) 1);
qed "complex_diff_mult_distrib";

Goalw [complex_diff_def]
      "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)";
by (simp_tac (simpset() addsimps [complex_add_mult_distrib2]) 1);
qed "complex_diff_mult_distrib2";

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

(*
Goal "[| sqrt(x) = 0; 0 <= x |] ==> x = 0";
by (auto_tac (claset() addIs [real_sqrt_eq_zero_cancel],
    simpset()));
qed "real_sqrt_eq_zero_cancel2";
*)

Goal "(cmod x = 0) = (x = 0)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (auto_tac (claset() addIs
    [real_sum_squares_cancel,real_sum_squares_cancel2],
    simpset() addsimps [complex_mod,complex_zero_def,
    realpow_num_two]));
qed "complex_mod_eq_zero_cancel";
Addsimps [complex_mod_eq_zero_cancel];

Goal "cmod (complex_of_real(real (n::nat))) = real n";
by (Simp_tac 1);
qed "complex_mod_complex_of_real_of_nat";
Addsimps [complex_mod_complex_of_real_of_nat];

Goal "cmod (-x) = cmod(x)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_mod,complex_minus,
    realpow_num_two]) 1);
qed "complex_mod_minus";
Addsimps [complex_mod_minus];

Goal "cmod(z * cnj(z)) = cmod(z) ^ 2";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_mod,complex_cnj,
    complex_mult, CLAIM "0 ^ 2 = (0::real)"]) 1);
by (simp_tac (simpset() addsimps [realpow_two_eq_mult]) 1);
qed "complex_mod_mult_cnj";

Goalw [cmod_def] "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2";
by Auto_tac;
qed "complex_mod_squared";

Goalw [cmod_def]  "0 <= cmod x";
by (auto_tac (claset() addIs [real_sqrt_ge_zero],simpset()));
qed "complex_mod_ge_zero";
Addsimps [complex_mod_ge_zero];

Goal "abs(cmod x) = cmod x";
by (auto_tac (claset() addIs [abs_eqI1],simpset()));
qed "abs_cmod_cancel";
Addsimps [abs_cmod_cancel];

Goal "cmod(x*y) = cmod(x) * cmod(y)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult,
    complex_mod,real_sqrt_mult_distrib2 RS sym] delsimps [realpow_Suc]));
by (res_inst_tac [("n","1")] realpow_Suc_cancel_eq 1);
by (auto_tac (claset(),simpset() addsimps [realpow_num_two RS sym] 
    delsimps [realpow_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_diff_def,realpow_num_two,
    real_add_mult_distrib2,real_add_mult_distrib] @ real_add_ac @ 
    real_mult_ac));
qed "complex_mod_mult";

Goal "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_add,
    complex_mod_squared,complex_mult,complex_cnj,real_diff_def] 
    delsimps [realpow_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2,
    real_add_mult_distrib,realpow_num_two] @ real_mult_ac @ real_add_ac));
qed "complex_mod_add_squared_eq";

Goal "Re(x * cnj y) <= cmod(x * cnj y)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mod,
    complex_mult,complex_cnj,real_diff_def] delsimps [realpow_Suc]));
qed "complex_Re_mult_cnj_le_cmod";
Addsimps [complex_Re_mult_cnj_le_cmod];

Goal "Re(x * cnj y) <= cmod(x * y)";
by (cut_inst_tac [("x","x"),("y","y")] complex_Re_mult_cnj_le_cmod 1);
by (asm_full_simp_tac (simpset() addsimps [complex_mod_mult]) 1);
qed "complex_Re_mult_cnj_le_cmod2";
Addsimps [complex_Re_mult_cnj_le_cmod2];

Goal "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y";
by (simp_tac (simpset() addsimps [real_add_mult_distrib,
    real_add_mult_distrib2,realpow_num_two]) 1);
qed "real_sum_squared_expand";

Goal "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2";
by (simp_tac (simpset() addsimps [real_sum_squared_expand,
    complex_mod_add_squared_eq,real_mult_assoc,complex_mod_mult RS sym]) 1);
qed "complex_mod_triangle_squared";
Addsimps [complex_mod_triangle_squared];

Goal "- cmod x <= cmod x";
by (rtac (complex_mod_ge_zero RSN (2,real_le_trans)) 1);
by (Simp_tac 1);
qed "complex_mod_minus_le_complex_mod";
Addsimps [complex_mod_minus_le_complex_mod];

Goal "cmod (x + y) <= cmod(x) + cmod(y)";
by (res_inst_tac [("n","1")] realpow_increasing 1);
by (auto_tac (claset() addIs [(complex_mod_ge_zero RSN (2,real_le_trans))],
    simpset() addsimps [realpow_num_two RS sym]));
qed "complex_mod_triangle_ineq";
Addsimps [complex_mod_triangle_ineq];

Goal "cmod(b + a) - cmod b <= cmod a";
by (cut_inst_tac [("x1","b"),("y1","a"),("z","-cmod b")]
   (complex_mod_triangle_ineq RS real_add_le_mono1) 1);
by (Simp_tac 1);
qed "complex_mod_triangle_ineq2";
Addsimps [complex_mod_triangle_ineq2];

Goal "cmod (x - y) = cmod (y - x)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (res_inst_tac [("z","y")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_diff,
    complex_mod,real_diff_mult_distrib2,realpow_num_two,
    real_diff_mult_distrib] @ real_add_ac @ real_mult_ac));
qed "complex_mod_diff_commute";

Goal "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s";
by (auto_tac (claset() addIs [order_le_less_trans,
    complex_mod_triangle_ineq],simpset()));
qed "complex_mod_add_less";

Goal "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s";
by (auto_tac (claset() addIs [real_mult_less_mono'],simpset()     
    addsimps [complex_mod_mult]));
qed "complex_mod_mult_less";

goal Complex.thy "cmod(a) - cmod(b) <= cmod(a + b)";
by (res_inst_tac [("R1.0","cmod(a)"),("R2.0","cmod(b)")]
    real_linear_less2 1);
by Auto_tac;
by (dtac (ARITH_PROVE "a < b ==> a - (b::real) < 0") 1);
by (rtac real_le_trans 1 THEN rtac order_less_imp_le 1);
by Auto_tac;
by (dtac (ARITH_PROVE "a < b ==> 0 < (b::real) - a") 1);
by (rtac (ARITH_PROVE "a  <= b + c ==> a - c <= (b::real)") 1);
by (rtac (complex_mod_minus RS subst) 1);
by (rtac real_le_trans 1);
by (rtac complex_mod_triangle_ineq 2);
by (auto_tac (claset(),simpset() addsimps complex_add_ac));
qed "complex_mod_diff_ineq";
Addsimps [complex_mod_diff_ineq];

Goal "Re z <= cmod z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mod]
    delsimps [realpow_Suc]));
qed "complex_Re_le_cmod";
Addsimps [complex_Re_le_cmod];

Goal "z ~= 0 ==> 0 < cmod z";
by (cut_inst_tac [("x","z")] complex_mod_ge_zero 1);
by (dtac order_le_imp_less_or_eq 1);
by Auto_tac;
qed "complex_mod_gt_zero";


(*---------------------------------------------------------------------------*)
(*                       a few more theorems                                 *)
(*---------------------------------------------------------------------------*)

Goal "cmod(x ^ n) = cmod(x) ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [complex_mod_mult]));
qed "complex_mod_complexpow";

Goal "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))";
by (induct_tac "n" 1);
by Auto_tac;
qed "complexpow_minus";

Goal "inverse (-x) = - inverse (x::complex)";
by (res_inst_tac [("z","x")] eq_Abs_complex 1);
by (asm_simp_tac (simpset() addsimps [complex_inverse,complex_minus,
    realpow_num_two]) 1);
qed "complex_inverse_minus";

Goalw [complex_divide_def] "x / (1::complex) = x";
by (Simp_tac 1);
qed "complex_divide_one";
Addsimps [complex_divide_one];

Goal "cmod(inverse x) = inverse(cmod x)";
by (complex_div_undefined_case_tac "x=0" 1);
by (res_inst_tac [("c1","cmod x")] (real_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [complex_mod_mult RS sym]));
qed "complex_mod_inverse";

Goalw [complex_divide_def,real_divide_def]
      "cmod(x/y) = cmod(x)/(cmod y)";
by (auto_tac (claset(),simpset() addsimps [complex_mod_mult,
    complex_mod_inverse]));
qed "complex_mod_divide";

Goalw [complex_divide_def]  
      "inverse(x/y) = y/(x::complex)";
by (auto_tac (claset(),simpset() addsimps [complex_inverse_distrib,
    complex_mult_commute]));
qed "complex_inverse_divide";
Addsimps [complex_inverse_divide];

Goal "((r::complex) * s) ^ n = (r ^ n) * (s ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps complex_mult_ac));
qed "complexpow_mult";

(*---------------------------------------------------------------------------*)
(*                       More exponentiation                                 *)
(*---------------------------------------------------------------------------*)

Goal "(0::complex) ^ (Suc n) = 0";
by (Auto_tac);
qed "complexpow_zero";
Addsimps [complexpow_zero];

Goal "r ~= (0::complex) --> r ^ n ~= 0";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult_not_zero]));
qed_spec_mp "complexpow_not_zero";
Addsimps [complexpow_not_zero];
AddIs [complexpow_not_zero];

Goal "r ^ n = (0::complex) ==> r = 0";
by (blast_tac (claset() addIs [ccontr] 
    addDs [complexpow_not_zero]) 1);
qed "complexpow_zero_zero";

Goalw [i_def] "ii ^ 2 = -(1::complex)";
by (auto_tac (claset(),simpset() addsimps 
    [complex_mult,complex_one_def,complex_minus,realpow_num_two]));
qed "complexpow_i_squared";
Addsimps [complexpow_i_squared];

Goalw [i_def,complex_zero_def] "ii ~= 0";
by Auto_tac;
qed "complex_i_not_zero";
Addsimps [complex_i_not_zero];

Goal "x * y ~= (0::complex) ==> x ~= 0";
by Auto_tac;
qed "complex_mult_eq_zero_cancel1";

Goal "x * y ~= 0 ==> y ~= (0::complex)";
by Auto_tac;
qed "complex_mult_eq_zero_cancel2";

Goal "(x * y ~= 0) = (x ~= 0 & y ~= (0::complex))";
by Auto_tac;
qed "complex_mult_not_eq_zero_iff";
AddIffs [complex_mult_not_eq_zero_iff];

Goal "inverse ((r::complex) ^ n) = (inverse r) ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [complex_inverse_distrib]));
qed "complexpow_inverse";

(*---------------------------------------------------------------------------*)
(* sgn                                                                       *)
(*---------------------------------------------------------------------------*)

Goalw [sgn_def] "sgn 0 = 0";
by (Simp_tac 1);
qed "sgn_zero";
Addsimps[sgn_zero];

Goalw [sgn_def] "sgn 1 = 1";
by (Simp_tac 1);
qed "sgn_one";
Addsimps [sgn_one];

Goalw [sgn_def] "sgn (-z) = - sgn(z)";
by Auto_tac;
qed "sgn_minus";

Goalw [sgn_def] 
    "sgn z = z / complex_of_real (cmod z)";
by (Simp_tac 1);
qed "sgn_eq";

Goal "EX x y. z = complex_of_real(x) + ii * complex_of_real(y)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,
    i_def,complex_mult,complex_add]));
qed "complex_split";

Goal "Re(complex_of_real(x) + ii * complex_of_real(y)) = x";
by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,
    i_def,complex_mult,complex_add]));
qed "Re_complex_i";
Addsimps [Re_complex_i];

Goal "Im(complex_of_real(x) + ii * complex_of_real(y)) = y";
by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,
    i_def,complex_mult,complex_add]));
qed "Im_complex_i";
Addsimps [Im_complex_i];

Goalw [i_def,complex_of_real_def] "ii * ii = complex_of_real (-1)";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add]));
qed "i_mult_eq";

Goalw [i_def,complex_one_def] "ii * ii = -(1::complex)";
by (simp_tac (simpset() addsimps [complex_mult,complex_minus]) 1);
qed "i_mult_eq2";
Addsimps [i_mult_eq2];

Goal "cmod (complex_of_real(x) + ii * complex_of_real(y)) = \
\     sqrt (x ^ 2 + y ^ 2)";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add,
    i_def,complex_of_real_def,cmod_def]));
qed "cmod_i";

Goalw [complex_of_real_def,i_def] 
     "complex_of_real xa + ii * complex_of_real ya = \
\     complex_of_real xb + ii * complex_of_real yb \
\      ==> xa = xb";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add]));
qed "complex_eq_Re_eq";

Goalw [complex_of_real_def,i_def] 
     "complex_of_real xa + ii * complex_of_real ya = \
\     complex_of_real xb + ii * complex_of_real yb \
\      ==> ya = yb";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add]));
qed "complex_eq_Im_eq";

Goal "(complex_of_real xa + ii * complex_of_real ya = \
\      complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))";
by (auto_tac (claset() addIs [complex_eq_Im_eq,complex_eq_Re_eq],simpset()));
qed "complex_eq_cancel_iff";
AddIffs [complex_eq_cancel_iff];

Goal "(complex_of_real xa + complex_of_real ya * ii = \
\      complex_of_real xb + complex_of_real yb * ii ) = ((xa = xb) & (ya = yb))";
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
qed "complex_eq_cancel_iffA";
AddIffs [complex_eq_cancel_iffA];

Goal "(complex_of_real xa + complex_of_real ya * ii = \
\      complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))";
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
qed "complex_eq_cancel_iffB";
AddIffs [complex_eq_cancel_iffB];

Goal "(complex_of_real xa + ii * complex_of_real ya  = \
\      complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))";
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
qed "complex_eq_cancel_iffC";
AddIffs [complex_eq_cancel_iffC];

Goal"(complex_of_real x + ii * complex_of_real y = \
\     complex_of_real xa) = (x = xa & y = 0)";
by (cut_inst_tac [("xa","x"),("ya","y"),("xb","xa"),("yb","0")]  
    complex_eq_cancel_iff 1);
by (asm_full_simp_tac (simpset() delsimps [complex_eq_cancel_iff]) 1);
qed "complex_eq_cancel_iff2";
Addsimps [complex_eq_cancel_iff2];

Goal"(complex_of_real x + complex_of_real y * ii = \
\     complex_of_real xa) = (x = xa & y = 0)";
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
qed "complex_eq_cancel_iff2a";
Addsimps [complex_eq_cancel_iff2a];

Goal "(complex_of_real x + ii * complex_of_real y = \
\     ii * complex_of_real ya) = (x = 0 & y = ya)";
by (cut_inst_tac [("xa","x"),("ya","y"),("xb","0"),("yb","ya")]  
    complex_eq_cancel_iff 1);
by (asm_full_simp_tac (simpset() delsimps [complex_eq_cancel_iff]) 1);
qed "complex_eq_cancel_iff3";
Addsimps [complex_eq_cancel_iff3];

Goal "(complex_of_real x + complex_of_real y * ii = \
\     ii * complex_of_real ya) = (x = 0 & y = ya)";
by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
qed "complex_eq_cancel_iff3a";
Addsimps [complex_eq_cancel_iff3a];

Goalw [complex_of_real_def,i_def,complex_zero_def] 
     "complex_of_real x + ii * complex_of_real y = 0 \
\     ==> x = 0";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add]));
qed "complex_split_Re_zero";

Goalw [complex_of_real_def,i_def,complex_zero_def] 
     "complex_of_real x + ii * complex_of_real y = 0 \
\     ==> y = 0";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add]));
qed "complex_split_Im_zero";

Goalw [sgn_def,complex_divide_def] 
      "Re(sgn z) = Re(z)/cmod z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_of_real_inverse RS sym]));
by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,
    complex_mult,real_divide_def]));
qed "Re_sgn";
Addsimps [Re_sgn];

Goalw [sgn_def,complex_divide_def] 
      "Im(sgn z) = Im(z)/cmod z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_of_real_inverse RS sym]));
by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,
    complex_mult,real_divide_def]));
qed "Im_sgn";
Addsimps [Im_sgn];

Goalw [complex_of_real_def,i_def] 
     "inverse(complex_of_real x + ii * complex_of_real y) = \
\     complex_of_real(x/(x ^ 2 + y ^ 2)) - \
\     ii * complex_of_real(y/(x ^ 2 + y ^ 2))";
by (auto_tac (claset(),simpset() addsimps [complex_mult,complex_add,
    complex_diff_def,complex_minus,complex_inverse,real_divide_def]));
qed "complex_inverse_complex_split";

(*----------------------------------------------------------------------------*)
(* Many of the theorems below need to be moved elsewhere e.g. Transc.ML. Also *)
(* many of the theorems are not used - so should they be kept?                *)
(*----------------------------------------------------------------------------*)

Goalw [i_def,complex_of_real_def]
    "Re (ii * complex_of_real y) = 0";
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "Re_mult_i_eq";
Addsimps [Re_mult_i_eq];

Goalw [i_def,complex_of_real_def]
    "Im (ii * complex_of_real y) = y";
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "Im_mult_i_eq";
Addsimps [Im_mult_i_eq];

Goalw [i_def,complex_of_real_def]
    "cmod (ii * complex_of_real y) = abs y";
by (auto_tac (claset(),simpset() addsimps [complex_mult,
    complex_mod,realpow_num_two]));
qed "complex_mod_mult_i";
Addsimps [complex_mod_mult_i];

Goalw [arg_def] 
   "0 < y ==> cos (arg(ii * complex_of_real y)) = 0";
by (auto_tac (claset(),simpset() addsimps [abs_eqI2]));
by (res_inst_tac [("a","pi/2")] someI2 1);
by Auto_tac;
by (res_inst_tac [("R2.0","0")] real_less_trans 1);
by Auto_tac;
qed "cos_arg_i_mult_zero";
Addsimps [cos_arg_i_mult_zero];

Goalw [arg_def] 
   "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0";
by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2]));
by (res_inst_tac [("a","- pi/2")] someI2 1);
by Auto_tac;
by (res_inst_tac [("j","0")] real_le_trans 1);
by Auto_tac;
qed "cos_arg_i_mult_zero2";
Addsimps [cos_arg_i_mult_zero2];

Goalw [complex_zero_def,complex_of_real_def] 
      "(complex_of_real y ~= 0) = (y ~= 0)";
by Auto_tac;
qed "complex_of_real_not_zero_iff";
Addsimps [complex_of_real_not_zero_iff];

Goal "(complex_of_real y = 0) = (y = 0)";
by Auto_tac;
by (rtac ccontr 1 THEN dtac (complex_of_real_not_zero_iff RS iffD2) 1);
by (Asm_full_simp_tac 1);
qed "complex_of_real_zero_iff";
Addsimps [complex_of_real_zero_iff];

Goal "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0";
by (cut_inst_tac [("R1.0","y"),("R2.0","0")] real_linear 1);
by Auto_tac;
qed "cos_arg_i_mult_zero3";
Addsimps [cos_arg_i_mult_zero3];

(*---------------------------------------------------------------------------*)
(* Finally! Polar form for complex numbers                                   *) 
(*---------------------------------------------------------------------------*)

Goal "EX r a. z = complex_of_real r * \
\     (complex_of_real(cos a) + ii * complex_of_real(sin a))";
by (cut_inst_tac [("z","z")] complex_split 1);
by (auto_tac (claset(),simpset() addsimps [polar_Ex,
    complex_add_mult_distrib2,complex_of_real_mult] @ complex_mult_ac));
qed "complex_split_polar";

Goalw [rcis_def,cis_def] "EX r a. z = rcis r a";
by (rtac complex_split_polar 1);
qed "rcis_Ex";

Goal "Re(complex_of_real r * \
\     (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a";
by (auto_tac (claset(),simpset() addsimps [complex_add_mult_distrib2,
    complex_of_real_mult] @ complex_mult_ac));
qed "Re_complex_polar";
Addsimps [Re_complex_polar];

Goalw [rcis_def,cis_def] "Re(rcis r a) = r * cos a";
by Auto_tac;
qed "Re_rcis";
Addsimps [Re_rcis];

Goal "Im(complex_of_real r * \
\     (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a";
by (auto_tac (claset(),simpset() addsimps [complex_add_mult_distrib2,
    complex_of_real_mult] @ complex_mult_ac));
qed "Im_complex_polar";
Addsimps [Im_complex_polar];

Goalw [rcis_def,cis_def] "Im(rcis r a) = r * sin a";
by Auto_tac;
qed "Im_rcis";
Addsimps [Im_rcis];

Goal "cmod (complex_of_real r * \
\     (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r";
by (auto_tac (claset(),simpset() addsimps [complex_add_mult_distrib2,
    cmod_i,complex_of_real_mult,real_add_mult_distrib2
    RS sym,realpow_mult]  @ complex_mult_ac@ real_mult_ac 
    delsimps [realpow_Suc]));
qed "complex_mod_complex_polar";
Addsimps [complex_mod_complex_polar];

Goalw [rcis_def,cis_def] "cmod(rcis r a) = abs r";
by Auto_tac;
qed "complex_mod_rcis";
Addsimps [complex_mod_rcis];

Goalw [cmod_def] "cmod z = sqrt (Re (z * cnj z))";
by (rtac (real_sqrt_eq_iff RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult_cnj]));
qed "complex_mod_sqrt_Re_mult_cnj";

Goal "Re(cnj z) = Re z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_cnj]));
qed "complex_Re_cnj";
Addsimps [complex_Re_cnj];

Goal "Im(cnj z) = - Im z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_cnj]));
qed "complex_Im_cnj";
Addsimps [complex_Im_cnj];

Goal "Im (z * cnj z) = 0";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_cnj,complex_mult]));
qed "complex_In_mult_cnj_zero";
Addsimps [complex_In_mult_cnj_zero];

Goal "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Re_mult";

Goalw [complex_of_real_def] "Re (z * complex_of_real c) = Re(z) * c";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Re_mult_complex_of_real";
Addsimps [complex_Re_mult_complex_of_real];

Goalw [complex_of_real_def] "Im (z * complex_of_real c) = Im(z) * c";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Im_mult_complex_of_real";
Addsimps [complex_Im_mult_complex_of_real];

Goalw [complex_of_real_def] "Re (complex_of_real c * z) = c * Re(z)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Re_mult_complex_of_real2";
Addsimps [complex_Re_mult_complex_of_real2];

Goalw [complex_of_real_def] "Im (complex_of_real c * z) = c * Im(z)";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Im_mult_complex_of_real2";
Addsimps [complex_Im_mult_complex_of_real2];

(*---------------------------------------------------------------------------*)
(*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *) 
(*---------------------------------------------------------------------------*)

Goalw [rcis_def] "cis a = rcis 1 a";
by (Simp_tac 1);
qed "cis_rcis_eq";

Goalw [rcis_def,cis_def] 
  "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)";
by (auto_tac (claset(),simpset() addsimps [cos_add,sin_add,
    complex_add_mult_distrib2,complex_add_mult_distrib]
     @ complex_mult_ac @ complex_add_ac));
by (auto_tac (claset(),simpset() addsimps [complex_add_mult_distrib2 RS sym,
    complex_mult_assoc RS sym,complex_of_real_mult,complex_of_real_add,
    complex_add_assoc RS sym,i_mult_eq] delsimps [i_mult_eq2]));
by (auto_tac (claset(),simpset() addsimps complex_add_ac));
by (auto_tac (claset(),simpset() addsimps [complex_add_assoc RS sym,
    complex_of_real_add,real_add_mult_distrib2,
    real_diff_def] @ real_mult_ac @ real_add_ac));
qed "rcis_mult";

Goal "cis a * cis b = cis (a + b)";
by (simp_tac (simpset() addsimps [cis_rcis_eq,rcis_mult]) 1);
qed "cis_mult";

Goalw [cis_def] "cis 0 = 1";
by Auto_tac;
qed "cis_zero";
Addsimps [cis_zero];

Goalw [cis_def] "cis 0 = complex_of_real 1";
by Auto_tac;
qed "cis_zero2";
Addsimps [cis_zero2];

Goalw [rcis_def] "rcis 0 a = 0";
by (Simp_tac 1);
qed "rcis_zero_mod";
Addsimps [rcis_zero_mod];

Goalw [rcis_def] "rcis r 0 = complex_of_real r";
by (Simp_tac 1);
qed "rcis_zero_arg";
Addsimps [rcis_zero_arg];

Goalw [complex_of_real_def,complex_one_def] 
   "complex_of_real (-(1::real)) = -(1::complex)";
by (simp_tac (simpset() addsimps [complex_minus]) 1);
qed "complex_of_real_minus_one";

Goal "ii * (ii * x) = - x";
by (simp_tac (simpset() addsimps [complex_mult_assoc RS sym]) 1);
qed "complex_i_mult_minus";
Addsimps [complex_i_mult_minus];

Goal "ii * ii * x = - x";
by (Simp_tac 1);
qed "complex_i_mult_minus2";
Addsimps [complex_i_mult_minus2];

Goalw [cis_def] 
   "cis (real (Suc n) * a) = cis a * cis (real n * a)";
by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
    real_add_mult_distrib,cos_add,sin_add,complex_add_mult_distrib,
    complex_add_mult_distrib2,complex_of_real_add,complex_of_real_mult] 
    @ complex_mult_ac @ complex_add_ac));
by (auto_tac (claset(),simpset() addsimps [complex_add_mult_distrib2 RS sym,
    complex_mult_assoc RS sym,i_mult_eq,complex_of_real_mult,
    complex_of_real_add,complex_add_assoc RS sym,complex_of_real_minus
    RS sym,real_diff_def] @ real_mult_ac delsimps [i_mult_eq2]));
qed "cis_real_of_nat_Suc_mult";

Goal "(cis a) ^ n = cis (real n * a)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [cis_real_of_nat_Suc_mult]));
qed "DeMoivre";

Goalw [rcis_def] 
   "(rcis r a) ^ n = rcis (r ^ n) (real n * a)";
by (auto_tac (claset(),simpset() addsimps [complexpow_mult,
    DeMoivre,complex_of_real_pow]));
qed "DeMoivre2";

Goalw [cis_def] "inverse(cis a) = cis (-a)";
by (auto_tac (claset(),simpset() addsimps [complex_inverse_complex_split,
    complex_of_real_minus,complex_diff_def]));
qed "cis_inverse";
Addsimps [cis_inverse];

Goal "inverse(rcis r a) = rcis (1/r) (-a)";
by (real_div_undefined_case_tac "r=0" 1);
by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
    COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [complex_inverse_complex_split,
    complex_add_mult_distrib2,complex_of_real_mult,rcis_def,cis_def,
    realpow_num_two] @ complex_mult_ac @ real_mult_ac));
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2 RS sym,
    complex_of_real_minus,complex_diff_def]));
qed "rcis_inverse";

Goalw [complex_divide_def] "cis a / cis b = cis (a - b)";
by (auto_tac (claset(),simpset() addsimps [cis_mult,real_diff_def]));
qed "cis_divide";

Goalw [complex_divide_def]
 "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)";
by (real_div_undefined_case_tac "r2=0" 1);
by (simp_tac (simpset() addsimps [rename_numerals DIVISION_BY_ZERO,
    COMPLEX_INVERSE_ZERO]) 1);
by (auto_tac (claset(),simpset() addsimps [rcis_inverse,rcis_mult,
    real_diff_def]));
qed "rcis_divide";

Goalw [cis_def] "Re(cis a) = cos a";
by Auto_tac;
qed "Re_cis";
Addsimps [Re_cis];

Goalw [cis_def] "Im(cis a) = sin a";
by Auto_tac;
qed "Im_cis";
Addsimps [Im_cis];

Goal "cos (real n * a) = Re(cis a ^ n)";
by (auto_tac (claset(),simpset() addsimps [DeMoivre]));
qed "cos_n_Re_cis_pow_n";
 
Goal "sin (real n * a) = Im(cis a ^ n)";
by (auto_tac (claset(),simpset() addsimps [DeMoivre]));
qed "sin_n_Im_cis_pow_n";

Goalw [expi_def,cis_def]
    "expi (ii * complex_of_real y) = \
\    complex_of_real (cos y) + ii * complex_of_real (sin y)";
by Auto_tac;
qed "expi_Im_split";

Goalw [expi_def]
    "expi (ii * complex_of_real y) = cis y";
by Auto_tac;
qed "expi_Im_cis";

Goalw [expi_def] "expi(a + b) = expi(a) * expi(b)";
by (auto_tac (claset(),simpset() addsimps [complex_Re_add,exp_add,
    complex_Im_add,cis_mult RS sym,complex_of_real_mult] @
    complex_mult_ac));
qed "expi_add";

Goalw [expi_def] 
     "expi(complex_of_real x + ii * complex_of_real y) = \
\     complex_of_real (exp(x)) * cis y";
by Auto_tac;
qed "expi_complex_split";

Goalw [expi_def] "expi (0::complex) = 1";
by Auto_tac;
qed "expi_zero";
Addsimps [expi_zero];

goal Complex.thy 
     "Re (w * z) = Re w * Re z - Im w * Im z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Re_mult_eq";

goal Complex.thy 
     "Im (w * z) = Re w * Im z + Im w * Re z";
by (res_inst_tac [("z","z")] eq_Abs_complex 1);
by (res_inst_tac [("z","w")] eq_Abs_complex 1);
by (auto_tac (claset(),simpset() addsimps [complex_mult]));
qed "complex_Im_mult_eq";

goal Complex.thy 
   "EX a r. z = complex_of_real r * expi a";
by (cut_inst_tac [("z","z")] rcis_Ex 1);
by (auto_tac (claset(),simpset() addsimps [expi_def,rcis_def,
    complex_mult_assoc RS sym,complex_of_real_mult]));
by (res_inst_tac [("x","ii * complex_of_real a")] exI 1);
by Auto_tac;
qed "complex_expi_Ex";


(****
Goal "[| - pi < a; a <= pi |] ==> (-pi < a & a <= 0) | (0 <= a & a <= pi)";
by Auto_tac;
qed "lemma_split_interval";

Goalw [arg_def] 
  "[| r ~= 0; - pi < a; a <= pi |] \
\  ==> arg(complex_of_real r * \
\      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
by Auto_tac;
by (cut_inst_tac [("R1.0","0"),("R2.0","r")] real_linear 1);
by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy)
    [rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) @ [real_divide_def,
    real_minus_mult_eq2 RS sym] @ real_mult_ac));
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
by (dtac lemma_split_interval 1 THEN Step_tac 1);
****)