--- a/src/HOL/Complex/CStar.ML Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/CStar.ML Thu Feb 05 10:45:28 2004 +0100
@@ -194,7 +194,7 @@
Goalw [congruent_def]
"congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
by (ALLGOALS(Ultra_tac));
qed "starfunC_congruent";
@@ -203,7 +203,7 @@
"( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
\ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
by (Ultra_tac 1);
qed "starfunC";
@@ -219,7 +219,7 @@
"( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
\ Abs_hypreal(hyprel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
by (Ultra_tac 1);
qed "starfunCR";
@@ -523,7 +523,7 @@
Goalw [congruent_def]
"congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
by (ALLGOALS(Fuf_tac));
qed "starfunC_n_congruent";
@@ -531,7 +531,7 @@
"( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
\ Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})";
by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
by (Ultra_tac 1);
qed "starfunC_n";
--- a/src/HOL/Complex/Complex.thy Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/Complex.thy Thu Feb 05 10:45:28 2004 +0100
@@ -3,12 +3,10 @@
Copyright: 2001 University of Edinburgh
*)
-header {* Complex numbers *}
+header {* Complex Numbers: Rectangular and Polar Representations *}
theory Complex = HLog:
-subsection {* Representation of complex numbers *}
-
datatype complex = Complex real real
instance complex :: zero ..
@@ -89,7 +87,7 @@
(* abbreviation for (cos a + i sin a) *)
cis :: "real => complex"
- "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"
+ "cis a == Complex (cos a) (sin a)"
(* abbreviation for r*(cos a + i sin a) *)
rcis :: "[real, real] => complex"
@@ -139,7 +137,7 @@
subsection{*Unary Minus*}
-lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)"
+lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)"
by (simp add: complex_minus_def)
lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
@@ -151,7 +149,8 @@
subsection{*Addition*}
-lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
+lemma complex_add [simp]:
+ "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
by (simp add: complex_add_def)
lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
@@ -188,7 +187,7 @@
subsection{*Multiplication*}
-lemma complex_mult:
+lemma complex_mult [simp]:
"Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
by (simp add: complex_mult_def)
@@ -208,7 +207,7 @@
subsection{*Inverse*}
-lemma complex_inverse:
+lemma complex_inverse [simp]:
"inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
by (simp add: complex_inverse_def)
@@ -272,6 +271,28 @@
subsection{*Embedding Properties for @{term complex_of_real} Map*}
+lemma Complex_add_complex_of_real [simp]:
+ "Complex x y + complex_of_real r = Complex (x+r) y"
+by (simp add: complex_of_real_def)
+
+lemma complex_of_real_add_Complex [simp]:
+ "complex_of_real r + Complex x y = Complex (r+x) y"
+by (simp add: i_def complex_of_real_def)
+
+lemma Complex_mult_complex_of_real:
+ "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
+by (simp add: complex_of_real_def)
+
+lemma complex_of_real_mult_Complex:
+ "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
+by (simp add: i_def complex_of_real_def)
+
+lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
+by (simp add: i_def complex_of_real_def)
+
+lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
+by (simp add: i_def complex_of_real_def)
+
lemma complex_of_real_one [simp]: "complex_of_real 1 = 1"
by (simp add: complex_one_def complex_of_real_def)
@@ -313,7 +334,7 @@
real_divide_def)
done
-lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
+lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
by (simp add: cmod_def)
lemma complex_mod_zero [simp]: "cmod(0) = 0"
@@ -330,6 +351,46 @@
by simp
+subsection{*The Functions @{term Re} and @{term Im}*}
+
+lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
+by (induct z, induct w, simp add: complex_mult)
+
+lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z"
+by (induct z, induct w, simp add: complex_mult)
+
+lemma Re_i_times [simp]: "Re(ii * z) = - Im z"
+by (simp add: complex_Re_mult_eq)
+
+lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
+by (simp add: complex_Re_mult_eq)
+
+lemma Im_i_times [simp]: "Im(ii * z) = Re z"
+by (simp add: complex_Im_mult_eq)
+
+lemma Im_times_i [simp]: "Im(z * ii) = Re z"
+by (simp add: complex_Im_mult_eq)
+
+lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Re_mult_complex_of_real [simp]:
+ "Re (z * complex_of_real c) = Re(z) * c"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Im_mult_complex_of_real [simp]:
+ "Im (z * complex_of_real c) = Im(z) * c"
+by (simp add: complex_Im_mult_eq)
+
+lemma complex_Re_mult_complex_of_real2 [simp]:
+ "Re (complex_of_real c * z) = c * Re(z)"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Im_mult_complex_of_real2 [simp]:
+ "Im (complex_of_real c * z) = c * Im(z)"
+by (simp add: complex_Im_mult_eq)
+
+
subsection{*Conjugation is an Automorphism*}
lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
@@ -420,14 +481,20 @@
lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
apply (induct x, induct y)
-apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric]
- simp del: realpow_Suc)
+apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric])
apply (rule_tac n = 1 in power_inject_base)
apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib
add_ac mult_ac)
done
+lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
+by (simp add: cmod_def)
+
+lemma cmod_complex_polar [simp]:
+ "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
+by (simp only: cmod_unit_one complex_mod_mult, simp)
+
lemma complex_mod_add_squared_eq:
"cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
apply (induct x, induct y)
@@ -506,10 +573,7 @@
done
lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
-by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse)
-
-lemma complex_inverse_divide [simp]: "inverse(x/y) = y/(x::complex)"
-by (simp add: complex_divide_def inverse_mult_distrib mult_commute)
+by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
subsection{*Exponentiation*}
@@ -566,20 +630,7 @@
by (simp add: sgn_def)
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
-apply (simp add: sgn_def)
-done
-
-lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
-apply (induct z)
-apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
-done
-
-(*????delete????*)
-lemma Re_complex_i [simp]: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
-by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
-
-lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
-by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
+by (simp add: sgn_def)
lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
by (simp add: i_def complex_of_real_def complex_mult complex_add)
@@ -587,78 +638,22 @@
lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
by (simp add: i_def complex_one_def complex_mult complex_minus)
-lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
- sqrt (x ^ 2 + y ^ 2)"
-by (simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
-
-lemma complex_eq_Re_eq:
- "complex_of_real xa + ii * complex_of_real ya =
- complex_of_real xb + ii * complex_of_real yb
- ==> xa = xb"
-by (simp add: complex_of_real_def i_def complex_mult complex_add)
-
-lemma complex_eq_Im_eq:
- "complex_of_real xa + ii * complex_of_real ya =
- complex_of_real xb + ii * complex_of_real yb
- ==> ya = yb"
-by (simp add: complex_of_real_def i_def complex_mult complex_add)
-
-(*FIXME: tidy up this mess by fixing a canonical form for complex expressions,
-e.g. x + y*ii*)
-
-lemma complex_eq_cancel_iff [iff]:
- "(complex_of_real xa + ii * complex_of_real ya =
- complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
-by (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
-
-lemma complex_eq_cancel_iffA [iff]:
- "(complex_of_real xa + complex_of_real ya * ii =
- complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
-by (simp add: mult_commute)
-
-lemma complex_eq_cancel_iffB [iff]:
- "(complex_of_real xa + complex_of_real ya * ii =
- complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
-by (auto simp add: mult_commute)
-
-lemma complex_eq_cancel_iffC [iff]:
- "(complex_of_real xa + ii * complex_of_real ya =
- complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
-by (auto simp add: mult_commute)
-
lemma complex_eq_cancel_iff2 [simp]:
- "(complex_of_real x + ii * complex_of_real y =
- complex_of_real xa) = (x = xa & y = 0)"
-apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff)
-apply (simp del: complex_eq_cancel_iff)
-done
+ "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
+by (simp add: complex_of_real_def)
lemma complex_eq_cancel_iff2a [simp]:
- "(complex_of_real x + complex_of_real y * ii =
- complex_of_real xa) = (x = xa & y = 0)"
-by (auto simp add: mult_commute)
+ "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
+by (simp add: complex_of_real_def)
-lemma complex_eq_cancel_iff3 [simp]:
- "(complex_of_real x + ii * complex_of_real y =
- ii * complex_of_real ya) = (x = 0 & y = ya)"
-apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff)
-apply (simp del: complex_eq_cancel_iff)
-done
+lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
+by (simp add: complex_zero_def)
-lemma complex_eq_cancel_iff3a [simp]:
- "(complex_of_real x + complex_of_real y * ii =
- ii * complex_of_real ya) = (x = 0 & y = ya)"
-by (auto simp add: mult_commute)
+lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
+by (simp add: complex_one_def)
-lemma complex_split_Re_zero:
- "complex_of_real x + ii * complex_of_real y = 0
- ==> x = 0"
-by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
-
-lemma complex_split_Im_zero:
- "complex_of_real x + ii * complex_of_real y = 0
- ==> y = 0"
-by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
+lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
+by (simp add: i_def)
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
apply (induct z)
@@ -687,77 +682,53 @@
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 [simp]: "Re (ii * complex_of_real y) = 0"
-by (simp add: i_def complex_of_real_def complex_mult)
-
-lemma Im_mult_i_eq [simp]: "Im (ii * complex_of_real y) = y"
-by (simp add: i_def complex_of_real_def complex_mult)
-
-lemma complex_mod_mult_i [simp]: "cmod (ii * complex_of_real y) = abs y"
-by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square)
-
lemma cos_arg_i_mult_zero_pos:
- "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
+ "0 < y ==> cos (arg(Complex 0 y)) = 0"
apply (simp add: arg_def abs_if)
apply (rule_tac a = "pi/2" in someI2, auto)
apply (rule order_less_trans [of _ 0], auto)
done
lemma cos_arg_i_mult_zero_neg:
- "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
+ "y < 0 ==> cos (arg(Complex 0 y)) = 0"
apply (simp add: arg_def abs_if)
apply (rule_tac a = "- pi/2" in someI2, auto)
apply (rule order_trans [of _ 0], auto)
done
lemma cos_arg_i_mult_zero [simp]:
- "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
-apply (insert linorder_less_linear [of y 0])
-apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
-done
+ "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
+by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
subsection{*Finally! Polar Form for Complex Numbers*}
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 right_distrib complex_of_real_mult mult_ac)
+ "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
+apply (induct z)
+apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
done
lemma rcis_Ex: "\<exists>r a. z = rcis r a"
-apply (simp add: rcis_def cis_def)
-apply (rule complex_split_polar)
+apply (induct z)
+apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
done
-lemma Re_complex_polar [simp]:
- "Re(complex_of_real r *
- (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
-by (auto simp add: right_distrib complex_of_real_mult mult_ac)
-
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
by (simp add: rcis_def cis_def)
-lemma Im_complex_polar [simp]:
- "Im(complex_of_real r *
- (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
- r * sin a"
-by (auto simp add: right_distrib complex_of_real_mult mult_ac)
-
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
by (simp add: rcis_def cis_def)
-lemma complex_mod_complex_polar [simp]:
- "cmod (complex_of_real r *
- (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
- abs r"
-by (auto simp add: right_distrib cmod_i complex_of_real_mult
- right_distrib [symmetric] power_mult_distrib mult_ac
- simp del: realpow_Suc)
+lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
+proof -
+ have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
+ by (simp only: power_mult_distrib right_distrib)
+ thus ?thesis by simp
+qed
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
-by (simp add: rcis_def cis_def)
+by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
apply (simp add: cmod_def)
@@ -774,24 +745,6 @@
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
by (induct z, simp add: complex_cnj complex_mult)
-lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
-by (induct z, induct w, simp add: complex_mult)
-
-lemma complex_Re_mult_complex_of_real [simp]:
- "Re (z * complex_of_real c) = Re(z) * c"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Im_mult_complex_of_real [simp]:
- "Im (z * complex_of_real c) = Im(z) * c"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Re_mult_complex_of_real2 [simp]:
- "Re (complex_of_real c * z) = c * Re(z)"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Im_mult_complex_of_real2 [simp]:
- "Im (complex_of_real c * z) = c * Im(z)"
-by (induct z, simp add: complex_of_real_def complex_mult)
(*---------------------------------------------------------------------------*)
(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *)
@@ -801,21 +754,13 @@
by (simp add: rcis_def)
lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib
- mult_ac add_ac)
-apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2)
-apply (auto simp add: add_ac)
-apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac)
-done
+by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
lemma cis_mult: "cis a * cis b = cis (a + b)"
by (simp add: cis_rcis_eq rcis_mult)
lemma cis_zero [simp]: "cis 0 = 1"
-by (simp add: cis_def)
-
-lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1"
-by (simp add: cis_def)
+by (simp add: cis_def complex_one_def)
lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
by (simp add: rcis_def)
@@ -825,8 +770,7 @@
lemma complex_of_real_minus_one:
"complex_of_real (-(1::real)) = -(1::complex)"
-apply (simp add: complex_of_real_def complex_one_def complex_minus)
-done
+by (simp add: complex_of_real_def complex_one_def complex_minus)
lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
by (simp add: complex_mult_assoc [symmetric])
@@ -834,10 +778,7 @@
lemma cis_real_of_nat_Suc_mult:
"cis (real (Suc n) * a) = cis a * cis (real n * a)"
-apply (simp add: cis_def)
-apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add left_distrib right_distrib complex_of_real_add complex_of_real_mult mult_ac add_ac)
-apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2)
-done
+by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
apply (induct_tac "n")
@@ -852,12 +793,7 @@
complex_diff_def)
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-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
+by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
lemma cis_divide: "cis a / cis b = cis (a - b)"
by (simp add: complex_divide_def cis_mult real_diff_def)
@@ -880,35 +816,13 @@
lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
by (auto simp add: DeMoivre)
-lemma expi_Im_split:
- "expi (ii * complex_of_real y) =
- complex_of_real (cos y) + ii * complex_of_real (sin y)"
-by (simp add: expi_def cis_def)
-
-lemma expi_Im_cis:
- "expi (ii * complex_of_real y) = cis y"
-by (simp add: expi_def)
-
lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
by (simp add: expi_def complex_Re_add exp_add complex_Im_add
cis_mult [symmetric] complex_of_real_mult mult_ac)
-lemma expi_complex_split:
- "expi(complex_of_real x + ii * complex_of_real y) =
- complex_of_real (exp(x)) * cis y"
-by (simp add: expi_def)
-
lemma expi_zero [simp]: "expi (0::complex) = 1"
by (simp add: expi_def)
-lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
-by (induct z, induct w, simp add: complex_mult)
-
-lemma complex_Im_mult_eq:
- "Im (w * z) = Re w * Im z + Im w * Re z"
-apply (induct z, induct w, simp add: complex_mult)
-done
-
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
apply (insert rcis_Ex [of z])
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
@@ -1023,46 +937,22 @@
val complexpow_minus = thm"complexpow_minus";
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_i_squared = thm"complexpow_i_squared";
val complex_i_not_zero = thm"complex_i_not_zero";
val sgn_zero = thm"sgn_zero";
val sgn_one = thm"sgn_one";
val sgn_minus = thm"sgn_minus";
val sgn_eq = thm"sgn_eq";
-val complex_split = thm"complex_split";
-val Re_complex_i = thm"Re_complex_i";
-val Im_complex_i = thm"Im_complex_i";
val i_mult_eq = thm"i_mult_eq";
val i_mult_eq2 = thm"i_mult_eq2";
-val cmod_i = thm"cmod_i";
-val complex_eq_Re_eq = thm"complex_eq_Re_eq";
-val complex_eq_Im_eq = thm"complex_eq_Im_eq";
-val complex_eq_cancel_iff = thm"complex_eq_cancel_iff";
-val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA";
-val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB";
-val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC";
-val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2";
-val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a";
-val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3";
-val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a";
-val complex_split_Re_zero = thm"complex_split_Re_zero";
-val complex_split_Im_zero = thm"complex_split_Im_zero";
val Re_sgn = thm"Re_sgn";
val Im_sgn = thm"Im_sgn";
val complex_inverse_complex_split = thm"complex_inverse_complex_split";
-val Re_mult_i_eq = thm"Re_mult_i_eq";
-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 complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val complex_split_polar = thm"complex_split_polar";
val rcis_Ex = thm"rcis_Ex";
-val Re_complex_polar = thm"Re_complex_polar";
val Re_rcis = thm"Re_rcis";
-val Im_complex_polar = thm"Im_complex_polar";
val Im_rcis = thm"Im_rcis";
-val complex_mod_complex_polar = thm"complex_mod_complex_polar";
val complex_mod_rcis = thm"complex_mod_rcis";
val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
val complex_Re_cnj = thm"complex_Re_cnj";
@@ -1077,7 +967,6 @@
val rcis_mult = thm"rcis_mult";
val cis_mult = thm"cis_mult";
val cis_zero = thm"cis_zero";
-val cis_zero2 = thm"cis_zero2";
val rcis_zero_mod = thm"rcis_zero_mod";
val rcis_zero_arg = thm"rcis_zero_arg";
val complex_of_real_minus_one = thm"complex_of_real_minus_one";
@@ -1093,10 +982,7 @@
val Im_cis = thm"Im_cis";
val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
-val expi_Im_split = thm"expi_Im_split";
-val expi_Im_cis = thm"expi_Im_cis";
val expi_add = thm"expi_add";
-val expi_complex_split = thm"expi_complex_split";
val expi_zero = thm"expi_zero";
val complex_Re_mult_eq = thm"complex_Re_mult_eq";
val complex_Im_mult_eq = thm"complex_Im_mult_eq";
--- a/src/HOL/Complex/ComplexBin.ML Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/ComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
@@ -367,9 +367,9 @@
val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
- end
+ end;
-structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData)
+structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData);
(*For addition, we already have rules for the operand 0.
Multiplication is omitted because there are already special rules for
@@ -386,7 +386,7 @@
ComplexAbstractNumerals.proc diff_complex_number_of),
("complex_eq_eval_numerals",
["(m::complex) = 0", "(m::complex) = 1", "(m::complex) = number_of v"],
- ComplexAbstractNumerals.proc eq_complex_number_of)]
+ ComplexAbstractNumerals.proc eq_complex_number_of)];
end;
@@ -447,44 +447,7 @@
Addsimps [complex_of_real_zero_iff];
-(*** Real and imaginary stuff ***)
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + ii * number_of ya = \
-\ number_of xb + ii * number_of yb) = \
-\ (((number_of xa :: complex) = number_of xb) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff]));
-qed "complex_number_of_eq_cancel_iff";
-Addsimps [complex_number_of_eq_cancel_iff];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + number_of ya * ii = \
-\ number_of xb + number_of yb * ii) = \
-\ (((number_of xa :: complex) = number_of xb) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffA]));
-qed "complex_number_of_eq_cancel_iffA";
-Addsimps [complex_number_of_eq_cancel_iffA];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + number_of ya * ii = \
-\ number_of xb + ii * number_of yb) = \
-\ (((number_of xa :: complex) = number_of xb) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffB]));
-qed "complex_number_of_eq_cancel_iffB";
-Addsimps [complex_number_of_eq_cancel_iffB];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + ii * number_of ya = \
-\ number_of xb + number_of yb * ii) = \
-\ (((number_of xa :: complex) = number_of xb) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffC]));
-qed "complex_number_of_eq_cancel_iffC";
-Addsimps [complex_number_of_eq_cancel_iffC];
-
+(*Convert???
Goalw [complex_number_of_def]
"((number_of xa :: complex) + ii * number_of ya = \
\ number_of xb) = \
@@ -524,6 +487,7 @@
complex_of_real_zero_iff]));
qed "complex_number_of_eq_cancel_iff3a";
Addsimps [complex_number_of_eq_cancel_iff3a];
+*)
Goalw [complex_number_of_def] "cnj (number_of v :: complex) = number_of v";
by (rtac complex_cnj_complex_of_real 1);
--- a/src/HOL/Complex/NSCA.ML Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSCA.ML Thu Feb 05 10:45:28 2004 +0100
@@ -943,11 +943,8 @@
\ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex";
by (auto_tac (claset(),simpset() addsimps [SComplex_def,
hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
-by (res_inst_tac [("x","complex_of_real r + ii * complex_of_real ra")] exI 1);
+by (res_inst_tac [("x","Complex r ra")] exI 1);
by (Ultra_tac 1);
-by (case_tac "X x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
- complex_add,complex_mult]));
qed "Reals_Re_Im_SComplex";
Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \
@@ -987,8 +984,7 @@
by (res_inst_tac [("z","t")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1);
by Auto_tac;
-by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")]
- exI 1);
+by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1);
by Auto_tac;
qed "stc_part_Ex";
--- a/src/HOL/Complex/NSComplex.thy Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy Thu Feb 05 10:45:28 2004 +0100
@@ -37,15 +37,15 @@
hcomplex_diff_def:
"w - z == w + -(z::hcomplex)"
+ hcinv_def:
+ "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
+ hcomplexrel `` {%n. inverse(X n)})"
+
constdefs
hcomplex_of_complex :: "complex => hcomplex"
"hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
- hcinv :: "hcomplex => hcomplex"
- "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
- hcomplexrel `` {%n. inverse(X n)})"
-
(*--- real and Imaginary parts ---*)
hRe :: "hcomplex => hypreal"
@@ -99,6 +99,11 @@
"hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
+constdefs
+ HComplex :: "[hypreal,hypreal] => hcomplex"
+ "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"
+
+
defs (overloaded)
(*----------- division ----------*)
@@ -182,8 +187,7 @@
apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
done
-(*??delete*)
-lemma hcomplexrel_iff [iff]:
+lemma hcomplexrel_iff [simp]:
"((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
by (simp add: hcomplexrel_def)
@@ -195,7 +199,7 @@
Abs_hypreal(hyprel `` {%n. Re(X n)})"
apply (simp add: hRe_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hIm:
@@ -203,17 +207,20 @@
Abs_hypreal(hyprel `` {%n. Im(X n)})"
apply (simp add: hIm_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_hRe_hIm_cancel_iff:
"(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
apply (rule eq_Abs_hcomplex [of z])
apply (rule eq_Abs_hcomplex [of w])
-apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
+apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
apply (ultra+)
done
+lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
+by (simp add: hcomplex_hRe_hIm_cancel_iff)
+
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
@@ -231,14 +238,15 @@
lemma hcomplex_add_congruent2:
"congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
-by (auto simp add: congruent2_def, ultra)
+by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra)
lemma hcomplex_add:
- "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
- Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
+ "Abs_hcomplex(hcomplexrel``{%n. X n}) +
+ Abs_hcomplex(hcomplexrel``{%n. Y n}) =
+ Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
apply (simp add: hcomplex_add_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto simp add: iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
@@ -286,7 +294,7 @@
Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
apply (simp add: hcomplex_minus_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
@@ -303,7 +311,7 @@
Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
apply (simp add: hcomplex_mult_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
@@ -350,7 +358,7 @@
Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
apply (simp add: hcinv_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_mult_inv_left:
@@ -428,6 +436,15 @@
apply (simp add: minus_equation_iff [of x y])
done
+lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
+by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
+
+lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
+by (simp add: mult_assoc [symmetric])
+
+lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
+by (simp add: iii_def hcomplex_zero_def)
+
subsection{*More Multiplication Laws*}
@@ -469,7 +486,7 @@
"hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
apply (simp add: hcomplex_of_hypreal_def)
-apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_of_hypreal_cancel_iff [iff]:
@@ -541,6 +558,34 @@
by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
+subsection{*HComplex theorems*}
+
+lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
+done
+
+lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
+done
+
+text{*Relates the two nonstandard constructions*}
+lemma HComplex_eq_Abs_hcomplex_Complex:
+ "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
+ Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
+by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm)
+
+lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
+by (simp add: hcomplex_equality)
+
+lemma hcomplex_induct [case_names rect, induct type: hcomplex]:
+ "(\<And>x y. P (HComplex x y)) ==> P z"
+by (rule hcomplex_surj [THEN subst], blast)
+
+
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
lemma hcmod:
@@ -549,12 +594,11 @@
apply (simp add: hcmod_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcmod_zero [simp]: "hcmod(0) = 0"
-apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
-done
+by (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
lemma hcmod_one [simp]: "hcmod(1) = 1"
by (simp add: hcomplex_one_def hcmod hypreal_one_num)
@@ -569,6 +613,64 @@
hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
by simp
+lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')"
+apply (rule iffI)
+ prefer 2 apply simp
+apply (simp add: HComplex_def iii_def)
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of x'])
+apply (rule eq_Abs_hypreal [of y'])
+apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
+apply (ultra+)
+done
+
+lemma HComplex_add [simp]:
+ "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
+by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib)
+
+lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
+by (simp add: HComplex_def hcomplex_of_hypreal_minus)
+
+lemma HComplex_diff [simp]:
+ "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
+by (simp add: diff_minus)
+
+lemma HComplex_mult [simp]:
+ "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
+by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus
+ hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
+ add_ac mult_ac right_distrib)
+
+(*HComplex_inverse is proved below*)
+
+lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0"
+by (simp add: HComplex_def)
+
+lemma HComplex_add_hcomplex_of_hypreal [simp]:
+ "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
+by (simp add: hcomplex_of_hypreal_eq)
+
+lemma hcomplex_of_hypreal_add_HComplex [simp]:
+ "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
+by (simp add: i_def hcomplex_of_hypreal_eq)
+
+lemma HComplex_mult_hcomplex_of_hypreal:
+ "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
+by (simp add: hcomplex_of_hypreal_eq)
+
+lemma hcomplex_of_hypreal_mult_HComplex:
+ "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
+by (simp add: i_def hcomplex_of_hypreal_eq)
+
+lemma i_hcomplex_of_hypreal [simp]:
+ "iii * hcomplex_of_hypreal r = HComplex 0 r"
+by (simp add: HComplex_def)
+
+lemma hcomplex_of_hypreal_i [simp]:
+ "hcomplex_of_hypreal r * iii = HComplex 0 r"
+by (simp add: mult_commute)
+
subsection{*Conjugation*}
@@ -577,7 +679,7 @@
Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
apply (simp add: hcnj_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
@@ -777,7 +879,7 @@
Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
apply (simp add: hcpow_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hcomplex_of_hypreal_hyperpow:
@@ -817,6 +919,9 @@
show "z^(Suc n) = z * (z^n)" by simp
qed
+lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
+by (simp add: power2_eq_square)
+
lemma hcomplex_of_hypreal_pow:
"hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
@@ -872,15 +977,6 @@
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
by (blast intro: ccontr dest: hcpow_not_zero)
-lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
-by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
-
-lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
-by (simp add: numeral_2_eq_2)
-
-lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
-by (simp add: iii_def hcomplex_zero_def)
-
lemma hcomplex_divide:
"Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
@@ -888,6 +984,7 @@
+
subsection{*The Function @{term hsgn}*}
lemma hsgn:
@@ -895,7 +992,7 @@
Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
apply (simp add: hsgn_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hsgn_zero [simp]: "hsgn 0 = 0"
@@ -914,144 +1011,33 @@
apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
done
-lemma lemma_hypreal_P_EX2:
- "(\<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, auto)
-done
-lemma complex_split2:
- "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
-by (blast intro: complex_split)
-
-(* Interesting proof! *)
-lemma hcomplex_split:
- "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
-apply (rule eq_Abs_hcomplex [of z])
-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)
-apply (drule choice, safe)+
-apply (rule_tac x = f in exI)
-apply (rule_tac x = fa in exI, auto)
-done
-
-lemma hRe_hcomplex_i [simp]:
- "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
-done
-
-lemma hIm_hcomplex_i [simp]:
- "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
+lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
-done
-
-lemma hcmod_i:
- "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
- ( *f* sqrt) (x ^ 2 + y ^ 2)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
-done
-
-lemma hcomplex_eq_hRe_eq:
- "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
- hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
- ==> xa = xb"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of xa])
-apply (rule eq_Abs_hypreal [of ya])
-apply (rule eq_Abs_hypreal [of xb])
-apply (rule eq_Abs_hypreal [of yb])
-apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
-done
-
-lemma hcomplex_eq_hIm_eq:
- "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
- hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
- ==> ya = yb"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of xa])
-apply (rule eq_Abs_hypreal [of ya])
-apply (rule eq_Abs_hypreal [of xb])
-apply (rule eq_Abs_hypreal [of yb])
-apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun
+ hypreal_mult hypreal_add hcmod numeral_2_eq_2)
done
-lemma hcomplex_eq_cancel_iff [simp]:
- "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
- hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
- ((xa = xb) & (ya = yb))"
-by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
-
-lemma hcomplex_eq_cancel_iffA [iff]:
- "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
- hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iffB [iff]:
- "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
- hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iffC [iff]:
- "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
- hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
+lemma hcomplex_eq_cancel_iff1 [simp]:
+ "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
+by (simp add: hcomplex_of_hypreal_eq)
lemma hcomplex_eq_cancel_iff2 [simp]:
- "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
- hcomplex_of_hypreal xa) = (x = xa & y = 0)"
-apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff)
-apply (simp del: hcomplex_eq_cancel_iff)
-done
+ "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
+by (simp add: hcomplex_of_hypreal_eq)
-lemma hcomplex_eq_cancel_iff2a [simp]:
- "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
- hcomplex_of_hypreal xa) = (x = xa & y = 0)"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iff3 [simp]:
- "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
- iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
-apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff)
-apply (simp del: hcomplex_eq_cancel_iff)
-done
+lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
+by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
-lemma hcomplex_eq_cancel_iff3a [simp]:
- "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
- iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
-apply (simp add: hcomplex_mult_commute)
-done
+lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
+by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
-lemma hcomplex_split_hRe_zero:
- "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
- ==> x = 0"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
-apply (simp add: complex_split_Re_zero)
-done
+lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
+by (insert hcomplex_of_hypreal_i [of 1], simp)
-lemma hcomplex_split_hIm_zero:
- "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
- ==> y = 0"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
-apply (simp add: complex_split_Im_zero)
-done
+lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
+by (simp add: i_eq_HComplex_0_1)
lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
apply (rule eq_Abs_hcomplex [of z])
@@ -1064,8 +1050,7 @@
done
lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
-apply (auto intro: real_sum_squares_cancel)
-done
+by (auto intro: real_sum_squares_cancel)
lemma hcomplex_inverse_complex_split:
"inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
@@ -1074,8 +1059,16 @@
apply (rule eq_Abs_hypreal [of x])
apply (rule eq_Abs_hypreal [of y])
apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
+apply (simp add: diff_minus)
done
+lemma HComplex_inverse:
+ "inverse (HComplex x y) =
+ HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
+by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
+
+
+
lemma hRe_mult_i_eq[simp]:
"hRe (iii * hcomplex_of_hypreal y) = 0"
apply (simp add: iii_def)
@@ -1096,7 +1089,7 @@
done
lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
-by (simp add: hcomplex_mult_commute)
+by (simp only: hcmod_mult_i hcomplex_mult_commute)
(*---------------------------------------------------------------------------*)
(* harg *)
@@ -1105,31 +1098,29 @@
lemma harg:
"harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
Abs_hypreal(hyprel `` {%n. arg (X n)})"
-
apply (simp add: harg_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
done
lemma cos_harg_i_mult_zero_pos:
- "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
+ "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
- hypreal_zero_num hypreal_less starfun harg, ultra)
+apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
+ hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
done
lemma cos_harg_i_mult_zero_neg:
- "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
+ "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
- hypreal_zero_num hypreal_less starfun harg, ultra)
+apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
+ hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
done
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 linorder_less_linear)
-apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
-done
+ "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
+by (auto simp add: linorder_neq_iff
+ cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
lemma hcomplex_of_hypreal_zero_iff [simp]:
"(hcomplex_of_hypreal y = 0) = (y = 0)"
@@ -1141,16 +1132,21 @@
subsection{*Polar Form for Nonstandard Complex Numbers*}
lemma complex_split_polar2:
- "\<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)
+ "\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))"
+by (blast intro: complex_split_polar)
+
+lemma lemma_hypreal_P_EX2:
+ "(\<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, auto)
done
lemma hcomplex_split_polar:
- "\<exists>r a. z = hcomplex_of_hypreal r *
- (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
+ "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
apply (rule eq_Abs_hcomplex [of z])
-apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
+apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
apply (cut_tac z = x in complex_split_polar2)
apply (drule choice, safe)+
apply (rule_tac x = f in exI)
@@ -1161,7 +1157,7 @@
"hcis (Abs_hypreal(hyprel `` {%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
apply (simp add: hcis_def)
-apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
done
lemma hcis_eq:
@@ -1178,35 +1174,38 @@
by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
-apply (simp add: hrcis_def hcis_eq)
+apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
apply (rule hcomplex_split_polar)
done
lemma hRe_hcomplex_polar [simp]:
- "hRe(hcomplex_of_hypreal r *
- (hcomplex_of_hypreal(( *f* cos) a) +
- iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
-by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
+ "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+ r * ( *f* cos) a"
+by (simp add: hcomplex_of_hypreal_mult_HComplex)
lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
by (simp add: hrcis_def hcis_eq)
lemma hIm_hcomplex_polar [simp]:
- "hIm(hcomplex_of_hypreal r *
- (hcomplex_of_hypreal(( *f* cos) a) +
- iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
-by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
+ "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+ r * ( *f* sin) a"
+by (simp add: hcomplex_of_hypreal_mult_HComplex)
lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
by (simp add: hrcis_def hcis_eq)
+
+lemma hcmod_unit_one [simp]:
+ "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
+apply (rule eq_Abs_hypreal [of a])
+apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal
+ hcomplex_mult hcmod hcomplex_add hypreal_one_def)
+done
+
lemma hcmod_complex_polar [simp]:
- "hcmod (hcomplex_of_hypreal r *
- (hcomplex_of_hypreal(( *f* cos) a) +
- iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of a])
-apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
+ "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+ abs r"
+apply (simp only: hcmod_mult hcmod_unit_one, simp)
done
lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
@@ -1316,20 +1315,16 @@
done
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
-apply (simp add: NSDeMoivre)
-done
+by (simp add: NSDeMoivre)
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
-apply (simp add: NSDeMoivre)
-done
+by (simp add: NSDeMoivre)
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
-apply (simp add: NSDeMoivre_ext)
-done
+by (simp add: NSDeMoivre_ext)
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
-apply (simp add: NSDeMoivre_ext)
-done
+by (simp add: NSDeMoivre_ext)
lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
apply (simp add: hexpi_def)
@@ -1545,27 +1540,11 @@
val hsgn_minus = thm"hsgn_minus";
val hsgn_eq = thm"hsgn_eq";
val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
-val complex_split2 = thm"complex_split2";
-val hcomplex_split = thm"hcomplex_split";
-val hRe_hcomplex_i = thm"hRe_hcomplex_i";
-val hIm_hcomplex_i = thm"hIm_hcomplex_i";
val hcmod_i = thm"hcmod_i";
-val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq";
-val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq";
-val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff";
-val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA";
-val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB";
-val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC";
val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
-val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a";
-val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3";
-val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a";
-val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero";
-val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero";
val hRe_hsgn = thm"hRe_hsgn";
val hIm_hsgn = thm"hIm_hsgn";
val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
-val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split";
val hRe_mult_i_eq = thm"hRe_mult_i_eq";
val hIm_mult_i_eq = thm"hIm_mult_i_eq";
val hcmod_mult_i = thm"hcmod_mult_i";
--- a/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
@@ -482,6 +482,7 @@
(*** Real and imaginary stuff ***)
+(*Convert???
Goalw [hcomplex_number_of_def]
"((number_of xa :: hcomplex) + iii * number_of ya = \
\ number_of xb + iii * number_of yb) = \
@@ -561,6 +562,7 @@
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
qed "hcomplex_number_of_eq_cancel_iff3a";
Addsimps [hcomplex_number_of_eq_cancel_iff3a];
+*)
Goalw [hcomplex_number_of_def] "hcnj (number_of v :: hcomplex) = number_of v";
by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
--- a/src/HOL/Real/PReal.thy Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Real/PReal.thy Thu Feb 05 10:45:28 2004 +0100
@@ -386,17 +386,18 @@
proof (intro exI conjI)
show "0 < x*y" by (simp add: mult_pos)
show "x * y \<notin> mult_set A B"
- proof (auto simp add: mult_set_def)
- fix u::rat and v::rat
- assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
- moreover
- with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
- moreover
- with prems have "0\<le>v"
- by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems)
- moreover
- hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
- ultimately show False by force
+ proof -
+ { fix u::rat and v::rat
+ assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
+ moreover
+ with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
+ moreover
+ with prems have "0\<le>v"
+ by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems)
+ moreover
+ hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
+ ultimately have False by force}
+ thus ?thesis by (auto simp add: mult_set_def)
qed
qed
qed
@@ -646,14 +647,15 @@
proof (intro exI conjI)
show "0 < inverse x" by simp
show "inverse x \<notin> inverse_set A"
- proof (auto simp add: inverse_set_def)
- fix y::rat
- assume ygt: "inverse x < y"
- have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
- have iyless: "inverse y < x"
- by (simp add: inverse_less_imp_less [of x] ygt)
- show "inverse y \<in> A"
- by (simp add: preal_downwards_closed [OF A x] iyless)
+ proof -
+ { fix y::rat
+ assume ygt: "inverse x < y"
+ have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
+ have iyless: "inverse y < x"
+ by (simp add: inverse_less_imp_less [of x] ygt)
+ have "inverse y \<in> A"
+ by (simp add: preal_downwards_closed [OF A x] iyless)}
+ thus ?thesis by (auto simp add: inverse_set_def)
qed
qed
qed
--- a/src/HOL/Ring_and_Field.thy Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Thu Feb 05 10:45:28 2004 +0100
@@ -94,10 +94,10 @@
by (simp add: add_commute)
lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
- proof (rule add_left_cancel [of "-a", THEN iffD1])
- show "(-a + -(-a) = -a + a)"
- by simp
- qed
+proof (rule add_left_cancel [of "-a", THEN iffD1])
+ show "(-a + -(-a) = -a + a)"
+ by simp
+qed
lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
apply (rule right_minus_eq [THEN iffD1, symmetric])
@@ -120,15 +120,15 @@
by (simp add: diff_minus)
lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
- proof
- assume "- a = - b"
- hence "- (- a) = - (- b)"
- by simp
- thus "a=b" by simp
- next
- assume "a=b"
- thus "-a = -b" by simp
- qed
+proof
+ assume "- a = - b"
+ hence "- (- a) = - (- b)"
+ by simp
+ thus "a=b" by simp
+next
+ assume "a=b"
+ thus "-a = -b" by simp
+qed
lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
by (subst neg_equal_iff_equal [symmetric], simp)
@@ -139,16 +139,16 @@
text{*The next two equations can make the simplifier loop!*}
lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
- proof -
+proof -
have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
- qed
+qed
lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
- proof -
+proof -
have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
- qed
+qed
subsection {* Derived rules for multiplication *}
@@ -263,13 +263,13 @@
lemma add_less_imp_less_left:
assumes less: "c + a < c + b" shows "a < (b::'a::ordered_semiring)"
- proof (rule ccontr)
- assume "~ a < b"
- hence "b \<le> a" by (simp add: linorder_not_less)
- hence "c+b \<le> c+a" by (rule add_left_mono)
- with this and less show False
- by (simp add: linorder_not_less [symmetric])
- qed
+proof (rule ccontr)
+ assume "~ a < b"
+ hence "b \<le> a" by (simp add: linorder_not_less)
+ hence "c+b \<le> c+a" by (rule add_left_mono)
+ with this and less show False
+ by (simp add: linorder_not_less [symmetric])
+qed
lemma add_less_imp_less_right:
"a + c < b + c ==> a < (b::'a::ordered_semiring)"
@@ -306,7 +306,7 @@
lemma le_imp_neg_le:
assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
- proof -
+proof -
have "-a+a \<le> -a+b"
by (rule add_left_mono)
hence "0 \<le> -a+b"
@@ -315,18 +315,18 @@
by (rule add_right_mono)
thus ?thesis
by (simp add: add_assoc)
- qed
+qed
lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
- proof
- assume "- b \<le> - a"
- hence "- (- a) \<le> - (- b)"
- by (rule le_imp_neg_le)
- thus "a\<le>b" by simp
- next
- assume "a\<le>b"
- thus "-b \<le> -a" by (rule le_imp_neg_le)
- qed
+proof
+ assume "- b \<le> - a"
+ hence "- (- a) \<le> - (- b)"
+ by (rule le_imp_neg_le)
+ thus "a\<le>b" by simp
+next
+ assume "a\<le>b"
+ thus "-b \<le> -a" by (rule le_imp_neg_le)
+qed
lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
by (subst neg_le_iff_le [symmetric], simp)
@@ -346,16 +346,16 @@
text{*The next several equations can make the simplifier loop!*}
lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"
- proof -
+proof -
have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
thus ?thesis by simp
- qed
+qed
lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"
- proof -
+proof -
have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
thus ?thesis by simp
- qed
+qed
lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
apply (simp add: linorder_not_less [symmetric])
@@ -645,13 +645,13 @@
lemma mult_less_imp_less_left:
assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
shows "a < (b::'a::ordered_semiring)"
- proof (rule ccontr)
- assume "~ a < b"
- hence "b \<le> a" by (simp add: linorder_not_less)
- hence "c*b \<le> c*a" by (rule mult_left_mono)
- with this and less show False
- by (simp add: linorder_not_less [symmetric])
- qed
+proof (rule ccontr)
+ assume "~ a < b"
+ hence "b \<le> a" by (simp add: linorder_not_less)
+ hence "c*b \<le> c*a" by (rule mult_left_mono)
+ with this and less show False
+ by (simp add: linorder_not_less [symmetric])
+qed
lemma mult_less_imp_less_right:
"[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
@@ -723,52 +723,50 @@
text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
of an ordering.*}
lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
- proof cases
- assume "a=0" thus ?thesis by simp
- next
- assume anz [simp]: "a\<noteq>0"
- thus ?thesis
- proof auto
- assume "a * b = 0"
- hence "inverse a * (a * b) = 0" by simp
- thus "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])
- qed
- qed
+proof cases
+ assume "a=0" thus ?thesis by simp
+next
+ assume anz [simp]: "a\<noteq>0"
+ { assume "a * b = 0"
+ hence "inverse a * (a * b) = 0" by simp
+ hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])}
+ thus ?thesis by force
+qed
text{*Cancellation of equalities with a common factor*}
lemma field_mult_cancel_right_lemma:
assumes cnz: "c \<noteq> (0::'a::field)"
and eq: "a*c = b*c"
shows "a=b"
- proof -
+proof -
have "(a * c) * inverse c = (b * c) * inverse c"
by (simp add: eq)
thus "a=b"
by (simp add: mult_assoc cnz)
- qed
+qed
lemma field_mult_cancel_right [simp]:
"(a*c = b*c) = (c = (0::'a::field) | a=b)"
- proof cases
- assume "c=0" thus ?thesis by simp
- next
- assume "c\<noteq>0"
- thus ?thesis by (force dest: field_mult_cancel_right_lemma)
- qed
+proof cases
+ assume "c=0" thus ?thesis by simp
+next
+ assume "c\<noteq>0"
+ thus ?thesis by (force dest: field_mult_cancel_right_lemma)
+qed
lemma field_mult_cancel_left [simp]:
"(c*a = c*b) = (c = (0::'a::field) | a=b)"
by (simp add: mult_commute [of c] field_mult_cancel_right)
lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
- proof
+proof
assume ianz: "inverse a = 0"
assume "a \<noteq> 0"
hence "1 = a * inverse a" by simp
also have "... = 0" by (simp add: ianz)
finally have "1 = (0::'a::field)" .
thus False by (simp add: eq_commute)
- qed
+qed
subsection{*Basic Properties of @{term inverse}*}
@@ -790,35 +788,35 @@
lemma nonzero_inverse_minus_eq:
assumes [simp]: "a\<noteq>0" shows "inverse(-a) = -inverse(a::'a::field)"
- proof -
- have "-a * inverse (- a) = -a * - inverse a"
- by simp
- thus ?thesis
- by (simp only: field_mult_cancel_left, simp)
- qed
+proof -
+ have "-a * inverse (- a) = -a * - inverse a"
+ by simp
+ thus ?thesis
+ by (simp only: field_mult_cancel_left, simp)
+qed
lemma inverse_minus_eq [simp]:
- "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
- proof cases
- assume "a=0" thus ?thesis by (simp add: inverse_zero)
- next
- assume "a\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_minus_eq)
- qed
+ "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
+proof cases
+ assume "a=0" thus ?thesis by (simp add: inverse_zero)
+next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
lemma nonzero_inverse_eq_imp_eq:
assumes inveq: "inverse a = inverse b"
and anz: "a \<noteq> 0"
and bnz: "b \<noteq> 0"
shows "a = (b::'a::field)"
- proof -
+proof -
have "a * inverse b = a * inverse a"
by (simp add: inveq)
hence "(a * inverse b) * b = (a * inverse a) * b"
by simp
thus "a = b"
by (simp add: mult_assoc anz bnz)
- qed
+qed
lemma inverse_eq_imp_eq:
"inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"