[isabelle] case_names



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