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