src/HOL/Complex/Complex.thy
changeset 14341 a09441bd4f1e
parent 14335 9c0b5e081037
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Complex/Complex.thy	Tue Jan 06 10:38:14 2004 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Tue Jan 06 10:40:15 2004 +0100
     1.3 @@ -343,20 +343,18 @@
     1.4  done
     1.5  declare complex_add_minus_right_zero [simp]
     1.6  
     1.7 -lemma complex_add_minus_left_zero:
     1.8 +lemma complex_add_minus_left:
     1.9        "-z + z = (0::complex)"
    1.10  apply (unfold complex_add_def complex_minus_def complex_zero_def)
    1.11  apply (simp (no_asm))
    1.12  done
    1.13 -declare complex_add_minus_left_zero [simp]
    1.14  
    1.15  lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
    1.16  apply (simp (no_asm) add: complex_add_assoc [symmetric])
    1.17  done
    1.18  
    1.19  lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
    1.20 -apply (simp (no_asm) add: complex_add_assoc [symmetric])
    1.21 -done
    1.22 +by (simp add: complex_add_minus_left complex_add_assoc [symmetric])
    1.23  
    1.24  declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]
    1.25  
    1.26 @@ -373,7 +371,7 @@
    1.27  lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"
    1.28  apply safe
    1.29  apply (drule_tac f = "%t.-x + t" in arg_cong)
    1.30 -apply (simp add: complex_add_assoc [symmetric])
    1.31 +apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])
    1.32  done
    1.33  declare complex_add_left_cancel [iff]
    1.34  
    1.35 @@ -413,7 +411,7 @@
    1.36  done
    1.37  
    1.38  lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"
    1.39 -by (auto simp add: complex_diff_def complex_add_assoc)
    1.40 +by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)
    1.41  
    1.42  
    1.43  subsection{*Multiplication*}
    1.44 @@ -552,7 +550,7 @@
    1.45    show "0 + z = z"
    1.46      by (rule complex_add_zero_left) 
    1.47    show "-z + z = 0"
    1.48 -    by (rule complex_add_minus_left_zero) 
    1.49 +    by (rule complex_add_minus_left) 
    1.50    show "z - w = z + -w"
    1.51      by (simp add: complex_diff_def)
    1.52    show "(u * v) * w = u * (v * w)"
    1.53 @@ -561,10 +559,16 @@
    1.54      by (rule complex_mult_commute) 
    1.55    show "1 * z = z"
    1.56      by (rule complex_mult_one_left) 
    1.57 -  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
    1.58 +  show "0 \<noteq> (1::complex)"
    1.59      by (rule complex_zero_not_eq_one) 
    1.60    show "(u + v) * w = u * w + v * w"
    1.61      by (rule complex_add_mult_distrib) 
    1.62 +  show "z+u = z+v ==> u=v"
    1.63 +    proof -
    1.64 +      assume eq: "z+u = z+v" 
    1.65 +      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
    1.66 +      thus "u = v" by (simp add: complex_add_minus_left)
    1.67 +    qed
    1.68    assume neq: "w \<noteq> 0"
    1.69    thus "z / w = z * inverse w"
    1.70      by (simp add: complex_divide_def)
    1.71 @@ -1700,7 +1704,6 @@
    1.72  val complex_add_zero_left = thm"complex_add_zero_left";
    1.73  val complex_add_zero_right = thm"complex_add_zero_right";
    1.74  val complex_add_minus_right_zero = thm"complex_add_minus_right_zero";
    1.75 -val complex_add_minus_left_zero = thm"complex_add_minus_left_zero";
    1.76  val complex_add_minus_cancel = thm"complex_add_minus_cancel";
    1.77  val complex_minus_add_cancel = thm"complex_minus_add_cancel";
    1.78  val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus";