src/HOL/Complex/ComplexBin.ML
changeset 14373 67a628beb981
parent 14290 84fda1b39947
child 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/ComplexBin.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/ComplexBin.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -60,11 +60,11 @@
     1.4  
     1.5  (*For specialist use: NOT as default simprules*)
     1.6  Goal "2 * z = (z+z::complex)";
     1.7 -by (simp_tac (simpset () addsimps [lemma, complex_add_mult_distrib]) 1);
     1.8 +by (simp_tac (simpset () addsimps [lemma, left_distrib]) 1);
     1.9  qed "complex_mult_2";
    1.10  
    1.11  Goal "z * 2 = (z+z::complex)";
    1.12 -by (stac complex_mult_commute 1 THEN rtac complex_mult_2 1);
    1.13 +by (stac mult_commute 1 THEN rtac complex_mult_2 1);
    1.14  qed "complex_mult_2_right";
    1.15  
    1.16  (** Equals (=) **)
    1.17 @@ -88,7 +88,7 @@
    1.18  qed "complex_mult_minus1";
    1.19  
    1.20  Goal "z * -1 = -(z::complex)";
    1.21 -by (stac complex_mult_commute 1 THEN rtac complex_mult_minus1 1);
    1.22 +by (stac mult_commute 1 THEN rtac complex_mult_minus1 1);
    1.23  qed "complex_mult_minus1_right";
    1.24  
    1.25  Addsimps [complex_mult_minus1,complex_mult_minus1_right];
    1.26 @@ -111,7 +111,7 @@
    1.27  qed "complex_add_number_of_left";
    1.28  
    1.29  Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::complex)";
    1.30 -by (simp_tac (simpset() addsimps [complex_mult_assoc RS sym]) 1);
    1.31 +by (simp_tac (simpset() addsimps [mult_assoc RS sym]) 1);
    1.32  qed "complex_mult_number_of_left";
    1.33  
    1.34  Goalw [complex_diff_def]
    1.35 @@ -121,7 +121,7 @@
    1.36  
    1.37  Goal "number_of v + (c - number_of w) = \
    1.38  \     number_of (bin_add v (bin_minus w)) + (c::complex)";
    1.39 -by (auto_tac (claset(),simpset() addsimps [complex_diff_def]@ complex_add_ac));
    1.40 +by (auto_tac (claset(),simpset() addsimps [complex_diff_def]@ add_ac));
    1.41  qed "complex_add_number_of_diff2";
    1.42  
    1.43  Addsimps [complex_add_number_of_left, complex_mult_number_of_left,
    1.44 @@ -133,40 +133,10 @@
    1.45  (** Combining of literal coefficients in sums of products **)
    1.46  
    1.47  Goal "(x = y) = (x-y = (0::complex))";
    1.48 -by (simp_tac (simpset() addsimps [complex_diff_eq_eq]) 1);   
    1.49 +by (simp_tac (simpset() addsimps [diff_eq_eq]) 1);   
    1.50  qed "complex_eq_iff_diff_eq_0";
    1.51  
    1.52 -(** For combine_numerals **)
    1.53  
    1.54 -Goal "i*u + (j*u + k) = (i+j)*u + (k::complex)";
    1.55 -by (asm_simp_tac (simpset() addsimps [complex_add_mult_distrib]
    1.56 -    @ complex_add_ac) 1);
    1.57 -qed "left_complex_add_mult_distrib";
    1.58 -
    1.59 -(** For cancel_numerals **)
    1.60 -
    1.61 -Goal "((x::complex) = u + v) = (x - (u + v) = 0)";
    1.62 -by (auto_tac (claset(),simpset() addsimps [complex_diff_eq_eq]));
    1.63 -qed "complex_eq_add_diff_eq_0";
    1.64 -
    1.65 -Goal "((x::complex) = n) = (x - n = 0)";
    1.66 -by (auto_tac (claset(),simpset() addsimps [complex_diff_eq_eq]));
    1.67 -qed "complex_eq_diff_eq_0";
    1.68 -
    1.69 -val complex_rel_iff_rel_0_rls = [complex_eq_diff_eq_0,complex_eq_add_diff_eq_0];
    1.70 -
    1.71 -Goal "!!i::complex. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    1.72 -by (auto_tac (claset(), simpset() addsimps [complex_add_mult_distrib,
    1.73 -    complex_diff_def] @ complex_add_ac));
    1.74 -by (asm_simp_tac (simpset() addsimps [complex_add_assoc RS sym]) 1);
    1.75 -by (simp_tac (simpset() addsimps [complex_add_assoc]) 1);
    1.76 -qed "complex_eq_add_iff1";
    1.77 -
    1.78 -Goal "!!i::complex. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    1.79 -by (simp_tac (simpset() addsimps [ complex_eq_add_iff1]) 1);
    1.80 -by (auto_tac (claset(), simpset() addsimps [complex_diff_def, 
    1.81 -    complex_add_mult_distrib]@ complex_add_ac));
    1.82 -qed "complex_eq_add_iff2";
    1.83  
    1.84  structure Complex_Numeral_Simprocs =
    1.85  struct
    1.86 @@ -276,29 +246,26 @@
    1.87  		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
    1.88  
    1.89  (*To let us treat subtraction as addition*)
    1.90 -val diff_simps = [complex_diff_def, complex_minus_add_distrib, 
    1.91 -                  complex_minus_minus];
    1.92 +val diff_simps = [complex_diff_def, minus_add_distrib, minus_minus];
    1.93  
    1.94  (* push the unary minus down: - x * y = x * - y *)
    1.95  val complex_minus_mult_eq_1_to_2 = 
    1.96 -    [complex_minus_mult_eq1 RS sym, complex_minus_mult_eq2] MRS trans 
    1.97 +    [minus_mult_left RS sym, minus_mult_right] MRS trans 
    1.98      |> standard;
    1.99  
   1.100  (*to extract again any uncancelled minuses*)
   1.101  val complex_minus_from_mult_simps = 
   1.102 -    [complex_minus_minus, complex_minus_mult_eq1 RS sym, 
   1.103 -     complex_minus_mult_eq2 RS sym];
   1.104 +    [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
   1.105  
   1.106  (*combine unary minus with numeric literals, however nested within a product*)
   1.107  val complex_mult_minus_simps =
   1.108 -    [complex_mult_assoc, complex_minus_mult_eq1, complex_minus_mult_eq_1_to_2];
   1.109 +    [mult_assoc, minus_mult_left, complex_minus_mult_eq_1_to_2];
   1.110  
   1.111  (*Final simplification: cancel + and *  *)
   1.112  val simplify_meta_eq = 
   1.113      Int_Numeral_Simprocs.simplify_meta_eq
   1.114 -         [complex_add_zero_left, complex_add_zero_right,
   1.115 - 	  complex_mult_zero_left, complex_mult_zero_right, complex_mult_one_left, 
   1.116 -          complex_mult_one_right];
   1.117 +         [add_zero_left, add_zero_right,
   1.118 + 	  mult_zero_left, mult_zero_right, mult_1, mult_1_right];
   1.119  
   1.120  val prep_simproc = Real_Numeral_Simprocs.prep_simproc;
   1.121  
   1.122 @@ -313,11 +280,11 @@
   1.123    val trans_tac         = Real_Numeral_Simprocs.trans_tac
   1.124    val norm_tac = 
   1.125       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.126 -                                         complex_minus_simps@complex_add_ac))
   1.127 +                                         complex_minus_simps@add_ac))
   1.128       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
   1.129       THEN ALLGOALS
   1.130                (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
   1.131 -                                         complex_add_ac@complex_mult_ac))
   1.132 +                                         add_ac@mult_ac))
   1.133    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.134    val simplify_meta_eq  = simplify_meta_eq
   1.135    end;
   1.136 @@ -328,8 +295,8 @@
   1.137    val prove_conv = Bin_Simprocs.prove_conv
   1.138    val mk_bal   = HOLogic.mk_eq
   1.139    val dest_bal = HOLogic.dest_bin "op =" complexT
   1.140 -  val bal_add1 = complex_eq_add_iff1 RS trans
   1.141 -  val bal_add2 = complex_eq_add_iff2 RS trans
   1.142 +  val bal_add1 = eq_add_iff1 RS trans
   1.143 +  val bal_add2 = eq_add_iff2 RS trans
   1.144  );
   1.145  
   1.146  
   1.147 @@ -348,15 +315,15 @@
   1.148    val dest_sum		= dest_sum
   1.149    val mk_coeff		= mk_coeff
   1.150    val dest_coeff	= dest_coeff 1
   1.151 -  val left_distrib	= left_complex_add_mult_distrib RS trans
   1.152 +  val left_distrib	= combine_common_factor RS trans
   1.153    val prove_conv	= Bin_Simprocs.prove_conv_nohyps
   1.154    val trans_tac         = Real_Numeral_Simprocs.trans_tac
   1.155    val norm_tac = 
   1.156       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.157 -                                         complex_minus_simps@complex_add_ac))
   1.158 +                                         complex_minus_simps@add_ac))
   1.159       THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
   1.160       THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
   1.161 -                                              complex_add_ac@complex_mult_ac))
   1.162 +                                              add_ac@mult_ac))
   1.163    val numeral_simp_tac	= ALLGOALS 
   1.164                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.165    val simplify_meta_eq  = simplify_meta_eq
   1.166 @@ -470,7 +437,7 @@
   1.167    val sg_ref    = Sign.self_ref (Theory.sign_of (the_context ()))
   1.168    val T	     = Complex_Numeral_Simprocs.complexT
   1.169    val plus   = Const ("op *", [T,T] ---> T)
   1.170 -  val add_ac = complex_mult_ac
   1.171 +  val add_ac = mult_ac
   1.172  end;
   1.173  
   1.174  structure Complex_Times_Assoc = Assoc_Fold (Complex_Times_Assoc_Data);
   1.175 @@ -479,9 +446,6 @@
   1.176  
   1.177  Addsimps [complex_of_real_zero_iff];
   1.178  
   1.179 -(*Simplification of  x-y = 0 *)
   1.180 -
   1.181 -AddIffs [complex_eq_iff_diff_eq_0 RS sym];
   1.182  
   1.183  (*** Real and imaginary stuff ***)
   1.184