941 Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals; \ |
941 Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals; \ |
942 \ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals \ |
942 \ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals \ |
943 \ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex"; |
943 \ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex"; |
944 by (auto_tac (claset(),simpset() addsimps [SComplex_def, |
944 by (auto_tac (claset(),simpset() addsimps [SComplex_def, |
945 hcomplex_of_complex_def,SReal_def,hypreal_of_real_def])); |
945 hcomplex_of_complex_def,SReal_def,hypreal_of_real_def])); |
946 by (res_inst_tac [("x","complex_of_real r + ii * complex_of_real ra")] exI 1); |
946 by (res_inst_tac [("x","Complex r ra")] exI 1); |
947 by (Ultra_tac 1); |
947 by (Ultra_tac 1); |
948 by (case_tac "X x" 1); |
|
949 by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def, |
|
950 complex_add,complex_mult])); |
|
951 qed "Reals_Re_Im_SComplex"; |
948 qed "Reals_Re_Im_SComplex"; |
952 |
949 |
953 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \ |
950 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \ |
954 \ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals & \ |
951 \ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals & \ |
955 \ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals)"; |
952 \ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals)"; |
985 eq_Abs_hcomplex_Bex,SComplex_SReal_iff,capprox_approx_iff])); |
982 eq_Abs_hcomplex_Bex,SComplex_SReal_iff,capprox_approx_iff])); |
986 by (REPEAT(dtac st_part_Ex 1 THEN Step_tac 1)); |
983 by (REPEAT(dtac st_part_Ex 1 THEN Step_tac 1)); |
987 by (res_inst_tac [("z","t")] eq_Abs_hypreal 1); |
984 by (res_inst_tac [("z","t")] eq_Abs_hypreal 1); |
988 by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1); |
985 by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1); |
989 by Auto_tac; |
986 by Auto_tac; |
990 by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")] |
987 by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1); |
991 exI 1); |
|
992 by Auto_tac; |
988 by Auto_tac; |
993 qed "stc_part_Ex"; |
989 qed "stc_part_Ex"; |
994 |
990 |
995 Goal "x:CFinite ==> EX! t. t : SComplex & x @c= t"; |
991 Goal "x:CFinite ==> EX! t. t : SComplex & x @c= t"; |
996 by (dtac stc_part_Ex 1 THEN Step_tac 1); |
992 by (dtac stc_part_Ex 1 THEN Step_tac 1); |