src/HOL/Complex/NSComplexBin.ML
changeset 14373 67a628beb981
parent 14353 79f9fbef9106
child 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/NSComplexBin.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -161,49 +161,6 @@
     1.4  
     1.5  (**** Simprocs for numeric literals ****)
     1.6  
     1.7 -(** Combining of literal coefficients in sums of products **)
     1.8 -
     1.9 -Goal "(x = y) = (x-y = (0::hcomplex))";
    1.10 -by (simp_tac (simpset() addsimps [hcomplex_diff_eq_eq]) 1);   
    1.11 -qed "hcomplex_eq_iff_diff_eq_0";
    1.12 -
    1.13 -(** For combine_numerals **)
    1.14 -
    1.15 -Goal "i*u + (j*u + k) = (i+j)*u + (k::hcomplex)";
    1.16 -by (asm_simp_tac (simpset() addsimps [hcomplex_add_mult_distrib]
    1.17 -    @ add_ac) 1);
    1.18 -qed "left_hcomplex_add_mult_distrib";
    1.19 -
    1.20 -(** For cancel_numerals **)
    1.21 -
    1.22 -Goal "((x::hcomplex) = u + v) = (x - (u + v) = 0)";
    1.23 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_eq_eq]));
    1.24 -qed "hcomplex_eq_add_diff_eq_0";
    1.25 -
    1.26 -Goal "((x::hcomplex) = n) = (x - n = 0)";
    1.27 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_eq_eq]));
    1.28 -qed "hcomplex_eq_diff_eq_0";
    1.29 -
    1.30 -val hcomplex_rel_iff_rel_0_rls = [hcomplex_eq_diff_eq_0,hcomplex_eq_add_diff_eq_0];
    1.31 -
    1.32 -Goal "!!i::hcomplex. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    1.33 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_mult_distrib,
    1.34 -    hcomplex_diff_def] @ add_ac));
    1.35 -by (asm_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1);
    1.36 -by (simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
    1.37 -qed "hcomplex_eq_add_iff1";
    1.38 -
    1.39 -Goal "!!i::hcomplex. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    1.40 -by (res_inst_tac [("z","i")] eq_Abs_hcomplex 1);
    1.41 -by (res_inst_tac [("z","j")] eq_Abs_hcomplex 1);
    1.42 -by (res_inst_tac [("z","u")] eq_Abs_hcomplex 1);
    1.43 -by (res_inst_tac [("z","m")] eq_Abs_hcomplex 1);
    1.44 -by (res_inst_tac [("z","n")] eq_Abs_hcomplex 1);
    1.45 -by (auto_tac (claset(), simpset() addsimps [hcomplex_diff,hcomplex_add,
    1.46 -    hcomplex_mult,complex_eq_add_iff2]));
    1.47 -qed "hcomplex_eq_add_iff2";
    1.48 -
    1.49 -
    1.50  structure HComplex_Numeral_Simprocs =
    1.51  struct
    1.52  
    1.53 @@ -358,8 +315,8 @@
    1.54    val prove_conv = Bin_Simprocs.prove_conv
    1.55    val mk_bal   = HOLogic.mk_eq
    1.56    val dest_bal = HOLogic.dest_bin "op =" hcomplexT
    1.57 -  val bal_add1 = hcomplex_eq_add_iff1 RS trans
    1.58 -  val bal_add2 = hcomplex_eq_add_iff2 RS trans
    1.59 +  val bal_add1 = eq_add_iff1 RS trans
    1.60 +  val bal_add2 = eq_add_iff2 RS trans
    1.61  );
    1.62  
    1.63  
    1.64 @@ -378,7 +335,7 @@
    1.65    val dest_sum		= dest_sum
    1.66    val mk_coeff		= mk_coeff
    1.67    val dest_coeff	= dest_coeff 1
    1.68 -  val left_distrib	= left_hcomplex_add_mult_distrib RS trans
    1.69 +  val left_distrib	= combine_common_factor RS trans
    1.70    val prove_conv	= Bin_Simprocs.prove_conv_nohyps
    1.71    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    1.72    val norm_tac = 
    1.73 @@ -507,9 +464,6 @@
    1.74  
    1.75  Addsimps [hcomplex_of_complex_zero_iff];
    1.76  
    1.77 -(*Simplification of  x-y = 0 *)
    1.78 -
    1.79 -AddIffs [hcomplex_eq_iff_diff_eq_0 RS sym];
    1.80  
    1.81  (** extra thms **)
    1.82