This is a follow-up to my earlier post to this list concerning
induction starting from 1 and beyond. I received a very helpful reply
to that post from Joachim Breitner, with an example which included
the use of case_names. I am having the same problem with this that I
have had with several other features of Isar: Where is it defined?
It's not in the Isabelle/Isar Reference Manual; it's not in
Programming and Proving in Isabelle/HOL; it's not in A Tutorial
Introduction to Structured Isar Proofs; it's not in the Concrete
Semantics book. There are 74 examples of case_names in the 1768-page
document, "Isabelle/HOL -- Higher-Order Logic"; but examples are not
the same thing as a definition. What is the syntax of a case name?
Can it be a two-digit number like 10 (which is forbidden for labels)?
Can it be like an identifier except that it starts with a digit (like
4Runner)? Can it include special characters, and, if so, which ones?
And so on. And I'm not so much interested in answers to those
specific questions as I am in finding a syntax definition for
case_names, preferably a syntax diagram like the ones in the
Isabelle/Isar Reference Manual, which have been very useful to me. (I
was taught very early on that induction from examples is never enough
-- I was told that this is like the boy who decided that all cows are
brown, because he'd seen several dozen cows, all of which were brown,
and he'd never seen a black one.) -WDMaurer
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
This archive was generated by a fusion of
Pipermail (Mailman edition) and