[isabelle-dev] complex argument function(s)

[Lawrence Paulson]

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.

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.

Remark number two: I dug into this because of constructions involving Arg in that Apostol volume that turned out to have nothing to do with anything.

Larry

> 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
>