Re: [isabelle] structured proofs vs. verifications



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
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.