# HG changeset patch # User wenzelm # Date 1010952871 -3600 # Node ID 4e45fb10c811a6c37ee3cd3b30d6f9c9ca7c8502 # Parent 1fce8f51034dbcc2c47ccef40c44f39701d6eeb5 tuned; diff -r 1fce8f51034d -r 4e45fb10c811 src/HOL/Real/Complex_Numbers.thy --- a/src/HOL/Real/Complex_Numbers.thy Sun Jan 13 21:14:14 2002 +0100 +++ b/src/HOL/Real/Complex_Numbers.thy Sun Jan 13 21:14:31 2002 +0100 @@ -10,52 +10,39 @@ subsection {* The field of real numbers *} (* FIXME move *) -instance real :: inverse .. -instance real :: ring - by intro_classes (auto simp add: real_add_mult_distrib) +instance real :: field + by intro_classes (simp_all add: real_add_mult_distrib real_divide_def) -instance real :: field -proof - fix a b :: real - show "a \ 0 \ inverse a * a = 1" by simp - show "b \ 0 \ a / b = a * inverse b" by (simp add: real_divide_def) -qed - -lemma real_power_two: "(r::real)^2 = r * r" +lemma real_power_two: "(r::real)\ = r * r" by (simp add: numeral_2_eq_2) -lemma real_sqr_ge_zero [iff]: "0 \ (r::real)^2" +lemma real_sqr_ge_zero [iff]: "0 \ (r::real)\" by (simp add: real_power_two) -lemma real_sqr_gt_zero [iff]: "(r::real) \ 0 \ 0 < r^2" +lemma real_sqr_gt_zero: "(r::real) \ 0 ==> 0 < r\" proof - assume "r \ 0" - hence "0 \ r^2" by simp - also have "0 \ r^2" by simp + hence "0 \ r\" by simp + also have "0 \ r\" by (simp add: real_sqr_ge_zero) finally show ?thesis . qed -lemma real_sqr_not_zero: "r \ 0 \ (r::real)^2 \ 0" +lemma real_sqr_not_zero: "r \ 0 ==> (r::real)\ \ 0" by simp -subsection {* The field of complex numbers *} +subsection {* Representation of complex numbers *} datatype complex = Complex real real -consts Re :: "complex \ real" +consts Re :: "complex => real" primrec "Re (Complex x y) = x" -consts Im :: "complex \ real" +consts Im :: "complex => real" primrec "Im (Complex x y) = y" -constdefs - complex :: "'a \ complex" - "complex x == Complex (real x) 0" - conjg :: "complex \ complex" - "conjg z == Complex (Re z) (-Im z)" - im_unit :: complex ("\") - "\ == Complex 0 1" +lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" + by (induct z) simp instance complex :: zero .. instance complex :: one .. @@ -63,7 +50,6 @@ instance complex :: plus .. instance complex :: minus .. instance complex :: times .. -instance complex :: power .. instance complex :: inverse .. defs (overloaded) @@ -75,18 +61,11 @@ uminus_complex_def: "- z == Complex (- Re z) (- Im z)" mult_complex_def: "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)" - inverse_complex_def: "(z::complex) \ 0 \ inverse z == - Complex (Re z / ((Re z)^2 + (Im z)^2)) (- Im z / ((Re z)^2 + (Im z)^2))" - divide_complex_def: "(w::complex) \ 0 \ z / (w::complex) == z * inverse w" + inverse_complex_def: "(z::complex) \ 0 ==> inverse z == + Complex (Re z / ((Re z)\ + (Im z)\)) (- Im z / ((Re z)\ + (Im z)\))" + divide_complex_def: "(w::complex) \ 0 ==> z / (w::complex) == z * inverse w" -primrec (power_complex) - "z^0 = 1" - "z^(Suc n) = (z::complex) * (z^n)" - -lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" - by (induct z) simp - -lemma complex_equality [simp, intro?]: "Re z = Re w \ Im z = Im w \ z = w" +lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w" by (induct z, induct w) simp lemma Re_zero [simp]: "Re 0 = 0" @@ -97,10 +76,6 @@ and Im_one [simp]: "Im 1 = 0" by (simp_all add: one_complex_def) -lemma zero_complex_iff: "(z = 0) = (Re z = 0 \ Im z = 0)" - and one_complex_iff: "(z = 1) = (Re z = 1 \ Im z = 0)" - by auto - lemma Re_add [simp]: "Re (z + w) = Re z + Re w" by (simp add: add_complex_def) @@ -113,10 +88,10 @@ lemma Im_diff [simp]: "Im (z - w) = Im z - Im w" by (simp add: minus_complex_def) -lemma Re_uminus [simp]: "Re (- z) = - Re z" +lemma Re_uminus [simp]: "Re (-z) = - Re z" by (simp add: uminus_complex_def) -lemma Im_uminus [simp]: "Im (- z) = - Im z" +lemma Im_uminus [simp]: "Im (-z) = - Im z" by (simp add: uminus_complex_def) lemma Re_mult [simp]: "Re (z * w) = Re z * Re w - Im z * Im w" @@ -125,10 +100,13 @@ lemma Im_mult [simp]: "Im (z * w) = Re z * Im w + Im z * Re w" by (simp add: mult_complex_def) -lemma complex_power_two: "z^2 = z * (z::complex)" - by (simp add: numeral_2_eq_2) +lemma zero_complex_iff: "(z = 0) = (Re z = 0 \ Im z = 0)" + and one_complex_iff: "(z = 1) = (Re z = 1 \ Im z = 0)" + by (auto simp add: complex_equality) +subsection {* The field of complex numbers *} + instance complex :: field proof fix z u v w :: complex @@ -138,9 +116,9 @@ by (simp add: add_complex_def) show "0 + z = z" by (simp add: add_complex_def zero_complex_def) - show "- z + z = 0" - by (simp add: minus_complex_def) - show "z - w = z + - w" + show "-z + z = 0" + by (simp add: complex_equality minus_complex_def) + show "z - w = z + -w" by (simp add: add_complex_def minus_complex_def uminus_complex_def) show "(u * v) * w = u * (v * w)" by (simp add: mult_complex_def ring_mult_ac ring_distrib real_diff_def) (* FIXME *) @@ -151,6 +129,8 @@ show "(u + v) * w = u * w + v * w" by (simp add: add_complex_def mult_complex_def ring_distrib) assume neq: "w \ 0" + thus "z / w = z * inverse w" + by (simp add: divide_complex_def) show "inverse w * w = 1" proof have neq': "Re w * Re w + Im w * Im w \ 0" @@ -166,13 +146,52 @@ by (simp add: inverse_complex_def real_power_two real_mult_ac real_add_divide_distrib [symmetric]) qed - from neq show "z / w = z * inverse w" - by (simp add: divide_complex_def) qed -lemma im_unit_square: "\^2 = -1" - -- {* key property of the imaginary unit @{text \} *} +subsection {* Basic operations *} + +instance complex :: power .. +primrec (power_complex) + "z ^ 0 = 1" + "z ^ Suc n = (z::complex) * (z ^ n)" + +lemma complex_power_two: "z\ = z * (z::complex)" + by (simp add: complex_equality numeral_2_eq_2) + + +constdefs + im_unit :: complex ("\") + "\ == Complex 0 1" + +lemma im_unit_square: "\\ = -1" by (simp add: im_unit_def complex_power_two mult_complex_def number_of_complex_def) + +constdefs + conjg :: "complex => complex" + "conjg z == Complex (Re z) (- Im z)" + +lemma Re_cong [simp]: "Re (conjg z) = Re z" + by (simp add: conjg_def) + +lemma Im_cong [simp]: "Im (conjg z) = - Im z" + by (simp add: conjg_def) + +lemma Re_conjg_self: "Re (z * conjg z) = (Re z)\ + (Im z)\" + by (simp add: real_power_two) + +lemma Im_conjg_self: "Im (z * conjg z) = 0" + by simp + + +subsection {* Embedding other number domains *} + +constdefs + complex :: "'a => complex" + "complex x == Complex (real x) 0"; + +lemma Re_complex [simp]: "Re (complex x) = real x" + by (simp add: complex_def) + end