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

[Manuel Eberl]

On 17/09/13 00:13, Makarius wrote:
> 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.
To reiterate my question, does that mean you want a
"Fun_Cases.fun_cases" command that takes a term and a string and
registers the fun_cases rule derived from the term under the given name?


> 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.
I honestly don't remember. With the documentation on Isabelle/ML being
so sparse, one is, as a beginner, all but forced to experiment with
snippets of code from other parts of Isabelle until stuff works, and
that's what I did. At any rate, I suppose I can simply remove the dummy
pattern feature again.

Cheers,
Manuel