Equivalence between apply and Isar styles in Isabelle

user_5069802 0
Viewed 98

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.

isabelle
1 Answers

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.

user_47769390
Related