Re: [isabelle-dev] the function "real"

[Lars Noschinski]

On 12.11.2015 13:58, Lars Noschinski wrote:
> On 11.11.2015 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
> 
> I replaced this 'by safe meson+' now. I am a bit surprised that this
> proof broke, it is just basic set theory and first order logic.

Ok, bisected to the change which broke this proof: it is 933eb9e6a1cc by
Larry. The good news is the current head unbroke the proof agian.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the function "real"

[Florian Haftmann]

>> There are a great many examples of theorems involving various coercion
>> functions and the relations =, <, <=. In a number of cases, the “real”
>> versions were declared as [iff]-rules, while the “of_nat/of_int”
>> versions were declared as [simp]-rules only. When identifying the two,
>> I decided it would make sense to go for iff, for maximum automation,
>> but I now think this was a mistake. I’m trying the alternative right now.
> 
> Same here. I avoid modifications of the claset as much as possible these
> days because it can lead to proof searches going astray although the
> goal had nothing to do with those modifications.

I have made similar experiences when trying in vain to turn INF and SUP
into abbreviations.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the function "real"

[Lawrence Paulson]

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  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 + 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  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 + 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  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 

Re: [isabelle-dev] the function "real"

[Lars Noschinski]

On 11.11.2015 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

I replaced this 'by safe meson+' now. I am a bit surprised that this
proof broke, it is just basic set theory and first order logic.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the function "real"

[Fabian Immler]

One example was broken and I fixed it in 06bfc5cfaeab, but the rest went 
through as usual.

Fabian


> Am 12.11.2015 um 11:00 schrieb Fabian Immler :
> 
> Some examples have always been very slow. But I will double-check and mark 
> the slow ones as (* slow *) to reduce confusion in the future.
> 
> Fabian
> 
>> Am 11.11.2015 um 18:29 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 + 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  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 + 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  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

Re: [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  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 + 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  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 + 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  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 

Re: [isabelle-dev] the function "real"

[Lawrence Paulson]

There are a great many examples of theorems involving various coercion 
functions and the relations =, <, <=. In a number of cases, the “real” versions 
were declared as [iff]-rules, while the “of_nat/of_int” versions were declared 
as [simp]-rules only. When identifying the two, I decided it would make sense 
to go for iff, for maximum automation, but I now think this was a mistake. I’m 
trying the alternative right now.

Larry

> On 12 Nov 2015, at 13:30, Tobias Nipkow  wrote:
> 
> I am not surprised at all that the simplifier behaves differently because the 
> simpset is modified all the time and is full of theorems wih coercions. But 
> blast is another matter. Concrete questions:
> 
> - Are there any coercion-related permanent intro/dest/elim theorems (either 
> before or now)?
> 
> - Could they kick in during a proof concerned only with basic set theory and 
> first order logic?
> 
> I want to make sure that it is not something else that caused blast to break.
> 
> Tobias
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the function "real"

[Tobias Nipkow]

On 12/11/2015 13:03, Lawrence Paulson wrote:

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.


I am not surprised at all that the simplifier behaves differently because the 
simpset is modified all the time and is full of theorems wih coercions. But 
blast is another matter. Concrete questions:


- Are there any coercion-related permanent intro/dest/elim theorems (either 
before or now)?


- Could they kick in during a proof concerned only with basic set theory and 
first order logic?


I want to make sure that it is not something else that caused blast to break.

Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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 + 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  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 + 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  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

Re: [isabelle-dev] the function "real"

[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  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 + 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  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

Re: [isabelle-dev] the function "real"

[Johannes Hölzl]

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 + 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  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

Re: [isabelle-dev] the function "real"

[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  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

Re: [isabelle-dev] the function "real"

[Johannes Hölzl]

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 + 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  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 + 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  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