thanks for fixing that! I’m doing a new round of changes and I shall delete the theorem you mentioned. There are many such redundant theorems now, I have deleted quite a few already.
I’m going to try to make the other change as well. The problem is that for a great many theorems, their behaviour with the simplifier and/or blast differed according to which coercion function they were expressed with. This makes it impossible to duplicate the prior behaviour. I have already observed that adding these additional simplification rules breaks a few proofs, so we have to see how it goes. Larry > On 12 Nov 2015, at 08:46, Manuel Eberl <ebe...@in.tum.de> wrote: > > I just repaired Akra_Bazzi. > > In the process of doing so, I noticed two things: > > 1. Due to the new definition of ‘real’, the theorem Real.of_nat_nat, which is > stated as ‘0 ≤ x ⟹ real (nat x) = real x’ now essentially means ‘0 ≤ x ⟹ real > (nat (int x)) = real x’, which is rather silly. > > Moreover, Real.of_nat_nat shadows Int.ring_1_class.of_nat_nat, which even > implies Real.of_nat_nat. I therefore suggest we just remove Real.of_nat_nat > completely. > > > 2. Goals like ‘real (floor x) ≤ x’ used to be solvable by ‘simp’, whereas the > now equivalent ‘of_int (floor x) ≤ x’ is not. (I don't know if simp used to > do that with a simp rule or a solver) > > It would probably nice to have ‘simp’ do this sort of thing again, but in all > instances that I encountered, ‘linarith’ did the trick as well. > > > I'm a bit busy right now, but I am, in general, willing to help out with > fixing the AFP. Which entries would you want me to look at? > > > Cheers, > > Manuel > > > On 11/11/15 22:09, Johannes Hölzl 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 >> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
