Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Complex.thy
changeset 54489 03ff4d1e6784
parent 54230 b1d955791529
child 55734 3f5b2745d659 
--- a/src/HOL/Complex.thy	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Complex.thy	Tue Nov 19 10:05:53 2013 +0100
@@ -108,7 +108,12 @@
 definition complex_divide_def:
   "x / (y\<Colon>complex) = x * inverse y"
 
-lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
+lemma Complex_eq_1 [simp]:
+  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
+  by (simp add: complex_one_def)
+
+lemma Complex_eq_neg_1 [simp]:
+  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
   by (simp add: complex_one_def)
 
 lemma complex_Re_one [simp]: "Re 1 = 1"
@@ -166,21 +171,21 @@
 lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
   using complex_Re_of_int [of "numeral v"] by simp
 
-lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
-  using complex_Re_of_int [of "neg_numeral v"] by simp
+lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
+  using complex_Re_of_int [of "- numeral v"] by simp
 
 lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
   using complex_Im_of_int [of "numeral v"] by simp
 
-lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
-  using complex_Im_of_int [of "neg_numeral v"] by simp
+lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
+  using complex_Im_of_int [of "- numeral v"] by simp
 
 lemma Complex_eq_numeral [simp]:
-  "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
+  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
   by (simp add: complex_eq_iff)
 
 lemma Complex_eq_neg_numeral [simp]:
-  "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
+  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
   by (simp add: complex_eq_iff)
 
 
@@ -421,7 +426,7 @@
 lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
   by (simp add: complex_eq_iff)
 
-lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
+lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
   by (simp add: complex_eq_iff)
 
 lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
@@ -508,7 +513,7 @@
 lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
   by (simp add: complex_eq_iff)
 
-lemma complex_cnj_neg_numeral [simp]: "cnj (neg_numeral w) = neg_numeral w"
+lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
   by (simp add: complex_eq_iff)
 
 lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
isabelle