author huffman Mon, 14 May 2007 18:03:25 +0200 changeset 22968 7134874437ac parent 22967 0651b224528a child 22969 bf523cac9a05
tuned
 src/HOL/Complex/Complex.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/NthRoot.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complex/Complex.thy	Mon May 14 17:45:42 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Mon May 14 18:03:25 2007 +0200
@@ -67,8 +67,8 @@
lemma complex_Im_zero [simp]: "Im 0 = 0"

-lemma complex_zero_iff [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)"
-unfolding complex_zero_def by simp
+lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)"

lemma complex_Re_one [simp]: "Re 1 = 1"
@@ -76,12 +76,18 @@
lemma complex_Im_one [simp]: "Im 1 = 0"

+lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 \<and> y = 0)"
+
lemma complex_Re_i [simp]: "Re(ii) = 0"

lemma complex_Im_i [simp]: "Im(ii) = 1"

+lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
+

subsection{*Unary Minus*}

@@ -156,16 +162,12 @@
subsection{*Inverse*}

lemma complex_inverse [simp]:
-     "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
+  "inverse (Complex x y) = Complex (x / (x\<twosuperior> + y\<twosuperior>)) (- y / (x\<twosuperior> + y\<twosuperior>))"

lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
apply (induct z)
-apply (rename_tac x y)
-             power2_eq_square mult_ac)
done

@@ -510,17 +512,6 @@
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)"

-lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
-
-lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
-
-lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
-
-
-
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
proof (induct z)
case (Complex x y)```
```--- a/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 17:45:42 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 18:03:25 2007 +0200
@@ -475,7 +475,7 @@
subsection {* Square Root of Sum of Squares *}

lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
-by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero])
+by (rule real_sqrt_ge_zero [OF sum_squares_ge_zero])

lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
by simp```