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-requ...@mailbroy.informatik.tu-muenchen.de> 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 <l...@cam.ac.uk> > To: Isabelle-dev list > <isabelle-dev@mailbroy.informatik.tu-muenchen.de>, Johannes H?lzl > <johannes.hoe...@gmx.de> > 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 <hu...@in.tum.de> > To: Lawrence Paulson <l...@cam.ac.uk>, Isabelle-dev list > <isabelle-dev@mailbroy.informatik.tu-muenchen.de>, Johannes H?lzl > <johannes.hoe...@gmx.de> > Subject: Re: [isabelle-dev] quaternions > Message-ID: <bb02446e-ef9b-5a39-f243-35f81adc1...@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 <nip...@in.tum.de> > 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 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 <ebe...@in.tum.de> > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de > Subject: Re: [isabelle-dev] quaternions > Message-ID: <1a9a4b13-dc41-95b5-e268-8976629b8...@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-...@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@mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > ------------------------------ > > End of isabelle-dev Digest, Vol 133, Issue 13 > ********************************************* _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
