src/HOL/Complex/NSCA.ML
changeset 14373 67a628beb981
parent 14365 3d4df8c166ae
child 14374 61de62096768
     1.1 --- a/src/HOL/Complex/NSCA.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -4,6 +4,9 @@
     1.4      Description : Infinite, infinitesimal complex number etc! 
     1.5  *)
     1.6  
     1.7 +val complex_induct = thm"complex.induct";
     1.8 +
     1.9 +
    1.10  (*--------------------------------------------------------------------------------------*)
    1.11  (* Closure laws for members of (embedded) set standard complex SComplex                 *)
    1.12  (* -------------------------------------------------------------------------------------*)
    1.13 @@ -785,8 +788,8 @@
    1.14  by (dres_inst_tac [("x","m")] spec 1);
    1.15  by (Ultra_tac 1);
    1.16  by (rename_tac "Z x" 1);
    1.17 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.18 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    1.19 +by (case_tac "X x" 1);
    1.20 +by (case_tac "Y x" 1);
    1.21  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    1.22      complex_mod] delsimps [realpow_Suc]));
    1.23  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    1.24 @@ -806,8 +809,8 @@
    1.25  by (dres_inst_tac [("x","m")] spec 1);
    1.26  by (Ultra_tac 1);
    1.27  by (rename_tac "Z x" 1);
    1.28 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.29 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    1.30 +by (case_tac "X x" 1);
    1.31 +by (case_tac "Y x" 1);
    1.32  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    1.33      complex_mod] delsimps [realpow_Suc]));
    1.34  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    1.35 @@ -836,12 +839,13 @@
    1.36  by (TRYALL(Force_tac));
    1.37  by (ultra_tac (claset(),HOL_ss) 1);
    1.38  by (dtac sym 1 THEN dtac sym 1); 
    1.39 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.40 -by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    1.41 +by (case_tac "X x" 1);
    1.42 +by (case_tac "Y x" 1);
    1.43  by (auto_tac (claset(),
    1.44      HOL_ss addsimps [complex_minus,complex_add,
    1.45      complex_mod, snd_conv, fst_conv,numeral_2_eq_2]));
    1.46 -by (subgoal_tac "sqrt (abs(xa + - xb) ^ 2 + abs(y + - ya) ^ 2) < u" 1);
    1.47 +by (rename_tac "a b c d" 1);
    1.48 +by (subgoal_tac "sqrt (abs(a + - c) ^ 2 + abs(b + - d) ^ 2) < u" 1);
    1.49  by (rtac lemma_sqrt_hcomplex_capprox 2);
    1.50  by Auto_tac;
    1.51  by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1); 
    1.52 @@ -868,7 +872,7 @@
    1.53  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.54  by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
    1.55  by (Ultra_tac 1);
    1.56 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.57 +by (dtac sym 1 THEN case_tac "X x" 1);
    1.58  by (auto_tac (claset(),
    1.59      simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
    1.60  by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
    1.61 @@ -884,7 +888,7 @@
    1.62  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.63  by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
    1.64  by (Ultra_tac 1);
    1.65 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.66 +by (dtac sym 1 THEN case_tac "X x" 1);
    1.67  by (auto_tac (claset(),simpset() addsimps [complex_mod] delsimps [realpow_Suc]));
    1.68  by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
    1.69  by (dtac order_less_le_trans 1 THEN assume_tac 1);
    1.70 @@ -901,7 +905,7 @@
    1.71  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.72  by (res_inst_tac [("x","2*(u + v)")] exI 1);
    1.73  by (Ultra_tac 1);
    1.74 -by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.75 +by (dtac sym 1 THEN case_tac "X x" 1);
    1.76  by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
    1.77  by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
    1.78  by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
    1.79 @@ -941,7 +945,7 @@
    1.80      hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
    1.81  by (res_inst_tac [("x","complex_of_real r + ii  * complex_of_real ra")] exI 1);
    1.82  by (Ultra_tac 1);
    1.83 -by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.84 +by (case_tac "X x" 1);
    1.85  by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
    1.86      complex_add,complex_mult]));
    1.87  qed "Reals_Re_Im_SComplex";