Theory Refine_Imperative_HOL.IICF_List_SetO

section ‹Sets by Lists that Own their Elements›
theory IICF_List_SetO
imports "../Intf/IICF_Set"
begin
  text ‹Minimal implementation, only supporting a few operations›

  definition "lso_assn A ≡ hr_comp (list_assn A) (br set (λ_. True))"
  lemmas [fcomp_norm_unfold] = lso_assn_def[symmetric]
  lemma lso_is_pure[safe_constraint_rules]: "is_pure A ⟹ is_pure (lso_assn A)"
    unfolding lso_assn_def by safe_constraint

  lemma lso_empty_aref: "(uncurry0 (RETURN []), uncurry0 (RETURN op_set_empty)) 
    ∈ unit_rel  →⇩f ⟨br set (λ_. True)⟩nres_rel"
    by (auto simp: in_br_conv intro!: frefI nres_relI)

  lemma lso_ins_aref: "(uncurry (RETURN oo ((#) )), uncurry (RETURN oo op_set_insert)) 
    ∈ Id ×⇩r br set (λ_. True) →⇩f ⟨br set (λ_. True)⟩nres_rel"
    by (auto simp: in_br_conv intro!: frefI nres_relI)

  sepref_decl_impl (no_register) lso_empty: hn_Nil[to_hfref] uses lso_empty_aref .  
  definition [simp]: "op_lso_empty ≡ op_set_empty"
  lemma lso_fold_custom_empty:
    "{} = op_lso_empty"
    "op_set_empty = op_lso_empty"
    by auto
  lemmas [sepref_fr_rules] = lso_empty_hnr[folded op_lso_empty_def]

  sepref_decl_impl lso_insert: hn_Cons[to_hfref] uses lso_ins_aref .
    
  thm hn_Cons[FCOMP lso_ins_aref]  

  (* TODO: Allow (controlled) backtracking over comb-rules, then we can have a general list-bex operation! *)
  definition [simp]: "op_lso_bex P S ≡ ∃x∈S. P x"
  lemma fold_lso_bex: "Bex ≡ λs P. op_lso_bex P s" by auto

  definition [simp]: "mop_lso_bex P S ≡ ASSERT (∀x∈S. ∃y. P x = RETURN y) ⪢ RETURN (∃x∈S. P x = RETURN True)"

  lemma op_mop_lso_bex:  "RETURN (op_lso_bex P S) = mop_lso_bex (RETURN o P) S" by simp

  sepref_register op_lso_bex
  lemma lso_bex_arity[sepref_monadify_arity]: 
    "op_lso_bex ≡ λ⇩2P s. SP op_lso_bex$(λ⇩2x. P$x)$s" by (auto intro!: eq_reflection ext)
  lemma op_lso_bex_monadify[sepref_monadify_comb]:  
    "EVAL$(op_lso_bex$(λ⇩2x. P x)$s) ≡ (⤜) $(EVAL$s)$(λ⇩2s. mop_lso_bex$(λ⇩2x. EVAL $ P x)$s)" by simp

  definition "lso_abex P l ≡ nfoldli l (Not) (λx _. P x) False"
  lemma lso_abex_to_set: "lso_abex P l ≤ mop_lso_bex P (set l)"
  proof -
    { fix b
      have "nfoldli l (Not) (λx _. P x) b ≤ ASSERT (∀x∈set l. ∃y. P x = RETURN y) ⪢ RETURN ((∃x∈set l. P x = RETURN True) ∨ b)"
        apply (induction l arbitrary: b) 
        applyS simp
        applyS (clarsimp simp add: pw_le_iff refine_pw_simps; blast) 
        done
    } from this[of False] show ?thesis by (simp add: lso_abex_def)
  qed    



  locale lso_bex_impl_loc = 
    fixes Pi and P :: "'a ⇒ bool nres"
    fixes li :: "'c list" and l :: "'a list"
    fixes A :: "'a ⇒ 'c ⇒ assn"
    fixes F :: assn
    
    assumes Prl: "⋀x xi. ⟦x∈set l⟧ ⟹ hn_refine (F * hn_ctxt A x xi) (Pi xi) (F * hn_ctxt A x xi) bool_assn (P x)"
  begin  
    sepref_register l
    sepref_register P

    lemma [sepref_comb_rules]:
      assumes "Γ ⟹⇩t F' * F * hn_ctxt A x xi"
      assumes "x∈set l"
      shows "hn_refine Γ (Pi xi) (F' * F * hn_ctxt A x xi) bool_assn (P$x)"
      using hn_refine_frame[OF Prl[OF assms(2)], of Γ F'] assms(1)
      by (simp add: assn_assoc)


    schematic_goal lso_bex_impl: 
      "hn_refine (hn_ctxt (list_assn A) l li * F) (?c) (F * hn_ctxt (list_assn A) l li) bool_assn (lso_abex P l)"
      unfolding lso_abex_def[abs_def]
      by sepref
  end    
  concrete_definition lso_bex_impl uses lso_bex_impl_loc.lso_bex_impl  
  
  lemma hn_lso_bex[sepref_prep_comb_rule,sepref_comb_rules]: 
    assumes FR: "Γ ⟹⇩t hn_ctxt (lso_assn A) s li * F"
    assumes Prl: "⋀x xi. ⟦x∈s⟧ ⟹ hn_refine (F * hn_ctxt A x xi) (Pi xi) (F * hn_ctxt A x xi) bool_assn (P x)"
    notes [simp del] = mop_lso_bex_def
    shows "hn_refine Γ (lso_bex_impl Pi li) (F * hn_ctxt (lso_assn A) s li) bool_assn (mop_lso_bex$(λ⇩2x. P x)$s)"
    apply (rule hn_refine_cons_pre[OF FR])
    apply (clarsimp simp: hn_ctxt_def lso_assn_def hr_comp_def in_br_conv hnr_pre_ex_conv)
    apply (rule hn_refine_preI)
    apply (drule mod_starD; clarsimp)
    apply (rule hn_refine_ref[OF lso_abex_to_set])
  proof -
    fix l assume [simp]: "s=set l"

    from Prl have Prl': "⋀x xi. ⟦x∈set l⟧ ⟹ hn_refine (F * hn_ctxt A x xi) (Pi xi) (F * hn_ctxt A x xi) bool_assn (P x)"
      by simp

    show "hn_refine (list_assn A l li * F) (lso_bex_impl Pi li) (∃⇩Aba. F * list_assn A ba li * ↑ (set l = set ba)) bool_assn
           (lso_abex P l)"
      apply (rule hn_refine_cons[OF _ lso_bex_impl.refine])
      applyS (simp add: hn_ctxt_def; rule entt_refl)
      apply1 unfold_locales apply1 (rule Prl') applyS simp
      applyS (sep_auto intro!: enttI simp: hn_ctxt_def)
      applyS (rule entt_refl)
      done
  qed    

end