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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
