Theory Pairing_Heap_LLVM.Heaps_Abs

theory Heaps_Abs
  imports Ordered_Pairing_Heap_List2
    Weidenbach_Book_Base.Explorer
    Isabelle_LLVM.IICF
    More_Sepref.WB_More_Refinement
begin


text ‹
  We first tried to follow the setup from Isabelle LLVM, but it is not
  clear how useful this really is. Hence we adapted the definition from
  the abstract operations.
›
locale hmstruct_with_prio =
    fixes lt :: ‹'v ⇒ 'v ⇒ bool› and
    le :: ‹'v ⇒ 'v ⇒ bool›
  assumes hm_le: ‹⋀a b. le a b ⟷ a = b ∨ lt a b› and
    hm_trans: ‹transp le› and
    hm_transt: ‹transp lt› and
    hm_totalt: ‹totalp lt›
begin

    definition prio_peek_min where
      "prio_peek_min ≡  (λ(𝒜, b, w). (λv.
          v ∈# b
        ∧ (∀v'∈set_mset b. le (w v) (w v'))))"

    definition mop_prio_peek_min where
      "mop_prio_peek_min ≡  (λ(𝒜, b, w). doN {ASSERT (b≠{#}); SPEC (prio_peek_min (𝒜, b,w))})"

    definition mop_prio_change_weight where
      "mop_prio_change_weight ≡  (λv ω (𝒜, b, w). doN {
        ASSERT (v ∈# 𝒜);
        ASSERT (v ∈# b ⟶ le ω (w v));
        RETURN (𝒜, b, w(v := ω))
     })"

    definition mop_prio_insert where
      "mop_prio_insert ≡  (λv ω (𝒜, b, w). doN {
        ASSERT (v ∉# b ∧  v∈#𝒜);
        RETURN (𝒜, add_mset v b, w(v := ω))
     })"

    definition mop_prio_is_in where
      ‹mop_prio_is_in = (λv (𝒜, b, w). do {
      ASSERT (v ∈# 𝒜);
      RETURN (v ∈#b)
      })›
    definition mop_prio_insert_maybe where
      "mop_prio_insert_maybe ≡  (λv ω (bw). doN {
        b ← mop_prio_is_in v bw;
        if ¬b then mop_prio_insert v ω (bw)
        else mop_prio_change_weight v ω (bw)
     })"

     text ‹TODO this is a shortcut and it could make sense to force w to remember the old values.›
    definition mop_prio_old_weight where
      "mop_prio_old_weight = (λv (𝒜, b, w). doN {
        ASSERT (v ∈# 𝒜);
        b ← mop_prio_is_in v (𝒜, b, w);
        if b then RETURN (w v) else RES UNIV
     })"

    definition mop_prio_insert_raw_unchanged where
      "mop_prio_insert_raw_unchanged = (λv h. doN {
        ASSERT (v ∉# fst (snd h));
        w ← mop_prio_old_weight v h;
        mop_prio_insert v w h
     })"

    definition mop_prio_insert_unchanged where
      "mop_prio_insert_unchanged =  (λv (bw). doN {
        b ← mop_prio_is_in v bw;
        if ¬b then mop_prio_insert_raw_unchanged v (bw)
        else RETURN bw
     })"

    definition prio_del where
      ‹prio_del = (λv (𝒜, b, w). (𝒜, b - {#v#}, w))›

    definition mop_prio_del where
      "mop_prio_del = (λv (𝒜, b, w). doN {
        ASSERT (v ∈# b ∧ v ∈# 𝒜);
        RETURN (prio_del v (𝒜, b, w))
     })"

    definition mop_prio_pop_min where
      "mop_prio_pop_min = (λ𝒜bw. doN {
      v ← mop_prio_peek_min 𝒜bw;
      bw ← mop_prio_del v 𝒜bw;
      RETURN (v, bw)
      })"

sublocale pairing_heap
  by unfold_locales (rule hm_le hm_trans hm_transt hm_totalt)+

end

end