*To*: Gergely Buday <gbuday at gmail.com>*Subject*: Re: [isabelle] structured proofs vs. verifications*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 2 Jul 2014 15:23:35 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CA+3iOzn+a2qa+mQ+Vrj=gfUgAT+Uww1-x2KExPmX9ZUu0qtc3Q@mail.gmail.com>*References*: <CA+3iOzn+a2qa+mQ+Vrj=gfUgAT+Uww1-x2KExPmX9ZUu0qtc3Q@mail.gmail.com>

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 On 2 Jul 2014, at 15:14, Gergely Buday <gbuday at gmail.com> wrote: > 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? > > - Gergely >

**References**:**[isabelle] structured proofs vs. verifications***From:*Gergely Buday

- Previous by Date: [isabelle] structured proofs vs. verifications
- Next by Date: [isabelle] Surpress warning-squiggly lines in JEdit
- Previous by Thread: [isabelle] structured proofs vs. verifications
- Next by Thread: [isabelle] Surpress warning-squiggly lines in JEdit
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list