diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat Sep 01 01:21:48 2007 +0200
@@ -376,8 +376,16 @@
 
 instance real :: norm
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
+ML"set Toplevel.debug"
 
-axclass real_normed_vector < real_vector, norm
+class sgn_div_norm = scaleR + inverse + norm + sgn +
+assumes sgn_div_norm: "sgn x = x /# norm x"
+(* FIXME junk needed because of bug in locales *)
+and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn"
+and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse"
+and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR"
+
+axclass real_normed_vector < real_vector, sgn_div_norm
   norm_ge_zero [simp]: "0 \<le> norm x"
   norm_eq_zero [simp]: "(norm x = 0) = (x = 0)"
   norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -407,6 +415,9 @@
 
 instance real :: real_normed_field
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
+apply (simp add: real_sgn_def)
+(* FIXME junk *)
+apply(rule refl)+
 apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
 apply (rule abs_triangle_ineq)
@@ -584,27 +595,25 @@
 
 subsection {* Sign function *}
 
-definition
-  sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where
-  "sgn x = scaleR (inverse (norm x)) x"
+lemma norm_sgn:
+  "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
+by (simp add: sgn_div_norm norm_scaleR)
 
-lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
-unfolding sgn_def by (simp add: norm_scaleR)
+lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0"
+by (simp add: sgn_div_norm)
 
-lemma sgn_zero [simp]: "sgn 0 = 0"
-unfolding sgn_def by simp
-
-lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
-unfolding sgn_def by simp
+lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)"
+by (simp add: sgn_div_norm)
 
-lemma sgn_minus: "sgn (- x) = - sgn x"
-unfolding sgn_def by simp
+lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)"
+by (simp add: sgn_div_norm)
 
-lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
-unfolding sgn_def by (simp add: norm_scaleR mult_ac)
+lemma sgn_scaleR:
+  "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
+by (simp add: sgn_div_norm norm_scaleR mult_ac)
 
 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
-unfolding sgn_def by simp
+by (simp add: sgn_div_norm)
 
 lemma sgn_of_real:
   "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
@@ -613,10 +622,10 @@
 lemma sgn_mult:
   fixes x y :: "'a::real_normed_div_algebra"
   shows "sgn (x * y) = sgn x * sgn y"
-unfolding sgn_def by (simp add: norm_mult mult_commute)
+by (simp add: sgn_div_norm norm_mult mult_commute)
 
 lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
-unfolding sgn_def by (simp add: divide_inverse)
+by (simp add: sgn_div_norm divide_inverse)
 
 lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
 unfolding real_sgn_eq by simp