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

[Manuel Eberl]

Hallo,

I just remembered that I wanted to tell you that I have done what you
asked and set everything up in exactly the same way that inductive_cases
does it. I sent my changes to Alexander Krauss last Wednesday so that he
can review them.

Cheers,
Manuel

On 09/17/2013 06:19 PM, Makarius wrote:
> 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