[isabelle-dev] the function "real"

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 12 13:03:43 CET 2015 

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

More information about the isabelle-dev mailing list