Theory Refine_Imperative_HOL.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 ∧ i≤length 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 ⟹ i≤length 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
"i≠parent i"
"i≠left i"
"i≠right 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 "i≤length 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 ∧ j≠i ⟶ 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 ∧ j≠i ⟶ 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
where
"sink_op_opt h k ≡ RECT (λD (h,k). do {
ASSERT (k>0 ∧ k≤length 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 ‹Empty›
abbreviation (input) empty :: "'a 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"
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"
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_rel1⟩nres_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 (l≠1) 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) []
apply (auto simp: in_set_conv_val simp: heap_min_prop) []
apply auto []
apply (cases h; auto simp: val_of_def) []
apply auto []
apply (cases h; auto simp: val_of_def) []
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) []
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_rel1⟩nres_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_rel⟩nres_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_rel1⟩nres_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_rel1⟩nres_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 → ⟨Id⟩nres_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