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

[Makarius]

On Fri, 13 Sep 2013, Alexander Krauss wrote:

> This refers to Isabelle f557a4645f61:
>
> * New command "fun_cases" derives ad-hoc elimination rules for
> function equations as simplified instances of f.elims, analogous to
> inductive_cases.  See HOL/ex/Fundefs.thy for some examples.

Thanks.  I see that you have already provided canonical entries for NEWS 
and CONTRIBUTORS, as appropriate for the relase.

Doing some other routine maintenance elsewhere, I've come across the 
sources of HOL/Tools/Function/fun_cases.ML and 
HOL/Tools/Function/function_elims.ML today and got stuck there -- that 
also needs to be consolidated in the remaining weeks before the relase.


The main thing still missing in Isabelle/5ccee1cb245a is a regular ML 
interface Fun_Cases.fun_cases.

Manuel is one of many people who have picked up the wrong terminology of 
"the ML level of Isabelle" elsewhere, and fell into a corresponding trap 
like so many other people did for the first time writing their own tools 
in Isabelle/ML.  (This is not a problem, if lessons are learned from it.)

Since most Isabelle users use Isar syntax most of the time, one might get 
the idea that everything is Isar syntax.  This is not the case.  On the 
contrary, Isabelle/Isar consists mainly of Isabelle/ML interfaces with a 
thin layer of concrete syntax on top.  Whatever tool is built, it requires 
first and foremost a proper ML interface, such that it can be re-used 
routinely to build further tools.  Concrete syntax is merely a convenient 
add-on, which is usually provided as well, but not abolutely mandatory.

Since we've had some interesting discussions about Isabelle in the mid 
1990-ies on isabelle-users recently, and there is also the new high-end 
(co)datatype package becoming mainstream in Isabelle2013-1, it might be 
interesting to look at the 1995 version of HOL/datatype here: 
http://isabelle.in.tum.de/repos/Old_HOL/file/9b403e123c1b/datatype.ML#l435 
This is how some add-on tool struggles with string-only "interfaces".  It 
pastes together strings for concrete syntax parsers for types, consts, 
axioms, and hopes for the best.  (In current Isabelle one could always use 
YXML to force terms down the throat of tools without proper ML interfaces, 
but this should be the last resort.)


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.)


 	Makarius