Re: [isabelle-dev] Future of permanent_interpretation

> What is the conclusion of this thread for the coming release? Whatever > happens, the time window for it is approx. Nov/Dec 2015. The situation is still somehow inconclusive. I am working currently to re-integrate permanent_interpretation »as it is« into Pure, to provide a base for further

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

Hi Clemens, > I'm not familiar with the termination argument for abbreviations, but certainly we can say that abbreviations define a reduction system (in fact a rewrite system), and I would assume that there are no cycles and infinite paths. Now my patch will clone part of this system,

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

Hi Bertram, Christian and Bertram, I would like to put my two cents in this topic. I have done a simple experiment about this using my AFP entry about the QR decomposition, where a strong use of map_range is done. With the current map_range definition, the computation of the QR decomposition of

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] Proposal to use hierarchical heaps with Poly/ML

On 12/11/15 21:17, Lars Hupel wrote: Hi Japheth, A lot of space could be saved if Isabelle saves heaps in this way. For our L4.verified project we found a 7× reduction in size. out of curiousity: How did you arrive at this number? Have you implemented incremental heaps for Isabelle? As I

Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

On 12/11/15 16:45, Japheth Lim wrote: > [...] > A lot of space could be saved if Isabelle saves heaps in this way. For > our L4.verified project we found a 7× reduction in size. I would like to add that the 7x reduction is from 50GB for a full build of all our heaps (i.e. regression test). This

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] Proposal to use hierarchical heaps with Poly/ML

On Thu, 12 Nov 2015, Japheth Lim wrote: For a long time, Poly/ML has supported hierarchical heaps (PolyML.SaveState.saveChild). As I understand it, this feature was not used because it makes heaps no longer self-contained; moving them to a different path would break the loading process.

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