Email Gateway (Aug 19 2022 at 17:30): Email Gateway (Aug 19 2022 at 17:30):From: "W. Douglas Maurer" <maurer@gwu.edu>
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
Email Gateway (Aug 19 2022 at 17:31):From: Christian Sternagel <c.sternagel@gmail.com>
The attribute "case_names" is documented in the reference manual.
$ isabelle doc isar-ref
search for "case_names" and on page 134 you will find a (short) description.
In essence the attribute just allows you to choose your own names for
cases (which will be used by the "induct/induction" and "cases" methods).
cheers
chris
Email Gateway (Aug 19 2022 at 17:31):From: "W. Douglas Maurer" <maurer@gwu.edu>
OK. I see the problem now. The problem is that at one point I was
told that, when searching Isabelle/Isar documentation for something
including an underscore, I have to substitute a hyphen. Now I find
that this is sometimes true and sometimes not. For "Isabelle/HOL --
Higher-Order Logic," it is true; for "Isabelle/Isar Reference
Manual," it's apparently not true. I was searching for case-names
when I should have been searching for case_names.
Email Gateway (Aug 19 2022 at 17:32):From: Lars Noschinski <noschinl@in.tum.de>
When looking for commands and the like, I usually prefer to scroll
throught the index. Search has (or had) problems with ligatures in at
least some pdf viewers, so I found this the most reliable method for my
purposes.
Email Gateway (Aug 19 2022 at 17:32):From: Christian Sternagel <c.sternagel@gmail.com>
Indeed. I think some while ago this advice was true for all docu PDFs,
but (I guess due to the confusion this caused) this was changed in more
recent releases. I guess "tutorial" is an exception since it is somewhat
outdated (style-wise) but still a source of many nice examples.
But guessing aside ;), you can always try the index first.
cheers
chris
Email Gateway (Aug 19 2022 at 17:32):From: Makarius <makarius@sketis.net>
PDF is electronic paper, with some uncertainty of real paper. Some PDF
viewers also use OCR to find things, but you never know 100% what it is.
To make really sure, you can always search the formal sources in
$ISABELLE_HOME/src/Doc/Isar_Ref/.
Makarius
Email Gateway (Aug 19 2022 at 17:32):From: Makarius <makarius@sketis.net>
No. Talking about source files I was referring to the default Isabelle
source editor, which is Isabelle/jEdit. The above
$ISABELLE_HOME/src/Doc/Isar_Ref works literally in its file-dialog, even
on Windows.
See also the Isabelle/jEdit manual that is accessible in the application
itself, in the prominent Documentation panel.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC