Re: [isabelle-dev] quaternions
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, wrote: > Send isabelle-dev mailing list submissions to > isabelle-dev@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-requ...@mailbroy.informatik.tu-muenchen.de > > You can reach the person managing the list at > isabelle-dev-ow...@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 > To: Isabelle-dev list > , Johannes H?lzl > > Subject: [isabelle-dev] quaternions > Message-ID: <5b41a03d-65ae-4a0f-b5d2-d405caede...@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 > To: Lawrence Paulson , Isabelle-dev list > , Johannes H?lzl > > Subject: Re: [isabelle-dev] quaternions > Message-ID: > 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 > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de > Subject: Re: [isabelle-dev] quaternions > Message-ID: <50edc647-c34c-057c-4c02-471dac7ce...@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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > -- next
Re: [isabelle-dev] quaternions
The cross product development is 200 lines long while the quaternion development is 730. Should they be separate entries, or do cross products belong elsewhere? Larry > On 18 Jun 2018, at 13:18, Tobias Nipkow wrote: > > Why not simply the AFP? signature.asc Description: Message signed with OpenPGP ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
> 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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] quaternions
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev