[isabelle-dev] the function "real"

[Lawrence Paulson]

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