[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases
eberlm at in.tum.de
Tue Sep 17 00:20:24 CEST 2013
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.
More information about the isabelle-dev