src/HOL/Complex/Complex.thy
changeset 14335 9c0b5e081037
parent 14334 6137d24eef79
child 14341 a09441bd4f1e
     1.1 --- a/src/HOL/Complex/Complex.thy	Thu Jan 01 10:06:32 2004 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Thu Jan 01 21:47:07 2004 +0100
     1.3 @@ -483,28 +483,6 @@
     1.4  apply (auto simp add: complex_mult complex_minus real_diff_def)
     1.5  done
     1.6  
     1.7 -declare complex_minus_mult_eq1 [symmetric, simp] complex_minus_mult_eq2 [symmetric, simp]
     1.8 -
     1.9 -lemma complex_mult_minus_one: "-(1::complex) * z = -z"
    1.10 -apply (simp (no_asm))
    1.11 -done
    1.12 -declare complex_mult_minus_one [simp]
    1.13 -
    1.14 -lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
    1.15 -apply (subst complex_mult_commute)
    1.16 -apply (simp (no_asm))
    1.17 -done
    1.18 -declare complex_mult_minus_one_right [simp]
    1.19 -
    1.20 -lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
    1.21 -apply (simp (no_asm))
    1.22 -done
    1.23 -declare complex_minus_mult_cancel [simp]
    1.24 -
    1.25 -lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
    1.26 -apply (simp (no_asm))
    1.27 -done
    1.28 -
    1.29  lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)"
    1.30  apply (rule_tac z = z1 in eq_Abs_complex)
    1.31  apply (rule_tac z = z2 in eq_Abs_complex)
    1.32 @@ -541,6 +519,13 @@
    1.33  apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO)
    1.34  done
    1.35  
    1.36 +instance complex :: division_by_zero
    1.37 +proof
    1.38 +  fix x :: complex
    1.39 +  show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO)
    1.40 +  show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 
    1.41 +qed
    1.42 +
    1.43  lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
    1.44  apply (rule_tac z = z in eq_Abs_complex)
    1.45  apply (auto simp add: complex_mult complex_inverse complex_one_def 
    1.46 @@ -554,6 +539,61 @@
    1.47  by (auto intro: complex_mult_commute [THEN subst])
    1.48  declare complex_mult_inv_right [simp]
    1.49  
    1.50 +
    1.51 +subsection {* The field of complex numbers *}
    1.52 +
    1.53 +instance complex :: field
    1.54 +proof
    1.55 +  fix z u v w :: complex
    1.56 +  show "(u + v) + w = u + (v + w)"
    1.57 +    by (rule complex_add_assoc) 
    1.58 +  show "z + w = w + z"
    1.59 +    by (rule complex_add_commute) 
    1.60 +  show "0 + z = z"
    1.61 +    by (rule complex_add_zero_left) 
    1.62 +  show "-z + z = 0"
    1.63 +    by (rule complex_add_minus_left_zero) 
    1.64 +  show "z - w = z + -w"
    1.65 +    by (simp add: complex_diff_def)
    1.66 +  show "(u * v) * w = u * (v * w)"
    1.67 +    by (rule complex_mult_assoc) 
    1.68 +  show "z * w = w * z"
    1.69 +    by (rule complex_mult_commute) 
    1.70 +  show "1 * z = z"
    1.71 +    by (rule complex_mult_one_left) 
    1.72 +  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
    1.73 +    by (rule complex_zero_not_eq_one) 
    1.74 +  show "(u + v) * w = u * w + v * w"
    1.75 +    by (rule complex_add_mult_distrib) 
    1.76 +  assume neq: "w \<noteq> 0"
    1.77 +  thus "z / w = z * inverse w"
    1.78 +    by (simp add: complex_divide_def)
    1.79 +  show "inverse w * w = 1"
    1.80 +    by (simp add: neq complex_mult_inv_left) 
    1.81 +qed
    1.82 +
    1.83 +
    1.84 +lemma complex_mult_minus_one: "-(1::complex) * z = -z"
    1.85 +apply (simp (no_asm))
    1.86 +done
    1.87 +declare complex_mult_minus_one [simp]
    1.88 +
    1.89 +lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
    1.90 +apply (subst complex_mult_commute)
    1.91 +apply (simp (no_asm))
    1.92 +done
    1.93 +declare complex_mult_minus_one_right [simp]
    1.94 +
    1.95 +lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
    1.96 +apply (simp (no_asm))
    1.97 +done
    1.98 +declare complex_minus_mult_cancel [simp]
    1.99 +
   1.100 +lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
   1.101 +apply (simp (no_asm))
   1.102 +done
   1.103 +
   1.104 +
   1.105  lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)"
   1.106  apply auto
   1.107  apply (drule_tac f = "%x. x*inverse c" in arg_cong)
   1.108 @@ -603,11 +643,7 @@
   1.109  done
   1.110  
   1.111  lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)"
   1.112 -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
   1.113 -apply (case_tac "y = 0", simp add: COMPLEX_INVERSE_ZERO)
   1.114 -apply (rule_tac c1 = "x*y" in complex_mult_left_cancel [THEN iffD1])
   1.115 -apply (auto simp add: complex_mult_not_zero complex_mult_ac)
   1.116 -apply (auto simp add: complex_mult_not_zero complex_mult_assoc [symmetric])
   1.117 +apply (rule inverse_mult_distrib) 
   1.118  done
   1.119  
   1.120