tuned
authorhuffman
Mon May 14 18:03:25 2007 +0200 (2007-05-14)
changeset 229687134874437ac
parent 22967 0651b224528a
child 22969 bf523cac9a05
tuned
src/HOL/Complex/Complex.thy
src/HOL/Hyperreal/NthRoot.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Mon May 14 17:45:42 2007 +0200
     1.2 +++ b/src/HOL/Complex/Complex.thy	Mon May 14 18:03:25 2007 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4  lemma complex_Im_zero [simp]: "Im 0 = 0"
     1.5  by (simp add: complex_zero_def)
     1.6  
     1.7 -lemma complex_zero_iff [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)"
     1.8 -unfolding complex_zero_def by simp
     1.9 +lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)"
    1.10 +by (simp add: complex_zero_def)
    1.11  
    1.12  lemma complex_Re_one [simp]: "Re 1 = 1"
    1.13  by (simp add: complex_one_def)
    1.14 @@ -76,12 +76,18 @@
    1.15  lemma complex_Im_one [simp]: "Im 1 = 0"
    1.16  by (simp add: complex_one_def)
    1.17  
    1.18 +lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 \<and> y = 0)"
    1.19 +by (simp add: complex_one_def)
    1.20 +
    1.21  lemma complex_Re_i [simp]: "Re(ii) = 0"
    1.22  by (simp add: i_def)
    1.23  
    1.24  lemma complex_Im_i [simp]: "Im(ii) = 1"
    1.25  by (simp add: i_def)
    1.26  
    1.27 +lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
    1.28 +by (simp add: i_def)
    1.29 +
    1.30  
    1.31  subsection{*Unary Minus*}
    1.32  
    1.33 @@ -156,16 +162,12 @@
    1.34  subsection{*Inverse*}
    1.35  
    1.36  lemma complex_inverse [simp]:
    1.37 -     "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
    1.38 +  "inverse (Complex x y) = Complex (x / (x\<twosuperior> + y\<twosuperior>)) (- y / (x\<twosuperior> + y\<twosuperior>))"
    1.39  by (simp add: complex_inverse_def)
    1.40  
    1.41  lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
    1.42  apply (induct z)
    1.43 -apply (rename_tac x y)
    1.44 -apply (auto simp add:
    1.45 -             complex_one_def complex_zero_def add_divide_distrib [symmetric] 
    1.46 -             power2_eq_square mult_ac)
    1.47 -apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) 
    1.48 +apply (simp add: power2_eq_square [symmetric] add_divide_distrib [symmetric])
    1.49  done
    1.50  
    1.51  
    1.52 @@ -510,17 +512,6 @@
    1.53       "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
    1.54  by (simp add: complex_of_real_def)
    1.55  
    1.56 -lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
    1.57 -by (simp add: complex_zero_def)
    1.58 -
    1.59 -lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
    1.60 -by (simp add: complex_one_def)
    1.61 -
    1.62 -lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
    1.63 -by (simp add: i_def)
    1.64 -
    1.65 -
    1.66 -
    1.67  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
    1.68  proof (induct z)
    1.69    case (Complex x y)
     2.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 17:45:42 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 18:03:25 2007 +0200
     2.3 @@ -475,7 +475,7 @@
     2.4  subsection {* Square Root of Sum of Squares *}
     2.5  
     2.6  lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
     2.7 -by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero])
     2.8 +by (rule real_sqrt_ge_zero [OF sum_squares_ge_zero])
     2.9  
    2.10  lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    2.11  by simp