11 imports Complex |
11 imports Complex |
12 begin |
12 begin |
13 |
13 |
14 types hcomplex = "complex star" |
14 types hcomplex = "complex star" |
15 |
15 |
16 syntax hcomplex_of_complex :: "real => real star" |
16 abbreviation |
17 translations "hcomplex_of_complex" => "star_of :: complex => complex star" |
17 hcomplex_of_complex :: "complex => complex star" |
18 |
18 "hcomplex_of_complex == star_of" |
19 constdefs |
19 |
|
20 definition |
20 |
21 |
21 (*--- real and Imaginary parts ---*) |
22 (*--- real and Imaginary parts ---*) |
22 |
23 |
23 hRe :: "hcomplex => hypreal" |
24 hRe :: "hcomplex => hypreal" |
24 "hRe == *f* Re" |
25 "hRe = *f* Re" |
25 |
26 |
26 hIm :: "hcomplex => hypreal" |
27 hIm :: "hcomplex => hypreal" |
27 "hIm == *f* Im" |
28 "hIm = *f* Im" |
28 |
29 |
29 |
30 |
30 (*----------- modulus ------------*) |
31 (*----------- modulus ------------*) |
31 |
32 |
32 hcmod :: "hcomplex => hypreal" |
33 hcmod :: "hcomplex => hypreal" |
33 "hcmod == *f* cmod" |
34 "hcmod = *f* cmod" |
34 |
35 |
35 (*------ imaginary unit ----------*) |
36 (*------ imaginary unit ----------*) |
36 |
37 |
37 iii :: hcomplex |
38 iii :: hcomplex |
38 "iii == star_of ii" |
39 "iii = star_of ii" |
39 |
40 |
40 (*------- complex conjugate ------*) |
41 (*------- complex conjugate ------*) |
41 |
42 |
42 hcnj :: "hcomplex => hcomplex" |
43 hcnj :: "hcomplex => hcomplex" |
43 "hcnj == *f* cnj" |
44 "hcnj = *f* cnj" |
44 |
45 |
45 (*------------ Argand -------------*) |
46 (*------------ Argand -------------*) |
46 |
47 |
47 hsgn :: "hcomplex => hcomplex" |
48 hsgn :: "hcomplex => hcomplex" |
48 "hsgn == *f* sgn" |
49 "hsgn = *f* sgn" |
49 |
50 |
50 harg :: "hcomplex => hypreal" |
51 harg :: "hcomplex => hypreal" |
51 "harg == *f* arg" |
52 "harg = *f* arg" |
52 |
53 |
53 (* abbreviation for (cos a + i sin a) *) |
54 (* abbreviation for (cos a + i sin a) *) |
54 hcis :: "hypreal => hcomplex" |
55 hcis :: "hypreal => hcomplex" |
55 "hcis == *f* cis" |
56 "hcis = *f* cis" |
56 |
57 |
57 (*----- injection from hyperreals -----*) |
58 (*----- injection from hyperreals -----*) |
58 |
59 |
59 hcomplex_of_hypreal :: "hypreal => hcomplex" |
60 hcomplex_of_hypreal :: "hypreal => hcomplex" |
60 "hcomplex_of_hypreal == *f* complex_of_real" |
61 "hcomplex_of_hypreal = *f* complex_of_real" |
61 |
62 |
62 (* abbreviation for r*(cos a + i sin a) *) |
63 (* abbreviation for r*(cos a + i sin a) *) |
63 hrcis :: "[hypreal, hypreal] => hcomplex" |
64 hrcis :: "[hypreal, hypreal] => hcomplex" |
64 "hrcis == *f2* rcis" |
65 "hrcis = *f2* rcis" |
65 |
66 |
66 (*------------ e ^ (x + iy) ------------*) |
67 (*------------ e ^ (x + iy) ------------*) |
67 |
68 |
68 hexpi :: "hcomplex => hcomplex" |
69 hexpi :: "hcomplex => hcomplex" |
69 "hexpi == *f* expi" |
70 "hexpi = *f* expi" |
70 |
71 |
71 HComplex :: "[hypreal,hypreal] => hcomplex" |
72 HComplex :: "[hypreal,hypreal] => hcomplex" |
72 "HComplex == *f2* Complex" |
73 "HComplex = *f2* Complex" |
73 |
74 |
74 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) |
75 hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) |
75 "(z::hcomplex) hcpow (n::hypnat) == ( *f2* op ^) z n" |
76 "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
76 |
77 |
77 lemmas hcomplex_defs [transfer_unfold] = |
78 lemmas hcomplex_defs [transfer_unfold] = |
78 hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def |
79 hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def |
79 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
80 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
80 |
81 |
919 |
920 |
920 lemma hcomplex_number_of_hIm [simp]: |
921 lemma hcomplex_number_of_hIm [simp]: |
921 "hIm(number_of v :: hcomplex) = 0" |
922 "hIm(number_of v :: hcomplex) = 0" |
922 by (transfer, simp) |
923 by (transfer, simp) |
923 |
924 |
924 |
|
925 ML |
|
926 {* |
|
927 val iii_def = thm"iii_def"; |
|
928 |
|
929 val hRe = thm"hRe"; |
|
930 val hIm = thm"hIm"; |
|
931 val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff"; |
|
932 val hcomplex_hRe_zero = thm"hcomplex_hRe_zero"; |
|
933 val hcomplex_hIm_zero = thm"hcomplex_hIm_zero"; |
|
934 val hcomplex_hRe_one = thm"hcomplex_hRe_one"; |
|
935 val hcomplex_hIm_one = thm"hcomplex_hIm_one"; |
|
936 val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex"; |
|
937 val hcomplex_of_complex_i = thm"hcomplex_of_complex_i"; |
|
938 val star_n_add = thm"star_n_add"; |
|
939 val hRe_add = thm"hRe_add"; |
|
940 val hIm_add = thm"hIm_add"; |
|
941 val hRe_minus = thm"hRe_minus"; |
|
942 val hIm_minus = thm"hIm_minus"; |
|
943 val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus"; |
|
944 val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq"; |
|
945 val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one"; |
|
946 val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right"; |
|
947 val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel"; |
|
948 val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel"; |
|
949 val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib"; |
|
950 val hcomplex_of_hypreal = thm"hcomplex_of_hypreal"; |
|
951 val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff"; |
|
952 val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus"; |
|
953 val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse"; |
|
954 val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add"; |
|
955 val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff"; |
|
956 val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult"; |
|
957 val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide"; |
|
958 val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one"; |
|
959 val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero"; |
|
960 val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow"; |
|
961 val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal"; |
|
962 val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal"; |
|
963 val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero"; |
|
964 val hcmod = thm"hcmod"; |
|
965 val hcmod_zero = thm"hcmod_zero"; |
|
966 val hcmod_one = thm"hcmod_one"; |
|
967 val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal"; |
|
968 val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs"; |
|
969 val hcnj = thm"hcnj"; |
|
970 val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff"; |
|
971 val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj"; |
|
972 val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal"; |
|
973 val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj"; |
|
974 val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus"; |
|
975 val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse"; |
|
976 val hcomplex_hcnj_add = thm"hcomplex_hcnj_add"; |
|
977 val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff"; |
|
978 val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult"; |
|
979 val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide"; |
|
980 val hcnj_one = thm"hcnj_one"; |
|
981 val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow"; |
|
982 val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero"; |
|
983 val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff"; |
|
984 val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj"; |
|
985 val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel"; |
|
986 |
|
987 val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat"; |
|
988 val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat"; |
|
989 val hcmod_minus = thm"hcmod_minus"; |
|
990 val hcmod_mult_hcnj = thm"hcmod_mult_hcnj"; |
|
991 val hcmod_ge_zero = thm"hcmod_ge_zero"; |
|
992 val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel"; |
|
993 val hcmod_mult = thm"hcmod_mult"; |
|
994 val hcmod_add_squared_eq = thm"hcmod_add_squared_eq"; |
|
995 val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod"; |
|
996 val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2"; |
|
997 val hcmod_triangle_squared = thm"hcmod_triangle_squared"; |
|
998 val hcmod_triangle_ineq = thm"hcmod_triangle_ineq"; |
|
999 val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2"; |
|
1000 val hcmod_diff_commute = thm"hcmod_diff_commute"; |
|
1001 val hcmod_add_less = thm"hcmod_add_less"; |
|
1002 val hcmod_mult_less = thm"hcmod_mult_less"; |
|
1003 val hcmod_diff_ineq = thm"hcmod_diff_ineq"; |
|
1004 val hcpow = thm"hcpow"; |
|
1005 val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow"; |
|
1006 val hcmod_hcomplexpow = thm"hcmod_hcomplexpow"; |
|
1007 val hcmod_hcpow = thm"hcmod_hcpow"; |
|
1008 val hcpow_minus = thm"hcpow_minus"; |
|
1009 val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse"; |
|
1010 val hcmod_divide = thm"hcmod_divide"; |
|
1011 val hcpow_mult = thm"hcpow_mult"; |
|
1012 val hcpow_zero = thm"hcpow_zero"; |
|
1013 val hcpow_zero2 = thm"hcpow_zero2"; |
|
1014 val hcpow_not_zero = thm"hcpow_not_zero"; |
|
1015 val hcpow_zero_zero = thm"hcpow_zero_zero"; |
|
1016 val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq"; |
|
1017 val hcomplexpow_i_squared = thm"hcomplexpow_i_squared"; |
|
1018 val hcomplex_i_not_zero = thm"hcomplex_i_not_zero"; |
|
1019 val star_n_divide = thm"star_n_divide"; |
|
1020 val hsgn = thm"hsgn"; |
|
1021 val hsgn_zero = thm"hsgn_zero"; |
|
1022 val hsgn_one = thm"hsgn_one"; |
|
1023 val hsgn_minus = thm"hsgn_minus"; |
|
1024 val hsgn_eq = thm"hsgn_eq"; |
|
1025 val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2"; |
|
1026 val hcmod_i = thm"hcmod_i"; |
|
1027 val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2"; |
|
1028 val hRe_hsgn = thm"hRe_hsgn"; |
|
1029 val hIm_hsgn = thm"hIm_hsgn"; |
|
1030 val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff"; |
|
1031 val hRe_mult_i_eq = thm"hRe_mult_i_eq"; |
|
1032 val hIm_mult_i_eq = thm"hIm_mult_i_eq"; |
|
1033 val hcmod_mult_i = thm"hcmod_mult_i"; |
|
1034 val hcmod_mult_i2 = thm"hcmod_mult_i2"; |
|
1035 val harg = thm"harg"; |
|
1036 val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero"; |
|
1037 val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff"; |
|
1038 val complex_split_polar2 = thm"complex_split_polar2"; |
|
1039 val hcomplex_split_polar = thm"hcomplex_split_polar"; |
|
1040 val hcis = thm"hcis"; |
|
1041 val hcis_eq = thm"hcis_eq"; |
|
1042 val hrcis = thm"hrcis"; |
|
1043 val hrcis_Ex = thm"hrcis_Ex"; |
|
1044 val hRe_hcomplex_polar = thm"hRe_hcomplex_polar"; |
|
1045 val hRe_hrcis = thm"hRe_hrcis"; |
|
1046 val hIm_hcomplex_polar = thm"hIm_hcomplex_polar"; |
|
1047 val hIm_hrcis = thm"hIm_hrcis"; |
|
1048 val hcmod_complex_polar = thm"hcmod_complex_polar"; |
|
1049 val hcmod_hrcis = thm"hcmod_hrcis"; |
|
1050 val hcis_hrcis_eq = thm"hcis_hrcis_eq"; |
|
1051 val hrcis_mult = thm"hrcis_mult"; |
|
1052 val hcis_mult = thm"hcis_mult"; |
|
1053 val hcis_zero = thm"hcis_zero"; |
|
1054 val hrcis_zero_mod = thm"hrcis_zero_mod"; |
|
1055 val hrcis_zero_arg = thm"hrcis_zero_arg"; |
|
1056 val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus"; |
|
1057 val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2"; |
|
1058 val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult"; |
|
1059 val NSDeMoivre = thm"NSDeMoivre"; |
|
1060 val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult"; |
|
1061 val NSDeMoivre_ext = thm"NSDeMoivre_ext"; |
|
1062 val DeMoivre2 = thm"DeMoivre2"; |
|
1063 val DeMoivre2_ext = thm"DeMoivre2_ext"; |
|
1064 val hcis_inverse = thm"hcis_inverse"; |
|
1065 val hrcis_inverse = thm"hrcis_inverse"; |
|
1066 val hRe_hcis = thm"hRe_hcis"; |
|
1067 val hIm_hcis = thm"hIm_hcis"; |
|
1068 val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n"; |
|
1069 val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n"; |
|
1070 val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n"; |
|
1071 val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n"; |
|
1072 val hexpi_add = thm"hexpi_add"; |
|
1073 val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex"; |
|
1074 val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex"; |
|
1075 val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex"; |
|
1076 *} |
|
1077 |
|
1078 end |
925 end |