[isabelle-dev] the function "real"

[Johannes Hölzl]

Hi Larry,

this is a huge change and after I adapted Markov_Models I see that it
simplifies some proofs.

If you want I can adapt all AFP entries for which I'm the maintainer, or
which are related to Probability theory:

  Density_Compiler
  Integration
  Lower_Semicontinuous
  Markov_Models
  Ordinary_Differential_Equations
  Possibilistic_Noninterference
  Probabilistic_Noninterference
  UpDown_Scheme
  Girth_Chromatic
  Probabilistic_System_Zoo
  Random_Graph_Subgraph_Threshold
  pGCL

Just tell me which of these you are already working on, so we can merge
without conflicts.

 - Johannes


Am Mittwoch, den 11.11.2015, 12:28 +0000 schrieb Lawrence Paulson:
> I’m glad to have your support. It’s just possible that I might ask your help in getting some things working in the AFP.
> 
> Larry
> 
> > On 10 Nov 2015, at 17:53, Manuel Eberl <eberlm at in.tum.de> wrote:
> > 
> > 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