Theory Refine_Imperative_HOL.Sepref_ICF_Bindings

theory Sepref_ICF_Bindings
imports Sepref_Tool 
  Collections.Refine_Dflt_ICF
  "IICF/IICF"
begin
  subsection ‹Miscellaneous›
  lemma (in -) rev_append_hnr[param,sepref_import_param]:
    "(rev_append, rev_append)  Alist_rel  Alist_rel  Alist_rel"
    unfolding rev_append_def by parametricity
  
  subsection ‹Sets by List›

  (* TODO: Move to Collections *)
  lemma lsr_finite[simp, intro]: "(l,s)Rlist_set_rel  finite s"
    by (auto simp: list_set_rel_def br_def)

  lemma it_to_sorted_list_triv:  
    assumes "distinct l"
    shows "RETURN l  it_to_sorted_list (λ_ _. True) (set l)"
    using assms unfolding it_to_sorted_list_def
    by refine_vcg auto

  lemma [sepref_gen_algo_rules]: "GEN_ALGO (return) (IS_TO_SORTED_LIST (λ_ _. True) (pure (Alist_set_rel)) (pure A))"
    unfolding GEN_ALGO_def IS_TO_SORTED_LIST_def
    apply (simp add: list_assn_pure_conv)
    apply rule
    apply rule
    apply (sep_auto simp: pure_def intro: it_to_sorted_list_triv simp: list_set_rel_def br_def)
    done

  lemma list_set_rel_compp:
    assumes "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A"  
    shows "Idlist_set_rel O Aset_rel = Alist_set_rel"
    unfolding list_set_rel_def
  proof (safe; clarsimp simp: in_br_conv)  
    fix x z
    assume "(set x,z)Aset_rel" "distinct x"
    from obtain_list_from_setrel[OF IS_RIGHT_UNIQUE A this(1)] obtain zl where
      [simp]: "z = set zl" and X_ZL: "(x, zl)  Alist_rel" .
        
    have "distinct zl" 
      using param_distinct[OF assms, THEN fun_relD, OF X_ZL] distinct x
      by auto  
    show "(x,z)  Alist_rel O br set distinct"  
      apply (rule relcompI[OF X_ZL])
      by (auto simp: in_br_conv distinct zl)  
  next    
    fix x y
    assume XY: "(x, y)  Alist_rel" and "distinct y"  

    have "distinct x" 
      using param_distinct[OF assms, THEN fun_relD, OF XY] distinct y
      by auto  
      
    show "(x, set y)  br set distinct O Aset_rel"  
      apply (rule relcompI[where b="set x"])
      subgoal by (auto simp: in_br_conv distinct x)
      subgoal by (rule param_set[OF IS_RIGHT_UNIQUE A, THEN fun_relD, OF XY])
      done  
  qed

  lemma GEN_OP_EQ_Id: "GEN_OP (=) (=) (IdIdbool_rel)" by simp

  hide_const (open) Intf_Set.op_set_isEmpty Intf_Set.op_set_delete

  lemma autoref_import_set_unfolds:
    "{} = op_set_empty"
    "uncurry (RETURN oo (∈)) = uncurry (RETURN oo op_set_member)"
    "Intf_Set.op_set_isEmpty = IICF_Set.op_set_is_empty"
    "Intf_Set.op_set_delete = IICF_Set.op_set_delete"
    "insert = IICF_Set.op_set_insert"
    by (auto intro!: ext)


  context fixes A :: "'a  'ai  assn" begin
    private lemma APA: "PROP Q; CONSTRAINT is_pure A  PROP Q" .
    private lemma APAru: "PROP Q; CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A  PROP Q" .
    private lemma APAlu: "PROP Q; CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A  PROP Q" .
    private lemma APAbu: "PROP Q; CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A; CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A  PROP Q" .
    definition "list_set_assn = pure (Idlist_set_rel O the_pure Aset_rel)"
    context
      notes [fcomp_norm_unfold] = list_set_assn_def[symmetric]
      notes [simp] = IS_LEFT_UNIQUE_def
    begin

      lemmas hnr_op_ls_empty = list_set_autoref_empty[of Id, sepref_param, unfolded autoref_import_set_unfolds,
        FCOMP op_set_empty.fref[of "the_pure A"]]
      lemmas hnr_mop_ls_empty = hnr_op_ls_empty[FCOMP mk_mop_rl0_np[OF mop_set_empty_alt]]

      definition [simp]: "op_ls_empty = op_set_empty"
      sepref_register op_ls_empty
    
      lemmas hnr_op_ls_is_empty[sepref_fr_rules] = list_set_autoref_isEmpty[of Id, sepref_param, THEN APA, unfolded autoref_import_set_unfolds,
        FCOMP op_set_is_empty.fref[of "the_pure A"]]
      lemmas hnr_mop_ls_is_empty[sepref_fr_rules] = hnr_op_ls_is_empty[FCOMP mk_mop_rl1_np[OF mop_set_is_empty_alt]]

      lemmas hnr_op_ls_member[sepref_fr_rules] = list_set_autoref_member[OF GEN_OP_EQ_Id, sepref_param, THEN APAlu, unfolded autoref_import_set_unfolds,
        FCOMP op_set_member.fref[of "the_pure A"]]
      lemmas hnr_mop_ls_member[sepref_fr_rules] = hnr_op_ls_member[FCOMP mk_mop_rl2_np[OF mop_set_member_alt]]

      lemmas hnr_op_ls_insert[sepref_fr_rules] = list_set_autoref_insert[OF GEN_OP_EQ_Id, sepref_param, THEN APAru, unfolded autoref_import_set_unfolds,
        FCOMP op_set_insert.fref[of "the_pure A"]]
      lemmas hnr_mop_ls_insert[sepref_fr_rules] = hnr_op_ls_insert[FCOMP mk_mop_rl2_np[OF mop_set_insert_alt]]

      lemmas hnr_op_ls_delete[sepref_fr_rules] = list_set_autoref_delete[OF GEN_OP_EQ_Id, sepref_param, THEN APAbu, unfolded autoref_import_set_unfolds,
        FCOMP op_set_delete.fref[of "the_pure A"]]
      lemmas hnr_mop_ls_delete[sepref_fr_rules] = hnr_op_ls_delete[FCOMP mk_mop_rl2_np[OF mop_set_delete_alt]]

      text ‹Adapting this optimization from Autoref. ›
      sepref_decl_op set_insert_dj: "insert" :: "[λ(x,s). xs]f K ×r Kset_rel  Kset_rel" 
        where "IS_RIGHT_UNIQUE K" "IS_LEFT_UNIQUE K" .
  
      lemma fold_set_insert_dj: "Set.insert = op_set_insert_dj" by simp

      lemma ls_insert_dj_hnr_aux: 
        "(uncurry (return oo Cons), uncurry mop_set_insert_dj)  (pure Id)k *a (pure (Idlist_set_rel))k a pure (Idlist_set_rel)"
        using list_set_autoref_insert_dj[where R=Id,param_fo]
        apply (sep_auto intro!: hfrefI hn_refineI simp: pure_def refine_pw_simps eintros del: exI)
        apply force
        done

      lemmas ls_insert_dj_hnr[sepref_fr_rules] = ls_insert_dj_hnr_aux[THEN APAbu, FCOMP mop_set_insert_dj.fref[of "the_pure A"]]  
      lemmas ls_insert_dj_hnr_mop[sepref_fr_rules] 
        = ls_insert_dj_hnr[FCOMP mk_op_rl2[OF mop_set_insert_dj_alt]]

      private lemma hd_in_set_conv: "hd l  set l  l[]" by auto
    
      lemma ls_pick_hnr_aux: "(return o hd, mop_set_pick)  (pure (Idlist_set_rel))k a id_assn"
        apply (sep_auto 
          intro!: hfrefI hn_refineI 
          simp: pure_def IS_PURE_def IS_ID_def list_set_rel_def refine_pw_simps
          eintros del: exI)
        apply (auto simp: in_br_conv hd_in_set_conv)
        done    

      lemmas ls_pick_hnr[sepref_fr_rules] = ls_pick_hnr_aux[THEN APA,FCOMP mop_set_pick.fref[of "the_pure A"]]
      lemma ls_pick_hnr_mop[sepref_fr_rules]: "CONSTRAINT is_pure A  (return  hd, op_set_pick)  [λs. s{}]a list_set_assnk  A"
        using ls_pick_hnr
        by (simp add: hfref_to_ASSERT_conv mop_set_pick_alt[abs_def])

    end
  end    

  interpretation ls: set_custom_empty "return []" op_ls_empty
    by unfold_locales simp
  lemmas [sepref_fr_rules] = hnr_op_ls_empty[folded op_ls_empty_def]
    

end