[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases

[Makarius]

On Wed, 2 Oct 2013, Alexander Krauss wrote:

> Nevertheless, it is also a bit irritating that there seems to be no 
> proper way of adding support for wildcards to fun_cases (and 
> inductive_cases). This should be addressed at some point, but for now we 
> are fine.

There is no fundamental problem to support wildcards here -- the 
mechanisms are available since about 2007/2008.  It is just a matter of 
priority: how much time is it worth spending there now, compared to other 
more pressing issues.

The general challenge is to maintain the system that it moves continously 
forward instead of partially backward, by introducing special cases that 
don't quite work.  Tools are built in analogy of other tools, and making a 
move here means to make an analogous move there.  This is a semantic 
version of avoiding diverging clones.

For example, more than 10 years ago the HOL datatype package could not 
handle sort constraints for its type variables, due to lack of mechanisms 
for that in the underlying Pure type inference.  There was a special case 
for HOLCF/domain (by David von Oheimb) to make that work partially. 
Later the Isabelle framework supported constraints more uniformly, and 
exactly that partial *solution* then broke down, and made it also hard to 
push the improvement from the bottom through to that slightly diverged 
tool.


 	Makarius