About signs in divisions etc. I found the following paper very useful:
http://research.microsoft.com/apps/pubs/default.aspx?id=151917
Maybe someone else will find it useful too.
Cheers
On Fri, Jun 3, 2016 at 9:29 PM, Makarius wrote:
> On 03/06/16 18:49, David Matthews wrote:
>
>> The Poly/ML
On 03/06/16 18:49, David Matthews wrote:
> The Poly/ML implementation was based on the idea that something called a
> "multiple" ought to follow the usual rules of multiplication; nothing
> stronger than that. I don't think I found anything that indicated what
> the sign should be. The GCD code
On 02/06/2016 08:19, Manuel Eberl wrote:
I do think that we should enforce the same thing in the ML
implementation of gcd/lcm. Any definition of gcd/lcm for integers where
either of them may be negative does not make much sense to me. My guess
would be that lcm can be negative in the implementati
I believe Florian's proposal is good. On a proof-engineering level, the
only "inconvinience" is mainly that the property
gcd a b * lcm a b = a * b
does not hold as such but generally I suspect in the form
gcd a b * lcm a b = normalize(a * b) -- The normalize in GCD.thy perhaps
has the property
Florian has already hinted at it, but I will say it again explicitly:
Mathematically, gcd and lcm are not operations on the elements of a
ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
divisibility). In fact, these equivalence classes form a complete
lattice w.r.t. div
>> Both are ok in my view; ironically, lcm is used more often in
>> Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial,
>> though:
>>
>> Integer.gcd = PolyML.gcd
>> Integer.lcm = abs oo PolyML.lcm
>
> These two lines are the plan. Is that a good one or a bad one?
I
On 01/06/16 21:27, Florian Haftmann wrote:
> Note that the mixed signs of PolyML.IntInf.lcm maintain the property
>
> gcd a b * lcm a b = a * b
>
> whereas the lcm in GCD.thy obeys
>
> gcd a b * lcm a b = normalize a * normalize b
>
> which emphasises the dual nature of the gcd/lcm
Hi Makarius,
> presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
> understand the situation of gcd / lcm for negative arguments.
>
> We have the following slightly divergent operations:
>
> * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")
>
> * PolyML.IntI
Dear integer experts,
presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
understand the situation of gcd / lcm for negative arguments.
We have the following slightly divergent operations:
* HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")
* PolyML.IntInf.gcd:
