[isabelle-dev] the function "real"

[Lawrence Paulson]

The first phase of this project is finished: the function “real” now has the monomorphic type nat => real and is simply an abbreviation for the generic function, of_nat. In addition, the function “real_of_int” abbreviates the generic function of_int.

It took about a week to convert all the theories in the main Isabelle/HOL directory. Most of them needed little or no attention, the big exceptions being Probability (which frequently used “real” with the type ereal => real) and Decision_Procs, which contained many thousands of instances of “real” on integers and floats.

The main priority at the moment is to fix the decision procedure mir, which isn’t working but appears to be entirely unused. Then there is still a lot of cleaning up to do, especially in Real.thy and its ancestors. Two or three dozen theorems existed in duplicate forms, with versions for “real” separate from versions for the other coercions; occasionally these variants were named systematically, but often their names were unrelated from the originals, and the names of variables in the theorems were almost always different. The simplification status of the two variants generally differed as well. Thus the behaviour of the simplifier on a formula depended on which coercion had been used, and in 150 cases, the simplification itself included the mapping of one coercion to another (there were two equivalent theorems for doing this).

Innumerable type constraints have now become redundant (things such as real_of_int (i::int)), but I intend to leave them as they are. I have a lot of AFP entries to fix.

Larry