[isabelle-dev] quaternions

Mon Jun 18 15:01:07 CEST 2018

To me, the first application of cross products that crosses my mind is
vector analysis; it can help define concepts like the curl. Thus, if
it is not a separate AFP entry, I think it might fit in analysis.

Mohammad

On Mon, Jun 18, 2018 at 2:24 PM,
<isabelle-dev-request at mailbroy.informatik.tu-muenchen.de> wrote:
> Send isabelle-dev mailing list submissions to
>         isabelle-dev at mailbroy.informatik.tu-muenchen.de
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> or, via email, send a message with subject or body 'help' to
>         isabelle-dev-request at mailbroy.informatik.tu-muenchen.de
>
> You can reach the person managing the list at
>         isabelle-dev-owner at mailbroy.informatik.tu-muenchen.de
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of isabelle-dev digest..."
>
>
> Today's Topics:
>
>    1. quaternions (Lawrence Paulson)
>    2. Re: quaternions (Lars Hupel)
>    3. Re: quaternions (Tobias Nipkow)
>    4. Re: quaternions (Manuel Eberl)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 18 Jun 2018 11:36:58 +0100
> From: Lawrence Paulson <lp15 at cam.ac.uk>
> To: Isabelle-dev list
>         <isabelle-dev at mailbroy.informatik.tu-muenchen.de>, Johannes H?lzl
>         <johannes.hoelzl at gmx.de>
> Subject: [isabelle-dev] quaternions
> Message-ID: <5B41A03D-65AE-4A0F-B5D2-D405CAEDEC97 at cam.ac.uk>
> Content-Type: text/plain;       charset=us-ascii
>
> 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
>
>
>
> ------------------------------
>
> Message: 2
> Date: Mon, 18 Jun 2018 14:17:34 +0200
> From: Lars Hupel <hupel at in.tum.de>
> To: Lawrence Paulson <lp15 at cam.ac.uk>, Isabelle-dev list
>         <isabelle-dev at mailbroy.informatik.tu-muenchen.de>, Johannes H?lzl
>         <johannes.hoelzl at gmx.de>
> Subject: Re: [isabelle-dev] quaternions
> Message-ID: <bb02446e-ef9b-5a39-f243-35f81adc1829 at in.tum.de>
> Content-Type: text/plain; charset=utf-8
>
>> So where does this material belong? Arguably not in Analysis, which is already too large.
>
> Why not a regular AFP entry?
>
> Cheers
> Lars
>
>
> ------------------------------
>
> Message: 3
> Date: Mon, 18 Jun 2018 14:18:08 +0200
> From: Tobias Nipkow <nipkow at in.tum.de>
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] quaternions
> Message-ID: <50edc647-c34c-057c-4c02-471dac7ce55b at in.tum.de>
> Content-Type: text/plain; charset="utf-8"; Format="flowed"
>
> 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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180618/982c6bcb/attachment-0001.p7s>
>
> ------------------------------
>
> Message: 4
> Date: Mon, 18 Jun 2018 14:23:52 +0200
> From: Manuel Eberl <eberlm at in.tum.de>
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] quaternions
> Message-ID: <1a9a4b13-dc41-95b5-e268-8976629b808d at in.tum.de>
> Content-Type: text/plain; charset="utf-8"
>
> I would also have suggested an AFP entry.
>
>> let reflect_along = new_definition
>>  `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;
> Think of it as x being the direction of a ray of light hitting a mirror
> (in the shape of a hyperplane through the origin with normal vector a)
> and being reflected. The result is the direction of the reflected ray.
>
> Where it belongs I cannot say; that depends on what kinds of results are
> proven about it. I for one would consider this a very ?applied? concept
> (I know it from ray tracing), so unless we have a concrete application
> for it, I'm not sure we need it at all.
>
> Manuel
>
>
> On 2018-06-18 14:17, Lars Hupel wrote:
>>> So where does this material belong? Arguably not in Analysis, which is already too large.
>> Why not a regular AFP entry?
>>
>> Cheers
>> Lars
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180618/cfb02d7b/attachment.html>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
> ------------------------------
>
> End of isabelle-dev Digest, Vol 133, Issue 13
> *********************************************