types complex and hcomplex are now instances of class ringpower:
omitting redundant lemmas
--- a/src/HOL/Complex/CLim.ML Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/CLim.ML Tue Jan 13 10:37:52 2004 +0100
@@ -1097,7 +1097,7 @@
\ ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
by (rtac (complex_mult_commute RS subst) 1);
by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
- complexpow_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
+ power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
complex_minus_mult_eq1 RS sym]) 1);
by (fold_goals_tac [o_def]);
by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
@@ -1127,7 +1127,7 @@
by (REPEAT(assume_tac 1));
by (asm_full_simp_tac
(simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
- complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac
+ power_inverse,complex_minus_mult_eq1] @ complex_mult_ac
delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
qed "CDERIV_quotient";
--- a/src/HOL/Complex/Complex.thy Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/Complex.thy Tue Jan 13 10:37:52 2004 +0100
@@ -51,7 +51,7 @@
"sgn z == z / complex_of_real(cmod z)"
arg :: "complex => real"
- "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a <= pi"
+ "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
defs (overloaded)
@@ -94,11 +94,6 @@
"w / (z::complex) == w * inverse z"
-primrec
- complexpow_0: "z ^ 0 = complex_of_real 1"
- complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
-
-
constdefs
(* abbreviation for (cos a + i sin a) *)
@@ -280,7 +275,7 @@
by (auto dest: sym)
declare complex_minus_zero_iff2 [simp]
-lemma complex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::complex))"
+lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))"
by auto
@@ -494,7 +489,7 @@
apply (simp (no_asm) add: complex_mult_commute)
done
-lemma complex_zero_not_eq_one: "(0::complex) ~= 1"
+lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1"
apply (unfold complex_zero_def complex_one_def)
apply (simp (no_asm) add: complex_Re_Im_cancel_iff)
done
@@ -504,8 +499,9 @@
subsection{*Inverse*}
-lemma complex_inverse: "inverse (Abs_complex(x,y)) =
- Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
+lemma complex_inverse:
+ "inverse (Abs_complex(x,y)) =
+ Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
apply (unfold complex_inverse_def)
apply (simp (no_asm))
done
@@ -524,7 +520,7 @@
show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO)
qed
-lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
+lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
apply (rule_tac z = z in eq_Abs_complex)
apply (auto simp add: complex_mult complex_inverse complex_one_def
complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
@@ -533,7 +529,7 @@
done
declare complex_mult_inv_left [simp]
-lemma complex_mult_inv_right: "z ~= (0::complex) ==> z * inverse(z) = 1"
+lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1"
by (auto intro: complex_mult_commute [THEN subst])
declare complex_mult_inv_right [simp]
@@ -641,11 +637,6 @@
apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
done
-lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_of_real_mult [symmetric])
-done
-
lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)"
apply (unfold cmod_def)
apply (simp (no_asm))
@@ -744,11 +735,6 @@
done
declare complex_cnj_one [simp]
-lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_cnj_mult)
-done
-
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
apply (rule_tac z = z in eq_Abs_complex)
apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def)
@@ -756,12 +742,12 @@
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
apply (rule_tac z = z in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def complex_diff_def complex_minus i_def complex_mult)
+apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
+ complex_minus i_def complex_mult)
done
-lemma complex_cnj_zero: "cnj 0 = 0"
+lemma complex_cnj_zero [simp]: "cnj 0 = 0"
by (simp add: cnj_def complex_zero_def)
-declare complex_cnj_zero [simp]
lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"
apply (rule_tac z = z in eq_Abs_complex)
@@ -826,7 +812,7 @@
lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
by (unfold cmod_def, auto)
-lemma complex_mod_ge_zero: "0 <= cmod x"
+lemma complex_mod_ge_zero: "0 \<le> cmod x"
apply (unfold cmod_def)
apply (auto intro: real_sqrt_ge_zero)
done
@@ -852,14 +838,14 @@
apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
done
-lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= cmod(x * cnj y)"
+lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"
apply (rule_tac z = x in eq_Abs_complex)
apply (rule_tac z = y in eq_Abs_complex)
apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
done
declare complex_Re_mult_cnj_le_cmod [simp]
-lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) <= cmod(x * y)"
+lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"
apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod)
apply (simp add: complex_mod_mult)
done
@@ -869,25 +855,25 @@
apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
done
-lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2"
+lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
done
declare complex_mod_triangle_squared [simp]
-lemma complex_mod_minus_le_complex_mod: "- cmod x <= cmod x"
+lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
apply (rule order_trans [OF _ complex_mod_ge_zero])
apply (simp (no_asm))
done
declare complex_mod_minus_le_complex_mod [simp]
-lemma complex_mod_triangle_ineq: "cmod (x + y) <= cmod(x) + cmod(y)"
+lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"
apply (rule_tac n = 1 in realpow_increasing)
apply (auto intro: order_trans [OF _ complex_mod_ge_zero]
simp add: power2_eq_square [symmetric])
done
declare complex_mod_triangle_ineq [simp]
-lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b <= cmod a"
+lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
apply (cut_tac x1 = b and y1 = a and c = "-cmod b"
in complex_mod_triangle_ineq [THEN add_right_mono])
apply (simp (no_asm))
@@ -906,7 +892,7 @@
lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)
-lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) <= cmod(a + b)"
+lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)"
apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])
apply auto
apply (rule order_trans [of _ 0], rule order_less_imp_le)
@@ -919,13 +905,13 @@
done
declare complex_mod_diff_ineq [simp]
-lemma complex_Re_le_cmod: "Re z <= cmod z"
+lemma complex_Re_le_cmod: "Re z \<le> cmod z"
apply (rule_tac z = z in eq_Abs_complex)
apply (auto simp add: complex_mod simp del: realpow_Suc)
done
declare complex_Re_le_cmod [simp]
-lemma complex_mod_gt_zero: "z ~= 0 ==> 0 < cmod z"
+lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
apply (cut_tac x = z in complex_mod_ge_zero)
apply (drule order_le_imp_less_or_eq, auto)
done
@@ -933,25 +919,6 @@
subsection{*A Few More Theorems*}
-lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_mod_mult)
-done
-
-lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-by (induct_tac "n", auto)
-
-lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)"
-apply (rule_tac z = x in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_inverse complex_minus power2_eq_square)
-done
-
-lemma complex_divide_one: "x / (1::complex) = x"
-apply (unfold complex_divide_def)
-apply (simp (no_asm))
-done
-declare complex_divide_one [simp]
-
lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"
apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO)
apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])
@@ -971,59 +938,51 @@
done
declare complex_inverse_divide [simp]
-lemma complexpow_mult: "((r::complex) * s) ^ n = (r ^ n) * (s ^ n)"
-apply (induct_tac "n")
-apply (auto simp add: complex_mult_ac)
-done
+
+subsection{*Exponentiation*}
+
+primrec
+ complexpow_0: "z ^ 0 = 1"
+ complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
+
+
+instance complex :: ringpower
+proof
+ fix z :: complex
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
-subsection{*More Exponentiation*}
-
-lemma complexpow_zero: "(0::complex) ^ (Suc n) = 0"
-by auto
-declare complexpow_zero [simp]
-
-lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0"
+lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
apply (induct_tac "n")
-apply (auto simp add: )
-done
-declare complexpow_not_zero [simp]
-declare complexpow_not_zero [intro]
-
-lemma complexpow_zero_zero: "r ^ n = (0::complex) ==> r = 0"
-by (blast intro: ccontr dest: complexpow_not_zero)
-
-lemma complexpow_i_squared: "ii ^ 2 = -(1::complex)"
-apply (unfold i_def)
-apply (auto simp add: complex_mult complex_one_def complex_minus numeral_2_eq_2)
+apply (auto simp add: complex_of_real_mult [symmetric])
done
-declare complexpow_i_squared [simp]
-lemma complex_i_not_zero: "ii ~= 0"
-by (unfold i_def complex_zero_def, auto)
-declare complex_i_not_zero [simp]
-
-lemma complex_mult_eq_zero_cancel1: "x * y ~= (0::complex) ==> x ~= 0"
-by auto
-
-lemma complex_mult_eq_zero_cancel2: "x * y ~= 0 ==> y ~= (0::complex)"
-by auto
-
-lemma complex_mult_not_eq_zero_iff: "(x * y ~= 0) = (x ~= 0 & y ~= (0::complex))"
-by auto
-declare complex_mult_not_eq_zero_iff [iff]
-
-lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n"
+lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
apply (induct_tac "n")
-apply (auto simp add: inverse_mult_distrib)
+apply (auto simp add: complex_cnj_mult)
done
-(*---------------------------------------------------------------------------*)
-(* sgn *)
-(*---------------------------------------------------------------------------*)
+lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: complex_mod_mult)
+done
+
+lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
+by (induct_tac "n", auto)
+
+lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
+by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
+
+lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
+by (unfold i_def complex_zero_def, auto)
+
+
+subsection{*The Function @{term sgn}*}
lemma sgn_zero: "sgn 0 = 0"
-
apply (unfold sgn_def)
apply (simp (no_asm))
done
@@ -1044,7 +1003,7 @@
apply (simp (no_asm))
done
-lemma complex_split: "EX x y. z = complex_of_real(x) + ii * complex_of_real(y)"
+lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
apply (rule_tac z = z in eq_Abs_complex)
apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
done
@@ -1184,6 +1143,9 @@
(* many of the theorems are not used - so should they be kept? *)
(*----------------------------------------------------------------------------*)
+lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
+by (auto simp add: complex_zero_def complex_of_real_def)
+
lemma Re_mult_i_eq:
"Re (ii * complex_of_real y) = 0"
apply (unfold i_def complex_of_real_def)
@@ -1205,50 +1167,37 @@
done
declare complex_mod_mult_i [simp]
-lemma cos_arg_i_mult_zero:
+lemma cos_arg_i_mult_zero_pos:
"0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
apply (unfold arg_def)
apply (auto simp add: abs_eqI2)
apply (rule_tac a = "pi/2" in someI2, auto)
apply (rule order_less_trans [of _ 0], auto)
done
-declare cos_arg_i_mult_zero [simp]
-lemma cos_arg_i_mult_zero2:
+lemma cos_arg_i_mult_zero_neg:
"y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
apply (unfold arg_def)
apply (auto simp add: abs_minus_eqI2)
apply (rule_tac a = "- pi/2" in someI2, auto)
apply (rule order_trans [of _ 0], auto)
done
-declare cos_arg_i_mult_zero2 [simp]
-lemma complex_of_real_not_zero_iff:
- "(complex_of_real y ~= 0) = (y ~= 0)"
-apply (unfold complex_zero_def complex_of_real_def, auto)
-done
-declare complex_of_real_not_zero_iff [simp]
-
-lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)"
-apply auto
-apply (rule ccontr, drule complex_of_real_not_zero_iff [THEN iffD2], simp)
-done
-declare complex_of_real_zero_iff [simp]
-
-lemma cos_arg_i_mult_zero3: "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0"
-by (cut_tac x = y and y = 0 in linorder_less_linear, auto)
-declare cos_arg_i_mult_zero3 [simp]
+lemma cos_arg_i_mult_zero [simp]
+ : "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
+by (cut_tac x = y and y = 0 in linorder_less_linear,
+ auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
subsection{*Finally! Polar Form for Complex Numbers*}
-lemma complex_split_polar: "EX r a. z = complex_of_real r *
+lemma complex_split_polar: "\<exists>r a. z = complex_of_real r *
(complex_of_real(cos a) + ii * complex_of_real(sin a))"
apply (cut_tac z = z in complex_split)
-apply (auto simp add: polar_Ex complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
+apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
done
-lemma rcis_Ex: "EX r a. z = rcis r a"
+lemma rcis_Ex: "\<exists>r a. z = rcis r a"
apply (unfold rcis_def cis_def)
apply (rule complex_split_polar)
done
@@ -1415,7 +1364,7 @@
lemma DeMoivre2:
"(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
apply (unfold rcis_def)
-apply (auto simp add: complexpow_mult DeMoivre complex_of_real_pow)
+apply (auto simp add: power_mult_distrib DeMoivre complex_of_real_pow)
done
lemma cis_inverse: "inverse(cis a) = cis (-a)"
@@ -1425,9 +1374,9 @@
declare cis_inverse [simp]
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-apply (case_tac "r=0")
-apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
-apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def power2_eq_square complex_mult_ac mult_ac)
+apply (case_tac "r=0", simp)
+apply (auto simp add: complex_inverse_complex_split right_distrib
+ complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac)
apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def)
done
@@ -1436,8 +1385,7 @@
apply (auto simp add: cis_mult real_diff_def)
done
-lemma rcis_divide:
- "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
+lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
apply (unfold complex_divide_def)
apply (case_tac "r2=0")
apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
@@ -1461,13 +1409,11 @@
lemma expi_Im_split:
"expi (ii * complex_of_real y) =
complex_of_real (cos y) + ii * complex_of_real (sin y)"
-apply (unfold expi_def cis_def, auto)
-done
+by (unfold expi_def cis_def, auto)
lemma expi_Im_cis:
"expi (ii * complex_of_real y) = cis y"
-apply (unfold expi_def, auto)
-done
+by (unfold expi_def, auto)
lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
apply (unfold expi_def)
@@ -1477,8 +1423,7 @@
lemma expi_complex_split:
"expi(complex_of_real x + ii * complex_of_real y) =
complex_of_real (exp(x)) * cis y"
-apply (unfold expi_def, auto)
-done
+by (unfold expi_def, auto)
lemma expi_zero: "expi (0::complex) = 1"
by (unfold expi_def, auto)
@@ -1498,7 +1443,7 @@
done
lemma complex_expi_Ex:
- "EX a r. z = complex_of_real r * expi a"
+ "\<exists>a r. z = complex_of_real r * expi a"
apply (cut_tac z = z in rcis_Ex)
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
@@ -1506,12 +1451,12 @@
(****
-Goal "[| - pi < a; a <= pi |] ==> (-pi < a & a <= 0) | (0 <= a & a <= pi)"
+Goal "[| - pi < a; a \<le> pi |] ==> (-pi < a & a \<le> 0) | (0 \<le> a & a \<le> pi)"
by Auto_tac
qed "lemma_split_interval";
Goalw [arg_def]
- "[| r ~= 0; - pi < a; a <= pi |] \
+ "[| r \<noteq> 0; - pi < a; a \<le> pi |] \
\ ==> arg(complex_of_real r * \
\ (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
by Auto_tac
@@ -1680,21 +1625,11 @@
val complex_mod_gt_zero = thm"complex_mod_gt_zero";
val complex_mod_complexpow = thm"complex_mod_complexpow";
val complexpow_minus = thm"complexpow_minus";
-val complex_inverse_minus = thm"complex_inverse_minus";
-val complex_divide_one = thm"complex_divide_one";
val complex_mod_inverse = thm"complex_mod_inverse";
val complex_mod_divide = thm"complex_mod_divide";
val complex_inverse_divide = thm"complex_inverse_divide";
-val complexpow_mult = thm"complexpow_mult";
-val complexpow_zero = thm"complexpow_zero";
-val complexpow_not_zero = thm"complexpow_not_zero";
-val complexpow_zero_zero = thm"complexpow_zero_zero";
val complexpow_i_squared = thm"complexpow_i_squared";
val complex_i_not_zero = thm"complex_i_not_zero";
-val complex_mult_eq_zero_cancel1 = thm"complex_mult_eq_zero_cancel1";
-val complex_mult_eq_zero_cancel2 = thm"complex_mult_eq_zero_cancel2";
-val complex_mult_not_eq_zero_iff = thm"complex_mult_not_eq_zero_iff";
-val complexpow_inverse = thm"complexpow_inverse";
val sgn_zero = thm"sgn_zero";
val sgn_one = thm"sgn_one";
val sgn_minus = thm"sgn_minus";
@@ -1724,10 +1659,7 @@
val Im_mult_i_eq = thm"Im_mult_i_eq";
val complex_mod_mult_i = thm"complex_mod_mult_i";
val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
-val cos_arg_i_mult_zero2 = thm"cos_arg_i_mult_zero2";
-val complex_of_real_not_zero_iff = thm"complex_of_real_not_zero_iff";
val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val cos_arg_i_mult_zero3 = thm"cos_arg_i_mult_zero3";
val complex_split_polar = thm"complex_split_polar";
val rcis_Ex = thm"rcis_Ex";
val Re_complex_polar = thm"Re_complex_polar";
--- a/src/HOL/Complex/NSComplex.thy Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy Tue Jan 13 10:37:52 2004 +0100
@@ -6,9 +6,6 @@
theory NSComplex = NSInduct:
-(*for Ring_and_Field?*)
-declare field_mult_eq_0_iff [simp]
-
(* Move to one of the hyperreal theories *)
lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
apply (induct_tac "m")
@@ -17,13 +14,13 @@
(* not proved already? strange! *)
lemma hypreal_of_nat_le_iff:
- "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
+ "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
apply (unfold hypreal_le_def)
apply auto
done
declare hypreal_of_nat_le_iff [simp]
-lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
+lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric]
del: hypreal_of_nat_zero)
done
@@ -31,7 +28,7 @@
declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
-lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
+lemma hypreal_of_hypnat_ge_zero: "0 \<le> hypreal_of_hypnat n"
apply (rule_tac z = "n" in eq_Abs_hypnat)
apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
done
@@ -40,7 +37,7 @@
constdefs
hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
- "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) &
+ "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
{n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
@@ -147,10 +144,6 @@
hcomplexrel `` {%n. X n * Y n})"
-primrec
- hcomplexpow_0: "z ^ 0 = 1"
- hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
-
consts
"hcpow" :: "[hcomplex,hypnat] => hcomplex" (infixr 80)
@@ -220,13 +213,13 @@
done
declare lemma_hcomplexrel_refl [simp]
-lemma hcomplex_empty_not_mem: "{} ~: hcomplex"
+lemma hcomplex_empty_not_mem: "{} \<notin> hcomplex"
apply (unfold hcomplex_def)
apply (auto elim!: quotientE)
done
declare hcomplex_empty_not_mem [simp]
-lemma Rep_hcomplex_nonempty: "Rep_hcomplex x ~= {}"
+lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \<noteq> {}"
apply (cut_tac x = "x" in Rep_hcomplex)
apply auto
done
@@ -290,23 +283,8 @@
done
declare hcomplex_hIm_one [simp]
-(*-----------------------------------------------------------------------*)
-(* hcomplex_of_complex: the injection from complex to hcomplex *)
-(* ----------------------------------------------------------------------*)
-lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
-apply (rule inj_onI , rule ccontr)
-apply (auto simp add: hcomplex_of_complex_def)
-done
-
-lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
-apply (unfold iii_def hcomplex_of_complex_def)
-apply (simp (no_asm))
-done
-
-(*-----------------------------------------------------------------------*)
-(* Addition for nonstandard complex numbers: hcomplex_add *)
-(* ----------------------------------------------------------------------*)
+subsection{*Addition for Nonstandard Complex Numbers*}
lemma hcomplex_add_congruent2:
"congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
@@ -358,9 +336,8 @@
apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
done
-(*-----------------------------------------------------------------------*)
-(* hypreal_minus: additive inverse on nonstandard complex *)
-(* ----------------------------------------------------------------------*)
+
+subsection{*Additive Inverse on Nonstandard Complex Numbers*}
lemma hcomplex_minus_congruent:
"congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
@@ -427,7 +404,7 @@
apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
done
-lemma hcomplex_zero_not_eq_one: "(0::hcomplex) ~= (1::hcomplex)"
+lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
apply (unfold hcomplex_zero_def hcomplex_one_def)
apply auto
done
@@ -446,7 +423,7 @@
done
lemma hcomplex_mult_inv_left:
- "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
+ "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
apply (unfold hcomplex_zero_def hcomplex_one_def)
apply (rule_tac z = "z" in eq_Abs_hcomplex)
apply (auto simp add: hcomplex_inverse hcomplex_mult)
@@ -553,11 +530,11 @@
declare hcomplex_mult_minus_one_right [simp]
lemma hcomplex_mult_left_cancel:
- "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
+ "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
by (simp add: field_mult_cancel_left)
lemma hcomplex_mult_right_cancel:
- "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
+ "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
apply (simp add: Ring_and_Field.field_mult_cancel_right);
done
@@ -661,12 +638,6 @@
apply (auto simp add: hcomplex_of_hypreal)
done
-lemma hcomplex_of_hypreal_pow:
- "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
-done
-
lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
apply (rule_tac z = "z" in eq_Abs_hypreal)
apply (auto simp add: hcomplex_of_hypreal hRe)
@@ -679,7 +650,7 @@
done
declare hIm_hcomplex_of_hypreal [simp]
-lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon ~= 0"
+lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \<noteq> 0"
apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
done
declare hcomplex_of_hypreal_epsilon_not_zero [simp]
@@ -802,10 +773,6 @@
done
declare hcnj_one [simp]
-lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_hcnj_mult)
-done
(* MOVE to NSComplexBin
Goal "z + hcnj z =
@@ -844,9 +811,7 @@
done
-(*---------------------------------------------------------------------------*)
-(* More theorems about hcmod *)
-(*---------------------------------------------------------------------------*)
+subsection{*More Theorems about the Function @{term hcmod}*}
lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
@@ -877,7 +842,7 @@
apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
done
-lemma hcmod_ge_zero: "(0::hypreal) <= hcmod x"
+lemma hcmod_ge_zero: "(0::hypreal) \<le> hcmod x"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
done
@@ -906,20 +871,20 @@
hypreal_of_real_def [symmetric])
done
-lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) <= hcmod(x * hcnj y)"
+lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
apply (rule_tac z = "y" in eq_Abs_hcomplex)
apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
done
declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
-lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) <= hcmod(x * y)"
+lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \<le> hcmod(x * y)"
apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
apply (simp add: hcmod_mult)
done
declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
-lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 <= (hcmod(x) + hcmod(y)) ^ 2"
+lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
apply (rule_tac z = "y" in eq_Abs_hcomplex)
apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
@@ -929,14 +894,14 @@
done
declare hcmod_triangle_squared [simp]
-lemma hcmod_triangle_ineq: "hcmod (x + y) <= hcmod(x) + hcmod(y)"
+lemma hcmod_triangle_ineq: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
apply (rule_tac z = "y" in eq_Abs_hcomplex)
apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
done
declare hcmod_triangle_ineq [simp]
-lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a"
+lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \<le> hcmod a"
apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
apply (simp add: add_ac)
done
@@ -970,7 +935,7 @@
apply (auto intro: complex_mod_mult_less)
done
-lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) <= hcmod(a + b)"
+lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
apply (rule_tac z = "a" in eq_Abs_hcomplex)
apply (rule_tac z = "b" in eq_Abs_hcomplex)
apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
@@ -997,45 +962,12 @@
apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
done
-lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcmod_mult)
-done
-
lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
apply (rule_tac z = "x" in eq_Abs_hcomplex)
apply (rule_tac z = "n" in eq_Abs_hypnat)
apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
done
-lemma hcomplexpow_minus:
- "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-apply (induct_tac "n")
-apply auto
-done
-
-lemma hcpow_minus:
- "(-x::hcomplex) hcpow n =
- (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
-apply (rule_tac z = "x" in eq_Abs_hcomplex)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
-apply ultra
-apply (auto simp add: complexpow_minus)
-apply ultra
-done
-
-lemma hccomplex_inverse_minus: "inverse(-x) = - inverse (x::hcomplex)"
-apply (rule_tac z = "x" in eq_Abs_hcomplex)
-apply (auto simp add: hcomplex_inverse hcomplex_minus complex_inverse_minus)
-done
-
-lemma hcomplex_div_one: "x / (1::hcomplex) = x"
-apply (unfold hcomplex_divide_def)
-apply (simp (no_asm))
-done
-declare hcomplex_div_one [simp]
-
lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
@@ -1055,58 +987,78 @@
done
declare hcomplex_inverse_divide [simp]
-lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"
+
+subsection{*Exponentiation*}
+
+primrec
+ hcomplexpow_0: "z ^ 0 = 1"
+ hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
+
+instance hcomplex :: ringpower
+proof
+ fix z :: hcomplex
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
+
+
+lemma hcomplex_of_hypreal_pow:
+ "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
+done
+
+lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
apply (induct_tac "n")
-apply (auto simp add: mult_ac)
+apply (auto simp add: hcomplex_hcnj_mult)
+done
+
+lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: hcmod_mult)
+done
+
+lemma hcomplexpow_minus:
+ "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
+apply (induct_tac "n")
+apply auto
+done
+
+lemma hcpow_minus:
+ "(-x::hcomplex) hcpow n =
+ (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
+apply (rule_tac z = "x" in eq_Abs_hcomplex)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
+apply ultra
+apply (auto simp add: complexpow_minus)
+apply ultra
done
lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
apply (rule_tac z = "r" in eq_Abs_hcomplex)
apply (rule_tac z = "s" in eq_Abs_hcomplex)
apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (auto simp add: hcpow hypreal_mult hcomplex_mult complexpow_mult)
+apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
done
-lemma hcomplexpow_zero: "(0::hcomplex) ^ (Suc n) = 0"
-apply auto
-done
-declare hcomplexpow_zero [simp]
-
-lemma hcpow_zero:
- "0 hcpow (n + 1) = 0"
+lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
apply (unfold hcomplex_zero_def hypnat_one_def)
apply (rule_tac z = "n" in eq_Abs_hypnat)
apply (auto simp add: hcpow hypnat_add)
done
-declare hcpow_zero [simp]
-lemma hcpow_zero2:
- "0 hcpow (hSuc n) = 0"
+lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
apply (unfold hSuc_def)
apply (simp (no_asm))
done
-declare hcpow_zero2 [simp]
-lemma hcomplexpow_not_zero [rule_format (no_asm)]:
- "r ~= (0::hcomplex) --> r ^ n ~= 0"
-apply (induct_tac "n")
-apply (auto)
-done
-declare hcomplexpow_not_zero [simp]
-declare hcomplexpow_not_zero [intro]
-
-lemma hcpow_not_zero: "r ~= 0 ==> r hcpow n ~= (0::hcomplex)"
+lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
apply (rule_tac z = "r" in eq_Abs_hcomplex)
apply (rule_tac z = "n" in eq_Abs_hypnat)
apply (auto simp add: hcpow hcomplex_zero_def)
apply ultra
-apply (auto dest: complexpow_zero_zero)
-done
-declare hcpow_not_zero [simp]
-declare hcpow_not_zero [intro]
-
-lemma hcomplexpow_zero_zero: "r ^ n = (0::hcomplex) ==> r = 0"
-apply (blast intro: ccontr dest: hcomplexpow_not_zero)
done
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
@@ -1124,26 +1076,12 @@
done
declare hcomplexpow_i_squared [simp]
-lemma hcomplex_i_not_zero: "iii ~= 0"
+lemma hcomplex_i_not_zero: "iii \<noteq> 0"
apply (unfold iii_def hcomplex_zero_def)
apply auto
done
declare hcomplex_i_not_zero [simp]
-lemma hcomplex_mult_eq_zero_cancel1: "x * y ~= (0::hcomplex) ==> x ~= 0"
-apply auto
-done
-
-lemma hcomplex_mult_eq_zero_cancel2: "x * y ~= (0::hcomplex) ==> y ~= 0"
-apply auto
-done
-
-lemma hcomplex_mult_not_eq_zero_iff:
- "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
-apply auto
-done
-declare hcomplex_mult_not_eq_zero_iff [iff]
-
lemma hcomplex_divide:
"Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
@@ -1186,8 +1124,8 @@
done
lemma lemma_hypreal_P_EX2:
- "(EX (x::hypreal) y. P x y) =
- (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
+ "(\<exists>(x::hypreal) y. P x y) =
+ (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
apply auto
apply (rule_tac z = "x" in eq_Abs_hypreal)
apply (rule_tac z = "y" in eq_Abs_hypreal)
@@ -1195,13 +1133,13 @@
done
lemma complex_split2:
- "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
+ "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
apply (blast intro: complex_split)
done
(* Interesting proof! *)
lemma hcomplex_split:
- "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
+ "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
apply (rule_tac z = "z" in eq_Abs_hcomplex)
apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
apply (cut_tac z = "x" in complex_split2)
@@ -1409,54 +1347,45 @@
apply (auto, ultra)
done
-lemma cos_harg_i_mult_zero:
+lemma cos_harg_i_mult_zero_pos:
"0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
+apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
+ hypreal_zero_num hypreal_less starfun harg)
apply (ultra)
done
-declare cos_harg_i_mult_zero [simp]
-lemma cos_harg_i_mult_zero2:
+lemma cos_harg_i_mult_zero_neg:
"y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
+apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
+ hypreal_zero_num hypreal_less starfun harg)
apply (ultra)
done
-declare cos_harg_i_mult_zero2 [simp]
-lemma hcomplex_of_hypreal_not_zero_iff:
- "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
+lemma cos_harg_i_mult_zero [simp]:
+ "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
+apply (cut_tac x = "y" and y = "0" in hypreal_linear)
+apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
+done
+
+lemma hcomplex_of_hypreal_zero_iff [simp]:
+ "(hcomplex_of_hypreal y = 0) = (y = 0)"
apply (rule_tac z = "y" in eq_Abs_hypreal)
apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
done
-declare hcomplex_of_hypreal_not_zero_iff [simp]
-lemma hcomplex_of_hypreal_zero_iff: "(hcomplex_of_hypreal y = 0) = (y = 0)"
-apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
-done
-declare hcomplex_of_hypreal_zero_iff [simp]
-lemma cos_harg_i_mult_zero3:
- "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
-apply (cut_tac x = "y" and y = "0" in hypreal_linear)
-apply auto
-done
-declare cos_harg_i_mult_zero3 [simp]
-
-(*---------------------------------------------------------------------------*)
-(* Polar form for nonstandard complex numbers *)
-(*---------------------------------------------------------------------------*)
+subsection{*Polar Form for Nonstandard Complex Numbers*}
lemma complex_split_polar2:
- "ALL n. EX r a. (z n) = complex_of_real r *
+ "\<forall>n. \<exists>r a. (z n) = complex_of_real r *
(complex_of_real(cos a) + ii * complex_of_real(sin a))"
apply (blast intro: complex_split_polar)
done
lemma hcomplex_split_polar:
- "EX r a. z = hcomplex_of_hypreal r *
+ "\<exists>r a. z = hcomplex_of_hypreal r *
(hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
apply (rule_tac z = "z" in eq_Abs_hcomplex)
apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
@@ -1491,7 +1420,7 @@
apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
done
-lemma hrcis_Ex: "EX r a. z = hrcis r a"
+lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
apply (simp (no_asm) add: hrcis_def hcis_eq)
apply (rule hcomplex_split_polar)
done
@@ -1627,7 +1556,7 @@
lemma DeMoivre2:
"(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
apply (unfold hrcis_def)
-apply (auto simp add: hcomplexpow_mult NSDeMoivre hcomplex_of_hypreal_pow)
+apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
done
lemma DeMoivre2_ext:
@@ -1691,7 +1620,18 @@
done
-subsection{*@{term hcomplex_of_complex} Preserves Field Properties*}
+subsection{*@{term hcomplex_of_complex}: the Injection from
+ type @{typ complex} to to @{typ hcomplex}*}
+
+lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
+apply (rule inj_onI , rule ccontr)
+apply (auto simp add: hcomplex_of_complex_def)
+done
+
+lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
+apply (unfold iii_def hcomplex_of_complex_def)
+apply (simp (no_asm))
+done
lemma hcomplex_of_complex_add:
"hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
@@ -1905,26 +1845,17 @@
val hcmod_hcpow = thm"hcmod_hcpow";
val hcomplexpow_minus = thm"hcomplexpow_minus";
val hcpow_minus = thm"hcpow_minus";
-val hccomplex_inverse_minus = thm"hccomplex_inverse_minus";
-val hcomplex_div_one = thm"hcomplex_div_one";
val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
val hcmod_divide = thm"hcmod_divide";
val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
-val hcomplexpow_mult = thm"hcomplexpow_mult";
val hcpow_mult = thm"hcpow_mult";
-val hcomplexpow_zero = thm"hcomplexpow_zero";
val hcpow_zero = thm"hcpow_zero";
val hcpow_zero2 = thm"hcpow_zero2";
-val hcomplexpow_not_zero = thm"hcomplexpow_not_zero";
val hcpow_not_zero = thm"hcpow_not_zero";
-val hcomplexpow_zero_zero = thm"hcomplexpow_zero_zero";
val hcpow_zero_zero = thm"hcpow_zero_zero";
val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
-val hcomplex_mult_eq_zero_cancel1 = thm"hcomplex_mult_eq_zero_cancel1";
-val hcomplex_mult_eq_zero_cancel2 = thm"hcomplex_mult_eq_zero_cancel2";
-val hcomplex_mult_not_eq_zero_iff = thm"hcomplex_mult_not_eq_zero_iff";
val hcomplex_divide = thm"hcomplex_divide";
val hsgn = thm"hsgn";
val hsgn_zero = thm"hsgn_zero";
@@ -1959,10 +1890,7 @@
val hcmod_mult_i2 = thm"hcmod_mult_i2";
val harg = thm"harg";
val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
-val cos_harg_i_mult_zero2 = thm"cos_harg_i_mult_zero2";
-val hcomplex_of_hypreal_not_zero_iff = thm"hcomplex_of_hypreal_not_zero_iff";
val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
-val cos_harg_i_mult_zero3 = thm"cos_harg_i_mult_zero3";
val complex_split_polar2 = thm"complex_split_polar2";
val hcomplex_split_polar = thm"hcomplex_split_polar";
val hcis = thm"hcis";