[isabelle-dev] complex argument function(s)

[Dr A. Koutsoukou-Argyraki]

     Remark number one: for some reason, the HOL Light library defines 
Arg
     to range from 0 to 2pi. Although some authors make that choice, you
     then have to define Ln similarly so that you have Arg z = Im (Ln z).
     It’s truly bizarre that this identity fails in HOL Light.

On 2021-07-01 10:53, Lawrence Paulson wrote:
> Oh yes, the old convention: when you have a multi-valued function, the
> “principal value” is capitalised. In the case of Isabelle/HOL, that
> means we need to choose the name Arg, not arg. To smooth the
> changeover, surely it’s best to leave the first definition (but now
> capitalised) where it is and replace the second definition by the same
> statement but proved as a theorem. At least a renaming is relatively
> easy to accomplish even if it triggers hundreds of errors.

I agree with Larry that this sounds like the optimal solution.


> Remark number one: for some reason, the HOL Light library defines Arg
> to range from 0 to 2pi. Although some authors make that choice, you
> then have to define Ln similarly so that you have Arg z = Im (Ln z).
> It’s truly bizarre that this identity fails in HOL Light.

Which of the range conventions would you prefer to keep? I think any one 
is fine as long as things are
all consistent

Best,
Angeliki

> 
>> On 1 Jul 2021, at 09:37, Manuel Eberl <eberlm at in.tum.de> wrote:
>> 
>> On 01/07/2021 03:09, Dr A. Koutsoukou-Argyraki wrote:
>>> Usually in the literature it's  -\pi < Arg z \leq \pi
>>> while arg z = Arg z + 2 \pi N, where N \in \nat
>> 
>> I don't understand what the second one means. Is this a multi-valued
>> function or what does the "N" mean here?
>> 
>> I agree with Larry that one of the two "arg" functions has to go. As 
>> for
>> which one, I have no preference. Making one of them into an 
>> abbreviation
>> sounds reasonable, although I am not sure if it really is less work 
>> than
>> just replacing it in one go immediately.
>> 
>> Note that we also have "is_Arg" and "Arg2pi", so perhaps "Arg" would 
>> be
>> more consistent than "arg".
>> 
>> Manuel
>>