prove existence, uniqueness, and other properties of complex arg function
authorhuffman
Thu Sep 08 08:41:28 2011 -0700 (2011-09-08)
changeset 44844f74a4175a3a8
parent 44843 93d0f85cfe4a
child 44845 5e51075cbd97
child 44846 e9d1fcbc7d20
prove existence, uniqueness, and other properties of complex arg function
src/HOL/Complex.thy
     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.92 +    by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
    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.95 +      simp add: cis_def)
    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