author | paulson |
Tue, 23 Dec 2003 16:53:33 +0100 | |
changeset 14323 | 27724f528f82 |
parent 14322 | fa78e7eb1dac |
child 14324 | c9c6832f9b22 |
src/HOL/Complex/CLim.ML | file | annotate | diff | comparison | revisions | |
src/HOL/Complex/Complex.ML | file | annotate | diff | comparison | revisions | |
src/HOL/Complex/Complex.thy | file | annotate | diff | comparison | revisions | |
src/HOL/Complex/NSCA.ML | file | annotate | diff | comparison | revisions | |
src/HOL/Complex/NSComplex.thy | file | annotate | diff | comparison | revisions | |
src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Complex/CLim.ML Tue Dec 23 16:52:49 2003 +0100 +++ b/src/HOL/Complex/CLim.ML Tue Dec 23 16:53:33 2003 +0100 @@ -1059,7 +1059,7 @@ "x ~= 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"; by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); by (forward_tac [CInfinitesimal_add_not_zero] 1); -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,two_eq_Suc_Suc]) 2); +by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2); by (auto_tac (claset(), simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] delsimps [hcomplex_minus_mult_eq1 RS sym, @@ -1116,7 +1116,7 @@ Goal "x ~= (0::complex) \\<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"; -by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc])); +by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); qed "lemma_complex_mult_inverse_squared"; Addsimps [lemma_complex_mult_inverse_squared];
--- a/src/HOL/Complex/Complex.ML Tue Dec 23 16:52:49 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1588 +0,0 @@ -(* 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 (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 (case_tac "y=0" 1); -by (asm_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, real_abs_def]) 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 [("x","y"),("y","0")] linorder_less_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 (case_tac "r=0" 1); -by (asm_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 (case_tac "r2=0" 1); -by (asm_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 [("x","0"),("y","r")] linorder_less_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); -****) -
--- a/src/HOL/Complex/Complex.thy Tue Dec 23 16:52:49 2003 +0100 +++ b/src/HOL/Complex/Complex.thy Tue Dec 23 16:53:33 2003 +0100 @@ -4,108 +4,1958 @@ Description: Complex numbers *) -Complex = HLog + +theory Complex = HLog: typedef complex = "{p::(real*real). True}" + by blast -instance - complex :: {ord,zero,one,plus,minus,times,power,inverse} +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") + "ii" :: complex ("ii") constdefs (*--- real and Imaginary parts ---*) - - Re :: complex => real + + Re :: "complex => real" "Re(z) == fst(Rep_complex z)" - Im :: complex => real + Im :: "complex => real" "Im(z) == snd(Rep_complex z)" (*----------- modulus ------------*) - cmod :: complex => real - "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)" + cmod :: "complex => real" + "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)" - (*----- injection from reals -----*) - - complex_of_real :: real => complex + (*----- injection from reals -----*) + + complex_of_real :: "real => complex" "complex_of_real r == Abs_complex(r,0::real)" - + (*------- complex conjugate ------*) - cnj :: complex => complex + cnj :: "complex => complex" "cnj z == Abs_complex(Re z, -Im z)" - (*------------ Argand -------------*) + (*------------ Argand -------------*) - sgn :: complex => complex + sgn :: "complex => complex" "sgn z == z / complex_of_real(cmod z)" - arg :: complex => real + arg :: "complex => real" "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a <= pi" - -defs + - complex_zero_def +defs (overloaded) + + complex_zero_def: "0 == Abs_complex(0::real,0)" - complex_one_def + complex_one_def: "1 == Abs_complex(1,0::real)" - (*------ imaginary unit ----------*) - - i_def + (*------ imaginary unit ----------*) + + i_def: "ii == Abs_complex(0::real,1)" (*----------- negation -----------*) - - complex_minus_def - "- (z::complex) == Abs_complex(-Re z, -Im z)" + + complex_minus_def: + "- (z::complex) == Abs_complex(-Re z, -Im z)" - + (*----------- inverse -----------*) - complex_inverse_def + 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 + complex_add_def: "w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))" - complex_diff_def + complex_diff_def: "w - (z::complex) == w + -(z::complex)" - complex_mult_def + 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 + complex_divide_def: "w / (z::complex) == w * inverse z" - + primrec - complexpow_0 "z ^ 0 = complex_of_real 1" - complexpow_Suc "z ^ (Suc n) = (z::complex) * (z ^ n)" + complexpow_0: "z ^ 0 = complex_of_real 1" + complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)" constdefs (* abbreviation for (cos a + i sin a) *) - cis :: real => complex + 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 :: "[real, real] => complex" "rcis r a == complex_of_real r * cis a" (* e ^ (x + iy) *) - expi :: complex => complex + 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)" +apply (auto dest: inj_Abs_complex [THEN injD]) +done +declare Abs_complex_cancel_iff [simp] + +lemma pair_mem_complex: "(x,y) : complex" +apply (unfold complex_def) +apply auto +done +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" +apply (unfold i_def) +apply auto +done +declare complex_Re_i [simp] + +lemma complex_Im_i: "Im(ii) = 1" +apply (unfold i_def) +apply auto +done +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" +apply (unfold complex_of_real_def) +apply auto +done +declare Re_complex_of_real [simp] + +lemma Im_complex_of_real: "Im(complex_of_real z) = 0" +apply (unfold complex_of_real_def) +apply auto +done +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) +apply 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))" +apply (auto dest: sym) +done +declare complex_minus_zero_iff2 [simp] + +lemma complex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::complex))" +apply auto +done + + +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: real_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_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_left_zero [simp] + +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)" +apply (simp (no_asm) add: complex_add_assoc [symmetric]) +done + +declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp] + +lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y" +apply (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus) +done + +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_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]) +apply 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]) +apply 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)" +apply (auto simp add: complex_diff_def complex_add_assoc) +done + + +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 real_diff_mult_distrib2 real_add_mult_distrib2 real_diff_mult_distrib real_add_mult_distrib real_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 real_mult_left_commute real_diff_mult_distrib2 real_add_mult_distrib2) +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)" +apply (unfold complex_divide_def) +apply auto +done +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 + +declare complex_minus_mult_eq1 [symmetric, simp] complex_minus_mult_eq2 [symmetric, simp] + +lemma complex_mult_minus_one: "-(1::complex) * z = -z" +apply (simp (no_asm)) +done +declare complex_mult_minus_one [simp] + +lemma complex_mult_minus_one_right: "z * -(1::complex) = -z" +apply (subst complex_mult_commute) +apply (simp (no_asm)) +done +declare complex_mult_minus_one_right [simp] + +lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)" +apply (simp (no_asm)) +done +declare complex_minus_mult_cancel [simp] + +lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)" +apply (simp (no_asm)) +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 real_add_mult_distrib real_diff_def real_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) ~= 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)" +apply (unfold complex_inverse_def complex_zero_def) +apply auto +done + +lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0" +apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO) +done + +lemma complex_mult_inv_left: "z ~= (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 real_add_divide_distrib [symmetric] real_power_two 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) +apply auto +done +declare complex_mult_inv_left [simp] + +lemma complex_mult_inv_right: "z ~= (0::complex) ==> z * inverse(z) = 1" +apply (auto intro: complex_mult_commute [THEN subst]) +done +declare complex_mult_inv_right [simp] + +lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)" +apply auto +apply (drule_tac f = "%x. x*inverse c" in arg_cong) +apply (simp add: complex_mult_ac) +done + +lemma complex_mult_right_cancel: "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)" +apply (safe) +apply (drule_tac f = "%x. x*inverse c" in arg_cong) +apply (simp add: complex_mult_ac) +done + +lemma complex_inverse_not_zero: "z ~= 0 ==> inverse(z::complex) ~= 0" +apply (safe) +apply (frule complex_mult_right_cancel [THEN iffD2]) +apply (erule_tac [2] V = "inverse z = 0" in thin_rl) +apply (assumption , auto) +done +declare complex_inverse_not_zero [simp] + +lemma complex_mult_not_zero: "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0" +apply (safe) +apply (drule_tac f = "%z. inverse x*z" in arg_cong) +apply (simp add: complex_mult_assoc [symmetric]) +done + +lemmas complex_mult_not_zeroE = complex_mult_not_zero [THEN notE, standard] + +lemma complex_inverse_inverse: "inverse(inverse (x::complex)) = x" +apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) +apply (rule_tac c1 = "inverse x" in complex_mult_right_cancel [THEN iffD1]) +apply (erule complex_inverse_not_zero) +apply (auto dest: complex_inverse_not_zero) +done +declare complex_inverse_inverse [simp] + +lemma complex_inverse_one: "inverse(1::complex) = 1" +apply (unfold complex_one_def) +apply (simp (no_asm) add: complex_inverse) +done +declare complex_inverse_one [simp] + +lemma complex_minus_inverse: "inverse(-x) = -inverse(x::complex)" +apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) +apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1]) +apply force +apply (subst complex_mult_inv_left) +apply auto +done + +lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)" +apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) +apply (case_tac "y = 0", simp add: COMPLEX_INVERSE_ZERO) +apply (rule_tac c1 = "x*y" in complex_mult_left_cancel [THEN iffD1]) +apply (auto simp add: complex_mult_not_zero complex_mult_ac) +apply (auto simp add: complex_mult_not_zero complex_mult_assoc [symmetric]) +done + + +subsection{*Division*} + +(*adding some of these theorems to simpset as for reals: + not 100% convinced for some*) + +lemma complex_times_divide1_eq: "(x::complex) * (y/z) = (x*y)/z" +apply (simp (no_asm) add: complex_divide_def complex_mult_assoc) +done + +lemma complex_times_divide2_eq: "(y/z) * (x::complex) = (y*x)/z" +apply (simp (no_asm) add: complex_divide_def complex_mult_ac) +done + +declare complex_times_divide1_eq [simp] complex_times_divide2_eq [simp] + +lemma complex_divide_divide1_eq: "(x::complex) / (y/z) = (x*z)/y" +apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_ac) +done + +lemma complex_divide_divide2_eq: "((x::complex) / y) / z = x/(y*z)" +apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_assoc) +done + +declare complex_divide_divide1_eq [simp] complex_divide_divide2_eq [simp] + +(** As with multiplication, pull minus signs OUT of the / operator **) + +lemma complex_minus_divide_eq: "(-x) / (y::complex) = - (x/y)" +apply (simp (no_asm) add: complex_divide_def) +done +declare complex_minus_divide_eq [simp] + +lemma complex_divide_minus_eq: "(x / -(y::complex)) = - (x/y)" +apply (simp (no_asm) add: complex_divide_def complex_minus_inverse) +done +declare complex_divide_minus_eq [simp] + +lemma complex_add_divide_distrib: "(x+y)/(z::complex) = x/z + y/z" +apply (simp (no_asm) add: complex_divide_def complex_add_mult_distrib) +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)" +apply (auto dest: inj_complex_of_real [THEN injD]) +done +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") +apply (simp add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) +apply (simp add: complex_inverse complex_of_real_def real_divide_def real_inverse_distrib real_power_two) +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_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_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: "cmod(1) = 1" +apply (unfold cmod_def) +apply (simp add: ); +done +declare complex_mod_one [simp] + +lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x" +apply (unfold complex_of_real_def) +apply (simp (no_asm) add: 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))" +apply (simp (no_asm)) +done + + +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)" +apply (auto dest: inj_cnj [THEN injD]) +done +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 real_power_two) +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 real_power_two) +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_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n" +apply (induct_tac "n") +apply (auto simp add: complex_cnj_mult) +done + +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 (no_asm_simp) add: complex_add complex_cnj complex_of_real_def complex_diff_def complex_minus i_def complex_mult) +done + +lemma complex_cnj_zero: "cnj 0 = 0" +apply (simp add: cnj_def complex_zero_def) +done +declare complex_cnj_zero [simp] + +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 real_power_two) +done + + +subsection{*Algebra*} + +lemma complex_mult_zero_iff: "(x*y = (0::complex)) = (x = 0 | y = 0)" +apply auto +apply (auto intro: ccontr dest: complex_mult_not_zero) +done +declare complex_mult_zero_iff [iff] + +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*} + +(* +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"; +*) + +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 real_power_two) +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 real_power_two) +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: real_power_two real_abs_def) +done + +lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2" +apply (unfold cmod_def) +apply auto +done + +lemma complex_mod_ge_zero: "0 <= 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" +apply (auto intro: abs_eqI1) +done +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 realpow_Suc_cancel_eq) +apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc) +apply (auto simp add: real_diff_def real_power_two real_add_mult_distrib2 real_add_mult_distrib real_add_ac real_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: real_add_mult_distrib2 real_add_mult_distrib real_power_two real_mult_ac real_add_ac) +done + +lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= 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) <= 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: real_add_mult_distrib real_add_mult_distrib2 real_power_two) +done + +lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (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 <= 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) <= cmod(x) + cmod(y)" +apply (rule_tac n = "1" in realpow_increasing) +apply (auto intro: order_trans [OF _ complex_mod_ge_zero] + simp add: real_power_two [symmetric]) +done +declare complex_mod_triangle_ineq [simp] + +lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b <= cmod a" +apply (cut_tac x1 = "b" and y1 = "a" and z = "-cmod b" in complex_mod_triangle_ineq [THEN real_add_le_mono1]) +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 real_diff_mult_distrib2 real_power_two real_diff_mult_distrib real_add_ac real_mult_ac) +done + +lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" +apply (auto intro: order_le_less_trans complex_mod_triangle_ineq) +done + +lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" +apply (auto intro: real_mult_less_mono' simp add: complex_mod_mult) +done + +lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) <= 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) +apply (simp add: ); +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 <= 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 ~= 0 ==> 0 < cmod z" +apply (cut_tac x = "z" in complex_mod_ge_zero) +apply (drule order_le_imp_less_or_eq) +apply auto +done + + +subsection{*A Few More Theorems*} + +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))" +apply (induct_tac "n") +apply auto +done + +lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)" +apply (rule_tac z = "x" in eq_Abs_complex) +apply (simp (no_asm_simp) add: complex_inverse complex_minus real_power_two) +done + +lemma complex_divide_one: "x / (1::complex) = x" +apply (unfold complex_divide_def) +apply (simp (no_asm)) +done +declare complex_divide_one [simp] + +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: complex_inverse_distrib complex_mult_commute) +done +declare complex_inverse_divide [simp] + +lemma complexpow_mult: "((r::complex) * s) ^ n = (r ^ n) * (s ^ n)" +apply (induct_tac "n") +apply (auto simp add: complex_mult_ac) +done + + +subsection{*More Exponentiation*} + +lemma complexpow_zero: "(0::complex) ^ (Suc n) = 0" +apply auto +done +declare complexpow_zero [simp] + +lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0" +apply (induct_tac "n") +apply (auto simp add: complex_mult_not_zero) +done +declare complexpow_not_zero [simp] +declare complexpow_not_zero [intro] + +lemma complexpow_zero_zero: "r ^ n = (0::complex) ==> r = 0" +apply (blast intro: ccontr dest: complexpow_not_zero) +done + +lemma complexpow_i_squared: "ii ^ 2 = -(1::complex)" +apply (unfold i_def) +apply (auto simp add: complex_mult complex_one_def complex_minus numeral_2_eq_2) +done +declare complexpow_i_squared [simp] + +lemma complex_i_not_zero: "ii ~= 0" +apply (unfold i_def complex_zero_def) +apply auto +done +declare complex_i_not_zero [simp] + +lemma complex_mult_eq_zero_cancel1: "x * y ~= (0::complex) ==> x ~= 0" +apply auto +done + +lemma complex_mult_eq_zero_cancel2: "x * y ~= 0 ==> y ~= (0::complex)" +apply auto +done + +lemma complex_mult_not_eq_zero_iff: "(x * y ~= 0) = (x ~= 0 & y ~= (0::complex))" +apply auto +done +declare complex_mult_not_eq_zero_iff [iff] + +lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n" +apply (induct_tac "n") +apply (auto simp add: complex_inverse_distrib) +done + +(*---------------------------------------------------------------------------*) +(* 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 +declare sgn_one [simp] + +lemma sgn_minus: "sgn (-z) = - sgn(z)" +apply (unfold sgn_def) +apply auto +done + +lemma sgn_eq: + "sgn z = z / complex_of_real (cmod z)" +apply (unfold sgn_def) +apply (simp (no_asm)) +done + +lemma complex_split: "EX x y. z = complex_of_real(x) + ii * complex_of_real(y)" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) +done + +lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x" +apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) +done +declare Re_complex_i [simp] + +lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y" +apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) +done +declare Im_complex_i [simp] + +lemma i_mult_eq: "ii * ii = complex_of_real (-1)" +apply (unfold i_def complex_of_real_def) +apply (auto simp add: complex_mult complex_add) +done + +lemma i_mult_eq2: "ii * ii = -(1::complex)" +apply (unfold i_def complex_one_def) +apply (simp (no_asm) add: complex_mult complex_minus) +done +declare i_mult_eq2 [simp] + +lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) = + sqrt (x ^ 2 + y ^ 2)" +apply (auto simp add: complex_mult complex_add i_def complex_of_real_def cmod_def) +done + +lemma complex_eq_Re_eq: + "complex_of_real xa + ii * complex_of_real ya = + complex_of_real xb + ii * complex_of_real yb + ==> xa = xb" +apply (unfold complex_of_real_def i_def) +apply (auto simp add: complex_mult complex_add) +done + +lemma complex_eq_Im_eq: + "complex_of_real xa + ii * complex_of_real ya = + complex_of_real xb + ii * complex_of_real yb + ==> ya = yb" +apply (unfold complex_of_real_def i_def) +apply (auto simp add: complex_mult complex_add) +done + +lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya = + complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" +apply (auto intro: complex_eq_Im_eq complex_eq_Re_eq) +done +declare complex_eq_cancel_iff [iff] + +lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii = + complex_of_real xb + complex_of_real yb * ii ) = ((xa = xb) & (ya = yb))" +apply (auto simp add: complex_mult_commute) +done +declare complex_eq_cancel_iffA [iff] + +lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii = + complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" +apply (auto simp add: complex_mult_commute) +done +declare complex_eq_cancel_iffB [iff] + +lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya = + complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))" +apply (auto simp add: complex_mult_commute) +done +declare complex_eq_cancel_iffC [iff] + +lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y = + complex_of_real xa) = (x = xa & y = 0)" +apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in complex_eq_cancel_iff) +apply (simp del: complex_eq_cancel_iff) +done +declare complex_eq_cancel_iff2 [simp] + +lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii = + complex_of_real xa) = (x = xa & y = 0)" +apply (auto simp add: complex_mult_commute) +done +declare complex_eq_cancel_iff2a [simp] + +lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y = + ii * complex_of_real ya) = (x = 0 & y = ya)" +apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in complex_eq_cancel_iff) +apply (simp del: complex_eq_cancel_iff) +done +declare complex_eq_cancel_iff3 [simp] + +lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii = + ii * complex_of_real ya) = (x = 0 & y = ya)" +apply (auto simp add: complex_mult_commute) +done +declare complex_eq_cancel_iff3a [simp] + +lemma complex_split_Re_zero: + "complex_of_real x + ii * complex_of_real y = 0 + ==> x = 0" +apply (unfold complex_of_real_def i_def complex_zero_def) +apply (auto simp add: complex_mult complex_add) +done + +lemma complex_split_Im_zero: + "complex_of_real x + ii * complex_of_real y = 0 + ==> y = 0" +apply (unfold complex_of_real_def i_def complex_zero_def) +apply (auto simp add: complex_mult complex_add) +done + +lemma Re_sgn: + "Re(sgn z) = Re(z)/cmod z" +apply (unfold sgn_def complex_divide_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_of_real_inverse [symmetric]) +apply (auto simp add: complex_of_real_def complex_mult real_divide_def) +done +declare Re_sgn [simp] + +lemma Im_sgn: + "Im(sgn z) = Im(z)/cmod z" +apply (unfold sgn_def complex_divide_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_of_real_inverse [symmetric]) +apply (auto simp add: complex_of_real_def complex_mult real_divide_def) +done +declare Im_sgn [simp] + +lemma complex_inverse_complex_split: + "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))" +apply (unfold complex_of_real_def i_def) +apply (auto simp add: complex_mult complex_add complex_diff_def complex_minus complex_inverse real_divide_def) +done + +(*----------------------------------------------------------------------------*) +(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) +(* many of the theorems are not used - so should they be kept? *) +(*----------------------------------------------------------------------------*) + +lemma Re_mult_i_eq: + "Re (ii * complex_of_real y) = 0" +apply (unfold i_def complex_of_real_def) +apply (auto simp add: complex_mult) +done +declare Re_mult_i_eq [simp] + +lemma Im_mult_i_eq: + "Im (ii * complex_of_real y) = y" +apply (unfold i_def complex_of_real_def) +apply (auto simp add: complex_mult) +done +declare Im_mult_i_eq [simp] + +lemma complex_mod_mult_i: + "cmod (ii * complex_of_real y) = abs y" +apply (unfold i_def complex_of_real_def) +apply (auto simp add: complex_mult complex_mod real_power_two) +done +declare complex_mod_mult_i [simp] + +lemma cos_arg_i_mult_zero: + "0 < y ==> cos (arg(ii * complex_of_real y)) = 0" +apply (unfold arg_def) +apply (auto simp add: abs_eqI2) +apply (rule_tac a = "pi/2" in someI2) +apply auto +apply (rule order_less_trans [of _ 0]) +apply auto +done +declare cos_arg_i_mult_zero [simp] + +lemma cos_arg_i_mult_zero2: + "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0" +apply (unfold arg_def) +apply (auto simp add: abs_minus_eqI2) +apply (rule_tac a = "- pi/2" in someI2) +apply auto +apply (rule order_trans [of _ 0]) +apply auto +done +declare cos_arg_i_mult_zero2 [simp] + +lemma complex_of_real_not_zero_iff: + "(complex_of_real y ~= 0) = (y ~= 0)" +apply (unfold complex_zero_def complex_of_real_def) +apply auto +done +declare complex_of_real_not_zero_iff [simp] + +lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)" +apply auto +apply (rule ccontr , drule complex_of_real_not_zero_iff [THEN iffD2]) +apply simp +done +declare complex_of_real_zero_iff [simp] + +lemma cos_arg_i_mult_zero3: "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0" +apply (cut_tac x = "y" and y = "0" in linorder_less_linear) +apply auto +done +declare cos_arg_i_mult_zero3 [simp] + + +subsection{*Finally! Polar Form for Complex Numbers*} + +lemma complex_split_polar: "EX r a. z = complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))" +apply (cut_tac z = "z" in complex_split) +apply (auto simp add: polar_Ex complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) +done + +lemma rcis_Ex: "EX r a. z = rcis r a" +apply (unfold rcis_def cis_def) +apply (rule complex_split_polar) +done + +lemma Re_complex_polar: "Re(complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a" +apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) +done +declare Re_complex_polar [simp] + +lemma Re_rcis: "Re(rcis r a) = r * cos a" +apply (unfold rcis_def cis_def) +apply auto +done +declare Re_rcis [simp] + +lemma Im_complex_polar: "Im(complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a" +apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) +done +declare Im_complex_polar [simp] + +lemma Im_rcis: "Im(rcis r a) = r * sin a" +apply (unfold rcis_def cis_def) +apply auto +done +declare Im_rcis [simp] + +lemma complex_mod_complex_polar: "cmod (complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r" +apply (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult real_add_mult_distrib2 [symmetric] realpow_mult complex_mult_ac real_mult_ac simp del: realpow_Suc) +done +declare complex_mod_complex_polar [simp] + +lemma complex_mod_rcis: "cmod(rcis r a) = abs r" +apply (unfold rcis_def cis_def) +apply auto +done +declare complex_mod_rcis [simp] + +lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" +apply (unfold cmod_def) +apply (rule real_sqrt_eq_iff [THEN iffD2]) +apply (auto simp add: complex_mult_cnj) +done + +lemma complex_Re_cnj: "Re(cnj z) = Re z" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_cnj) +done +declare complex_Re_cnj [simp] + +lemma complex_Im_cnj: "Im(cnj z) = - Im z" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_cnj) +done +declare complex_Im_cnj [simp] + +lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_cnj complex_mult) +done +declare complex_In_mult_cnj_zero [simp] + +lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = "w" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done + +lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c" +apply (unfold complex_of_real_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done +declare complex_Re_mult_complex_of_real [simp] + +lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c" +apply (unfold complex_of_real_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done +declare complex_Im_mult_complex_of_real [simp] + +lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)" +apply (unfold complex_of_real_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done +declare complex_Re_mult_complex_of_real2 [simp] + +lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)" +apply (unfold complex_of_real_def) +apply (rule_tac z = "z" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done +declare complex_Im_mult_complex_of_real2 [simp] + +(*---------------------------------------------------------------------------*) +(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *) +(*---------------------------------------------------------------------------*) + +lemma cis_rcis_eq: "cis a = rcis 1 a" +apply (unfold rcis_def) +apply (simp (no_asm)) +done + +lemma rcis_mult: + "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)" +apply (unfold rcis_def cis_def) +apply (auto simp add: cos_add sin_add complex_add_mult_distrib2 complex_add_mult_distrib complex_mult_ac complex_add_ac) +apply (auto simp add: complex_add_mult_distrib2 [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2) +apply (auto simp add: complex_add_ac) +apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add real_add_mult_distrib2 real_diff_def mult_ac add_ac) +done + +lemma cis_mult: "cis a * cis b = cis (a + b)" +apply (simp (no_asm) add: cis_rcis_eq rcis_mult) +done + +lemma cis_zero: "cis 0 = 1" +apply (unfold cis_def) +apply auto +done +declare cis_zero [simp] + +lemma cis_zero2: "cis 0 = complex_of_real 1" +apply (unfold cis_def) +apply auto +done +declare cis_zero2 [simp] + +lemma rcis_zero_mod: "rcis 0 a = 0" +apply (unfold rcis_def) +apply (simp (no_asm)) +done +declare rcis_zero_mod [simp] + +lemma rcis_zero_arg: "rcis r 0 = complex_of_real r" +apply (unfold rcis_def) +apply (simp (no_asm)) +done +declare rcis_zero_arg [simp] + +lemma complex_of_real_minus_one: + "complex_of_real (-(1::real)) = -(1::complex)" +apply (unfold complex_of_real_def complex_one_def) +apply (simp (no_asm) add: complex_minus) +done + +lemma complex_i_mult_minus: "ii * (ii * x) = - x" +apply (simp (no_asm) add: complex_mult_assoc [symmetric]) +done +declare complex_i_mult_minus [simp] + +lemma complex_i_mult_minus2: "ii * ii * x = - x" +apply (simp (no_asm)) +done +declare complex_i_mult_minus2 [simp] + +lemma cis_real_of_nat_Suc_mult: + "cis (real (Suc n) * a) = cis a * cis (real n * a)" +apply (unfold cis_def) +apply (auto simp add: 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) +apply (auto simp add: complex_add_mult_distrib2 [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2) +done + +lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" +apply (induct_tac "n") +apply (auto simp add: cis_real_of_nat_Suc_mult) +done + +lemma DeMoivre2: + "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" +apply (unfold rcis_def) +apply (auto simp add: complexpow_mult DeMoivre complex_of_real_pow) +done + +lemma cis_inverse: "inverse(cis a) = cis (-a)" +apply (unfold cis_def) +apply (auto simp add: complex_inverse_complex_split complex_of_real_minus complex_diff_def) +done +declare cis_inverse [simp] + +lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)" +apply (case_tac "r=0") +apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) +apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def real_power_two complex_mult_ac real_mult_ac) +apply (auto simp add: real_add_mult_distrib2 [symmetric] complex_of_real_minus complex_diff_def) +done + +lemma cis_divide: "cis a / cis b = cis (a - b)" +apply (unfold complex_divide_def) +apply (auto simp add: cis_mult real_diff_def) +done + +lemma rcis_divide: + "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)" +apply (unfold complex_divide_def) +apply (case_tac "r2=0") +apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) +apply (auto simp add: rcis_inverse rcis_mult real_diff_def) +done + +lemma Re_cis: "Re(cis a) = cos a" +apply (unfold cis_def) +apply auto +done +declare Re_cis [simp] + +lemma Im_cis: "Im(cis a) = sin a" +apply (unfold cis_def) +apply auto +done +declare Im_cis [simp] + +lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" +apply (auto simp add: DeMoivre) +done + +lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" +apply (auto simp add: DeMoivre) +done + +lemma expi_Im_split: + "expi (ii * complex_of_real y) = + complex_of_real (cos y) + ii * complex_of_real (sin y)" +apply (unfold expi_def cis_def) +apply auto +done + +lemma expi_Im_cis: + "expi (ii * complex_of_real y) = cis y" +apply (unfold expi_def) +apply auto +done + +lemma expi_add: "expi(a + b) = expi(a) * expi(b)" +apply (unfold expi_def) +apply (auto simp add: complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult complex_mult_ac) +done + +lemma expi_complex_split: + "expi(complex_of_real x + ii * complex_of_real y) = + complex_of_real (exp(x)) * cis y" +apply (unfold expi_def) +apply auto +done + +lemma expi_zero: "expi (0::complex) = 1" +apply (unfold expi_def) +apply auto +done +declare expi_zero [simp] + +lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = "w" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done + +lemma complex_Im_mult_eq: + "Im (w * z) = Re w * Im z + Im w * Re z" +apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = "w" in eq_Abs_complex) +apply (auto simp add: complex_mult) +done + +lemma complex_expi_Ex: + "EX a r. z = complex_of_real r * expi a" +apply (cut_tac z = "z" in rcis_Ex) +apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult) +apply (rule_tac x = "ii * complex_of_real a" in exI) +apply auto +done + + +(**** +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 [("x","0"),("y","r")] linorder_less_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 safe); +****) + + +ML +{* +val complex_zero_def = thm"complex_zero_def"; +val complex_one_def = thm"complex_one_def"; +val complex_minus_def = thm"complex_minus_def"; +val complex_diff_def = thm"complex_diff_def"; +val complex_divide_def = thm"complex_divide_def"; +val complex_mult_def = thm"complex_mult_def"; +val complex_add_def = thm"complex_add_def"; +val complex_of_real_def = thm"complex_of_real_def"; +val i_def = thm"i_def"; +val expi_def = thm"expi_def"; +val cis_def = thm"cis_def"; +val rcis_def = thm"rcis_def"; +val cmod_def = thm"cmod_def"; +val cnj_def = thm"cnj_def"; +val sgn_def = thm"sgn_def"; +val arg_def = thm"arg_def"; +val complexpow_0 = thm"complexpow_0"; +val complexpow_Suc = thm"complexpow_Suc"; + +val inj_Rep_complex = thm"inj_Rep_complex"; +val inj_Abs_complex = thm"inj_Abs_complex"; +val Abs_complex_cancel_iff = thm"Abs_complex_cancel_iff"; +val pair_mem_complex = thm"pair_mem_complex"; +val Abs_complex_inverse2 = thm"Abs_complex_inverse2"; +val eq_Abs_complex = thm"eq_Abs_complex"; +val Re = thm"Re"; +val Im = thm"Im"; +val Abs_complex_cancel = thm"Abs_complex_cancel"; +val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff"; +val complex_Re_zero = thm"complex_Re_zero"; +val complex_Im_zero = thm"complex_Im_zero"; +val complex_Re_one = thm"complex_Re_one"; +val complex_Im_one = thm"complex_Im_one"; +val complex_Re_i = thm"complex_Re_i"; +val complex_Im_i = thm"complex_Im_i"; +val Re_complex_of_real_zero = thm"Re_complex_of_real_zero"; +val Im_complex_of_real_zero = thm"Im_complex_of_real_zero"; +val Re_complex_of_real_one = thm"Re_complex_of_real_one"; +val Im_complex_of_real_one = thm"Im_complex_of_real_one"; +val Re_complex_of_real = thm"Re_complex_of_real"; +val Im_complex_of_real = thm"Im_complex_of_real"; +val complex_minus = thm"complex_minus"; +val complex_Re_minus = thm"complex_Re_minus"; +val complex_Im_minus = thm"complex_Im_minus"; +val complex_minus_minus = thm"complex_minus_minus"; +val inj_complex_minus = thm"inj_complex_minus"; +val complex_minus_zero = thm"complex_minus_zero"; +val complex_minus_zero_iff = thm"complex_minus_zero_iff"; +val complex_minus_zero_iff2 = thm"complex_minus_zero_iff2"; +val complex_minus_not_zero_iff = thm"complex_minus_not_zero_iff"; +val complex_add = thm"complex_add"; +val complex_Re_add = thm"complex_Re_add"; +val complex_Im_add = thm"complex_Im_add"; +val complex_add_commute = thm"complex_add_commute"; +val complex_add_assoc = thm"complex_add_assoc"; +val complex_add_left_commute = thm"complex_add_left_commute"; +val complex_add_zero_left = thm"complex_add_zero_left"; +val complex_add_zero_right = thm"complex_add_zero_right"; +val complex_add_minus_right_zero = thm"complex_add_minus_right_zero"; +val complex_add_minus_left_zero = thm"complex_add_minus_left_zero"; +val complex_add_minus_cancel = thm"complex_add_minus_cancel"; +val complex_minus_add_cancel = thm"complex_minus_add_cancel"; +val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus"; +val complex_minus_add_distrib = thm"complex_minus_add_distrib"; +val complex_add_left_cancel = thm"complex_add_left_cancel"; +val complex_add_right_cancel = thm"complex_add_right_cancel"; +val complex_eq_minus_iff = thm"complex_eq_minus_iff"; +val complex_eq_minus_iff2 = thm"complex_eq_minus_iff2"; +val complex_diff_0 = thm"complex_diff_0"; +val complex_diff_0_right = thm"complex_diff_0_right"; +val complex_diff_self = thm"complex_diff_self"; +val complex_diff = thm"complex_diff"; +val complex_diff_eq_eq = thm"complex_diff_eq_eq"; +val complex_mult = thm"complex_mult"; +val complex_mult_commute = thm"complex_mult_commute"; +val complex_mult_assoc = thm"complex_mult_assoc"; +val complex_mult_left_commute = thm"complex_mult_left_commute"; +val complex_mult_one_left = thm"complex_mult_one_left"; +val complex_mult_one_right = thm"complex_mult_one_right"; +val complex_mult_zero_left = thm"complex_mult_zero_left"; +val complex_mult_zero_right = thm"complex_mult_zero_right"; +val complex_divide_zero = thm"complex_divide_zero"; +val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1"; +val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2"; +val complex_mult_minus_one = thm"complex_mult_minus_one"; +val complex_mult_minus_one_right = thm"complex_mult_minus_one_right"; +val complex_minus_mult_cancel = thm"complex_minus_mult_cancel"; +val complex_minus_mult_commute = thm"complex_minus_mult_commute"; +val complex_add_mult_distrib = thm"complex_add_mult_distrib"; +val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2"; +val complex_zero_not_eq_one = thm"complex_zero_not_eq_one"; +val complex_inverse = thm"complex_inverse"; +val COMPLEX_INVERSE_ZERO = thm"COMPLEX_INVERSE_ZERO"; +val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO"; +val complex_mult_inv_left = thm"complex_mult_inv_left"; +val complex_mult_inv_right = thm"complex_mult_inv_right"; +val complex_mult_left_cancel = thm"complex_mult_left_cancel"; +val complex_mult_right_cancel = thm"complex_mult_right_cancel"; +val complex_inverse_not_zero = thm"complex_inverse_not_zero"; +val complex_mult_not_zero = thm"complex_mult_not_zero"; +val complex_inverse_inverse = thm"complex_inverse_inverse"; +val complex_inverse_one = thm"complex_inverse_one"; +val complex_minus_inverse = thm"complex_minus_inverse"; +val complex_inverse_distrib = thm"complex_inverse_distrib"; +val complex_times_divide1_eq = thm"complex_times_divide1_eq"; +val complex_times_divide2_eq = thm"complex_times_divide2_eq"; +val complex_divide_divide1_eq = thm"complex_divide_divide1_eq"; +val complex_divide_divide2_eq = thm"complex_divide_divide2_eq"; +val complex_minus_divide_eq = thm"complex_minus_divide_eq"; +val complex_divide_minus_eq = thm"complex_divide_minus_eq"; +val complex_add_divide_distrib = thm"complex_add_divide_distrib"; +val inj_complex_of_real = thm"inj_complex_of_real"; +val complex_of_real_one = thm"complex_of_real_one"; +val complex_of_real_zero = thm"complex_of_real_zero"; +val complex_of_real_eq_iff = thm"complex_of_real_eq_iff"; +val complex_of_real_minus = thm"complex_of_real_minus"; +val complex_of_real_inverse = thm"complex_of_real_inverse"; +val complex_of_real_add = thm"complex_of_real_add"; +val complex_of_real_diff = thm"complex_of_real_diff"; +val complex_of_real_mult = thm"complex_of_real_mult"; +val complex_of_real_divide = thm"complex_of_real_divide"; +val complex_of_real_pow = thm"complex_of_real_pow"; +val complex_mod = thm"complex_mod"; +val complex_mod_zero = thm"complex_mod_zero"; +val complex_mod_one = thm"complex_mod_one"; +val complex_mod_complex_of_real = thm"complex_mod_complex_of_real"; +val complex_of_real_abs = thm"complex_of_real_abs"; +val complex_cnj = thm"complex_cnj"; +val inj_cnj = thm"inj_cnj"; +val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff"; +val complex_cnj_cnj = thm"complex_cnj_cnj"; +val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real"; +val complex_mod_cnj = thm"complex_mod_cnj"; +val complex_cnj_minus = thm"complex_cnj_minus"; +val complex_cnj_inverse = thm"complex_cnj_inverse"; +val complex_cnj_add = thm"complex_cnj_add"; +val complex_cnj_diff = thm"complex_cnj_diff"; +val complex_cnj_mult = thm"complex_cnj_mult"; +val complex_cnj_divide = thm"complex_cnj_divide"; +val complex_cnj_one = thm"complex_cnj_one"; +val complex_cnj_pow = thm"complex_cnj_pow"; +val complex_add_cnj = thm"complex_add_cnj"; +val complex_diff_cnj = thm"complex_diff_cnj"; +val complex_cnj_zero = thm"complex_cnj_zero"; +val complex_cnj_zero_iff = thm"complex_cnj_zero_iff"; +val complex_mult_cnj = thm"complex_mult_cnj"; +val complex_mult_zero_iff = thm"complex_mult_zero_iff"; +val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero"; +val complex_diff_mult_distrib = thm"complex_diff_mult_distrib"; +val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2"; +val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel"; +val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat"; +val complex_mod_minus = thm"complex_mod_minus"; +val complex_mod_mult_cnj = thm"complex_mod_mult_cnj"; +val complex_mod_squared = thm"complex_mod_squared"; +val complex_mod_ge_zero = thm"complex_mod_ge_zero"; +val abs_cmod_cancel = thm"abs_cmod_cancel"; +val complex_mod_mult = thm"complex_mod_mult"; +val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq"; +val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod"; +val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2"; +val real_sum_squared_expand = thm"real_sum_squared_expand"; +val complex_mod_triangle_squared = thm"complex_mod_triangle_squared"; +val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod"; +val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq"; +val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2"; +val complex_mod_diff_commute = thm"complex_mod_diff_commute"; +val complex_mod_add_less = thm"complex_mod_add_less"; +val complex_mod_mult_less = thm"complex_mod_mult_less"; +val complex_mod_diff_ineq = thm"complex_mod_diff_ineq"; +val complex_Re_le_cmod = thm"complex_Re_le_cmod"; +val complex_mod_gt_zero = thm"complex_mod_gt_zero"; +val complex_mod_complexpow = thm"complex_mod_complexpow"; +val complexpow_minus = thm"complexpow_minus"; +val complex_inverse_minus = thm"complex_inverse_minus"; +val complex_divide_one = thm"complex_divide_one"; +val complex_mod_inverse = thm"complex_mod_inverse"; +val complex_mod_divide = thm"complex_mod_divide"; +val complex_inverse_divide = thm"complex_inverse_divide"; +val complexpow_mult = thm"complexpow_mult"; +val complexpow_zero = thm"complexpow_zero"; +val complexpow_not_zero = thm"complexpow_not_zero"; +val complexpow_zero_zero = thm"complexpow_zero_zero"; +val complexpow_i_squared = thm"complexpow_i_squared"; +val complex_i_not_zero = thm"complex_i_not_zero"; +val complex_mult_eq_zero_cancel1 = thm"complex_mult_eq_zero_cancel1"; +val complex_mult_eq_zero_cancel2 = thm"complex_mult_eq_zero_cancel2"; +val complex_mult_not_eq_zero_iff = thm"complex_mult_not_eq_zero_iff"; +val complexpow_inverse = thm"complexpow_inverse"; +val sgn_zero = thm"sgn_zero"; +val sgn_one = thm"sgn_one"; +val sgn_minus = thm"sgn_minus"; +val sgn_eq = thm"sgn_eq"; +val complex_split = thm"complex_split"; +val Re_complex_i = thm"Re_complex_i"; +val Im_complex_i = thm"Im_complex_i"; +val i_mult_eq = thm"i_mult_eq"; +val i_mult_eq2 = thm"i_mult_eq2"; +val cmod_i = thm"cmod_i"; +val complex_eq_Re_eq = thm"complex_eq_Re_eq"; +val complex_eq_Im_eq = thm"complex_eq_Im_eq"; +val complex_eq_cancel_iff = thm"complex_eq_cancel_iff"; +val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA"; +val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB"; +val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC"; +val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2"; +val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a"; +val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3"; +val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a"; +val complex_split_Re_zero = thm"complex_split_Re_zero"; +val complex_split_Im_zero = thm"complex_split_Im_zero"; +val Re_sgn = thm"Re_sgn"; +val Im_sgn = thm"Im_sgn"; +val complex_inverse_complex_split = thm"complex_inverse_complex_split"; +val Re_mult_i_eq = thm"Re_mult_i_eq"; +val Im_mult_i_eq = thm"Im_mult_i_eq"; +val complex_mod_mult_i = thm"complex_mod_mult_i"; +val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero"; +val cos_arg_i_mult_zero2 = thm"cos_arg_i_mult_zero2"; +val complex_of_real_not_zero_iff = thm"complex_of_real_not_zero_iff"; +val complex_of_real_zero_iff = thm"complex_of_real_zero_iff"; +val cos_arg_i_mult_zero3 = thm"cos_arg_i_mult_zero3"; +val complex_split_polar = thm"complex_split_polar"; +val rcis_Ex = thm"rcis_Ex"; +val Re_complex_polar = thm"Re_complex_polar"; +val Re_rcis = thm"Re_rcis"; +val Im_complex_polar = thm"Im_complex_polar"; +val Im_rcis = thm"Im_rcis"; +val complex_mod_complex_polar = thm"complex_mod_complex_polar"; +val complex_mod_rcis = thm"complex_mod_rcis"; +val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj"; +val complex_Re_cnj = thm"complex_Re_cnj"; +val complex_Im_cnj = thm"complex_Im_cnj"; +val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero"; +val complex_Re_mult = thm"complex_Re_mult"; +val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real"; +val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real"; +val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2"; +val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2"; +val cis_rcis_eq = thm"cis_rcis_eq"; +val rcis_mult = thm"rcis_mult"; +val cis_mult = thm"cis_mult"; +val cis_zero = thm"cis_zero"; +val cis_zero2 = thm"cis_zero2"; +val rcis_zero_mod = thm"rcis_zero_mod"; +val rcis_zero_arg = thm"rcis_zero_arg"; +val complex_of_real_minus_one = thm"complex_of_real_minus_one"; +val complex_i_mult_minus = thm"complex_i_mult_minus"; +val complex_i_mult_minus2 = thm"complex_i_mult_minus2"; +val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult"; +val DeMoivre = thm"DeMoivre"; +val DeMoivre2 = thm"DeMoivre2"; +val cis_inverse = thm"cis_inverse"; +val rcis_inverse = thm"rcis_inverse"; +val cis_divide = thm"cis_divide"; +val rcis_divide = thm"rcis_divide"; +val Re_cis = thm"Re_cis"; +val Im_cis = thm"Im_cis"; +val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n"; +val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n"; +val expi_Im_split = thm"expi_Im_split"; +val expi_Im_cis = thm"expi_Im_cis"; +val expi_add = thm"expi_add"; +val expi_complex_split = thm"expi_complex_split"; +val expi_zero = thm"expi_zero"; +val complex_Re_mult_eq = thm"complex_Re_mult_eq"; +val complex_Im_mult_eq = thm"complex_Im_mult_eq"; +val complex_expi_Ex = thm"complex_expi_Ex"; + +val complex_add_ac = thms"complex_add_ac"; +val complex_mult_ac = thms"complex_mult_ac"; +*} + end
--- a/src/HOL/Complex/NSCA.ML Tue Dec 23 16:52:49 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Tue Dec 23 16:53:33 2003 +0100 @@ -838,11 +838,10 @@ by (res_inst_tac [("z","X x")] eq_Abs_complex 1); by (res_inst_tac [("z","Y x")] eq_Abs_complex 1); by (auto_tac (claset(),HOL_ss addsimps [complex_minus,complex_add, - complex_mod,pair_mem_complex RS Abs_complex_inverse,snd_conv, - fst_conv,two_eq_Suc_Suc])); + complex_mod, snd_conv, fst_conv,numeral_2_eq_2])); by (rtac (realpow_two_abs RS subst) 1); by (res_inst_tac [("x1","xa + - xb")] (realpow_two_abs RS subst) 1); -by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1); +by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1); by (rtac lemma_sqrt_hcomplex_capprox 1); by Auto_tac; qed "hcomplex_capproxI"; @@ -869,11 +868,11 @@ by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac); by (Ultra_tac 1); by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1); -by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc])); +by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc])); by (rtac ccontr 1 THEN dtac real_leI 1); by (dtac order_less_le_trans 1 THEN assume_tac 1); by (dtac (real_sqrt_ge_abs1 RSN (2,order_less_le_trans)) 1); -by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc RS sym])); +by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2 RS sym])); qed "CFinite_HFinite_Re"; Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite \ @@ -901,12 +900,12 @@ by (res_inst_tac [("x","2*(u + v)")] exI 1); by (Ultra_tac 1); by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1); -by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc])); +by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc])); by (subgoal_tac "0 < u" 1 THEN arith_tac 2); by (subgoal_tac "0 < v" 1 THEN arith_tac 2); by (rtac (realpow_two_abs RS subst) 1); by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1); -by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1); +by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1); by (rtac lemma_sqrt_hcomplex_capprox 1); by Auto_tac; qed "HFinite_Re_Im_CFinite";
--- a/src/HOL/Complex/NSComplex.thy Tue Dec 23 16:52:49 2003 +0100 +++ b/src/HOL/Complex/NSComplex.thy Tue Dec 23 16:53:33 2003 +0100 @@ -866,7 +866,7 @@ lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj two_eq_Suc_Suc) +apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2) done @@ -951,7 +951,7 @@ lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2" apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj two_eq_Suc_Suc) +apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) done lemma hcmod_ge_zero: "(0::hypreal) <= hcmod x" @@ -976,9 +976,9 @@ apply (rule_tac z = "x" in eq_Abs_hcomplex) apply (rule_tac z = "y" in eq_Abs_hcomplex) apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult - two_eq_Suc_Suc realpow_two [symmetric] + numeral_2_eq_2 realpow_two [symmetric] simp del: realpow_Suc) -apply (auto simp add: two_eq_Suc_Suc [symmetric] complex_mod_add_squared_eq +apply (auto simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq hypreal_add [symmetric] hypreal_mult [symmetric] hypreal_of_real_def [symmetric]) done @@ -1000,9 +1000,9 @@ apply (rule_tac z = "x" in eq_Abs_hcomplex) apply (rule_tac z = "y" in eq_Abs_hcomplex) apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add - hypreal_le realpow_two [symmetric] two_eq_Suc_Suc + hypreal_le realpow_two [symmetric] numeral_2_eq_2 simp del: realpow_Suc) -apply (simp (no_asm) add: two_eq_Suc_Suc [symmetric]) +apply (simp (no_asm) add: numeral_2_eq_2 [symmetric]) done declare hcmod_triangle_squared [simp] @@ -1191,7 +1191,7 @@ declare hcomplex_i_mult_eq [simp] lemma hcomplexpow_i_squared: "iii ^ 2 = - 1" -apply (simp (no_asm) add: two_eq_Suc_Suc) +apply (simp (no_asm) add: numeral_2_eq_2) done declare hcomplexpow_i_squared [simp] @@ -1296,7 +1296,7 @@ ( *f* sqrt) (x ^ 2 + y ^ 2)" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i two_eq_Suc_Suc) +apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2) done lemma hcomplex_eq_hRe_eq: @@ -1420,7 +1420,7 @@ iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split two_eq_Suc_Suc) +apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2) done lemma hRe_mult_i_eq:
--- a/src/HOL/IsaMakefile Tue Dec 23 16:52:49 2003 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 23 16:53:33 2003 +0100 @@ -168,8 +168,7 @@ Complex/Complex_Main.thy\ Complex/CLim.ML Complex/CLim.thy\ Complex/CSeries.ML Complex/CSeries.thy\ - Complex/CStar.ML Complex/CStar.thy\ - Complex/Complex.ML Complex/Complex.thy\ + Complex/CStar.ML Complex/CStar.thy Complex/Complex.thy\ Complex/ComplexArith0.ML Complex/ComplexArith0.thy\ Complex/ComplexBin.ML Complex/ComplexBin.thy\ Complex/NSCA.ML Complex/NSCA.thy\