Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Gergely Buday <gbuday@gmail.com>
Hi,
upon trying to verify some easy theorems I get the response that why I
don't solve them by simp_all or some other automatic method. I do this
as I want to learn how to do a rigorous, step-by-step structured Isar
proof.
But it is clear that for larger theories and more diffcult lemmas one
has to combine structured proofs with automatic methods. It is also
more economic if the goal is not a research paper but a verification
per se.
Is it written down somewhere which kind of proofs can be solved
automatically, and which need more user interaction? What I have seen
tells me that e.g. induction should be explicit as Isabelle does not
figure out which variable is worth doing induction upon.
If there is no explicit writing on this, which afp entry or regular
theory would you recommend to read?
Email Gateway (Aug 19 2022 at 14:51):From: Lawrence Paulson <lp15@cam.ac.uk>
The proofs that are most likely to be done by a simple induction followed by auto are properties of recursively defined functions. Once you have existential quantifiers in your assumptions, forward reasoning using other lemmas, or tricky calculations involving arithmetic formulas, then you find yourself needing a structured proof.
Often it easiest simply to try induction and auto, to see what is left over. Sometimes these leftover subgoals suggest lemmas to prove first. You can even prove these locally in “nested blocks” (admittedly, an advanced technique); by proving these lemmas first, you may find that induction and auto will now do the job.
Larry
Last updated: Apr 26 2024 at 20:16 UTC