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

[Makarius]

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 
past.


> 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 
all.


 	Makarius