[isabelle-dev] quaternions

[Tobias Nipkow]

Why not simply the AFP?

Tobias

On 18/06/2018 12:36, Lawrence Paulson wrote:
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180618/982c6bcb/attachment.bin>