# HG changeset patch
# User huffman
# Date 1158426877 -7200
# Node ID 2e8227b81bf16b372ff620c01ffbb31af1f92994
# Parent  055d9a1bbddf8cd874a048c8f2f61984c90a92a1
add instance for real_algebra_1 and real_normed_div_algebra

diff -r 055d9a1bbddf -r 2e8227b81bf1 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Sat Sep 16 19:12:54 2006 +0200
+++ b/src/HOL/Complex/Complex.thy	Sat Sep 16 19:14:37 2006 +0200
@@ -259,6 +259,32 @@
 qed
 
 
+subsection{*The real algebra of complex numbers*}
+
+instance complex :: scaleR ..
+
+defs (overloaded)
+  complex_scaleR_def: "r *# x == Complex r 0 * x"
+
+instance complex :: real_algebra_1
+proof
+  fix a b :: real
+  fix x y :: complex
+  show "a *# (x + y) = a *# x + a *# y"
+    by (simp add: complex_scaleR_def right_distrib)
+  show "(a + b) *# x = a *# x + b *# x"
+    by (simp add: complex_scaleR_def left_distrib [symmetric])
+  show "(a * b) *# x = a *# b *# x"
+    by (simp add: complex_scaleR_def mult_assoc [symmetric])
+  show "1 *# x = x"
+    by (simp add: complex_scaleR_def complex_one_def [symmetric])
+  show "a *# x * y = a *# (x * y)"
+    by (simp add: complex_scaleR_def mult_assoc)
+  show "x * a *# y = a *# (x * y)"
+    by (simp add: complex_scaleR_def mult_left_commute)
+qed
+
+
 subsection{*Embedding Properties for @{term complex_of_real} Map*}
 
 lemma Complex_add_complex_of_real [simp]:
@@ -553,6 +579,34 @@
 done
 
 
+subsection{*The normed division algebra of complex numbers*}
+
+instance complex :: norm ..
+
+defs (overloaded)
+  complex_norm_def: "norm == cmod"
+
+lemma of_real_complex_of_real: "of_real r = complex_of_real r"
+by (simp add: complex_of_real_def of_real_def complex_scaleR_def)
+
+instance complex :: real_normed_div_algebra
+proof (intro_classes, unfold complex_norm_def)
+  fix r :: real
+  fix x y :: complex
+  show "0 \<le> cmod x"
+    by (rule complex_mod_ge_zero)
+  show "(cmod x = 0) = (x = 0)"
+    by (rule complex_mod_eq_zero_cancel)
+  show "cmod (x + y) \<le> cmod x + cmod y"
+    by (rule complex_mod_triangle_ineq)
+  show "cmod (of_real r) = abs r"
+    by (simp add: of_real_complex_of_real)
+  show "cmod (x * y) = cmod x * cmod y"
+    by (rule complex_mod_mult)
+  show "cmod 1 = 1"
+    by (rule complex_mod_one)
+qed
+
 subsection{*A Few More Theorems*}
 
 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"