brianh at cs.pdx.edu
Fri Aug 31 01:17:23 CEST 2007
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:
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
More information about the isabelle-dev