add helper lemma for proof generation of CFG optimizations

This helper lemma is used in cases when the loop head set representation
is different in a proof goal and in a lemma. Previously, the simplifier
was used on the proof goal, but the result does not always match the
representation of the lemma that is then applied. Now, the helper lemma
is applied instead.

Author: gauravpartha

BoogieLang/CFGOptimizationsLoop.thy

@@ -308,6 +308,12 @@ next
     by simp
 qed
 
+lemma hybrid_block_lemma_loop_eq_loop_heads:
+  assumes "hybrid_block_lemma_loop A M \<Lambda> \<Gamma> \<Omega> G  G' succ tgt_block tgt_cmds_0 lsLoopHeads1 posts"
+      and "lsLoopHeads1 = lsLoopHeads2"
+    shows "hybrid_block_lemma_loop A M \<Lambda> \<Gamma> \<Omega> G  G' succ tgt_block tgt_cmds_0 lsLoopHeads2 posts"
+  using assms
+  by simp
 
 subsection \<open>Main Lemmas for Loops\<close>