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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[isabelle-dev] the function "real"

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