[isabelle-dev] Status of recdef?

[Lawrence Paulson]

I agree that it would be great to get rid of recdef. That code is very complicated (being essentially an emulation of code written for HOL4) and is all but impossible to maintain.

Larry

On 22 Aug 2011, at 10:31, Alexander Krauss wrote:

> 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 at 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 at lapbroy38:~/wd/afp/thys$ grep -lr '^recdef' .
> ./Simpl/Language.thy
> 
> Alex
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev