src/HOL/Complex.thy
 changeset 53015 a1119cf551e8 parent 51002 496013a6eb38 child 53374 a14d2a854c02
```     1.1 --- a/src/HOL/Complex.thy	Tue Aug 13 14:20:22 2013 +0200
1.2 +++ b/src/HOL/Complex.thy	Tue Aug 13 16:25:47 2013 +0200
1.3 @@ -103,7 +103,7 @@
1.4
1.5  definition complex_inverse_def:
1.6    "inverse x =
1.7 -    Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
1.8 +    Complex (Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)) (- Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2))"
1.9
1.10  definition complex_divide_def:
1.11    "x / (y\<Colon>complex) = x * inverse y"
1.12 @@ -128,15 +128,15 @@
1.14
1.15  lemma complex_inverse [simp]:
1.16 -  "inverse (Complex a b) = Complex (a / (a\<twosuperior> + b\<twosuperior>)) (- b / (a\<twosuperior> + b\<twosuperior>))"
1.17 +  "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
1.19
1.20  lemma complex_Re_inverse:
1.21 -  "Re (inverse x) = Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)"
1.22 +  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
1.24
1.25  lemma complex_Im_inverse:
1.26 -  "Im (inverse x) = - Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)"
1.27 +  "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
1.29
1.30  instance
1.31 @@ -267,7 +267,7 @@
1.32  begin
1.33
1.34  definition complex_norm_def:
1.35 -  "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
1.36 +  "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
1.37
1.38  abbreviation cmod :: "complex \<Rightarrow> real"
1.39    where "cmod \<equiv> norm"
1.40 @@ -283,7 +283,7 @@
1.41
1.42  lemmas cmod_def = complex_norm_def
1.43
1.44 -lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
1.45 +lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
1.47
1.48  instance proof
1.49 @@ -439,7 +439,7 @@
1.50  lemma i_squared [simp]: "ii * ii = -1"
1.52
1.53 -lemma power2_i [simp]: "ii\<twosuperior> = -1"
1.54 +lemma power2_i [simp]: "ii\<^sup>2 = -1"
1.56
1.57  lemma inverse_i [simp]: "inverse ii = - ii"
1.58 @@ -529,10 +529,10 @@
1.59  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"