Work backwards from goal in structured (isar) proof

Question

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?

Answer 1

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