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

[Makarius]

On Tue, 17 Sep 2013, Manuel Eberl wrote:

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

The documentation is both too much and too little.  There are many layers 
of documentation from different times, written by different people, in 
different situations.  You have a bazar of information where you need to 
guess how reliable it is, and how relevant for a particular problem at 
hand.

(BTW, for the Coq sources this is much more challenging: hardly any add-on 
documents to explain things, and more than one natural language used in 
the sources.  Nonetheless, I can read what they do, and make my 
conclusions, because the general approach is not totally alien: it is just 
another interactive theorem prover of basically the same age as Isabelle, 
but more complicated sources.)


Principle number one for getting things right in Isabelle is the following 
induction over the Isabelle sources: you assume that what is there is 
right (or almost right) and then make a step to continue that for your 
tool.

That means to look around for similar tools, to see how they are done. 
For 'fun_cases' that is obviously 'inductive_cases' and 'inductive_simps'. 
Then you go through that and try to get a feeling what is done there, and 
why.  Variable.auto_fixes is particulary important here -- it got somehow 
lost in your version.

Note that 'inductive_cases' was originally done in analogy to the 
'theorem' specification element -- its simpler form without 
fixes/assumes/shows/obtains.  This explains why it follows certain 
policies about the "eigen-context" via auto-fixes, but omits later 
additions like "_" that are available in the richer specification language 
of 'inductive' or 'function'.


 	Makarius