Theory WB_More_Sepref_LLVM

theory WB_More_Sepref_LLVM
  imports
    Isabelle_LLVM.IICF
    WB_More_Refinement
begin


lemma refine_ASSERT_move_to_pre:
  assumes ‹(uncurry g, uncurry h) ∈ [uncurry P]⇩a A *⇩a B → x_assn›
  shows
  ‹(uncurry g, uncurry (λN C. do {ASSERT (P N C); h N C}))
    ∈ A *⇩a B →⇩a x_assn›
  apply sepref_to_hoare
  apply vcg
  apply (subst POSTCOND_def hn_ctxt_def sep_conj_empty' pure_true_conv EXTRACT_def)+
  apply (auto simp: nofail_ASSERT_bind)
  apply (rule assms[to_hnr, simplified, unfolded hn_ctxt_def hn_refine_def htriple_def
    sep_conj_empty' pure_true_conv sep.add_assoc, rule_format])
  apply auto
  done

lemma refine_ASSERT_move_to_pre0:
  assumes ‹(g, h) ∈ [P]⇩a A  → x_assn›
  shows
  ‹(g, (λN. do {ASSERT (P N); h N}))
    ∈ A →⇩a x_assn›
  apply sepref_to_hoare
  apply vcg
  apply (subst POSTCOND_def hn_ctxt_def sep_conj_empty' pure_true_conv EXTRACT_def)+
  apply (auto simp: nofail_ASSERT_bind)
  apply (rule assms[to_hnr, simplified, unfolded hn_ctxt_def hn_refine_def htriple_def
    sep_conj_empty' pure_true_conv sep.add_assoc, rule_format])
  apply auto
  done

lemma refine_ASSERT_move_to_pre2:
  assumes ‹(uncurry2 g, uncurry2 h) ∈ [uncurry2 P]⇩a A *⇩a B *⇩a C → x_assn›
  shows
  ‹(uncurry2 g, uncurry2 (λN C D. do {ASSERT (P N C D); h N C D}))
    ∈ A *⇩a B *⇩a C →⇩a x_assn›
  apply sepref_to_hoare
  apply vcg
  apply (subst POSTCOND_def hn_ctxt_def sep_conj_empty' pure_true_conv EXTRACT_def)+
  apply (auto simp: nofail_ASSERT_bind)
  apply (rule assms[to_hnr, simplified, unfolded hn_ctxt_def hn_refine_def htriple_def
    sep_conj_empty' pure_true_conv sep.add_assoc, rule_format])
  apply auto
  done
end