John Hughes (Apr 30 2024 at 23:51): John Hughes (Apr 30 2024 at 23:51):Kevin Kappelmann recently answered a question of mine and tossed in "and I added proper intro and elim rules for your parallel definitions". (He also seems to have added an "iff" rule without comment, and I have no idea what that is.)
The form of that statement suggests to me that the cool kids know that they should add intro and elim rules in certain places in a proof document, but looking through P&P, and the tutorial, and the cookbook, and several other places, I can't seem to find anything that says when you should do so, or what constitutes a good intro or elim rule (or an iff rule, for that matter). I suspect that those who are steeped in the culture "just know". As an outsider, I'm frustrated.
So: is there a place I can read about suggested general rules for assembling a collection of lemmas/definitions/theorems, things like "whenever you make a definition, you should immediately prove two theorems, one for intro and one for elim, like this..."
I'm similarly puzzled about where to include [simp], and a reference for that would be a big help, but I'll give an explicit example in a later question to avoid confounding issues.
(Of course, as an alternative to a reference, I'd be happy if someone can give a quick explanation here, but I don't want to ask that anyone rewrite a textbook on my behalf.)
Mathias Fleury (May 01 2024 at 05:30):[simp] is for the simplifier to pick up automatically (that is in the prog-prove)
Mathias Fleury (May 01 2024 at 05:32):intro / dest: https://isabelle.in.tum.de/doc/tutorial.pdf, chapter 5 the rules of the game
Mathias Fleury (May 01 2024 at 05:34):iff is a theorem that other tools can pick up (like blast). No assumptions and only useful if the tool can do something with the result
Mathias Fleury (May 01 2024 at 05:34):Intro / dest rules are usually described for the inductive predicates where they are important for automation
Yong Kiam (May 01 2024 at 05:35):I found this: https://isabelle.systems/conventions/theorem_attributes.html (and that page seems useful in general)
Mathias Fleury (May 01 2024 at 05:36):Mathias Fleury said:
intro / dest: https://isabelle.in.tum.de/doc/tutorial.pdf, chapter 5 the rules of the game
(I suggest reading that chapter at some point of learning Isabelle)
Last updated: May 19 2024 at 04:18 UTC