Are apply style and Isar-proofs equivalents? This is a question that I have thougth for some time. Of course, Isar-proofs are much more readable, maintanable and easy to write (?) but my question is whether you could prove exactly the same things with both styles.
As an example, I'm currently working on a proof where I need to leave:
apply(simp split: prod.splits)
using some_lemma by fastforce
What is the equivalent form of these commands in apply and Isar style? Actually, I'm more interested in the Isar style since I'm told that it is bad style to mix styles.
The equivalent Isar style would be:
have "P"
using some_lemma by fastforce
then have "Q"
by (simp split: prod.splits)
Where "P" is represents the intermediate goal state after the first apply.
In general, anything provable can be proved both in Isar and in apply style; both have their strengths and weaknesses.
I personally use the style where I try to structure my proofs outside-in: outside (like induction) Isar, and if necessary, inside (like simplification, low-level stuff) with apply.
In general though I recommend you stay within Isar as much as possible.