Theory IICF_Abs_Heap

section ‹Heap Implementation On Lists›
theory IICF_Abs_Heap
imports 
  "HOL-Library.Multiset"
  "../../../Sepref" 
  "List-Index.List_Index"
  "../../Intf/IICF_List"
  "../../Intf/IICF_Prio_Bag"
begin

text ‹
  We define Min-Heaps, which implement multisets of prioritized values.
  The operations are: 
    empty heap, emptiness check, insert an element, 
    remove a minimum priority element.›

  subsection ‹Basic Definitions›

  type_synonym 'a heap = "'a list"

  locale heapstruct =
    fixes prio :: "'a  'b::linorder"
  begin
    definition valid :: "'a heap  nat  bool" 
      where "valid h i  i>0  ilength h"

    abbreviation α :: "'a heap  'a multiset" where "α  mset"
  
    
    lemma valid_empty[simp]: "¬valid [] i" by (auto simp: valid_def)
    lemma valid0[simp]: "¬valid h 0" by (auto simp: valid_def)
    lemma valid_glen[simp]: "i>length h  ¬valid h i" by (auto simp: valid_def)

    lemma valid_len[simp]: "h[]  valid h (length h)" by (auto simp: valid_def)

    lemma validI: "0<i  ilength h  valid h i"  
      by (auto simp: valid_def)

    definition val_of :: "'a heap  nat  'a" where "val_of l i  l!(i-1)"
    abbreviation prio_of :: "'a heap  nat  'b" where
      "prio_of l i  prio (val_of l i)"

    subsubsection ‹Navigating the tree›

    definition parent :: "nat  nat" where "parent i  i div 2"
    definition left :: "nat  nat" where "left i  2*i"
    definition right :: "nat  nat" where "right i  2*i + 1"

    abbreviation "has_parent h i  valid h (parent i)"
    abbreviation "has_left h i  valid h (left i)"
    abbreviation "has_right h i  valid h (right i)"

    abbreviation "vparent h i == val_of h (parent i)"
    abbreviation "vleft h i == val_of h (left i)"
    abbreviation "vright h i == val_of h (right i)"

    abbreviation "pparent h i == prio_of h (parent i)"
    abbreviation "pleft h i == prio_of h (left i)"
    abbreviation "pright h i == prio_of h (right i)"

    lemma parent_left_id[simp]: "parent (left i) = i"
      unfolding parent_def left_def
      by auto

    lemma parent_right_id[simp]: "parent (right i) = i"
      unfolding parent_def right_def
      by auto

    lemma child_of_parentD:
      "has_parent l i  left (parent i) = i  right (parent i) = i"
      unfolding parent_def left_def right_def valid_def
      by auto

    lemma rc_imp_lc: "valid h i; has_right h i  has_left h i"
      by (auto simp: valid_def left_def right_def)

    lemma plr_corner_cases[simp]: 
      assumes "0<i"
      shows 
      "iparent i"
      "ileft i"
      "iright i"
      "parent i  i"
      "left i  i"
      "right i  i"
      using assms
      by (auto simp: parent_def left_def right_def)

    lemma i_eq_parent_conv[simp]: "i=parent i  i=0"  
      by (auto simp: parent_def)

    subsubsection ‹Heap Property›
    text ‹The heap property states, that every node's priority is greater 
      or equal to its parent's priority ›
    definition heap_invar :: "'a heap  bool"
      where "heap_invar l 
       i. valid l i  has_parent l i  pparent l i  prio_of l i"


    definition "heap_rel1  br α heap_invar"  
    
    lemma heap_invar_empty[simp]: "heap_invar []"
      by (auto simp: heap_invar_def)

    function heap_induction_scheme :: "nat  unit" where
      "heap_induction_scheme i = (
        if i>1 then heap_induction_scheme (parent i) else ())"
      by pat_completeness auto  

    termination
      apply (relation "less_than")
      apply (auto simp: parent_def)
      done

    lemma 
      heap_parent_le: "heap_invar l; valid l i; has_parent l i 
         pparent l i  prio_of l i"
      unfolding heap_invar_def
      by auto

    lemma heap_min_prop:
      assumes H: "heap_invar h"
      assumes V: "valid h i"
      shows "prio_of h (Suc 0)  prio_of h i"
    proof (cases "i>1")
      case False with V show ?thesis
        by (auto simp: valid_def intro: Suc_lessI)
    next
      case True
      from V have "ilength h" "valid h (Suc 0)" by (auto simp: valid_def)
      with True show ?thesis
        apply (induction i rule: heap_induction_scheme.induct)  
        apply (rename_tac i)
        apply (case_tac "parent i = Suc 0")
        apply (rule order_trans[rotated])
        apply (rule heap_parent_le[OF H])
        apply (auto simp: valid_def) [3]

        apply (rule order_trans)  
        apply (rprems)
        apply (auto simp: parent_def) [4]
        apply (rule heap_parent_le[OF H])
        apply (auto simp: valid_def parent_def)
        done
    qed

    text ‹ Obviously, the heap property can also be stated in terms of children,
      i.e., each node's priority is smaller or equal to it's children's priority.›

    definition "children_ge h p i  
      (has_left h i  p  pleft h i)
     (has_right h i  p  pright h i)"
    
    definition "heap_invar' h  i. valid h i  children_ge h (prio_of h i) i"

    lemma heap_eq_heap':
      shows "heap_invar h  heap_invar' h"
      unfolding heap_invar_def 
      unfolding heap_invar'_def children_ge_def
      apply rule
      apply auto []
      apply clarsimp
      apply (frule child_of_parentD)
      apply auto []
      done

    subsection ‹Basic Operations›  
    text ‹The basic operations are the only operations that directly 
      modify the underlying data structure.›
    subsubsection ‹Val-Of›
    abbreviation (input) "val_of_pre l i  valid l i"
    definition val_of_op :: "'a heap  nat  'a nres" 
      where "val_of_op l i  ASSERT (i>0)  mop_list_get l (i-1)"
    lemma val_of_correct[refine_vcg]: 
      "val_of_pre l i  val_of_op l i  SPEC (λr. r = val_of l i)"
      unfolding val_of_op_def val_of_def valid_def
      by refine_vcg auto
    
    abbreviation (input) "prio_of_pre  val_of_pre"  
    definition "prio_of_op l i  do {v  val_of_op l i; RETURN (prio v)}"
    lemma prio_of_op_correct[refine_vcg]: 
      "prio_of_pre l i  prio_of_op l i  SPEC (λr. r = prio_of l i)"
      unfolding prio_of_op_def
      apply refine_vcg by simp

    subsubsection ‹Update›
    abbreviation "update_pre h i v  valid h i"
    definition update :: "'a heap  nat  'a  'a heap" 
      where "update h i v  h[i - 1 := v]"
    definition update_op :: "'a heap  nat  'a  'a heap nres" 
      where "update_op h i v  ASSERT (i>0)  mop_list_set h (i-1) v"
    lemma update_correct[refine_vcg]:
      "update_pre h i v  update_op h i v  SPEC(λr. r = update h i v)"
      unfolding update_op_def update_def valid_def by refine_vcg auto

    lemma update_valid[simp]: "valid (update h i v) j  valid h j"  
      by (auto simp: update_def valid_def)

    lemma val_of_update[simp]: "update_pre h i v; valid h j  val_of (update h i v) j = (
      if i=j then v else val_of h j)"  
      unfolding update_def val_of_def
      by (auto simp: nth_list_update valid_def)

    lemma length_update[simp]: "length (update l i v) = length l"
      by (auto simp: update_def)

    subsubsection ‹Exchange›
    text ‹ Exchange two elements ›

    definition exch :: "'a heap  nat  nat  'a heap" where
      "exch l i j  swap l (i - 1) (j - 1)"
    abbreviation "exch_pre l i j  valid l i  valid l j"

    definition exch_op :: "'a list  nat  nat  'a list nres"
    where "exch_op l i j  do { 
      ASSERT (i>0  j>0);
      l  mop_list_swap l (i - 1) (j - 1);
      RETURN l
    }"

    lemma exch_op_alt: "exch_op l i j = do { 
      vi  val_of_op l i;
      vj  val_of_op l j;
      l  update_op l i vj;
      l  update_op l j vi;
      RETURN l }"
      by (auto simp: exch_op_def swap_def val_of_op_def update_op_def 
        pw_eq_iff refine_pw_simps)

    lemma exch_op_correct[refine_vcg]: 
      "exch_pre l i j  exch_op l i j  SPEC (λr. r = exch l i j)"
      unfolding exch_op_def 
      apply refine_vcg
      apply (auto simp: exch_def valid_def)
      done
       
    lemma valid_exch[simp]: "valid (exch l i j) k = valid l k"
      unfolding exch_def by (auto simp: valid_def)
    
    lemma val_of_exch[simp]: "valid l i; valid l j; valid l k  
      val_of (exch l i j) k = (
        if k=i then val_of l j
        else if k=j then val_of l i
        else val_of l k
      )"
      unfolding exch_def val_of_def valid_def
      by (auto)

    lemma exch_eq[simp]: "exch h i i = h" 
      by (auto simp: exch_def)

    lemma α_exch[simp]: "valid l i; valid l j 
       α (exch l i j) = α l"
      unfolding exch_def valid_def 
      by (auto)

    lemma length_exch[simp]: "length (exch l i j) = length l"
      by (auto simp: exch_def)

    subsubsection ‹Butlast›
    text ‹Remove last element›

    abbreviation "butlast_pre l  l[]"
    definition butlast_op :: "'a heap  'a heap nres"
      where "butlast_op l  mop_list_butlast l"
    lemma butlast_op_correct[refine_vcg]: 
      "butlast_pre l  butlast_op l  SPEC (λr. r = butlast l)"
      unfolding butlast_op_def by (refine_vcg; auto)

    lemma valid_butlast_conv[simp]: "valid (butlast h) i  valid h i  i < length h"
      by (auto simp: valid_def)

    lemma valid_butlast: "valid (butlast h) i  valid h i"  
      by (cases h rule: rev_cases) (auto simp: valid_def)
    
    lemma val_of_butlast[simp]: "valid h i; i<length h 
       val_of (butlast h) i = val_of h i"
      by (auto simp: valid_def val_of_def nth_butlast)

    lemma val_of_butlast'[simp]: 
      "valid (butlast h) i  val_of (butlast h) i = val_of h i"
      by (cases h rule: rev_cases) (auto simp: valid_def val_of_def nth_append)

    lemma α_butlast[simp]: " length h  0  
       α (butlast h) = α h - {# val_of h (length h)#}"
      apply (cases h rule: rev_cases)
      apply (auto simp: val_of_def)   
      done

    lemma heap_invar_butlast[simp]: "heap_invar h  heap_invar (butlast h)"
      apply (cases "h = []")
      apply simp
      apply (auto simp: heap_invar_def dest: valid_butlast)
      done

    subsubsection ‹Append›  
    definition append_op :: "'a heap  'a  'a heap nres"
      where "append_op l v  mop_list_append l v"
    lemma append_op_correct[refine_vcg]: 
      "append_op l v  SPEC (λr. r = l@[v])"
      unfolding append_op_def by (refine_vcg; auto)
    

    lemma valid_append[simp]: "valid (l@[v]) i  valid l i  i = length l + 1"
      by (auto simp: valid_def)

    lemma val_of_append[simp]: "valid (l@[v]) i  
      val_of (l@[v]) i = (if valid l i then val_of l i else v)"
      unfolding valid_def val_of_def by (auto simp: nth_append)

    lemma α_append[simp]: "α (l@[v]) = α l + {#v#}"
      by auto

    subsection ‹Auxiliary operations›  
    text ‹The auxiliary operations do not have a corresponding abstract operation, but
      are to restore the heap property after modification.›
    subsubsection ‹Swim›

    text ‹This invariant expresses that the heap has a single defect,
      which can be repaired by swimming up›  
    definition swim_invar :: "'a heap  nat  bool"
      where "swim_invar h i  
        valid h i
       (j. valid h j  has_parent h j  ji  pparent h j  prio_of h j)
       (has_parent h i  
        (j. valid h j  has_parent h j  parent j = i 
           pparent h i  prio_of h j))"

    text ‹Move up an element that is too small, until it fits›
    definition swim_op :: "'a heap  nat  'a heap nres" where
      "swim_op h i  do {
        RECT (λswim (h,i). do {
          ASSERT (valid h i  swim_invar h i);
          if has_parent h i then do {
            ppi  prio_of_op h (parent i);
            pi  prio_of_op h i;
            if (¬ppi  pi) then do {
              h  exch_op h i (parent i);
              swim (h, parent i)
            } else
              RETURN h
          } else 
            RETURN h
        }) (h,i)
      }"

    lemma swim_invar_valid: "swim_invar h i  valid h i"
      unfolding swim_invar_def by simp
    
    lemma swim_invar_exit1: "¬has_parent h i  swim_invar h i  heap_invar h"
      unfolding heap_invar_def swim_invar_def by auto

    lemma swim_invar_exit2: "pparent h i  prio_of h i  swim_invar h i  heap_invar h"
      unfolding heap_invar_def swim_invar_def by auto

    lemma swim_invar_pres:
      assumes HPI: "has_parent h i" 
      assumes VIOLATED: "pparent h i > prio_of h i" 
      and INV: "swim_invar h i"
      defines "h'  exch h i (parent i)"
      shows "swim_invar h' (parent i)"
      unfolding swim_invar_def
      apply safe
      apply (simp add: h'_def HPI)

      using HPI VIOLATED INV
      unfolding swim_invar_def h'_def
      apply auto []

      using HPI VIOLATED INV
      unfolding swim_invar_def h'_def
      apply auto
      by (metis order_trans)


    lemma swim_invar_decr:
      assumes INV: "heap_invar h"
      assumes V: "valid h i"
      assumes DECR: "prio v  prio_of h i"
      shows "swim_invar (update h i v) i"
      using INV V DECR
      apply (auto simp: swim_invar_def heap_invar_def intro: dual_order.trans)
      done

    lemma swim_op_correct[refine_vcg]: 
    "swim_invar h i 
      swim_op h i  SPEC (λh'. α h' = α h  heap_invar h'  length h' = length h)"  
      unfolding swim_op_def
      using [[goals_limit = 1]]
      apply (refine_vcg  RECT_rule[where 
          pre="λ(hh,i). 
            swim_invar hh i 
           α hh = α h 
           length hh = length h" and
          V = "inv_image less_than snd"
          ])
      apply (auto) []
      apply (auto) []
      apply (auto) []
      apply (auto) []
      apply (auto simp: swim_invar_valid) []
      apply (auto) []
      apply (auto) []
      apply (auto) []

      apply rprems
        apply (auto simp: swim_invar_pres) []
        apply (auto simp: parent_def valid_def) []

      apply (auto) []
      apply (auto simp: swim_invar_exit2) []
      apply (auto) []
      apply (auto) []
      apply (auto simp: swim_invar_exit1) []
      apply (auto) []
      done



    subsubsection ‹Sink›
    text ‹Move down an element that is too big, until it fits in›

    definition sink_op :: "'a heap  nat  'a heap nres" where
      "sink_op h i  do {
        RECT (λsink (h,i). do {
          ASSERT (valid h i);
          if has_right h i then do {
            ASSERT (has_left h i);
            lp  prio_of_op h (left i);
            rp  prio_of_op h (right i);
            p  prio_of_op h i;
            if (lp < p  rp  lp) then do {
              h  exch_op h i (left i);
              sink (h,left i)
            } else if (rp<lp  rp < p) then do {
              h  exch_op h i (right i);
              sink (h,right i)
            } else 
              RETURN h
          } else if (has_left h i) then do {
            lp  prio_of_op h (left i);
            p  prio_of_op h i;
            if (lp < p) then do {
              h  exch_op h i (left i);
              sink (h,left i)
            } else
              RETURN h
            
          } else 
            RETURN h
        }) (h,i)
      }"

    text ‹This invariant expresses that the heap has a single defect, 
      which can be repaired by sinking›
    definition "sink_invar l i  
      valid l i
     (j. valid l j  ji  children_ge l (prio_of l j) j)
     (has_parent l i  children_ge l (pparent l i) i)"
    
    lemma sink_invar_valid: "sink_invar l i  valid l i"
      unfolding sink_invar_def by auto
    
    lemma sink_invar_exit: "sink_invar l i; children_ge l (prio_of l i) i 
       heap_invar' l"
      unfolding heap_invar'_def sink_invar_def
      by auto
    
    lemma sink_aux1: "¬ (2*i  length h)  ¬has_left h i  ¬has_right h i"
      unfolding valid_def left_def right_def by auto
    
    lemma sink_invar_pres1:
      assumes "sink_invar h i"
      assumes "has_left h i" "has_right h i"
      assumes "prio_of h i  pleft h i"
      assumes "pleft h i  pright h i"
      shows "sink_invar (exch h i (right i)) (right i)"
      using assms  
      unfolding sink_invar_def
      apply auto
      apply (auto simp: children_ge_def)
      done
    
    lemma sink_invar_pres2:
      assumes "sink_invar h i"
      assumes "has_left h i" "has_right h i"
      assumes "prio_of h i  pleft h i"
      assumes "pleft h i  pright h i"
      shows "sink_invar (exch h i (left i)) (left i)"
      using assms  
      unfolding sink_invar_def
      apply auto
      apply (auto simp: children_ge_def)
      done
    
    lemma sink_invar_pres3:
      assumes "sink_invar h i"
      assumes "has_left h i" "has_right h i"
      assumes "prio_of h i  pright h i"
      assumes "pleft h i  pright h i"
      shows "sink_invar (exch h i (left i)) (left i)"
      using assms  
      unfolding sink_invar_def
      apply auto
      apply (auto simp: children_ge_def)
      done
    
    lemma sink_invar_pres4:
      assumes "sink_invar h i"
      assumes "has_left h i" "has_right h i"
      assumes "prio_of h i  pright h i"
      assumes "pleft h i  pright h i"
      shows "sink_invar (exch h i (right i)) (right i)"
      using assms  
      unfolding sink_invar_def
      apply auto
      apply (auto simp: children_ge_def)
      done
    
    lemma sink_invar_pres5:
      assumes "sink_invar h i"
      assumes "has_left h i" "¬has_right h i"
      assumes "prio_of h i  pleft h i"
      shows "sink_invar (exch h i (left i)) (left i)"
      using assms  
      unfolding sink_invar_def
      apply auto
      apply (auto simp: children_ge_def)
      done
    
    lemmas sink_invar_pres = 
      sink_invar_pres1 
      sink_invar_pres2 
      sink_invar_pres3 
      sink_invar_pres4 
      sink_invar_pres5


    lemma sink_invar_incr:
      assumes INV: "heap_invar h"
      assumes V: "valid h i"
      assumes INCR: "prio v  prio_of h i"
      shows "sink_invar (update h i v) i"
      using INV V INCR
      apply (auto simp: sink_invar_def)
      apply (auto simp: children_ge_def heap_invar_def) []
      apply (auto simp: children_ge_def heap_invar_def intro: order_trans) []
      apply (frule spec[where x="left i"])
      apply auto []
      apply (frule spec[where x="right i"])
      apply auto []
      done


    lemma sink_op_correct[refine_vcg]: 
    "sink_invar h i 
      sink_op h i  SPEC (λh'. α h' = α h  heap_invar h'  length h' = length h)"  
      unfolding sink_op_def heap_eq_heap'
      using [[goals_limit = 1]]

      apply (refine_vcg  RECT_rule[where 
          pre="λ(hh,i). sink_invar hh i  α hh = α h  length hh = length h" and
          V = "measure (λ(l,i). length l - i)"
          ])

      apply (auto) []
      apply (auto) []
      apply (auto) []
      apply (auto) []
      apply (auto simp: sink_invar_valid) []
      apply (auto simp: valid_def left_def right_def) []

      apply rprems
        apply (auto intro: sink_invar_pres) []
        apply (auto simp: valid_def left_def right_def) []

      apply rprems
        apply (auto intro: sink_invar_pres) []
        apply (auto simp: valid_def left_def right_def) []

      apply (auto) []

      apply clarsimp
      apply (rule sink_invar_exit, assumption) []
      apply (auto simp: children_ge_def) []

      apply (auto) []
      
      apply rprems
        apply (auto intro: sink_invar_pres) []
        apply (auto simp: valid_def left_def right_def) []

      apply (auto) []

      apply clarsimp
      apply (rule sink_invar_exit, assumption) []
      apply (auto simp: children_ge_def) []

      apply (auto) []

      apply (auto) []

      apply clarsimp
      apply (rule sink_invar_exit, assumption) []
      apply (auto simp: children_ge_def) []

      apply (auto) []
      done

    lemma sink_op_swim_rule: 
      "swim_invar h i  sink_op h i  SPEC (λh'. h'=h)"  
      apply (frule swim_invar_valid)
      unfolding sink_op_def
      apply (subst RECT_unfold, refine_mono)
      apply (fold sink_op_def)
      apply refine_vcg
      apply (simp_all)
      apply (auto simp add: valid_def left_def right_def dest: swim_invar_valid) []
      apply (auto simp: swim_invar_def) []
      apply (auto simp: swim_invar_def) []
      apply (auto simp: swim_invar_def) []
      apply (auto simp: swim_invar_def) []
      apply (auto simp: swim_invar_def) []
      apply (auto simp: swim_invar_def) []
      done

    definition sink_op_opt
      ― ‹Sink operation as presented in Sedgewick et al. Algs4 reference implementation›
    where   
      "sink_op_opt h k  RECT (λD (h,k). do {
        ASSERT (k>0  klength h);
        let len = length h;
        if (2*k  len) then do {
          let j = 2*k;
          pj  prio_of_op h j;

          j  (
            if j<len then do {
              psj  prio_of_op h (Suc j);
              if pj>psj then RETURN (j+1) else RETURN j
            } else RETURN j);

          pj  prio_of_op h j;
          pk  prio_of_op h k;
          if (pk > pj) then do {
            h  exch_op h k j;
            D (h,j)
          } else
            RETURN h
        } else RETURN h    
      }) (h,k)"

    lemma sink_op_opt_eq: "sink_op_opt h k = sink_op h k"
      unfolding sink_op_opt_def sink_op_def
      apply (fo_rule arg_cong fun_cong)+
      apply (intro ext)
      unfolding sink_op_def[symmetric]
      apply (simp cong: if_cong split del: if_split add: Let_def)

      apply (auto simp: valid_def left_def right_def prio_of_op_def val_of_op_def 
        val_of_def less_imp_diff_less ASSERT_same_eq_conv nz_le_conv_less) []
      done

    subsubsection ‹Repair›  
    text ‹Repair a local defect in the heap. This can be done 
      by swimming and sinking. Note that, depending on the defect, only one
      of the operations will change the heap. 
      Moreover, note that we do not need repair to implement the heap operations. 
      However, it is required for heapmaps. ›
    
    definition "repair_op h i  do {
      h  sink_op h i;
      h  swim_op h i;
      RETURN h
    }"

    lemma update_sink_swim_cases:
      assumes "heap_invar h"
      assumes "valid h i"
      obtains "swim_invar (update h i v) i" | "sink_invar (update h i v) i"
      apply (cases rule: linear[of "prio v" "prio_of h i", THEN disjE])
      apply (blast dest: swim_invar_decr[OF assms])
      apply (blast dest: sink_invar_incr[OF assms])
      done

    lemma heap_invar_imp_swim_invar: "heap_invar h; valid h i  swim_invar h i"
      unfolding heap_invar_def swim_invar_def
      by (auto intro: order_trans)


    lemma repair_correct[refine_vcg]:
      assumes "heap_invar h" and "valid h i"
      shows "repair_op (update h i v) i  SPEC (λh'.
        heap_invar h'  α h' = α (update h i v)  length h' = length h)"
      apply (rule update_sink_swim_cases[of h i v, OF assms])
      unfolding repair_op_def  
      apply (refine_vcg sink_op_swim_rule)
      apply auto [4]
      apply (refine_vcg)
      using assms(2)
      apply (auto intro: heap_invar_imp_swim_invar simp: valid_def) []
      apply auto [3]
      done

    subsection ‹Operations›

    (*
    subsubsection ‹Length›
    definition length_op :: "'a heap ⇒ nat nres" where "length_op ≡ lst_op_length"

    lemma [refine_vcg]: "length_op l ≤ SPEC (λr. r = length l)"
      unfolding length_op_def
      by refine_vcg
    *)  

    subsubsection ‹Empty›
    abbreviation (input) empty :: "'a heap" ― ‹The empty heap›
      where "empty  []"
    definition empty_op :: "'a heap nres" 
      where "empty_op  mop_list_empty"
    lemma empty_op_correct[refine_vcg]:
      "empty_op  SPEC (λr. α r = {#}  heap_invar r)"
      unfolding empty_op_def apply refine_vcg by auto

    subsubsection ‹Emptiness check›  
    definition is_empty_op :: "'a heap  bool nres" ― ‹Check for emptiness›
      where "is_empty_op h  do {ASSERT (heap_invar h); let l=length h; RETURN (l=0)}"
    lemma is_empty_op_correct[refine_vcg]: 
      "heap_invar h  is_empty_op h  SPEC (λr. rα h = {#})"  
      unfolding is_empty_op_def
      apply refine_vcg by auto

    subsubsection ‹Insert›
    definition insert_op :: "'a  'a heap  'a heap nres" ― ‹Insert element›
      where "insert_op v h  do {
        ASSERT (heap_invar h);
        h  append_op h v;
        let l = length h;
        h  swim_op h l;
        RETURN h
      }"

    lemma swim_invar_insert: "heap_invar l  swim_invar (l@[x]) (Suc (length l))"
      unfolding swim_invar_def heap_invar_def valid_def parent_def val_of_def
      by (fastforce simp: nth_append)

    lemma  
      "(insert_op,RETURN oo op_mset_insert)  Id  heap_rel1  heap_rel1nres_rel"
      unfolding insert_op_def[abs_def] heap_rel1_def o_def
      by refine_vcg (auto simp: swim_invar_insert in_br_conv)

    lemma insert_op_correct:
      "heap_invar h  insert_op v h  SPEC (λh'. heap_invar h'  α h' = α h + {#v#})"
      unfolding insert_op_def
      by (refine_vcg) (auto simp: swim_invar_insert)
    lemmas [refine_vcg] = insert_op_correct  

    subsubsection ‹Pop minimum element›  

    definition pop_min_op :: "'a heap  ('a × 'a heap) nres" where
      "pop_min_op h  do {
        ASSERT (heap_invar h);
        ASSERT (valid h 1);
        m  val_of_op h 1;
        let l = length h;
        h  exch_op h 1 l;
        h  butlast_op h;
        
        if (l1) then do {
          h  sink_op h 1;
          RETURN (m,h)
        } else RETURN (m,h)
      }"


    lemma left_not_one[simp]: "left j  Suc 0"  
      by (auto simp: left_def)

    lemma right_one_conv[simp]: "right j = Suc 0  j=0"
      by (auto simp: right_def)

    lemma parent_one_conv[simp]: "parent (Suc 0) = 0"  
      by (auto simp: parent_def)

    lemma sink_invar_init:
      assumes I: "heap_invar h" 
      assumes NE: "length h > 1" 
      shows "sink_invar (butlast (exch h (Suc 0) (length h))) (Suc 0)"
    proof -
      from NE have V: "valid h (Suc 0)" "valid h (length h)" 
        apply -
        apply (auto simp: valid_def neq_Nil_conv) []
        by (cases h) (auto simp: valid_def)
    
      show ?thesis using I
        unfolding heap_eq_heap' heap_invar'_def sink_invar_def
        apply (intro impI conjI allI)
        using NE apply (auto simp: V valid_butlast_conv) []
        apply (auto simp add: children_ge_def V NE valid_butlast_conv) []
        apply (auto simp add: children_ge_def V NE valid_butlast_conv) []
        done
    qed

    lemma in_set_conv_val: "v  set h  (i. valid h i  v = val_of h i)"
      apply (rule iffI)
      apply (clarsimp simp add: valid_def val_of_def in_set_conv_nth)
      apply (rule_tac x="Suc i" in exI; auto)
      apply (clarsimp simp add: valid_def val_of_def in_set_conv_nth)
      apply (rule_tac x="i - Suc 0" in exI; auto)
      done
      

    lemma pop_min_op_correct: 
      assumes "heap_invar h" "α h  {#}" 
      shows "pop_min_op h  SPEC (λ(v,h'). heap_invar h' 
        v ∈# α h  α h' = α h - {#v#}  (v'set_mset (α h). prio v  prio v'))"
    proof -    
      note [simp del] = length_greater_0_conv
      note LG = length_greater_0_conv[symmetric]

      from assms show ?thesis
        unfolding pop_min_op_def  
        apply refine_vcg
        apply (simp_all add: sink_invar_init LG)
        apply (auto simp: valid_def) []
        apply (cases h; auto simp: val_of_def) [] (* FIXME: Looking below val_of! *)
        apply (auto simp: in_set_conv_val simp: heap_min_prop) []
        apply auto []
        apply (cases h; auto simp: val_of_def) [] (* FIXME: Looking below val_of! *)
        apply auto []
        apply (cases h; auto simp: val_of_def) [] (* FIXME: Looking below val_of! *)
        done
    qed    

    lemmas [refine_vcg] = pop_min_op_correct

    subsubsection ‹Peek minimum element›

    definition peek_min_op :: "'a heap  'a nres" where
      "peek_min_op h  do {
        ASSERT (heap_invar h);
        ASSERT (valid h 1);
        val_of_op h 1
      }"
    
    lemma peek_min_op_correct:
      assumes "heap_invar h" "α h  {#}" 
      shows "peek_min_op h  SPEC (λv. 
        v ∈# α h  (v'set_mset (α h). prio v  prio v'))"
      unfolding peek_min_op_def  
      apply refine_vcg
      using assms
      apply clarsimp_all
      apply (auto simp: valid_def) []  
      apply (cases h; auto simp: val_of_def) [] (* FIXME: Looking below val_of! *)
      apply (auto simp: in_set_conv_val simp: heap_min_prop) []
      done
      
    lemmas peek_min_op_correct'[refine_vcg] = peek_min_op_correct


    subsection ‹Operations as Relator-Style Refinement›

    lemma empty_op_refine: "(empty_op,RETURN op_mset_empty)heap_rel1nres_rel"
      apply (rule nres_relI)
      apply (rule order_trans)  
      apply (rule empty_op_correct)
      apply (auto simp: heap_rel1_def br_def pw_le_iff refine_pw_simps)
      done

    lemma is_empty_op_refine: "(is_empty_op,RETURN o op_mset_is_empty)  heap_rel1  bool_relnres_rel"
      apply (intro nres_relI fun_relI; simp)
      apply refine_vcg  
      apply (auto simp: heap_rel1_def br_def)
      done  

    lemma insert_op_refine: "(insert_op,RETURN oo op_mset_insert)  Id  heap_rel1  heap_rel1nres_rel"
      apply (intro nres_relI fun_relI; simp)
      apply (refine_vcg RETURN_as_SPEC_refine)
      apply (auto simp: heap_rel1_def br_def pw_le_iff refine_pw_simps)
      done  

    lemma pop_min_op_refine: 
      "(pop_min_op, PR_CONST (mop_prio_pop_min prio))  heap_rel1  Id ×r heap_rel1nres_rel"
      apply (intro fun_relI nres_relI)
      unfolding mop_prio_pop_min_def PR_CONST_def
      apply (refine_vcg SPEC_refine)
      apply (auto simp: heap_rel1_def br_def)
      done

    lemma peek_min_op_refine: 
      "(peek_min_op, PR_CONST (mop_prio_peek_min prio))  heap_rel1  Idnres_rel"
      apply (intro fun_relI nres_relI)
      unfolding mop_prio_peek_min_def PR_CONST_def
      apply (refine_vcg RES_refine)
      apply (auto simp: heap_rel1_def br_def)
      done


  end  

end