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 <ebe...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
