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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
