author huffman Mon, 08 Aug 2011 10:26:26 -0700 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 | comparison | revisions
```--- a/src/HOL/Complex.thy	Mon Aug 08 09:52:09 2011 -0700
+++ b/src/HOL/Complex.thy	Mon Aug 08 10:26:26 2011 -0700
@@ -25,14 +25,12 @@
lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
by (induct z) simp

-lemma complex_equality [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
+lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
by (induct x, induct y) simp

-lemma expand_complex_eq: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
+lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
by (induct x, induct y) simp

-lemmas complex_Re_Im_cancel_iff = expand_complex_eq
-

subsection {* Addition and Subtraction *}

@@ -152,7 +150,7 @@
right_distrib left_distrib right_diff_distrib left_diff_distrib
complex_inverse_def complex_divide_def
-  expand_complex_eq)
+  complex_eq_iff)

end

@@ -190,7 +188,7 @@

lemma Complex_eq_number_of [simp]:
"(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"

subsection {* Scalar Multiplication *}
@@ -215,17 +213,17 @@
proof
fix a b :: real and x y :: complex
show "scaleR a (x + y) = scaleR a x + scaleR a y"
-    by (simp add: expand_complex_eq right_distrib)
+    by (simp add: complex_eq_iff right_distrib)
show "scaleR (a + b) x = scaleR a x + scaleR b x"
-    by (simp add: expand_complex_eq left_distrib)
+    by (simp add: complex_eq_iff left_distrib)
show "scaleR a (scaleR b x) = scaleR (a * b) x"
-    by (simp add: expand_complex_eq mult_assoc)
+    by (simp add: complex_eq_iff mult_assoc)
show "scaleR 1 x = x"
show "scaleR a x * y = scaleR a (x * y)"
-    by (simp add: expand_complex_eq algebra_simps)
+    by (simp add: complex_eq_iff algebra_simps)
show "x * scaleR a y = scaleR a (x * y)"
-    by (simp add: expand_complex_eq algebra_simps)
+    by (simp add: complex_eq_iff algebra_simps)
qed

end
@@ -405,19 +403,19 @@

lemma complex_i_not_zero [simp]: "ii \<noteq> 0"

lemma complex_i_not_one [simp]: "ii \<noteq> 1"

lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w"

lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"

lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"

lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
@@ -451,31 +449,31 @@

lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"

lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"

lemma complex_cnj_zero [simp]: "cnj 0 = 0"

lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"

lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"

lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"

lemma complex_cnj_minus: "cnj (- x) = - cnj x"

lemma complex_cnj_one [simp]: "cnj 1 = 1"

lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"

lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
@@ -487,34 +485,34 @@
by (induct n, simp_all add: complex_cnj_mult)

lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"

lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"

lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w"

lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"

lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"

lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"

lemma complex_cnj_i [simp]: "cnj ii = - ii"

lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"

lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"

lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"

lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"