
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -291,35 +291,33 @@
      "(complex_of_real x = complex_of_real y) = (x = y)"
 by (simp add: complex_of_real_def)
 
-lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
+lemma complex_of_real_minus [simp]: "complex_of_real(-x) = - complex_of_real x"
 by (simp add: complex_of_real_def complex_minus)
 
-lemma complex_of_real_inverse:
+lemma complex_of_real_inverse [simp]:
      "complex_of_real(inverse x) = inverse(complex_of_real x)"
 apply (case_tac "x=0", simp)
-apply (simp add: complex_inverse complex_of_real_def real_divide_def
-                 inverse_mult_distrib power2_eq_square)
+apply (simp add: complex_of_real_def divide_inverse power2_eq_square)
 done
 
-lemma complex_of_real_add:
-     "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
+lemma complex_of_real_add [simp]:
+     "complex_of_real (x + y) = complex_of_real x + complex_of_real y"
 by (simp add: complex_add complex_of_real_def)
 
-lemma complex_of_real_diff:
-     "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
-by (simp add: complex_of_real_minus [symmetric] complex_diff_def 
-              complex_of_real_add)
+lemma complex_of_real_diff [simp]:
+     "complex_of_real (x - y) = complex_of_real x - complex_of_real y"
+by (simp add: complex_of_real_minus diff_minus)
 
-lemma complex_of_real_mult:
-     "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
+lemma complex_of_real_mult [simp]:
+     "complex_of_real (x * y) = complex_of_real x * complex_of_real y"
 by (simp add: complex_mult complex_of_real_def)
 
-lemma complex_of_real_divide:
-      "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
+lemma complex_of_real_divide [simp]:
+      "complex_of_real(x/y) = complex_of_real x / complex_of_real y"
 apply (simp add: complex_divide_def)
 apply (case_tac "y=0", simp)
-apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse 
-                 real_divide_def)
+apply (simp add: complex_of_real_mult complex_of_real_inverse 
+                 divide_inverse)
 done
 
 lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
@@ -407,7 +405,7 @@
 by (induct w, induct z, simp add: complex_cnj complex_add)
 
 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
-by (simp add: complex_diff_def complex_cnj_add complex_cnj_minus)
+by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
 
 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
 by (induct w, induct z, simp add: complex_cnj complex_mult)
@@ -423,7 +421,7 @@
 
 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
 apply (induct z)
-apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
+apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
                  complex_minus i_def complex_mult)
 done
 
@@ -561,7 +559,7 @@
 done
 
 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
-by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
+by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse)
 
 
 subsection{*Exponentiation*}
@@ -639,24 +637,33 @@
 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
 by (simp add: i_def)
 
+
+
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+  case (Complex x y)
+    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+    thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
+       by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
+
 
 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+  case (Complex x y)
+    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+    thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
+       by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
 
 lemma complex_inverse_complex_split:
      "inverse(complex_of_real x + ii * complex_of_real y) =
       complex_of_real(x/(x ^ 2 + y ^ 2)) -
       ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
 by (simp add: complex_of_real_def i_def complex_mult complex_add
-         complex_diff_def complex_minus complex_inverse real_divide_def)
+         diff_minus complex_minus complex_inverse divide_inverse)
 
 (*----------------------------------------------------------------------------*)
 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
@@ -738,7 +745,8 @@
 by (simp add: rcis_def)
 
 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
+by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
+              complex_of_real_def)
 
 lemma cis_mult: "cis a * cis b = cis (a + b)"
 by (simp add: cis_rcis_eq rcis_mult)
@@ -774,7 +782,7 @@
 
 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
 by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus 
-              complex_diff_def)
+              diff_minus)
 
 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
 by (simp add: divide_inverse rcis_def complex_of_real_inverse)
@@ -818,33 +826,31 @@
 
 instance complex :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::complex)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance complex :: number_ring
-proof
-  show "Numeral0 = (0::complex)" by (rule number_of_Pls)
-  show "-1 = - (1::complex)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: complex) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
+by (intro_classes, simp add: complex_number_of_def) 
+
+
+lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
+by (induct n, simp_all) 
+
+lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
+proof (cases z)
+  case (1 n)
+    thus ?thesis by simp
+next
+  case (2 n)
+    thus ?thesis 
+      by (simp only: of_int_minus complex_of_real_minus, simp)
 qed
 
 
 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
-apply (induct w) 
-apply (simp_all only: number_of complex_of_real_add [symmetric] 
-                      complex_of_real_minus, simp_all) 
-done
+by (simp add: complex_number_of_def real_number_of_def) 
 
 text{*This theorem is necessary because theorems such as
    @{text iszero_number_of_0} only hold for ordered rings. They cannot
@@ -855,50 +861,6 @@
 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
                iszero_def)  
 
-
-(*These allow simplification of expressions involving mixed numbers.
-  Convert???
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya =  
-        number_of xb) =  
-   (((number_of xa :: complex) = number_of xb) &  
-    ((number_of ya :: complex) = 0))"
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2";
-Addsimps [complex_number_of_eq_cancel_iff2];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii = \
-\       number_of xb) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = 0))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2a,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2a";
-Addsimps [complex_number_of_eq_cancel_iff2a];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya = \
-\    ii * number_of yb) = \
-\  (((number_of xa :: complex) = 0) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3";
-Addsimps [complex_number_of_eq_cancel_iff3];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii= \
-\    ii * number_of yb) = \
-\  (((number_of xa :: complex) = 0) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3a,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3a";
-Addsimps [complex_number_of_eq_cancel_iff3a];
-*)
-
 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
 apply (subst complex_number_of [symmetric])
 apply (rule complex_cnj_complex_of_real)
@@ -957,7 +919,6 @@
 val complex_zero_def = thm"complex_zero_def";
 val complex_one_def = thm"complex_one_def";
 val complex_minus_def = thm"complex_minus_def";
-val complex_diff_def = thm"complex_diff_def";
 val complex_divide_def = thm"complex_divide_def";
 val complex_mult_def = thm"complex_mult_def";
 val complex_add_def = thm"complex_add_def";




