[isabelle-dev] complex argument function(s)

[Lawrence Paulson]

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