Theory Worklist_Subsumption_Impl

theory Worklist_Subsumption_Impl
imports "../IICF/IICF" Worklist_Subsumption
begin

  locale Worklist2_Defs = Worklist1_Defs +
    fixes A :: "'a ⇒ 'ai ⇒ assn"
    fixes succsi :: "'ai ⇒ 'ai list Heap"
    fixes a⇩0i :: "'ai Heap"
    fixes Fi :: "'ai ⇒ bool Heap"
    fixes Lei :: "'ai ⇒ 'ai ⇒ bool Heap"

  locale Worklist2 = Worklist2_Defs + Worklist1 +
    (* TODO: This is the easy variant: Operations cannot depend on additional heap. *)
    assumes [sepref_fr_rules]: "(uncurry0 a⇩0i, uncurry0 (RETURN (PR_CONST a⇩0))) ∈ unit_assn⇧k →⇩a A"
    assumes [sepref_fr_rules]: "(Fi,RETURN o PR_CONST F) ∈ A⇧k →⇩a bool_assn"
    assumes [sepref_fr_rules]: "(uncurry Lei,uncurry (RETURN oo PR_CONST (≼))) ∈ A⇧k *⇩a A⇧k →⇩a bool_assn"
    assumes [sepref_fr_rules]: "(succsi,RETURN o PR_CONST succs) ∈ A⇧k →⇩a list_assn A"
  begin
    sepref_register "PR_CONST a⇩0" "PR_CONST F" "PR_CONST (≼)" "PR_CONST succs"

    lemma [def_pat_rules]:
      "a⇩0 ≡ UNPROTECT a⇩0" "F ≡ UNPROTECT F" "(≼) ≡ UNPROTECT (≼)" "succs ≡ UNPROTECT succs"
      by simp_all
    
    lemma take_from_mset_as_mop_mset_pick: "take_from_mset = mop_mset_pick"
      apply (intro ext)
      unfolding take_from_mset_def[abs_def] 
      by (auto simp: pw_eq_iff refine_pw_simps)

    lemma [safe_constraint_rules]: "CN_FALSE is_pure A ⟹ is_pure A" by simp

    sepref_thm worklist_algo2 is "uncurry0 worklist_algo1" :: "unit_assn⇧k →⇩a bool_assn"
      unfolding worklist_algo1_def add_succ1_def
      supply [[goals_limit = 1]]
      apply (rewrite in "Let ⌑ _" lso_fold_custom_empty)
      apply (rewrite in "{#a⇩0#}" lmso_fold_custom_empty)
      unfolding take_from_mset_as_mop_mset_pick fold_lso_bex
      by sepref

  end

  concrete_definition worklist_algo2 
    for Lei a⇩0i Fi succsi
    uses Worklist2.worklist_algo2.refine_raw is "(uncurry0 ?f,_)∈_"
  thm worklist_algo2_def

  context Worklist2 begin
    lemma Worklist2_this: "Worklist2 E a⇩0 F (≼) succs A succsi a⇩0i Fi Lei" 
      by unfold_locales

    lemma hnr_F_reachable: "(uncurry0 (worklist_algo2 Lei a⇩0i Fi succsi), uncurry0 (RETURN F_reachable)) 
      ∈ unit_assn⇧k →⇩a bool_assn"
      using worklist_algo2.refine[OF Worklist2_this, 
        FCOMP worklist_algo1_ref[THEN nres_relI],
        FCOMP worklist_algo_correct[THEN Id_SPEC_refine, THEN nres_relI]]
      by (simp add: RETURN_def)

  end

  context Worklist1 begin
    sepref_decl_op F_reachable :: "bool_rel" .
    lemma [def_pat_rules]: "F_reachable ≡ op_F_reachable" by simp


    lemma hnr_op_F_reachable:
      assumes "GEN_ALGO a⇩0i (λa⇩0i. (uncurry0 a⇩0i, uncurry0 (RETURN a⇩0)) ∈ unit_assn⇧k →⇩a A)"
      assumes "GEN_ALGO Fi (λFi. (Fi,RETURN o F) ∈ A⇧k →⇩a bool_assn)"
      assumes "GEN_ALGO Lei (λLei. (uncurry Lei,uncurry (RETURN oo (≼))) ∈ A⇧k *⇩a A⇧k →⇩a bool_assn)"
      assumes "GEN_ALGO succsi (λsuccsi. (succsi,RETURN o succs) ∈ A⇧k →⇩a list_assn A)"
      shows "(uncurry0 (worklist_algo2 Lei a⇩0i Fi succsi), uncurry0 (RETURN (PR_CONST op_F_reachable))) 
        ∈ unit_assn⇧k →⇩a bool_assn"
    proof -
      from assms interpret Worklist2 E a⇩0 F "(≼)" succs A succsi a⇩0i Fi Lei 
        by (unfold_locales; simp add: GEN_ALGO_def)
    
      from hnr_F_reachable show ?thesis by simp    
    qed  

    sepref_decl_impl hnr_op_F_reachable .
  end

end