This is very nice to hear. ‘real’ has plagued me for some time now and I
am glad to see it gone.
Thanks for the good work!
On 10/11/15 17:45, Lawrence Paulson wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
