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

[Manuel Eberl]

Hallo,
> 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?


> Anyway, looking briefly what is missing for the regular ML version of
> Fun_Cases.fun_cases, I fell over another stumbling block: the use of
> Proof_Context.read_term_pattern and pat_to_term.
>
> Manuel, can you say what is the idea and purpose behind it?
>
> From the existing inductive_cases and inductive_simps, it looks like
> plain Syntax.read_props together with Variable.auto_fixes would do the
> job, as is done in the analogous Inductive.mk_cases and
> Inductive.mk_simp_eq. (These things are non-trivial, and I always need
> to look myself carefully how things really work.)
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. I do think that read_props does not support dummy patterns.


Cheers,
Manuel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130917/466c71f0/attachment-0002.html>