Theory Refine_Imperative_HOL.IICF_Impl_Heapmap

section ‹Implementation of Heaps by Arrays›
theory IICF_Impl_Heapmap
imports IICF_Abs_Heapmap "../IICF_Indexed_Array_List"
begin

(* TODO/FIXME: Division setup of the code generator is a mess.
  TODO: Why does [code_unfold] not work to rewrite "x div 2"?
*)
text ‹Some setup to circumvent the really inefficient implementation 
  of division in the code generator, which has to consider several
  cases for negative divisors and dividends. ›
definition [code_unfold]: 
  "efficient_nat_div2 n     
     nat_of_integer (fst (Code_Numeral.divmod_abs (integer_of_nat n) 2))"

lemma efficient_nat_div2[simp]: "efficient_nat_div2 n = n div 2"
  by (simp add: efficient_nat_div2_def nat_of_integer.rep_eq)

  type_synonym 'v hma = "nat list × ('v list)"
  sepref_decl_intf 'v i_hma is "nat list × (nat  'v)"

  locale hmstruct_impl = hmstruct prio for prio :: "'v::heap  'p::linorder"
  begin
    lemma param_prio: "(prio,prio)  Id  Id" by simp
    lemmas [sepref_import_param] = param_prio
    sepref_register prio
  end

  context
    fixes maxsize :: nat
    fixes prio :: "'v::heap  'p::linorder"
    notes [map_type_eqs] = map_type_eqI[Pure.of "TYPE((nat,'v) ahm)" "TYPE('v i_hma)"]
  begin

    interpretation hmstruct .
    interpretation hmstruct_impl .
  
    definition "hm_impl1_α  λ(pq,ml). 
      (pq,λk. if kset pq then Some (ml!k) else None)"

    definition "hm_impl1_invar  λ(pq,ml). 
        hmr_invar (hm_impl1_α (pq,ml))
       set pq  {0..<maxsize}  
       ((pq=[]  ml=[])  (length ml = maxsize))"  

    definition "hm_impl1_weak_invar  λ(pq,ml). 
        set pq  {0..<maxsize}  
       ((pq=[]  ml=[])  (length ml = maxsize))"  

    definition "hm_impl1_rel  br hm_impl1_α hm_impl1_invar"
    definition "hm_weak_impl'_rel  br hm_impl1_α hm_impl1_weak_invar"


    lemmas hm_impl1_rel_defs = 
      hm_impl1_rel_def hm_weak_impl'_rel_def hm_impl1_weak_invar_def hm_impl1_invar_def hm_impl1_α_def in_br_conv
    

    lemma hm_impl_α_fst_eq: 
        "(x1, x2) = hm_impl1_α (x1a, x2a)  x1 = x1a"
      unfolding hm_impl1_α_def by (auto split: if_split_asm)


    term hm_empty_op  
    definition hm_empty_op' :: "'v hma nres" 
      where "hm_empty_op'  do {
        let pq = op_ial_empty_sz maxsize;
        let ml = op_list_empty;
        RETURN (pq,ml)
      }"


    lemma hm_empty_op'_refine: "(hm_empty_op', hm_empty_op)  hm_impl1_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_empty_op'_def hm_empty_op_def hm_impl1_rel_defs 
      by (auto simp: in_br_conv)

    definition hm_length' :: "'v hma  nat" where "hm_length'  λ(pq,ml). length pq"

    lemma hm_length'_refine: "(RETURN o hm_length',RETURN o hm_length)  hm_impl1_rel  nat_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_length'_def hm_length_def hm_impl1_rel_defs
      by (auto)
      
    term hm_key_of_op  
    definition "hm_key_of_op'  λ(pq,ml) i. ASSERT (i>0)  mop_list_get pq (i - 1)"
    lemma hm_key_of_op'_refine: "(hm_key_of_op', hm_key_of_op)  hm_impl1_rel  nat_rel  nat_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_key_of_op'_def hm_key_of_op_def hm_impl1_rel_defs
      by (auto)

    term hm_lookup  
    definition "hm_lookup_op'  λ(pq,ml) k. do {
      if (k<maxsize) then do {    ― ‹TODO: This check can be eliminated, but this will complicate refinement of keys in basic ops›
        let c = op_list_contains k pq;
        if c then do {
          v  mop_list_get ml k;
          RETURN (Some v)
        } else RETURN None
      } else RETURN None  
    }"
      
    lemma hm_lookup_op'_refine: "(uncurry hm_lookup_op', uncurry (RETURN oo hm_lookup)) 
       (hm_impl1_rel ×r nat_rel) f Idoption_relnres_rel"
      apply (intro frefI nres_relI)
      unfolding hm_lookup_op_def hm_lookup_op'_def o_def uncurry_def
      apply refine_vcg
      apply (auto simp: hm_impl1_rel_defs heapmap_α_def hmr_invar_def)
      done

    term hm_contains_key_op  
    definition "hm_contains_key_op'  λk (pq,ml). do {
      if (k<maxsize) then do {    ― ‹TODO: This check can be eliminated, but this will complicate refinement of keys in basic ops›
        RETURN (op_list_contains k pq)
      } else RETURN False  
    }"
      
    lemma hm_contains_key_op'_refine: "(uncurry hm_contains_key_op', uncurry hm_contains_key_op) 
       (nat_rel ×r hm_impl1_rel) f bool_relnres_rel"
      apply (intro frefI nres_relI)
      unfolding hm_contains_key_op_def hm_contains_key_op'_def o_def uncurry_def PR_CONST_def
      apply refine_vcg
      apply (auto simp: hm_impl1_rel_defs heapmap_α_def hmr_invar_def)
      done


    term hm_valid 

    definition "hm_exch_op'  λ(pq,ml) i j. do {
      ASSERT (hm_valid (hm_impl1_α (pq,ml)) i);
      ASSERT (hm_valid (hm_impl1_α (pq,ml)) j);
      pq  mop_list_swap pq (i - 1) (j - 1);
      RETURN (pq,ml)
    }"

    lemma hm_impl1_relI:
      assumes "hmr_invar b"
      assumes "(a,b)hm_weak_impl'_rel"
      shows "(a,b)hm_impl1_rel"
      using assms
      unfolding hmr_rel_def hm_impl1_rel_def hm_weak_impl'_rel_def in_br_conv
        hm_impl1_weak_invar_def hm_impl1_invar_def
      by auto

    lemma hm_impl1_nres_relI:
      assumes "b n SPEC hmr_invar"
      assumes "(a,b)hm_weak_impl'_relnres_rel"
      shows "(a,b)hm_impl1_relnres_rel"
      using assms hm_impl1_relI
      apply (auto simp: pw_le_iff pw_leof_iff refine_pw_simps in_br_conv nres_rel_def)
      apply blast
      done


    lemma hm_exch_op'_refine: "(hm_exch_op', hm_exch_op)  hm_impl1_rel  nat_rel  nat_rel  hm_impl1_relnres_rel"
      apply (intro fun_relI hm_impl1_nres_relI[OF hm_exch_op_invar])
      unfolding hm_exch_op'_def hm_exch_op_def
      apply (auto simp: pw_le_iff refine_pw_simps nres_rel_def
          hm_impl1_rel_def in_br_conv split: prod.splits)
      apply (auto simp: hm_impl1_α_def)
      unfolding hm_impl1_rel_defs
      apply auto
      done


    term hm_index_op  

    definition "hm_index_op'  λ(pq,ml) k. 
      do {
        ASSERT (hm_impl1_invar (pq,ml)  heapmap_α (hm_impl1_α (pq,ml)) k  None  kset pq);
        i  mop_list_index pq k;
        RETURN (i+1)
      }"
    lemma hm_index_op'_refine: "(hm_index_op',hm_index_op) 
       hm_impl1_rel  nat_rel  nat_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_index_op'_def hm_index_op_def hm_impl1_rel_defs
      apply (auto simp: pw_le_iff refine_pw_simps heapmap_α_def split: if_split_asm)
      done

    definition hm_update_op' where
      "hm_update_op'  λ(pq,ml) i v. do {
        ASSERT (hm_valid (hm_impl1_α (pq,ml)) i  hm_impl1_invar (pq,ml));
        k  mop_list_get pq (i - 1);
        ml  mop_list_set ml k v;
        RETURN (pq, ml)
      }"
    lemma hm_update_op'_refine: "(hm_update_op', hm_update_op)  hm_impl1_rel  nat_rel  Id  hm_impl1_relnres_rel"  
      apply (intro fun_relI hm_impl1_nres_relI[OF hm_update_op_invar])
      unfolding hm_update_op'_def hm_update_op_def
      apply (auto simp: pw_le_iff refine_pw_simps nres_rel_def
          hm_impl1_rel_def in_br_conv split: prod.splits)
      apply (auto simp: hm_impl1_α_def)
      unfolding hm_impl1_rel_defs
      apply (auto simp: subset_code(1))
      done
      
          
    term hm_butlast_op  

    lemma hm_butlast_op_invar: "hm_butlast_op hm n SPEC hmr_invar"
      unfolding hm_butlast_op_def h.butlast_op_def
      apply refine_vcg
      apply (clarsimp_all simp: hmr_rel_defs map_butlast distinct_butlast)
      apply safe

      apply (auto simp: in_set_conv_nth nth_butlast) []
      apply (metis Suc_pred len_greater_imp_nonempty length_greater_0_conv less_antisym)
      
      apply (auto dest: in_set_butlastD) []

      apply (metis One_nat_def append_butlast_last_id distinct_butlast last_conv_nth not_distinct_conv_prefix)
      done


    definition hm_butlast_op' where
      "hm_butlast_op'  λ(pq,ml). do {
        ASSERT (hmr_invar (hm_impl1_α (pq,ml)));
        pq  mop_list_butlast pq;
        RETURN (pq,ml)
      }"

    lemma set_butlast_distinct_conv: 
      "distinct l  set (butlast l) = set l - {last l}"  
      by (cases l rule: rev_cases; auto)

    lemma hm_butlast_op'_refine: "(hm_butlast_op', hm_butlast_op)  hm_impl1_rel  hm_impl1_relnres_rel"  
      apply (intro fun_relI hm_impl1_nres_relI[OF hm_butlast_op_invar])
      unfolding hm_butlast_op'_def hm_butlast_op_def
      apply (auto simp: pw_le_iff refine_pw_simps nres_rel_def
          hm_impl1_rel_def in_br_conv split: prod.splits)
      apply (auto simp: hm_impl1_α_def)
      unfolding hm_impl1_rel_defs
      apply (auto simp: restrict_map_def) []

      defer

      apply (auto dest: in_set_butlastD) []
      apply (auto intro!: ext 
        simp: hmr_invar_def set_butlast_distinct_conv last_conv_nth
        dest: in_set_butlastD) []
      done

    definition hm_append_op' 
      where "hm_append_op'  λ(pq,ml) k v. do {
        ASSERT (k  set pq  k<maxsize);
        ASSERT (hm_impl1_invar (pq,ml));
        pq  mop_list_append pq k;
        ml  (if length ml = 0 then mop_list_replicate maxsize v else RETURN ml);
        ml  mop_list_set ml k v;
        RETURN (pq,ml)
      }"

    lemma hm_append_op'_refine: "(uncurry2 hm_append_op', uncurry2 hm_append_op) 
       [λ((hm,k),v). k<maxsize]f (hm_impl1_rel ×r nat_rel) ×r Id  hm_impl1_relnres_rel"  
      apply (intro frefI hm_impl1_nres_relI[OF hm_append_op_invar])
      unfolding hm_append_op'_def hm_append_op_def
      apply (auto simp: pw_le_iff refine_pw_simps nres_rel_def
          hm_impl1_rel_def in_br_conv split: prod.splits)
      unfolding hm_impl1_rel_defs
      apply (auto simp: restrict_map_def hmr_invar_def split: prod.splits if_split_asm) 
      done
      
    definition "hm_impl2_rel  prod_assn (ial_assn maxsize id_assn) (array_assn id_assn)"
    definition "hm_impl_rel  hr_comp hm_impl2_rel hm_impl1_rel"

    lemmas [fcomp_norm_unfold] = hm_impl_rel_def[symmetric]

    (*lemma hm_impl_rel_precise[constraint_rules]: "precise hm_impl_rel"
      unfolding hm_impl_rel_def hm_impl1_rel_def hm_impl2_rel_def
      by (constraint_rules)*)


    subsection ‹Implement Basic Operations›  


    lemma param_parent: "(efficient_nat_div2,h.parent)  Id  Id" 
      by (intro fun_relI) (simp add: h.parent_def)
    lemmas [sepref_import_param] = param_parent
    sepref_register h.parent

    lemma param_left: "(h.left,h.left)  Id  Id" by simp
    lemmas [sepref_import_param] = param_left
    sepref_register h.left

    lemma param_right: "(h.right,h.right)  Id  Id" by simp
    lemmas [sepref_import_param] = param_right
    sepref_register h.right

    abbreviation (input) "prio_rel  (Id::('p×'p) set)"

    lemma param_prio_le: "((≤), (≤))  prio_rel  prio_rel  bool_rel" by simp
    lemmas [sepref_import_param] = param_prio_le
    
    lemma param_prio_lt: "((<), (<))  prio_rel  prio_rel  bool_rel" by simp
    lemmas [sepref_import_param] = param_prio_lt

    abbreviation "I_HM_UNF  TYPE(nat list × 'v list)"

    sepref_definition hm_length_impl is "RETURN o hm_length'" :: "hm_impl2_relkanat_assn"
      unfolding hm_length'_def hm_impl2_rel_def
      by sepref
    lemmas [sepref_fr_rules] = hm_length_impl.refine[FCOMP hm_length'_refine]
    sepref_register "hm_length::(nat,'v) ahm  _"

    sepref_definition hm_key_of_op_impl is "uncurry hm_key_of_op'" :: "hm_impl2_relk*anat_assnk anat_assn"
      unfolding hm_key_of_op'_def hm_impl2_rel_def
      by sepref
    lemmas [sepref_fr_rules] = hm_key_of_op_impl.refine[FCOMP hm_key_of_op'_refine]
    sepref_register "hm_key_of_op::(nat,'v) ahm  _"

    context 
      notes [id_rules] = itypeI[Pure.of maxsize "TYPE(nat)"]
      notes [sepref_import_param] = IdI[of maxsize]
    begin


    sepref_definition hm_lookup_impl is "uncurry hm_lookup_op'" :: "(hm_impl2_relk*anat_assnk aoption_assn id_assn)"
      unfolding hm_lookup_op'_def hm_impl2_rel_def
      by sepref
    lemmas [sepref_fr_rules] = 
      hm_lookup_impl.refine[FCOMP hm_lookup_op'_refine]
    sepref_register "hm_lookup::(nat,'v) ahm  _" 

    sepref_definition hm_exch_op_impl is "uncurry2 hm_exch_op'" :: "hm_impl2_reld*anat_assnk*anat_assnk a hm_impl2_rel"
      unfolding hm_exch_op'_def hm_impl2_rel_def
      by sepref
    lemmas [sepref_fr_rules] = hm_exch_op_impl.refine[FCOMP hm_exch_op'_refine]
    sepref_register "hm_exch_op::(nat,'v) ahm  _" 

    sepref_definition hm_index_op_impl is "uncurry hm_index_op'" :: "hm_impl2_relk*aid_assnk a id_assn"
      unfolding hm_index_op'_def hm_impl2_rel_def 
      by sepref
    lemmas [sepref_fr_rules] = hm_index_op_impl.refine[FCOMP hm_index_op'_refine]
    sepref_register "hm_index_op::(nat,'v) ahm  _" 

    sepref_definition hm_update_op_impl is "uncurry2 hm_update_op'" :: "hm_impl2_reld*aid_assnk*aid_assnk a hm_impl2_rel"
      unfolding hm_update_op'_def hm_impl2_rel_def 
      by sepref
    lemmas [sepref_fr_rules] = hm_update_op_impl.refine[FCOMP hm_update_op'_refine]
    sepref_register "hm_update_op::(nat,'v) ahm  _" 


    sepref_definition hm_butlast_op_impl is "hm_butlast_op'" :: "hm_impl2_reld a hm_impl2_rel"
      unfolding hm_butlast_op'_def hm_impl2_rel_def by sepref
    lemmas [sepref_fr_rules] = hm_butlast_op_impl.refine[FCOMP hm_butlast_op'_refine]
    sepref_register "hm_butlast_op::(nat,'v) ahm  _"

    sepref_definition hm_append_op_impl is "uncurry2 hm_append_op'" :: "hm_impl2_reld *a id_assnk *a id_assnk a hm_impl2_rel"
      unfolding hm_append_op'_def hm_impl2_rel_def 
      apply (rewrite array_fold_custom_replicate)
      by sepref
    lemmas [sepref_fr_rules] = hm_append_op_impl.refine[FCOMP hm_append_op'_refine]
    sepref_register "hm_append_op::(nat,'v) ahm  _" 


    subsection ‹Auxiliary Operations›

    lemmas [intf_of_assn] = intf_of_assnI[where R="hm_impl_rel :: (nat,'v) ahm  _" and 'a="'v i_hma"]

    sepref_definition hm_valid_impl is "uncurry (RETURN oo hm_valid)" :: "hm_impl_relk*anat_assnk a bool_assn "
      unfolding hm_valid_def[abs_def]
      by sepref
    lemmas [sepref_fr_rules] = hm_valid_impl.refine
    sepref_register "hm_valid::(nat,'v) ahm  _"


    (* Optimization *)
    definition "hm_the_lookup_op' hm k  do {
      let (pq,ml) = hm;
      ASSERT (heapmap_α (hm_impl1_α hm) k  None  hm_impl1_invar hm);
      v  mop_list_get ml k;
      RETURN v
    }"
    lemma hm_the_lookup_op'_refine: 
      "(hm_the_lookup_op', hm_the_lookup_op)  hm_impl1_rel  nat_rel  Idnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_the_lookup_op'_def hm_the_lookup_op_def
      apply refine_vcg
      apply (auto simp: hm_impl1_rel_defs heapmap_α_def hmr_invar_def split: if_split_asm)
      done

    sepref_definition hm_the_lookup_op_impl is "uncurry hm_the_lookup_op'" :: "hm_impl2_relk*aid_assnk aid_assn"  
      unfolding hm_the_lookup_op'_def[abs_def] hm_impl2_rel_def
      by sepref
    lemmas hm_the_lookup_op_impl[sepref_fr_rules] = hm_the_lookup_op_impl.refine[FCOMP hm_the_lookup_op'_refine]
    sepref_register "hm_the_lookup_op::(nat,'v) ahm  _"

    sepref_definition hm_val_of_op_impl is "uncurry hm_val_of_op" :: "hm_impl_relk*aid_assnk a id_assn"
      unfolding hm_val_of_op_def by sepref
    lemmas [sepref_fr_rules] = hm_val_of_op_impl.refine
    sepref_register "hm_val_of_op::(nat,'v) ahm  _"

    sepref_definition hm_prio_of_op_impl is "uncurry (PR_CONST hm_prio_of_op)" :: "hm_impl_relk*aid_assnk a id_assn"
      unfolding hm_prio_of_op_def[abs_def] PR_CONST_def by sepref
    lemmas [sepref_fr_rules] = hm_prio_of_op_impl.refine
    sepref_register "PR_CONST hm_prio_of_op::(nat,'v) ahm  _"
    lemma [def_pat_rules]: "hmstruct.hm_prio_of_op$prio  PR_CONST hm_prio_of_op"
      by simp

    text ‹No code theorem preparation, as we define optimized version later›  
    sepref_definition (no_prep_code) hm_swim_op_impl is "uncurry (PR_CONST hm_swim_op)" :: "hm_impl_reld*anat_assnk a hm_impl_rel"
      unfolding hm_swim_op_def[abs_def] PR_CONST_def
      using [[goals_limit = 1]]
      by sepref
    lemmas [sepref_fr_rules] = hm_swim_op_impl.refine
    sepref_register "PR_CONST hm_swim_op::(nat,'v) ahm  _"
    lemma [def_pat_rules]: "hmstruct.hm_swim_op$prio  PR_CONST hm_swim_op" by simp

    text ‹No code theorem preparation, as we define optimized version later›  
    sepref_definition (no_prep_code) hm_sink_op_impl is "uncurry (PR_CONST hm_sink_op)" :: "hm_impl_reld*anat_assnk a hm_impl_rel"
      unfolding hm_sink_op_def[abs_def] PR_CONST_def
      by sepref
    lemmas [sepref_fr_rules] = hm_sink_op_impl.refine
    sepref_register "PR_CONST hm_sink_op::(nat,'v) ahm  _"
    lemma [def_pat_rules]: "hmstruct.hm_sink_op$prio  PR_CONST hm_sink_op" by simp

    sepref_definition hm_repair_op_impl is "uncurry (PR_CONST hm_repair_op)" :: "hm_impl_reld*anat_assnk a hm_impl_rel"
      unfolding hm_repair_op_def[abs_def] PR_CONST_def
      by sepref
    lemmas [sepref_fr_rules] = hm_repair_op_impl.refine
    sepref_register "PR_CONST hm_repair_op::(nat,'v) ahm  _"
    lemma [def_pat_rules]: "hmstruct.hm_repair_op$prio  PR_CONST hm_repair_op" by simp

  subsection ‹Interface Operations›
  definition hm_rel_np where 
    "hm_rel_np  hr_comp hm_impl_rel heapmap_rel"
  lemmas [fcomp_norm_unfold] = hm_rel_np_def[symmetric]  

  definition hm_rel where
    "hm_rel K V  hr_comp hm_rel_np (the_pure K,the_pure Vmap_rel)"
  lemmas [fcomp_norm_unfold] = hm_rel_def[symmetric]  

  lemmas [intf_of_assn] = intf_of_assnI[where R="hm_rel K V" and 'a="('kk,'vv) i_map" for K V]

  lemma hm_rel_id_conv: "hm_rel id_assn id_assn = hm_rel_np"
    ― ‹Used for generic algorithms: Unfold with this, then let decl-impl compose with map_rel› again.›
    unfolding hm_rel_def by simp


  subsubsection ‹Synthesis›
  definition op_hm_empty_sz :: "nat  'kk'vv"
    where [simp]: "op_hm_empty_sz sz  op_map_empty"
  sepref_register "PR_CONST (op_hm_empty_sz maxsize)" :: "('k,'v) i_map"
  lemma [def_pat_rules]: "op_hm_empty_sz$maxsize  UNPROTECT (op_hm_empty_sz maxsize)" by simp

  lemma hm_fold_custom_empty_sz: 
    "op_map_empty = op_hm_empty_sz sz"
    "Map.empty = op_hm_empty_sz sz"
    by auto

  sepref_definition hm_empty_op_impl is "uncurry0 hm_empty_op'" :: "unit_assnk a hm_impl2_rel"  
    unfolding hm_empty_op'_def hm_impl2_rel_def array.fold_custom_empty
    by sepref
    
  sepref_definition hm_insert_op_impl is "uncurry2 hm_insert_op" :: "[λ((k,_),_). k<maxsize]a id_assnk*aid_assnk*ahm_impl_reld  hm_impl_rel"
    unfolding hm_insert_op_def
    by sepref

  sepref_definition hm_is_empty_op_impl is "hm_is_empty_op" :: "hm_impl_relk a bool_assn"
    unfolding hm_is_empty_op_def
    by sepref

  sepref_definition hm_lookup_op_impl is "uncurry hm_lookup_op" :: "id_assnk*ahm_impl_relk a option_assn id_assn"
    unfolding hm_lookup_op_def by sepref

  sepref_definition hm_contains_key_impl is "uncurry hm_contains_key_op'" :: "id_assnk*ahm_impl2_relk a bool_assn"
    unfolding hm_contains_key_op'_def hm_impl2_rel_def
    by sepref

  sepref_definition hm_decrease_key_op_impl is "uncurry2 hm_decrease_key_op" :: "id_assnk*aid_assnk*ahm_impl_reld a hm_impl_rel"
    unfolding hm_decrease_key_op_def by sepref

  sepref_definition hm_increase_key_op_impl is "uncurry2 hm_increase_key_op" :: "id_assnk*aid_assnk*ahm_impl_reld a hm_impl_rel"
    unfolding hm_increase_key_op_def by sepref

  sepref_definition hm_change_key_op_impl is "uncurry2 hm_change_key_op" :: "id_assnk*aid_assnk*ahm_impl_reld a hm_impl_rel"
    unfolding hm_change_key_op_def by sepref

  sepref_definition hm_pop_min_op_impl is hm_pop_min_op :: "hm_impl_reld a prod_assn (prod_assn nat_assn id_assn) hm_impl_rel "
    unfolding hm_pop_min_op_def[abs_def]
    by sepref

  sepref_definition hm_remove_op_impl is "uncurry hm_remove_op" :: "id_assnk *a hm_impl_reld a hm_impl_rel"
    unfolding hm_remove_op_def[abs_def] by sepref

  sepref_definition hm_peek_min_op_impl is "hm_peek_min_op" :: "hm_impl_relk a prod_assn nat_assn id_assn"
    unfolding hm_peek_min_op_def[abs_def] hm_kv_of_op_def
    by sepref



  subsubsection ‹Setup of Refinements›

  sepref_decl_impl (no_register) hm_empty: 
    hm_empty_op_impl.refine[FCOMP hm_empty_op'_refine, FCOMP hm_empty_aref] .

  context fixes K assumes "IS_BELOW_ID K" begin
    lemmas mop_map_update_new_fref' = mop_map_update_new.fref[of K] 
    lemmas op_map_update_fref' = op_map_update.fref[of K] 
  end  

  sepref_decl_impl (ismop) hm_insert: hm_insert_op_impl.refine[FCOMP hm_insert_op_aref]
    uses mop_map_update_new_fref'
    unfolding IS_BELOW_ID_def
    apply (parametricity; auto simp: single_valued_below_Id)
    done

  sepref_decl_impl hm_is_empty: hm_is_empty_op_impl.refine[FCOMP hm_is_empty_op_aref] .
  sepref_decl_impl hm_lookup: hm_lookup_op_impl.refine[FCOMP hm_lookup_op_aref] .

  sepref_decl_impl hm_contains_key: 
    hm_contains_key_impl.refine[FCOMP hm_contains_key_op'_refine, FCOMP hm_contains_key_op_aref]
    .

  sepref_decl_impl (ismop) hm_decrease_key: hm_decrease_key_op_impl.refine[FCOMP hm_decrease_key_op_aref] .
  sepref_decl_impl (ismop) hm_increase_key: hm_increase_key_op_impl.refine[FCOMP hm_increase_key_op_aref] .
  sepref_decl_impl (ismop) hm_change_key: hm_change_key_op_impl.refine[FCOMP hm_change_key_op_aref] .
    
  sepref_decl_impl (ismop) hm_remove: hm_remove_op_impl.refine[FCOMP hm_remove_op_aref] .

  sepref_decl_impl (ismop) hm_pop_min: hm_pop_min_op_impl.refine[FCOMP hm_pop_min_op_aref] .
  sepref_decl_impl (ismop) hm_peek_min: hm_peek_min_op_impl.refine[FCOMP hm_peek_min_op_aref] .

  ― ‹Realized as generic algorithm. Note that we use @{term id_assn} for the elements.›
  sepref_definition hm_upd_op_impl is "uncurry2 (RETURN ooo op_map_update)" :: "[λ((k,_),_). k<maxsize]a id_assnk *a id_assnk *a (hm_rel id_assn id_assn)d  hm_rel id_assn id_assn"
    unfolding op_pm_set_gen_impl by sepref

  sepref_decl_impl hm_upd_op_impl.refine[unfolded hm_rel_id_conv] uses op_map_update_fref'
    unfolding IS_BELOW_ID_def
    apply (parametricity; auto simp: single_valued_below_Id)
    done

end  
end

interpretation hm: map_custom_empty "PR_CONST (op_hm_empty_sz maxsize)"
  apply unfold_locales by simp

lemma op_hm_empty_sz_hnr[sepref_fr_rules]:
  "(uncurry0 (hm_empty_op_impl maxsize), uncurry0 (RETURN (PR_CONST (op_hm_empty_sz maxsize))))  unit_assnk a hm_rel maxsize prio K V"
  using hm_empty_hnr by simp


subsection ‹Manual fine-tuning of code-lemmas›
(* TODO: Integrate into Sepref-tool optimization phase! *)

context
notes [simp del] = CNV_def efficient_nat_div2
begin

lemma nested_case_bind: 
  "(case p of (a,b)  bind (case a of (a1,a2)  m a b a1 a2) (f a b)) 
  = (case p of ((a1,a2),b)  bind (m (a1,a2) b a1 a2) (f (a1,a2) b))"
  "(case p of (a,b)  bind (case b of (b1,b2)  m a b b1 b2) (f a b)) 
  = (case p of (a,b1,b2)  bind (m a (b1,b2) b1 b2) (f a (b1,b2)))"
  by (simp_all split: prod.splits)

lemma it_case: "(case p of (a,b)  f p a b) = (case p of (a,b)  f (a,b) a b)"
  by (auto split: prod.split)

lemma c2l: "(case p of (a,b)  bind (m a b) (f a b)) = 
  do { let (a,b) = p; bind (m a b) (f a b)}" by simp

lemma bind_Let: "do { x  do { let y = v; (f y :: 'a Heap)}; g x } = do { let y=v; x  f y; g x }" by auto
lemma bind_case: "do { x  (case y of (a,b)  f a b); (g x :: 'a Heap) } = do { let (a,b) = y; x  f a b; g x }"
  by (auto split: prod.splits)

lemma bind_case_mvup: "do { x  f; case y of (a,b)  g a b x } 
  = do { let (a,b) = y; x  f; (g a b x :: 'a Heap) }"
  by (auto split: prod.splits)

lemma if_case_mvup: "(if b then case p of (x1,x2)  f x1 x2 else e)
  = (case p of (x1,x2)  if b then f x1 x2 else e)" by auto

lemma nested_case: "(case p of (a,b)  (case p of (c,d)  f a b c d)) =
  (case p of (a,b)  f a b a b)"
  by (auto split: prod.split)

lemma split_prod_bound: "(λp. f p) = (λ(a,b). f (a,b))" by auto

lemma bpc_conv: "do { (a,b)  (m::(_*_) Heap); f a b } = do {
  ab  (m);
  f (fst ab) (snd ab)
}" 
  apply (subst (2) split_prod_bound)
  by simp

lemma it_case_pp: "(case p of ((p1,p2))  case p of ((p1',p2'))  f p1 p2 p1' p2')
  = (case p of ((p1,p2))  f p1 p2 p1 p2)"
  by (auto split: prod.split)


lemma it_case_ppp: "(case p of ((p1,p2),p3)  case p of ((p1',p2'),p3')  f p1 p2 p3 p1' p2' p3')
  = (case p of ((p1,p2),p3)  f p1 p2 p3 p1 p2 p3)"
  by (auto split: prod.split)

lemma it_case_pppp: "(case a1 of
              (((a, b), c), d) 
                case a1 of
                (((a', b'), c'), d')  f a b c d a' b' c' d') =
       (case a1 of
              (((a, b), c), d)  f a b c d a b c d)"
  by (auto split: prod.splits)

private lemmas inlines = hm_append_op_impl_def ial_append_def
    marl_length_def marl_append_def hm_length_impl_def ial_length_def
    hm_valid_impl_def hm_prio_of_op_impl_def hm_val_of_op_impl_def hm_key_of_op_impl_def
    ial_get_def hm_the_lookup_op_impl_def heap_array_set_def marl_get_def
    it_case_ppp it_case_pppp bind_case bind_case_mvup nested_case if_case_mvup
    it_case_pp

schematic_goal [code]: "hm_insert_op_impl maxsize prio hm k v = ?f"
  unfolding hm_insert_op_impl_def
  apply (rule CNV_eqD)
  apply (simp add: inlines  cong: if_cong)
  by (rule CNV_I)
  

schematic_goal "hm_swim_op_impl prio hm i  ?f"
  unfolding hm_swim_op_impl_def 
  apply (rule eq_reflection)
  apply (rule CNV_eqD)
  apply (simp add: inlines efficient_nat_div2  
    cong: if_cong)
  by (rule CNV_I)


lemma hm_swim_op_impl_code[code]: "hm_swim_op_impl prio hm i  ccpo.fixp (fun_lub Heap_lub) (fun_ord Heap_ord)
       (λcf (a1, a2).
           case a1 of
           ((a1b, a2b), a2a) 
             case a1b of
             (a, b)  do {
               let d2 = efficient_nat_div2 a2; 
               if 0 < d2  d2  b
               then do {
                      x  (case a1b of (a, n)  Array.nth a) (d2 - Suc 0);
                      x  Array.nth a2a x;
                      xa  (case a1b of (a, n)  Array.nth a) (a2 - Suc 0);
                      xa  Array.nth a2a xa;
                      if prio x  prio xa then return a1
                      else do {
                             x'g  hm_exch_op_impl a1 a2 (d2);
                             cf (x'g, d2)
                           }
                    }
               else return a1
             })
       (hm, i)"
  unfolding hm_swim_op_impl_def 
  apply (rule eq_reflection)
  apply (simp add: inlines efficient_nat_div2 Let_def 
    cong: if_cong)
  done

prepare_code_thms hm_swim_op_impl_code

schematic_goal hm_sink_opt_impl_code[code]: "hm_sink_op_impl prio hm i  ?f"
  unfolding hm_sink_op_impl_def 
  apply (rule eq_reflection)
  apply (rule CNV_eqD)
  apply (simp add: inlines 
    cong: if_cong)
  by (rule CNV_I)

prepare_code_thms hm_sink_opt_impl_code

export_code hm_swim_op_impl in SML_imp module_name Test


schematic_goal hm_change_key_opt_impl_code[code]: "
  hm_change_key_op_impl prio k v hm  ?f"
  unfolding hm_change_key_op_impl_def 
  apply (rule eq_reflection)
  apply (rule CNV_eqD)
  apply (simp add: inlines hm_contains_key_impl_def ial_contains_def
    hm_change_key_op_impl_def hm_index_op_impl_def hm_update_op_impl_def
    ial_index_def
    cong: if_cong split: prod.splits)
  oops


schematic_goal hm_change_key_opt_impl_code[code]: "
  hm_change_key_op_impl prio k v hm  case hm of (((a, b), ba), x2) 
       (do {
              x  Array.nth ba k;
              xa  Array.nth a x;
              xa  Array.upd xa v x2;
              hm_repair_op_impl prio (((a, b), ba), xa) (Suc x)
            })"
  unfolding hm_change_key_op_impl_def 
  apply (rule eq_reflection)
  apply (simp add: inlines hm_contains_key_impl_def ial_contains_def
    hm_change_key_op_impl_def hm_index_op_impl_def hm_update_op_impl_def
    ial_index_def
    cong: if_cong split: prod.splits)
  done


schematic_goal hm_set_opt_impl_code[code]: "hm_upd_op_impl maxsize prio hm k v  ?f"
  unfolding hm_upd_op_impl_def 
  apply (rule eq_reflection)
  apply (rule CNV_eqD)
  apply (simp add: inlines hm_contains_key_impl_def ial_contains_def
    hm_change_key_op_impl_def hm_index_op_impl_def hm_update_op_impl_def
    ial_index_def
    cong: if_cong)
  by (rule CNV_I)

schematic_goal hm_pop_min_opt_impl_code[code]: "hm_pop_min_op_impl prio hm  ?f"
  unfolding hm_pop_min_op_impl_def 
  apply (rule eq_reflection)
  apply (rule CNV_eqD)
  apply (simp add: inlines hm_contains_key_impl_def ial_contains_def
    hm_change_key_op_impl_def hm_index_op_impl_def hm_update_op_impl_def
    hm_butlast_op_impl_def ial_butlast_def
    ial_index_def
    cong: if_cong)
  by (rule CNV_I)
  
end

export_code 
  hm_empty_op_impl 
  hm_insert_op_impl
  hm_is_empty_op_impl
  hm_lookup_op_impl
  hm_contains_key_impl
  hm_decrease_key_op_impl
  hm_increase_key_op_impl
  hm_change_key_op_impl
  hm_upd_op_impl
  hm_pop_min_op_impl
  hm_remove_op_impl
  hm_peek_min_op_impl
  checking SML_imp


end