standard theorem naming scheme: complex_eqI, complex_eq_iff
authorhuffman
Mon Aug 08 10:26:26 2011 -0700 (2011-08-08)
changeset 44065eb64ffccfc75
parent 44064 5bce8ff0d9ae
child 44066 d74182c93f04
standard theorem naming scheme: complex_eqI, complex_eq_iff
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Mon Aug 08 09:52:09 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Mon Aug 08 10:26:26 2011 -0700
     1.3 @@ -25,14 +25,12 @@
     1.4  lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
     1.5    by (induct z) simp
     1.6  
     1.7 -lemma complex_equality [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
     1.8 +lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
     1.9    by (induct x, induct y) simp
    1.10  
    1.11 -lemma expand_complex_eq: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
    1.12 +lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
    1.13    by (induct x, induct y) simp
    1.14  
    1.15 -lemmas complex_Re_Im_cancel_iff = expand_complex_eq
    1.16 -
    1.17  
    1.18  subsection {* Addition and Subtraction *}
    1.19  
    1.20 @@ -152,7 +150,7 @@
    1.21    right_distrib left_distrib right_diff_distrib left_diff_distrib
    1.22    complex_inverse_def complex_divide_def
    1.23    power2_eq_square add_divide_distrib [symmetric]
    1.24 -  expand_complex_eq)
    1.25 +  complex_eq_iff)
    1.26  
    1.27  end
    1.28  
    1.29 @@ -190,7 +188,7 @@
    1.30  
    1.31  lemma Complex_eq_number_of [simp]:
    1.32    "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
    1.33 -by (simp add: expand_complex_eq)
    1.34 +by (simp add: complex_eq_iff)
    1.35  
    1.36  
    1.37  subsection {* Scalar Multiplication *}
    1.38 @@ -215,17 +213,17 @@
    1.39  proof
    1.40    fix a b :: real and x y :: complex
    1.41    show "scaleR a (x + y) = scaleR a x + scaleR a y"
    1.42 -    by (simp add: expand_complex_eq right_distrib)
    1.43 +    by (simp add: complex_eq_iff right_distrib)
    1.44    show "scaleR (a + b) x = scaleR a x + scaleR b x"
    1.45 -    by (simp add: expand_complex_eq left_distrib)
    1.46 +    by (simp add: complex_eq_iff left_distrib)
    1.47    show "scaleR a (scaleR b x) = scaleR (a * b) x"
    1.48 -    by (simp add: expand_complex_eq mult_assoc)
    1.49 +    by (simp add: complex_eq_iff mult_assoc)
    1.50    show "scaleR 1 x = x"
    1.51 -    by (simp add: expand_complex_eq)
    1.52 +    by (simp add: complex_eq_iff)
    1.53    show "scaleR a x * y = scaleR a (x * y)"
    1.54 -    by (simp add: expand_complex_eq algebra_simps)
    1.55 +    by (simp add: complex_eq_iff algebra_simps)
    1.56    show "x * scaleR a y = scaleR a (x * y)"
    1.57 -    by (simp add: expand_complex_eq algebra_simps)
    1.58 +    by (simp add: complex_eq_iff algebra_simps)
    1.59  qed
    1.60  
    1.61  end
    1.62 @@ -405,19 +403,19 @@
    1.63  by (simp add: i_def)
    1.64  
    1.65  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
    1.66 -by (simp add: expand_complex_eq)
    1.67 +by (simp add: complex_eq_iff)
    1.68  
    1.69  lemma complex_i_not_one [simp]: "ii \<noteq> 1"
    1.70 -by (simp add: expand_complex_eq)
    1.71 +by (simp add: complex_eq_iff)
    1.72  
    1.73  lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w"
    1.74 -by (simp add: expand_complex_eq)
    1.75 +by (simp add: complex_eq_iff)
    1.76  
    1.77  lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
    1.78 -by (simp add: expand_complex_eq)
    1.79 +by (simp add: complex_eq_iff)
    1.80  
    1.81  lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"
    1.82 -by (simp add: expand_complex_eq)
    1.83 +by (simp add: complex_eq_iff)
    1.84  
    1.85  lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
    1.86  by (simp add: i_def complex_of_real_def)
    1.87 @@ -451,31 +449,31 @@
    1.88  by (simp add: cnj_def)
    1.89  
    1.90  lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
    1.91 -by (simp add: expand_complex_eq)
    1.92 +by (simp add: complex_eq_iff)
    1.93  
    1.94  lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
    1.95  by (simp add: cnj_def)
    1.96  
    1.97  lemma complex_cnj_zero [simp]: "cnj 0 = 0"
    1.98 -by (simp add: expand_complex_eq)
    1.99 +by (simp add: complex_eq_iff)
   1.100  
   1.101  lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
   1.102 -by (simp add: expand_complex_eq)
   1.103 +by (simp add: complex_eq_iff)
   1.104  
   1.105  lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
   1.106 -by (simp add: expand_complex_eq)
   1.107 +by (simp add: complex_eq_iff)
   1.108  
   1.109  lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
   1.110 -by (simp add: expand_complex_eq)
   1.111 +by (simp add: complex_eq_iff)
   1.112  
   1.113  lemma complex_cnj_minus: "cnj (- x) = - cnj x"
   1.114 -by (simp add: expand_complex_eq)
   1.115 +by (simp add: complex_eq_iff)
   1.116  
   1.117  lemma complex_cnj_one [simp]: "cnj 1 = 1"
   1.118 -by (simp add: expand_complex_eq)
   1.119 +by (simp add: complex_eq_iff)
   1.120  
   1.121  lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
   1.122 -by (simp add: expand_complex_eq)
   1.123 +by (simp add: complex_eq_iff)
   1.124  
   1.125  lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
   1.126  by (simp add: complex_inverse_def)
   1.127 @@ -487,34 +485,34 @@
   1.128  by (induct n, simp_all add: complex_cnj_mult)
   1.129  
   1.130  lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
   1.131 -by (simp add: expand_complex_eq)
   1.132 +by (simp add: complex_eq_iff)
   1.133  
   1.134  lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
   1.135 -by (simp add: expand_complex_eq)
   1.136 +by (simp add: complex_eq_iff)
   1.137  
   1.138  lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w"
   1.139 -by (simp add: expand_complex_eq)
   1.140 +by (simp add: complex_eq_iff)
   1.141  
   1.142  lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
   1.143 -by (simp add: expand_complex_eq)
   1.144 +by (simp add: complex_eq_iff)
   1.145  
   1.146  lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
   1.147  by (simp add: complex_norm_def)
   1.148  
   1.149  lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
   1.150 -by (simp add: expand_complex_eq)
   1.151 +by (simp add: complex_eq_iff)
   1.152  
   1.153  lemma complex_cnj_i [simp]: "cnj ii = - ii"
   1.154 -by (simp add: expand_complex_eq)
   1.155 +by (simp add: complex_eq_iff)
   1.156  
   1.157  lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
   1.158 -by (simp add: expand_complex_eq)
   1.159 +by (simp add: complex_eq_iff)
   1.160  
   1.161  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
   1.162 -by (simp add: expand_complex_eq)
   1.163 +by (simp add: complex_eq_iff)
   1.164  
   1.165  lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
   1.166 -by (simp add: expand_complex_eq power2_eq_square)
   1.167 +by (simp add: complex_eq_iff power2_eq_square)
   1.168  
   1.169  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
   1.170  by (simp add: norm_mult power2_eq_square)
   1.171 @@ -721,4 +719,10 @@
   1.172  lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
   1.173  by (simp add: expi_def cis_def)
   1.174  
   1.175 +text {* Legacy theorem names *}
   1.176 +
   1.177 +lemmas expand_complex_eq = complex_eq_iff
   1.178 +lemmas complex_Re_Im_cancel_iff = complex_eq_iff
   1.179 +lemmas complex_equality = complex_eqI
   1.180 +
   1.181  end