[isabelle-dev] complex argument function(s)
lp15 at cam.ac.uk
Sat Jul 3 13:04:54 CEST 2021
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?
> 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).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev