Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

2018-06-18 Thread Makarius
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

[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

2018-06-18 Thread Lars Hupel
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

Re: [isabelle-dev] quaternions

2018-06-18 Thread 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

Re: [isabelle-dev] quaternions

2018-06-18 Thread Lawrence Paulson
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

[isabelle-dev] quaternions

2018-06-18 Thread Lawrence Paulson
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

Re: [isabelle-dev] quaternions

2018-06-18 Thread Manuel Eberl
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)

Re: [isabelle-dev] quaternions

2018-06-18 Thread Lars Hupel
> 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

Re: [isabelle-dev] quaternions

2018-06-18 Thread Mohammad Abdulaziz
> 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