Theory EPAC_Steps_Refine

theory EPAC_Steps_Refine
  imports EPAC_Checker
begin


lemma is_CL_import[sepref_fr_rules]:
  assumes ‹CONSTRAINT is_pure K›  ‹CONSTRAINT is_pure V› ‹CONSTRAINT is_pure R›
  shows
    ‹(return o pac_res, RETURN o pac_res) ∈ [λx. is_Extension x ∨ is_CL x]⇩a
       (pac_step_rel_assn K V R)⇧k → V›
    ‹(return o pac_src1, RETURN o pac_src1) ∈ [λx. is_Del x]⇩a (pac_step_rel_assn K V R)⇧k → K›
    ‹(return o new_id, RETURN o new_id) ∈ [λx. is_Extension x ∨ is_CL x]⇩a (pac_step_rel_assn K V R)⇧k → K›
    ‹(return o is_CL, RETURN o is_CL) ∈  (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
    ‹(return o is_Del, RETURN o is_Del) ∈ (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
    ‹(return o new_var, RETURN o new_var) ∈ [λx. is_Extension x]⇩a (pac_step_rel_assn K V R)⇧k → R›
    ‹(return o is_Extension, RETURN o is_Extension) ∈ (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
  using assms
  by (sepref_to_hoare; sep_auto simp: pac_step_rel_assn_alt_def is_pure_conv ent_true_drop pure_app_eq
    split: pac_step.splits; fail)+


lemma is_CL_import2[sepref_fr_rules]:
  assumes ‹CONSTRAINT is_pure K›  ‹CONSTRAINT is_pure V›
  shows
    ‹(return o pac_srcs, RETURN o pac_srcs) ∈ [λx. is_CL x]⇩a (pac_step_rel_assn K V R)⇧k →  list_assn (V ×⇩a K)›
  using assms
  by (sepref_to_hoare; sep_auto simp: pac_step_rel_assn_alt_def is_pure_conv ent_true_drop pure_app_eq
    assms[simplified] list_assn_pure_conv
    split: pac_step.splits)

lemma is_Mult_lastI:
  ‹¬ is_CL b ⟹ ¬is_Extension b ⟹ is_Del b›
  by (cases b) auto

end