author huffman Mon Aug 08 10:26:26 2011 -0700 (2011-08-08) changeset 44065 eb64ffccfc75 parent 44064 5bce8ff0d9ae child 44066 d74182c93f04
standard theorem naming scheme: complex_eqI, complex_eq_iff
 src/HOL/Complex.thy file | annotate | diff | revisions
```     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.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.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.64
1.65  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
1.68
1.69  lemma complex_i_not_one [simp]: "ii \<noteq> 1"
1.72
1.73  lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w"
1.76
1.77  lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
1.80
1.81  lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"
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.89
1.90  lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
1.93
1.94  lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
1.96
1.97  lemma complex_cnj_zero [simp]: "cnj 0 = 0"
1.100
1.101  lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
1.104
1.105  lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
1.108
1.109  lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
1.112
1.113  lemma complex_cnj_minus: "cnj (- x) = - cnj x"
1.116
1.117  lemma complex_cnj_one [simp]: "cnj 1 = 1"
1.120
1.121  lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
1.124
1.125  lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
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.133
1.134  lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
1.137
1.138  lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w"
1.141
1.142  lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
1.145
1.146  lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
1.148
1.149  lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
1.152
1.153  lemma complex_cnj_i [simp]: "cnj ii = - ii"
1.156
1.157  lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
1.160
1.161  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
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
```