Some Lessons Learned on Writing Predicate Logic Proofs in Isabelle/Isar

We describe our experience with the use of the proving assistant Isabelle and its proof development language Isar for formulating and proving formal mathematical statements. Our focus is on how to use classical predicate logic and well established proof principles for this purpose, bypassing Isabelle's meta-logic and related technical aspects as much as possible. By a small experiment on the proof of (part of a) verification condition for a program, we were able to identify a number of important patterns that arise in such proofs yielding to a workflow with which we feel personally comfortable; the resulting guidelines may serve as a starting point for a the application of Isabelle/Isar for the "average" mathematical user (i.e, a mathematical user who is not interested in Isabelle/Isar per se but just wants to use it as a tool for computer-supported formal theory development).