On 18/06/18 21:30, Lars Hupel wrote:
>
> the good news is that we have just received new hardware (Dual Epyc 7601).
>
> The bad news is that a current development snapshot
> (Isabelle/410818a69ee3) exhibits a problem on this hardware. In
> particular, the session HOL-Corec_Examples doesn't
Dear list,
the good news is that we have just received new hardware (Dual Epyc
7601).
The bad news is that a current development snapshot
(Isabelle/410818a69ee3) exhibits a problem on this hardware. In
particular, the session HOL-Corec_Examples doesn't appear to terminate.
$ cat
> 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-d
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
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)
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
> 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
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
