[isabelle-dev] Status of recdef?

[Alexander Krauss]

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