<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hallo,<br>
<blockquote
cite="mid:alpine.LNX.2.00.1309161951560.10063@macbroy21.informatik.tu-muenchen.de"
type="cite">
The main thing still missing in Isabelle/5ccee1cb245a is a regular
ML interface Fun_Cases.fun_cases.
<br>
</blockquote>
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context -> term -> thm
<meta http-equiv="content-type" content="text/html;
charset=ISO-8859-1">
– 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?<br>
<br>
<br>
<blockquote
cite="mid:alpine.LNX.2.00.1309161951560.10063@macbroy21.informatik.tu-muenchen.de"
type="cite">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.
<br>
<br>
Manuel, can you say what is the idea and purpose behind it?
<br>
<br>
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.)
<br>
</blockquote>
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.<br>
<br>
<br>
Cheers,<br>
Manuel<br>
</body>
</html>