[isabelle-dev] sgn

[Brian Huffman]

On Thursday 30 August 2007, Tobias Nipkow wrote:
> * new function "sgn" on ordered_idom, hence in particular on int and real.

HOL-Complex already defines a function called "sgn" for real normed vector 
spaces. The following definition is from Real/RealVector.thy:

definition
  sgn :: "'a::real_normed_vector => 'a" where
  "sgn x = scaleR (inverse (norm x)) x"

Originally this function was only for complex numbers, but I generalized it 
once the appropriate type classes were in place. On type "real" it coincides 
with the "sgn" function now defined in Ring_and_Field.thy. It would be nice 
if there were a single definition that could work for int, real, and complex, 
but I can't think of one. Probably something should be done about the name 
clash.

- Brian