src/HOL/Complex.thy
 changeset 54489 03ff4d1e6784 parent 54230 b1d955791529 child 55734 3f5b2745d659
```     1.1 --- a/src/HOL/Complex.thy	Tue Nov 19 01:30:14 2013 +0100
1.2 +++ b/src/HOL/Complex.thy	Tue Nov 19 10:05:53 2013 +0100
1.3 @@ -108,7 +108,12 @@
1.4  definition complex_divide_def:
1.5    "x / (y\<Colon>complex) = x * inverse y"
1.6
1.7 -lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
1.8 +lemma Complex_eq_1 [simp]:
1.9 +  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
1.10 +  by (simp add: complex_one_def)
1.11 +
1.12 +lemma Complex_eq_neg_1 [simp]:
1.13 +  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
1.15
1.16  lemma complex_Re_one [simp]: "Re 1 = 1"
1.17 @@ -166,21 +171,21 @@
1.18  lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
1.19    using complex_Re_of_int [of "numeral v"] by simp
1.20
1.21 -lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
1.22 -  using complex_Re_of_int [of "neg_numeral v"] by simp
1.23 +lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
1.24 +  using complex_Re_of_int [of "- numeral v"] by simp
1.25
1.26  lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
1.27    using complex_Im_of_int [of "numeral v"] by simp
1.28
1.29 -lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
1.30 -  using complex_Im_of_int [of "neg_numeral v"] by simp
1.31 +lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
1.32 +  using complex_Im_of_int [of "- numeral v"] by simp
1.33
1.34  lemma Complex_eq_numeral [simp]:
1.35 -  "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
1.36 +  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
1.38
1.39  lemma Complex_eq_neg_numeral [simp]:
1.40 -  "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
1.41 +  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
1.43
1.44
1.45 @@ -421,7 +426,7 @@
1.46  lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
1.48
1.49 -lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
1.50 +lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"