[isabelle-dev] quaternions

[Lawrence Paulson]

I have just formalised most of the HOL Light development of quaternions. It's a great advertisement for type classes: showing that quaternions constitute a real normed division algebra and an inner product space supersedes most of the HOL Light proofs (many files), which are devoted to developing the arithmetic and topological properties of quaternions. In the course of this, I also ported the HOL Light development of the three-dimensional vector cross product.

So where does this material belong? Arguably not in Analysis, which is already too large.

Another question: I did not port the quaternion material relating to the constant reflect_along, which is defined as follows:

(* Reflection of a vector about 0 along a line. *)

let reflect_along = new_definition
 `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;

Is this concept useful, and if so, where does it belong?

Larry