I’m trying again with a fume more simplification rules than before, but as I mentioned in my last message, it will not be possible to duplicate the prior behaviour.
Many thanks for taking a look! Larry > On 11 Nov 2015, at 21:09, Johannes Hölzl <hoe...@in.tum.de> wrote: > > It looks like the setup for blast changed, in the following entries is a > non-terminating blast call. They do not seam to be related to the change > at all: > > Graph_Theory > ShortestPath > Rank_Nullity_Theorem > Echelon_Form > Gauss_Jordan > > Interestingly in > Jordan_Normal_Form > QR_Decomposition > a real :: 'a => real is required! Both introduce a type class with > group/vector-space homomorphism. > > I did _not_ look yet into: > JinjaThreads > Ordinary_Differential_Equations > Affine_Arithmetic > Akra_Bazzi > > - Johannes > > Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb 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 <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 > > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
