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
```