Theory IICF_Abs_Heapmap

section Priority Maps implemented with List and Map
theory IICF_Abs_Heapmap
imports IICF_Abs_Heap "HOL-Library.Rewrite" "../../Intf/IICF_Prio_Map"
begin

  type_synonym ('k,'v) ahm = "'k list × ('k  'v)"

  subsection Basic Setup

  text First, we define a mapping to list-based heaps
  definition hmr_α :: "('k,'v) ahm  'v heap" where
    "hmr_α  λ(pq,m). map (the o m) pq"

  definition "hmr_invar  λ(pq,m). distinct pq  dom m  set pq"

  definition "hmr_rel  br hmr_α hmr_invar"

  lemmas hmr_rel_defs = hmr_rel_def hmr_α_def hmr_invar_def

  lemma hmr_empty_invar[simp]: "hmr_invar ([],Map.empty)"
    by (auto simp: hmr_invar_def)


  locale hmstruct = h: heapstruct prio for prio :: "'v  'b::linorder"
  begin

    text Next, we define a mapping to priority maps.

    definition heapmap_α :: "('k,'v) ahm  ('k  'v)" where
      "heapmap_α  λ(pq,m). m |` set pq"

    definition heapmap_invar :: "('k,'v) ahm  bool" where
      "heapmap_invar  λhm. hmr_invar hm  h.heap_invar (hmr_α hm)"
      
    definition "heapmap_rel  br heapmap_α heapmap_invar"

    lemmas heapmap_rel_defs = heapmap_rel_def br_def heapmap_α_def heapmap_invar_def

    lemma [refine_dref_RELATES]: "RELATES hmr_rel" by (simp add: RELATES_def)


    lemma h_heap_invarI[simp]: "heapmap_invar hm  h.heap_invar (hmr_α hm)"  
      by (simp add: heapmap_invar_def)

    lemma hmr_invarI[simp]: "heapmap_invar hm  hmr_invar hm"  
      unfolding heapmap_invar_def by blast



    lemma set_hmr_α[simp]: "hmr_invar hm  set (hmr_α hm) = ran (heapmap_α hm)"
      apply (clarsimp simp: hmr_α_def hmr_invar_def heapmap_α_def)
      by (smt Int_absorb1 comp_apply dom_restrict image_cong ran_is_image restrict_in)
      
    lemma in_h_hmr_α_conv[simp]: "hmr_invar hm  x ∈# h.α (hmr_α hm)  x  ran (heapmap_α hm)"  
      apply (clarsimp simp: hmr_α_def hmr_invar_def heapmap_α_def in_multiset_in_set ran_is_image)
      by (smt Int_absorb1 comp_apply image_cong restrict_in)

    subsection Basic Operations
    (* length, val_of_op, update, butlast, append, empty *)

    text In this section, we define the basic operations on heapmaps, 
      and their relations to heaps and maps.

    subsubsection Length
    text Length of the list that represents the heap
    definition hm_length :: "('k,'v) ahm  nat" where
      "hm_length  λ(pq,_). length pq"

    lemma hm_length_refine: "(hm_length, length)  hmr_rel  nat_rel"  
      apply (intro fun_relI)
      unfolding hm_length_def
      by (auto simp: hmr_rel_defs in_br_conv)
        
    lemma hm_length_hmr_α[simp]: "length (hmr_α hm) = hm_length hm"
      by (auto simp: hm_length_def hmr_α_def split: prod.splits)

    lemmas [refine] = hm_length_refine[param_fo]

    subsubsection Valid
    text Check whether index is valid
    definition "hm_valid hm i  i>0  i hm_length hm"

    lemma hm_valid_refine: "(hm_valid,h.valid)hmr_rel  nat_rel  bool_rel"
      apply (intro fun_relI)
      unfolding hm_valid_def h.valid_def
      by (parametricity add: hm_length_refine)

    lemma hm_valid_hmr_α[simp]: "h.valid (hmr_α hm) = hm_valid hm"
      by (intro ext) (auto simp: h.valid_def hm_valid_def)

    subsubsection Has-Child  
    definition "hm_has_child_op hm k  2*k  hm_length hm"
    definition "hm_left_child_op (k::nat)  2*k"   
    definition "hm_next_child_op (k::nat)  k+1"   
    definition "hm_has_next_child_op hm k  k+1  hm_length hm"   
    
    
    subsubsection Key-Of
    definition hm_key_of :: "('k,'v) ahm  nat  'k" where  
      "hm_key_of  λ(pq,m) i. pq!(i - 1)"

    definition hm_key_of_op :: "('k,'v) ahm  nat  'k nres" where
      "hm_key_of_op  λ(pq,m) i. doN {ASSERT (i>0); mop_list_get pq (i - 1)}"

    lemma hm_key_of_op_unfold:
      shows "hm_key_of_op hm i = doN {ASSERT (hm_valid hm i); RETURN (hm_key_of hm i)}"
      unfolding hm_valid_def hm_length_def hm_key_of_op_def hm_key_of_def
      by (auto split: prod.splits simp: pw_eq_iff refine_pw_simps)

    lemma val_of_hmr_α[simp]: "hm_valid hm i  h.val_of (hmr_α hm) i 
      = the (heapmap_α hm (hm_key_of hm i))"
      by (auto 
        simp: hmr_α_def h.val_of_def heapmap_α_def hm_key_of_def hm_valid_def hm_length_def
        split: prod.splits)
 
    lemma hm_α_key_ex[simp]:
      "hmr_invar hm; hm_valid hm i  (heapmap_α hm (hm_key_of hm i)  None)"
      unfolding heapmap_invar_def hmr_invar_def hm_valid_def heapmap_α_def 
        hm_key_of_def hm_length_def
      apply (clarsimp split: prod.splits)  
      by (meson domD in_set_conv_nth nz_le_conv_less subset_code(1))

    subsubsection Lookup
    abbreviation (input) hm_lookup where "hm_lookup  heapmap_α"

    definition "hm_the_lookup_op k hm  doN {
      ASSERT (heapmap_α hm k  None  hmr_invar hm);
      RETURN (the (heapmap_α hm k))}"

    (*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_map_lookup ml k;
      RETURN v
    }"
      
    lemma hm_the_lookup_op'_refine: 
      "(hm_the_lookup_op', hm_the_lookup_op) ∈ hmr_rel → nat_rel → ⟨Id⟩nres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_the_lookup_op'_def hm_the_lookup_op_def
      apply refine_vcg
      apply (auto)
      apply (auto simp: hm_impl1_rel_defs heapmap_α_def hmr_invar_def split: if_split_asm)
      done
    *)

    subsubsection Exchange  
    text Exchange two indices

    definition "hm_exch_op  λ(pq,m) i j. do {
      ASSERT (hm_valid (pq,m) i);
      ASSERT (hm_valid (pq,m) j);
      ASSERT (hmr_invar (pq,m));
      pq  mop_list_swap pq (i - 1) (j - 1);
      RETURN (pq,m)
    }"

    lemma hm_exch_op_invar: "hm_exch_op hm i j n SPEC hmr_invar"
      unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
      apply simp
      apply refine_vcg
      apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs)
      done

    lemma hm_exch_op_refine: "(hm_exch_op,h.exch_op)  hmr_rel  nat_rel  nat_rel  hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
      apply simp
      apply refine_vcg
      apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs in_br_conv)
      done
      
    lemmas hm_exch_op_refine'[refine] = hm_exch_op_refine[param_fo, THEN nres_relD]

    definition hm_exch :: "('k,'v) ahm  nat  nat  ('k,'v) ahm"
      where "hm_exch  λ(pq,m) i j. (swap pq (i-1) (j-1),m)"

      
    lemma hm_exch_op_α_correct: "hm_exch_op hm i j n SPEC (λhm'. 
      hm_valid hm i  hm_valid hm j  hm'=hm_exch hm i j
      )"
      unfolding hm_exch_op_def
      apply refine_vcg
      apply (auto simp add: hm_key_of_def hm_exch_def swap_def)
      done

    lemma hm_exch_α[simp]: "hm_valid hm i; hm_valid hm j 
       heapmap_α (hm_exch hm i j) = (heapmap_α hm)"
      by (auto simp: heapmap_α_def hm_exch_def hm_valid_def hm_length_def split: prod.splits)
      
    lemma hm_exch_valid[simp]: "hm_valid (hm_exch hm i j) = hm_valid hm"
      by (intro ext) (auto simp: hm_valid_def hm_length_def hm_exch_def split: prod.splits)
    lemma hm_exch_length[simp]: "hm_length (hm_exch hm i j) = hm_length hm"
      by (auto simp: hm_length_def hm_exch_def split: prod.splits)

    lemma hm_exch_same[simp]: "hm_exch hm i i = hm"  
      by (auto simp: hm_exch_def split: prod.splits)
      

    lemma hm_key_of_exch_conv[simp]:   
      "hm_valid hm i; hm_valid hm j; hm_valid hm k  
        hm_key_of (hm_exch hm i j) k = (
          if k=i then hm_key_of hm j
          else if k=j then hm_key_of hm i
          else hm_key_of hm k
          )"
      unfolding hm_exch_def hm_valid_def hm_length_def hm_key_of_def
      by (auto split: prod.splits simp: swap_nth)

    lemma hm_key_of_exch_matching[simp]:  
      "hm_valid hm i; hm_valid hm j  hm_key_of (hm_exch hm i j) i = hm_key_of hm j"
      "hm_valid hm i; hm_valid hm j  hm_key_of (hm_exch hm i j) j = hm_key_of hm i"
      by simp_all

    subsubsection Index
    text Obtaining the index of a key
    definition "hm_index  λ(pq,m) k. index pq k + 1"

    lemma hm_index_valid[simp]: "hmr_invar hm; heapmap_α hm k  None  hm_valid hm (hm_index hm k)"
      by (auto 
        simp: hm_valid_def heapmap_α_def hmr_invar_def hm_index_def hm_length_def Suc_le_eq
        simp: restrict_map_def split: if_splits)

    lemma hm_index_key_of[simp]: "hmr_invar hm; heapmap_α hm k  None  hm_key_of hm (hm_index hm k) = k"
      by (auto 
        simp: hm_valid_def heapmap_α_def hmr_invar_def hm_index_def hm_length_def hm_key_of_def Suc_le_eq
        simp: restrict_map_def split: if_splits)


    definition "hm_index_op  λ(pq,m) k. 
      do {
        ASSERT (hmr_invar (pq,m)  heapmap_α (pq,m) k  None);
        i  mop_list_index pq k;
        RETURN (i+1)
      }"

    lemma hm_index_op_correct:
      assumes "hmr_invar hm"
      assumes "heapmap_α hm k  None"
      shows "hm_index_op hm k  SPEC (λr. r= hm_index hm k)"
      using assms unfolding hm_index_op_def
      apply refine_vcg
      apply (auto simp: heapmap_α_def hmr_invar_def hm_index_def index_nth_id)
      done
    lemmas [refine_vcg] = hm_index_op_correct  
      

    subsubsection Update  
    text Updating the heap at an index
    definition hm_update_op :: "('k,'v) ahm  nat  'v  ('k,'v) ahm nres" where
      "hm_update_op  λ(pq,m) i v. do {
        ASSERT (hm_valid (pq,m) i  hmr_invar (pq,m));
        k  mop_list_get pq (i - 1);
        RETURN (pq, m(k  v))
      }"
    
    lemma hm_update_op_invar: "hm_update_op hm k v n SPEC hmr_invar"
      unfolding hm_update_op_def h.update_op_def
      apply refine_vcg
      by (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def)

    lemma hm_update_op_refine: "(hm_update_op, h.update_op)  hmr_rel  nat_rel  Id  hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_update_op_def h.update_op_def mop_list_get_alt mop_list_set_alt
      apply refine_vcg
      apply (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def in_br_conv)
      done
      
    lemmas [refine] = hm_update_op_refine[param_fo, THEN nres_relD]

    lemma hm_update_op_α_correct:
      assumes "hmr_invar hm"
      assumes "heapmap_α hm k  None"
      shows "hm_update_op hm (hm_index hm k) v n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(kv))"  
      using assms
      unfolding hm_update_op_def
      apply refine_vcg
      apply (auto simp: heapmap_rel_defs hmr_rel_defs hm_index_def restrict_map_def split: if_splits)
      done

    subsubsection Butlast  
    text Remove last element  
    definition hm_butlast_op :: "('k,'v) ahm  ('k,'v) ahm nres" where
      "hm_butlast_op  λ(pq,m). do {
        ASSERT (hmr_invar (pq,m));
        ASSERT (pq[]);
        k  mop_list_get pq (length pq - 1);
        pq  mop_list_butlast pq;
        RETURN (pq,m)
      }"

    lemma hm_butlast_op_refine: "(hm_butlast_op, h.butlast_op)  hmr_rel  hmr_relnres_rel"
      supply [simp del] = map_upd_eq_restrict
      apply (intro fun_relI nres_relI)
      unfolding hm_butlast_op_def h.butlast_op_def
      apply simp
      apply refine_vcg
      apply (clarsimp_all simp: hmr_rel_defs map_butlast distinct_butlast in_br_conv)
      apply (auto simp: neq_Nil_rev_conv) []
      done

    lemmas [refine] = hm_butlast_op_refine[param_fo, THEN nres_relD]

    lemma hm_butlast_op_α_correct: "hm_butlast_op hm n SPEC (
      λhm'. heapmap_α hm' = (heapmap_α hm)( hm_key_of hm (hm_length hm) := None ))"
    proof -
      have AUX: "xs[] 
         set (butlast xs) = (if xs!(length xs - 1)  set (butlast xs) then set xs else set xs - {xs!(length xs - 1)})"
        for xs :: "'a list"
        apply (cases xs rule: rev_cases)
        apply auto
        done
        
      have AUX: " distinct xs; xs[]   set (butlast xs) = set xs - {xs!(length xs - 1)}"
        for xs :: "'a list"
        apply (cases xs rule: rev_cases)
        by auto
        
      show ?thesis
        unfolding hm_butlast_op_def
        apply refine_vcg
        by (auto simp: heapmap_α_def hm_key_of_def hm_length_def hmr_invar_def AUX)
    qed
    
    subsubsection Append
    text Append new element at end of heap

    definition hm_append_op :: "('k,'v) ahm  'k  'v  ('k,'v) ahm nres"
      where "hm_append_op  λ(pq,m) k v. do {
        ASSERT (k  set pq);
        ASSERT (hmr_invar (pq,m));
        pq  mop_list_append pq k;
        let m = m (k  v);
        RETURN (pq,m)
      }"

    lemma hm_append_op_invar: "hm_append_op hm k v n SPEC hmr_invar"  
      unfolding hm_append_op_def h.append_op_def
      apply refine_vcg
      unfolding heapmap_α_def hmr_rel_defs
      apply (auto simp: )
      done

    lemma hm_append_op_refine: " heapmap_α hm k = None; (hm,h)hmr_rel  
       (hm_append_op hm k v, h.append_op h v)  hmr_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_append_op_def h.append_op_def
      apply refine_vcg
      unfolding heapmap_α_def hmr_rel_defs
      apply (auto simp: in_br_conv)
      done

    lemmas hm_append_op_refine'[refine] = hm_append_op_refine[param_fo, THEN nres_relD]
    
    lemma hm_append_op_α_correct: 
      "hm_append_op hm k v n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm) (k  v))"
      unfolding hm_append_op_def
      apply refine_vcg
      by (auto simp: heapmap_α_def)


    subsection Auxiliary Operations  
    text Auxiliary operations on heapmaps, which are derived 
      from the basic operations, but do not correspond to 
      operations of the priority map interface
    

    text We start with some setup

    lemma heapmap_hmr_relI: "(hm,h)heapmap_rel  (hm,hmr_α hm)  hmr_rel"  
      by (auto simp: heapmap_rel_defs hmr_rel_defs)

    lemma heapmap_hmr_relI': "heapmap_invar hm  (hm,hmr_α hm)  hmr_rel"  
      by (auto simp: heapmap_rel_defs hmr_rel_defs)

    text The basic principle how we prove correctness of our operations:
      Invariant preservation is shown by relating the operations to 
      operations on heaps. Then, only correctness on the abstraction 
      remains to be shown, assuming the operation does not fail.
        
    lemma heapmap_nres_relI':
      assumes "hm  hmr_rel h'"
      assumes "h'  SPEC (h.heap_invar)"
      assumes "hm n SPEC (λhm'. RETURN (heapmap_α hm')  h)"
      shows "hm  heapmap_rel h"
      using assms
      unfolding heapmap_rel_defs hmr_rel_def
      by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps)

    lemma heapmap_nres_relI'':
      assumes "hm  hmr_rel h'"
      assumes "h'  SPEC Φ"
      assumes "h'. Φ h'  h.heap_invar h'"
      assumes "hm n SPEC (λhm'. RETURN (heapmap_α hm')  h)"
      shows "hm  heapmap_rel h"
      apply (rule heapmap_nres_relI')
      apply fact
      apply (rule order_trans, fact)
      apply (clarsimp; fact)
      apply fact
      done

    subsubsection Val-of
    text Indexing into the heap
    definition hm_val_of_op :: "('k,'v) ahm  nat  'v nres" where
      "hm_val_of_op  λhm i. do {
        k  hm_key_of_op hm i;
        v  hm_the_lookup_op k hm;
        RETURN v
      }"

    lemma hm_val_of_op_refine: "(hm_val_of_op,h.val_of_op)  (hmr_rel  nat_rel  Idnres_rel)"  
      apply (intro fun_relI nres_relI)
      unfolding hm_val_of_op_def h.val_of_op_def 
        hm_key_of_op_def hm_key_of_def hm_valid_def hm_length_def
        hm_the_lookup_op_def
      apply clarsimp
      apply (rule refine_IdD)
      apply refine_vcg
      apply (auto simp: hmr_rel_defs in_br_conv heapmap_α_def)
      by (meson domD nth_mem subsetCE)

    lemmas [refine] = hm_val_of_op_refine[param_fo, THEN nres_relD]

    subsubsection Prio-of  
    text Priority of key
    definition "hm_prio_of_op h i  do {v  hm_val_of_op h i; RETURN (prio v)}"
    
    lemma hm_prio_of_op_refine: "(hm_prio_of_op, h.prio_of_op)  hmr_rel  nat_rel  Idnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_prio_of_op_def h.prio_of_op_def
      apply refine_rcg
      by auto

    lemmas hm_prio_of_op_refine'[refine] = hm_prio_of_op_refine[param_fo, THEN nres_relD]

    subsubsection Swim

    definition hm_swim_op :: "('k,'v) ahm  nat  ('k,'v) ahm nres" where
      "hm_swim_op h i  do {
        RECT (λswim (h,i). do {
          ASSERT (hm_valid h i  h.swim_invar (hmr_α h) i);
          if hm_valid h (h.parent i) then do {
            ppi  hm_prio_of_op h (h.parent i);
            pi  hm_prio_of_op h i;
            if (¬ppi  pi) then do {
              h  hm_exch_op h i (h.parent i);
              swim (h, h.parent i)
            } else
              RETURN h
          } else 
            RETURN h
        }) (h,i)
      }"

    lemma hm_swim_op_refine: "(hm_swim_op, h.swim_op)  hmr_rel  nat_rel  hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_swim_op_def h.swim_op_def
      apply refine_rcg
      apply refine_dref_type
      apply (clarsimp_all simp: hm_valid_refine[param_fo, THEN IdD])
      apply (simp add: hmr_rel_def in_br_conv)
      done

    lemmas hm_swim_op_refine'[refine] = hm_swim_op_refine[param_fo, THEN nres_relD]


    lemma hm_swim_op_nofail_imp_valid: 
      "nofail (hm_swim_op hm i)  hm_valid hm i  h.swim_invar (hmr_α hm) i"
      unfolding hm_swim_op_def
      apply (subst (asm) RECT_unfold, refine_mono)
      by (auto simp: refine_pw_simps)

    lemma hm_swim_op_α_correct: "hm_swim_op hm i n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
      apply (rule leof_add_nofailI)
      apply (drule hm_swim_op_nofail_imp_valid)
      unfolding hm_swim_op_def
      apply (rule RECT_rule_leof[where 
            pre="λ(hm',i). hm_valid hm' i  heapmap_α hm' = heapmap_α hm"
            and V = "inv_image less_than snd"
            ])
      apply simp
      apply simp

      unfolding hm_prio_of_op_def hm_val_of_op_def 
        hm_exch_op_def hm_key_of_op_def hm_the_lookup_op_def
      apply (refine_vcg)
      apply (clarsimp_all simp add: hm_valid_def hm_length_def)
      apply rprems
      apply (auto simp: heapmap_α_def h.parent_def)
      done

    subsubsection Sink  
    definition hm_sink_op
    where   
      "hm_sink_op h k  RECT (λD (h,k). do {
        ASSERT (k>0  khm_length h);
        if hm_has_child_op h k then do {
          let j = hm_left_child_op k;
          pj  hm_prio_of_op h j;

          j  (
            if hm_has_next_child_op h j then do {
              let j' = hm_next_child_op j;
              psj  hm_prio_of_op h j';
              if pj>psj then RETURN j' else RETURN j
            } else RETURN j);

          pj  hm_prio_of_op h j;
          pk  hm_prio_of_op h k;
          if (pk > pj) then do {
            h  hm_exch_op h k j;
            D (h,j)
          } else
            RETURN h
        } else RETURN h    
      }) (h,k)"
    
    lemma hm_sink_op_refine: "(hm_sink_op, h.sink_op)  hmr_rel  nat_rel  hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_sink_op_def h.sink_op_opt_eq[symmetric] h.sink_op_opt_def
      unfolding hm_has_child_op_def hm_has_next_child_op_def
        hm_left_child_op_def hm_next_child_op_def
      apply (rewrite at "let _ = length _ in _" Let_def)  
      apply (rewrite at "let _ = _ + 1 in _" Let_def)  
      apply refine_rcg
      apply refine_dref_type

      unfolding hmr_rel_def heapmap_rel_def 
      apply (auto simp: in_br_conv)
      done

    lemmas hm_sink_op_refine'[refine] = hm_sink_op_refine[param_fo, THEN nres_relD]

    lemma hm_sink_op_nofail_imp_valid: "nofail (hm_sink_op hm i)  hm_valid hm i"
      unfolding hm_sink_op_def
      apply (subst (asm) RECT_unfold, refine_mono)
      by (auto simp: refine_pw_simps hm_valid_def)
      
    lemma hm_sink_op_α_correct: "hm_sink_op hm i n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
      apply (rule leof_add_nofailI)
      apply (drule hm_sink_op_nofail_imp_valid)
      unfolding hm_sink_op_def 
      unfolding hm_left_child_op_def hm_has_child_op_def hm_has_next_child_op_def hm_next_child_op_def
      apply (rule RECT_rule_leof[where 
            pre="λ(hm',i). hm_valid hm' i  heapmap_α hm' = heapmap_α hm  hm_length hm' = hm_length hm"
            and V = "measure (λ(hm',i). hm_length hm' - i)"
            ])
      apply simp
      apply simp

      unfolding hm_prio_of_op_def hm_val_of_op_def hm_exch_op_def 
        hm_key_of_op_def hm_the_lookup_op_def
      apply (refine_vcg)
      apply (clarsimp_all simp add: hm_valid_def hm_length_def) (* Takes long *)
      apply rprems
      apply (clarsimp_all simp: heapmap_α_def h.parent_def split: prod.splits)
      apply (auto)
      done

    subsubsection Repair
    definition "hm_repair_op hm i  do {
      hm  hm_sink_op hm i;
      hm  hm_swim_op hm i;
      RETURN hm
    }"
    
    lemma hm_repair_op_refine: "(hm_repair_op, h.repair_op)  hmr_rel  nat_rel  hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_repair_op_def h.repair_op_def
      by refine_rcg
      
    lemmas hm_repair_op_refine'[refine] = hm_repair_op_refine[param_fo, THEN nres_relD]

    lemma hm_repair_op_α_correct: "hm_repair_op hm i n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
      unfolding hm_repair_op_def
      apply (refine_vcg 
        hm_swim_op_α_correct[THEN leof_trans] 
        hm_sink_op_α_correct[THEN leof_trans])
      by auto


    subsection Operations    
    text In this section, we define the operations that implement the priority-map interface

    subsubsection Empty
    definition hm_empty_op :: "('k,'v) ahm nres" 
      where "hm_empty_op  do { mmop_map_empty; RETURN ([],m) }"

    lemma hm_empty_op_aref: "(hm_empty_op,mop_map_empty)  heapmap_relnres_rel"  
      unfolding hm_empty_op_def 
      apply refine_vcg
      by (auto simp: heapmap_rel_defs hmr_rel_defs intro: nres_relI)

    subsubsection Insert
    definition hm_insert_op :: "'k  'v  ('k,'v) ahm  ('k,'v) ahm nres" where
      "hm_insert_op  λk v h. do {
        ASSERT (h.heap_invar (hmr_α h));
        h  hm_append_op h k v;
        let l = hm_length h;
        h  hm_swim_op h l;
        RETURN h
      }"
      
    lemma hm_insert_op_refine[refine]: " heapmap_α hm k = None; (hm,h)hmr_rel  
      hm_insert_op k v hm  hmr_rel (h.insert_op v h)"
      unfolding hm_insert_op_def h.insert_op_def
      apply refine_rcg
      by (auto simp: hmr_rel_def br_def)

    lemma hm_insert_op_aref: 
      "(hm_insert_op,mop_map_update_new)  Id  Id  heapmap_rel  heapmap_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding mop_map_update_new_alt
      apply (rule ASSERT_refine_right)
      apply (rule heapmap_nres_relI''[OF hm_insert_op_refine h.insert_op_correct])
      apply (unfold heapmap_rel_def in_br_conv; clarsimp)
      apply (erule heapmap_hmr_relI)
      apply (unfold heapmap_rel_def in_br_conv; clarsimp)
      apply (unfold heapmap_rel_def in_br_conv; clarsimp)
      unfolding hm_insert_op_def
      apply (refine_vcg 
        hm_append_op_α_correct[THEN leof_trans]
        hm_swim_op_α_correct[THEN leof_trans])
      apply (unfold heapmap_rel_def in_br_conv; clarsimp)
      done

    subsubsection Is-Empty  

    lemma hmr_α_empty_iff[simp]: 
      "hmr_invar hm  hmr_α hm = []  heapmap_α hm = Map.empty"  
      by (auto 
        simp: hmr_α_def heapmap_invar_def heapmap_α_def hmr_invar_def restrict_map_def fun_eq_iff
        split: prod.split if_splits)  

    definition hm_is_empty_op :: "('k,'v) ahm  bool nres" where
      "hm_is_empty_op  λhm. do {
        ASSERT (hmr_invar hm);
        let l = hm_length hm;
        RETURN (l=0)
      }"

    lemma hm_is_empty_op_refine: "(hm_is_empty_op, h.is_empty_op)  hmr_rel  bool_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_is_empty_op_def h.is_empty_op_def
      apply refine_rcg
      subgoal by (auto simp: hmr_rel_defs in_br_conv)
      subgoal by (parametricity add: hm_length_refine)
      done


    lemma hm_is_empty_op_aref: "(hm_is_empty_op, mop_map_is_empty)  heapmap_rel  bool_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_is_empty_op_def
      apply refine_vcg
      apply (auto simp: hmr_rel_defs in_br_conv heapmap_rel_defs hm_length_def)
      by (metis Int_absorb1 dom_restrict length_greater_0_conv ndomIff nth_mem)

    subsubsection Lookup  

    definition hm_lookup_op :: "'k  ('k,'v) ahm  'v option nres"
      where "hm_lookup_op  λk hm. doN {ASSERT (heapmap_invar hm); RETURN (hm_lookup hm k)}"

    lemma hm_lookup_op_aref: "(hm_lookup_op,RETURN oo op_map_lookup)  Id  heapmap_rel  Idoption_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_lookup_op_def heapmap_rel_def in_br_conv
      apply refine_vcg
      apply simp_all
      done

    lemma hm_the_lookup_op_aref: "(hm_the_lookup_op,mop_map_the_lookup)  Id  heapmap_rel  Idnres_rel"
      unfolding hm_the_lookup_op_def
      by (auto intro!: nres_relI simp: pw_eq_iff refine_pw_simps heapmap_rel_def in_br_conv)
      
    subsubsection Contains-Key  

    definition "hm_contains_key_op  λk (pq,m). doN {ASSERT (heapmap_invar (pq,m)); mop_list_contains k pq}"
    lemma hm_contains_key_op_aref: "(hm_contains_key_op,mop_map_contains_key)  Id  heapmap_rel  bool_relnres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding hm_contains_key_op_def heapmap_rel_defs
      apply refine_vcg
      by (auto simp: hmr_invar_def)

    subsubsection Decrease-Key  


    definition "hm_decrease_key_op  λk v hm. do {
      ASSERT (heapmap_invar hm);
      ASSERT (heapmap_α hm k  None  prio v  prio (the (heapmap_α hm k)));
      i  hm_index_op hm k;
      hm  hm_update_op hm i v;
      hm_swim_op hm i
    }"

    definition (in heapstruct) "decrease_key_op i v h  do {
      ASSERT (valid h i  prio v  prio_of h i);
      h  update_op h i v;
      swim_op h i
    }"

    lemma (in heapstruct) decrease_key_op_invar: 
      "heap_invar h; valid h i; prio v  prio_of h i  decrease_key_op i v h  SPEC heap_invar"
      unfolding decrease_key_op_def
      apply refine_vcg
      by (auto simp: swim_invar_decr)


    lemma index_op_inline_refine:
      assumes "heapmap_invar hm"
      assumes "heapmap_α hm k  None"
      assumes "f (hm_index hm k)  m"
      shows "do {i  hm_index_op hm k; f i}  m"  
      using hm_index_op_correct[of hm k] assms
      by (auto simp: pw_le_iff refine_pw_simps)

    lemma hm_decrease_key_op_refine: 
      "(hm,h)hmr_rel; (hm,m)heapmap_rel; m k = Some v' 
         hm_decrease_key_op k v hm hmr_rel (h.decrease_key_op (hm_index hm k) v h)"  
      unfolding hm_decrease_key_op_def h.decrease_key_op_def
      (*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
      apply (refine_rcg index_op_inline_refine)
      unfolding hmr_rel_def heapmap_rel_def in_br_conv
      apply (clarsimp_all)
      done

    lemma hm_index_op_inline_leof: 
      assumes "f (hm_index hm k) n m"
      shows "do {i  hm_index_op hm k; f i} n m"
      using hm_index_op_correct[of hm k] assms unfolding hm_index_op_def
      by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps split: prod.splits)

    lemma hm_decrease_key_op_α_correct: 
      "heapmap_invar hm  hm_decrease_key_op k v hm n SPEC (λhm'. heapmap_α hm' = heapmap_α hm(kv))"
      unfolding hm_decrease_key_op_def
      apply (refine_vcg 
        hm_update_op_α_correct[THEN leof_trans] 
        hm_swim_op_α_correct[THEN leof_trans]
        hm_index_op_inline_leof
        )
      apply simp_all
      done

    lemma hm_decrease_key_op_aref: 
      "(hm_decrease_key_op, PR_CONST (mop_pm_decrease_key prio))  Id  Id  heapmap_rel  heapmap_relnres_rel"
      unfolding PR_CONST_def
      apply (intro fun_relI nres_relI)
      apply (frule heapmap_hmr_relI)
      unfolding mop_pm_decrease_key_alt
      apply (rule ASSERT_refine_right; clarsimp)
      apply (rule heapmap_nres_relI')
      apply (rule hm_decrease_key_op_refine; assumption)
      unfolding heapmap_rel_def hmr_rel_def in_br_conv
      apply (rule h.decrease_key_op_invar; simp; fail )
      apply (refine_vcg hm_decrease_key_op_α_correct[THEN leof_trans]; simp; fail)
      done

    subsubsection Increase-Key  

    definition "hm_increase_key_op  λk v hm. do {
      ASSERT (heapmap_invar hm);
      ASSERT (heapmap_α hm k  None  prio v  prio (the (heapmap_α hm k)));
      i  hm_index_op hm k;
      hm  hm_update_op hm i v;
      hm_sink_op hm i
    }"

    definition (in heapstruct) "increase_key_op i v h  do {
      ASSERT (valid h i  prio v  prio_of h i);
      h  update_op h i v;
      sink_op h i
    }"

    lemma (in heapstruct) increase_key_op_invar: 
      "heap_invar h; valid h i; prio v  prio_of h i  increase_key_op i v h  SPEC heap_invar"
      unfolding increase_key_op_def
      apply refine_vcg
      by (auto simp: sink_invar_incr)

    lemma hm_increase_key_op_refine: 
      "(hm,h)hmr_rel; (hm,m)heapmap_rel; m k = Some v' 
         hm_increase_key_op k v hm hmr_rel (h.increase_key_op (hm_index hm k) v h)"  
      unfolding hm_increase_key_op_def h.increase_key_op_def
      (*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
      apply (refine_rcg index_op_inline_refine)
      unfolding hmr_rel_def heapmap_rel_def in_br_conv
      apply (clarsimp_all)
      done

    lemma hm_increase_key_op_α_correct: 
      "heapmap_invar hm  hm_increase_key_op k v hm n SPEC (λhm'. heapmap_α hm' = heapmap_α hm(kv))"
      unfolding hm_increase_key_op_def
      apply (refine_vcg 
        hm_update_op_α_correct[THEN leof_trans] 
        hm_sink_op_α_correct[THEN leof_trans]
        hm_index_op_inline_leof)
      apply simp_all
      done

    lemma hm_increase_key_op_aref: 
      "(hm_increase_key_op, PR_CONST (mop_pm_increase_key prio))  Id  Id  heapmap_rel  heapmap_relnres_rel"
      unfolding PR_CONST_def
      apply (intro fun_relI nres_relI)
      apply (frule heapmap_hmr_relI)
      unfolding mop_pm_increase_key_alt
      apply (rule ASSERT_refine_right; clarsimp)
      apply (rule heapmap_nres_relI')
      apply (rule hm_increase_key_op_refine; assumption)
      unfolding heapmap_rel_def hmr_rel_def in_br_conv
      apply (rule h.increase_key_op_invar; simp; fail )
      apply (refine_vcg hm_increase_key_op_α_correct[THEN leof_trans]; simp)
      done

    subsubsection Change-Key  

    definition "hm_change_key_op  λk v hm. do {
      ASSERT (heapmap_invar hm);
      ASSERT (heapmap_α hm k  None);
      i  hm_index_op hm k;
      hm  hm_update_op hm i v;
      hm_repair_op hm i
    }"

    definition (in heapstruct) "change_key_op i v h  do {
      ASSERT (valid h i);
      h  update_op h i v;
      repair_op h i
    }"

    lemma (in heapstruct) change_key_op_invar: 
      "heap_invar h; valid h i  change_key_op i v h  SPEC heap_invar"
      unfolding change_key_op_def
      apply (refine_vcg)
      apply hypsubst
      apply refine_vcg
      by (auto simp: sink_invar_incr)

    lemma hm_change_key_op_refine: 
      "(hm,h)hmr_rel; (hm,m)heapmap_rel; m k = Some v' 
         hm_change_key_op k v hm hmr_rel (h.change_key_op (hm_index hm k) v h)"  
      unfolding hm_change_key_op_def h.change_key_op_def
      (*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
      apply (refine_rcg index_op_inline_refine)
      unfolding hmr_rel_def heapmap_rel_def in_br_conv
      apply (clarsimp_all)
      done

    lemma hm_change_key_op_α_correct: 
      "heapmap_invar hm  hm_change_key_op k v hm n SPEC (λhm'. heapmap_α hm' = heapmap_α hm(kv))"
      unfolding hm_change_key_op_def
      apply (refine_vcg 
        hm_update_op_α_correct[THEN leof_trans] 
        hm_repair_op_α_correct[THEN leof_trans]
        hm_index_op_inline_leof)
      unfolding heapmap_rel_def in_br_conv
      apply simp
      apply simp
      done

    lemma hm_change_key_op_aref: 
      "(hm_change_key_op, mop_map_update_ex)  Id  Id  heapmap_rel  heapmap_relnres_rel"
      apply (intro fun_relI nres_relI)
      apply (frule heapmap_hmr_relI)
      unfolding mop_map_update_ex_alt
      apply (rule ASSERT_refine_right; clarsimp)
      apply (rule heapmap_nres_relI')
      apply (rule hm_change_key_op_refine; assumption)
      unfolding heapmap_rel_def hmr_rel_def in_br_conv
      apply (rule h.change_key_op_invar; simp; fail )
      apply ((refine_vcg hm_change_key_op_α_correct[THEN leof_trans]; simp))
      done

    subsubsection Set  

    text Realized as generic algorithm! (* TODO: Implement as such! *)
    lemma (in -) op_pm_set_gen_impl: "RETURN ooo op_map_update = (λk v m. do {
      c  RETURN (op_map_contains_key k m);
      if c then 
        mop_map_update_ex k v m
      else
        mop_map_update_new k v m
    })"
      apply (intro ext)
      unfolding op_map_contains_key_def mop_map_update_ex_def mop_map_update_new_def
      by simp

    definition "hm_set_op k v hm  do {
      c  hm_contains_key_op k hm;
      if c then
        hm_change_key_op k v hm
      else
        hm_insert_op k v hm
    }"

    (* TODO: Move. Near RETURN_to_SPEC_rule *)
    thm RETURN_to_SPEC_rule
    lemma SPEC_to_RETURN_rule: "m  RETURN x  m  SPEC ((=) x)"
      by (auto simp: pw_le_iff)
    
    lemma hm_set_op_aref: 
      "(hm_set_op, mop_map_update)  Id  Id  heapmap_rel  heapmap_relnres_rel"
      unfolding op_pm_set_gen_impl
      apply (intro fun_relI nres_relI)
      unfolding hm_set_op_def o_def
      using hm_contains_key_op_aref[param_fo]
      using hm_change_key_op_aref[param_fo]
      using hm_insert_op_aref[param_fo]
      by (fastforce simp: pw_le_iff pw_nres_rel_iff refine_pw_simps) (** Takes long *)
 
    subsubsection Pop-Min  

    definition hm_pop_min_op :: "('k,'v) ahm  (('k×'v) × ('k,'v) ahm) nres" where
      "hm_pop_min_op hm  do {
        ASSERT (heapmap_invar hm);
        ASSERT (hm_valid hm 1);
        k  hm_key_of_op hm 1;
        v  hm_the_lookup_op k hm;
        let l = hm_length hm;
        hm  hm_exch_op hm 1 l;
        hm  hm_butlast_op hm;
        
        if (l1) then do {
          hm  hm_sink_op hm 1;
          RETURN ((k,v),hm)
        } else RETURN ((k,v),hm)
      }"

    lemma hm_pop_min_op_refine: 
      "(hm_pop_min_op, h.pop_min_op)  hmr_rel  UNIV ×r hmr_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding hm_pop_min_op_def h.pop_min_op_def
      (* Project away stuff of second component *)
      unfolding ignore_snd_refine_conv hm_the_lookup_op_def hm_key_of_op_unfold
      apply (simp cong: if_cong add: Let_def)
      apply (simp add: unused_bind_conv h.val_of_op_def refine_pw_simps)

      (* Prove refinement *)
      apply refine_rcg
      unfolding hmr_rel_def in_br_conv
      apply (unfold heapmap_invar_def;simp)
      apply (auto simp: in_br_conv)
      done

    text We demonstrate two different approaches for proving correctness 
      here.
      The first approach uses the relation to plain heaps only to establish
      the invariant. 

      The second approach also uses the relation to heaps to establish 
      correctness of the result.

      The first approach seems to be more robust against badly set 
      up simpsets, which may be the case in early stages of development.

      Assuming a working simpset, the second approach may be less work,
      and the proof may look more elegant.
        

    text_raw \paragraph{First approach}
    text Transfer heapmin-property to heapmap-domain
    lemma heapmap_min_prop:
      assumes INV: "heapmap_invar hm"  
      assumes V': "heapmap_α hm k = Some v'"
      assumes NE: "hm_valid hm (Suc 0)"
      shows "prio (the (heapmap_α hm (hm_key_of hm (Suc 0))))  prio v'"
    proof -  
      ― ‹Transform into the domain of heaps
      obtain pq m where [simp]: "hm=(pq,m)" by (cases hm)

      from NE have [simp]: "pq[]" by (auto simp: hm_valid_def hm_length_def)

      have CNV_LHS: "prio (the (heapmap_α hm (hm_key_of hm (Suc 0)))) 
        = h.prio_of (hmr_α hm) (Suc 0)"
        by (auto simp: heapmap_α_def hm_key_of_def hmr_α_def h.val_of_def)
        
      from INV have INV': "h.heap_invar (hmr_α hm)"  
        unfolding heapmap_invar_def by auto

      from V' INV obtain i where IDX: "h.valid (hmr_α hm) i" 
        and CNV_RHS: "prio v' = h.prio_of (hmr_α hm) i" 
        apply (clarsimp simp: heapmap_α_def heapmap_invar_def hmr_invar_def hmr_α_def
          h.valid_def h.val_of_def restrict_map_eq)
        by (metis (no_types) Suc_leI comp_apply diff_Suc_Suc 
          diff_zero index_less_size_conv neq0_conv nth_index nth_map 
          old.nat.distinct(2) option.sel)
        
      from h.heap_min_prop[OF INV' IDX] show ?thesis
        unfolding CNV_LHS CNV_RHS .
    qed    


    text With the above lemma, the correctness proof is straightforward
    lemma hm_pop_min_α_correct: "hm_pop_min_op hm n SPEC (λ((k,v),hm'). 
        heapmap_α hm k = Some v 
       heapmap_α hm' = (heapmap_α hm)(k:=None) 
       (k' v'. heapmap_α hm k' = Some v'  prio v  prio v'))"  
      unfolding hm_pop_min_op_def hm_key_of_op_unfold hm_the_lookup_op_def
      apply (refine_vcg 
        hm_exch_op_α_correct[THEN leof_trans]
        hm_butlast_op_α_correct[THEN leof_trans]
        hm_sink_op_α_correct[THEN leof_trans]
        )
      apply (auto simp: heapmap_min_prop)
      done  

    lemma heapmap_nres_rel_prodI:
      assumes "hmx  (UNIV ×r hmr_rel) h'x"
      assumes "h'x  SPEC (λ(_,h'). h.heap_invar h')"
      assumes "hmx n SPEC (λ(r,hm'). RETURN (r,heapmap_α hm')  (R×rId) hx)"
      shows "hmx  (R×rheapmap_rel) hx"
      using assms
      unfolding heapmap_rel_def hmr_rel_def br_def heapmap_invar_def
      apply (auto simp: pw_le_iff pw_leof_iff refine_pw_simps; blast)
      done
      

    lemma hm_pop_min_op_aref: "(hm_pop_min_op, PR_CONST (mop_pm_pop_min prio))  heapmap_rel  (Id×rId)×rheapmap_relnres_rel"  
      unfolding PR_CONST_def
      apply (intro fun_relI nres_relI)
      apply (frule heapmap_hmr_relI)
      unfolding mop_pm_pop_min_alt
      apply (intro ASSERT_refine_right)
      apply (rule heapmap_nres_rel_prodI)
      apply (rule hm_pop_min_op_refine[param_fo, THEN nres_relD]; assumption)
      unfolding heapmap_rel_def hmr_rel_def in_br_conv
      apply (refine_vcg; simp)
      apply (refine_vcg hm_pop_min_α_correct[THEN leof_trans]; simp split: prod.splits)
      done
      
    text_raw \paragraph{Second approach}

    (* Alternative approach: Also use knowledge about result
      in multiset domain. Obtaining property seems infeasible at first attempt! *)  

    definition "hm_kv_of_op hm i  do {
      ASSERT (hm_valid hm i  hmr_invar hm);
      k  hm_key_of_op hm i;
      v  hm_the_lookup_op k hm;
      RETURN (k, v)
    }"


    definition "kvi_rel hm i  {((k,v),v) | k v. hm_key_of hm i = k}"

    lemma hm_kv_op_refine[refine]:
      assumes "(hm,h)hmr_rel"
      shows "hm_kv_of_op hm i  (kvi_rel hm i) (h.val_of_op h i)"
      unfolding hm_kv_of_op_def h.val_of_op_def kvi_rel_def 
        hm_key_of_op_unfold hm_the_lookup_op_def
      apply simp  
      apply refine_vcg
      using assms
      apply (auto 
        simp: hm_valid_def hm_length_def hmr_rel_defs in_br_conv heapmap_α_def hm_key_of_def
        split: prod.splits)
      by (meson contra_subsetD domIff not_None_eq nth_mem)  

    definition hm_pop_min_op' :: "('k,'v) ahm  (('k×'v) × ('k,'v) ahm) nres" where
      "hm_pop_min_op' hm  do {
        ASSERT (heapmap_invar hm);
        ASSERT (hm_valid hm 1);
        kv  hm_kv_of_op hm 1;
        let l = hm_length hm;
        hm  hm_exch_op hm 1 l;
        hm  hm_butlast_op hm;
        
        if (l1) then do {
          hm  hm_sink_op hm 1;
          RETURN (kv,hm)
        } else RETURN (kv,hm)
      }"


    lemma hm_pop_min_op_refine': 
      " (hm,h)hmr_rel   hm_pop_min_op' hm  (kvi_rel hm 1 ×r hmr_rel) (h.pop_min_op h)"
      unfolding hm_pop_min_op'_def h.pop_min_op_def
      (* Project away stuff of second component *)
      unfolding ignore_snd_refine_conv
      (* Prove refinement *)
      apply refine_rcg
      unfolding hmr_rel_def heapmap_rel_def
      apply (unfold heapmap_invar_def; simp add: in_br_conv)
      apply (simp_all add: in_br_conv)
      done


    lemma heapmap_nres_rel_prodI':
      assumes "hmx  (S ×r hmr_rel) h'x"
      assumes "h'x  SPEC Φ"
      assumes "h' r. Φ (r,h')  h.heap_invar h'"
      assumes "hmx n SPEC (λ(r,hm'). (r'. (r,r')S  Φ (r',hmr_α hm'))  hmr_invar hm'  RETURN (r,heapmap_α hm')  (R×rId) hx)"
      shows "hmx  (R×rheapmap_rel) hx"
      using assms
      unfolding heapmap_rel_def hmr_rel_def heapmap_invar_def
      apply (auto 
        simp: pw_le_iff pw_leof_iff refine_pw_simps in_br_conv
        )
      by meson

    lemma ex_in_kvi_rel_conv:
      "(r'. (r,r')kvi_rel hm i  Φ r')  (fst r = hm_key_of hm i  Φ (snd r))"  
      unfolding kvi_rel_def
      apply (cases r)
      apply auto
      done

      
    lemma hm_pop_min_aref': "(hm_pop_min_op', mop_pm_pop_min prio)  heapmap_rel  (Id×rId) ×r heapmap_relnres_rel"  
      apply (intro fun_relI nres_relI)
      apply (frule heapmap_hmr_relI)
      unfolding mop_pm_pop_min_alt
      apply (intro ASSERT_refine_right)
      apply (rule heapmap_nres_rel_prodI')
        apply (erule hm_pop_min_op_refine')

        apply (unfold heapmap_rel_def hmr_rel_def in_br_conv) []
        apply (rule h.pop_min_op_correct)
        apply simp
        apply simp

        apply simp

        apply (clarsimp simp: ex_in_kvi_rel_conv split: prod.splits)
        unfolding hm_pop_min_op'_def hm_kv_of_op_def hm_key_of_op_unfold
          hm_the_lookup_op_def
        apply (refine_vcg 
          hm_exch_op_α_correct[THEN leof_trans]
          hm_butlast_op_α_correct[THEN leof_trans]
          hm_sink_op_α_correct[THEN leof_trans]
          )
        unfolding heapmap_rel_def hmr_rel_def in_br_conv
        apply (auto intro: ranI) 
      done

    subsubsection Remove  

    definition "hm_remove_op k hm  do {
      ASSERT (heapmap_invar hm);
      ASSERT (k  dom (heapmap_α hm));
      i  hm_index_op hm k;
      let l = hm_length hm;
      hm  hm_exch_op hm i l;
      hm  hm_butlast_op hm;
      if i  l then
        hm_repair_op hm i
      else  
        RETURN hm
    }"

    definition (in heapstruct) "remove_op i h  do {
      ASSERT (heap_invar h);
      ASSERT (valid h i);
      let l = length h;
      h  exch_op h i l;
      h  butlast_op h;
      if i  l then
        repair_op h i
      else  
        RETURN h
    }"

    lemma (in -) swap_empty_iff[iff]: "swap l i j = []  l=[]"
      by (auto simp: swap_def)

    lemma (in heapstruct) 
      butlast_exch_last: "butlast (exch h i (length h)) = update (butlast h) i (last h)"  
      unfolding exch_def update_def
      apply (cases h rule: rev_cases)
      apply (auto simp: swap_def butlast_list_update)
      done

    lemma (in heapstruct) remove_op_invar: 
      " heap_invar h; valid h i   remove_op i h  SPEC heap_invar"
      unfolding remove_op_def
      apply refine_vcg
      apply (auto simp: valid_def) []
      apply (auto simp: valid_def exch_def) []
      apply (simp add: butlast_exch_last)
      apply refine_vcg
      apply auto []
      apply auto []
      apply (auto simp: valid_def) []
      apply auto []
      apply auto []
      done

    lemma hm_remove_op_refine[refine]: 
      " (hm,m)heapmap_rel; (hm,h)hmr_rel; heapmap_α hm k  None  
        hm_remove_op k hm  hmr_rel (h.remove_op (hm_index hm k) h)"
      unfolding hm_remove_op_def h.remove_op_def heapmap_rel_def
      (*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
      apply (refine_rcg index_op_inline_refine)
      unfolding hmr_rel_def
      apply (auto simp: in_br_conv)
      done

    lemma hm_remove_op_α_correct: 
      "hm_remove_op k hm n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k:=None))"  
      unfolding hm_remove_op_def
      apply (refine_vcg 
        hm_exch_op_α_correct[THEN leof_trans]
        hm_butlast_op_α_correct[THEN leof_trans]
        hm_repair_op_α_correct[THEN leof_trans]
        hm_index_op_inline_leof
        )
      apply (auto; fail)
      
      apply clarsimp
      apply (rewrite at "hm_index _ k = hm_length _" in asm eq_commute)
      apply (auto; fail)
      done

    lemma hm_remove_op_aref:
      "(hm_remove_op,mop_map_delete_ex)  Id  heapmap_rel  heapmap_relnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding mop_map_delete_ex_alt
      apply (rule ASSERT_refine_right)
      apply (frule heapmap_hmr_relI)
      apply (rule heapmap_nres_relI')
      apply (rule hm_remove_op_refine; assumption?)
      apply (unfold heapmap_rel_def in_br_conv; auto)

      unfolding heapmap_rel_def hmr_rel_def in_br_conv 
      apply (refine_vcg h.remove_op_invar; clarsimp; fail)
      apply (refine_vcg hm_remove_op_α_correct[THEN leof_trans]; simp; fail)
      done
      
    subsubsection Peek-Min 


    definition hm_peek_min_op :: "('k,'v) ahm  ('k×'v) nres" where
      "hm_peek_min_op hm  hm_kv_of_op hm 1"

    lemma hm_peek_min_op_aref: 
      "(hm_peek_min_op, PR_CONST (mop_pm_peek_min prio))  heapmap_rel  Id×rIdnres_rel"  
      unfolding PR_CONST_def
      apply (intro fun_relI nres_relI)
    proof -  
      fix hm and m :: "'k  'v"
      assume A: "(hm,m)heapmap_rel"
      
      from A have [simp]: "h.heap_invar (hmr_α hm)" "hmr_invar hm" "m=heapmap_α hm"
        unfolding heapmap_rel_def in_br_conv heapmap_invar_def
        by simp_all

      have "hm_peek_min_op hm   (kvi_rel hm 1) (h.peek_min_op (hmr_α hm))"
        unfolding hm_peek_min_op_def  h.peek_min_op_def
        apply (refine_rcg hm_kv_op_refine)
        using A
        apply (simp add: heapmap_hmr_relI)
        done
      also have "hmr_α hm  []  (h.peek_min_op (hmr_α hm)) 
         SPEC (λv. vran (heapmap_α hm)  (v'ran (heapmap_α hm). prio v  prio v'))"  
        apply refine_vcg
        by simp_all
      finally show "hm_peek_min_op hm   (Id ×r Id) (mop_pm_peek_min prio m)"  
        unfolding mop_pm_peek_min_alt
        apply (simp add: pw_le_iff refine_pw_simps hm_peek_min_op_def hm_kv_of_op_def 
            hm_key_of_op_unfold hm_the_lookup_op_def)
        apply (fastforce simp: kvi_rel_def ran_def)
        done

    qed    


  end

end