Theory Pairing_Heap_LLVM.Pairing_Heaps

theory Pairing_Heaps_Impl imports Relational_Pairing_Heaps Map_Fun_Rel begin hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC section ‹Imperative Pairing heaps› type_synonym ('a,'b)pairing_heaps_imp = ‹('a option list × 'a option list × 'a option list × 'a option list × 'b list × 'a option)› definition pairing_heaps_rel :: ‹('a option × nat option) set ⇒ ('b option ×'c option) set ⇒ (('a,'b)pairing_heaps_imp × (nat multiset × (nat,'c) hp_fun × nat option)) set› where pairing_heaps_rel_def_internal: ‹pairing_heaps_rel R S = {((prevs', nxts', children', parents', scores', h'), (𝒱, (prevs, nxts, children, parents, scores), h)). (h', h) ∈ R ∧ (prevs', prevs) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (nxts', nxts) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (children', children) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (parents', parents) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (map Some scores', scores) ∈ ⟨S⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) }› lemma pairing_heaps_rel_def: ‹⟨R,S⟩pairing_heaps_rel = {((prevs', nxts', children', parents', scores', h'), (𝒱, (prevs, nxts, children, parents, scores), h)). (h', h) ∈ R ∧ (prevs', prevs) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (nxts', nxts) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (children', children) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (parents', parents) ∈ ⟨R⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) ∧ (map Some scores', scores) ∈ ⟨S⟩map_fun_rel ((λa. (a,a))` set_mset 𝒱) }› unfolding pairing_heaps_rel_def_internal relAPP_def by auto definition op_hp_read_nxt_imp where ‹op_hp_read_nxt_imp = (λi (prevs, nxts, children, parents, scores, h). do { (nxts ! i) })› definition mop_hp_read_nxt_imp where ‹mop_hp_read_nxt_imp = (λi (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length nxts); RETURN (nxts ! i) })› lemma op_hp_read_nxt_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ (op_hp_read_nxt_imp i xs, hp_read_nxt' j ys) ∈ R› unfolding op_hp_read_nxt_imp_def by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma mop_hp_read_nxt_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ mop_hp_read_nxt_imp i xs ≤ SPEC (λa. (a, hp_read_nxt' j ys) ∈ R)› unfolding mop_hp_read_nxt_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) done definition op_hp_read_prev_imp where ‹op_hp_read_prev_imp = (λi (prevs, nxts, children, parents, scores, h). do { prevs ! i })› definition mop_hp_read_prev_imp where ‹mop_hp_read_prev_imp = (λi (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length prevs); RETURN (prevs ! i) })› lemma op_hp_read_prev_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ (op_hp_read_prev_imp i xs, hp_read_prev' j ys) ∈ R› unfolding op_hp_read_prev_imp_def by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma mop_hp_read_prev_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ mop_hp_read_prev_imp i xs ≤ SPEC (λa. (a, hp_read_prev' j ys) ∈ R)› unfolding mop_hp_read_prev_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) done definition op_hp_read_child_imp where ‹op_hp_read_child_imp = (λi (prevs, nxts, children, parents, scores, h). do { (children ! i) })› definition mop_hp_read_child_imp where ‹mop_hp_read_child_imp = (λi (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length children); RETURN (children ! i) })› lemma op_hp_read_child_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ (op_hp_read_child_imp i xs, hp_read_child' j ys) ∈ R› unfolding op_hp_read_child_imp_def by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma mop_hp_read_child_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ mop_hp_read_child_imp i xs ≤ SPEC (λa. (a, hp_read_child' j ys) ∈ R)› unfolding mop_hp_read_child_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) done definition mop_hp_read_parent_imp where ‹mop_hp_read_parent_imp = (λi (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length parents); RETURN (parents ! i) })› definition op_hp_read_parent_imp where ‹op_hp_read_parent_imp = (λi (prevs, nxts, children, parents, scores, h). do { (parents ! i) })› lemma op_hp_read_parent_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ (op_hp_read_parent_imp i xs, hp_read_parent' j ys) ∈ R› unfolding op_hp_read_parent_imp_def by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma mop_hp_read_parent_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ mop_hp_read_parent_imp i xs ≤ SPEC (λa. (a, hp_read_parent' j ys) ∈ R)› unfolding mop_hp_read_parent_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) done definition op_hp_read_score_imp :: ‹nat ⇒ ('a,'b)pairing_heaps_imp ⇒ 'b› where ‹op_hp_read_score_imp = (λi (prevs, nxts, children, parents, scores, h). do { ((scores ! i)) })› definition mop_hp_read_score_imp :: ‹nat ⇒ ('a,'b)pairing_heaps_imp ⇒ 'b nres› where ‹mop_hp_read_score_imp = (λi (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length scores); RETURN ((scores ! i)) })› lemma mop_hp_read_score_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ mop_hp_read_score_imp i xs ≤ SPEC (λa. (Some a, hp_read_score' j ys) ∈ S)› unfolding mop_hp_read_score_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def dest!: bspec) done fun hp_set_all' where ‹hp_set_all' i p q r s t (𝒱, u, h) = (𝒱, hp_set_all i p q r s t u, h)› definition mop_hp_set_all_imp :: ‹nat ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres›where ‹mop_hp_set_all_imp = (λi p q r s t (prevs, nxts, children, parents, scores, h). do { ASSERT (i < length nxts ∧ i < length prevs ∧ i < length parents ∧ i < length children ∧ i < length scores); RETURN (prevs[i := p], nxts[i:=q], children[i:=r], parents[i:=s], scores[i:=t], h) })› lemma mop_hp_set_all_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹(i,j)∈nat_rel ⟹ (p',p)∈R ⟹ (q',q)∈R⟹(r',r)∈R ⟹ (s',s)∈R⟹ (Some t',t)∈S ⟹ j ∈# fst ys ⟹ mop_hp_set_all_imp i p' q' r' s' t' xs ≤ SPEC (λa. (a, hp_set_all' j p q r s t ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_set_all_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def) subgoal by (force simp: pairing_heaps_rel_def map_fun_rel_def hp_set_all_def) done lemma fst_hp_set_all'[simp]: ‹fst (hp_set_all' i p q r s t x) = fst x› by (cases x) auto fun update_source_node_impl :: ‹_ ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp› where ‹update_source_node_impl i (prevs, nxts, parents, children, scores,_) = (prevs, nxts, parents, children, scores, i)› fun source_node_impl :: ‹('a,'b)pairing_heaps_imp ⇒ 'a option› where ‹source_node_impl (prevs, nxts, parents, children, scores,h) = h› lemma update_source_node_impl_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j) ∈ R ⟹ (update_source_node_impl i xs, update_source_node j ys) ∈ ⟨R,S⟩pairing_heaps_rel› by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma source_node_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (source_node_impl xs, source_node ys) ∈ R› by (auto simp: pairing_heaps_rel_def map_fun_rel_def) lemma hp_insert_alt_def: ‹hp_insert = (λi w arr. do { let h = source_node arr; if h = None then do { ASSERT (i ∈# fst arr); let arr = (hp_set_all' i None None None None (Some w) arr); RETURN (update_source_node (Some i) arr) } else do { ASSERT (i ∈# fst arr); ASSERT (hp_read_prev' i arr = None); ASSERT (hp_read_parent' i arr = None); let j = the h; ASSERT (j ∈# (fst arr) ∧ j ≠ i); ASSERT (hp_read_score' j (arr) ≠ None); ASSERT (hp_read_prev' j arr = None ∧ hp_read_nxt' j arr = None ∧ hp_read_parent' j arr = None); let y = (the (hp_read_score' j arr)); if y < w then do { let arr = hp_set_all' i None None (Some j) None (Some w) arr; ASSERT (j ∈# fst arr); let arr = hp_update_parents' j (Some i) arr; RETURN (update_source_node (Some i) arr) } else do { let child = hp_read_child' j arr; ASSERT (child ≠ None ⟶ the child ∈# fst arr); let arr = hp_set_all' j None None (Some i) None (Some y) arr; ASSERT (i ∈# fst arr); let arr = hp_set_all' i None child None (Some j) (Some (w)) arr; ASSERT (child ≠ None ⟶ the child ∈# fst arr); let arr = (if child = None then arr else hp_update_prev' (the child) (Some i) arr); ASSERT (child ≠ None ⟶ the child ∈# fst arr); let arr = (if child = None then arr else hp_update_parents' (the child) None arr); RETURN arr } } })› (is ‹?A = ?B›) proof - have ‹?A i w arr ≤ ⇓Id (?B i w arr)› for i w arr unfolding hp_insert_def by refine_vcg (solves ‹auto intro!: simp: Let_def›)+ moreover have ‹?B i w arr ≤ ⇓Id (?A i w arr)› for i w arr unfolding hp_insert_def by refine_vcg (auto intro!: ext bind_cong[OF refl] simp: Let_def) ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed definition mop_hp_update_prev'_imp :: ‹nat ⇒ 'a option ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres› where ‹mop_hp_update_prev'_imp = (λi v (prevs, nxts, parents, children). do { ASSERT (i < length prevs); RETURN (prevs[i:=v], nxts, parents, children) })› lemma mop_hp_update_prev'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ j ∈# fst ys ⟹ (i,j)∈nat_rel ⟹ (p',p)∈R ⟹ mop_hp_update_prev'_imp i p' xs ≤ SPEC (λa. (a, hp_update_prev' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_update_prev'_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def hp_update_prev_def) subgoal by (force simp: pairing_heaps_rel_def map_fun_rel_def hp_update_prev_def) done definition mop_hp_update_parent'_imp :: ‹nat ⇒ 'a option ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres› where ‹mop_hp_update_parent'_imp = (λi v (prevs, nxts,children, parents, scores). do { ASSERT (i < length parents); RETURN (prevs, nxts, children, parents[i:=v], scores) })› lemma mop_hp_update_parent'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ j ∈# fst ys ⟹ (i,j)∈nat_rel ⟹ (p',p)∈R ⟹ mop_hp_update_parent'_imp i p' xs ≤ SPEC (λa. (a, hp_update_parents' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_update_parent'_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def hp_update_parents_def) subgoal by (force simp: pairing_heaps_rel_def map_fun_rel_def hp_update_parents_def) done definition mop_hp_update_nxt'_imp :: ‹nat ⇒ 'a option ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres› where ‹mop_hp_update_nxt'_imp = (λi v (prevs, nxts, parents, children). do { ASSERT (i < length nxts); RETURN (prevs, nxts[i:=v], parents, children) })› lemma mop_hp_update_nxt'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ j ∈# fst ys ⟹ (i,j)∈nat_rel ⟹ (p',p)∈R ⟹ mop_hp_update_nxt'_imp i p' xs ≤ SPEC (λa. (a, hp_update_nxt' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_update_nxt'_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def hp_update_prev_def) subgoal by (force simp: pairing_heaps_rel_def map_fun_rel_def hp_update_nxt_def) done definition mop_hp_update_score_imp :: ‹nat ⇒ 'b ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres› where ‹mop_hp_update_score_imp = (λi v (prevs, nxts, parents, children, scores, h). do { ASSERT (i < length scores); RETURN (prevs, nxts, parents, children, scores[i:=v], h) })› lemma mop_hp_update_score_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈nat_rel ⟹ j ∈# fst ys ⟹ (Some p', p)∈S ⟹ mop_hp_update_score_imp i p' xs ≤ SPEC (λa. (a, hp_update_score' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_update_score_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def hp_update_prev_def) subgoal by (force simp: pairing_heaps_rel_def map_fun_rel_def hp_update_score_def) done definition mop_hp_update_child'_imp :: ‹nat ⇒ 'a option ⇒ ('a,'b)pairing_heaps_imp ⇒ ('a,'b)pairing_heaps_imp nres› where ‹mop_hp_update_child'_imp = (λi v (prevs, nxts, children, parents, scores). do { ASSERT (i < length children); RETURN (prevs, nxts, children[i:=v], parents, scores) })› lemma mop_hp_update_child'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ j ∈# fst ys ⟹ (i,j)∈nat_rel ⟹ (p',p)∈R ⟹ mop_hp_update_child'_imp i p' xs ≤ SPEC (λa. (a, hp_update_child' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding mop_hp_update_child'_imp_def apply refine_vcg subgoal by (auto simp: pairing_heaps_rel_def map_fun_rel_def hp_update_prev_def) subgoal by (force simp add: pairing_heaps_rel_def map_fun_rel_def hp_update_child_def) done (*TODO it is kind of unclear whether we should use nat or have a conversion 'a ⇒ nat as locale*) definition mop_hp_insert_impl :: ‹nat ⇒ 'b::linorder ⇒ (nat,'b)pairing_heaps_imp ⇒ (nat,'b)pairing_heaps_imp nres› where ‹mop_hp_insert_impl = (λi (w::'b) (arr :: (nat,'b)pairing_heaps_imp). do { let h = source_node_impl arr; if h = None then do { arr ← mop_hp_set_all_imp i None None None None w arr; RETURN (update_source_node_impl (Some i) arr) } else do { ASSERT (op_hp_read_prev_imp i arr = None); ASSERT (op_hp_read_parent_imp i arr = None); let j = (the h); ASSERT (op_hp_read_prev_imp j arr = None ∧ op_hp_read_nxt_imp j arr = None ∧ op_hp_read_parent_imp j arr = None); y ← mop_hp_read_score_imp j arr; if y < w then do { arr ← mop_hp_set_all_imp i None None (Some j) None ((w)) (arr); arr← mop_hp_update_parent'_imp j (Some i) arr; RETURN (update_source_node_impl (Some i) arr) } else do { child ← mop_hp_read_child_imp j arr; arr ← mop_hp_set_all_imp j None None (Some i) None (y) arr; arr ← mop_hp_set_all_imp i None child None (Some j) w arr; arr ← (if child = None then RETURN arr else mop_hp_update_prev'_imp (the child) (Some i) arr); arr ← (if child = None then RETURN arr else mop_hp_update_parent'_imp (the child) None arr); RETURN arr } } })› lemma Some_x_y_option_theD: ‹(Some x, y) ∈ ⟨S⟩option_rel ⟹ (x, the y) ∈ S› by (auto simp: option_rel_def) context begin private lemma in_pairing_heaps_rel_still: ‹(arra, arr') ∈ ⟨⟨nat_rel⟩option_rel, ⟨S⟩option_rel⟩pairing_heaps_rel ⟹ arr' = arr'' ⟹ (arra, arr'') ∈ ⟨⟨nat_rel⟩option_rel, ⟨S⟩option_rel⟩pairing_heaps_rel› by auto lemma mop_hp_insert_impl_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› ‹(i,j)∈nat_rel› ‹(w,w')∈nat_rel› shows ‹mop_hp_insert_impl i w xs ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (hp_insert j w' ys)› proof - have [refine]: ‹(Some i, Some j) ∈ ⟨nat_rel⟩option_rel› using assms by auto have K: ‹hp_read_child' (the (source_node ys)) ys ≠ None ⟶ the (hp_read_child' (the (source_node ys)) ys) ∈ 𝒱 ⟹ the (source_node ys) ∈# fst ys ⟹ op_hp_read_child_imp (the (source_node_impl xs)) xs ≠ None ⟹ the (op_hp_read_child_imp (the (source_node ys)) xs) ∈ 𝒱› for 𝒱 using op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] assms by auto show ?thesis using assms unfolding mop_hp_insert_impl_def hp_insert_alt_def apply (refine_vcg mop_hp_set_all_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_score_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel› and ys=ys and j=‹the (source_node_impl xs)›] Some_x_y_option_theD[where S=nat_rel] mop_hp_update_parent'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_child_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_prev'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel› and j=‹the (hp_read_child' (the (source_node ys)) ys)›]) subgoal by (auto dest: source_node_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro!: update_source_node_impl_spec simp: refl_on_def) subgoal by (auto dest!: op_hp_read_prev_imp_spec) subgoal by (auto dest!: op_hp_read_parent_imp_spec) subgoal using op_hp_read_parent_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] apply auto by (metis op_hp_read_prev_imp_spec pair_in_Id_conv) subgoal using op_hp_read_nxt_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal using op_hp_read_parent_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by auto subgoal by auto subgoal by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by auto subgoal by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal HH using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by auto subgoal by auto apply (rule in_pairing_heaps_rel_still, assumption) subgoal by auto apply assumption subgoal by auto subgoal using op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] by (metis HH option.collapse) subgoal using HH by auto apply (rule in_pairing_heaps_rel_still, assumption) subgoal by auto apply (assumption) apply (rule K) apply assumption subgoal by auto subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] by auto subgoal apply (frule K) by auto (metis BNF_Greatest_Fixpoint.IdD assms(1) op_hp_read_child_imp_spec option_rel_simp(3) source_node_spec)+ apply (rule autoref_opt(1)) subgoal using source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] by auto subgoal by auto done qed lemma hp_link_alt_def: ‹hp_link = (λ(i::'a) j arr. do { ASSERT (i ≠ j); ASSERT (i ∈# fst arr); ASSERT (j ∈# fst arr); ASSERT (hp_read_score' i arr ≠ None); ASSERT (hp_read_score' j arr ≠ None); let x = (the (hp_read_score' i arr)::'b::order); let y = (the (hp_read_score' j arr)::'b); let prev = hp_read_prev' i arr; let nxt = hp_read_nxt' j arr; ASSERT (nxt ≠ Some i ∧ nxt ≠ Some j); ASSERT (prev ≠ Some i ∧ prev ≠ Some j); let (parent,ch,w_p, w_c_h) = (if y < x then (i, j, x, y) else (j, i, y, x)); ASSERT (parent ∈# fst arr); ASSERT (ch ∈# fst arr); let child = hp_read_child' parent arr; ASSERT (child ≠ Some i ∧ child ≠ Some j); let child_c_h = hp_read_child' ch arr; ASSERT (child_c_h ≠ Some i ∧ child_c_h ≠ Some j ∧ (child_c_h ≠ None ⟶ child_c_h ≠ child)); ASSERT (distinct ([i, j] @ (if child_c_h ≠ None then [the child_c_h] else []) @ (if child ≠ None then [the child] else []) @ (if prev ≠ None then [the prev] else []) @ (if nxt ≠ None then [the nxt] else [])) ); ASSERT (ch ∈# fst arr); ASSERT (parent ∈# fst arr); ASSERT (child ≠ None ⟶ the child ∈# fst arr); ASSERT (nxt ≠ None ⟶ the nxt ∈# fst arr); ASSERT (prev ≠ None ⟶ the prev ∈# fst arr); let arr = hp_set_all' parent prev nxt (Some ch) None (Some (w_p::'b)) arr; let arr = hp_set_all' ch None child child_c_h (Some parent) (Some (w_c_h::'b)) arr; let arr = (if child = None then arr else hp_update_prev' (the child) (Some ch) arr); let arr = (if nxt = None then arr else hp_update_prev' (the nxt) (Some parent) arr); let arr = (if prev = None then arr else hp_update_nxt' (the prev) (Some parent) arr); let arr = (if child = None then arr else hp_update_parents' (the child) None arr); RETURN (arr, parent) })› (is ‹?A = ?B›) proof - define f where ‹f i j x y ≡ (if y < x then (i::'a, j::'a, x::'b, y::'b) else (j, i, y, x))› for i j x y have ‹?A i j arr ≤ ⇓Id (?B i j arr)› for i arr j unfolding hp_link_def f_def[symmetric] apply refine_vcg subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by simp (metis option.simps(2)) done moreover have ‹?B i j arr ≤ ⇓Id (?A i j arr)› for i j arr unfolding hp_link_def case_prod_beta f_def[symmetric] apply refine_vcg subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: f_def) subgoal by (auto simp: f_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (cases arr) simp done ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed definition maybe_mop_hp_update_prev'_imp where ‹maybe_mop_hp_update_prev'_imp child ch arr = (if child = None then RETURN arr else mop_hp_update_prev'_imp (the child) ch arr)› definition maybe_mop_hp_update_nxt'_imp where ‹maybe_mop_hp_update_nxt'_imp child ch arr = (if child = None then RETURN arr else mop_hp_update_nxt'_imp (the child) ch arr)› definition maybe_mop_hp_update_child'_imp where ‹maybe_mop_hp_update_child'_imp child ch arr = (if child = None then RETURN arr else mop_hp_update_child'_imp (the child) ch arr)› definition maybe_mop_hp_update_parent'_imp where ‹maybe_mop_hp_update_parent'_imp child ch arr = (if child = None then RETURN arr else mop_hp_update_parent'_imp (the child) ch arr)› lemma maybe_mop_hp_update_prev'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈⟨nat_rel⟩option_rel ⟹ (j ≠ None ⟹ the j ∈# fst ys) ⟹ (p',p)∈R ⟹ maybe_mop_hp_update_prev'_imp i p' xs ≤ SPEC (λa. (a, maybe_hp_update_prev' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding maybe_mop_hp_update_prev'_imp_def maybe_hp_update_prev'_def by (refine_vcg mop_hp_update_prev'_imp_spec) auto lemma maybe_mop_hp_update_nxt'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈⟨nat_rel⟩option_rel ⟹ (j ≠ None ⟹ the j ∈# fst ys) ⟹ (p',p)∈R ⟹ maybe_mop_hp_update_nxt'_imp i p' xs ≤ SPEC (λa. (a, maybe_hp_update_nxt' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding maybe_mop_hp_update_nxt'_imp_def maybe_hp_update_nxt'_def by (refine_vcg mop_hp_update_nxt'_imp_spec) auto lemma maybe_mop_hp_update_parent'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈⟨nat_rel⟩option_rel ⟹ (j ≠ None ⟹ the j ∈# fst ys) ⟹ (p',p)∈R ⟹ maybe_mop_hp_update_parent'_imp i p' xs ≤ SPEC (λa. (a, maybe_hp_update_parents' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding maybe_mop_hp_update_parent'_imp_def maybe_hp_update_parents'_def by (refine_vcg mop_hp_update_parent'_imp_spec) auto lemma maybe_mop_hp_update_child'_imp_spec: ‹(xs, ys) ∈ ⟨R,S⟩pairing_heaps_rel ⟹ (i,j)∈⟨nat_rel⟩option_rel ⟹ (j ≠ None ⟹ the j ∈# fst ys) ⟹ (p',p)∈R ⟹ maybe_mop_hp_update_child'_imp i p' xs ≤ SPEC (λa. (a, maybe_hp_update_child' j p ys) ∈ ⟨R,S⟩pairing_heaps_rel)› unfolding maybe_mop_hp_update_child'_imp_def maybe_hp_update_child'_def by (refine_vcg mop_hp_update_child'_imp_spec) auto definition mop_hp_link_imp :: ‹nat ⇒nat ⇒(nat, 'b::ord)pairing_heaps_imp ⇒ _ nres› where ‹mop_hp_link_imp = (λi j arr. do { ASSERT (i ≠ j); x ← mop_hp_read_score_imp i arr; y ← mop_hp_read_score_imp j arr; prev ← mop_hp_read_prev_imp i arr; nxt ← mop_hp_read_nxt_imp j arr; let (parent,ch,w_p, w_c_h) = (if y < x then (i, j, x, y) else (j, i, y, x)); child ← mop_hp_read_child_imp parent arr; child_c_h ← mop_hp_read_child_imp ch arr; arr ← mop_hp_set_all_imp parent prev nxt (Some ch) None ((w_p)) arr; arr ← mop_hp_set_all_imp ch None child child_c_h (Some parent) ((w_c_h)) arr; arr ← (if child = None then RETURN arr else mop_hp_update_prev'_imp (the child) (Some ch) arr); arr ← (if nxt = None then RETURN arr else mop_hp_update_prev'_imp (the nxt) (Some parent) arr); arr ← (if prev = None then RETURN arr else mop_hp_update_nxt'_imp (the prev) (Some parent) arr); arr ← (if child = None then RETURN arr else mop_hp_update_parent'_imp (the child) None arr); RETURN (arr, parent) })› lemma mop_hp_link_imp_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› ‹(i,j)∈nat_rel› ‹(w,w')∈nat_rel› shows ‹mop_hp_link_imp i w xs ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ×_r nat_rel) (hp_link j w' ys)› proof - have [refine]: ‹(Some i, Some j) ∈ ⟨nat_rel⟩option_rel› using assms by auto define f where ‹f i j x y ≡ RETURN (if y < x then (i::nat, j::nat, x::nat, y::nat) else (j, i, y, x))› for i j x y have Hf: ‹do {let (parent, ch, w_p, w_c_h) = (if y < x then (i, j, x, y) else (j, i, y, x)); P parent ch w_p w_c_h} = do {(parent, ch, w_p, w_c_h) ← f i j x y; P parent ch w_p w_c_h}› for i j x y w xs P unfolding f_def let_to_bind_conv .. have K: ‹hp_read_child' (the (source_node ys)) ys ≠ None ⟶ the (hp_read_child' (the (source_node ys)) ys) ∈ 𝒱 ⟹ the (source_node ys) ∈# fst ys ⟹ op_hp_read_child_imp (the (source_node_impl xs)) xs ≠ None ⟹ the (op_hp_read_child_imp (the (source_node ys)) xs) ∈ 𝒱› for 𝒱 using op_hp_read_child_imp_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel› ‹the (source_node ys)› ‹the (source_node_impl xs)›] source_node_spec[of xs ys ‹⟨nat_rel⟩option_rel› ‹⟨nat_rel⟩option_rel›] assms by auto have [refine]: ‹(x,x')∈nat_rel ⟹ (y,y')∈nat_rel⟹ f i w x y ≤ ⇓ (nat_rel ×_r nat_rel ×_r nat_rel ×_r nat_rel) (f j w' x' y')› for x' y' x y using assms by auto show ?thesis using assms op_hp_read_nxt_imp_spec[OF assms(1) assms(2)] op_hp_read_prev_imp_spec[OF assms(1) assms(2)] op_hp_read_child_imp_spec[OF assms(1) assms(2)] op_hp_read_nxt_imp_spec[OF assms(1) assms(3)] unfolding mop_hp_link_imp_def hp_link_alt_def Hf maybe_mop_hp_update_parent'_imp_def[symmetric] maybe_mop_hp_update_prev'_imp_def[symmetric] maybe_mop_hp_update_nxt'_imp_def[symmetric] maybe_hp_update_prev'_def[symmetric] maybe_hp_update_parents'_def[symmetric] maybe_hp_update_nxt'_def[symmetric] apply - apply (refine_vcg mop_hp_set_all_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_score_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel› and ys=ys and i=i and j=j] mop_hp_read_score_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel› and ys=ys and i=w and j=w'] Some_x_y_option_theD[where S=nat_rel] mop_hp_update_parent'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_prev'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel› and j=‹the (hp_read_child' (the (source_node ys)) ys)›] maybe_mop_hp_update_parent'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] maybe_mop_hp_update_prev'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] maybe_mop_hp_update_nxt'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_child_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_prev_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_nxt_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_parent_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›]) subgoal by (auto dest: source_node_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (solves auto) subgoal by auto subgoal by auto apply (solves auto) subgoal by simp apply (solves auto) apply (solves auto) done qed lemma vsids_pass₁_alt_def: ‹vsids_pass₁ = (λ(arr::'a multiset × ('a,'c::order) hp_fun × 'a option) (j::'a). do { (arr, j, _, n) ← WHILE_T(λ(arr, j,_, _). j ≠ None) (λ(arr, j, e::nat, n). do { if j = None then RETURN (arr, None, e, n) else do { let j = the j; ASSERT (j ∈# fst arr); let nxt = hp_read_nxt' j arr; if nxt = None then RETURN (arr, nxt, e+1, j) else do { ASSERT (nxt ≠ None); ASSERT (the nxt ∈# fst arr); let nnxt = hp_read_nxt' (the nxt) arr; (arr, n) ← hp_link j (the nxt) arr; RETURN (arr, nnxt, e+2, n) }} }) (arr, Some j, 0::nat, j); RETURN (arr, n) })› (is ‹?A = ?B›) proof - have K[refine]: ‹x2 = (x1a, x2a) ⟹ i = (x1, x2) ⟹ (((x1, x1a, x2a), Some arr, 0, arr), i::'a multiset × ('a,'c::order) hp_fun × 'a option, Some arr, 0::nat, arr) ∈ Id ×_r ⟨Id⟩option_rel ×_r nat_rel ×_r Id› ‹⋀x1 x2 x1a x2a. x2 = (x1a, x2a) ⟹ i = (x1, x2) ⟹ ((i, Some arr, 0, arr), (x1, x1a, x2a), Some arr, 0, arr) ∈ Id ×_r ⟨Id⟩option_rel ×_r nat_rel ×_r Id› for x2 x1a x2a arr x1 i by auto have [refine]: ‹(a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹ hp_link a b c ≤⇓Id (hp_link a' b' c')› for a b c a' b' c' by auto have ‹?A i arr ≤ ⇓Id (?B i arr)› for i arr unfolding vsids_pass₁_def by refine_vcg (solves auto)+ moreover have ‹?B i arr ≤ ⇓Id (?A i arr)› for i arr unfolding vsids_pass₁_def by refine_vcg (solves ‹auto intro!: ext bind_cong[OF refl] simp: Let_def›)+ ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed definition mop_vsids_pass₁_imp :: ‹(nat, 'b::ord)pairing_heaps_imp ⇒ nat ⇒ _ nres› where ‹mop_vsids_pass₁_imp = (λarr j. do { (arr, j, n) ← WHILE_T(λ(arr, j, _). j ≠ None) (λ(arr, j, n). do { if j = None then RETURN (arr, None, n) else do { let j = the j; nxt ← mop_hp_read_nxt_imp j arr; if nxt = None then RETURN (arr, nxt, j) else do { ASSERT (nxt ≠ None); nnxt ← mop_hp_read_nxt_imp (the nxt) arr; (arr, n) ← mop_hp_link_imp j (the nxt) arr; RETURN (arr, nnxt, n) }} }) (arr, Some j, j); RETURN (arr, n) })› lemma mop_vsids_pass₁_imp_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› ‹(i,j)∈nat_rel› shows ‹mop_vsids_pass₁_imp xs i ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ×_r nat_rel) (vsids_pass₁ ys j)› proof - let ?R = ‹{((arr, j, n), (arr', j', _, n')). (arr, arr') ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ∧ (j, j') ∈ ⟨nat_rel⟩option_rel ∧ (n,n')∈Id}› have K[refine0]: ‹((xs, Some i, i), ys, Some j, 0, j) ∈ ?R› using assms by auto show ?thesis unfolding mop_vsids_pass₁_imp_def vsids_pass₁_alt_def apply (refine_vcg mop_hp_insert_impl_spec WHILET_refine[where R= ?R] mop_hp_read_nxt_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_link_imp_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma vsids_pass₂_alt_def: ‹vsids_pass₂ = (λarr (j::'a). do { ASSERT (j ∈# fst arr); let nxt = hp_read_prev' j arr; (arr, j, leader, _) ← WHILE_T(λ(arr, j, leader, e). j ≠ None) (λ(arr, j, leader, e::nat). do { if j = None then RETURN (arr, None, leader, e) else do { let j = the j; ASSERT (j ∈# fst arr); let nnxt = hp_read_prev' j arr; (arr, n) ← hp_link j leader arr; RETURN (arr, nnxt, n, e+1) } }) (arr, nxt, j, 1::nat); RETURN (update_source_node (Some leader) arr) })› (is ‹?A = ?B›) proof - have K[refine]: ‹(((fst i, fst (snd i), snd (snd i)), hp_read_prev arr (fst (snd i)), arr, 1::nat), i, hp_read_prev' arr i, arr, 1::nat) ∈ Id ×_r ⟨Id⟩option_rel ×_r Id ×_r Id› ‹((i, hp_read_prev' arr i, arr, 1), (fst i, fst (snd i), snd (snd i)), hp_read_prev arr (fst (snd i)), arr, 1) ∈ Id ×_r ⟨Id⟩option_rel ×_r Id ×_r Id› for i arr by auto have [refine]: ‹(a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹ hp_link a b c ≤⇓Id (hp_link a' b' c')› for a b c a' b' c' by auto have ‹?A i arr ≤ ⇓Id (?B i arr)› for i arr unfolding vsids_pass₂_def case_prod_beta[of _ i] case_prod_beta[of _ ‹snd i›] by refine_vcg (solves auto)+ moreover have ‹?B i arr ≤ ⇓Id (?A i arr)› for i arr unfolding vsids_pass₂_def case_prod_beta[of _ i] case_prod_beta[of _ ‹snd i›] by refine_vcg (solves ‹auto intro!: ext bind_cong[OF refl] simp: Let_def›)+ ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed definition mop_vsids_pass₂_imp where ‹mop_vsids_pass₂_imp = (λarr (j::nat). do { nxt ← mop_hp_read_prev_imp j arr; (arr, j, leader) ← WHILE_T(λ(arr, j, leader). j ≠ None) (λ(arr, j, leader). do { if j = None then RETURN (arr, None, leader) else do { let j = the j; nnxt ← mop_hp_read_prev_imp j arr; (arr, n) ← mop_hp_link_imp j leader arr; RETURN (arr, nnxt, n) } }) (arr, nxt, j); RETURN (update_source_node_impl (Some leader) arr) })› lemma mop_vsids_pass₂_imp_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› ‹(i,j)∈nat_rel› shows ‹mop_vsids_pass₂_imp xs i ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (vsids_pass₂ ys j)› proof - let ?R = ‹{((arr, j, n), (arr', j', n', _)). (arr, arr') ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ∧ (j, j') ∈ ⟨nat_rel⟩option_rel ∧ (n,n')∈Id}› have K[refine0]: ‹((xs, Some i, i), ys, Some j, j, 0) ∈ ?R› using assms by auto show ?thesis using assms unfolding mop_vsids_pass₂_imp_def vsids_pass₂_alt_def apply (refine_vcg mop_hp_insert_impl_spec WHILET_refine[where R= ?R] mop_hp_read_nxt_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_prev_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_link_imp_spec mop_vsids_pass₁_imp_spec update_source_node_impl_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition mop_merge_pairs_imp where ‹mop_merge_pairs_imp arr j = do { (arr, j) ← mop_vsids_pass₁_imp arr j; mop_vsids_pass₂_imp arr j }› lemma mop_merge_pairs_imp_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› ‹(i,j)∈nat_rel› shows ‹mop_merge_pairs_imp xs i ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (merge_pairs ys j)› using assms unfolding mop_merge_pairs_imp_def merge_pairs_def by (refine_vcg mop_vsids_pass₁_imp_spec mop_vsids_pass₂_imp_spec) auto lemma vsids_pop_min_alt_def: ‹vsids_pop_min = (λarr. do { let h = source_node arr; if h = None then RETURN (None, arr) else do { ASSERT (the h ∈# fst arr); let j = hp_read_child' (the h) arr; if j = None then RETURN (h, (update_source_node None arr)) else do { ASSERT (the j ∈# fst arr); let arr = hp_update_prev' (the h) None arr; let arr = hp_update_child' (the h) None arr; let arr = hp_update_parents' (the j) None arr; arr ← merge_pairs (update_source_node None arr) (the j); RETURN (h, arr) } } })› (is ‹?A = ?B›) proof - have [simp]: ‹source_node arr = None ⟹ (fst arr, fst (snd arr), None) = arr› for arr by (cases arr) auto have K[refine]: ‹((source_node arr, fst arr, fst (snd arr), None), source_node arr, update_source_node None arr) ∈ Id› ‹((source_node arr, update_source_node None arr), source_node arr, fst arr, fst (snd arr), None) ∈ Id› for i arr by (solves ‹cases arr; auto›)+ have [refine]: ‹merge_pairs (fst arr, hp_update_parents (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) None (hp_update_child (the (source_node arr)) None (hp_update_prev (the (source_node arr)) None (fst (snd arr)))), None) (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) ≤ ⇓ Id (merge_pairs (update_source_node None (hp_update_parents' (the (hp_read_child' (the (source_node arr)) arr)) None (hp_update_child' (the (source_node arr)) None (hp_update_prev' (the (source_node arr)) None arr)))) (the (hp_read_child' (the (source_node arr)) arr)))› ‹merge_pairs (update_source_node None (hp_update_parents' (the (hp_read_child' (the (source_node arr)) arr)) None (hp_update_child' (the (source_node arr)) None (hp_update_prev' (the (source_node arr)) None arr)))) (the (hp_read_child' (the (source_node arr)) arr)) ≤ ⇓ Id (merge_pairs (fst arr, hp_update_parents (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) None (hp_update_child (the (source_node arr)) None (hp_update_prev (the (source_node arr)) None (fst (snd arr)))), None) (the (hp_read_child (the (source_node arr)) (fst (snd arr)))))› for arr by (solves ‹cases arr; auto›)+ have K: ‹snd (snd arr) = source_node arr› for arr by (cases arr) auto have ‹?A arr ≤ ⇓Id (?B arr)› for i arr unfolding vsids_pop_min_def case_prod_beta[of _ arr] case_prod_beta[of _ ‹snd arr›] K by refine_vcg (solves auto)+ moreover have ‹?B arr ≤ ⇓Id (?A arr)› for i arr unfolding vsids_pop_min_def case_prod_beta[of _ arr] case_prod_beta[of _ ‹snd arr›] K by refine_vcg (solves ‹auto intro!: ext bind_cong[OF refl] simp: Let_def›)+ ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed definition mop_vsids_pop_min_impl where ‹mop_vsids_pop_min_impl = (λarr. do { let h = source_node_impl arr; if h = None then RETURN (None, arr) else do { j ← mop_hp_read_child_imp (the h) arr; if j = None then RETURN (h, update_source_node_impl None arr) else do { arr ← mop_hp_update_prev'_imp (the h) None arr; arr ← mop_hp_update_child'_imp (the h) None arr; arr ← mop_hp_update_parent'_imp (the j) None arr; arr ← mop_merge_pairs_imp (update_source_node_impl None arr) (the j); RETURN (h, arr) } } })› lemma mop_vsids_pop_min_impl: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› shows ‹mop_vsids_pop_min_impl xs ≤ ⇓(⟨nat_rel⟩option_rel ×_r ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (vsids_pop_min ys)› proof - let ?R = ‹{((arr, j, n), (arr', j', n', _)). (arr, arr') ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ∧ (j, j') ∈ ⟨nat_rel⟩option_rel ∧ (n,n')∈Id}› have K[refine0]: ‹(the (source_node_impl xs), the (source_node ys)) ∈ nat_rel› if ‹source_node ys ≠ None› using source_node_spec[OF assms] by auto show ?thesis using assms source_node_spec[OF assms] unfolding mop_vsids_pop_min_impl_def vsids_pop_min_alt_def apply (refine_vcg mop_hp_insert_impl_spec WHILET_refine[where R= ?R] mop_hp_read_nxt_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_prev_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_link_imp_spec mop_vsids_pass₁_imp_spec mop_merge_pairs_imp_spec mop_hp_read_child_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_prev'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_child'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_parent'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›]) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal by auto subgoal by auto done qed definition mop_vsids_pop_min2_impl where ‹mop_vsids_pop_min2_impl = (λarr. do { let h = source_node_impl arr; ASSERT (h ≠ None); j ← mop_hp_read_child_imp (the h) arr; if j = None then RETURN (the h, update_source_node_impl None arr) else do { arr ← mop_hp_update_prev'_imp (the h) None arr; arr ← mop_hp_update_child'_imp (the h) None arr; arr ← mop_hp_update_parent'_imp (the j) None arr; arr ← mop_merge_pairs_imp (update_source_node_impl None arr) (the j); RETURN (the h, arr) } })› lemma vsids_pop_min2_alt_def: ‹vsids_pop_min2 = (λarr. do { let h = source_node arr; ASSERT (h ≠ None); ASSERT (the h ∈# fst arr); let j = hp_read_child' (the h) arr; if j = None then RETURN (the h, (update_source_node None arr)) else do { ASSERT (the j ∈# fst arr); let arr = hp_update_prev' (the h) None arr; let arr = hp_update_child' (the h) None arr; let arr = hp_update_parents' (the j) None arr; arr ← merge_pairs (update_source_node None arr) (the j); RETURN (the h, arr) } })› (is ‹?A = ?B›) proof - have [simp]: ‹source_node arr = None ⟹ (fst arr, fst (snd arr), None) = arr› for arr by (cases arr) auto have K[refine]: ‹((the (source_node arr), fst arr, fst (snd arr), None), the (source_node arr), update_source_node None arr) ∈ Id› ‹((the (source_node arr), fst arr, fst (snd arr), None), the (source_node arr), update_source_node None arr) ∈ Id› ‹((the (source_node arr), update_source_node None arr), the (source_node arr), fst arr, fst (snd arr), None) ∈ Id› for i arr by (solves ‹cases arr; auto›)+ have [refine]: ‹merge_pairs (fst arr, hp_update_parents (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) None (hp_update_child (the (source_node arr)) None (hp_update_prev (the (source_node arr)) None (fst (snd arr)))), None) (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) ≤ ⇓ Id (merge_pairs (update_source_node None (hp_update_parents' (the (hp_read_child' (the (source_node arr)) arr)) None (hp_update_child' (the (source_node arr)) None (hp_update_prev' (the (source_node arr)) None arr)))) (the (hp_read_child' (the (source_node arr)) arr)))› ‹merge_pairs (update_source_node None (hp_update_parents' (the (hp_read_child' (the (source_node arr)) arr)) None (hp_update_child' (the (source_node arr)) None (hp_update_prev' (the (source_node arr)) None arr)))) (the (hp_read_child' (the (source_node arr)) arr)) ≤ ⇓ Id (merge_pairs (fst arr, hp_update_parents (the (hp_read_child (the (source_node arr)) (fst (snd arr)))) None (hp_update_child (the (source_node arr)) None (hp_update_prev (the (source_node arr)) None (fst (snd arr)))), None) (the (hp_read_child (the (source_node arr)) (fst (snd arr)))))› for arr by (solves ‹cases arr; auto›)+ have K: ‹snd (snd arr) = source_node arr› for arr by (cases arr) auto have ‹?A arr ≤ ⇓Id (?B arr)› for i arr unfolding vsids_pop_min2_def case_prod_beta[of _ arr] case_prod_beta[of _ ‹snd arr›] Let_def K by refine_vcg (solves auto)+ moreover have ‹?B arr ≤ ⇓Id (?A arr)› for i arr unfolding vsids_pop_min2_def case_prod_beta[of _ arr] case_prod_beta[of _ ‹snd arr›] K by refine_vcg (solves ‹auto intro!: ext bind_cong[OF refl] simp: Let_def›)+ ultimately show ?thesis unfolding Down_id_eq apply - apply (intro ext) apply (rule antisym) apply assumption+ done qed lemma mop_vsids_pop_min2_impl: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› shows ‹mop_vsids_pop_min2_impl xs ≤ ⇓(nat_rel ×_r ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (vsids_pop_min2 ys)› proof - let ?R = ‹{((arr, j, n), (arr', j', n', _)). (arr, arr') ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel ∧ (j, j') ∈ ⟨nat_rel⟩option_rel ∧ (n,n')∈Id}› have K[refine0]: ‹(the (source_node_impl xs), the (source_node ys)) ∈ nat_rel› if ‹source_node ys ≠ None› using source_node_spec[OF assms] by auto show ?thesis using assms source_node_spec[OF assms] unfolding mop_vsids_pop_min2_impl_def vsids_pop_min2_alt_def apply (refine_vcg mop_hp_insert_impl_spec WHILET_refine[where R= ?R] mop_hp_read_nxt_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_read_prev_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_link_imp_spec mop_vsids_pass₁_imp_spec mop_merge_pairs_imp_spec mop_hp_read_child_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_prev'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_child'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›] mop_hp_update_parent'_imp_spec[where R=‹⟨nat_rel⟩option_rel› and S=‹⟨nat_rel⟩option_rel›]) subgoal by auto subgoal by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro!: update_source_node_impl_spec) subgoal by auto subgoal by auto done qed definition mop_unroot_hp_tree where ‹mop_unroot_hp_tree arr h = do { let a = source_node_impl arr; nnext ← mop_hp_read_nxt_imp h arr; parent ← mop_hp_read_parent_imp h arr; prev ← mop_hp_read_prev_imp h arr; if prev = None ∧ parent = None ∧ Some h ≠ a then RETURN (update_source_node_impl None arr) else if Some h = a then RETURN (update_source_node_impl None arr) else do { ASSERT (a ≠ None); let a' = the a; arr ← maybe_mop_hp_update_child'_imp parent nnext arr; arr ← maybe_mop_hp_update_nxt'_imp prev nnext arr; arr ← maybe_mop_hp_update_prev'_imp nnext prev arr; arr ← maybe_mop_hp_update_parent'_imp nnext parent arr; arr ← mop_hp_update_nxt'_imp h None arr; arr ← mop_hp_update_prev'_imp h None arr; arr ← mop_hp_update_parent'_imp h None arr; arr ← mop_hp_update_nxt'_imp h (Some a') arr; arr ← mop_hp_update_prev'_imp a' (Some h) arr; RETURN (update_source_node_impl None arr) } }› lemma mop_unroot_hp_tree_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› and ‹(h,i)∈nat_rel› shows ‹mop_unroot_hp_tree xs h ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (unroot_hp_tree ys i)› proof - show ?thesis using assms using source_node_spec[OF assms(1)] unfolding mop_unroot_hp_tree_def unroot_hp_tree_def apply (refine_rcg mop_hp_read_nxt_imp_spec assms mop_hp_read_parent_imp_spec mop_hp_read_prev_imp_spec update_source_node_impl_spec maybe_mop_hp_update_child'_imp_spec maybe_mop_hp_update_nxt'_imp_spec maybe_mop_hp_update_parent'_imp_spec maybe_mop_hp_update_prev'_imp_spec mop_hp_update_nxt'_imp_spec[where S=‹⟨nat_rel⟩option_rel›] mop_hp_update_prev'_imp_spec[where S=‹⟨nat_rel⟩option_rel›] mop_hp_update_parent'_imp_spec[where S=‹⟨nat_rel⟩option_rel›]) subgoal using source_node_spec[OF assms(1)] by auto subgoal by auto subgoal using source_node_spec[OF assms(1)] by auto subgoal by auto subgoal using source_node_spec[OF assms(1)] by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto apply assumption subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition mop_rescale_and_reroot where ‹mop_rescale_and_reroot h w' arr = do { nnext ← mop_hp_read_nxt_imp h arr; parent ← mop_hp_read_parent_imp h arr; prev ← mop_hp_read_prev_imp h arr; if source_node_impl arr = None then mop_hp_update_score_imp h w' arr else if prev = None ∧ parent = None ∧ Some h ≠ source_node_impl arr then mop_hp_update_score_imp h w' arr else if Some h = source_node_impl arr then mop_hp_update_score_imp h w' arr else do { arr ← mop_unroot_hp_tree arr h; arr ← mop_hp_update_score_imp h w' arr; mop_merge_pairs_imp arr h } }› lemma mop_rescale_and_reroot_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› and ‹(h,i)∈nat_rel› ‹(w, w') ∈ nat_rel› shows ‹mop_rescale_and_reroot h w xs ≤ ⇓(⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel) (rescale_and_reroot i w' ys)› proof - have [refine]: ‹(Some w, Some w') ∈ ⟨nat_rel⟩option_rel› using assms by auto show ?thesis using source_node_spec[OF assms(1)] assms(2,3) unfolding rescale_and_reroot_def mop_rescale_and_reroot_def apply (refine_rcg mop_hp_read_nxt_imp_spec assms mop_hp_read_parent_imp_spec mop_hp_read_prev_imp_spec mop_hp_update_score_imp_spec mop_unroot_hp_tree_spec mop_merge_pairs_imp_spec) subgoal by auto subgoal by auto subgoal by auto apply assumption subgoal by auto done qed definition mop_hp_is_in :: ‹_› where ‹mop_hp_is_in h = (λarr. do { parent ← mop_hp_read_parent_imp h arr; prev ← mop_hp_read_prev_imp h arr; let s = source_node_impl arr; RETURN (s ≠ None ∧ (prev ≠ None ∨ parent ≠ None ∨ the s = h)) })› lemma mop_hp_is_in_spec: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› and ‹(h,i)∈nat_rel› shows ‹mop_hp_is_in h xs ≤ ⇓bool_rel (hp_is_in i ys)› proof - have hp_is_in_alt_def: ‹hp_is_in w = (λbw. do { ASSERT (w ∈# fst bw); let parent = hp_read_parent' w bw; let prev = hp_read_prev' w bw; let s = source_node bw; RETURN (s ≠ None ∧ (hp_read_prev' w bw ≠ None ∨ hp_read_parent' w bw ≠ None ∨ the s = w)) })› for w by (auto simp: hp_is_in_def) show ?thesis using source_node_spec[OF assms(1)] assms(2) unfolding mop_hp_is_in_def hp_is_in_alt_def by (refine_vcg assms mop_hp_read_parent_imp_spec mop_hp_read_prev_imp_spec) auto qed lemma mop_hp_read_score_imp_mop_hp_read_score: assumes ‹(xs, ys) ∈ ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel› and ‹(h,i)∈nat_rel› shows ‹mop_hp_read_score_imp h xs ≤ ⇓nat_rel (mop_hp_read_score i ys)› unfolding mop_hp_read_score_def case_prod_beta mop_hp_read_score_imp_def apply (refine_vcg mop_hp_read_score_imp_spec) using assms apply (auto simp: pairing_heaps_rel_def map_fun_rel_def dest!: multi_member_split) done end end

Theory Pairing_Heap_LLVM.Pairing_Heaps_Impl