[isabelle-dev] case syntax

[Alexander Krauss]

On 01/12/2012 03:43 PM, Stefan Berghofer wrote:
> Quoting Makarius <makarius at sketis.net>:
>> Just to illuminate the general situation a bit, can you point to
>> relevant parts of your thesis, also the one of Konrad Slind for the
>> old version? Stefan had mentioned that at some point "as everybody
>> knows, Konrad used to do it like that" without giving a reference.
>
> you can find Konrad's thesis on the web at
>
> http://www.cl.cam.ac.uk/~ks121/papers/phd.html
>
> The pattern matching algorithm is described in Section 3.3 (p. 62 - 71)
> The steps of the algorithm are summarized in Figure 3.4.

Here is the younger history:

Konrad's algorithm sometimes leads to a blowup in the number of cases, 
which was always seen as problematic. In 2006, I thought I had found an 
algorithm that actually produces the minimal number of cases, but I 
didn't try to prove it. It was completely wrong of course, as I 
discovered later. The current "pattern_split.ML" is based on these ideas.

In 2007/8, I worked out how to actually optimize the number of cases, 
but the results are not practical: You get a relatively complex 
optimization problem (worse than NP-hard), and it is hard to predict the 
results, which makes it unsuitable for use in a package. Furthermore, it 
does not actually solve the underlying problem: even when minimizing, 
the number of cases is large (it can be exponential). But the theory is 
nice and interesting (ch. 4 of my thesis has all the details).

So, in short, it seems that Konrad's algorithm is basically the most 
appropriate we can get. When Stefan adapted it to the syntax 
translations, he also thought about adding some heuristics that improve 
it (by trying to guess the right variable to split on, instead of just 
picking the first), but I don't think that any such modifications went in.

Alex