author huffman Thu Sep 08 08:41:28 2011 -0700 (2011-09-08) changeset 44844 f74a4175a3a8 parent 44843 93d0f85cfe4a child 44845 5e51075cbd97 child 44846 e9d1fcbc7d20
prove existence, uniqueness, and other properties of complex arg function
 src/HOL/Complex.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Complex.thy	Thu Sep 08 07:27:57 2011 -0700
1.2 +++ b/src/HOL/Complex.thy	Thu Sep 08 08:41:28 2011 -0700
1.3 @@ -546,35 +546,6 @@
1.4    bounded_linear.isCont [OF bounded_linear_cnj]
1.5
1.6
1.7 -subsection {* Complex Argument *}
1.8 -
1.9 -definition arg :: "complex => real" where
1.10 -  "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
1.11 -
1.12 -(*----------------------------------------------------------------------------*)
1.13 -(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
1.14 -(* many of the theorems are not used - so should they be kept?                *)
1.15 -(*----------------------------------------------------------------------------*)
1.16 -
1.17 -lemma cos_arg_i_mult_zero_pos:
1.18 -   "0 < y ==> cos (arg(Complex 0 y)) = 0"
1.19 -apply (simp add: arg_def abs_if)
1.20 -apply (rule_tac a = "pi/2" in someI2, auto)
1.21 -apply (rule order_less_trans [of _ 0], auto)
1.22 -done
1.23 -
1.24 -lemma cos_arg_i_mult_zero_neg:
1.25 -   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
1.26 -apply (simp add: arg_def abs_if)
1.27 -apply (rule_tac a = "- pi/2" in someI2, auto)
1.28 -apply (rule order_trans [of _ 0], auto)
1.29 -done
1.30 -
1.31 -lemma cos_arg_i_mult_zero [simp]:
1.32 -     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
1.33 -by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
1.34 -
1.35 -
1.36  subsection{*Finally! Polar Form for Complex Numbers*}
1.37
1.38  subsubsection {* $\cos \theta + i \sin \theta$ *}
1.39 @@ -700,6 +671,93 @@
1.40  lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
1.41    by (simp add: expi_def cis_def)
1.42
1.43 +subsubsection {* Complex argument *}
1.44 +
1.45 +definition arg :: "complex \<Rightarrow> real" where
1.46 +  "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi))"
1.47 +
1.48 +lemma arg_zero: "arg 0 = 0"
1.49 +  by (simp add: arg_def)
1.50 +
1.51 +lemma of_nat_less_of_int_iff: (* TODO: move *)
1.52 +  "(of_nat n :: 'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
1.53 +  by (metis of_int_of_nat_eq of_int_less_iff)
1.54 +
1.55 +lemma real_of_nat_less_number_of_iff [simp]: (* TODO: move *)
1.56 +  "real (n::nat) < number_of w \<longleftrightarrow> n < number_of w"
1.57 +  unfolding real_of_nat_def nat_number_of_def number_of_eq
1.58 +  by (simp add: of_nat_less_of_int_iff zless_nat_eq_int_zless)
1.59 +
1.60 +lemma arg_unique:
1.61 +  assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
1.62 +  shows "arg z = x"
1.63 +proof -
1.64 +  from assms have "z \<noteq> 0" by auto
1.65 +  have "(SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi) = x"
1.66 +  proof
1.67 +    fix a def d \<equiv> "a - x"
1.68 +    assume a: "sgn z = cis a \<and> - pi < a \<and> a \<le> pi"
1.69 +    from a assms have "- (2*pi) < d \<and> d < 2*pi"
1.70 +      unfolding d_def by simp
1.71 +    moreover from a assms have "cos a = cos x" and "sin a = sin x"
1.72 +      by (simp_all add: complex_eq_iff)
1.73 +    hence "cos d = 1" unfolding d_def cos_diff by simp
1.74 +    moreover hence "sin d = 0" by (rule cos_one_sin_zero)
1.75 +    ultimately have "d = 0"
1.76 +      unfolding sin_zero_iff even_mult_two_ex
1.77 +      by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq)
1.78 +    thus "a = x" unfolding d_def by simp
1.79 +  qed (simp add: assms del: Re_sgn Im_sgn)
1.80 +  with z \<noteq> 0 show "arg z = x"
1.81 +    unfolding arg_def by simp
1.82 +qed
1.83 +
1.84 +lemma arg_correct:
1.85 +  assumes "z \<noteq> 0" shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
1.86 +proof (simp add: arg_def assms, rule someI_ex)
1.87 +  obtain r a where z: "z = rcis r a" using rcis_Ex by fast
1.88 +  with assms have "r \<noteq> 0" by auto
1.89 +  def b \<equiv> "if 0 < r then a else a + pi"
1.90 +  have b: "sgn z = cis b"
1.91 +    unfolding z b_def rcis_def using r \<noteq> 0
1.93 +  have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
1.94 +    by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
1.96 +  have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
1.97 +    by (case_tac x rule: int_diff_cases,
1.98 +      simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
1.99 +  def c \<equiv> "b - 2*pi * of_int \<lceil>(b - pi) / (2*pi)\<rceil>"
1.100 +  have "sgn z = cis c"
1.101 +    unfolding b c_def
1.102 +    by (simp add: cis_divide [symmetric] cis_2pi_int)
1.103 +  moreover have "- pi < c \<and> c \<le> pi"
1.104 +    using ceiling_correct [of "(b - pi) / (2*pi)"]
1.105 +    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
1.106 +  ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
1.107 +qed
1.108 +
1.109 +lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
1.110 +  by (cases "z = 0", simp_all add: arg_zero arg_correct)
1.111 +
1.112 +lemma cis_arg: "z \<noteq> 0 \<Longrightarrow> cis (arg z) = sgn z"
1.113 +  by (simp add: arg_correct)
1.114 +
1.115 +lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
1.116 +  by (cases "z = 0", simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
1.117 +
1.118 +lemma cos_arg_i_mult_zero_pos: (* TODO: delete *)
1.119 +   "0 < y ==> cos (arg(Complex 0 y)) = 0"
1.120 +  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
1.121 +
1.122 +lemma cos_arg_i_mult_zero_neg: (* TODO: delete *)
1.123 +   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
1.124 +  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
1.125 +
1.126 +lemma cos_arg_i_mult_zero [simp]:
1.127 +     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
1.128 +  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
1.129 +
1.130  text {* Legacy theorem names *}
1.131
1.132  lemmas expand_complex_eq = complex_eq_iff