[isabelle-dev] complex argument function(s)

[Lawrence Paulson]

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