I have a goal invariant (smallStep fac (i, f)) a r And am proving it by case-splitting over i. I am proving the case i = 0 and I would like to simplify the goal in that case (invariant (smallStep fac (i, f)) a r will simplify given i = 0). However, I am not sure how to do this in Isar, since proof steps work with forward reasoning. I found apply_end() in the Isar reference, but this doesn't allow one to use any additional facts (such as the aforementioned i=0). Because of this I feel like I'm stumbling in the dark a bit. Isn't it somehow possible to "burn the candle at both ends", i.e. use both forward and backward reasoning in structured proofs?
I often work backwards and forwards. I often start with:
proof -
(*forward part, currently empty*)
(*backward part*)
show ?thesis
sorry
Then if I need go backwards, I either write things above the show ?thesis or below it, like:
proof -
(*forward part*)
have "something"
using assms sorry
(*backward part*)
have "?P 0"
sorry
moreover have "?P i" if "i > 0"
sorry
ultimately show ?thesis
by (cases i) auto
or
proof -
(*forward part*)
have "something"
using assms sorry
(*backward part*)
show ?thesis
proof (cases i)
case 0
(*forward part*)
(*backward part*)
show ?cases
using 0
sorry
next
case (Suc j)
(*forward part*)
(*backward part*)
show ?cases
using Suc
sorry
qed