Gergely Buday (Feb 06 2024 at 13:20): Gergely Buday (Feb 06 2024 at 13:20):At https://isabelle.in.tum.de/doc/tutorial.pdf#page=79
in section 5.3 Elimination and 5.4 Destruction Rules there are examples of using the erule and drule methods in apply-style proofs. I rephrased these proofs in Isar but I had to use only the rule method. Did this happen because in a forward Isar proof that's natural? Is there any place for erule or drule in an Isar proof?
Kevin Kappelmann (Feb 06 2024 at 20:11):The question is unclear to me. Is there any unexpected behaviour of either rule, drule, or erule?
Maybe this page, particularly the linked theory at the top, answers your questions https://isabelle.systems/cookbook/src/proofs/methods/
Manuel Eberl (Feb 09 2024 at 11:14):Yes, it doesn't really make sense to use drule and erule in an Isar proof I think. They operate on hypotheses, and you normally don't have those in Isar (only chained facts). Unless you do an apply script or build a more complex proof method to solve an Isar goal, of course. For those purposes I have very rarely used erule in Isar.
Manuel Eberl (Feb 09 2024 at 11:15):I think that for non-automatic proof methods in Isar I mainly use rule and intro and subst. Occasionally fold/unfold, simp only:, and elim.
Last updated: May 02 2024 at 01:06 UTC