John Hughes (Jun 14 2025 at 14:37): John Hughes (Jun 14 2025 at 14:37):I see these two modifiers -- intro! and elim! -- used in various places, e.g., in HOL-Algebra, in places like this
lemma id_ring_hom [simp]: "id ∈ ring_hom R R"
by (auto intro!: ring_hom_memI)
but none of the standard documentation seems to say what they are. Can someone give a brief explanation of what they're doing, and how they differ from intro and elim?
Mathias Fleury (Jun 14 2025 at 15:34):intro and elim are apply by auto with a bound (maximum 4 times and 2 times or something like that)
Mathias Fleury (Jun 14 2025 at 15:34):intro! and elim! are applied unconditionnaly
John Hughes (Jun 14 2025 at 15:46):Thanks, Mathias. Is there someplace I could have learned this without resorting to Zulip?
Mathias Fleury (Jun 14 2025 at 15:48):It is mentioned in the tutorial:
The exclamation mark (intro!) signifies
safe rules, which are applied aggressively. Rules given without the exclama-
tion mark are applied reluctantly and their uses can be undone if the search
backtracks. Here the unsafe rule expresses transitivity of the divides relation:
(https://isabelle.in.tum.de/doc/tutorial.pdf, p105)
Last updated: Jun 21 2025 at 01:46 UTC