src/HOL/Complex/NSComplex.thy
changeset 14373 67a628beb981
parent 14371 c78c7da09519
child 14374 61de62096768
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -372,7 +372,7 @@
     1.4  apply (rule_tac z = "z1" in eq_Abs_hcomplex)
     1.5  apply (rule_tac z = "z2" in eq_Abs_hcomplex)
     1.6  apply (rule_tac z = "w" in eq_Abs_hcomplex)
     1.7 -apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
     1.8 +apply (auto simp add: hcomplex_mult hcomplex_add left_distrib)
     1.9  done
    1.10  
    1.11  lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
    1.12 @@ -400,7 +400,7 @@
    1.13  apply (auto simp add: hcomplex_inverse hcomplex_mult)
    1.14  apply (ultra)
    1.15  apply (rule ccontr)
    1.16 -apply (drule complex_mult_inv_left)
    1.17 +apply (drule left_inverse)
    1.18  apply auto
    1.19  done
    1.20  
    1.21 @@ -744,24 +744,6 @@
    1.22  done
    1.23  declare hcnj_one [simp]
    1.24  
    1.25 -
    1.26 -(* MOVE to NSComplexBin
    1.27 -Goal "z + hcnj z =
    1.28 -      hcomplex_of_hypreal (2 * hRe(z))"
    1.29 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    1.30 -by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
    1.31 -    hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
    1.32 -qed "hcomplex_add_hcnj";
    1.33 -
    1.34 -Goal "z - hcnj z = \
    1.35 -\     hcomplex_of_hypreal (hypreal_of_real 2 * hIm(z)) * iii";
    1.36 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    1.37 -by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
    1.38 -    hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
    1.39 -    complex_diff_cnj,iii_def,hcomplex_mult]));
    1.40 -qed "hcomplex_diff_hcnj";
    1.41 -*)
    1.42 -
    1.43  lemma hcomplex_hcnj_zero:
    1.44        "hcnj 0 = 0"
    1.45  apply (unfold hcomplex_zero_def)