Re: [isabelle-dev] Status of recdef?
Hi, This took me a bit longer to answer properly, but anyway: On 07/24/2011 05:05 PM, Makarius wrote: The old recdef package is another ancient duplicate that is mostly used in old manuals now. Is there a scheme for eventual removal? The situation is a bit subtle. Unfortunately, the function package, due to its general notion of pattern matching, has a notable efficiency problem, which becomes fatal when specifications are larger and have certain nested and overlapping patterns. Theoretical, the specification itself may explode exponentially when the patterns are made disjoint. This is inherent in the problem and also applies to recdef, but does not seem to occur in practice. However, we do frequently see a quadratic blowup, e.g. when we have a datatype T with many constructors C1 ... Cn, and when the matching has the form function f :: T = T = bool where f C1 C1 - True | f C2 C2 - True | ... f Cn Cn - True | f _ _ - False The catch-all pattern at the bottom is then transformed into O(n^2) equations. Unlike recdef, the function package implements this transformation as a preprocessor and works with the O(n^2) equations internally. Then it produces proof obligations that these equations are indeed pairwise disjoint. The number of proof obligations is thus O(n^4). The constant factor is also quite bad, since each proof obligation is solved using auto by default. At the time, this seemed to be the fair price to pay for the extra generality, but since in practice most definitions use normal datatype constructor patterns, it is actually quite a pain. The only plausible solution to this issue is to add special treatment to the common case, which avoids the proof obligations entirely. This could be done in different ways, but is a rather complex architectural change. So far I have not attacked it, since there were always other things that were more pressing, easier, or scientifically more rewarding. But it is still on my list, and I intend to look at this again soon. Now that a number of other issues have accumulated with the function package, it is a good time to revisit some of the internals. Since it is already marked as legacy_feature for quite some time, one could move it to src/HOL/Library/Old_Recdef.thy, for example. I did this now. Now, all uses of recdef in the distribution and the AFP remain because of the problem mentioned above. I have eliminated all other uses. krauss@lapbroy38:~/wd/isabelle/src/HOL$ grep -lr '^recdef' . ./Decision_Procs/Cooper.thy ./Decision_Procs/MIR.thy ./Decision_Procs/Parametric_Ferrante_Rackoff.thy ./Decision_Procs/Ferrack.thy krauss@lapbroy38:~/wd/afp/thys$ grep -lr '^recdef' . ./Simpl/Language.thy Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I've come across something strange in the file isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if anybody could think of an explanation. A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def Sup_bool_def) this is strange because this exact text already appears in the file Complete_Lattice.thy (I refer to Florian's version of HOL), which is imported by Main, which is indirectly imported by Diagram. And just in case I was mistaken on this last point, I modified Diagram to import Main explicitly, just to be sure. This instance declaration is still necessary. I just don't get this. I thought that an instance declaration lasted for ever. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson l...@cam.ac.uk wrote: I've come across something strange in the file isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if anybody could think of an explanation. A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def Sup_bool_def) this is strange because this exact text already appears in the file Complete_Lattice.thy (I refer to Florian's version of HOL), which is imported by Main, which is indirectly imported by Diagram. And just in case I was mistaken on this last point, I modified Diagram to import Main explicitly, just to be sure. This instance declaration is still necessary. I just don't get this. I thought that an instance declaration lasted for ever. DataRefinementIBP/Preliminaries.thy contains the following line: class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra So your instance proof above is for class Preliminaries.complete_boolean_algebra, while the instance in Complete_Lattice.thy is for the separate Complete_Lattice.complete_boolean_algebra class. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
Hello everyone, Isabelle prints out warning messages whenever anyone declares a duplicate simp rule, intro rule, etc. It would be nice if Isabelle would print a similar warning whenever a definition reuses a name that is already in scope in the current context. For example, if a theory defines a class like this... class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra ...and a class called complete_boolean_algebra is already in scope, then a warning message ought to be printed. Such a warning message would be useful for constant names, lemma names, etc. as well. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
