[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases
makarius at sketis.net
Tue Sep 17 00:13:01 CEST 2013
On Tue, 17 Sep 2013, Manuel Eberl wrote:
>> The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
>> interface Fun_Cases.fun_cases.
> What do you mean by that? There exists an ML function
> Fun_Cases.mk_fun_cases : Proof.context -> term -> thm -- is that not an
> ML interface to the Fun_Cases tool? Or do you also want a function that
> registers the resulting theorem with a given name, as the fun_cases
> command does?
When you have an Isar command, its main functionality needs to be
available directly in ML as well. That is an automatism, without
thinking. For the opposite you would have to provide a proof over future
uses of your tool.
There is a certain standard naming scheme and implementation scheme to
provide both some foobar and foobar_cmd simultaneously.
> The reason for this was that I wanted to be able to use dummy patterns
> in the input terms, i.e. write something like "list_to_option xs = Some
> _". Obviously, it's not hugely important, but it does add a small amount
> of convenience.
A rather small feature. Many years ago, every Isabelle tool had its own
way to parse and type-check terms. That lead into a big mess rather
quickly. We have managed to get out of the mess around 2007/2008, and
there are standard ways to do things.
These standard ways are not immediately obvious, but vialating standards
is also no option. It would inevitably lead back to the mess from the
> I do think that read_props does not support dummy patterns.
It does, you merely need to look further. (It also takes time, so I would
rather give up the feature here).
Note that Proof_Context.read_pattern is for reading patterns, as the name
says. This gives you quite different policies for type checking, and lots
of potential for surprise. From where did you get the idea to use
Proof_Context.read_pattern? It is hardly ever used in existing sources at
More information about the isabelle-dev