[isabelle] structured proofs vs. verifications



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.