[isabelle-dev] the function "real"

[Johannes Hölzl]

Okay, I look at the AFP entries.

I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow
if this is unusual.

 - Johannes

Am Mittwoch, den 11.11.2015, 17:19 +0000 schrieb Lawrence Paulson:
> 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 <hoelzl at 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 <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
> > 
> > 
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>