# HG changeset patch # User wenzelm # Date 1010947350 -3600 # Node ID 611ab32b2176d977dc51a98944dc3a6e3d045ddf # Parent c93b2f69b3ba03fee19ee9439b65ab4319f043e6 Real/Complex_Numbers.thy; diff -r c93b2f69b3ba -r 611ab32b2176 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Jan 12 22:44:10 2002 +0100 +++ b/src/HOL/IsaMakefile Sun Jan 13 19:42:30 2002 +0100 @@ -112,7 +112,7 @@ HOL-Real: HOL $(OUT)/HOL-Real -$(OUT)/HOL-Real: $(OUT)/HOL \ +$(OUT)/HOL-Real: $(OUT)/HOL Real/Complex_Numbers.thy \ Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \ Real/PRat.ML Real/PRat.thy \ Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ diff -r c93b2f69b3ba -r 611ab32b2176 src/HOL/Real/Complex_Numbers.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/Complex_Numbers.thy Sun Jan 13 19:42:30 2002 +0100 @@ -0,0 +1,178 @@ +(* Title: HOL/Real/Complex_Numbers.thy + ID: $Id$ + Author: Gertrud Bauer and Markus Wenzel, TU München + License: GPL (GNU GENERAL PUBLIC LICENSE) +*) + +header {* Complex numbers *} + +theory Complex_Numbers = RealPow + Ring_and_Field: + +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 +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" + by (simp add: numeral_2_eq_2) + +lemma real_sqr_ge_zero [iff]: "0 \ (r::real)^2" + by (simp add: real_power_two) + +lemma real_sqr_gt_zero [iff]: "(r::real) \ 0 \ 0 < r^2" +proof - + assume "r \ 0" + hence "0 \ r^2" by simp + also have "0 \ r^2" by simp + finally show ?thesis . +qed + +lemma real_sqr_not_zero: "r \ 0 \ (r::real)^2 \ 0" + by simp + + +subsection {* The field of complex numbers *} + +datatype complex = Complex real real + +consts Re :: "complex \ real" +primrec "Re (Complex x y) = x" + +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" + +instance complex :: zero .. +instance complex :: one .. +instance complex :: number .. +instance complex :: plus .. +instance complex :: minus .. +instance complex :: times .. +instance complex :: power .. +instance complex :: inverse .. + +defs (overloaded) + zero_complex_def: "0 == Complex 0 0" + one_complex_def: "1 == Complex 1 0" + number_of_complex_def: "number_of b == Complex (number_of b) 0" + add_complex_def: "z + w == Complex (Re z + Re w) (Im z + Im w)" + minus_complex_def: "z - w == Complex (Re z - Re w) (Im z - Im w)" + 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" + +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" + by (induct z, induct w) simp + +lemma Re_zero [simp]: "Re 0 = 0" + and Im_zero [simp]: "Im 0 = 0" + by (simp_all add: zero_complex_def) + +lemma Re_one [simp]: "Re 1 = 1" + 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) + +lemma Im_add [simp]: "Im (z + w) = Im z + Im w" + by (simp add: add_complex_def) + +lemma Re_diff [simp]: "Re (z - w) = Re z - Re w" + by (simp add: minus_complex_def) + +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" + by (simp add: uminus_complex_def) + +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" + by (simp add: mult_complex_def) + +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) + + +instance complex :: field +proof + fix z u v w :: complex + show "(u + v) + w = u + (v + w)" + by (simp add: add_complex_def) + show "z + w = w + z" + 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" + 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 *) + show "z * w = w * z" + by (simp add: mult_complex_def) + show "1 * z = z" + by (simp add: one_complex_def mult_complex_def) + show "(u + v) * w = u * w + v * w" + by (simp add: add_complex_def mult_complex_def ring_distrib) + assume neq: "w \ 0" + show "inverse w * w = 1" + proof + have neq': "Re w * Re w + Im w * Im w \ 0" + proof - + have ge: "0 \ Re w * Re w" "0 \ Im w * Im w" by simp_all + from neq have "Re w \ 0 \ Im w \ 0" by (simp add: zero_complex_iff) + hence "Re w * Re w \ 0 \ Im w * Im w \ 0" by simp + thus ?thesis by rule (insert ge, arith+) + qed + with neq show "Re (inverse w * w) = Re 1" + by (simp add: inverse_complex_def real_power_two real_add_divide_distrib [symmetric]) + from neq show "Im (inverse w * w) = Im 1" + 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 \} *} + by (simp add: im_unit_def complex_power_two mult_complex_def number_of_complex_def) + +end diff -r c93b2f69b3ba -r 611ab32b2176 src/HOL/Real/ROOT.ML --- a/src/HOL/Real/ROOT.ML Sat Jan 12 22:44:10 2002 +0100 +++ b/src/HOL/Real/ROOT.ML Sun Jan 13 19:42:30 2002 +0100 @@ -7,4 +7,5 @@ by Jacques Fleuriot *) +no_document time_use_thy "Ring_and_Field"; time_use_thy "Real";