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
