It would be great if you could help. I have just committed some corrections to a number of AFP theories, including that one I think. Affine_Arithmetic comes with some examples that run extremely slowly; I’m not sure whether there is a problem or whether it is always like that. If you want to take over with those, I can do some more tidying up with the main libraries.
Larry > On 11 Nov 2015, at 17:17, Johannes Hölzl <hoe...@in.tum.de> wrote: > > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
