The Dottie Number

Once upon a time, goes the story, a lady named Dottie got bored and started playing with her calculator, pressing the cosine key over and over again. At first the numbers fluctuated wildly, but over time they always settled down to approximately 0.739085. (This only works if your calculator is set to radians, not degrees.) She had discovered the unique fixed point of the cosine function. The Dottie number has several further properties: it is a global attractor, meaning the limit is the same no matter what number you start with, and it is transcendental. It is a great example for showing off a range of computer algebra techniques in Isabelle, such as differentiation and unlimited precision real computations. Let’s prove those properties just mentioned and calculate (by proof!) its value to 12 decimal places. Getting started We begin by defining dottie to be the unique fixed point of cos. But this definition, using the definite descriptor THE, will be good for nothing until both…