[isabelle-dev] complex argument function(s)

[Manuel Eberl]

I'm happy to have whatever you deem useful moved to the library.

Manuel


On 03/07/2021 13:04, Lawrence Paulson wrote:
> Yesterday I renamed arg -> Arg along with most of the arg_ theorems (though we still have arg_unique and Arg_unique).
>
> I noticed some useful-looking basic lemmas about Arg in Stirling_Formula/Gamma_Asymptotics.thy (added to the AFP by Manuel in 2016) that we might bring into the libraries. Any comments?
>
> Larry
>
>> On 25 Jun 2021, at 21:28, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>
>> I’ve just noticed that we define both arg and Arg, the latter in Complex_Transcendental.
>>
>> The definitions are different but arg z = Arg z holds unconditionally. It looks like a historical accident, maybe arg was introduced in the 1990s and forgotten about.
>>
>> Interestingly enough, arg is used far more despite there being almost nothing proved about it. Some lemmas are proved in Complex_Geometry/More_Complex.thy, and many occurrences of “arg” are simply variables.
>>
>> This is a mess. Any suggestions? Maybe Arg could (temporarily) be made an abbreviation for arg. Arg is the usual of the function (principal value of the argument).
>>
>> Larry
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev