tidying of the complex numbers
authorpaulson
Tue Feb 03 11:06:36 2004 +0100 (2004-02-03)
changeset 1437367a628beb981
parent 14372 51ddf8963c95
child 14374 61de62096768
tidying of the complex numbers
src/HOL/Complex/CLim.ML
src/HOL/Complex/CSeries.ML
src/HOL/Complex/Complex.thy
src/HOL/Complex/ComplexArith0.ML
src/HOL/Complex/ComplexBin.ML
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSComplexBin.ML
src/HOL/Complex/ex/BinEx.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Complex/CLim.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -284,7 +284,7 @@
     1.4  (*** NSCLIM_zero, CLIM_zero, etc. ***)
     1.5  
     1.6  Goal "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0";
     1.7 -by (res_inst_tac [("z1","l")] (complex_add_minus_right_zero RS subst) 1);
     1.8 +by (res_inst_tac [("a1","l")] (right_minus RS subst) 1);
     1.9  by (rewtac complex_diff_def);
    1.10  by (rtac NSCLIM_add 1 THEN Auto_tac);
    1.11  qed "NSCLIM_zero";
    1.12 @@ -701,7 +701,7 @@
    1.13  by (Step_tac 1);
    1.14  by (dres_inst_tac [("x","x - a")] spec 1);
    1.15  by (dres_inst_tac [("x","x + a")] spec 2);
    1.16 -by (auto_tac (claset(), simpset() addsimps complex_add_ac));
    1.17 +by (auto_tac (claset(), simpset() addsimps add_ac));
    1.18  qed "CDERIV_CLIM_iff";
    1.19  
    1.20  Goalw [cderiv_def] "(CDERIV f x :> D) = \
    1.21 @@ -755,10 +755,10 @@
    1.22      [mem_cinfmal_iff RS sym,hcomplex_add_commute]));
    1.23  by (dres_inst_tac [("c","xa + - hcomplex_of_complex x")] capprox_mult1 1);
    1.24  by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite
    1.25 -    RS subsetD],simpset() addsimps [hcomplex_mult_assoc]));
    1.26 +    RS subsetD],simpset() addsimps [mult_assoc]));
    1.27  by (dres_inst_tac [("x3","D")] (CFinite_hcomplex_of_complex RSN
    1.28      (2,CInfinitesimal_CFinite_mult) RS (mem_cinfmal_iff RS iffD1)) 1);
    1.29 -by (blast_tac (claset() addIs [capprox_trans,hcomplex_mult_commute RS subst,
    1.30 +by (blast_tac (claset() addIs [capprox_trans,mult_commute RS subst,
    1.31      (capprox_minus_iff RS iffD2)]) 1);
    1.32  qed "NSCDERIV_isNSContc";
    1.33  
    1.34 @@ -833,10 +833,9 @@
    1.35  by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1);
    1.36  by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4);
    1.37  by (auto_tac (claset() addSIs [capprox_add_mono1],
    1.38 -      simpset() addsimps [hcomplex_add_mult_distrib, right_distrib, 
    1.39 -			  hcomplex_mult_commute, hcomplex_add_assoc]));
    1.40 -by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
    1.41 -    (hcomplex_add_commute RS subst) 1);
    1.42 +     simpset() addsimps [left_distrib, right_distrib, mult_commute, add_assoc]));
    1.43 +by (res_inst_tac [("b1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
    1.44 +    (add_commute RS subst) 1);
    1.45  by (auto_tac (claset() addSIs [CInfinitesimal_add_capprox_self2 RS capprox_sym,
    1.46  			       CInfinitesimal_add, CInfinitesimal_mult,
    1.47  			       CInfinitesimal_hcomplex_of_complex_mult,
    1.48 @@ -853,7 +852,7 @@
    1.49  Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D";
    1.50  by (asm_full_simp_tac 
    1.51      (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff,
    1.52 -                         minus_mult_right, complex_add_mult_distrib2 RS sym,
    1.53 +                         minus_mult_right, right_distrib RS sym,
    1.54                           complex_diff_def] 
    1.55               delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1);
    1.56  by (etac (NSCLIM_const RS NSCLIM_mult) 1);
    1.57 @@ -866,9 +865,8 @@
    1.58  
    1.59  Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D";
    1.60  by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1);
    1.61 -by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1);
    1.62 -by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym] 
    1.63 -                   delsimps [complex_minus_add_distrib, complex_minus_minus]
    1.64 +by (res_inst_tac [("t","f x")] (minus_minus RS subst) 1);
    1.65 +by (asm_simp_tac (simpset() addsimps [minus_add_distrib RS sym] 
    1.66                     delsimps [minus_add_distrib, minus_minus]
    1.67  
    1.68  ) 1);
    1.69 @@ -1032,12 +1030,12 @@
    1.70  by (dtac (CDERIV_Id RS CDERIV_mult) 2);
    1.71  by (auto_tac (claset(), 
    1.72                simpset() addsimps [complex_of_real_add RS sym,
    1.73 -                        complex_add_mult_distrib,real_of_nat_Suc] 
    1.74 +                        left_distrib,real_of_nat_Suc] 
    1.75                   delsimps [complex_of_real_add]));
    1.76  by (case_tac "n" 1);
    1.77  by (auto_tac (claset(), 
    1.78 -              simpset() addsimps [complex_mult_assoc, complex_add_commute]));
    1.79 -by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
    1.80 +              simpset() addsimps [mult_assoc, add_commute]));
    1.81 +by (auto_tac (claset(),simpset() addsimps [mult_commute]));
    1.82  qed "CDERIV_pow";
    1.83  Addsimps [CDERIV_pow,simplify (simpset()) CDERIV_pow];
    1.84  
    1.85 @@ -1095,10 +1093,9 @@
    1.86  
    1.87  Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \
    1.88  \     ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
    1.89 -by (rtac (complex_mult_commute RS subst) 1);
    1.90 -by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
    1.91 -    power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
    1.92 -complex_minus_mult_eq1 RS sym]) 1);
    1.93 +by (rtac (mult_commute RS subst) 1);
    1.94 +by (asm_simp_tac (simpset() addsimps [minus_mult_left,
    1.95 +    power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym]) 1);
    1.96  by (fold_goals_tac [o_def]);
    1.97  by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
    1.98  qed "CDERIV_inverse_fun";
    1.99 @@ -1126,8 +1123,8 @@
   1.100  by (dtac CDERIV_mult 2);
   1.101  by (REPEAT(assume_tac 1));
   1.102  by (asm_full_simp_tac
   1.103 -    (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
   1.104 -                         power_inverse,complex_minus_mult_eq1] @ complex_mult_ac 
   1.105 +    (simpset() addsimps [complex_divide_def, right_distrib,
   1.106 +                         power_inverse,minus_mult_left] @ mult_ac 
   1.107         delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
   1.108  qed "CDERIV_quotient";
   1.109  
   1.110 @@ -1161,7 +1158,7 @@
   1.111  by (Step_tac 1);
   1.112  by (res_inst_tac 
   1.113      [("x","%z. if  z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
   1.114 -by (auto_tac (claset(),simpset() addsimps [complex_mult_assoc,
   1.115 +by (auto_tac (claset(),simpset() addsimps [mult_assoc,
   1.116      CLAIM "z ~= x ==> z - x ~= (0::complex)"]));
   1.117  by (auto_tac (claset(),simpset() addsimps [isContc_iff,CDERIV_iff]));
   1.118  by (ALLGOALS(rtac (CLIM_equal RS iffD1)));
     2.1 --- a/src/HOL/Complex/CSeries.ML	Tue Feb 03 10:19:21 2004 +0100
     2.2 +++ b/src/HOL/Complex/CSeries.ML	Tue Feb 03 11:06:36 2004 +0100
     2.3 @@ -37,7 +37,7 @@
     2.4  by (induct_tac "n" 1);
     2.5  by (Auto_tac);
     2.6  by (auto_tac (claset(),simpset() addsimps 
     2.7 -    [complex_add_mult_distrib2]));
     2.8 +    [right_distrib]));
     2.9  qed "sumc_mult";
    2.10  
    2.11  Goal "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f";
    2.12 @@ -49,7 +49,7 @@
    2.13  Goal "n < p ==> sumc 0 p f + \
    2.14  \                - sumc 0 n f = sumc n p f";
    2.15  by (dres_inst_tac [("f1","f")] (sumc_split_add RS sym) 1);
    2.16 -by (asm_simp_tac (simpset() addsimps complex_add_ac) 1);
    2.17 +by (asm_simp_tac (simpset() addsimps add_ac) 1);
    2.18  qed "sumc_split_add_minus";
    2.19  
    2.20  Goal "cmod(sumc m n f) <= sumr m n (%i. cmod(f i))";
    2.21 @@ -67,7 +67,7 @@
    2.22  Goal "sumc 0 n (%i. r) = complex_of_real (real n) * r";
    2.23  by (induct_tac "n" 1);
    2.24  by (auto_tac (claset(),
    2.25 -              simpset() addsimps [complex_add_mult_distrib,
    2.26 +              simpset() addsimps [left_distrib,
    2.27                                    complex_of_real_add RS sym,
    2.28                                    real_of_nat_Suc]));
    2.29  qed "sumc_const";
    2.30 @@ -109,7 +109,7 @@
    2.31  by (induct_tac "na" 1);
    2.32  by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
    2.33                                        real_of_nat_Suc,complex_of_real_add RS sym,
    2.34 -                                      complex_add_mult_distrib]));
    2.35 +                                      left_distrib]));
    2.36  qed_spec_mp "sumc_interval_const";
    2.37  
    2.38  Goal "(ALL n. m <= n --> f n = r) & m <= na \
    2.39 @@ -117,7 +117,7 @@
    2.40  by (induct_tac "na" 1);
    2.41  by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
    2.42                                        real_of_nat_Suc,complex_of_real_add RS sym,
    2.43 -                                      complex_add_mult_distrib]));
    2.44 +                                      left_distrib]));
    2.45  qed_spec_mp "sumc_interval_const2";
    2.46  
    2.47  (*** 
     3.1 --- a/src/HOL/Complex/Complex.thy	Tue Feb 03 10:19:21 2004 +0100
     3.2 +++ b/src/HOL/Complex/Complex.thy	Tue Feb 03 11:06:36 2004 +0100
     3.3 @@ -1,13 +1,15 @@
     3.4  (*  Title:       Complex.thy
     3.5      Author:      Jacques D. Fleuriot
     3.6      Copyright:   2001 University of Edinburgh
     3.7 -    Description: Complex numbers
     3.8  *)
     3.9  
    3.10 +header {* Complex numbers *}
    3.11 +
    3.12  theory Complex = HLog:
    3.13  
    3.14 -typedef complex = "{p::(real*real). True}"
    3.15 -  by blast
    3.16 +subsection {* Representation of complex numbers *}
    3.17 +
    3.18 +datatype complex = Complex real real
    3.19  
    3.20  instance complex :: zero ..
    3.21  instance complex :: one ..
    3.22 @@ -18,18 +20,19 @@
    3.23  instance complex :: power ..
    3.24  
    3.25  consts
    3.26 -  "ii"    :: complex        ("ii")
    3.27 +  "ii"    :: complex    ("\<i>")
    3.28 +
    3.29 +consts Re :: "complex => real"
    3.30 +primrec "Re (Complex x y) = x"
    3.31 +
    3.32 +consts Im :: "complex => real"
    3.33 +primrec "Im (Complex x y) = y"
    3.34 +
    3.35 +lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
    3.36 +  by (induct z) simp
    3.37  
    3.38  constdefs
    3.39  
    3.40 -  (*--- real and Imaginary parts ---*)
    3.41 -
    3.42 -  Re :: "complex => real"
    3.43 -  "Re(z) == fst(Rep_complex z)"
    3.44 -
    3.45 -  Im :: "complex => real"
    3.46 -  "Im(z) == snd(Rep_complex z)"
    3.47 -
    3.48    (*----------- modulus ------------*)
    3.49  
    3.50    cmod :: "complex => real"
    3.51 @@ -38,12 +41,12 @@
    3.52    (*----- injection from reals -----*)
    3.53  
    3.54    complex_of_real :: "real => complex"
    3.55 -  "complex_of_real r == Abs_complex(r,0::real)"
    3.56 +  "complex_of_real r == Complex r 0"
    3.57  
    3.58    (*------- complex conjugate ------*)
    3.59  
    3.60    cnj :: "complex => complex"
    3.61 -  "cnj z == Abs_complex(Re z, -Im z)"
    3.62 +  "cnj z == Complex (Re z) (-Im z)"
    3.63  
    3.64    (*------------ Argand -------------*)
    3.65  
    3.66 @@ -57,41 +60,29 @@
    3.67  defs (overloaded)
    3.68  
    3.69    complex_zero_def:
    3.70 -  "0 == Abs_complex(0::real,0)"
    3.71 +  "0 == Complex 0 0"
    3.72  
    3.73    complex_one_def:
    3.74 -  "1 == Abs_complex(1,0::real)"
    3.75 -
    3.76 -  (*------ imaginary unit ----------*)
    3.77 +  "1 == Complex 1 0"
    3.78  
    3.79 -  i_def:
    3.80 -  "ii == Abs_complex(0::real,1)"
    3.81 -
    3.82 -  (*----------- negation -----------*)
    3.83 +  i_def: "ii == Complex 0 1"
    3.84  
    3.85 -  complex_minus_def:
    3.86 -  "- (z::complex) == Abs_complex(-Re z, -Im z)"
    3.87 -
    3.88 +  complex_minus_def: "- z == Complex (- Re z) (- Im z)"
    3.89  
    3.90 -  (*----------- inverse -----------*)
    3.91    complex_inverse_def:
    3.92 -  "inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2),
    3.93 -                            -Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))"
    3.94 +   "inverse z ==
    3.95 +    Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) (- Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))"
    3.96  
    3.97    complex_add_def:
    3.98 -  "w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))"
    3.99 +    "z + w == Complex (Re z + Re w) (Im z + Im w)"
   3.100  
   3.101    complex_diff_def:
   3.102 -  "w - (z::complex) == w + -(z::complex)"
   3.103 +    "z - w == z + - (w::complex)"
   3.104  
   3.105 -  complex_mult_def:
   3.106 -  "w * (z::complex) == Abs_complex(Re(w) * Re(z) - Im(w) * Im(z),
   3.107 -			Re(w) * Im(z) + Im(w) * Re(z))"
   3.108 +  complex_mult_def: 
   3.109 +    "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
   3.110  
   3.111 -
   3.112 -  (*----------- division ----------*)
   3.113 -  complex_divide_def:
   3.114 -  "w / (z::complex) == w * inverse z"
   3.115 +  complex_divide_def: "w / (z::complex) == w * inverse z"
   3.116  
   3.117  
   3.118  constdefs
   3.119 @@ -109,429 +100,152 @@
   3.120    "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
   3.121  
   3.122  
   3.123 -lemma inj_Rep_complex: "inj Rep_complex"
   3.124 -apply (rule inj_on_inverseI)
   3.125 -apply (rule Rep_complex_inverse)
   3.126 -done
   3.127 -
   3.128 -lemma inj_Abs_complex: "inj Abs_complex"
   3.129 -apply (rule inj_on_inverseI)
   3.130 -apply (rule Abs_complex_inverse)
   3.131 -apply (simp (no_asm) add: complex_def)
   3.132 -done
   3.133 -declare inj_Abs_complex [THEN injD, simp]
   3.134 -
   3.135 -lemma Abs_complex_cancel_iff: "(Abs_complex x = Abs_complex y) = (x = y)"
   3.136 -by (auto dest: inj_Abs_complex [THEN injD])
   3.137 -declare Abs_complex_cancel_iff [simp]
   3.138 +lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
   3.139 +  by (induct z, induct w) simp
   3.140  
   3.141 -lemma pair_mem_complex: "(x,y) : complex"
   3.142 -by (unfold complex_def, auto)
   3.143 -declare pair_mem_complex [simp]
   3.144 -
   3.145 -lemma Abs_complex_inverse2: "Rep_complex (Abs_complex (x,y)) = (x,y)"
   3.146 -apply (simp (no_asm) add: Abs_complex_inverse)
   3.147 -done
   3.148 -declare Abs_complex_inverse2 [simp]
   3.149 -
   3.150 -lemma eq_Abs_complex: "(!!x y. z = Abs_complex(x,y) ==> P) ==> P"
   3.151 -apply (rule_tac p = "Rep_complex z" in PairE)
   3.152 -apply (drule_tac f = Abs_complex in arg_cong)
   3.153 -apply (force simp add: Rep_complex_inverse)
   3.154 -done
   3.155 -
   3.156 -lemma Re: "Re(Abs_complex(x,y)) = x"
   3.157 -apply (unfold Re_def)
   3.158 -apply (simp (no_asm))
   3.159 -done
   3.160 +lemma Re: "Re(Complex x y) = x"
   3.161 +by simp
   3.162  declare Re [simp]
   3.163  
   3.164 -lemma Im: "Im(Abs_complex(x,y)) = y"
   3.165 -apply (unfold Im_def)
   3.166 -apply (simp (no_asm))
   3.167 -done
   3.168 +lemma Im: "Im(Complex x y) = y"
   3.169 +by simp
   3.170  declare Im [simp]
   3.171  
   3.172 -lemma Abs_complex_cancel: "Abs_complex(Re(z),Im(z)) = z"
   3.173 -apply (rule_tac z = z in eq_Abs_complex)
   3.174 -apply (simp (no_asm_simp))
   3.175 -done
   3.176 -declare Abs_complex_cancel [simp]
   3.177 -
   3.178  lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"
   3.179 -apply (rule_tac z = w in eq_Abs_complex)
   3.180 -apply (rule_tac z = z in eq_Abs_complex)
   3.181 -apply (auto dest: inj_Abs_complex [THEN injD])
   3.182 -done
   3.183 +by (induct w, induct z, simp)
   3.184  
   3.185  lemma complex_Re_zero: "Re 0 = 0"
   3.186 -apply (unfold complex_zero_def)
   3.187 -apply (simp (no_asm))
   3.188 -done
   3.189 +by (simp add: complex_zero_def)
   3.190  
   3.191  lemma complex_Im_zero: "Im 0 = 0"
   3.192 -apply (unfold complex_zero_def)
   3.193 -apply (simp (no_asm))
   3.194 -done
   3.195 +by (simp add: complex_zero_def)
   3.196  declare complex_Re_zero [simp] complex_Im_zero [simp]
   3.197  
   3.198  lemma complex_Re_one: "Re 1 = 1"
   3.199 -apply (unfold complex_one_def)
   3.200 -apply (simp (no_asm))
   3.201 -done
   3.202 +by (simp add: complex_one_def)
   3.203  declare complex_Re_one [simp]
   3.204  
   3.205  lemma complex_Im_one: "Im 1 = 0"
   3.206 -apply (unfold complex_one_def)
   3.207 -apply (simp (no_asm))
   3.208 -done
   3.209 +by (simp add: complex_one_def)
   3.210  declare complex_Im_one [simp]
   3.211  
   3.212  lemma complex_Re_i: "Re(ii) = 0"
   3.213 -by (unfold i_def, auto)
   3.214 +by (simp add: i_def)
   3.215  declare complex_Re_i [simp]
   3.216  
   3.217  lemma complex_Im_i: "Im(ii) = 1"
   3.218 -by (unfold i_def, auto)
   3.219 +by (simp add: i_def)
   3.220  declare complex_Im_i [simp]
   3.221  
   3.222  lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0"
   3.223 -apply (unfold complex_of_real_def)
   3.224 -apply (simp (no_asm))
   3.225 -done
   3.226 +by (simp add: complex_of_real_def)
   3.227  declare Re_complex_of_real_zero [simp]
   3.228  
   3.229  lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0"
   3.230 -apply (unfold complex_of_real_def)
   3.231 -apply (simp (no_asm))
   3.232 -done
   3.233 +by (simp add: complex_of_real_def)
   3.234  declare Im_complex_of_real_zero [simp]
   3.235  
   3.236  lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1"
   3.237 -apply (unfold complex_of_real_def)
   3.238 -apply (simp (no_asm))
   3.239 -done
   3.240 +by (simp add: complex_of_real_def)
   3.241  declare Re_complex_of_real_one [simp]
   3.242  
   3.243  lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0"
   3.244 -apply (unfold complex_of_real_def)
   3.245 -apply (simp (no_asm))
   3.246 -done
   3.247 +by (simp add: complex_of_real_def)
   3.248  declare Im_complex_of_real_one [simp]
   3.249  
   3.250  lemma Re_complex_of_real: "Re(complex_of_real z) = z"
   3.251 -by (unfold complex_of_real_def, auto)
   3.252 +by (simp add: complex_of_real_def)
   3.253  declare Re_complex_of_real [simp]
   3.254  
   3.255  lemma Im_complex_of_real: "Im(complex_of_real z) = 0"
   3.256 -by (unfold complex_of_real_def, auto)
   3.257 +by (simp add: complex_of_real_def)
   3.258  declare Im_complex_of_real [simp]
   3.259  
   3.260  
   3.261  subsection{*Negation*}
   3.262  
   3.263 -lemma complex_minus: "- Abs_complex(x,y) = Abs_complex(-x,-y)"
   3.264 -apply (unfold complex_minus_def)
   3.265 -apply (simp (no_asm))
   3.266 -done
   3.267 +lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)"
   3.268 +by (simp add: complex_minus_def)
   3.269  
   3.270  lemma complex_Re_minus: "Re (-z) = - Re z"
   3.271 -apply (unfold Re_def)
   3.272 -apply (rule_tac z = z in eq_Abs_complex)
   3.273 -apply (auto simp add: complex_minus)
   3.274 -done
   3.275 +by (simp add: complex_minus_def)
   3.276  
   3.277  lemma complex_Im_minus: "Im (-z) = - Im z"
   3.278 -apply (unfold Im_def)
   3.279 -apply (rule_tac z = z in eq_Abs_complex)
   3.280 -apply (auto simp add: complex_minus)
   3.281 -done
   3.282 -
   3.283 -lemma complex_minus_minus: "- (- z) = (z::complex)"
   3.284 -apply (unfold complex_minus_def)
   3.285 -apply (simp (no_asm))
   3.286 -done
   3.287 -declare complex_minus_minus [simp]
   3.288 -
   3.289 -lemma inj_complex_minus: "inj(%r::complex. -r)"
   3.290 -apply (rule inj_onI)
   3.291 -apply (drule_tac f = uminus in arg_cong, simp)
   3.292 -done
   3.293 +by (simp add: complex_minus_def)
   3.294  
   3.295  lemma complex_minus_zero: "-(0::complex) = 0"
   3.296 -apply (unfold complex_zero_def)
   3.297 -apply (simp (no_asm) add: complex_minus)
   3.298 -done
   3.299 +by (simp add: complex_minus_def complex_zero_def)
   3.300  declare complex_minus_zero [simp]
   3.301  
   3.302  lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))"
   3.303 -apply (rule_tac z = x in eq_Abs_complex)
   3.304 -apply (auto dest: inj_Abs_complex [THEN injD]
   3.305 -            simp add: complex_zero_def complex_minus)
   3.306 -done
   3.307 +by (induct x, simp add: complex_minus_def complex_zero_def)
   3.308  declare complex_minus_zero_iff [simp]
   3.309  
   3.310 -lemma complex_minus_zero_iff2: "(0 = -x) = (x = (0::real))"
   3.311 -by (auto dest: sym)
   3.312 -declare complex_minus_zero_iff2 [simp]
   3.313 -
   3.314 -lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))"
   3.315 -by auto
   3.316 -
   3.317  
   3.318  subsection{*Addition*}
   3.319  
   3.320 -lemma complex_add:
   3.321 -      "Abs_complex(x1,y1) + Abs_complex(x2,y2) = Abs_complex(x1+x2,y1+y2)"
   3.322 -apply (unfold complex_add_def)
   3.323 -apply (simp (no_asm))
   3.324 -done
   3.325 +lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
   3.326 +by (simp add: complex_add_def)
   3.327  
   3.328  lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)"
   3.329 -apply (unfold Re_def)
   3.330 -apply (rule_tac z = x in eq_Abs_complex)
   3.331 -apply (rule_tac z = y in eq_Abs_complex)
   3.332 -apply (auto simp add: complex_add)
   3.333 -done
   3.334 +by (simp add: complex_add_def)
   3.335  
   3.336  lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)"
   3.337 -apply (unfold Im_def)
   3.338 -apply (rule_tac z = x in eq_Abs_complex)
   3.339 -apply (rule_tac z = y in eq_Abs_complex)
   3.340 -apply (auto simp add: complex_add)
   3.341 -done
   3.342 +by (simp add: complex_add_def)
   3.343  
   3.344  lemma complex_add_commute: "(u::complex) + v = v + u"
   3.345 -apply (unfold complex_add_def)
   3.346 -apply (simp (no_asm) add: real_add_commute)
   3.347 -done
   3.348 +by (simp add: complex_add_def add_commute)
   3.349  
   3.350  lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)"
   3.351 -apply (unfold complex_add_def)
   3.352 -apply (simp (no_asm) add: real_add_assoc)
   3.353 -done
   3.354 -
   3.355 -lemma complex_add_left_commute: "(x::complex) + (y + z) = y + (x + z)"
   3.356 -apply (unfold complex_add_def)
   3.357 -apply (simp (no_asm) add: add_left_commute)
   3.358 -done
   3.359 -
   3.360 -lemmas complex_add_ac = complex_add_assoc complex_add_commute
   3.361 -                      complex_add_left_commute
   3.362 +by (simp add: complex_add_def add_assoc)
   3.363  
   3.364  lemma complex_add_zero_left: "(0::complex) + z = z"
   3.365 -apply (unfold complex_add_def complex_zero_def)
   3.366 -apply (simp (no_asm))
   3.367 -done
   3.368 -declare complex_add_zero_left [simp]
   3.369 +by (simp add: complex_add_def complex_zero_def)
   3.370  
   3.371  lemma complex_add_zero_right: "z + (0::complex) = z"
   3.372 -apply (unfold complex_add_def complex_zero_def)
   3.373 -apply (simp (no_asm))
   3.374 -done
   3.375 -declare complex_add_zero_right [simp]
   3.376 -
   3.377 -lemma complex_add_minus_right_zero:
   3.378 -      "z + -z = (0::complex)"
   3.379 -apply (unfold complex_add_def complex_minus_def complex_zero_def)
   3.380 -apply (simp (no_asm))
   3.381 -done
   3.382 -declare complex_add_minus_right_zero [simp]
   3.383 -
   3.384 -lemma complex_add_minus_left:
   3.385 -      "-z + z = (0::complex)"
   3.386 -apply (unfold complex_add_def complex_minus_def complex_zero_def)
   3.387 -apply (simp (no_asm))
   3.388 -done
   3.389 -
   3.390 -lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
   3.391 -apply (simp (no_asm) add: complex_add_assoc [symmetric])
   3.392 -done
   3.393 -
   3.394 -lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
   3.395 -by (simp add: complex_add_minus_left complex_add_assoc [symmetric])
   3.396 -
   3.397 -declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]
   3.398 -
   3.399 -lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y"
   3.400 -by (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus)
   3.401 +by (simp add: complex_add_def complex_zero_def)
   3.402  
   3.403 -lemma complex_minus_add_distrib: "-(x + y) = -x + -(y::complex)"
   3.404 -apply (rule_tac z = x in eq_Abs_complex)
   3.405 -apply (rule_tac z = y in eq_Abs_complex)
   3.406 -apply (auto simp add: complex_minus complex_add)
   3.407 -done
   3.408 -declare complex_minus_add_distrib [simp]
   3.409 -
   3.410 -lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"
   3.411 -apply safe
   3.412 -apply (drule_tac f = "%t.-x + t" in arg_cong)
   3.413 -apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])
   3.414 -done
   3.415 -declare complex_add_left_cancel [iff]
   3.416 -
   3.417 -lemma complex_add_right_cancel: "(y + (x::complex)= z + x) = (y = z)"
   3.418 -apply (simp (no_asm) add: complex_add_commute)
   3.419 -done
   3.420 -declare complex_add_right_cancel [simp]
   3.421 -
   3.422 -lemma complex_eq_minus_iff: "((x::complex) = y) = (0 = x + - y)"
   3.423 -apply safe
   3.424 -apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)
   3.425 -done
   3.426 -
   3.427 -lemma complex_eq_minus_iff2: "((x::complex) = y) = (x + - y = 0)"
   3.428 -apply safe
   3.429 -apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)
   3.430 -done
   3.431 -
   3.432 -lemma complex_diff_0: "(0::complex) - x = -x"
   3.433 -apply (simp (no_asm) add: complex_diff_def)
   3.434 -done
   3.435 -
   3.436 -lemma complex_diff_0_right: "x - (0::complex) = x"
   3.437 -apply (simp (no_asm) add: complex_diff_def)
   3.438 -done
   3.439 -
   3.440 -lemma complex_diff_self: "x - x = (0::complex)"
   3.441 -apply (simp (no_asm) add: complex_diff_def)
   3.442 -done
   3.443 -
   3.444 -declare complex_diff_0 [simp] complex_diff_0_right [simp] complex_diff_self [simp]
   3.445 +lemma complex_add_minus_left: "-z + z = (0::complex)"
   3.446 +by (simp add: complex_add_def complex_minus_def complex_zero_def)
   3.447  
   3.448  lemma complex_diff:
   3.449 -      "Abs_complex(x1,y1) - Abs_complex(x2,y2) = Abs_complex(x1-x2,y1-y2)"
   3.450 -apply (unfold complex_diff_def)
   3.451 -apply (simp (no_asm) add: complex_add complex_minus)
   3.452 -done
   3.453 -
   3.454 -lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"
   3.455 -by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)
   3.456 -
   3.457 +      "Complex x1 y1 - Complex x2 y2 = Complex (x1-x2) (y1-y2)"
   3.458 +by (simp add: complex_add_def complex_minus_def complex_diff_def)
   3.459  
   3.460  subsection{*Multiplication*}
   3.461  
   3.462  lemma complex_mult:
   3.463 -      "Abs_complex(x1,y1) * Abs_complex(x2,y2) =
   3.464 -       Abs_complex(x1*x2 - y1*y2,x1*y2 + y1*x2)"
   3.465 -apply (unfold complex_mult_def)
   3.466 -apply (simp (no_asm))
   3.467 -done
   3.468 +     "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
   3.469 +by (simp add: complex_mult_def)
   3.470  
   3.471  lemma complex_mult_commute: "(w::complex) * z = z * w"
   3.472 -apply (unfold complex_mult_def)
   3.473 -apply (simp (no_asm) add: real_mult_commute real_add_commute)
   3.474 -done
   3.475 +by (simp add: complex_mult_def mult_commute add_commute)
   3.476  
   3.477  lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
   3.478 -apply (unfold complex_mult_def)
   3.479 -apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc right_diff_distrib right_distrib left_diff_distrib left_distrib mult_left_commute)
   3.480 -done
   3.481 -
   3.482 -lemma complex_mult_left_commute: "(x::complex) * (y * z) = y * (x * z)"
   3.483 -apply (unfold complex_mult_def)
   3.484 -apply (simp (no_asm) add: complex_Re_Im_cancel_iff mult_left_commute right_diff_distrib right_distrib)
   3.485 -done
   3.486 -
   3.487 -lemmas complex_mult_ac = complex_mult_assoc complex_mult_commute
   3.488 -                      complex_mult_left_commute
   3.489 +by (simp add: complex_mult_def mult_ac add_ac 
   3.490 +              right_diff_distrib right_distrib left_diff_distrib left_distrib)
   3.491  
   3.492  lemma complex_mult_one_left: "(1::complex) * z = z"
   3.493 -apply (unfold complex_one_def)
   3.494 -apply (rule_tac z = z in eq_Abs_complex)
   3.495 -apply (simp (no_asm_simp) add: complex_mult)
   3.496 -done
   3.497 -declare complex_mult_one_left [simp]
   3.498 +by (simp add: complex_mult_def complex_one_def)
   3.499  
   3.500  lemma complex_mult_one_right: "z * (1::complex) = z"
   3.501 -apply (simp (no_asm) add: complex_mult_commute)
   3.502 -done
   3.503 -declare complex_mult_one_right [simp]
   3.504 -
   3.505 -lemma complex_mult_zero_left: "(0::complex) * z = 0"
   3.506 -apply (unfold complex_zero_def)
   3.507 -apply (rule_tac z = z in eq_Abs_complex)
   3.508 -apply (simp (no_asm_simp) add: complex_mult)
   3.509 -done
   3.510 -declare complex_mult_zero_left [simp]
   3.511 -
   3.512 -lemma complex_mult_zero_right: "z * 0 = (0::complex)"
   3.513 -apply (simp (no_asm) add: complex_mult_commute)
   3.514 -done
   3.515 -declare complex_mult_zero_right [simp]
   3.516 -
   3.517 -lemma complex_divide_zero: "0 / z = (0::complex)"
   3.518 -by (unfold complex_divide_def, auto)
   3.519 -declare complex_divide_zero [simp]
   3.520 -
   3.521 -lemma complex_minus_mult_eq1: "-(x * y) = -x * (y::complex)"
   3.522 -apply (rule_tac z = x in eq_Abs_complex)
   3.523 -apply (rule_tac z = y in eq_Abs_complex)
   3.524 -apply (auto simp add: complex_mult complex_minus real_diff_def)
   3.525 -done
   3.526 -
   3.527 -lemma complex_minus_mult_eq2: "-(x * y) = x * -(y::complex)"
   3.528 -apply (rule_tac z = x in eq_Abs_complex)
   3.529 -apply (rule_tac z = y in eq_Abs_complex)
   3.530 -apply (auto simp add: complex_mult complex_minus real_diff_def)
   3.531 -done
   3.532 -
   3.533 -lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)"
   3.534 -apply (rule_tac z = z1 in eq_Abs_complex)
   3.535 -apply (rule_tac z = z2 in eq_Abs_complex)
   3.536 -apply (rule_tac z = w in eq_Abs_complex)
   3.537 -apply (auto simp add: complex_mult complex_add left_distrib real_diff_def add_ac)
   3.538 -done
   3.539 -
   3.540 -lemma complex_add_mult_distrib2: "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)"
   3.541 -apply (rule_tac z1 = "z1 + z2" in complex_mult_commute [THEN ssubst])
   3.542 -apply (simp (no_asm) add: complex_add_mult_distrib)
   3.543 -apply (simp (no_asm) add: complex_mult_commute)
   3.544 -done
   3.545 -
   3.546 -lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1"
   3.547 -apply (unfold complex_zero_def complex_one_def)
   3.548 -apply (simp (no_asm) add: complex_Re_Im_cancel_iff)
   3.549 -done
   3.550 -declare complex_zero_not_eq_one [simp]
   3.551 -declare complex_zero_not_eq_one [THEN not_sym, simp]
   3.552 +by (simp add: complex_mult_def complex_one_def)
   3.553  
   3.554  
   3.555  subsection{*Inverse*}
   3.556  
   3.557  lemma complex_inverse:
   3.558 -     "inverse (Abs_complex(x,y)) =
   3.559 -      Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
   3.560 -apply (unfold complex_inverse_def)
   3.561 -apply (simp (no_asm))
   3.562 -done
   3.563 -
   3.564 -lemma COMPLEX_INVERSE_ZERO: "inverse 0 = (0::complex)"
   3.565 -by (unfold complex_inverse_def complex_zero_def, auto)
   3.566 -
   3.567 -lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0"
   3.568 -apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO)
   3.569 -done
   3.570 -
   3.571 -instance complex :: division_by_zero
   3.572 -proof
   3.573 -  fix x :: complex
   3.574 -  show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO)
   3.575 -  show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 
   3.576 -qed
   3.577 +     "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
   3.578 +by (simp add: complex_inverse_def)
   3.579  
   3.580  lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
   3.581 -apply (rule_tac z = z in eq_Abs_complex)
   3.582 +apply (induct z) 
   3.583 +apply (rename_tac x y) 
   3.584  apply (auto simp add: complex_mult complex_inverse complex_one_def 
   3.585         complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
   3.586  apply (drule_tac y = y in real_sum_squares_not_zero)
   3.587  apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
   3.588  done
   3.589 -declare complex_mult_inv_left [simp]
   3.590 -
   3.591 -lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1"
   3.592 -by (auto intro: complex_mult_commute [THEN subst])
   3.593 -declare complex_mult_inv_right [simp]
   3.594  
   3.595  
   3.596  subsection {* The field of complex numbers *}
   3.597 @@ -556,14 +270,14 @@
   3.598    show "1 * z = z"
   3.599      by (rule complex_mult_one_left) 
   3.600    show "0 \<noteq> (1::complex)"
   3.601 -    by (rule complex_zero_not_eq_one) 
   3.602 +    by (simp add: complex_zero_def complex_one_def)
   3.603    show "(u + v) * w = u * w + v * w"
   3.604 -    by (rule complex_add_mult_distrib) 
   3.605 +    by (simp add: complex_mult_def complex_add_def left_distrib real_diff_def add_ac)
   3.606    show "z+u = z+v ==> u=v"
   3.607      proof -
   3.608        assume eq: "z+u = z+v" 
   3.609        hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
   3.610 -      thus "u = v" by (simp add: complex_add_minus_left)
   3.611 +      thus "u = v" by (simp add: complex_add_minus_left complex_add_zero_left)
   3.612      qed
   3.613    assume neq: "w \<noteq> 0"
   3.614    thus "z / w = z * inverse w"
   3.615 @@ -572,40 +286,33 @@
   3.616      by (simp add: neq complex_mult_inv_left) 
   3.617  qed
   3.618  
   3.619 +instance complex :: division_by_zero
   3.620 +proof
   3.621 +  show inv: "inverse 0 = (0::complex)"
   3.622 +    by (simp add: complex_inverse_def complex_zero_def)
   3.623 +  fix x :: complex
   3.624 +  show "x/0 = 0" 
   3.625 +    by (simp add: complex_divide_def inv)
   3.626 +qed
   3.627  
   3.628 -lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
   3.629 -apply (simp)
   3.630 -done
   3.631  
   3.632  subsection{*Embedding Properties for @{term complex_of_real} Map*}
   3.633  
   3.634 -lemma inj_complex_of_real: "inj complex_of_real"
   3.635 -apply (rule inj_onI)
   3.636 -apply (auto dest: inj_Abs_complex [THEN injD] simp add: complex_of_real_def)
   3.637 -done
   3.638 -
   3.639 -lemma complex_of_real_one:
   3.640 -      "complex_of_real 1 = 1"
   3.641 -apply (unfold complex_one_def complex_of_real_def)
   3.642 -apply (rule refl)
   3.643 -done
   3.644 +lemma complex_of_real_one: "complex_of_real 1 = 1"
   3.645 +by (simp add: complex_one_def complex_of_real_def)
   3.646  declare complex_of_real_one [simp]
   3.647  
   3.648 -lemma complex_of_real_zero:
   3.649 -      "complex_of_real 0 = 0"
   3.650 -apply (unfold complex_zero_def complex_of_real_def)
   3.651 -apply (rule refl)
   3.652 -done
   3.653 +lemma complex_of_real_zero: "complex_of_real 0 = 0"
   3.654 +by (simp add: complex_zero_def complex_of_real_def)
   3.655  declare complex_of_real_zero [simp]
   3.656  
   3.657  lemma complex_of_real_eq_iff:
   3.658       "(complex_of_real x = complex_of_real y) = (x = y)"
   3.659 -by (auto dest: inj_complex_of_real [THEN injD])
   3.660 +by (simp add: complex_of_real_def) 
   3.661  declare complex_of_real_eq_iff [iff]
   3.662  
   3.663  lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
   3.664 -apply (simp (no_asm) add: complex_of_real_def complex_minus)
   3.665 -done
   3.666 +by (simp add: complex_of_real_def complex_minus)
   3.667  
   3.668  lemma complex_of_real_inverse:
   3.669   "complex_of_real(inverse x) = inverse(complex_of_real x)"
   3.670 @@ -615,133 +322,93 @@
   3.671  done
   3.672  
   3.673  lemma complex_of_real_add:
   3.674 - "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
   3.675 -apply (simp (no_asm) add: complex_add complex_of_real_def)
   3.676 -done
   3.677 +     "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
   3.678 +by (simp add: complex_add complex_of_real_def)
   3.679  
   3.680  lemma complex_of_real_diff:
   3.681 - "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
   3.682 -apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
   3.683 -done
   3.684 +     "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
   3.685 +by (simp add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
   3.686  
   3.687  lemma complex_of_real_mult:
   3.688 - "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
   3.689 -apply (simp (no_asm) add: complex_mult complex_of_real_def)
   3.690 -done
   3.691 +     "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
   3.692 +by (simp add: complex_mult complex_of_real_def)
   3.693  
   3.694  lemma complex_of_real_divide:
   3.695        "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
   3.696 -apply (unfold complex_divide_def)
   3.697 -apply (case_tac "y=0")
   3.698 -apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
   3.699 -apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
   3.700 +apply (simp add: complex_divide_def)
   3.701 +apply (case_tac "y=0", simp)
   3.702 +apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
   3.703  done
   3.704  
   3.705 -lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)"
   3.706 -apply (unfold cmod_def)
   3.707 -apply (simp (no_asm))
   3.708 -done
   3.709 +lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
   3.710 +by (simp add: cmod_def)
   3.711  
   3.712  lemma complex_mod_zero: "cmod(0) = 0"
   3.713 -apply (unfold cmod_def)
   3.714 -apply (simp (no_asm))
   3.715 -done
   3.716 +by (simp add: cmod_def)
   3.717  declare complex_mod_zero [simp]
   3.718  
   3.719  lemma complex_mod_one [simp]: "cmod(1) = 1"
   3.720  by (simp add: cmod_def power2_eq_square)
   3.721  
   3.722  lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
   3.723 -apply (simp add: complex_of_real_def power2_eq_square complex_mod)
   3.724 -done
   3.725 +by (simp add: complex_of_real_def power2_eq_square complex_mod)
   3.726  declare complex_mod_complex_of_real [simp]
   3.727  
   3.728  lemma complex_of_real_abs:
   3.729       "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
   3.730 -by (simp)
   3.731 +by simp
   3.732  
   3.733  
   3.734  
   3.735  subsection{*Conjugation is an Automorphism*}
   3.736  
   3.737 -lemma complex_cnj: "cnj (Abs_complex(x,y)) = Abs_complex(x,-y)"
   3.738 -apply (unfold cnj_def)
   3.739 -apply (simp (no_asm))
   3.740 -done
   3.741 -
   3.742 -lemma inj_cnj: "inj cnj"
   3.743 -apply (rule inj_onI)
   3.744 -apply (auto simp add: cnj_def Abs_complex_cancel_iff complex_Re_Im_cancel_iff)
   3.745 -done
   3.746 +lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
   3.747 +by (simp add: cnj_def)
   3.748  
   3.749  lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)"
   3.750 -by (auto dest: inj_cnj [THEN injD])
   3.751 +by (simp add: cnj_def complex_Re_Im_cancel_iff)
   3.752  declare complex_cnj_cancel_iff [simp]
   3.753  
   3.754  lemma complex_cnj_cnj: "cnj (cnj z) = z"
   3.755 -apply (unfold cnj_def)
   3.756 -apply (simp (no_asm))
   3.757 -done
   3.758 +by (simp add: cnj_def)
   3.759  declare complex_cnj_cnj [simp]
   3.760  
   3.761  lemma complex_cnj_complex_of_real:
   3.762 - "cnj (complex_of_real x) = complex_of_real x"
   3.763 -apply (unfold complex_of_real_def)
   3.764 -apply (simp (no_asm) add: complex_cnj)
   3.765 -done
   3.766 +     "cnj (complex_of_real x) = complex_of_real x"
   3.767 +by (simp add: complex_of_real_def complex_cnj)
   3.768  declare complex_cnj_complex_of_real [simp]
   3.769  
   3.770  lemma complex_mod_cnj: "cmod (cnj z) = cmod z"
   3.771 -apply (rule_tac z = z in eq_Abs_complex)
   3.772 -apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square)
   3.773 -done
   3.774 +by (induct z, simp add: complex_cnj complex_mod power2_eq_square)
   3.775  declare complex_mod_cnj [simp]
   3.776  
   3.777  lemma complex_cnj_minus: "cnj (-z) = - cnj z"
   3.778 -apply (unfold cnj_def)
   3.779 -apply (simp (no_asm) add: complex_minus complex_Re_minus complex_Im_minus)
   3.780 -done
   3.781 +by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus)
   3.782  
   3.783  lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
   3.784 -apply (rule_tac z = z in eq_Abs_complex)
   3.785 -apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square)
   3.786 -done
   3.787 +by (induct z, simp add: complex_cnj complex_inverse power2_eq_square)
   3.788  
   3.789  lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
   3.790 -apply (rule_tac z = w in eq_Abs_complex)
   3.791 -apply (rule_tac z = z in eq_Abs_complex)
   3.792 -apply (simp (no_asm_simp) add: complex_cnj complex_add)
   3.793 -done
   3.794 +by (induct w, induct z, simp add: complex_cnj complex_add)
   3.795  
   3.796  lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
   3.797 -apply (unfold complex_diff_def)
   3.798 -apply (simp (no_asm) add: complex_cnj_add complex_cnj_minus)
   3.799 -done
   3.800 +by (simp add: complex_diff_def complex_cnj_add complex_cnj_minus)
   3.801  
   3.802  lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
   3.803 -apply (rule_tac z = w in eq_Abs_complex)
   3.804 -apply (rule_tac z = z in eq_Abs_complex)
   3.805 -apply (simp (no_asm_simp) add: complex_cnj complex_mult)
   3.806 -done
   3.807 +by (induct w, induct z, simp add: complex_cnj complex_mult)
   3.808  
   3.809  lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"
   3.810 -apply (unfold complex_divide_def)
   3.811 -apply (simp (no_asm) add: complex_cnj_mult complex_cnj_inverse)
   3.812 -done
   3.813 +by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse)
   3.814  
   3.815  lemma complex_cnj_one: "cnj 1 = 1"
   3.816 -apply (unfold cnj_def complex_one_def)
   3.817 -apply (simp (no_asm))
   3.818 -done
   3.819 +by (simp add: cnj_def complex_one_def)
   3.820  declare complex_cnj_one [simp]
   3.821  
   3.822  lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
   3.823 -apply (rule_tac z = z in eq_Abs_complex)
   3.824 -apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def)
   3.825 -done
   3.826 +by (induct z, simp add: complex_add complex_cnj complex_of_real_def)
   3.827  
   3.828  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
   3.829 -apply (rule_tac z = z in eq_Abs_complex)
   3.830 +apply (induct z)
   3.831  apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def 
   3.832                   complex_minus i_def complex_mult)
   3.833  done
   3.834 @@ -750,81 +417,62 @@
   3.835  by (simp add: cnj_def complex_zero_def)
   3.836  
   3.837  lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"
   3.838 -apply (rule_tac z = z in eq_Abs_complex)
   3.839 -apply (auto simp add: complex_zero_def complex_cnj)
   3.840 -done
   3.841 +by (induct z, simp add: complex_zero_def complex_cnj)
   3.842  declare complex_cnj_zero_iff [iff]
   3.843  
   3.844  lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
   3.845 -apply (rule_tac z = z in eq_Abs_complex)
   3.846 -apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
   3.847 -done
   3.848 +by (induct z, simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
   3.849  
   3.850  
   3.851  subsection{*Algebra*}
   3.852  
   3.853  lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"
   3.854 -apply (unfold complex_zero_def)
   3.855 -apply (rule_tac z = x in eq_Abs_complex)
   3.856 -apply (rule_tac z = y in eq_Abs_complex)
   3.857 -apply (auto simp add: complex_add)
   3.858 -done
   3.859 +by (induct x, induct y, simp add: complex_zero_def complex_add)
   3.860  declare complex_add_left_cancel_zero [simp]
   3.861  
   3.862 -lemma complex_diff_mult_distrib:
   3.863 -      "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)"
   3.864 -apply (unfold complex_diff_def)
   3.865 -apply (simp (no_asm) add: complex_add_mult_distrib)
   3.866 -done
   3.867 +lemma complex_diff_mult_distrib: "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)"
   3.868 +by (simp add: complex_diff_def left_distrib)
   3.869  
   3.870 -lemma complex_diff_mult_distrib2:
   3.871 -      "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)"
   3.872 -apply (unfold complex_diff_def)
   3.873 -apply (simp (no_asm) add: complex_add_mult_distrib2)
   3.874 -done
   3.875 +lemma complex_diff_mult_distrib2: "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)"
   3.876 +by (simp add: complex_diff_def right_distrib)
   3.877  
   3.878  
   3.879  subsection{*Modulus*}
   3.880  
   3.881  lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
   3.882 -apply (rule_tac z = x in eq_Abs_complex)
   3.883 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square)
   3.884 +apply (induct x)
   3.885 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
   3.886 +            simp add: complex_mod complex_zero_def power2_eq_square)
   3.887  done
   3.888  declare complex_mod_eq_zero_cancel [simp]
   3.889  
   3.890 -lemma complex_mod_complex_of_real_of_nat: "cmod (complex_of_real(real (n::nat))) = real n"
   3.891 -apply (simp (no_asm))
   3.892 -done
   3.893 +lemma complex_mod_complex_of_real_of_nat:
   3.894 +     "cmod (complex_of_real(real (n::nat))) = real n"
   3.895 +by simp
   3.896  declare complex_mod_complex_of_real_of_nat [simp]
   3.897  
   3.898  lemma complex_mod_minus: "cmod (-x) = cmod(x)"
   3.899 -apply (rule_tac z = x in eq_Abs_complex)
   3.900 -apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square)
   3.901 -done
   3.902 +by (induct x, simp add: complex_mod complex_minus power2_eq_square)
   3.903  declare complex_mod_minus [simp]
   3.904  
   3.905  lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
   3.906 -apply (rule_tac z = z in eq_Abs_complex)
   3.907 -apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult);
   3.908 -apply (simp (no_asm) add: power2_eq_square real_abs_def)
   3.909 +apply (induct z, simp add: complex_mod complex_cnj complex_mult)
   3.910 +apply (simp add: power2_eq_square real_abs_def)
   3.911  done
   3.912  
   3.913 -lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
   3.914 -by (unfold cmod_def, auto)
   3.915 +lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
   3.916 +by (simp add: cmod_def)
   3.917  
   3.918  lemma complex_mod_ge_zero: "0 \<le> cmod x"
   3.919 -apply (unfold cmod_def)
   3.920 -apply (auto intro: real_sqrt_ge_zero)
   3.921 -done
   3.922 +by (simp add: cmod_def)
   3.923  declare complex_mod_ge_zero [simp]
   3.924  
   3.925  lemma abs_cmod_cancel: "abs(cmod x) = cmod x"
   3.926 -by (auto intro: abs_eqI1)
   3.927 +by (simp add: abs_if linorder_not_less) 
   3.928  declare abs_cmod_cancel [simp]
   3.929  
   3.930  lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
   3.931 -apply (rule_tac z = x in eq_Abs_complex)
   3.932 -apply (rule_tac z = y in eq_Abs_complex)
   3.933 +apply (induct x, induct y)
   3.934  apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
   3.935  apply (rule_tac n = 1 in power_inject_base)
   3.936  apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
   3.937 @@ -832,38 +480,30 @@
   3.938  done
   3.939  
   3.940  lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
   3.941 -apply (rule_tac z = x in eq_Abs_complex)
   3.942 -apply (rule_tac z = y in eq_Abs_complex)
   3.943 +apply (induct x, induct y)
   3.944  apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   3.945  apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
   3.946  done
   3.947  
   3.948  lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"
   3.949 -apply (rule_tac z = x in eq_Abs_complex)
   3.950 -apply (rule_tac z = y in eq_Abs_complex)
   3.951 +apply (induct x, induct y)
   3.952  apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   3.953  done
   3.954  declare complex_Re_mult_cnj_le_cmod [simp]
   3.955  
   3.956  lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"
   3.957 -apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod)
   3.958 -apply (simp add: complex_mod_mult)
   3.959 -done
   3.960 +by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult)
   3.961  declare complex_Re_mult_cnj_le_cmod2 [simp]
   3.962  
   3.963  lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
   3.964 -apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
   3.965 -done
   3.966 +by (simp add: left_distrib right_distrib power2_eq_square)
   3.967  
   3.968  lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
   3.969 -apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
   3.970 -done
   3.971 +by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
   3.972  declare complex_mod_triangle_squared [simp]
   3.973  
   3.974  lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
   3.975 -apply (rule order_trans [OF _ complex_mod_ge_zero]) 
   3.976 -apply (simp (no_asm))
   3.977 -done
   3.978 +by (rule order_trans [OF _ complex_mod_ge_zero], simp)
   3.979  declare complex_mod_minus_le_complex_mod [simp]
   3.980  
   3.981  lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"
   3.982 @@ -874,15 +514,11 @@
   3.983  declare complex_mod_triangle_ineq [simp]
   3.984  
   3.985  lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
   3.986 -apply (cut_tac x1 = b and y1 = a and c = "-cmod b" 
   3.987 -       in complex_mod_triangle_ineq [THEN add_right_mono])
   3.988 -apply (simp (no_asm))
   3.989 -done
   3.990 +by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp)
   3.991  declare complex_mod_triangle_ineq2 [simp]
   3.992  
   3.993  lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
   3.994 -apply (rule_tac z = x in eq_Abs_complex)
   3.995 -apply (rule_tac z = y in eq_Abs_complex)
   3.996 +apply (induct x, induct y)
   3.997  apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
   3.998  done
   3.999  
  3.1000 @@ -901,18 +537,16 @@
  3.1001  apply (rule complex_mod_minus [THEN subst])
  3.1002  apply (rule order_trans)
  3.1003  apply (rule_tac [2] complex_mod_triangle_ineq)
  3.1004 -apply (auto simp add: complex_add_ac)
  3.1005 +apply (auto simp add: add_ac)
  3.1006  done
  3.1007  declare complex_mod_diff_ineq [simp]
  3.1008  
  3.1009  lemma complex_Re_le_cmod: "Re z \<le> cmod z"
  3.1010 -apply (rule_tac z = z in eq_Abs_complex)
  3.1011 -apply (auto simp add: complex_mod simp del: realpow_Suc)
  3.1012 -done
  3.1013 +by (induct z, simp add: complex_mod del: realpow_Suc)
  3.1014  declare complex_Re_le_cmod [simp]
  3.1015  
  3.1016  lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
  3.1017 -apply (cut_tac x = z in complex_mod_ge_zero)
  3.1018 +apply (insert complex_mod_ge_zero [of z])
  3.1019  apply (drule order_le_imp_less_or_eq, auto)
  3.1020  done
  3.1021  
  3.1022 @@ -920,22 +554,16 @@
  3.1023  subsection{*A Few More Theorems*}
  3.1024  
  3.1025  lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"
  3.1026 -apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO)
  3.1027 +apply (case_tac "x=0", simp)
  3.1028  apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])
  3.1029  apply (auto simp add: complex_mod_mult [symmetric])
  3.1030  done
  3.1031  
  3.1032 -lemma complex_mod_divide:
  3.1033 -      "cmod(x/y) = cmod(x)/(cmod y)"
  3.1034 -apply (unfold complex_divide_def real_divide_def)
  3.1035 -apply (auto simp add: complex_mod_mult complex_mod_inverse)
  3.1036 -done
  3.1037 +lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
  3.1038 +by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse)
  3.1039  
  3.1040 -lemma complex_inverse_divide:
  3.1041 -      "inverse(x/y) = y/(x::complex)"
  3.1042 -apply (unfold complex_divide_def)
  3.1043 -apply (auto simp add: inverse_mult_distrib complex_mult_commute)
  3.1044 -done
  3.1045 +lemma complex_inverse_divide: "inverse(x/y) = y/(x::complex)"
  3.1046 +by (simp add: complex_divide_def inverse_mult_distrib mult_commute)
  3.1047  declare complex_inverse_divide [simp]
  3.1048  
  3.1049  
  3.1050 @@ -977,34 +605,29 @@
  3.1051  by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
  3.1052  
  3.1053  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
  3.1054 -by (unfold i_def complex_zero_def, auto)
  3.1055 +by (simp add: i_def complex_zero_def)
  3.1056  
  3.1057  
  3.1058  subsection{*The Function @{term sgn}*}
  3.1059  
  3.1060  lemma sgn_zero: "sgn 0 = 0"
  3.1061 -apply (unfold sgn_def)
  3.1062 -apply (simp (no_asm))
  3.1063 -done
  3.1064 +by (simp add: sgn_def)
  3.1065  declare sgn_zero [simp]
  3.1066  
  3.1067  lemma sgn_one: "sgn 1 = 1"
  3.1068 -apply (unfold sgn_def)
  3.1069 -apply (simp (no_asm))
  3.1070 -done
  3.1071 +by (simp add: sgn_def)
  3.1072  declare sgn_one [simp]
  3.1073  
  3.1074  lemma sgn_minus: "sgn (-z) = - sgn(z)"
  3.1075 -by (unfold sgn_def, auto)
  3.1076 +by (simp add: sgn_def)
  3.1077  
  3.1078  lemma sgn_eq:
  3.1079      "sgn z = z / complex_of_real (cmod z)"
  3.1080 -apply (unfold sgn_def)
  3.1081 -apply (simp (no_asm))
  3.1082 +apply (simp add: sgn_def)
  3.1083  done
  3.1084  
  3.1085  lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
  3.1086 -apply (rule_tac z = z in eq_Abs_complex)
  3.1087 +apply (induct z)
  3.1088  apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
  3.1089  done
  3.1090  
  3.1091 @@ -1017,59 +640,46 @@
  3.1092  declare Im_complex_i [simp]
  3.1093  
  3.1094  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
  3.1095 -apply (unfold i_def complex_of_real_def)
  3.1096 -apply (auto simp add: complex_mult complex_add)
  3.1097 -done
  3.1098 +by (simp add: i_def complex_of_real_def complex_mult complex_add)
  3.1099  
  3.1100  lemma i_mult_eq2: "ii * ii = -(1::complex)"
  3.1101 -apply (unfold i_def complex_one_def)
  3.1102 -apply (simp (no_asm) add: complex_mult complex_minus)
  3.1103 -done
  3.1104 +by (simp add: i_def complex_one_def complex_mult complex_minus)
  3.1105  declare i_mult_eq2 [simp]
  3.1106  
  3.1107  lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
  3.1108        sqrt (x ^ 2 + y ^ 2)"
  3.1109 -apply (auto simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
  3.1110 -done
  3.1111 +by (simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
  3.1112  
  3.1113  lemma complex_eq_Re_eq:
  3.1114       "complex_of_real xa + ii * complex_of_real ya =
  3.1115        complex_of_real xb + ii * complex_of_real yb
  3.1116         ==> xa = xb"
  3.1117 -apply (unfold complex_of_real_def i_def)
  3.1118 -apply (auto simp add: complex_mult complex_add)
  3.1119 -done
  3.1120 +by (simp add: complex_of_real_def i_def complex_mult complex_add)
  3.1121  
  3.1122  lemma complex_eq_Im_eq:
  3.1123       "complex_of_real xa + ii * complex_of_real ya =
  3.1124        complex_of_real xb + ii * complex_of_real yb
  3.1125         ==> ya = yb"
  3.1126 -apply (unfold complex_of_real_def i_def)
  3.1127 -apply (auto simp add: complex_mult complex_add)
  3.1128 -done
  3.1129 +by (simp add: complex_of_real_def i_def complex_mult complex_add)
  3.1130  
  3.1131  lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya =
  3.1132         complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
  3.1133 -apply (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
  3.1134 -done
  3.1135 +by (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
  3.1136  declare complex_eq_cancel_iff [iff]
  3.1137  
  3.1138  lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii =
  3.1139 -       complex_of_real xb + complex_of_real yb * ii ) = ((xa = xb) & (ya = yb))"
  3.1140 -apply (auto simp add: complex_mult_commute)
  3.1141 -done
  3.1142 +       complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
  3.1143 +by (simp add: mult_commute)
  3.1144  declare complex_eq_cancel_iffA [iff]
  3.1145  
  3.1146  lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii =
  3.1147         complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
  3.1148 -apply (auto simp add: complex_mult_commute)
  3.1149 -done
  3.1150 +by (auto simp add: mult_commute)
  3.1151  declare complex_eq_cancel_iffB [iff]
  3.1152  
  3.1153  lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya  =
  3.1154         complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
  3.1155 -apply (auto simp add: complex_mult_commute)
  3.1156 -done
  3.1157 +by (auto simp add: mult_commute)
  3.1158  declare complex_eq_cancel_iffC [iff]
  3.1159  
  3.1160  lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y =
  3.1161 @@ -1081,8 +691,7 @@
  3.1162  
  3.1163  lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii =
  3.1164        complex_of_real xa) = (x = xa & y = 0)"
  3.1165 -apply (auto simp add: complex_mult_commute)
  3.1166 -done
  3.1167 +by (auto simp add: mult_commute)
  3.1168  declare complex_eq_cancel_iff2a [simp]
  3.1169  
  3.1170  lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y =
  3.1171 @@ -1094,39 +703,31 @@
  3.1172  
  3.1173  lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii =
  3.1174        ii * complex_of_real ya) = (x = 0 & y = ya)"
  3.1175 -apply (auto simp add: complex_mult_commute)
  3.1176 -done
  3.1177 +by (auto simp add: mult_commute)
  3.1178  declare complex_eq_cancel_iff3a [simp]
  3.1179  
  3.1180  lemma complex_split_Re_zero:
  3.1181       "complex_of_real x + ii * complex_of_real y = 0
  3.1182        ==> x = 0"
  3.1183 -apply (unfold complex_of_real_def i_def complex_zero_def)
  3.1184 -apply (auto simp add: complex_mult complex_add)
  3.1185 -done
  3.1186 +by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
  3.1187  
  3.1188  lemma complex_split_Im_zero:
  3.1189       "complex_of_real x + ii * complex_of_real y = 0
  3.1190        ==> y = 0"
  3.1191 -apply (unfold complex_of_real_def i_def complex_zero_def)
  3.1192 -apply (auto simp add: complex_mult complex_add)
  3.1193 -done
  3.1194 +by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
  3.1195  
  3.1196 -lemma Re_sgn:
  3.1197 -      "Re(sgn z) = Re(z)/cmod z"
  3.1198 -apply (unfold sgn_def complex_divide_def)
  3.1199 -apply (rule_tac z = z in eq_Abs_complex)
  3.1200 -apply (auto simp add: complex_of_real_inverse [symmetric])
  3.1201 -apply (auto simp add: complex_of_real_def complex_mult real_divide_def)
  3.1202 +lemma Re_sgn: "Re(sgn z) = Re(z)/cmod z"
  3.1203 +apply (induct z)
  3.1204 +apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
  3.1205 +apply (simp add: complex_of_real_def complex_mult real_divide_def)
  3.1206  done
  3.1207  declare Re_sgn [simp]
  3.1208  
  3.1209  lemma Im_sgn:
  3.1210        "Im(sgn z) = Im(z)/cmod z"
  3.1211 -apply (unfold sgn_def complex_divide_def)
  3.1212 -apply (rule_tac z = z in eq_Abs_complex)
  3.1213 -apply (auto simp add: complex_of_real_inverse [symmetric])
  3.1214 -apply (auto simp add: complex_of_real_def complex_mult real_divide_def)
  3.1215 +apply (induct z)
  3.1216 +apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
  3.1217 +apply (simp add: complex_of_real_def complex_mult real_divide_def)
  3.1218  done
  3.1219  declare Im_sgn [simp]
  3.1220  
  3.1221 @@ -1134,9 +735,8 @@
  3.1222       "inverse(complex_of_real x + ii * complex_of_real y) =
  3.1223        complex_of_real(x/(x ^ 2 + y ^ 2)) -
  3.1224        ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
  3.1225 -apply (unfold complex_of_real_def i_def)
  3.1226 -apply (auto simp add: complex_mult complex_add complex_diff_def complex_minus complex_inverse real_divide_def)
  3.1227 -done
  3.1228 +by (simp add: complex_of_real_def i_def complex_mult complex_add 
  3.1229 +         complex_diff_def complex_minus complex_inverse real_divide_def)
  3.1230  
  3.1231  (*----------------------------------------------------------------------------*)
  3.1232  (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
  3.1233 @@ -1146,47 +746,37 @@
  3.1234  lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
  3.1235  by (auto simp add: complex_zero_def complex_of_real_def)
  3.1236  
  3.1237 -lemma Re_mult_i_eq:
  3.1238 -    "Re (ii * complex_of_real y) = 0"
  3.1239 -apply (unfold i_def complex_of_real_def)
  3.1240 -apply (auto simp add: complex_mult)
  3.1241 -done
  3.1242 +lemma Re_mult_i_eq: "Re (ii * complex_of_real y) = 0"
  3.1243 +by (simp add: i_def complex_of_real_def complex_mult)
  3.1244  declare Re_mult_i_eq [simp]
  3.1245  
  3.1246 -lemma Im_mult_i_eq:
  3.1247 -    "Im (ii * complex_of_real y) = y"
  3.1248 -apply (unfold i_def complex_of_real_def)
  3.1249 -apply (auto simp add: complex_mult)
  3.1250 -done
  3.1251 +lemma Im_mult_i_eq: "Im (ii * complex_of_real y) = y"
  3.1252 +by (simp add: i_def complex_of_real_def complex_mult)
  3.1253  declare Im_mult_i_eq [simp]
  3.1254  
  3.1255 -lemma complex_mod_mult_i:
  3.1256 -    "cmod (ii * complex_of_real y) = abs y"
  3.1257 -apply (unfold i_def complex_of_real_def)
  3.1258 -apply (auto simp add: complex_mult complex_mod power2_eq_square)
  3.1259 -done
  3.1260 +lemma complex_mod_mult_i: "cmod (ii * complex_of_real y) = abs y"
  3.1261 +by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square)
  3.1262  declare complex_mod_mult_i [simp]
  3.1263  
  3.1264  lemma cos_arg_i_mult_zero_pos:
  3.1265     "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
  3.1266 -apply (unfold arg_def)
  3.1267 -apply (auto simp add: abs_eqI2)
  3.1268 +apply (simp add: arg_def abs_if)
  3.1269  apply (rule_tac a = "pi/2" in someI2, auto)
  3.1270  apply (rule order_less_trans [of _ 0], auto)
  3.1271  done
  3.1272  
  3.1273  lemma cos_arg_i_mult_zero_neg:
  3.1274     "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
  3.1275 -apply (unfold arg_def)
  3.1276 -apply (auto simp add: abs_minus_eqI2)
  3.1277 +apply (simp add: arg_def abs_if)
  3.1278  apply (rule_tac a = "- pi/2" in someI2, auto)
  3.1279  apply (rule order_trans [of _ 0], auto)
  3.1280  done
  3.1281  
  3.1282  lemma cos_arg_i_mult_zero [simp]
  3.1283      : "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
  3.1284 -by (cut_tac x = y and y = 0 in linorder_less_linear, 
  3.1285 -    auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
  3.1286 +apply (insert linorder_less_linear [of y 0]) 
  3.1287 +apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
  3.1288 +done
  3.1289  
  3.1290  
  3.1291  subsection{*Finally! Polar Form for Complex Numbers*}
  3.1292 @@ -1198,97 +788,75 @@
  3.1293  done
  3.1294  
  3.1295  lemma rcis_Ex: "\<exists>r a. z = rcis r a"
  3.1296 -apply (unfold rcis_def cis_def)
  3.1297 +apply (simp add: rcis_def cis_def)
  3.1298  apply (rule complex_split_polar)
  3.1299  done
  3.1300  
  3.1301  lemma Re_complex_polar: "Re(complex_of_real r *
  3.1302        (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
  3.1303 -apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
  3.1304 -done
  3.1305 +by (auto simp add: right_distrib complex_of_real_mult mult_ac)
  3.1306  declare Re_complex_polar [simp]
  3.1307  
  3.1308  lemma Re_rcis: "Re(rcis r a) = r * cos a"
  3.1309 -by (unfold rcis_def cis_def, auto)
  3.1310 +by (simp add: rcis_def cis_def)
  3.1311  declare Re_rcis [simp]
  3.1312  
  3.1313  lemma Im_complex_polar [simp]:
  3.1314       "Im(complex_of_real r * 
  3.1315           (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
  3.1316        r * sin a"
  3.1317 -by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac)
  3.1318 +by (auto simp add: right_distrib complex_of_real_mult mult_ac)
  3.1319  
  3.1320  lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
  3.1321 -by (unfold rcis_def cis_def, auto)
  3.1322 +by (simp add: rcis_def cis_def)
  3.1323  
  3.1324  lemma complex_mod_complex_polar [simp]:
  3.1325       "cmod (complex_of_real r * 
  3.1326              (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
  3.1327        abs r"
  3.1328 -by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult
  3.1329 +by (auto simp add: right_distrib cmod_i complex_of_real_mult
  3.1330                        right_distrib [symmetric] power_mult_distrib mult_ac 
  3.1331           simp del: realpow_Suc)
  3.1332  
  3.1333  lemma complex_mod_rcis: "cmod(rcis r a) = abs r"
  3.1334 -by (unfold rcis_def cis_def, auto)
  3.1335 +by (simp add: rcis_def cis_def)
  3.1336  declare complex_mod_rcis [simp]
  3.1337  
  3.1338  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
  3.1339 -apply (unfold cmod_def)
  3.1340 +apply (simp add: cmod_def)
  3.1341  apply (rule real_sqrt_eq_iff [THEN iffD2])
  3.1342  apply (auto simp add: complex_mult_cnj)
  3.1343  done
  3.1344  
  3.1345  lemma complex_Re_cnj: "Re(cnj z) = Re z"
  3.1346 -apply (rule_tac z = z in eq_Abs_complex)
  3.1347 -apply (auto simp add: complex_cnj)
  3.1348 -done
  3.1349 +by (induct z, simp add: complex_cnj)
  3.1350  declare complex_Re_cnj [simp]
  3.1351  
  3.1352  lemma complex_Im_cnj: "Im(cnj z) = - Im z"
  3.1353 -apply (rule_tac z = z in eq_Abs_complex)
  3.1354 -apply (auto simp add: complex_cnj)
  3.1355 -done
  3.1356 +by (induct z, simp add: complex_cnj)
  3.1357  declare complex_Im_cnj [simp]
  3.1358  
  3.1359  lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0"
  3.1360 -apply (rule_tac z = z in eq_Abs_complex)
  3.1361 -apply (auto simp add: complex_cnj complex_mult)
  3.1362 -done
  3.1363 +by (induct z, simp add: complex_cnj complex_mult)
  3.1364  declare complex_In_mult_cnj_zero [simp]
  3.1365  
  3.1366  lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
  3.1367 -apply (rule_tac z = z in eq_Abs_complex)
  3.1368 -apply (rule_tac z = w in eq_Abs_complex)
  3.1369 -apply (auto simp add: complex_mult)
  3.1370 -done
  3.1371 +by (induct z, induct w, simp add: complex_mult)
  3.1372  
  3.1373  lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c"
  3.1374 -apply (unfold complex_of_real_def)
  3.1375 -apply (rule_tac z = z in eq_Abs_complex)
  3.1376 -apply (auto simp add: complex_mult)
  3.1377 -done
  3.1378 +by (induct z, simp add: complex_of_real_def complex_mult)
  3.1379  declare complex_Re_mult_complex_of_real [simp]
  3.1380  
  3.1381  lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c"
  3.1382 -apply (unfold complex_of_real_def)
  3.1383 -apply (rule_tac z = z in eq_Abs_complex)
  3.1384 -apply (auto simp add: complex_mult)
  3.1385 -done
  3.1386 +by (induct z, simp add: complex_of_real_def complex_mult)
  3.1387  declare complex_Im_mult_complex_of_real [simp]
  3.1388  
  3.1389  lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)"
  3.1390 -apply (unfold complex_of_real_def)
  3.1391 -apply (rule_tac z = z in eq_Abs_complex)
  3.1392 -apply (auto simp add: complex_mult)
  3.1393 -done
  3.1394 +by (induct z, simp add: complex_of_real_def complex_mult)
  3.1395  declare complex_Re_mult_complex_of_real2 [simp]
  3.1396  
  3.1397  lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)"
  3.1398 -apply (unfold complex_of_real_def)
  3.1399 -apply (rule_tac z = z in eq_Abs_complex)
  3.1400 -apply (auto simp add: complex_mult)
  3.1401 -done
  3.1402 +by (induct z, simp add: complex_of_real_def complex_mult)
  3.1403  declare complex_Im_mult_complex_of_real2 [simp]
  3.1404  
  3.1405  (*---------------------------------------------------------------------------*)
  3.1406 @@ -1296,64 +864,51 @@
  3.1407  (*---------------------------------------------------------------------------*)
  3.1408  
  3.1409  lemma cis_rcis_eq: "cis a = rcis 1 a"
  3.1410 -apply (unfold rcis_def)
  3.1411 -apply (simp (no_asm))
  3.1412 -done
  3.1413 +by (simp add: rcis_def)
  3.1414  
  3.1415  lemma rcis_mult:
  3.1416    "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
  3.1417 -apply (unfold rcis_def cis_def)
  3.1418 -apply (auto simp add: cos_add sin_add complex_add_mult_distrib2 complex_add_mult_distrib complex_mult_ac complex_add_ac)
  3.1419 -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)
  3.1420 -apply (auto simp add: complex_add_ac)
  3.1421 +apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib 
  3.1422 +                 mult_ac add_ac)
  3.1423 +apply (auto simp add: right_distrib [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)
  3.1424 +apply (auto simp add: add_ac)
  3.1425  apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac)
  3.1426  done
  3.1427  
  3.1428  lemma cis_mult: "cis a * cis b = cis (a + b)"
  3.1429 -apply (simp (no_asm) add: cis_rcis_eq rcis_mult)
  3.1430 -done
  3.1431 +by (simp add: cis_rcis_eq rcis_mult)
  3.1432  
  3.1433  lemma cis_zero: "cis 0 = 1"
  3.1434 -by (unfold cis_def, auto)
  3.1435 +by (simp add: cis_def)
  3.1436  declare cis_zero [simp]
  3.1437  
  3.1438  lemma cis_zero2: "cis 0 = complex_of_real 1"
  3.1439 -by (unfold cis_def, auto)
  3.1440 +by (simp add: cis_def)
  3.1441  declare cis_zero2 [simp]
  3.1442  
  3.1443  lemma rcis_zero_mod: "rcis 0 a = 0"
  3.1444 -apply (unfold rcis_def)
  3.1445 -apply (simp (no_asm))
  3.1446 -done
  3.1447 +by (simp add: rcis_def)
  3.1448  declare rcis_zero_mod [simp]
  3.1449  
  3.1450  lemma rcis_zero_arg: "rcis r 0 = complex_of_real r"
  3.1451 -apply (unfold rcis_def)
  3.1452 -apply (simp (no_asm))
  3.1453 -done
  3.1454 +by (simp add: rcis_def)
  3.1455  declare rcis_zero_arg [simp]
  3.1456  
  3.1457  lemma complex_of_real_minus_one:
  3.1458     "complex_of_real (-(1::real)) = -(1::complex)"
  3.1459 -apply (unfold complex_of_real_def complex_one_def)
  3.1460 -apply (simp (no_asm) add: complex_minus)
  3.1461 +apply (simp add: complex_of_real_def complex_one_def complex_minus)
  3.1462  done
  3.1463  
  3.1464  lemma complex_i_mult_minus: "ii * (ii * x) = - x"
  3.1465 -apply (simp (no_asm) add: complex_mult_assoc [symmetric])
  3.1466 -done
  3.1467 +by (simp add: complex_mult_assoc [symmetric])
  3.1468  declare complex_i_mult_minus [simp]
  3.1469  
  3.1470 -lemma complex_i_mult_minus2: "ii * ii * x = - x"
  3.1471 -apply (simp (no_asm))
  3.1472 -done
  3.1473 -declare complex_i_mult_minus2 [simp]
  3.1474  
  3.1475  lemma cis_real_of_nat_Suc_mult:
  3.1476     "cis (real (Suc n) * a) = cis a * cis (real n * a)"
  3.1477 -apply (unfold cis_def)
  3.1478 -apply (auto simp add: real_of_nat_Suc left_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)
  3.1479 -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)
  3.1480 +apply (simp add: cis_def)
  3.1481 +apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add left_distrib right_distrib complex_of_real_add complex_of_real_mult mult_ac add_ac)
  3.1482 +apply (auto simp add: right_distrib [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)
  3.1483  done
  3.1484  
  3.1485  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
  3.1486 @@ -1363,14 +918,11 @@
  3.1487  
  3.1488  lemma DeMoivre2:
  3.1489     "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
  3.1490 -apply (unfold rcis_def)
  3.1491 -apply (auto simp add: power_mult_distrib DeMoivre complex_of_real_pow)
  3.1492 +apply (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
  3.1493  done
  3.1494  
  3.1495  lemma cis_inverse: "inverse(cis a) = cis (-a)"
  3.1496 -apply (unfold cis_def)
  3.1497 -apply (auto simp add: complex_inverse_complex_split complex_of_real_minus complex_diff_def)
  3.1498 -done
  3.1499 +by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus complex_diff_def)
  3.1500  declare cis_inverse [simp]
  3.1501  
  3.1502  lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
  3.1503 @@ -1381,23 +933,20 @@
  3.1504  done
  3.1505  
  3.1506  lemma cis_divide: "cis a / cis b = cis (a - b)"
  3.1507 -apply (unfold complex_divide_def)
  3.1508 -apply (auto simp add: cis_mult real_diff_def)
  3.1509 -done
  3.1510 +by (simp add: complex_divide_def cis_mult real_diff_def)
  3.1511  
  3.1512  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
  3.1513 -apply (unfold complex_divide_def)
  3.1514 -apply (case_tac "r2=0")
  3.1515 -apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
  3.1516 -apply (auto simp add: rcis_inverse rcis_mult real_diff_def)
  3.1517 +apply (simp add: complex_divide_def)
  3.1518 +apply (case_tac "r2=0", simp)
  3.1519 +apply (simp add: rcis_inverse rcis_mult real_diff_def)
  3.1520  done
  3.1521  
  3.1522  lemma Re_cis: "Re(cis a) = cos a"
  3.1523 -by (unfold cis_def, auto)
  3.1524 +by (simp add: cis_def)
  3.1525  declare Re_cis [simp]
  3.1526  
  3.1527  lemma Im_cis: "Im(cis a) = sin a"
  3.1528 -by (unfold cis_def, auto)
  3.1529 +by (simp add: cis_def)
  3.1530  declare Im_cis [simp]
  3.1531  
  3.1532  lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
  3.1533 @@ -1409,65 +958,40 @@
  3.1534  lemma expi_Im_split:
  3.1535      "expi (ii * complex_of_real y) =
  3.1536       complex_of_real (cos y) + ii * complex_of_real (sin y)"
  3.1537 -by (unfold expi_def cis_def, auto)
  3.1538 +by (simp add: expi_def cis_def)
  3.1539  
  3.1540  lemma expi_Im_cis:
  3.1541      "expi (ii * complex_of_real y) = cis y"
  3.1542 -by (unfold expi_def, auto)
  3.1543 +by (simp add: expi_def)
  3.1544  
  3.1545  lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
  3.1546 -apply (unfold expi_def)
  3.1547 -apply (auto simp add: complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult complex_mult_ac)
  3.1548 -done
  3.1549 +by (simp add: expi_def complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult mult_ac)
  3.1550  
  3.1551  lemma expi_complex_split:
  3.1552       "expi(complex_of_real x + ii * complex_of_real y) =
  3.1553        complex_of_real (exp(x)) * cis y"
  3.1554 -by (unfold expi_def, auto)
  3.1555 +by (simp add: expi_def)
  3.1556  
  3.1557  lemma expi_zero: "expi (0::complex) = 1"
  3.1558 -by (unfold expi_def, auto)
  3.1559 +by (simp add: expi_def)
  3.1560  declare expi_zero [simp]
  3.1561  
  3.1562  lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
  3.1563 -apply (rule_tac z = z in eq_Abs_complex)
  3.1564 -apply (rule_tac z = w in eq_Abs_complex)
  3.1565 -apply (auto simp add: complex_mult)
  3.1566 -done
  3.1567 +by (induct z, induct w, simp add: complex_mult)
  3.1568  
  3.1569  lemma complex_Im_mult_eq:
  3.1570       "Im (w * z) = Re w * Im z + Im w * Re z"
  3.1571 -apply (rule_tac z = z in eq_Abs_complex)
  3.1572 -apply (rule_tac z = w in eq_Abs_complex)
  3.1573 -apply (auto simp add: complex_mult)
  3.1574 +apply (induct z, induct w, simp add: complex_mult)
  3.1575  done
  3.1576  
  3.1577  lemma complex_expi_Ex: 
  3.1578     "\<exists>a r. z = complex_of_real r * expi a"
  3.1579 -apply (cut_tac z = z in rcis_Ex)
  3.1580 +apply (insert rcis_Ex [of z])
  3.1581  apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
  3.1582  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
  3.1583  done
  3.1584  
  3.1585  
  3.1586 -(****
  3.1587 -Goal "[| - pi < a; a \<le> pi |] ==> (-pi < a & a \<le> 0) | (0 \<le> a & a \<le> pi)"
  3.1588 -by Auto_tac
  3.1589 -qed "lemma_split_interval";
  3.1590 -
  3.1591 -Goalw [arg_def]
  3.1592 -  "[| r \<noteq> 0; - pi < a; a \<le> pi |] \
  3.1593 -\  ==> arg(complex_of_real r * \
  3.1594 -\      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
  3.1595 -by Auto_tac
  3.1596 -by (cut_inst_tac [("x","0"),("y","r")] linorder_less_linear 1);
  3.1597 -by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy)
  3.1598 -    [rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) [real_divide_def,
  3.1599 -    minus_mult_right RS sym] mult_ac));
  3.1600 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
  3.1601 -by (dtac lemma_split_interval 1 THEN safe)
  3.1602 -****)
  3.1603 -
  3.1604  
  3.1605  ML
  3.1606  {*
  3.1607 @@ -1490,15 +1014,8 @@
  3.1608  val complexpow_0 = thm"complexpow_0";
  3.1609  val complexpow_Suc = thm"complexpow_Suc";
  3.1610  
  3.1611 -val inj_Rep_complex = thm"inj_Rep_complex";
  3.1612 -val inj_Abs_complex = thm"inj_Abs_complex";
  3.1613 -val Abs_complex_cancel_iff = thm"Abs_complex_cancel_iff";
  3.1614 -val pair_mem_complex = thm"pair_mem_complex";
  3.1615 -val Abs_complex_inverse2 = thm"Abs_complex_inverse2";
  3.1616 -val eq_Abs_complex = thm"eq_Abs_complex";
  3.1617  val Re = thm"Re";
  3.1618  val Im = thm"Im";
  3.1619 -val Abs_complex_cancel = thm"Abs_complex_cancel";
  3.1620  val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff";
  3.1621  val complex_Re_zero = thm"complex_Re_zero";
  3.1622  val complex_Im_zero = thm"complex_Im_zero";
  3.1623 @@ -1515,55 +1032,20 @@
  3.1624  val complex_minus = thm"complex_minus";
  3.1625  val complex_Re_minus = thm"complex_Re_minus";
  3.1626  val complex_Im_minus = thm"complex_Im_minus";
  3.1627 -val complex_minus_minus = thm"complex_minus_minus";
  3.1628 -val inj_complex_minus = thm"inj_complex_minus";
  3.1629  val complex_minus_zero = thm"complex_minus_zero";
  3.1630  val complex_minus_zero_iff = thm"complex_minus_zero_iff";
  3.1631 -val complex_minus_zero_iff2 = thm"complex_minus_zero_iff2";
  3.1632 -val complex_minus_not_zero_iff = thm"complex_minus_not_zero_iff";
  3.1633  val complex_add = thm"complex_add";
  3.1634  val complex_Re_add = thm"complex_Re_add";
  3.1635  val complex_Im_add = thm"complex_Im_add";
  3.1636  val complex_add_commute = thm"complex_add_commute";
  3.1637  val complex_add_assoc = thm"complex_add_assoc";
  3.1638 -val complex_add_left_commute = thm"complex_add_left_commute";
  3.1639  val complex_add_zero_left = thm"complex_add_zero_left";
  3.1640  val complex_add_zero_right = thm"complex_add_zero_right";
  3.1641 -val complex_add_minus_right_zero = thm"complex_add_minus_right_zero";
  3.1642 -val complex_add_minus_cancel = thm"complex_add_minus_cancel";
  3.1643 -val complex_minus_add_cancel = thm"complex_minus_add_cancel";
  3.1644 -val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus";
  3.1645 -val complex_minus_add_distrib = thm"complex_minus_add_distrib";
  3.1646 -val complex_add_left_cancel = thm"complex_add_left_cancel";
  3.1647 -val complex_add_right_cancel = thm"complex_add_right_cancel";
  3.1648 -val complex_eq_minus_iff = thm"complex_eq_minus_iff";
  3.1649 -val complex_eq_minus_iff2 = thm"complex_eq_minus_iff2";
  3.1650 -val complex_diff_0 = thm"complex_diff_0";
  3.1651 -val complex_diff_0_right = thm"complex_diff_0_right";
  3.1652 -val complex_diff_self = thm"complex_diff_self";
  3.1653  val complex_diff = thm"complex_diff";
  3.1654 -val complex_diff_eq_eq = thm"complex_diff_eq_eq";
  3.1655  val complex_mult = thm"complex_mult";
  3.1656 -val complex_mult_commute = thm"complex_mult_commute";
  3.1657 -val complex_mult_assoc = thm"complex_mult_assoc";
  3.1658 -val complex_mult_left_commute = thm"complex_mult_left_commute";
  3.1659  val complex_mult_one_left = thm"complex_mult_one_left";
  3.1660  val complex_mult_one_right = thm"complex_mult_one_right";
  3.1661 -val complex_mult_zero_left = thm"complex_mult_zero_left";
  3.1662 -val complex_mult_zero_right = thm"complex_mult_zero_right";
  3.1663 -val complex_divide_zero = thm"complex_divide_zero";
  3.1664 -val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1";
  3.1665 -val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2";
  3.1666 -val complex_minus_mult_commute = thm"complex_minus_mult_commute";
  3.1667 -val complex_add_mult_distrib = thm"complex_add_mult_distrib";
  3.1668 -val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2";
  3.1669 -val complex_zero_not_eq_one = thm"complex_zero_not_eq_one";
  3.1670  val complex_inverse = thm"complex_inverse";
  3.1671 -val COMPLEX_INVERSE_ZERO = thm"COMPLEX_INVERSE_ZERO";
  3.1672 -val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO";
  3.1673 -val complex_mult_inv_left = thm"complex_mult_inv_left";
  3.1674 -val complex_mult_inv_right = thm"complex_mult_inv_right";
  3.1675 -val inj_complex_of_real = thm"inj_complex_of_real";
  3.1676  val complex_of_real_one = thm"complex_of_real_one";
  3.1677  val complex_of_real_zero = thm"complex_of_real_zero";
  3.1678  val complex_of_real_eq_iff = thm"complex_of_real_eq_iff";
  3.1679 @@ -1580,7 +1062,6 @@
  3.1680  val complex_mod_complex_of_real = thm"complex_mod_complex_of_real";
  3.1681  val complex_of_real_abs = thm"complex_of_real_abs";
  3.1682  val complex_cnj = thm"complex_cnj";
  3.1683 -val inj_cnj = thm"inj_cnj";
  3.1684  val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff";
  3.1685  val complex_cnj_cnj = thm"complex_cnj_cnj";
  3.1686  val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real";
  3.1687 @@ -1686,7 +1167,6 @@
  3.1688  val rcis_zero_arg = thm"rcis_zero_arg";
  3.1689  val complex_of_real_minus_one = thm"complex_of_real_minus_one";
  3.1690  val complex_i_mult_minus = thm"complex_i_mult_minus";
  3.1691 -val complex_i_mult_minus2 = thm"complex_i_mult_minus2";
  3.1692  val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult";
  3.1693  val DeMoivre = thm"DeMoivre";
  3.1694  val DeMoivre2 = thm"DeMoivre2";
  3.1695 @@ -1706,9 +1186,6 @@
  3.1696  val complex_Re_mult_eq = thm"complex_Re_mult_eq";
  3.1697  val complex_Im_mult_eq = thm"complex_Im_mult_eq";
  3.1698  val complex_expi_Ex = thm"complex_expi_Ex";
  3.1699 -
  3.1700 -val complex_add_ac = thms"complex_add_ac";
  3.1701 -val complex_mult_ac = thms"complex_mult_ac";
  3.1702  *}
  3.1703  
  3.1704  end
     4.1 --- a/src/HOL/Complex/ComplexArith0.ML	Tue Feb 03 10:19:21 2004 +0100
     4.2 +++ b/src/HOL/Complex/ComplexArith0.ML	Tue Feb 03 11:06:36 2004 +0100
     4.3 @@ -19,7 +19,7 @@
     4.4    val trans_tac         = Real_Numeral_Simprocs.trans_tac
     4.5    val norm_tac =  ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps @ mult_1s)) 
     4.6                    THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
     4.7 -                  THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_mult_ac))
     4.8 +                  THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
     4.9    val numeral_simp_tac	=  ALLGOALS (simp_tac (HOL_ss addsimps rel_complex_number_of@bin_simps))
    4.10    val simplify_meta_eq  = simplify_meta_eq
    4.11    end
    4.12 @@ -105,7 +105,7 @@
    4.13    val dest_coeff	= dest_coeff
    4.14    val find_first	= find_first []
    4.15    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    4.16 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@complex_mult_ac))
    4.17 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    4.18    end;
    4.19  
    4.20  
    4.21 @@ -173,13 +173,13 @@
    4.22  Addsimps [complex_minus1_divide];
    4.23  
    4.24  Goal "(x + - a = (0::complex)) = (x=a)";
    4.25 -by (simp_tac (simpset() addsimps [complex_diff_eq_eq,symmetric complex_diff_def]) 1);
    4.26 +by (simp_tac (simpset() addsimps [diff_eq_eq,symmetric complex_diff_def]) 1);
    4.27  qed "complex_add_minus_iff";
    4.28  Addsimps [complex_add_minus_iff];
    4.29  
    4.30  Goal "(x+y = (0::complex)) = (y = -x)";
    4.31  by Auto_tac;
    4.32 -by (dtac (sym RS (complex_diff_eq_eq RS iffD2)) 1);
    4.33 +by (dtac (sym RS (diff_eq_eq RS iffD2)) 1);
    4.34  by Auto_tac;  
    4.35  qed "complex_add_eq_0_iff";
    4.36  AddIffs [complex_add_eq_0_iff];
     5.1 --- a/src/HOL/Complex/ComplexBin.ML	Tue Feb 03 10:19:21 2004 +0100
     5.2 +++ b/src/HOL/Complex/ComplexBin.ML	Tue Feb 03 11:06:36 2004 +0100
     5.3 @@ -60,11 +60,11 @@
     5.4  
     5.5  (*For specialist use: NOT as default simprules*)
     5.6  Goal "2 * z = (z+z::complex)";
     5.7 -by (simp_tac (simpset () addsimps [lemma, complex_add_mult_distrib]) 1);
     5.8 +by (simp_tac (simpset () addsimps [lemma, left_distrib]) 1);
     5.9  qed "complex_mult_2";
    5.10  
    5.11  Goal "z * 2 = (z+z::complex)";
    5.12 -by (stac complex_mult_commute 1 THEN rtac complex_mult_2 1);
    5.13 +by (stac mult_commute 1 THEN rtac complex_mult_2 1);
    5.14  qed "complex_mult_2_right";
    5.15  
    5.16  (** Equals (=) **)
    5.17 @@ -88,7 +88,7 @@
    5.18  qed "complex_mult_minus1";
    5.19  
    5.20  Goal "z * -1 = -(z::complex)";
    5.21 -by (stac complex_mult_commute 1 THEN rtac complex_mult_minus1 1);
    5.22 +by (stac mult_commute 1 THEN rtac complex_mult_minus1 1);
    5.23  qed "complex_mult_minus1_right";
    5.24  
    5.25  Addsimps [complex_mult_minus1,complex_mult_minus1_right];
    5.26 @@ -111,7 +111,7 @@
    5.27  qed "complex_add_number_of_left";
    5.28  
    5.29  Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::complex)";
    5.30 -by (simp_tac (simpset() addsimps [complex_mult_assoc RS sym]) 1);
    5.31 +by (simp_tac (simpset() addsimps [mult_assoc RS sym]) 1);
    5.32  qed "complex_mult_number_of_left";
    5.33  
    5.34  Goalw [complex_diff_def]
    5.35 @@ -121,7 +121,7 @@
    5.36  
    5.37  Goal "number_of v + (c - number_of w) = \
    5.38  \     number_of (bin_add v (bin_minus w)) + (c::complex)";
    5.39 -by (auto_tac (claset(),simpset() addsimps [complex_diff_def]@ complex_add_ac));
    5.40 +by (auto_tac (claset(),simpset() addsimps [complex_diff_def]@ add_ac));
    5.41  qed "complex_add_number_of_diff2";
    5.42  
    5.43  Addsimps [complex_add_number_of_left, complex_mult_number_of_left,
    5.44 @@ -133,40 +133,10 @@
    5.45  (** Combining of literal coefficients in sums of products **)
    5.46  
    5.47  Goal "(x = y) = (x-y = (0::complex))";
    5.48 -by (simp_tac (simpset() addsimps [complex_diff_eq_eq]) 1);   
    5.49 +by (simp_tac (simpset() addsimps [diff_eq_eq]) 1);   
    5.50  qed "complex_eq_iff_diff_eq_0";
    5.51  
    5.52 -(** For combine_numerals **)
    5.53  
    5.54 -Goal "i*u + (j*u + k) = (i+j)*u + (k::complex)";
    5.55 -by (asm_simp_tac (simpset() addsimps [complex_add_mult_distrib]
    5.56 -    @ complex_add_ac) 1);
    5.57 -qed "left_complex_add_mult_distrib";
    5.58 -
    5.59 -(** For cancel_numerals **)
    5.60 -
    5.61 -Goal "((x::complex) = u + v) = (x - (u + v) = 0)";
    5.62 -by (auto_tac (claset(),simpset() addsimps [complex_diff_eq_eq]));
    5.63 -qed "complex_eq_add_diff_eq_0";
    5.64 -
    5.65 -Goal "((x::complex) = n) = (x - n = 0)";
    5.66 -by (auto_tac (claset(),simpset() addsimps [complex_diff_eq_eq]));
    5.67 -qed "complex_eq_diff_eq_0";
    5.68 -
    5.69 -val complex_rel_iff_rel_0_rls = [complex_eq_diff_eq_0,complex_eq_add_diff_eq_0];
    5.70 -
    5.71 -Goal "!!i::complex. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    5.72 -by (auto_tac (claset(), simpset() addsimps [complex_add_mult_distrib,
    5.73 -    complex_diff_def] @ complex_add_ac));
    5.74 -by (asm_simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1);
    5.75 -by (simp_tac (simpset() addsimps [complex_add_assoc]) 1);
    5.76 -qed "complex_eq_add_iff1";
    5.77 -
    5.78 -Goal "!!i::complex. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    5.79 -by (simp_tac (simpset() addsimps [ complex_eq_add_iff1]) 1);
    5.80 -by (auto_tac (claset(), simpset() addsimps [complex_diff_def, 
    5.81 -    complex_add_mult_distrib]@ complex_add_ac));
    5.82 -qed "complex_eq_add_iff2";
    5.83  
    5.84  structure Complex_Numeral_Simprocs =
    5.85  struct
    5.86 @@ -276,29 +246,26 @@
    5.87  		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
    5.88  
    5.89  (*To let us treat subtraction as addition*)
    5.90 -val diff_simps = [complex_diff_def, complex_minus_add_distrib, 
    5.91 -                  complex_minus_minus];
    5.92 +val diff_simps = [complex_diff_def, minus_add_distrib, minus_minus];
    5.93  
    5.94  (* push the unary minus down: - x * y = x * - y *)
    5.95  val complex_minus_mult_eq_1_to_2 = 
    5.96 -    [complex_minus_mult_eq1 RS sym, complex_minus_mult_eq2] MRS trans 
    5.97 +    [minus_mult_left RS sym, minus_mult_right] MRS trans 
    5.98      |> standard;
    5.99  
   5.100  (*to extract again any uncancelled minuses*)
   5.101  val complex_minus_from_mult_simps = 
   5.102 -    [complex_minus_minus, complex_minus_mult_eq1 RS sym, 
   5.103 -     complex_minus_mult_eq2 RS sym];
   5.104 +    [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
   5.105  
   5.106  (*combine unary minus with numeric literals, however nested within a product*)
   5.107  val complex_mult_minus_simps =
   5.108 -    [complex_mult_assoc, complex_minus_mult_eq1, complex_minus_mult_eq_1_to_2];
   5.109 +    [mult_assoc, minus_mult_left, complex_minus_mult_eq_1_to_2];
   5.110  
   5.111  (*Final simplification: cancel + and *  *)
   5.112  val simplify_meta_eq = 
   5.113      Int_Numeral_Simprocs.simplify_meta_eq
   5.114 -         [complex_add_zero_left, complex_add_zero_right,
   5.115 - 	  complex_mult_zero_left, complex_mult_zero_right, complex_mult_one_left, 
   5.116 -          complex_mult_one_right];
   5.117 +         [add_zero_left, add_zero_right,
   5.118 + 	  mult_zero_left, mult_zero_right, mult_1, mult_1_right];
   5.119  
   5.120  val prep_simproc = Real_Numeral_Simprocs.prep_simproc;
   5.121  
   5.122 @@ -313,11 +280,11 @@
   5.123    val trans_tac         = Real_Numeral_Simprocs.trans_tac
   5.124    val norm_tac = 
   5.125       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   5.126 -                                         complex_minus_simps@complex_add_ac))
   5.127 +                                         complex_minus_simps@add_ac))
   5.128       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
   5.129       THEN ALLGOALS
   5.130                (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
   5.131 -                                         complex_add_ac@complex_mult_ac))
   5.132 +                                         add_ac@mult_ac))
   5.133    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   5.134    val simplify_meta_eq  = simplify_meta_eq
   5.135    end;
   5.136 @@ -328,8 +295,8 @@
   5.137    val prove_conv = Bin_Simprocs.prove_conv
   5.138    val mk_bal   = HOLogic.mk_eq
   5.139    val dest_bal = HOLogic.dest_bin "op =" complexT
   5.140 -  val bal_add1 = complex_eq_add_iff1 RS trans
   5.141 -  val bal_add2 = complex_eq_add_iff2 RS trans
   5.142 +  val bal_add1 = eq_add_iff1 RS trans
   5.143 +  val bal_add2 = eq_add_iff2 RS trans
   5.144  );
   5.145  
   5.146  
   5.147 @@ -348,15 +315,15 @@
   5.148    val dest_sum		= dest_sum
   5.149    val mk_coeff		= mk_coeff
   5.150    val dest_coeff	= dest_coeff 1
   5.151 -  val left_distrib	= left_complex_add_mult_distrib RS trans
   5.152 +  val left_distrib	= combine_common_factor RS trans
   5.153    val prove_conv	= Bin_Simprocs.prove_conv_nohyps
   5.154    val trans_tac         = Real_Numeral_Simprocs.trans_tac
   5.155    val norm_tac = 
   5.156       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   5.157 -                                         complex_minus_simps@complex_add_ac))
   5.158 +                                         complex_minus_simps@add_ac))
   5.159       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
   5.160       THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
   5.161 -                                              complex_add_ac@complex_mult_ac))
   5.162 +                                              add_ac@mult_ac))
   5.163    val numeral_simp_tac	= ALLGOALS 
   5.164                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   5.165    val simplify_meta_eq  = simplify_meta_eq
   5.166 @@ -470,7 +437,7 @@
   5.167    val sg_ref    = Sign.self_ref (Theory.sign_of (the_context ()))
   5.168    val T	     = Complex_Numeral_Simprocs.complexT
   5.169    val plus   = Const ("op *", [T,T] ---> T)
   5.170 -  val add_ac = complex_mult_ac
   5.171 +  val add_ac = mult_ac
   5.172  end;
   5.173  
   5.174  structure Complex_Times_Assoc = Assoc_Fold (Complex_Times_Assoc_Data);
   5.175 @@ -479,9 +446,6 @@
   5.176  
   5.177  Addsimps [complex_of_real_zero_iff];
   5.178  
   5.179 -(*Simplification of  x-y = 0 *)
   5.180 -
   5.181 -AddIffs [complex_eq_iff_diff_eq_0 RS sym];
   5.182  
   5.183  (*** Real and imaginary stuff ***)
   5.184  
     6.1 --- a/src/HOL/Complex/NSCA.ML	Tue Feb 03 10:19:21 2004 +0100
     6.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Feb 03 11:06:36 2004 +0100
     6.3 @@ -4,6 +4,9 @@
     6.4      Description : Infinite, infinitesimal complex number etc! 
     6.5  *)
     6.6  
     6.7 +val complex_induct = thm"complex.induct";
     6.8 +
     6.9 +
    6.10  (*--------------------------------------------------------------------------------------*)
    6.11  (* Closure laws for members of (embedded) set standard complex SComplex                 *)
    6.12  (* -------------------------------------------------------------------------------------*)
    6.13 @@ -785,8 +788,8 @@
    6.14  by (dres_inst_tac [("x","m")] spec 1);
    6.15  by (Ultra_tac 1);
    6.16  by (rename_tac "Z x" 1);
    6.17 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.18 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    6.19 +by (case_tac "X x" 1);
    6.20 +by (case_tac "Y x" 1);
    6.21  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    6.22      complex_mod] delsimps [realpow_Suc]));
    6.23  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    6.24 @@ -806,8 +809,8 @@
    6.25  by (dres_inst_tac [("x","m")] spec 1);
    6.26  by (Ultra_tac 1);
    6.27  by (rename_tac "Z x" 1);
    6.28 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.29 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    6.30 +by (case_tac "X x" 1);
    6.31 +by (case_tac "Y x" 1);
    6.32  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    6.33      complex_mod] delsimps [realpow_Suc]));
    6.34  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    6.35 @@ -836,12 +839,13 @@
    6.36  by (TRYALL(Force_tac));
    6.37  by (ultra_tac (claset(),HOL_ss) 1);
    6.38  by (dtac sym 1 THEN dtac sym 1); 
    6.39 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.40 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    6.41 +by (case_tac "X x" 1);
    6.42 +by (case_tac "Y x" 1);
    6.43  by (auto_tac (claset(),
    6.44      HOL_ss addsimps [complex_minus,complex_add,
    6.45      complex_mod, snd_conv, fst_conv,numeral_2_eq_2]));
    6.46 -by (subgoal_tac "sqrt (abs(xa + - xb) ^ 2 + abs(y + - ya) ^ 2) < u" 1);
    6.47 +by (rename_tac "a b c d" 1);
    6.48 +by (subgoal_tac "sqrt (abs(a + - c) ^ 2 + abs(b + - d) ^ 2) < u" 1);
    6.49  by (rtac lemma_sqrt_hcomplex_capprox 2);
    6.50  by Auto_tac;
    6.51  by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1); 
    6.52 @@ -868,7 +872,7 @@
    6.53  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    6.54  by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
    6.55  by (Ultra_tac 1);
    6.56 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.57 +by (dtac sym 1 THEN case_tac "X x" 1);
    6.58  by (auto_tac (claset(),
    6.59      simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
    6.60  by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
    6.61 @@ -884,7 +888,7 @@
    6.62  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    6.63  by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
    6.64  by (Ultra_tac 1);
    6.65 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.66 +by (dtac sym 1 THEN case_tac "X x" 1);
    6.67  by (auto_tac (claset(),simpset() addsimps [complex_mod] delsimps [realpow_Suc]));
    6.68  by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
    6.69  by (dtac order_less_le_trans 1 THEN assume_tac 1);
    6.70 @@ -901,7 +905,7 @@
    6.71  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    6.72  by (res_inst_tac [("x","2*(u + v)")] exI 1);
    6.73  by (Ultra_tac 1);
    6.74 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.75 +by (dtac sym 1 THEN case_tac "X x" 1);
    6.76  by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
    6.77  by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
    6.78  by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
    6.79 @@ -941,7 +945,7 @@
    6.80      hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
    6.81  by (res_inst_tac [("x","complex_of_real r + ii  * complex_of_real ra")] exI 1);
    6.82  by (Ultra_tac 1);
    6.83 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    6.84 +by (case_tac "X x" 1);
    6.85  by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
    6.86      complex_add,complex_mult]));
    6.87  qed "Reals_Re_Im_SComplex";
     7.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Feb 03 10:19:21 2004 +0100
     7.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Feb 03 11:06:36 2004 +0100
     7.3 @@ -372,7 +372,7 @@
     7.4  apply (rule_tac z = "z1" in eq_Abs_hcomplex)
     7.5  apply (rule_tac z = "z2" in eq_Abs_hcomplex)
     7.6  apply (rule_tac z = "w" in eq_Abs_hcomplex)
     7.7 -apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
     7.8 +apply (auto simp add: hcomplex_mult hcomplex_add left_distrib)
     7.9  done
    7.10  
    7.11  lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
    7.12 @@ -400,7 +400,7 @@
    7.13  apply (auto simp add: hcomplex_inverse hcomplex_mult)
    7.14  apply (ultra)
    7.15  apply (rule ccontr)
    7.16 -apply (drule complex_mult_inv_left)
    7.17 +apply (drule left_inverse)
    7.18  apply auto
    7.19  done
    7.20  
    7.21 @@ -744,24 +744,6 @@
    7.22  done
    7.23  declare hcnj_one [simp]
    7.24  
    7.25 -
    7.26 -(* MOVE to NSComplexBin
    7.27 -Goal "z + hcnj z =
    7.28 -      hcomplex_of_hypreal (2 * hRe(z))"
    7.29 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    7.30 -by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
    7.31 -    hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
    7.32 -qed "hcomplex_add_hcnj";
    7.33 -
    7.34 -Goal "z - hcnj z = \
    7.35 -\     hcomplex_of_hypreal (hypreal_of_real 2 * hIm(z)) * iii";
    7.36 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    7.37 -by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
    7.38 -    hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
    7.39 -    complex_diff_cnj,iii_def,hcomplex_mult]));
    7.40 -qed "hcomplex_diff_hcnj";
    7.41 -*)
    7.42 -
    7.43  lemma hcomplex_hcnj_zero:
    7.44        "hcnj 0 = 0"
    7.45  apply (unfold hcomplex_zero_def)
     8.1 --- a/src/HOL/Complex/NSComplexBin.ML	Tue Feb 03 10:19:21 2004 +0100
     8.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Tue Feb 03 11:06:36 2004 +0100
     8.3 @@ -161,49 +161,6 @@
     8.4  
     8.5  (**** Simprocs for numeric literals ****)
     8.6  
     8.7 -(** Combining of literal coefficients in sums of products **)
     8.8 -
     8.9 -Goal "(x = y) = (x-y = (0::hcomplex))";
    8.10 -by (simp_tac (simpset() addsimps [hcomplex_diff_eq_eq]) 1);   
    8.11 -qed "hcomplex_eq_iff_diff_eq_0";
    8.12 -
    8.13 -(** For combine_numerals **)
    8.14 -
    8.15 -Goal "i*u + (j*u + k) = (i+j)*u + (k::hcomplex)";
    8.16 -by (asm_simp_tac (simpset() addsimps [hcomplex_add_mult_distrib]
    8.17 -    @ add_ac) 1);
    8.18 -qed "left_hcomplex_add_mult_distrib";
    8.19 -
    8.20 -(** For cancel_numerals **)
    8.21 -
    8.22 -Goal "((x::hcomplex) = u + v) = (x - (u + v) = 0)";
    8.23 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_eq_eq]));
    8.24 -qed "hcomplex_eq_add_diff_eq_0";
    8.25 -
    8.26 -Goal "((x::hcomplex) = n) = (x - n = 0)";
    8.27 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_eq_eq]));
    8.28 -qed "hcomplex_eq_diff_eq_0";
    8.29 -
    8.30 -val hcomplex_rel_iff_rel_0_rls = [hcomplex_eq_diff_eq_0,hcomplex_eq_add_diff_eq_0];
    8.31 -
    8.32 -Goal "!!i::hcomplex. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    8.33 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_mult_distrib,
    8.34 -    hcomplex_diff_def] @ add_ac));
    8.35 -by (asm_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1);
    8.36 -by (simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
    8.37 -qed "hcomplex_eq_add_iff1";
    8.38 -
    8.39 -Goal "!!i::hcomplex. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    8.40 -by (res_inst_tac [("z","i")] eq_Abs_hcomplex 1);
    8.41 -by (res_inst_tac [("z","j")] eq_Abs_hcomplex 1);
    8.42 -by (res_inst_tac [("z","u")] eq_Abs_hcomplex 1);
    8.43 -by (res_inst_tac [("z","m")] eq_Abs_hcomplex 1);
    8.44 -by (res_inst_tac [("z","n")] eq_Abs_hcomplex 1);
    8.45 -by (auto_tac (claset(), simpset() addsimps [hcomplex_diff,hcomplex_add,
    8.46 -    hcomplex_mult,complex_eq_add_iff2]));
    8.47 -qed "hcomplex_eq_add_iff2";
    8.48 -
    8.49 -
    8.50  structure HComplex_Numeral_Simprocs =
    8.51  struct
    8.52  
    8.53 @@ -358,8 +315,8 @@
    8.54    val prove_conv = Bin_Simprocs.prove_conv
    8.55    val mk_bal   = HOLogic.mk_eq
    8.56    val dest_bal = HOLogic.dest_bin "op =" hcomplexT
    8.57 -  val bal_add1 = hcomplex_eq_add_iff1 RS trans
    8.58 -  val bal_add2 = hcomplex_eq_add_iff2 RS trans
    8.59 +  val bal_add1 = eq_add_iff1 RS trans
    8.60 +  val bal_add2 = eq_add_iff2 RS trans
    8.61  );
    8.62  
    8.63  
    8.64 @@ -378,7 +335,7 @@
    8.65    val dest_sum		= dest_sum
    8.66    val mk_coeff		= mk_coeff
    8.67    val dest_coeff	= dest_coeff 1
    8.68 -  val left_distrib	= left_hcomplex_add_mult_distrib RS trans
    8.69 +  val left_distrib	= combine_common_factor RS trans
    8.70    val prove_conv	= Bin_Simprocs.prove_conv_nohyps
    8.71    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    8.72    val norm_tac = 
    8.73 @@ -507,9 +464,6 @@
    8.74  
    8.75  Addsimps [hcomplex_of_complex_zero_iff];
    8.76  
    8.77 -(*Simplification of  x-y = 0 *)
    8.78 -
    8.79 -AddIffs [hcomplex_eq_iff_diff_eq_0 RS sym];
    8.80  
    8.81  (** extra thms **)
    8.82  
     9.1 --- a/src/HOL/Complex/ex/BinEx.thy	Tue Feb 03 10:19:21 2004 +0100
     9.2 +++ b/src/HOL/Complex/ex/BinEx.thy	Tue Feb 03 11:06:36 2004 +0100
     9.3 @@ -381,8 +381,7 @@
     9.4  text{*Multiplication requires distributive laws.  Perhaps versions instantiated
     9.5  to literal constants should be added to the simpset.*}
     9.6  
     9.7 -lemmas distrib = complex_add_mult_distrib complex_add_mult_distrib2
     9.8 -                 complex_diff_mult_distrib complex_diff_mult_distrib2
     9.9 +lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib
    9.10  
    9.11  lemma "(1 + ii) * (1 - ii) = 2"
    9.12  by (simp add: distrib)
    9.13 @@ -393,10 +392,8 @@
    9.14  lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
    9.15  by (simp add: distrib)
    9.16  
    9.17 -text{*No inequalities: we have no ordering on the complex numbers.*}
    9.18 +text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
    9.19  
    9.20  text{*No powers (not supported yet)*}
    9.21  
    9.22 -text{*No linear arithmetic*}
    9.23 -
    9.24  end
    10.1 --- a/src/HOL/IsaMakefile	Tue Feb 03 10:19:21 2004 +0100
    10.2 +++ b/src/HOL/IsaMakefile	Tue Feb 03 11:06:36 2004 +0100
    10.3 @@ -138,7 +138,7 @@
    10.4  
    10.5  $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\
    10.6    Library/Zorn.thy\
    10.7 -  Real/Complex_Numbers.thy Real/Lubs.thy Real/rat_arith.ML Real/RatArith.thy\
    10.8 +  Real/Lubs.thy Real/rat_arith.ML Real/RatArith.thy\
    10.9    Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   10.10    Real/ROOT.ML Real/Real.thy \
   10.11    Real/RealArith.thy Real/real_arith.ML Real/RealDef.thy \