Theory Pairing_Heap_LLVM.Relational_Pairing

theory Relational_Pairing_Heaps imports Pairing_Heaps begin subsection ‹Flat Version of Pairing Heaps› subsubsection ‹Splitting genealogy to Relations› text ‹In this subsection, we replace the tree version by several arrays that represent the relations (parent, child, next, previous) of the same trees.› (*TODO: this is missing the parents*) type_synonym ('a, 'b) hp_fun = ‹(('a ⇒ 'a option) × ('a ⇒ 'a option) × ('a ⇒ 'a option) × ('a ⇒ 'a option) × ('a ⇒ 'b option))› definition hp_set_all :: ‹'a ⇒ 'a option ⇒ 'a option ⇒ 'a option ⇒ 'a option ⇒ 'b option ⇒ ('a, 'b) hp_fun ⇒ ('a, 'b) hp_fun › where ‹hp_set_all i prev nxt child par sc = (λ(prevs, nxts, childs, parents, scores). (prevs(i:=prev), nxts(i:=nxt), childs(i:=child), parents(i:=par), scores(i:=sc)))› definition hp_update_prev :: ‹'a ⇒ 'a option ⇒ ('a, 'b) hp_fun ⇒ ('a, 'b) hp_fun› where ‹hp_update_prev i prev = (λ(prevs, nxts, childs, parents, score). (prevs(i:=prev), nxts, childs, parents, score))› definition hp_update_nxt :: ‹'a ⇒ 'a option ⇒ ('a, 'b) hp_fun ⇒ ('a, 'b) hp_fun› where ‹hp_update_nxt i nxt = (λ(prevs, nxts, childs, parents, score). (prevs, nxts(i:=nxt), childs, parents, score))› definition hp_update_parents :: ‹'a ⇒ 'a option ⇒ ('a, 'b) hp_fun ⇒ ('a, 'b) hp_fun› where ‹hp_update_parents i nxt = (λ(prevs, nxts, childs, parents, score). (prevs, nxts, childs, parents(i:=nxt), score))› definition hp_update_score :: ‹'a ⇒ 'b option ⇒ ('a, 'b) hp_fun ⇒ ('a, 'b) hp_fun› where ‹hp_update_score i nxt = (λ(prevs, nxts, childs, parents, score). (prevs, nxts, childs, parents, score(i:=nxt)))› fun hp_read_nxt :: ‹_ ⇒ ('a, 'b) hp_fun ⇒ _› where ‹hp_read_nxt i (prevs, nxts, childs) = nxts i› fun hp_read_prev :: ‹_ ⇒ ('a, 'b) hp_fun ⇒ _› where ‹hp_read_prev i (prevs, nxts, childs) = prevs i› fun hp_read_child :: ‹_ ⇒ ('a, 'b) hp_fun ⇒ _› where ‹hp_read_child i (prevs, nxts, childs, parents, scores) = childs i› fun hp_read_parent :: ‹_ ⇒ ('a, 'b) hp_fun ⇒ _› where ‹hp_read_parent i (prevs, nxts, childs, parents, scores) = parents i› fun hp_read_score :: ‹_ ⇒ ('a, 'b) hp_fun ⇒ _› where ‹hp_read_score i (prevs, nxts, childs, parents, scores) = scores i› text ‹ It was not entirely clear from the ground up whether we would actually need to have the conditions of emptyness of the previous or the parent. However, these are the only conditions to know whether a node is in the treen or not, so we decided to include them. It is critical to not add that the scores are empty, because this is the only way to track the scores after removing a node. We initially inlined the definition of term‹empty_outside›, but the simplifier immediatly hung himself. › definition empty_outside :: ‹_› where ‹empty_outside 𝒱 prevs = (∀x. x ∉# 𝒱 ⟶ prevs x = None)› definition encoded_hp_prop :: ‹'e multiset ⇒ ('e,'f) hp multiset ⇒ ('e, 'f) hp_fun ⇒ _› where ‹encoded_hp_prop 𝒱 m = (λ(prevs,nxts,children, parents, scores). distinct_mset (∑_# (mset_nodes `# m)) ∧ set_mset (∑_# (mset_nodes `# m)) ⊆ set_mset 𝒱 ∧ (∀m∈# m. ∀x ∈# mset_nodes m. prevs x = map_option node (hp_prev x m)) ∧ (∀m'∈#m. ∀x ∈# mset_nodes m'. nxts x = map_option node (hp_next x m')) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. children x = map_option node (hp_child x m)) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. parents x = map_option node (hp_parent x m)) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. scores x = map_option score (hp_node x m)) ∧ empty_outside (∑_# (mset_nodes `# m)) prevs ∧ empty_outside (∑_# (mset_nodes `# m)) parents)› lemma empty_outside_alt_def: ‹empty_outside 𝒱 f = (dom f ∩ UNIV - set_mset 𝒱 = {})› unfolding empty_outside_def by auto lemma empty_outside_add_mset[simp]: ‹f v = None ⟹ empty_outside (add_mset v 𝒱) f ⟷ empty_outside 𝒱 f› unfolding empty_outside_alt_def by auto lemma empty_outside_notin_None: ‹empty_outside 𝒱 prevs ⟹ a ∉# 𝒱 ⟹ prevs a = None› unfolding empty_outside_alt_def by auto lemma empty_outside_update_already_in[simp]: ‹x ∈# 𝒱 ⟹ empty_outside 𝒱 (prevs(x := a)) = empty_outside 𝒱 prevs› unfolding empty_outside_alt_def by auto lemma encoded_hp_prop_irrelevant: assumes ‹a ∉# ∑_# (mset_nodes `# m)› and ‹a∈#𝒱› and ‹encoded_hp_prop 𝒱 m (prevs, nxts, children, parents, scores)› shows ‹encoded_hp_prop 𝒱 (add_mset (Hp a sc []) m) (prevs, nxts(a:=None), children(a:=None), parents, scores(a:=Some sc))› using assms by (auto simp: encoded_hp_prop_def empty_outside_notin_None) lemma hp_parent_single_child[simp]: ‹hp_parent (node a) (Hp m w_m [a]) = Some (Hp m w_m [a])› by (cases a) (auto simp: hp_parent.simps(1)) lemma hp_parent_children_single_hp_parent[simp]: ‹hp_parent_children b [a] = hp_parent b a› by (auto simp: hp_parent_children_def) lemma hp_parent_single_child_If: ‹b ≠ m ⟹ hp_parent b (Hp m w_m (a # [])) = (if b = node a then Some (Hp m w_m [a]) else hp_parent b a)› by (auto simp: hp_parent_simps) lemma hp_parent_single_child_If2: ‹distinct_mset (add_mset m (mset_nodes a)) ⟹ hp_parent b (Hp m w_m (a # [])) = (if b = m then None else if b = node a then Some (Hp m w_m [a]) else hp_parent b a)› by (auto simp: hp_parent_simps) lemma hp_parent_single_child_If3: ‹distinct_mset (add_mset m (mset_nodes a + sum_list (map mset_nodes xs))) ⟹ hp_parent b (Hp m w_m (a # xs)) = (if b = m then None else if b = node a then Some (Hp m w_m (a # xs)) else hp_parent_children b (a # xs))› by (auto simp: hp_parent_simps) lemma hp_parent_is_first_child[simp]: ‹hp_parent (node a) (Hp m w_m (a # ch_m)) = Some (Hp m w_m (a # ch_m))› by (auto simp: hp_parent.simps(1)) lemma hp_parent_children_in_first_child[simp]: ‹distinct_mset (mset_nodes a + sum_list (map mset_nodes ch_m)) ⟹ xa ∈# mset_nodes a ⟹ hp_parent_children xa (a # ch_m) = hp_parent xa a› by (auto simp: hp_parent_children_cons split: option.splits dest: multi_member_split) lemma encoded_hp_prop_link: fixes ch_m a prevs parents m defines ‹prevs' ≡ (if ch_m = [] then prevs else prevs (node (hd ch_m) := Some (node a)))› defines ‹parents' ≡ (if ch_m = [] then parents else parents (node (hd ch_m) := None))› assumes ‹encoded_hp_prop 𝒱 (add_mset (Hp m w_m ch_m) (add_mset a x)) (prevs, nxts, children, parents, scores)› shows ‹encoded_hp_prop 𝒱 (add_mset (Hp m w_m (a # ch_m)) x) (prevs', nxts(node a:= if ch_m = [] then None else Some (node (hd ch_m))), children(m := Some (node a)), parents'(node a:= Some m), scores(m:=Some w_m))› proof - have H[simp]: ‹distinct_mset (sum_list (map mset_nodes ch_m) + (mset_nodes a))› ‹distinct_mset (mset_nodes a)› ‹distinct_mset (sum_list (map mset_nodes ch_m))› and dist: ‹distinct_mset (sum_list (map mset_nodes ch_m) + (mset_nodes a) + ∑_# (mset_nodes `# x))› ‹m ∉# sum_list (map mset_nodes ch_m) + (mset_nodes a) + ∑_# (mset_nodes `# x)› and incl: ‹set_mset (∑_# (mset_nodes `# add_mset (Hp m w_m ch_m) (add_mset a x))) ⊆ set_mset 𝒱› using assms unfolding encoded_hp_prop_def prod.simps apply auto by (metis distinct_mset_add mset_nodes_simps sum_mset.insert union_assoc)+ have [simp]: ‹distinct_mset (mset_nodes a + sum_list (map mset_nodes ch_m))› by (metis H(1) union_ac(2)) have 1: ‹ch_m ≠ [] ⟹ node a ≠ node (hd ch_m)› if ‹distinct_mset (sum_list (map mset_nodes ch_m) + (mset_nodes a + ∑_# (mset_nodes `# x)))› using that by (cases ch_m; cases a; auto) have K: ‹xa ∈# mset_nodes a ⟹ xa ∉# sum_list (map mset_nodes ch_m)› ‹xa ∈# sum_list (map mset_nodes ch_m) ⟹ xa ∉# mset_nodes a›for xa using H by (auto simp del: H dest!: multi_member_split) have [simp]: ‹ch_m ≠ [] ⟹ ma ∈# x ⟹ hp_parent (node (hd ch_m)) ma = None› ‹ma ∈# x ⟹ hp_parent (node a) ma = None› ‹ma ∈# x ⟹ node a ∉# mset_nodes ma› for ma by (cases ch_m; cases ‹hd ch_m›; cases a; use dist in ‹auto simp del: H dest!: multi_member_split›; fail)+ have [simp]: ‹xa ∈# sum_list (map mset_nodes ch_m) ⟹ xa ≠ node (hd ch_m) ⟹ (hp_parent xa (Hp m w_m ch_m)) = (hp_parent_children xa (a # ch_m))› for xa using dist H by (cases ch_m; cases x) (auto simp: hp_parent_single_child_If3 hp_parent_children_cons simp del: H dest!: multi_member_split split: option.splits) show ?thesis using assms 1 unfolding encoded_hp_prop_def prod.simps apply (intro conjI impI ballI) subgoal by (auto simp: ac_simps) subgoal by (auto simp: ac_simps) subgoal apply (auto simp: prevs'_def hp_prev_skip_hd_children dest: multi_member_split) by (metis add_mset_disjoint(1) distinct_mset_add image_msetI in_Union_mset_iff mset_add node_hd_in_sum union_iff) subgoal apply simp apply (intro conjI impI allI) subgoal by (auto dest!: multi_member_split simp: add_mset_eq_add_mset) subgoal by (auto dest: multi_member_split)[] subgoal by (auto dest!: multi_member_split)[] subgoal by (auto dest: multi_member_split distinct_mset_union simp: hp_next_skip_hd_children) done subgoal by (auto split: option.splits simp: K) subgoal by (auto simp: hp_parent_single_child_If2 hp_parent_single_child_If3) subgoal by (auto split: option.splits simp: K(2)) subgoal by (auto simp: ac_simps) subgoal by (auto simp: ac_simps) done qed fun find_first_not_none where ‹find_first_not_none (None # xs) = find_first_not_none xs› | ‹find_first_not_none (Some a # _) = Some a›| ‹find_first_not_none [] = None› lemma find_first_not_none_alt_def: ‹find_first_not_none xs = map_option the (option_hd (filter ((≠) None) xs))› by (induction xs rule: find_first_not_none.induct) auto text ‹In the following we distinguish between the tree part and the tree part without parent (aka the list part). The latter corresponds to a tree where we have removed the source, but the leafs remains in the correct form. They are different for first level nexts and first level children.› definition encoded_hp_prop_list :: ‹'e multiset ⇒ ('e,'f) hp multiset ⇒ ('e,'f) hp list ⇒ _› where ‹encoded_hp_prop_list 𝒱 m xs = (λ(prevs,nxts,children, parents, scores). distinct_mset (∑_# (mset_nodes `# m + mset_nodes `# (mset xs))) ∧ set_mset (∑_# (mset_nodes `# m + mset_nodes `# (mset xs))) ⊆ set_mset 𝒱 ∧ (∀m'∈#m. ∀x ∈# mset_nodes m'. nxts x = map_option node (hp_next x m')) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. prevs x = map_option node (hp_prev x m)) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. children x = map_option node (hp_child x m)) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. parents x = map_option node (hp_parent x m)) ∧ (∀m∈# m. ∀x ∈# mset_nodes m. scores x = map_option score (hp_node x m)) ∧ (∀x ∈# ∑_# (mset_nodes `# mset xs). nxts x = map_option node (hp_next_children x xs)) ∧ (∀x ∈# ∑_# (mset_nodes `# mset xs). prevs x = map_option node (hp_prev_children x xs)) ∧ (∀x ∈# ∑_# (mset_nodes `# mset xs). children x = map_option node (hp_child_children x xs)) ∧ (∀x ∈# ∑_# (mset_nodes `# mset xs). parents x = map_option node (hp_parent_children x xs)) ∧ (∀x ∈# ∑_# (mset_nodes `# mset xs). scores x = map_option score (hp_node_children x xs)) ∧ empty_outside (∑_# (mset_nodes `# m + mset_nodes `# (mset xs))) prevs ∧ empty_outside (∑_# (mset_nodes `# m + mset_nodes `# (mset xs))) parents) › lemma encoded_hp_prop_list_encoded_hp_prop[simp]: ‹encoded_hp_prop_list 𝒱 arr [] h = encoded_hp_prop 𝒱 arr h› unfolding encoded_hp_prop_list_def encoded_hp_prop_def by auto lemma encoded_hp_prop_list_encoded_hp_prop_single[simp]: ‹encoded_hp_prop_list 𝒱 {#} [arr] h = encoded_hp_prop 𝒱 {#arr#} h› unfolding encoded_hp_prop_list_def encoded_hp_prop_def by auto lemma empty_outside_set_none_outside[simp]: ‹empty_outside 𝒱 prevs ⟹ a ∉# 𝒱 ⟹ empty_outside 𝒱 (prevs(a := None))› unfolding empty_outside_alt_def by auto lemma encoded_hp_prop_list_remove_min: fixes parents a child children defines ‹parents' ≡ (if children a = None then parents else parents(the (children a) := None))› assumes ‹encoded_hp_prop_list 𝒱 (add_mset (Hp a b child) xs) [] (prevs, nxts, children, parents, scores)› shows ‹encoded_hp_prop_list 𝒱 xs child (prevs(a:=None), nxts, children(a:=None), parents', scores)› proof - have a: ‹children a = None ⟷ child = []› and b: ‹children a ≠ None ⟹ the (children a) = node (hd child)› using assms unfolding encoded_hp_prop_list_def by (cases child; auto simp: ac_simps hp_parent_single_child_If3 dest: multi_member_split; fail)+ have dist: ‹distinct_mset (∑_# (mset_nodes `# add_mset (Hp a b child) xs))› using assms unfolding encoded_hp_prop_list_def prod.simps by (metis empty_neutral(2) image_mset_empty mset_zero_iff) then have ‹child ≠ [] ⟹ distinct_mset (mset_nodes ((hd child)) + sum_list (map mset_nodes (tl child)))› ‹child ≠ [] ⟹ distinct_mset (mset_nodes ((hd child)))› using distinct_mset_union by (cases child; auto; fail)+ moreover have ‹parents a = None› using assms unfolding encoded_hp_prop_list_def a by (cases child) (auto simp: ac_simps hp_parent_single_child_If3 hp_parent_simps_if dest: multi_member_split) ultimately show ?thesis using assms b unfolding encoded_hp_prop_list_def a apply (cases child) apply (auto simp: ac_simps hp_parent_single_child_If3 hp_parent_simps_if dest: multi_member_split) apply (metis (no_types, lifting) disjunct_not_in distinct_mset_add insert_DiffM node_in_mset_nodes sum_mset.insert union_iff) apply (metis hp_node_None_notin2 option.case_eq_if option.exhaust_sel) apply (metis hp_node.simps(1) hp_node_children_simps2) apply (metis hp_child.simps(1) hp_child_hp_children_simps2) done qed lemma hp_parent_children_skip_first[simp]: ‹x ∈# sum_list (map mset_nodes ch') ⟹ distinct_mset (sum_list (map mset_nodes ch) + sum_list (map mset_nodes ch')) ⟹ hp_parent_children x (ch @ ch') = hp_parent_children x ch'› by (induction ch) (auto simp: hp_parent_children_cons dest!: multi_member_split) lemma hp_parent_children_skip_last[simp]: ‹x ∈# sum_list (map mset_nodes ch) ⟹ distinct_mset (sum_list (map mset_nodes ch) + sum_list (map mset_nodes ch')) ⟹ hp_parent_children x (ch @ ch') = hp_parent_children x ch› by (induction ch) (auto simp: hp_parent_children_cons dest!: multi_member_split split: option.splits) lemma hp_parent_first_child[simp]: ‹n ≠ m ⟹ hp_parent n (Hp m w_m (Hp n w_n ch_n # ch_m)) = Some (Hp m w_m (Hp n w_n ch_n # ch_m))› by (auto simp: hp_parent.simps(1)) lemma encoded_hp_prop_list_link: fixes m ch_m prevs b hp_m n nxts children parents defines ‹prevs₀ ≡ (if ch_m = [] then prevs else prevs (node (hd ch_m) := Some n))› defines ‹prevs' ≡ (if b = [] then prevs₀ else prevs₀ (node (hd b) := Some m)) (n:= None)› defines ‹nxts' ≡ nxts (m := map_option node (option_hd b), n := map_option node (option_hd ch_m))› defines ‹children' ≡ children (m := Some n)› defines ‹parents' ≡ (if ch_m = [] then parents else parents(node (hd ch_m) := None))(n := Some m)› assumes ‹encoded_hp_prop_list 𝒱 (xs) (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b) (prevs, nxts, children, parents, scores)› shows ‹encoded_hp_prop_list 𝒱 xs (a @ [Hp m w_m (Hp n w_n ch_n # ch_m)] @ b) (prevs', nxts', children', parents', scores)› proof - have dist: ‹distinct_mset (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + (∑_# (mset_nodes `# xs) + (sum_list (map mset_nodes a) + sum_list (map mset_nodes b)))))› and notin: ‹n ∉# sum_list (map mset_nodes ch_m)› ‹n ∉# sum_list (map mset_nodes ch_n)› ‹n ∉# sum_list (map mset_nodes a)› ‹n ∉# sum_list (map mset_nodes b)› ‹m ∉# sum_list (map mset_nodes ch_m)› ‹m ∉# sum_list (map mset_nodes ch_n)› ‹m ∉# sum_list (map mset_nodes a)› ‹m ∉# sum_list (map mset_nodes b)› ‹n ≠ m› ‹m ≠ n› and nxts1: ‹(∀m'∈#xs. ∀x∈#mset_nodes m'. nxts x = map_option node (hp_next x m'))› and prevs1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. prevs x = map_option node (hp_prev x m))› and parents1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. parents x = map_option node (hp_parent x m))› and child1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. children x = map_option node (hp_child x m))› and scores1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. scores x = map_option score (hp_node x m))› and nxts2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). nxts x = map_option node (hp_next_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and prevs2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). prevs x = map_option node (hp_prev_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and parents2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). parents x = map_option node (hp_parent_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and child2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). children x = map_option node (hp_child_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and scores2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). scores x = map_option score (hp_node_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and dist2: ‹distinct_mset (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and others_empty: ‹empty_outside (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) prevs› ‹empty_outside (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) parents› and incl: ‹set_mset (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) ⊆ set_mset 𝒱› using assms unfolding encoded_hp_prop_list_def by auto have [simp]: ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b) + sum_list (map mset_nodes ch_m))› "distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))" ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m)))› ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_n))› ‹distinct_mset (sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes a)))› "distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b))" ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n)))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b)))› using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis distinct_mset_add union_ac(3)) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 group_cancel.add1 group_cancel.add2) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 group_cancel.add1 group_cancel.add2) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) done have [simp]: ‹m ≠ node (hd ch_m)› ‹n ≠ node (hd ch_m)› ‹(node (hd ch_m)) ∉# sum_list (map mset_nodes b)› ‹node (hd ch_m) ∉# sum_list (map mset_nodes ch_n)›if ‹ch_m ≠ []› using dist that notin by (cases ch_m; auto dest: multi_member_split; fail)+ have [simp]: ‹m ≠ node (hd b)› ‹n ≠ node (hd b)› if ‹b ≠ []› using dist that notin unfolding encoded_hp_prop_list_def by (cases b; auto; fail)+ have [simp]: ‹ma ∈# xs ⟹ node (hd ch_m) ∉# mset_nodes ma› if ‹ch_m ≠ []› for ma using dist that notin by (cases ch_m; auto dest!: multi_member_split; fail)+ have [simp]: ‹hp_parent_children (node (hd ch_m)) ch_m = None› by (metis ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_m))› distinct_mset_add hp_parent.simps(2) hp_parent_None_iff_children_None hp_parent_children_hd_None sum_image_mset_sum_map) define NOTIN where ‹NOTIN x ch_n ≡ x ∉# sum_list (map mset_nodes ch_n)› for x and ch_n :: ‹('a, 'b) hp list› have K[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes a)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes b)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes ch_m)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ ¬x ∉# sum_list (map mset_nodes ch_n)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ≠ n› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ NOTIN x a› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ NOTIN x b› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ≠ n› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ∉# sum_list (map mset_nodes ch_n)› and K'[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes ch_m)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes ch_n)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes b)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ≠ n› and K''[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes b) ⟹ (x ∉# sum_list (map mset_nodes a))› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ∉# sum_list (map mset_nodes ch_n)› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ≠ n› for x using dist notin by (auto dest!: multi_member_split simp: NOTIN_def) note [simp] = NOTIN_def[symmetric] show ?thesis using dist2 unfolding encoded_hp_prop_list_def prod.simps assms(1-5) apply (intro conjI impI allI) subgoal using assms unfolding encoded_hp_prop_list_def by (auto simp: ac_simps simp del: NOTIN_def[symmetric]) subgoal using incl by auto subgoal using nxts1 by auto subgoal using prevs1 apply (cases ch_m; cases b) apply (auto) apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mem_diff_mset mset_add node_in_mset_nodes sum_mset.insert union_iff) apply (metis (no_types, lifting) add_mset_disjoint(1) distinct_mset_add mset_add node_in_mset_nodes sum_mset.insert union_iff)+ done subgoal using child1 by auto subgoal using parents1 by auto subgoal using scores1 by auto subgoal using nxts2 by (auto dest: multi_member_split simp: K hp_next_children_append_single_remove_children) subgoal using prevs2 supply [cong del] = image_mset_cong by (auto simp add: K K' K'' hp_prev_children_append_single_remove_children hp_prev_skip_hd_children map_option_skip_in_child) subgoal using child2 notin(9) by (auto simp add: K K' K'' hp_child_children_skip_first[of _ ‹[_]›, simplified] hp_child_children_skip_first[of _ ‹_ # _›, simplified] hp_child_children_skip_last[of _ _ ‹[_]›, simplified] hp_child_children_skip_last[of _ ‹[_]›, simplified] notin hp_child_children_skip_last[of _ ‹[_, _]›, simplified] hp_child_children_skip_first[of _ _ ‹[_]›, simplified] split: option.splits) subgoal using parents2 notin(9) by (auto simp add: K K' K'' hp_parent_children_skip_first[of _ ‹[_]›, simplified] hp_parent_children_skip_first[of _ ‹_ # _›, simplified] hp_parent_simps_single_if hp_parent_children_skip_last[of _ _ ‹[_]›, simplified] hp_parent_children_skip_last[of _ ‹[_]›, simplified] notin hp_parent_children_skip_last[of _ ‹[_, _]›, simplified] hp_parent_children_skip_first[of _ _ ‹[_]›, simplified] split: option.splits) subgoal using scores2 by (auto split: option.splits simp: K K' K'' hp_node_children_Cons_if ex_hp_node_children_Some_in_mset_nodes dest: multi_member_split) subgoal using others_empty by (auto simp add: K K' K'' ac_simps) subgoal using others_empty by (auto simp add: K K' K'' ac_simps) done qed lemma encoded_hp_prop_list_link2: fixes m ch_m prevs b hp_m n nxts children ch_n a parents defines ‹prevs' ≡ (if ch_n = [] then prevs else prevs (node (hd ch_n) := Some m))(m := None, n := map_option node (option_last a))› defines ‹nxts₀ ≡ (if a = [] then nxts else nxts(node (last a) := Some n))› defines ‹nxts' ≡ nxts₀ (n := map_option node (option_hd b), m := map_option node (option_hd ch_n))› defines ‹children' ≡ children (n := Some m)› defines ‹parents' ≡ (if ch_n = [] then parents else parents(node (hd ch_n) := None))(m := Some n)› assumes ‹encoded_hp_prop_list 𝒱 (xs) (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b) (prevs, nxts, children, parents, scores)› shows ‹encoded_hp_prop_list 𝒱 xs (a @ [Hp n w_n (Hp m w_m ch_m # ch_n)] @ b) (prevs', nxts', children', parents', scores)› proof - have dist: ‹distinct_mset (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + (∑_# (mset_nodes `# xs) + (sum_list (map mset_nodes a) + sum_list (map mset_nodes b)))))› and notin: ‹n ∉# sum_list (map mset_nodes ch_m)› ‹n ∉# sum_list (map mset_nodes ch_n)› ‹n ∉# sum_list (map mset_nodes a)› ‹n ∉# sum_list (map mset_nodes b)› ‹m ∉# sum_list (map mset_nodes ch_m)› ‹m ∉# sum_list (map mset_nodes ch_n)› ‹m ∉# sum_list (map mset_nodes a)› ‹m ∉# sum_list (map mset_nodes b)› ‹n ≠ m› ‹m ≠ n› and nxts1: ‹(∀m'∈#xs. ∀x∈#mset_nodes m'. nxts x = map_option node (hp_next x m'))› and prevs1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. prevs x = map_option node (hp_prev x m))› and child1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. children x = map_option node (hp_child x m))› and parent1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. parents x = map_option node (hp_parent x m))› and nxts2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). nxts x = map_option node (hp_next_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and prevs2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). prevs x = map_option node (hp_prev_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and child2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). children x = map_option node (hp_child_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and parent2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). parents x = map_option node (hp_parent_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and scores2: ‹(∀x∈#∑_# (mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)). scores x = map_option score (hp_node_children x (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and scores1: ‹(∀m∈#xs. ∀x∈#mset_nodes m. scores x = map_option score (hp_node x m))› and dist2: ‹distinct_mset (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b)))› and others_empty: ‹empty_outside (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) prevs› ‹empty_outside (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) parents› and incl: ‹set_mset (∑_# (mset_nodes `# xs + mset_nodes `# mset (a @ [Hp m w_m ch_m, Hp n w_n ch_n] @ b))) ⊆ set_mset 𝒱› using assms unfolding encoded_hp_prop_list_def prod.simps by clarsimp_all have [simp]: ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m)))› ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_n))› ‹distinct_mset (sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes ch_m))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + (sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes a)))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n)))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes ch_n) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes b) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n))))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes ch_n) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes a))› ‹distinct_mset (sum_list (map mset_nodes a) + (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b)))› ‹distinct_mset (sum_list (map mset_nodes ch_m) + sum_list (map mset_nodes b))› using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis distinct_mset_add union_ac(3)) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 group_cancel.add1 group_cancel.add2) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 group_cancel.add1 group_cancel.add2) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 union_commute union_lcomm) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 union_commute union_lcomm) using dist apply (smt (verit, del_insts) WB_List_More.distinct_mset_union2 union_commute union_lcomm) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) using dist apply (metis (no_types, lifting) distinct_mset_add union_assoc union_commute) done have [simp]: ‹m ≠ node (hd ch_m)› ‹n ≠ node (hd ch_m)› ‹(node (hd ch_m)) ∉# sum_list (map mset_nodes b)› ‹node (hd ch_m) ∉# sum_list (map mset_nodes ch_n)›if ‹ch_m ≠ []› using dist that notin by (cases ch_m; auto dest: multi_member_split; fail)+ have [simp]: ‹m ≠ node (hd ch_n)› ‹n ≠ node (hd ch_n)› ‹(node (hd ch_n)) ∉# sum_list (map mset_nodes b)› ‹node (hd ch_n) ∉# sum_list (map mset_nodes ch_m)›if ‹ch_n ≠ []› using dist that notin by (cases ch_n; auto dest: multi_member_split; fail)+ have [simp]: ‹m ≠ node (hd b)› ‹n ≠ node (hd b)› if ‹b ≠ []› using dist that notin unfolding encoded_hp_prop_list_def by (cases b; auto; fail)+ define NOTIN where ‹NOTIN x ch_n ≡ x ∉# sum_list (map mset_nodes ch_n)› for x and ch_n :: ‹('a, 'b) hp list› have K[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes a)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes b)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ∉# sum_list (map mset_nodes ch_m)› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes ch_n) ⟹ x ≠ n› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ NOTIN x a› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ NOTIN x b› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ≠ n› ‹x ∈# sum_list (map mset_nodes ch_m) ⟹ x ∉# sum_list (map mset_nodes ch_n)› and K'[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes ch_m)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes ch_n)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ∉# sum_list (map mset_nodes b)› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes a) ⟹ x ≠ n› and K''[unfolded NOTIN_def[symmetric]]: ‹x ∈# sum_list (map mset_nodes b) ⟹ (x ∉# sum_list (map mset_nodes a))› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ∉# sum_list (map mset_nodes ch_n)› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ∉# sum_list (map mset_nodes ch_m)› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ≠ m› ‹x ∈# sum_list (map mset_nodes b) ⟹ x ≠ n› for x using dist notin by (auto dest!: multi_member_split simp: NOTIN_def) have [simp]: ‹node (last a) ∉# sum_list (map mset_nodes ch_m)› ‹node (last a) ∉# sum_list (map mset_nodes ch_n)› if ‹a ≠ []› using that dist by (cases a rule: rev_cases; cases ‹last a›; auto; fail)+ note [simp] = NOTIN_def[symmetric] have [simp]: ‹hp_parent_children (node (hd ch_m)) ch_m = None› by (metis ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes ch_m))› distinct_mset_add hp_parent.simps(2) hp_parent_None_iff_children_None hp_parent_children_hd_None sum_image_mset_sum_map) have [simp]: ‹ch_n ≠ [] ⟹ hp_parent_children (node (hd ch_n)) ch_n = None› using dist by (cases ch_n; cases ‹hd ch_n›) (auto simp: hp_parent_children_cons distinct_mset_add split: option.splits) have [iff]: ‹ch_n ≠ [] ⟹ ma ∈# xs ⟹ node (hd ch_n) ∈# mset_nodes ma ⟷ False› for ma using dist2 apply auto by (metis (no_types, lifting) add_mset_disjoint(1) distinct_mset_add insert_DiffM inter_mset_empty_distrib_right node_hd_in_sum sum_mset.insert) show ?thesis using dist2 unfolding encoded_hp_prop_list_def prod.simps assms(1-5) apply (intro conjI impI allI) subgoal using assms unfolding encoded_hp_prop_list_def by (auto simp: ac_simps simp del: NOTIN_def[symmetric]) subgoal using incl by auto subgoal using nxts1 apply (cases a rule: rev_cases) apply auto by (metis (no_types, lifting) add_diff_cancel_right' distinct_mset_in_diff mset_add node_in_mset_nodes sum_mset.insert union_iff) subgoal using prevs1 by auto subgoal using child1 by auto subgoal using parent1 by auto subgoal using scores1 by auto subgoal using nxts2 by (auto dest: multi_member_split simp: K hp_next_children_append_single_remove_children hp_next_children_skip_last_not_last notin) subgoal using prevs2 supply [cong del] = image_mset_cong by (auto simp add: K K' K'' hp_prev_children_append_single_remove_children hp_prev_skip_hd_children map_option_skip_in_child hp_prev_children_skip_first_append[of _ ‹[_]›, simplified]) subgoal using child2 by (auto simp add: K K' K'' hp_child_children_skip_first[of _ ‹[_]›, simplified] hp_child_children_skip_first[of _ ‹_ # _›, simplified] hp_child_children_skip_last[of _ _ ‹[_]›, simplified] hp_child_children_skip_last[of _ ‹[_]›, simplified] notin hp_child_children_skip_last[of _ ‹[_, _]›, simplified] hp_child_children_skip_first[of _ _ ‹[_,_]›, simplified] hp_child_children_skip_first[of _ _ ‹[_]›, simplified] split: option.splits) subgoal using parent2 notin(9) by (auto simp add: K K' K'' hp_parent_children_skip_first[of _ ‹[_]›, simplified] hp_parent_children_skip_first[of _ ‹_ # _›, simplified] hp_parent_simps_single_if hp_parent_children_skip_last[of _ _ ‹[_]›, simplified] hp_parent_children_skip_last[of _ ‹[_]›, simplified] notin hp_parent_children_skip_last[of _ ‹[_, _]›, simplified] hp_parent_children_skip_first[of _ _ ‹[_]›, simplified] hp_parent_children_skip_first[of _ _ ‹[_,_]›, simplified] eq_commute[of n ‹node (hd [])›] split: option.splits) subgoal using scores2 by (auto split: option.splits simp: K K' K'' hp_node_children_Cons_if ex_hp_node_children_Some_in_mset_nodes dest: multi_member_split) subgoal using others_empty by (auto simp add: K K' K'' ac_simps add_mset_commute[of m n]) subgoal using others_empty by (auto simp add: K K' K'' ac_simps add_mset_commute[of m n]) done qed definition encoded_hp_prop_list_conc :: "'a::linorder multiset × ('a, 'b) hp_fun × 'a option ⇒ 'a multiset × ('a, 'b) hp option ⇒ bool" where ‹encoded_hp_prop_list_conc = (λ(𝒱, arr, h) (𝒱', x). 𝒱 = 𝒱' ∧ (case x of None ⇒ encoded_hp_prop_list 𝒱' {#} ([]:: ('a, 'b) hp list) arr ∧ h = None | Some x ⇒ encoded_hp_prop_list 𝒱' {#x#} [] arr ∧ set_mset (mset_nodes x) ⊆ set_mset 𝒱 ∧ h = Some (node x)))› lemma encoded_hp_prop_list_conc_alt_def: ‹encoded_hp_prop_list_conc = (λ(𝒱, arr, h) (𝒱', x). 𝒱 = 𝒱' ∧ (case x of None ⇒ encoded_hp_prop_list 𝒱' {#} ([]:: ('a::linorder, 'b) hp list) arr ∧ h = None | Some x ⇒ encoded_hp_prop_list 𝒱' {#x#} [] arr ∧ h = Some (node x)))› unfolding encoded_hp_prop_list_conc_def encoded_hp_prop_list_def by (auto split: option.splits intro!: ext) definition encoded_hp_prop_list2_conc :: "'a::linorder multiset × ('a, 'b) hp_fun × 'a option ⇒ 'a multiset × ('a, 'b) hp list ⇒ bool" where ‹encoded_hp_prop_list2_conc = (λ(𝒱, arr, h) (𝒱', x). 𝒱' = 𝒱 ∧ (encoded_hp_prop_list 𝒱 {#} x arr ∧ set_mset (sum_list (map mset_nodes x)) ⊆ set_mset 𝒱 ∧ h = None))› lemma encoded_hp_prop_list2_conc_alt_def: ‹encoded_hp_prop_list2_conc = (λ(𝒱, arr, h) (𝒱', x). 𝒱 = 𝒱' ∧ (encoded_hp_prop_list 𝒱 {#} x arr ∧ h = None))› unfolding encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def by (auto split: option.splits intro!: ext) lemma encoded_hp_prop_list_update_score: fixes h :: ‹('a, nat) hp› and a arr and hs :: ‹('a, nat) hp multiset› and x defines arr': ‹arr' ≡ hp_update_score a (Some x) arr› assumes enc: ‹encoded_hp_prop_list 𝒱 (add_mset (Hp a b c) hs) [] arr› shows ‹encoded_hp_prop_list 𝒱 (add_mset (Hp a x c) hs) [] arr'› proof - obtain prevs nxts childs parents scores 𝒱 where arr: ‹arr = ((prevs, nxts, childs, parents, scores))› and dist: ‹distinct_mset (sum_list (map mset_nodes c) + ∑_# (mset_nodes `# hs))› ‹a ∉# sum_list (map mset_nodes c)› ‹a ∉# ∑_# (mset_nodes `# hs)› and 𝒱: ‹set_mset (sum_list (map mset_nodes xs)) ⊆ 𝒱› by (cases arr) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) have find_key_in_nodes: ‹find_key a h ≠ None ⟹ node (the (find_key a h)) ∈# mset_nodes h› by (cases ‹a ∈# mset_nodes h›) (use find_key_None_or_itself[of a h] in ‹auto simp del: find_key_None_or_itself›) have in_find_key_in_nodes1: ‹x ∈# mset_nodes y ⟹ find_key a h = Some y ⟹ x ∈# mset_nodes h› for x y using mset_nodes_find_key_subset[of a h] by auto have [simp]: ‹find_key a h = None ⟹ remove_key a h = Some h› by (metis find_key.simps find_key_none_iff hp.exhaust_sel hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps2 option_last_Nil option_last_Some_iff(2) remove_key_notin_unchanged) have [simp]: ‹map_option node (hp_parent xa (Hp a b c)) = map_option node (hp_parent xa (Hp a x c))› for xa by (cases c; auto simp: hp_parent.simps(1)) have ‹remove_key a h ≠ None ⟹ node (the (remove_key a h)) ∈# mset_nodes h› by (metis remove_key.simps get_min2.simps hp.exhaust_sel option.collapse option.distinct(2) remove_key_notin_unchanged) then show ?thesis supply [[goals_limit=1]] using enc unfolding arr hp_update_nxt_def hp_update_prev_def case_prod_beta encoded_hp_prop_list_def prod.simps arr' apply - apply (intro conjI impI ballI) subgoal by (auto simp: find_remove_mset_nodes_full) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal apply (auto simp: find_remove_mset_nodes_full hp_update_score_def) by (metis hp_child_hp_children_simps2) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) subgoal by (auto simp: find_remove_mset_nodes_full hp_update_score_def) done qed subsubsection ‹Refinement to Imperative version› definition hp_insert :: ‹'a ⇒ 'b::linorder ⇒ 'a multiset × ('a,'b) hp_fun × 'a option ⇒ ('a multiset × ('a,'b) hp_fun × 'a option) nres› where ‹hp_insert = (λ(i::'a) (w::'b) (𝒱::'a multiset, arr :: ('a, 'b) hp_fun, h :: 'a option). do { if h = None then do { ASSERT (i ∈# 𝒱); RETURN (𝒱, hp_set_all i None None None None (Some w) arr, Some i) } else do { ASSERT (i ∈# 𝒱); ASSERT (hp_read_prev i arr = None); ASSERT (hp_read_parent i arr = None); let (j::'a) = ((the h) :: 'a); ASSERT (j ∈# 𝒱 ∧ j ≠ i); ASSERT (hp_read_score j (arr :: ('a, 'b) hp_fun) ≠ 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)::'b); if y < w then do { let arr = hp_set_all i None None (Some j) None (Some (w::'b)) (arr::('a, 'b) hp_fun); let arr = hp_update_parents j (Some i) arr; let nxt = hp_read_nxt j arr; RETURN (𝒱, arr :: ('a, 'b) hp_fun, Some i) } else do { let child = hp_read_child j arr; ASSERT (child ≠ None ⟶ the child ∈# 𝒱); let arr = hp_set_all j None None (Some i) None (Some y) arr; let arr = hp_set_all i None child None (Some j) (Some (w::'b)) arr; let arr = (if child = None then arr else hp_update_prev (the child) (Some i) arr); let arr = (if child = None then arr else hp_update_parents (the child) None arr); RETURN (𝒱, arr :: ('a, 'b) hp_fun, h) } } })› lemma hp_insert_spec: assumes ‹encoded_hp_prop_list_conc arr h› and ‹snd h ≠ None ⟹ i ∉# mset_nodes (the (snd h))› and ‹i ∈# fst arr› shows ‹hp_insert i w arr ≤ ⇓ {(arr, h). encoded_hp_prop_list_conc arr h} (ACIDS.mop_hm_insert i w h)› proof - let ?h = ‹snd h› obtain prevs nxts childs scores parents 𝒱 where arr: ‹arr = (𝒱, (prevs, nxts, childs, parents, scores), map_option node ?h)› by (cases arr; cases ?h) (use assms in ‹auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) have enc: ‹encoded_hp_prop 𝒱 {#Hp i w [the ?h]#} (prevs, nxts(i := None, node (the ?h) := None), childs(i ↦ node (the ?h)), parents(node (the ?h) ↦ i), scores(i ↦ w))› and enc2: ‹encoded_hp_prop 𝒱 {#Hp (node (the ?h)) (score (the ?h)) (Hp i w [] # hps (the ?h))#} (if hps (the ?h) = [] then prevs else prevs(node (hd (hps (the ?h))) ↦ node (Hp i w [])), nxts (i := None, node (Hp i w []) := if hps (the ?h) = [] then None else Some (node (hd (hps (the ?h))))), childs(i := None)(node (the ?h) ↦ node (Hp i w [])), (if hps (the ?h) = [] then parents else parents(node (hd (hps (the ?h))) := None))(node (Hp i w []) ↦ node (the ?h)), scores(i ↦ w, node (the ?h) ↦ score (the ?h)))› (is ?G) if ‹?h ≠ None› proof - have ‹encoded_hp_prop 𝒱 {#the ?h#} (prevs, nxts, childs, parents, scores)› using that assms by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def encoded_hp_prop_def arr) then have 0: ‹encoded_hp_prop 𝒱 {#Hp i w [], the ?h#} (prevs, nxts(i := None), childs(i := None), parents, scores(i ↦ w))› using encoded_hp_prop_irrelevant[of i ‹{#the ?h#}› 𝒱 prevs nxts childs parents scores w] that assms by (auto simp: arr) from encoded_hp_prop_link[OF this] show ‹encoded_hp_prop 𝒱 {#Hp i w [the ?h]#} (prevs, nxts(i := None, node (the ?h) := None), childs(i ↦ node (the ?h)), parents(node (the ?h) ↦ i), scores(i ↦ w))› by auto from 0 have ‹encoded_hp_prop 𝒱 {#Hp (node (the ?h)) (score (the ?h)) (hps (the ?h)), Hp i w []#} (prevs, nxts(i := None), childs(i := None), parents, scores(i ↦ w))› by (cases ‹the ?h›) (auto simp: add_mset_commute) from encoded_hp_prop_link[OF this] show ?G . qed have prev_parent_i: ‹?h ≠ None ⟹ hp_read_prev i (prevs, nxts, childs, parents, scores) = None› ‹?h ≠ None ⟹ hp_read_parent i (prevs, nxts, childs, parents, scores) = None› using assms unfolding encoded_hp_prop_list_conc_def by (force simp: arr encoded_hp_prop_def empty_outside_alt_def dest!: multi_member_split[of i])+ have 1: ‹?h ≠ None ⟹ hps (the ?h) ≠ [] ⟹ i ≠ node (hd (hps (the ?h)))› using assms by (cases ‹the ?h›; cases ‹hps (the ?h)›; cases h) auto have [simp]: ‹encoded_hp_prop 𝒱 {#Hp x1a x2 x3#} (prevs, nxts, childs, parents, scores) ⟹ scores x1a = Some x2› ‹encoded_hp_prop 𝒱 {#Hp x1a x2 x3#} (prevs, nxts, childs, parents, scores) ⟹ parents x1a = None› ‹encoded_hp_prop 𝒱 {#Hp x1a x2 x3#} (prevs, nxts, childs, parents, scores) ⟹ childs x1a = map_option node (option_hd x3)› for x1a x2 x3 by (auto simp: encoded_hp_prop_def) show ?thesis using assms unfolding hp_insert_def arr prod.simps ACIDS.mop_hm_insert_def apply refine_vcg subgoal by auto subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def empty_outside_alt_def split: option.splits prod.splits) subgoal by auto subgoal using prev_parent_i by auto subgoal using prev_parent_i by auto subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal by (cases ‹the ?h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal by (cases ‹the ?h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_set_all_def split: option.splits prod.splits) subgoal using enc by (cases h, simp; cases ‹the ?h›) (auto simp: hp_set_all_def encoded_hp_prop_list_conc_def fun_upd_idem hp_update_parents_def) subgoal using enc by (cases h, simp; cases ‹the ?h›; cases ‹hps (the ?h)›; cases ‹hd (hps (the ?h))›) (auto simp: hp_set_all_def encoded_hp_prop_list_conc_def fun_upd_idem hp_update_parents_def arr) subgoal using enc2 1 by (cases h, simp; cases ‹the ?h›) (auto simp: hp_set_all_def encoded_hp_prop_list_conc_def fun_upd_idem hp_update_prev_def fun_upd_twist hp_update_parents_def) done qed definition hp_link :: ‹'a ⇒ 'a ⇒ 'a multiset × ('a,'b::order) hp_fun × 'a option ⇒ (('a multiset × ('a,'b) hp_fun × 'a option) × 'a) nres› where ‹hp_link = (λ(i::'a) j (𝒱::'a multiset, arr :: ('a, 'b) hp_fun, h :: 'a option). do { ASSERT (i ≠ j); ASSERT (i ∈# 𝒱); ASSERT (j ∈# 𝒱); ASSERT (hp_read_score i arr ≠ None); ASSERT (hp_read_score j arr ≠ None); let x = (the (hp_read_score i arr)::'b); 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)); 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 ∈# 𝒱); ASSERT (parent ∈# 𝒱); ASSERT (child ≠ None ⟶ the child ∈# 𝒱); ASSERT (nxt ≠ None ⟶ the nxt ∈# 𝒱); ASSERT (prev ≠ None ⟶ the prev ∈# 𝒱); let arr = hp_set_all parent prev nxt (Some ch) None (Some (w_p::'b)) (arr::('a, 'b) hp_fun); let arr = hp_set_all ch None child child_c_h (Some parent) (Some (w_c_h::'b)) (arr::('a, 'b) hp_fun); 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 :: ('a, 'b) hp_fun, h), parent) })› lemma fun_upd_twist2: "a ≠ c ⟹ a ≠ e ⟹ c ≠ e ⟹ m(a := b, c := d, e := f) = (m(e := f, c := d))(a := b)" by auto lemma hp_link: assumes enc: ‹encoded_hp_prop_list2_conc arr (𝒱', xs @ x # y # ys)› and ‹i = node x› and ‹j = node y› shows ‹hp_link i j arr ≤ SPEC (λ(arr, n). encoded_hp_prop_list2_conc arr (𝒱', xs @ ACIDS.link x y # ys) ∧ n = node (ACIDS.link x y))› proof - obtain prevs nxts childs parents scores 𝒱 where arr: ‹arr = (𝒱, (prevs, nxts, childs, parents, scores), None)› and dist: ‹distinct_mset (∑_# (mset_nodes `# (mset (xs @ x # y # ys))))› and 𝒱: ‹set_mset (sum_list (map mset_nodes (xs @ x # y # ys))) ⊆ set_mset 𝒱› and 𝒱'[simp]: ‹𝒱' = 𝒱› by (cases arr) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) have ij: ‹i ≠ j› using dist assms(2,3) by (cases x; cases y) auto have xy: ‹Hp (node x) (score x) (hps x) = x› ‹Hp (node y) (score y) (hps y) = y› and sc: ‹score x = the (scores i)› ‹score y = the (scores j)› and link_x_y: ‹ACIDS.link x y = ACIDS.link (Hp i (the (scores i)) (hps x)) (Hp j (the (scores j)) (hps y))› by (cases x; cases y; use assms in ‹auto simp: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def arr simp del: ACIDS.link.simps›; fail)+ obtain ch_x w_x ch_y w_y where x: ‹x = Hp i w_x ch_x› and y: ‹y = Hp j w_y ch_y› using assms(2-3) by (cases y; cases x) auto have sc': ‹scores i = Some w_x› ‹scores j = Some w_y› ‹prevs i = map_option node (option_last xs)› ‹nxts i = Some j› ‹prevs j = Some i› ‹nxts j = map_option node (option_hd ys)› ‹childs i = map_option node (option_hd ch_x)› ‹childs j = map_option node (option_hd ch_y)› ‹xs ≠ [] ⟹ nxts (node (last xs)) = Some i› ‹ys ≠ [] ⟹ prevs (node (hd ys)) = Some j› ‹parents i = None› ‹parents j = None› using assms(1) x y apply (auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def arr hp_child_children_Cons_if) apply (smt (verit) assms(3) hp_next_None_notin_children hp_next_children.elims list.discI list.inject list.sel(1) option_hd_Nil option_hd_Some_hd) using assms(1) x y apply (cases xs rule: rev_cases; auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def arr) apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' assms(2) distinct_mset_in_diff hp_next_children_simps(1) hp_next_children_skip_first_append node_in_mset_nodes option.map(2) sum_image_mset_sum_map) using assms(1) x y apply (cases ys;auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def arr) apply (cases ‹hd ys›) apply (auto simp:) by (simp add: hp_parent_None_notin_same_hd hp_parent_children_cons) have par: ‹parents j = None› ‹parents i = None› ‹ch_x ≠ [] ⟹ parents (node (hd ch_x)) = Some i› ‹ch_y ≠ [] ⟹ parents (node (hd ch_y)) = Some j› using assms(1) x y apply (auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def arr hp_child_children_Cons_if) apply (metis hp_parent_None_iff_children_None hp_parent_None_notin_same_hd hp_parent_children_cons hp_parent_hd_None sum_image_mset_sum_map) apply (metis assms(2) hp_parent_children_cons hp_parent_simps_single_if option.simps(5)) apply (cases ch_y) apply (simp_all add: hp_parent_children_skip_first[of _ _ ‹[_]›, simplified] distinct_mset_add) apply (subst hp_parent_children_skip_first[of _ _ ‹[_]›, simplified]) apply simp apply simp apply (metis distinct_mset_add inter_mset_empty_distrib_right) apply (subst hp_parent_children_skip_last[of _ ‹[_]›, simplified]) apply simp apply simp apply (metis distinct_mset_add inter_mset_empty_distrib_right) apply simp done have diff: ‹nxts j ≠ Some j› ‹nxts j ≠ Some i› ‹nxts i ≠ Some i› ‹prevs i ≠ Some i› ‹prevs i ≠ Some j› ‹childs i ≠ Some i› ‹childs i ≠ Some j› ‹childs j ≠ Some i› ‹childs j ≠ Some j› ‹childs i ≠ None ⟹ childs i ≠ childs j› ‹childs j ≠ None ⟹ childs i ≠ childs j› ‹prevs i ≠ None ⟹ prevs i ≠ nxts j› using dist sc' unfolding x y apply (cases ys; cases xs rule: rev_cases; auto split: if_splits; fail)+ using dist sc' unfolding x y apply (cases ys; cases xs rule: rev_cases; cases ‹last xs›; cases ‹hd ys›; cases ch_x; cases ch_y; cases ‹hd ch_x›; cases ‹hd ch_y›; auto split: if_splits; fail)+ done have dist2: ‹distinct([i, j] @ (if childs i ≠ None then [the (childs i)] else []) @ (if childs j ≠ None then [the (childs j)] else []) @ (if prevs i ≠ None then [the (prevs i)] else []) @ (if nxts j ≠ None then [the (nxts j)] else []))› using dist sc' unfolding x y by (cases ys; cases xs rule: rev_cases; cases ‹last xs›; cases ‹hd ys›; cases ch_x; cases ch_y; cases ‹hd ch_x›; cases ‹hd ch_y›) (auto split: if_splits) have if_pair: ‹(if a then (b, c) else (d,f)) = (if a then b else d, if a then c else f)› for a b c d f by auto have enc0: ‹encoded_hp_prop_list 𝒱 {#} (xs @ [Hp (node x) (score x) (hps x), Hp (node y) (score y) (hps y)] @ ys) (prevs, nxts, childs, parents, scores)› using enc unfolding x y by (auto simp: encoded_hp_prop_list2_conc_def arr) then have H: ‹fst x1= 𝒱 ⟹ snd (snd x1) = None⟹ encoded_hp_prop_list2_conc x1 (𝒱', xs @ ACIDS.link x y # ys) ⟷ encoded_hp_prop_list 𝒱 {#} (xs @ ACIDS.link x y # ys) (fst (snd x1))› for x1 using dist 𝒱 unfolding x y by (cases x1) (simp add: encoded_hp_prop_list2_conc_def) have KK [intro!]: ‹ch_x ≠ [] ⟹ ys ≠ [] ⟹ node (hd ch_x) ≠ node (hd ys)› using dist2 sc' by simp have subs: ‹set_mset (sum_list (map mset_nodes (xs @ Hp i w_x ch_x # Hp j w_y ch_y # ys))) ⊆ set_mset 𝒱› using assms(1) sc'(7,3) unfolding encoded_hp_prop_list2_conc_def x y arr prod.simps encoded_hp_prop_list_def by (clarsimp_all simp: encoded_hp_prop_list_def) then have childs_i: ‹childs i ≠ None ⟹ the (childs i) ∈# 𝒱› ‹prevs i ≠ None ⟹ the (prevs i) ∈# 𝒱› using sc'(7,3) unfolding encoded_hp_prop_list2_conc_def x y arr prod.simps encoded_hp_prop_list_def apply (clarsimp_all simp: encoded_hp_prop_list_def) apply (metis node_hd_in_sum option.sel subsetD) by (metis 𝒱 dist distinct_mset_add hp_next_children_None_notin hp_next_children_last list.discI map_append option_hd_Some_hd option_last_Nil option_last_Some_iff(2) subset_eq sum_image_mset_sum_map sum_list_append) have childs_j: ‹childs j ≠ None ⟹ the (childs j) ∈# 𝒱› ‹nxts j ≠ None ⟹ the (nxts j) ∈# 𝒱› using subs sc'(6,8) unfolding encoded_hp_prop_list2_conc_def x y arr prod.simps apply (clarsimp_all simp: encoded_hp_prop_list_def) apply (metis node_hd_in_sum option.sel subsetD) by (metis basic_trans_rules(31) node_hd_in_sum option.sel) show ?thesis unfolding hp_link_def arr prod.simps apply refine_vcg subgoal using ij by auto subgoal using dist 𝒱 by (auto simp: x) subgoal using dist 𝒱 by (auto simp: y) subgoal using sc' by auto subgoal using sc' by auto subgoal using diff by auto subgoal using diff by auto subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using diff by (auto split: if_splits) subgoal using dist2 by (clarsimp split: if_splits) subgoal by (clarsimp split: if_splits) subgoal by (clarsimp split: if_splits) subgoal using childs_i childs_j by (clarsimp simp: split: if_splits) subgoal using childs_i childs_j by (clarsimp simp: split: if_splits) subgoal using childs_i childs_j by (clarsimp simp: split: if_splits) subgoal premises p for parent b ch ba w_p w_c x1 x2 apply (cases ‹the (scores j) < the (scores i)›) subgoal apply (subst H) using p(1-12) p(19)[symmetric] dist2 𝒱 apply (solves simp) using p(1-12) p(19)[symmetric] dist2 𝒱 apply (solves simp) apply (subst arg_cong2[THEN iffD1, of _ _ _ _ ‹encoded_hp_prop_list 𝒱 {#}›, OF _ _ encoded_hp_prop_list_link[of 𝒱 ‹{#}› xs ‹node x› ‹score x› ‹hps x› ‹node y› ‹score y› ‹hps y› ys prevs nxts childs parents scores, OF enc0]]) subgoal using sc' p(1-12) p(19)[symmetric] dist2 𝒱 by (simp add: x y) subgoal using sc' p(1-12) p(19)[symmetric] dist2 𝒱 par apply (simp add: x y) apply (intro conjI impI) subgoal apply (simp add: fun_upd_idem fun_upd_twist fun_upd_idem[of ‹childs(parent ↦ ch)›] hp_set_all_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply auto[2] done subgoal supply [[goals_limit=1]] apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist[of _ _ parents]) apply force apply (subst fun_upd_twist[of _ _ prevs]) apply force apply blast done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_idem[of ‹nxts(parent := None)›]) apply (simp (no_asm_simp)) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_twist[of _ _ parents]) apply force apply (simp (no_asm_simp)) apply (subst fun_upd_idem[of ‹nxts(parent := None)(ch ↦ node (hd ch_x))›]) apply (simp (no_asm_simp)) apply force apply force done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist2[of _ _ _ prevs]) apply (rule KK) apply assumption apply assumption apply force apply force apply (subst fun_upd_twist[of _ _ ‹prevs(ch := None)›]) apply (rule KK[symmetric]) apply assumption apply assumption apply (subst fun_upd_twist[of _ _ ‹parents›]) apply argo apply blast done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist2) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_idem[of ‹nxts› ‹node (last xs)›]) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (simp (no_asm)) apply (subst fun_upd_twist[of _ _ ‹nxts›]) apply argo apply blast done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹childs(parent ↦ ch)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist2) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ ‹prevs(ch := None)›]) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_idem[of ‹nxts(ch ↦ node (hd ch_x), parent ↦ node (hd ys))›]) apply (simp (no_asm_simp)) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (simp (no_asm_simp)) apply (subst fun_upd_twist[of _ _ ‹parents›]) apply argo apply blast done done apply (rule TrueI) done subgoal supply [[goals_limit=1]] apply (subst H) using p(1-12) p(19)[symmetric] dist2 𝒱 apply simp using p(1-12) p(19)[symmetric] dist2 𝒱 apply simp apply (subst arg_cong2[THEN iffD1, of _ _ _ _ ‹encoded_hp_prop_list 𝒱 {#}›, OF _ _ encoded_hp_prop_list_link2[of 𝒱 ‹{#}› xs ‹node x› ‹score x› ‹hps x› ‹node y› ‹score y› ‹hps y› ys prevs nxts childs parents scores, OF enc0]]) subgoal using sc' p(1-12) p(19)[symmetric] dist2 𝒱 by (simp add: x y) subgoal using sc' p(1-12) p(19)[symmetric] dist2 𝒱 apply (simp add: x y) apply (intro conjI impI) subgoal by (simp add: fun_upd_idem fun_upd_twist fun_upd_idem[of ‹childs(parent ↦ ch)›] hp_set_all_def) subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_idem[of prevs _ ]) apply (simp (no_asm_simp)) apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_twist[of _ _ parents]) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def) apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_twist2[of _ _ _ nxts]) apply force apply force apply force apply (subst fun_upd_idem[of ‹nxts(ch := None)›]) apply (simp (no_asm_simp)) apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹(nxts(node (last xs) ↦ parent))›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_twist2) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ parents]) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ nxts]) apply force apply (subst fun_upd_twist[of _ _ ‹(prevs(parent ↦ node (last xs)))›]) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹prevs(parent := None)›]) apply (simp (no_asm_simp)) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_twist2) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ parents]) apply force apply (simp (no_asm_simp)) apply (subst fun_upd_idem[of ‹prevs(parent := None)›]) apply (simp (no_asm_simp)) apply (subst fun_upd_idem[of ‹(prevs(parent := None))(_ ↦ _)›]) apply (simp (no_asm_simp)) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply force done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_twist[of _ _ prevs]) apply force apply (subst fun_upd_idem[of ‹(prevs(parent ↦ node (last xs)))(ch := None)›]) apply (simp (no_asm_simp)) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_idem[of ‹nxts(node (last xs) ↦ parent)›]) apply (simp (no_asm_simp)) apply force apply (subst fun_upd_twist[of _ _ nxts]) apply force apply (simp (no_asm_simp)) done subgoal apply (simp (no_asm_simp) add: hp_set_all_def hp_update_nxt_def fun_upd_idem fun_upd_twist hp_update_prev_def hp_update_parents_def) apply (subst fun_upd_idem[of ‹(prevs(parent ↦ node (last xs)))(ch := None)(node (hd ch_y) ↦ ch)›]) apply (simp (no_asm_simp)) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist2) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_idem[of ‹nxts(node (last xs) ↦ parent)›]) apply (simp (no_asm_simp)) apply (smt (z3) IntI Un_iff empty_iff mem_Collect_eq option.simps(9) option_hd_Some_hd) apply (subst fun_upd_twist[of _ _ nxts]) apply force apply (subst fun_upd_twist[of _ _ parents]) apply force apply (simp (no_asm)) done done apply (rule TrueI) done done subgoal premises p using p(1-12) p(19)[symmetric] dist2 𝒱 using sc' by (cases ‹the (scores j) < the (scores i)›) (simp_all add: x y split: if_split) done qed text ‹In an imperative setting use the two pass approaches is better than the alternative. The term‹e::nat› of the loop is a dummy counter.› definition vsids_pass₁ where ‹vsids_pass₁ = (λ(𝒱::'a multiset, arr :: ('a, 'b::order) hp_fun, h :: 'a option) (j::'a). do { ((𝒱, arr, h), j, _, n) ← WHILE_T(λ((𝒱, arr, h), j, e, n). j ≠ None) (λ((𝒱, arr, h), j, e::nat, n). do { if j = None then RETURN ((𝒱, arr, h), None, e, n) else do { let j = the j; ASSERT (j ∈# 𝒱); let nxt = hp_read_nxt j arr; if nxt = None then RETURN ((𝒱, arr, h), nxt, e+1, j) else do { ASSERT (nxt ≠ None); ASSERT (the nxt ∈# 𝒱); let nnxt = hp_read_nxt (the nxt) arr; ((𝒱, arr, h), n) ← hp_link j (the nxt) (𝒱, arr, h); RETURN ((𝒱, arr, h), nnxt, e+2, n) }} }) ((𝒱, arr, h), Some j, 0::nat, j); RETURN ((𝒱, arr, h), n) })› lemma vsids_pass₁: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹encoded_hp_prop_list2_conc arr (𝒱', xs)› and ‹xs ≠ []› and ‹j = node (hd xs)› shows ‹vsids_pass₁ arr j ≤ SPEC(λ(arr, j). encoded_hp_prop_list2_conc arr (𝒱', ACIDS.pass₁ xs) ∧ j = node (last (ACIDS.pass₁ xs)))› proof - obtain prevs nxts childs scores 𝒱 where arr: ‹arr = (𝒱, (prevs, nxts, childs, scores), None)› and dist: ‹distinct_mset (∑_# (mset_nodes `# (mset (xs))))› and 𝒱: ‹set_mset (sum_list (map mset_nodes xs)) ⊆ set_mset 𝒱› and [simp]: ‹𝒱' = 𝒱› by (cases arr) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) define I where ‹I ≡ (λ(arr, nnxt::'a option, e, k). encoded_hp_prop_list2_conc arr (𝒱, ACIDS.pass₁(take e xs) @ drop e xs) ∧ nnxt = map_option node (option_hd (drop (e) xs)) ∧ e ≤ (length xs) ∧ (nnxt = None ⟷ e = length xs) ∧ (nnxt ≠ None ⟶ even e) ∧ k = (if e=0 then j else node (last (ACIDS.pass₁(take e xs)))))› have I0: ‹I ((𝒱, (prevs, nxts, childs, scores), None), Some j, 0, j)› using assms unfolding I_def prod.simps by (cases xs, auto simp: arr; fail)+ have I_no_next: ‹I ((𝒱, arr, ch'), None, Suc e, y)› if ‹I ((𝒱, arr, ch'), Some y, e, n)› and ‹hp_read_nxt y arr = None› for s a b prevs x2 nxts children x1b x2b x1c x2c x1d x2d arr e y ch' 𝒱 n proof - have ‹e = length xs - 1› ‹xs ≠ []› using that apply (cases ‹drop e xs›; cases ‹hd (drop e xs)›) apply (auto simp: I_def encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def) apply (subst (asm) hp_next_children_hd_simps) apply simp apply simp apply (rule distinct_mset_mono) prefer 2 apply assumption apply (auto simp: drop_is_single_iff) using that apply (auto simp: I_def) done then show ?thesis using that ACIDS.pass₁_append_even[of ‹butlast xs› ‹[last xs]›] by (auto simp: I_def) qed have link_pre1: ‹encoded_hp_prop_list2_conc (x1, x1a, x2a) (𝒱', ACIDS.pass₁ (take x2b xs) @ xs!x2b # xs!(Suc x2b) # drop (x2b+2) xs)› (is ?H1) and link_pre2: ‹the x1b = node (xs ! x2b)› (is ?H2) and link_pre3: ‹the (hp_read_nxt (the x1b) x1a) = node (xs ! Suc x2b)› (is ?H3) if ‹I s› and s: ‹case s of (x, xa) ⇒ (case x of (𝒱, arr, h) ⇒ λ(j, e, n). j ≠ None) xa› ‹s = (a, b)› "x2b' = (x2b, j)" ‹b = (x1b, x2b')› ‹x2 = (x1a, x2a)› ‹a = (x1, x2)› ‹x1b ≠ None› and nxt: ‹hp_read_nxt (the x1b) x1a ≠ None› for s a b x1 x2 x1a x2a x1b x2b j x2b' proof - have ‹encoded_hp_prop_list x1 {#} (ACIDS.pass₁ (take x2b xs) @ drop x2b xs) x1a› ‹x2b < length xs› ‹x1b = Some (node (hd (drop x2b xs)))› using that by (auto simp: I_def encoded_hp_prop_list2_conc_def arr) then have ‹drop x2b xs ≠ []› ‹tl (drop x2b xs) ≠ []› ‹Suc x2b < length xs› ‹the x1b = node (xs ! x2b)› ‹the (hp_read_nxt (the x1b) x1a) = node (xs ! Suc x2b)› using nxt unfolding s apply - apply (cases ‹drop x2b xs›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (cases ‹drop x2b xs›; cases ‹hd (drop x2b xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (cases ‹drop x2b xs›; cases ‹hd (drop x2b xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (smt (verit) Suc_le_eq append_eq_conv_conj hp_next_None_notin_children hp_next_children.elims length_Suc_conv_rev list.discI list.inject nat_less_le option_last_Nil option_last_Some_iff(2)) apply (cases ‹drop x2b xs›; cases ‹hd (drop x2b xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (subst (asm) hp_next_children_hd_simps) apply simp apply simp apply (rule distinct_mset_mono') apply assumption apply (auto simp: drop_is_single_iff) apply (metis hd_drop_conv_nth hp.sel(1) list.sel(1)) apply (cases ‹drop x2b xs›; cases ‹tl (drop x2b xs)›; cases ‹hd (drop x2b xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) by (metis Cons_nth_drop_Suc list.inject nth_via_drop) then show ?H1 using that ‹x2b < length xs› by (cases ‹drop x2b xs›; cases ‹tl (drop x2b xs)›) (auto simp: I_def encoded_hp_prop_list2_conc_def Cons_nth_drop_Suc) show ?H2 ?H3 using ‹the x1b = node (xs ! x2b)› ‹the (hp_read_nxt (the x1b) x1a) = node (xs ! Suc x2b)› by fast+ qed have I_Suc_Suc: ‹I ((x2c, x2d, xe), hp_read_nxt (the (hp_read_nxt (the nxt) x2a)) x2a, k + 2, n)› if inv: ‹I s› and brk: ‹case s of (x, xa) ⇒ (case x of (𝒱, arr, h) ⇒ λ(j, e, n). j ≠ None) xa› and st: ‹s = (arr2, b)› ‹b = (nxt, k')› ‹k' = (k, j)› ‹x1a = (x2a, x1b)› ‹arr2 = (𝒱'', x1a)› ‹linkedn = (linked, n)› ‹x1d = (x2d, xe)› ‹linked = (x2c, x1d)› and nxt: ‹nxt ≠ None› and nxts: ‹hp_read_nxt (the nxt) x2a ≠ None› ‹hp_read_nxt (the nxt) x2a ≠ None› and linkedn: ‹case linkedn of (arr, n) ⇒ encoded_hp_prop_list2_conc arr (𝒱', ACIDS.pass₁ (take k xs) @ ACIDS.link (xs ! k) (xs ! Suc k) # drop (k + 2) xs) ∧ n = node (ACIDS.link (xs ! k) (xs ! Suc k))› for s arr2 b x1a x2a x1b nxt k linkedn linked n x2c x1d x2d xe j k' 𝒱'' proof - have enc: ‹encoded_hp_prop_list 𝒱' {#} (ACIDS.pass₁ (take k xs) @ drop k xs) x2a› ‹k < length xs› ‹nxt = Some (node (hd (drop k xs)))› and dist: ‹distinct_mset (∑_# (mset_nodes `# (mset (ACIDS.pass₁ (take k xs) @ drop k xs))))› using that by (auto simp: I_def encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def) then have ‹drop k xs ≠ []› ‹tl (drop k xs) ≠ []› ‹Suc k < length xs› ‹the nxt = node (xs ! k)› using nxt unfolding st apply - apply (cases ‹drop k xs›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (cases ‹drop k xs›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (cases ‹drop k xs›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (metis hp_read_nxt.simps option.sel that(12)) apply (cases ‹drop k xs›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (subst (asm) hp_next_children_hd_simps) apply simp apply simp apply (rule distinct_mset_mono') apply assumption apply (auto simp: drop_is_single_iff) apply (metis Some_to_the Suc_lessI drop_eq_ConsD drop_eq_Nil2 hp_read_nxt.simps nat_in_between_eq(1) option.map(1) option_hd_Nil that(12)) apply (cases ‹drop k xs›; cases ‹tl (drop k xs)›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) apply (metis hp.sel(1) nth_via_drop) by (metis hp.sel(1) nth_via_drop) then have le: ‹Suc (Suc k) ≤ length xs› using enc nxts unfolding st nxt apply - apply (cases ‹drop k xs›; cases ‹tl (drop k xs)›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def) done have take_nth: ‹take (Suc (Suc k)) xs = take k xs @ [xs!k, xs!Suc k]› using le by (auto simp: take_Suc_conv_app_nth) have nnxts: ‹hp_read_nxt (the (hp_read_nxt (node (hd (drop k xs))) x2a)) x2a = map_option node (option_hd (drop (Suc (Suc k)) xs))› using enc nxts le ‹tl (drop k xs) ≠ []› unfolding st nxt apply - apply (cases ‹drop k xs›; cases ‹tl (drop k xs)›; cases ‹hd (tl (drop k xs))›; cases ‹hd (drop k xs)›) apply (auto simp: I_def encoded_hp_prop_list_def arr) apply (subst hp_next_children_hd_simps) apply (solves simp) apply (rule distinct_mset_mono'[OF dist]) by (auto simp: drop_is_single_iff drop_Suc_nth) show ?thesis using inv nxt le linkedn nnxts unfolding st by (auto simp: I_def take_Suc take_nth ACIDS.pass₁_append_even) qed show ?thesis unfolding vsids_pass₁_def arr prod.simps apply (refine_vcg WHILET_rule[where I=I and R = ‹measure (λ(arr, nnxt::'a option, e, _). length xs -e)›] hp_link) subgoal by auto subgoal by (rule I0) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def encoded_hp_prop_list2_conc_def) subgoal for s a b x1 x2 x1a x2a x1b x2b by (auto simp: I_no_next) subgoal by (auto simp: I_def) subgoal for s a b x1 x2 x1a x2a x1b x2b x1c x2c using hp_next_children_in_nodes2[of ‹(node (hd (drop x1c xs)))› ‹(ACIDS.pass₁ (take x1c xs) @ drop x1c xs)›] by (auto 5 3 simp: I_def encoded_hp_prop_list_def encoded_hp_prop_list2_conc_def) apply (rule link_pre1; assumption?) apply (rule link_pre2; assumption) subgoal premises p for s a b x1 x2 x1a x2a x1b x2b using link_pre3[OF p(1-8)] p(9-) by auto subgoal for s arr2 b 𝒱' x1a x2a x1b nxt k linkedn linked n x2c x1d x2d xe by (rule I_Suc_Suc) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def) subgoal using assms by (auto simp: I_def) done qed definition vsids_pass₂ where ‹vsids_pass₂ = (λ(𝒱::'a multiset, arr :: ('a, 'b::order) hp_fun, h :: 'a option) (j::'a). do { ASSERT (j ∈# 𝒱); let nxt = hp_read_prev j arr; ((𝒱, arr, h), j, leader, _) ← WHILE_T(λ((𝒱, arr, h), j, leader, e). j ≠ None) (λ((𝒱, arr, h), j, leader, e::nat). do { if j = None then RETURN ((𝒱, arr, h), None, leader, e) else do { let j = the j; ASSERT (j ∈# 𝒱); let nnxt = hp_read_prev j arr; ((𝒱, arr, h), n) ← hp_link j leader (𝒱, arr, h); RETURN ((𝒱, arr, h), nnxt, n, e+1) } }) ((𝒱, arr, h), nxt, j, 1::nat); RETURN (𝒱, arr, Some leader) })› lemma vsids_pass₂: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹encoded_hp_prop_list2_conc arr (𝒱', xs)› and ‹xs ≠ []› and ‹j = node (last xs)› shows ‹vsids_pass₂ arr j ≤ SPEC(λ(arr). encoded_hp_prop_list_conc arr (𝒱', ACIDS.pass₂ xs))› proof - obtain prevs nxts childs scores 𝒱 where arr: ‹arr = (𝒱, (prevs, nxts, childs, scores), None)› and dist: ‹distinct_mset (∑_# (mset_nodes `# (mset (xs))))› and 𝒱: ‹set_mset (sum_list (map mset_nodes xs)) ⊆ set_mset 𝒱› and [simp]: ‹𝒱' = 𝒱› by (cases arr) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) have prevs_lastxs: ‹prevs (node (last xs)) = map_option node (option_last (butlast xs))› using assms by (cases xs rule: rev_cases; cases ‹last xs›) (auto simp: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def arr) define I where ‹I ≡ (λ(arr, nnxt::'a option, leader, e'). let e = length xs - e' in encoded_hp_prop_list2_conc arr (𝒱, take e xs @ [the (ACIDS.pass₂ (drop e xs))]) ∧ nnxt = map_option node (option_last (take e xs)) ∧ leader = node (the (ACIDS.pass₂ (drop e xs))) ∧ e ≤ (length xs) ∧ (nnxt = None ⟷ e = 0) ∧ e' > 0)› have I0: ‹I ((𝒱, (prevs, nxts, childs, scores), None), hp_read_prev j (prevs, nxts, childs, scores), j, 1)› using assms prevs_lastxs unfolding I_def prod.simps Let_def by (auto simp: arr butlast_Nil_iff) have j𝒱: ‹j ∈# 𝒱› using assms by (cases xs rule: rev_cases) (auto simp: encoded_hp_prop_list2_conc_def arr) have links_pre1: ‹encoded_hp_prop_list2_conc (𝒱', arr', h') (𝒱, take (length xs - Suc e) xs @ xs ! (length xs - Suc e) # the (ACIDS.pass₂ (drop (length xs - e) xs)) # [])› (is ?H1) and links_pre2: ‹the x1b = node (xs ! (length xs - Suc e))› (is ?H2) and links_pre3: ‹leader = node (the (ACIDS.pass₂ (drop (length xs - e) xs)))› (is ?H3) if I: ‹I s› and brk: ‹case s of (x, xa) ⇒ (case x of (𝒱, arr, h) ⇒ λ(j, leader, e). j ≠ None) xa› and st: ‹s = (a, b)› ‹x2b = (leader, e)› ‹b = (x1b, x2b)› ‹xy = (arr', h')› ‹a = (𝒱', xy)› and no_None: ‹x1b ≠ None› for s a b 𝒱' xy arr' h' x1b x2b x1c x2c e leader proof - have ‹e < length xs› ‹length xs - e < length xs› using I brk no_None unfolding st I_def by (auto simp: I_def Let_def) then have take_Suc: ‹take (length xs - e) xs = take (length xs - Suc e) xs @ [xs ! (length xs - Suc e)]› using I brk take_Suc_conv_app_nth[of "length xs - Suc e" xs] unfolding st apply (cases ‹take (length xs - e) xs› rule: rev_cases) apply (auto simp: I_def Let_def) done then show ?H1 using I brk unfolding st apply (cases ‹take (length xs - e) xs› rule: rev_cases) apply (auto simp: I_def Let_def) done show ?H2 using I brk unfolding st I_def Let_def by (auto simp: take_Suc) show ?H3 using I brk unfolding st I_def Let_def by (auto simp: take_Suc) qed have I_Suc: ‹I ((x1d, x1e, x2e), hp_read_prev (the x1b) x1a, new_leader, e + 1)› if I: ‹I s› and brk: ‹case s of (x, xa) ⇒ (case x of (𝒱, arr, h) ⇒ λ(j, leader, e). j ≠ None) xa› and st: ‹s = (a, b)› ‹x2b = (x1c, e)› ‹b = (x1b, x2b)› ‹x2 = (x1a, x2a)› ‹a = (𝒱', x2)› ‹linkedn = (linked, new_leader)› ‹x2d = (x1e, x2e)› ‹linked = (x1d, x2d)› and no_None: ‹x1b ≠ None› and ‹case linkedn of (arr, n) ⇒ encoded_hp_prop_list2_conc arr (𝒱, take (length xs - Suc e) xs @ [ACIDS.link (xs ! (length xs - Suc e)) (the (ACIDS.pass₂ (drop (length xs - e) xs)))]) ∧ n = node (ACIDS.link (xs ! (length xs - Suc e)) (the (ACIDS.pass₂ (drop (length xs - e) xs))))› for s a b 𝒱' x2 x1a x2a x1b x2b x1c e linkedn linked new_leader x1d x2d x1e x2e proof - have e: ‹e < length xs› ‹length xs - e < length xs› using I brk no_None unfolding st I_def by (auto simp: I_def Let_def) then have [simp]: ‹ACIDS.link (xs ! (length xs - Suc e)) (the (ACIDS.pass₂ (drop (length xs - e) xs))) = the (ACIDS.pass₂ (drop (length xs - Suc e) xs))› using that by (auto simp: I_def Let_def simp flip: Cons_nth_drop_Suc split: option.split) have [simp]: ‹hp_read_prev (node (last (take (length xs - e) xs))) x1a = map_option node (option_last (take (length xs - Suc e) xs))› using e I take_Suc_conv_app_nth[of "length xs - Suc e" xs] unfolding I_def st Let_def by (cases ‹(take (length xs - e) xs)› rule: rev_cases; cases ‹last (take (length xs - e) xs)›) (auto simp: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def) show ?thesis using that e by (auto simp: I_def Let_def) qed show ?thesis unfolding vsids_pass₂_def arr prod.simps apply (refine_vcg WHILET_rule[where I=I and R = ‹measure (λ(arr, nnxt::'a option, _, e). length xs -e)›] hp_link) subgoal using j𝒱 by auto subgoal by auto subgoal by (rule I0) subgoal by auto subgoal by auto subgoal for s a b x1 x2 x1a x2a x1b x2b x1c x2c by (cases ‹take (length xs - x2c) xs› rule: rev_cases) (auto simp: I_def Let_def encoded_hp_prop_list2_conc_def) apply (rule links_pre1; assumption) subgoal by (rule links_pre2) subgoal by (rule links_pre3) subgoal by (rule I_Suc) subgoal for s a b 𝒱' x2 x1a x2a x1b x2b x1c e linkedn linked new_leader x1d x2d x1e x2e by (auto simp: I_def Let_def) subgoal using assms ACIDS.mset_nodes_pass₂[of xs] by (auto simp: I_def Let_def encoded_hp_prop_list_conc_def encoded_hp_prop_list2_conc_def split: option.split simp del: ACIDS.mset_nodes_pass₂) done qed definition merge_pairs where ‹merge_pairs arr j = do { (arr, j) ← vsids_pass₁ arr j; vsids_pass₂ arr j }› lemma vsids_merge_pairs: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹encoded_hp_prop_list2_conc arr (𝒱', xs)› and ‹xs ≠ []› and ‹j = node (hd xs)› shows ‹merge_pairs arr j ≤ SPEC(λ(arr). encoded_hp_prop_list_conc arr (𝒱', ACIDS.merge_pairs xs))› proof - show ?thesis unfolding merge_pairs_def apply (refine_vcg vsids_pass₁ vsids_pass₂[of _ 𝒱' "ACIDS.pass₁ xs"]) apply (rule assms)+ subgoal by auto subgoal using assms by (cases xs rule: ACIDS.pass₁.cases) auto subgoal using assms by auto subgoal by (auto simp: ACIDS.pass12_merge_pairs) done qed definition hp_update_child where ‹hp_update_child i nxt = (λ(prevs, nxts, childs, scores). (prevs, nxts, childs(i:=nxt), scores))› definition vsids_pop_min :: ‹_› where ‹vsids_pop_min = (λ(𝒱::'a multiset, arr :: ('a, 'b::order) hp_fun, h :: 'a option). do { if h = None then RETURN (None, (𝒱, arr, h)) else do { ASSERT (the h ∈# 𝒱); let j = hp_read_child (the h) arr; if j = None then RETURN (h, (𝒱, arr, None)) else do { ASSERT (the j ∈# 𝒱); 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 (𝒱, arr, None) (the j); RETURN (h, arr) } } })› lemma node_remove_key_itself_iff[simp]: ‹remove_key (y) z ≠ None ⟹ node z = node (the (remove_key (y) z)) ⟷ y ≠ node z› by (cases z) auto lemma vsids_pop_min: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹encoded_hp_prop_list_conc arr (𝒱, h)› shows ‹vsids_pop_min arr ≤ SPEC(λ(j, arr). j = (if h = None then None else Some (get_min2 h)) ∧ encoded_hp_prop_list_conc arr (𝒱, ACIDS.del_min h))› proof - show ?thesis unfolding vsids_pop_min_def apply (refine_vcg vsids_merge_pairs[of _ 𝒱 ‹case the h of Hp _ _ child ⇒ child›]) subgoal using assms by (cases h) (auto simp: encoded_hp_prop_list_conc_def) subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def split: option.splits) subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def split: option.splits) subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms encoded_hp_prop_list_remove_min[of 𝒱 ‹node (the h)› ‹score (the h)› ‹hps (the h)› ‹{#}› ‹fst (fst (snd arr))› ‹(fst o snd) (fst (snd arr))› ‹(fst o snd o snd) (fst (snd arr))› ‹(fst o snd o snd o snd) (fst (snd arr))› ‹(snd o snd o snd o snd) (fst (snd arr))›] by (cases ‹the h›; cases ‹fst (snd arr)›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list2_conc_def hp_update_parents_def hp_update_nxt_def hp_update_score_def hp_update_child_def hp_update_prev_def get_min2_alt_def split: option.splits if_splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹h›; cases ‹the h›) (auto simp: get_min2_alt_def ACIDS.pass12_merge_pairs encoded_hp_prop_list_conc_def split: option.splits) done qed text ‹Unconditionnal version of the previous function› definition vsids_pop_min2 :: ‹_› where ‹vsids_pop_min2 = (λ(𝒱::'a multiset, arr :: ('a, 'b::order) hp_fun, h :: 'a option). do { ASSERT (h≠None); ASSERT (the h ∈# 𝒱); let j = hp_read_child (the h) arr; if j = None then RETURN (the h, (𝒱, arr, None)) else do { ASSERT (the j ∈# 𝒱); 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 (𝒱, arr, None) (the j); RETURN (the h, arr) } } )› lemma vsids_pop_min2: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹encoded_hp_prop_list_conc arr (𝒱, h)› and ‹h ≠ None› shows ‹vsids_pop_min2 arr ≤ SPEC(λ(j, arr). j = (get_min2 h) ∧ encoded_hp_prop_list_conc arr (𝒱, ACIDS.del_min h))› proof - show ?thesis unfolding vsids_pop_min2_def apply (refine_vcg vsids_merge_pairs[of _ 𝒱 ‹case the h of Hp _ _ child ⇒ child›]) subgoal using assms by (cases h) (auto simp: encoded_hp_prop_list_conc_def) subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms encoded_hp_prop_list_remove_min[of 𝒱 ‹node (the h)› ‹score (the h)› ‹hps (the h)› ‹{#}› ‹fst (fst (snd arr))› ‹(fst o snd) (fst (snd arr))› ‹(fst o snd o snd) (fst (snd arr))› ‹(fst o snd o snd o snd) (fst (snd arr))› ‹(snd o snd o snd o snd) (fst (snd arr))›] by (cases ‹the h›; cases ‹fst (snd arr)›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list2_conc_def hp_update_parents_def hp_update_nxt_def hp_update_score_def hp_update_child_def hp_update_prev_def get_min2_alt_def split: option.splits if_splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹the h›) (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def get_min2_alt_def split: option.splits) subgoal using assms by (cases ‹h›; cases ‹the h›) (auto simp: get_min2_alt_def ACIDS.pass12_merge_pairs encoded_hp_prop_list_conc_def split: option.splits) done qed lemma in_remove_key_in_find_keyD: ‹m' ∈# (if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#}) ⟹ distinct_mset (mset_nodes h) ⟹ x' ∈# mset_nodes m' ⟹ x' ∈# mset_nodes h› using find_remove_mset_nodes_full[of h a ‹the (remove_key a h)› ‹the (find_key a h)›] in_remove_key_in_nodes[of a h x'] apply (auto split: if_splits simp: find_key_None_remove_key_ident) apply (metis hp_node_None_notin2 hp_node_in_find_key0) by (metis union_iff) lemma map_option_node_map_option_node_iff: ‹(x ≠ None ⟹ distinct_mset (mset_nodes (the x))) ⟹ (x ≠ None ⟹ y ≠ node (the x)) ⟹ map_option node x = map_option node (map_option (λx. the (remove_key y x)) x)› by (cases x; cases ‹the x›) auto lemma distinct_mset_hp_parent: ‹distinct_mset (mset_nodes h) ⟹ hp_parent a h = Some ya ⟹ distinct_mset (mset_nodes ya)› apply (induction a h arbitrary: ya rule: hp_parent.induct) apply (auto simp: hp_parent_simps_if hp_parent_children_cons split: if_splits option.splits) apply (metis (no_types, lifting) WB_List_More.distinct_mset_union2 distinct_mset_union hp_parent_children_Some_iff in_list_in_setD list.map(2) map_append sum_list.Cons sum_list_append) by (metis distinct_mset_union) lemma in_find_key_children_same_hp_parent: ‹hp_parent k (Hp x n c) = None ⟹ x' ∈# mset_nodes m' ⟹ x ∉# sum_list (map mset_nodes c) ⟹ distinct_mset (sum_list (map mset_nodes c)) ⟹ find_key_children k c = Some m' ⟹ hp_parent x' (Hp x n c) = hp_parent x' m'› apply (induction k c rule: find_key_children.induct) subgoal by (auto split: if_splits option.splits simp: hp_parent_simps_single_if hp_parent_children_cons) subgoal for k xa na c xs apply (auto split: if_splits option.splits simp: hp_parent_simps_single_if hp_parent_children_cons) apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(3) sum_image_mset_sum_map) apply (metis (no_types, lifting) ACIDS.hp_node_find_key_children find_key_children.simps(1) find_key_children_None_or_itself hp.sel(1) hp_node_None_notin2 hp_node_children_simps(3) hp_node_node_itself hp_parent_children_in_first_child hp_parent_in_nodes list.exhaust_sel list.simps(9) mset_nodes_find_key_children_subset mset_subset_eqD node_in_mset_nodes option.sel sum_image_mset_sum_map sum_list_simps(2)) apply (metis hp_node_None_notin2 hp_node_children_None_notin2 hp_node_in_find_key_children sum_image_mset_sum_map) apply (smt (verit, ccfv_threshold) basic_trans_rules(31) find_key_children.elims find_key_children.simps(2) hp.exhaust_sel hp.sel(1) hp_parent_children_in_first_child hp_parent_in_nodes list.distinct(1) list.exhaust_sel list.simps(9) mset_nodes_find_key_children_subset option.sel option.simps(2) set_mset_mono sum_image_mset_sum_map sum_list_simps(2)) apply (metis disjunct_not_in distinct_mset_add find_key_noneD find_key_none_iff mset_map mset_nodes_find_key_children_subset mset_subset_eqD node_hd_in_sum option.sel sum_mset_sum_list) apply (smt (verit, ccfv_threshold) basic_trans_rules(31) find_key_children.elims find_key_children.simps(2) hp.exhaust_sel hp.sel(1) hp_parent_children_in_first_child hp_parent_in_nodes list.distinct(1) list.exhaust_sel list.simps(9) mset_nodes_find_key_children_subset option.sel option.simps(2) set_mset_mono sum_image_mset_sum_map sum_list_simps(2)) apply (smt (verit) ACIDS.hp_node_find_key_children distinct_mset_add ex_hp_node_children_Some_in_mset_nodes find_key_children.simps(1) find_key_children_None_or_itself find_key_none_iff hp.sel(1) hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps(3) hp_node_in_find_key_children hp_node_node_itself hp_parent_children_in_first_child hp_parent_in_nodes list.exhaust_sel list.simps(9) option.sel option_last_Nil option_last_Some_iff(2) sum_list_simps(2)) apply (metis Duplicate_Free_Multiset.distinct_mset_union2 hp_parent_children_hd_None option.simps(2) sum_image_mset_sum_map union_commute) apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin if_Some_None_eq_None mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_mset_sum_list) apply (metis Duplicate_Free_Multiset.distinct_mset_union2 hp.sel(1) hp_parent_in_nodes mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(2) sum_image_mset_sum_map union_commute) apply (metis basic_trans_rules(31) mset_nodes_find_key_children_subset option.distinct(1) option.sel set_mset_mono sum_image_mset_sum_map) apply (metis distinct_mset_add find_key_noneD find_key_none_iff hp_parent_children_None_notin hp_parent_children_skip_first hp_parent_children_skip_last mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_mset_sum_list) apply (simp add: distinct_mset_add) using distinct_mset_union by blast done lemma in_find_key_same_hp_parent: ‹x' ∈# mset_nodes m' ⟹ distinct_mset (mset_nodes h) ⟹ find_key a h = Some m' ⟹ hp_parent a h = None ⟹ ∃y. hp_prev a h = Some y ⟹ hp_parent x' h = hp_parent x' m'› by (induction a h rule: find_key.induct) (auto split: if_splits intro: in_find_key_children_same_hp_parent) lemma in_find_key_children_same_hp_parent2: ‹x' ≠ k ⟹ x' ∈# mset_nodes m' ⟹ x ∉# sum_list (map mset_nodes c) ⟹ distinct_mset (sum_list (map mset_nodes c)) ⟹ find_key_children k c = Some m' ⟹ hp_parent x' (Hp x n c) = hp_parent x' m'› apply (induction k c rule: find_key_children.induct) subgoal by (auto split: if_splits option.splits simp: hp_parent_simps_single_if hp_parent_children_cons) subgoal for k xa na c xs apply (auto split: if_splits option.splits simp: hp_parent_simps_single_if hp_parent_children_cons) apply (metis add_diff_cancel_left' distinct_mem_diff_mset hp_parent_children_None_notin) apply (metis hp_node_None_notin2 hp_node_children_None_notin2 hp_node_in_find_key_children sum_image_mset_sum_map) apply (metis hp.sel(1) hp_parent_in_nodes2 mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(2) sum_image_mset_sum_map) apply (metis disjunct_not_in distinct_mset_add find_key_noneD find_key_none_iff mset_map mset_nodes_find_key_children_subset mset_subset_eqD node_hd_in_sum option.sel sum_mset_sum_list) apply (metis hp_node_None_notin2 hp_node_children_None_notin2 hp_node_in_find_key_children sum_image_mset_sum_map) apply (metis hp.sel(1) hp_parent_in_nodes2 mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(2) sum_image_mset_sum_map) apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map) apply (metis basic_trans_rules(31) distinct_mset_union ex_hp_node_children_Some_in_mset_nodes hp.sel(1) hp_node_children_simps(1) hp_parent_in_nodes mset_nodes_find_key_children_subset option.sel option.simps(2) set_mset_mono sum_image_mset_sum_map union_commute) apply (metis distinct_mset_union hp_parent_children_hd_None option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map) apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin mset_nodes_find_key_children_subset mset_subset_eqD option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map) apply (metis distinct_mset_union hp.sel(1) hp_parent_in_nodes mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(2) sum_image_mset_sum_map) apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map) apply (metis disjunct_not_in distinct_mset_add hp_node_None_notin2 hp_node_children_None_notin2 hp_node_in_find_key_children hp_parent_children_None_notin sum_image_mset_sum_map) apply (metis distinct_mset_union hp_parent_children_hd_None option.simps(2) sum_image_mset_sum_map) using distinct_mset_union by blast done lemma in_find_key_same_hp_parent2: ‹x' ∈# mset_nodes m' ⟹ distinct_mset (mset_nodes h) ⟹ find_key a h = Some m' ⟹ x' ≠ a ⟹ hp_parent x' h = hp_parent x' m'› by (induction a h rule: find_key.induct) (auto split: if_splits intro: in_find_key_children_same_hp_parent2) lemma encoded_hp_prop_list_remove_find: fixes h :: ‹('a, nat) hp› and a arr and hs :: ‹('a, nat) hp multiset› defines ‹arr₁ ≡ (if hp_parent a h = None then arr else hp_update_child (node (the (hp_parent a h))) (map_option node (hp_next a h)) arr)› defines ‹arr₂ ≡ (if hp_prev a h = None then arr₁ else hp_update_nxt (node (the (hp_prev a h))) (map_option node (hp_next a h)) arr₁)› defines ‹arr₃ ≡ (if hp_next a h = None then arr₂ else hp_update_prev (node (the (hp_next a h))) (map_option node (hp_prev a h)) arr₂)› defines ‹arr₄ ≡ (if hp_next a h = None then arr₃ else hp_update_parents (node (the (hp_next a h))) (map_option node (hp_parent a h)) arr₃)› defines ‹arr' ≡ hp_update_parents a None (hp_update_prev a None (hp_update_nxt a None arr₄))› assumes enc: ‹encoded_hp_prop_list 𝒱 (add_mset h {#}) [] arr› shows ‹encoded_hp_prop_list 𝒱 ((if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#})) [] arr'› proof - obtain prevs nxts childs parents scores where arr: ‹arr = ((prevs, nxts, childs, parents, scores))› and dist: ‹distinct_mset (mset_nodes h)› and 𝒱: ‹set_mset (mset_nodes h) ⊆ set_mset 𝒱› by (cases arr) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_def›) have find_key_in_nodes: ‹find_key a h ≠ None ⟹ node (the (find_key a h)) ∈# mset_nodes h› by (cases ‹a ∈# mset_nodes h›) (use find_key_None_or_itself[of a h] in ‹auto simp del: find_key_None_or_itself›) have in_find_key_in_nodes1: ‹x ∈# mset_nodes y ⟹ find_key a h = Some y ⟹ x ∈# mset_nodes h› for x y using mset_nodes_find_key_subset[of a h] by auto have [simp]: ‹find_key a h = None ⟹ remove_key a h = Some h› by (metis find_key.simps find_key_none_iff hp.exhaust_sel hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps2 option_last_Nil option_last_Some_iff(2) remove_key_notin_unchanged) have HX1: ‹ (find_key (node m') h ≠ None ⟹ distinct_mset (mset_nodes (the (find_key (node m') h)) + (if hp_next (node m') h = None then {#} else mset_nodes (the (hp_next (node m') h))))) ⟹ x' ∈# mset_nodes m' ⟹ x' ∉# mset_nodes y' ⟹ find_key (node y) h = Some y ⟹ m' = y' ∨ m' = y ⟹ hp_next (node y) h ≠ None ⟹ x' = node (the (hp_next (node y) h)) ⟹ map_option node (hp_prev (node y) h) = map_option node (hp_prev (node (the (hp_next (node y) h))) m')› for y y' m' x' by (smt (z3) distinct_mset_iff mset_add node_in_mset_nodes option.distinct(1) option.sel union_mset_add_mset_left union_mset_add_mset_right) have dist: ‹distinct_mset (mset_nodes h)› and nxts: ‹(∀m'∈#{#h#}. ∀x∈#mset_nodes m'. nxts x = map_option node (hp_next x m'))› and prevs: ‹(∀m∈#{#h#}. ∀x∈#mset_nodes m. prevs x = map_option node (hp_prev x m))› and childs: ‹(∀m∈#{#h#}. ∀x∈#mset_nodes m. childs x = map_option node (hp_child x m))› and parents: ‹(∀m∈#{#h#}. ∀x∈#mset_nodes m. parents x = map_option node (hp_parent x m))› and scores: ‹(∀m∈#{#h#}. ∀x∈#mset_nodes m. scores x = hp_score x m)› and empty_outside: ‹empty_outside (∑_# (mset_nodes `# {#h#} + mset_nodes `# mset [])) prevs› ‹empty_outside (∑_# (mset_nodes `# {#h#} + mset_nodes `# mset [])) parents› using enc unfolding encoded_hp_prop_list_def prod.simps arr by auto let ?a = ‹(if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#})› have H: ‹remove_key a h ≠ None ⟹ node (the (remove_key a h)) ∈# mset_nodes h› by (metis remove_key.simps get_min2.simps hp.exhaust_sel option.collapse option.distinct(2) remove_key_notin_unchanged) show ?thesis supply [[goals_limit=1]] using dist unfolding arr hp_update_child_def hp_update_nxt_def hp_update_prev_def case_prod_beta hp_update_parents_def encoded_hp_prop_list_def prod.simps apply - proof (intro conjI impI ballI) show ‹distinct_mset (∑_# (mset_nodes `# ?a + mset_nodes `# mset []))› using dist apply (auto simp: find_remove_mset_nodes_full) apply (metis distinct_mset_mono' mset_nodes_find_key_subset option.distinct(2) option.sel) done next show ‹set_mset (∑_# (mset_nodes `# ((if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#})) + mset_nodes `# mset [])) ⊆ set_mset 𝒱› using 𝒱 apply (auto dest: in_find_key_in_nodes1) apply (metis Set.basic_monos(7) in_remove_key_in_nodes option.distinct(2) option.sel) done next fix m' and x' assume ‹m'∈#?a› and ‹x' ∈# mset_nodes m'› then show ‹fst (snd arr') x' = map_option node (hp_next x' m')› using nxts dist H hp_next_find_key[of h a x'] hp_next_find_key_itself[of h a] in_remove_key_in_nodes[of a h x'] in_find_key_notin_remove_key[of h a x'] in_find_key_in_nodes[of a h x'] unfolding assms(1-5) arr using hp_next_remove_key_other[of h a x'] find_key_None_or_itself[of a h] hp_next_find_key_itself[of h a] has_prev_still_in_remove_key[of h a] in_remove_key_changed[of a h] hp_parent_itself[of h] remove_key_None_iff[of a h] find_key_head_node_iff[of h m'] by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) next fix m' and x' assume M': ‹m'∈#?a› ‹x' ∈# mset_nodes m'› then show ‹fst arr' x' = map_option node (hp_prev x' m')› using prevs H dist hp_prev_find_key[of h a x'] in_remove_key_in_nodes[of a h x'] in_find_key_notin_remove_key[of h a x'] in_find_key_in_nodes[of a h x'] unfolding assms(1-5) arr using hp_prev_remove_key_other[of h a x'] find_key_None_or_itself[of a h] hp_prev_find_key_itself[of h a] has_prev_still_in_remove_key[of h a] in_remove_key_changed[of a h] hp_parent_itself[of h] remove_key_None_iff[of a h] find_key_head_node_iff[of h m'] using hp_prev_and_next_same_node[of h x' m' ‹the (hp_next (node m') h)›] distinct_mset_find_node_next[of h ‹node m'› ‹the (find_key (node m') h)›] apply (simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits del: find_key_None_or_itself hp_parent_itself) apply (intro conjI impI allI) subgoal by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) apply (intro conjI impI allI) subgoal by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal unfolding eq_commute[of _ x'] by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using node_in_mset_nodes[of ‹the (hp_next (node m') h)›] unfolding eq_commute[of _ x'] by auto subgoal using node_in_mset_nodes[of ‹the (hp_next (node m') h)›] unfolding eq_commute[of _ x'] by auto subgoal for y y' apply (clarsimp simp add: atomize_not hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself) apply (intro conjI impI) using HX1[of y x' y' m'] apply (auto simp add: atomize_not hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself) done subgoal by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_prev_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) done next fix m' and x' assume M': ‹m'∈#?a› ‹x' ∈# mset_nodes m'› have helper1: ‹hp_parent (node yb) yyy = None› if ‹distinct_mset (mset_nodes yyy)› and ‹node y ∈# mset_nodes h› and ‹hp_parent (node yyy) h = Some y› and ‹hp_child (node y) h = Some yb› for y :: ‹('a, nat) hp› and ya :: ‹('a, nat) hp› and yb :: ‹('a, nat) hp› and z :: ‹('a, nat) hp› and yyy using childs[simplified] by (metis dist hp_child_hp_parent hp_parent_itself option.map_sel option.sel option_last_Nil option_last_Some_iff(1) that) have helper2: ‹hp_child (node ya) yyy ≠ hp_child (node ya) h› if ‹distinct_mset (mset_nodes yyy)› and ‹hp_parent (node yyy) h = Some ya› ‹node ya ∈# mset_nodes h› for y :: ‹('a, nat) hp› and ya :: ‹('a, nat) hp› and yyy yya using childs[simplified] by (metis dist that hp_child_hp_parent hp_parent_hp_child hp_parent_itself map_option_is_None option.map_sel option.sel option_last_Nil option_last_Some_iff(1)) have helper4: ‹map_option node (map_option (λx. the (remove_key (node yy) x)) (hp_child (x') h)) = map_option node (hp_child (x') h)› if ‹∃y. hp_child (x') h = Some y ⟹ ∃z. hp_parent (node (the (hp_child (x') h))) h = Some z ∧ node z = x'› and ‹node h = node yya ⟹ find_key (node yya) h ≠ Some yya› and ‹hp_parent (node yy) h = None› for yya yy x' using that childs[simplified] dist apply - using distinct_sum_next_prev_child[of h x'] apply (auto simp: map_option_node_remove_key_iff) apply (subst eq_commute) apply (rule ccontr) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) have ‹find_key a h ≠ None ⟹ distinct_mset (mset_nodes (the (find_key a h)))› by (meson dist distinct_mset_mono' mset_nodes_find_key_subset) then show ‹fst (snd (snd arr')) x' = map_option node (hp_child x' m')› using childs dist H M' hp_child_find_key[of h a x'] in_remove_key_in_nodes[of a h x'] in_find_key_notin_remove_key[of h a x'] in_find_key_in_nodes[of a h x'] hp_parent_hp_child[of h x'] hp_child_hp_parent[of h x'] hp_child_hp_parent[of h x'] (*hp_parent_hp_child[of ‹the (find_key a h)› x']*) hp_parent_hp_child[of ‹the (find_key a h)› x'] unfolding assms(1-5) arr using hp_child_remove_key_other[of h a x'] find_key_None_or_itself[of a h] hp_next_find_key_itself[of h a] has_prev_still_in_remove_key[of h a] in_remove_key_changed[of a h] hp_parent_itself[of h] remove_key_None_iff[of a h] find_key_head_node_iff[of h m'] apply (simp split: if_splits(2) del: find_key_None_or_itself hp_parent_itself) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) apply (solves ‹auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def helper2 map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself›)[] apply (solves ‹auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def helper2 map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself›)[] apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself) apply (intro conjI impI) subgoal for yy yya apply auto apply (subst (asm) helper4) apply assumption+ apply simp done apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) subgoal by auto subgoal for y y' using hp_child_remove_key_other[of h a x', symmetric] apply (auto simp: map_option.compositionality comp_def) apply (subst (asm) map_option_node_map_option_node_iff) apply auto[] apply (smt (verit, del_insts) None_eq_map_option_iff node_remove_key_itself_iff option.distinct(2) option.exhaust_sel option.map_sel remove_key_None_iff) apply (smt (verit) None_eq_map_option_iff node_remove_key_itself_iff option.exhaust_sel option.simps(9) remove_key_None_iff) by (metis (no_types, lifting) map_option_cong node_remove_key_itself_iff option.sel option.simps(3) remove_key_None_iff) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal apply auto by (metis no_relative_ancestor_or_notin) subgoal apply auto by (smt (verit, del_insts) None_eq_map_option_iff hp.exhaust_sel hp_child_remove_is_remove_hp_child node_remove_key_itself_iff option.exhaust_sel option.map(2) option.simps(1)) subgoal by (smt (verit, ccfv_SIG) None_eq_map_option_iff node_remove_key_itself_iff option.exhaust_sel option.map_sel remove_key_None_iff) subgoal by (smt (verit, ccfv_SIG) None_eq_map_option_iff node_remove_key_itself_iff option.exhaust_sel option.map_sel remove_key_None_iff) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) apply (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def hp_update_parents_def map_option.compositionality comp_def map_option_node_hp_next_remove_key split: if_splits simp del: find_key_None_or_itself hp_parent_itself) subgoal using distinct_sum_next_prev_child[of h x'] apply (auto simp: remove_key_None_iff map_option_node_remove_key_iff) apply (subst (asm) map_option_node_remove_key_iff) apply simp apply (meson distinct_mset_add) by (auto simp: remove_key_None_iff) done have helper1: False if ‹distinct_mset (mset_nodes h)› and ‹node y ∈# mset_nodes m'› and ‹node y ∈# mset_nodes ya› and ‹remove_key a h = Some m'› and ‹find_key a h = Some ya› and ‹x' = node y› for ya :: ‹('a, nat) hp› and y :: ‹('a, nat) hp› and yb :: ‹('a, nat) hp› by (metis that Some_to_the in_find_key_notin_remove_key option_last_Nil option_last_Some_iff(2)) have helper3: ‹False› if ‹distinct_mset (mset_nodes h)› and ‹x' ∈# mset_nodes m'› and ‹x' ∈# mset_nodes ya› and ‹remove_key a h = Some m'› and ‹find_key a h = Some ya› for ya :: ‹('a, nat) hp› by (metis that Some_to_the in_find_key_notin_remove_key option_last_Nil option_last_Some_iff(1)) have helperb4: ‹False› if ‹h = m'› and ‹hp_next a m' = Some z› and ‹find_key a m' = None› for z :: ‹('a, nat) hp› and y :: ‹('a, nat) hp› by (metis that find_key_None_remove_key_ident hp_next_None_notin in_remove_key_changed option.sel option.simps(2)) have [simp]: ‹map_option (λx. node (the (remove_key a x))) (hp_parent a h) = map_option node (hp_parent a h)› for z :: ‹('a, nat) hp› by (smt (verit, ccfv_SIG) None_eq_map_option_iff distinct_mset_find_node_next distinct_mset_union find_key_None_or_itself find_key_None_remove_key_ident find_key_notin hp_child_find_key hp_child_hp_parent hp_parent_hp_child hp_parent_in_nodes hp_parent_itself in_remove_key_changed node_remove_key_itself_iff option.exhaust_sel option.map_sel option.sel option.sel remove_key_None_iff dist) have helperc1: ‹a ∈# mset_nodes m' ⟹ h = m' ⟹ find_key a m' = None ⟹ False› by (metis find_key_None_remove_key_ident in_remove_key_changed option.sel option_hd_Nil option_hd_Some_iff(1)) have helperc2: ‹ ∀x∈#mset_nodes m'. parents x = map_option node (hp_parent x m') ⟹ hp_parent x' m' = map_option (λx. the (remove_key a x)) (hp_parent x' m') ⟹ map_option node (hp_parent x' m') = map_option (λx. node (the (remove_key a x))) (hp_parent x' m')› by (metis (mono_tags, lifting) None_eq_map_option_iff map_option_cong option.map_sel option.sel) have helperc3: False if ‹remove_key a h = Some m'› and ‹hp_parent a m' = Some (the (remove_key a y))› and ‹hp_parent a h = Some y› for y :: ‹('a, nat) hp› by (metis dist that hp_parent_itself hp_parent_remove_key option.sel option.simps(2)) have helperc4: ‹map_option node (hp_parent x' h) = map_option node (map_option (λx. the (remove_key a x)) (hp_parent x' h))› if ‹remove_key a h = Some m'› and ‹hp_parent x' m' = map_option (λx. the (remove_key a x)) (hp_parent x' h)› and ‹hp_next a h = None› and ‹hp_parent a h = None› and ‹hp_prev a h = None› by (metis that find_key_None_remove_key_ident find_key_notin no_relative_ancestor_or_notin option.sel option.simps(2) remove_key_None_iff) have helperc5: ‹map_option node (hp_parent x' h) = map_option node (map_option (λx. the (remove_key a x)) (hp_parent x' h))› if ‹∀x∈#mset_nodes h. parents x = map_option node (hp_parent x h)› and ‹distinct_mset (mset_nodes h)› and ‹node m' ∈# mset_nodes h› and ‹remove_key a h = Some m'› and ‹hp_parent x' m' = map_option (λx. the (remove_key a x)) (hp_parent x' h)› and ‹x' ∉# the (map_option mset_nodes (find_key a h))› ‹node (the (None :: ('a, nat) hp option)) = x'› using that apply - apply (rule map_option_node_map_option_node_iff) apply (meson distinct_mset_hp_parent option.exhaust_sel) apply auto[] apply (smt (verit, ccfv_threshold) Duplicate_Free_Multiset.distinct_mset_mono None_eq_map_option_iff find_key_None_or_itself find_key_None_remove_key_ident hp_child_find_key hp_child_hp_parent hp_parent_hp_child hp_parent_remove_key in_remove_key_changed mset_nodes_find_key_subset node_in_mset_nodes option.map_sel option.sel option_last_Nil option_last_Some_iff(2) remove_key_notin_unchanged) done have helperc6: ‹map_option node (hp_parent x' h) = map_option (λx. node (the (remove_key a x))) (hp_parent x' h)› if ‹∀x∈#mset_nodes h. parents x = map_option node (hp_parent x h)› and ‹remove_key a h = Some m'› and ‹hp_parent x' m' = map_option (λx. the (remove_key a x)) (hp_parent x' h)› and ‹x' ∉# the (map_option mset_nodes (find_key a h))› using that dist by ((smt (verit, ccfv_SIG) Duplicate_Free_Multiset.distinct_mset_mono None_eq_map_option_iff find_key_None_or_itself find_key_None_remove_key_ident hp_child_find_key hp_child_hp_parent hp_parent_None_notin hp_parent_hp_child map_option_cong mset_nodes_find_key_subset node_in_mset_nodes node_remove_key_itself_iff option.map_sel option.sel option_last_Nil option_last_Some_iff(2) remove_key_None_iff)+)[] have helperd1: ‹hp_parent a m' = None› if ‹a ∈# mset_nodes h› and ‹find_key a h = Some m'› and ‹hp_next a h = None› and ‹hp_parent a h = None› and ‹hp_prev a h = None› by (metis that ACIDS.find_key_node_itself no_relative_ancestor_or_notin option.sel) have helperd2: ‹hp_parent a m' = None› if ‹find_key a h = Some m'› by (metis dist that Duplicate_Free_Multiset.distinct_mset_mono find_key_None_or_itself hp_parent_itself mset_nodes_find_key_subset option.sel option.simps(3)) have helperd3: ‹node ya ∉# mset_nodes m'› if ‹distinct_mset (mset_nodes m' + mset_nodes ya)› for ya :: ‹('a, nat) hp› by (smt (verit, best) that disjunct_not_in distinct_mset_add node_in_mset_nodes option.sel option.simps(3)) show ‹fst (snd (snd (snd arr'))) x' = map_option node (hp_parent x' m')› using parents dist H M' apply - apply (frule in_remove_key_in_find_keyD) apply (solves auto)[] apply (solves auto)[] unfolding union_iff apply (rule disjE, assumption) subgoal unfolding assms(1-5) arr using find_key_None_remove_key_ident[of a h] hp_parent_remove_key_other[of h a x'] distinct_mset_hp_parent[of h a ‹the (hp_parent a h)›] by (clarsimp simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def in_the_default_empty_iff intro: helper1 split: if_splits simp del: find_key_None_or_itself hp_parent_itself) (intro conjI impI allI; auto dest: helper1 helper3 dest: helperb4 hp_next_not_same_node intro: helperc1 helperc2 helperc3 dest: helperc4 helperc5 intro: helperc6)+ subgoal unfolding assms(1-5) arr using in_find_key_same_hp_parent[of x' m' h a] in_find_key_same_hp_parent2[of x' m' h a] distinct_mset_find_node_next[of h a ‹the (find_key a h)›] by (cases ‹x' = a›) (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def helperd3 map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def in_the_default_empty_iff split: if_splits simp del: find_key_None_or_itself hp_parent_itself intro: helperd1 simp: helperd2) done show ‹snd (snd (snd (snd arr'))) x' = map_option score (hp_node x' m')› using scores M' dist H hp_child_find_key[of h a x'] in_remove_key_in_nodes[of a h x'] in_find_key_notin_remove_key[of h a x'] in_find_key_in_nodes[of a h x'] hp_parent_hp_child[of h x'] hp_child_hp_parent[of h x'] hp_node_in_find_key[of h a x'] unfolding assms(1-5) arr using hp_score_remove_key_other[of h a x'] find_key_None_or_itself[of a h] hp_next_find_key_itself[of h a] has_prev_still_in_remove_key[of h a] in_remove_key_changed[of a h] hp_parent_itself[of h] remove_key_None_iff[of a h] find_key_head_node_iff[of h m'] node_remove_key_in_mset_nodes[of a h] by (auto simp add: hp_update_child_def hp_update_prev_def hp_update_nxt_def map_option.compositionality comp_def map_option_node_hp_next_remove_key hp_update_parents_def in_the_default_empty_iff split: if_splits simp del: find_key_None_or_itself hp_parent_itself) next fix x :: 'a assume ‹x ∈# ∑_# (mset_nodes `# mset [])› then show ‹fst (snd arr') x = map_option node (hp_next_children x [])› ‹fst arr' x = map_option node (hp_prev_children x [])› ‹fst (snd (snd arr')) x = map_option node (hp_child_children x [])› and ‹fst (snd (snd (snd arr'))) x = map_option node (hp_parent_children x [])› ‹snd (snd (snd (snd arr'))) x = map_option score (hp_node_children x [])› by auto next have H: ‹(∑_# (mset_nodes `# ((if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#})) + mset_nodes `# mset [])) = (∑_#(mset_nodes `# {#h#}))› using find_remove_mset_nodes_full[of h a ‹the (remove_key a h)› ‹the (find_key a h)›] find_key_None_remove_key_ident[of a h] dist apply (cases ‹find_key a h›; cases ‹remove_key a h›; auto simp: ac_simps) apply (metis find_key_head_node_iff option.sel remove_key_None_iff) done show ‹empty_outside (∑_# (mset_nodes `# ?a + mset_nodes `# mset [])) (fst arr')› using empty_outside hp_next_in_nodes2[of a h] unfolding H unfolding assms(1-5) arr by (auto simp: hp_update_parents_def hp_update_prev_def hp_update_child_def hp_update_nxt_def empty_outside_alt_def) show ‹empty_outside (∑_# (mset_nodes `# ?a + mset_nodes `# mset [])) (fst (snd (snd (snd arr'))))› using empty_outside hp_next_in_nodes2[of a h] unfolding H unfolding assms(1-5) arr by (auto simp: hp_update_parents_def hp_update_prev_def hp_update_child_def hp_update_nxt_def empty_outside_alt_def) qed qed text ‹In the kissat implementation prev and parent are merged.› lemma in_node_iff_prev_parent_or_root: assumes ‹distinct_mset (mset_nodes h)› shows ‹i ∈# mset_nodes h ⟷ hp_prev i h ≠ None ∨ hp_parent i h ≠ None ∨ i = node h› using assms proof (induction h arbitrary: i) case (Hp x1a x2a x3a) note IH = this(1) and dist = this(2) have ?case if pre:‹i ≠ x1a› ‹i ∈# sum_list (map mset_nodes x3a)› proof - obtain c where c: ‹c ∈ set x3a› and i_c: ‹i ∈#mset_nodes c› using pre unfolding in_mset_sum_list_iff by auto have dist_c: ‹distinct_mset (mset_nodes c)› using c dist by (simp add: distinct_mset_add sum_list_map_remove1) obtain ys zs where x3a_def: ‹x3a = ys @ c # zs› using split_list[OF c] by auto have i_ys: ‹i ∉# ∑_# (mset_nodes `# mset ys)› ‹i ∉# sum_list (map mset_nodes zs)› using dist i_c by (auto simp: x3a_def disjunct_not_in distinct_mset_add) have dist_c_zs: ‹distinct_mset (mset_nodes c + sum_list (map mset_nodes zs))› using WB_List_More.distinct_mset_union2 dist x3a_def by auto consider ‹i = node c› | ‹i ≠ node c› by blast then show ?case proof cases case 2 then have ‹hp_prev i c ≠ None ⟹ hp_prev_children i x3a ≠ None› using c dist i_c i_ys dist_c_zs by (auto simp: x3a_def hp_prev_children_skip_last_append[of _ ‹[_]›, simplified]) moreover have ‹hp_parent i c ≠ None ⟹ hp_parent_children i x3a ≠ None› using c dist i_c by (auto dest!: split_list simp: hp_parent_children_append_case hp_parent_children_cons split: option.splits) ultimately show ?thesis using i_c 2 IH[of c i, OF c dist_c] by (cases ‹hp_prev i c›) (auto simp del: hp_prev_None_notin hp_parent_None_notin simp: hp_parent_simps_single_if) next case 1 have ‹hp_prev_children (node c) (ys @ c # zs) = (option_last ys)› using i_ys hp_prev_children_Cons_append_found[of i ys ‹hps c› zs ‹score c›] 1 dist_c by (cases c) (auto simp del: hp_prev_children_Cons_append_found) then show ?thesis using c dist i_c i_ys dist_c_zs by (auto dest!: simp: x3a_def 1) qed qed then show ?case using dist IH by (auto simp add: hp_parent_none_children) qed lemma encoded_hp_prop_list_in_node_iff_prev_parent_or_root: assumes ‹encoded_hp_prop_list_conc arr h› and ‹snd h ≠ None› shows ‹i ∈# mset_nodes (the (snd h)) ⟷ hp_read_prev i (fst (snd arr)) ≠ None ∨ hp_read_parent i (fst (snd arr)) ≠ None ∨ Some i = snd (snd arr)› using assms in_node_iff_prev_parent_or_root[of ‹the (snd h)› i] by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def simp del: hp_prev_None_notin hp_parent_None_notin) (*TODO Move*) fun update_source_node where ‹update_source_node i (𝒱,arr,_) = (𝒱, arr, i)› fun source_node :: ‹(nat multiset × (nat,'c) hp_fun × nat option) ⇒ _› where ‹source_node (𝒱,arr,h) = h› fun hp_read_nxt' :: ‹_› where ‹hp_read_nxt' i (𝒱, arr, h) = hp_read_nxt i arr› fun hp_read_parent' :: ‹_› where ‹hp_read_parent' i (𝒱, arr, h) = hp_read_parent i arr› fun hp_read_score' :: ‹_› where ‹hp_read_score' i (𝒱, arr, h) = (hp_read_score i arr)› fun hp_read_child' :: ‹_› where ‹hp_read_child' i (𝒱, arr, h) = hp_read_child i arr› fun hp_read_prev' :: ‹_› where ‹hp_read_prev' i (𝒱, arr, h) = hp_read_prev i arr› fun hp_update_child' where ‹hp_update_child' i p(𝒱, u, h) = (𝒱, hp_update_child i p u, h)› fun hp_update_parents' where ‹hp_update_parents' i p(𝒱, u, h) = (𝒱, hp_update_parents i p u, h)› fun hp_update_prev' where ‹hp_update_prev' i p (𝒱, u, h) = (𝒱, hp_update_prev i p u, h)› fun hp_update_nxt' where ‹hp_update_nxt' i p(𝒱, u, h) = (𝒱, hp_update_nxt i p u, h)› fun hp_update_score' where ‹hp_update_score' i p(𝒱, u, h) = (𝒱, hp_update_score i p u, h)› definition maybe_hp_update_prev' where ‹maybe_hp_update_prev' child ch arr = (if child = None then arr else hp_update_prev' (the child) ch arr)› definition maybe_hp_update_nxt' where ‹maybe_hp_update_nxt' child ch arr = (if child = None then arr else hp_update_nxt' (the child) ch arr)› definition maybe_hp_update_parents' where ‹maybe_hp_update_parents' child ch arr = (if child = None then arr else hp_update_parents' (the child) ch arr)› definition maybe_hp_update_child' where ‹maybe_hp_update_child' child ch arr = (if child = None then arr else hp_update_child' (the child) ch arr)› definition unroot_hp_tree where ‹unroot_hp_tree arr h = do { ASSERT (h ∈# fst arr); let a = source_node arr; ASSERT (a ≠ None ⟶ the a ∈# fst arr); let nnext = hp_read_nxt' h arr; let parent = hp_read_parent' h arr; let prev = hp_read_prev' h arr; if prev = None ∧ parent = None ∧ Some h ≠ a then RETURN (update_source_node None arr) else if Some h = a then RETURN (update_source_node None arr) else do { ASSERT (a ≠ None); ASSERT (nnext ≠ None ⟶ the nnext ∈# fst arr); ASSERT (parent ≠ None ⟶ the parent ∈# fst arr); ASSERT (prev ≠ None ⟶ the prev ∈# fst arr); let a' = the a; let arr = maybe_hp_update_child' parent nnext arr; let arr = maybe_hp_update_nxt' prev nnext arr; let arr = maybe_hp_update_prev' nnext prev arr; let arr = maybe_hp_update_parents' nnext parent arr; let arr = hp_update_nxt' h None arr; let arr = hp_update_prev' h None arr; let arr = hp_update_parents' h None arr; let arr = hp_update_nxt' h (Some a') arr; let arr = hp_update_prev' a' (Some h) arr; RETURN (update_source_node None arr) } }› lemma unroot_hp_tree_alt_def: ‹unroot_hp_tree arr h = do { ASSERT (h ∈# fst arr); let a = source_node arr; ASSERT (a ≠ None ⟶ the a ∈# fst arr); let nnext = hp_read_nxt' h arr; let parent = hp_read_parent' h arr; let prev = hp_read_prev' h arr; if prev = None ∧ parent = None ∧ Some h ≠ a then RETURN (update_source_node None arr) else if Some h = a then RETURN (update_source_node None arr) else do { ASSERT (a ≠ None); ASSERT (nnext ≠ None ⟶ the nnext ∈# fst arr); ASSERT (parent ≠ None ⟶ the parent ∈# fst arr); ASSERT (prev ≠ None ⟶ the prev ∈# fst arr); let a' = the a; arr ← do { let arr = maybe_hp_update_child' parent nnext arr; let arr = maybe_hp_update_nxt' prev nnext arr; let arr = maybe_hp_update_prev' nnext prev arr; let arr = maybe_hp_update_parents' nnext parent arr; let arr = hp_update_nxt' h None arr; let arr = hp_update_prev' h None arr; let arr = hp_update_parents' h None arr; RETURN (update_source_node None arr) }; let arr = hp_update_nxt' h (Some a') arr; let arr = hp_update_prev' a' (Some h) arr; RETURN (arr) } }› unfolding unroot_hp_tree_def nres_monad3 Let_def apply (cases arr) by (auto intro!: bind_cong[OF refl] simp: maybe_hp_update_child'_def maybe_hp_update_nxt'_def maybe_hp_update_prev'_def maybe_hp_update_parents'_def) lemma hp_update_fst_snd: ‹hp_update_prev i j (fst (snd arr)) = fst (snd (hp_update_prev' i j arr))› ‹hp_update_nxt i j (fst (snd arr)) = fst (snd (hp_update_nxt' i j arr))› ‹hp_update_parents i j (fst (snd arr)) = fst (snd (hp_update_parents' i j arr))› ‹hp_update_child i j (fst (snd arr)) = fst (snd (hp_update_child' i j arr))› by (solves ‹cases arr; auto›)+ lemma find_remove_mset_nodes_full2: ‹distinct_mset (mset_nodes h) ⟹ sum_mset (mset_nodes `# ((if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#}))) = mset_nodes h› using find_remove_mset_nodes_full[of h a] apply (auto) apply (auto simp add: find_key_None_remove_key_ident) apply (metis find_key_head_node_iff option.sel remove_key_None_iff) done definition encoded_hp_prop_mset2_conc :: "'a::linorder multiset × ('a, 'b) hp_fun × 'a option ⇒ 'a::linorder multiset × ('a, 'b) hp multiset ⇒ bool" where ‹encoded_hp_prop_mset2_conc = (λ(𝒱, arr, h) (𝒱', x). 𝒱 = 𝒱' ∧ (encoded_hp_prop_list 𝒱 x [] arr))› lemma fst_update[simp]: ‹ fst (hp_update_prev' a b x) = fst x› ‹fst (hp_update_nxt' a b x) = fst x› ‹fst (update_source_node y x) = fst x› by (cases x;auto; fail)+ lemma encoded_hp_prop_mset2_conc_combine_list2_conc: ‹encoded_hp_prop_mset2_conc arr (𝒱, {#a,b#}) ⟹ encoded_hp_prop_list2_conc (hp_update_prev' (node b) (Some (node a)) (hp_update_nxt' (node a) (Some (node b)) (update_source_node None arr))) (𝒱, [a,b])› unfolding encoded_hp_prop_mset2_conc_def encoded_hp_prop_list2_conc_alt_def encoded_hp_prop_list_def case_prod_beta apply (intro conjI) 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 apply (cases arr) apply (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) apply (metis hp_next_None_notin hp_next_children.simps(2) hp_next_children_simps(2) hp_next_children_simps(3)) by (metis hp_next_None_notin hp_next_children.simps(2) hp_next_children_simps(2) hp_next_children_simps(3)) subgoal apply (cases arr) apply (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) apply (metis hp_prev_None_notin hp_prev_children.simps(2) hp_prev_children_simps(2) hp_prev_children_simps(3)) by (metis hp_prev_None_notin hp_prev_children.simps(2) hp_prev_children_simps(2) hp_prev_children_simps(3)) subgoal apply (cases arr) apply (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) by (metis hp_child_None_notin hp_child_children_hp_child hp_child_children_simps(2) hp_child_children_simps(3))+ subgoal apply (cases arr) apply (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) by (metis hp_parent_None_notin hp_parent_children_cons hp_parent_children_single_hp_parent option.case_eq_if) subgoal apply (cases arr) apply (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) by (metis hp_node_None_notin2 hp_node_children_Cons_if) subgoal by (cases arr) (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) subgoal by (cases arr) (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) subgoal by (cases arr) (auto simp: encoded_hp_prop_list_def hp_update_prev_def hp_update_nxt_def) done lemma update_source_node_fst_simps[simp]: ‹fst (snd (update_source_node None arr)) = fst (snd arr)› ‹fst (update_source_node None arr) = fst arr› ‹snd (snd (update_source_node None arr)) = None› by (solves ‹cases arr; auto›)+ lemma maybe_hp_update_fst_snd: ‹fst (snd (maybe_hp_update_child' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_child' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_prev' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_prev' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_nxt' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_nxt' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_parents' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_parents' (node (the b)) x arr)))› and maybe_hp_update_fst_snd2: ‹( (maybe_hp_update_child' (map_option node b) x arr')) = (if b = None then ( arr') else ( (hp_update_child' (node (the b)) x arr')))› ‹( (maybe_hp_update_prev' (map_option node b) x arr')) = (if b = None then ( arr') else ( (hp_update_prev' (node (the b)) x arr')))› ‹( (maybe_hp_update_nxt' (map_option node b) x arr')) = (if b = None then ( arr') else ( (hp_update_nxt' (node (the b)) x arr')))› ‹( (maybe_hp_update_parents' (map_option node b) x arr')) = (if b = None then ( arr') else ( (hp_update_parents' (node (the b)) x arr')))› for x b arr apply (solves ‹cases arr; auto simp: maybe_hp_update_child'_def maybe_hp_update_parents'_def maybe_hp_update_prev'_def maybe_hp_update_nxt'_def maybe_hp_update_prev'_def maybe_hp_update_nxt'_def›)+ done lemma fst_hp_update_simp[simp]: ‹fst (hp_update_prev' i x arr) = fst arr› ‹fst (hp_update_nxt' i x arr) = fst arr› ‹fst (hp_update_child' i x arr) = fst arr› ‹fst (hp_update_parents' i x arr) = fst arr› by (solves ‹cases arr; auto›)+ lemma fst_maybe_hp_update_simp[simp]: ‹fst (maybe_hp_update_prev' i y arr) = fst arr› ‹fst (maybe_hp_update_nxt' i y arr) = fst arr› ‹fst (maybe_hp_update_child' i y arr) = fst arr› ‹fst (maybe_hp_update_parents' i y arr) = fst arr› by (solves ‹cases arr; cases i; auto simp: maybe_hp_update_prev'_def maybe_hp_update_nxt'_def maybe_hp_update_child'_def maybe_hp_update_parents'_def›)+ lemma encoded_hp_prop_list_remove_find2: fixes h :: ‹('a::linorder, nat) hp› and a arr and hs :: ‹('a, nat) hp multiset› defines ‹arr₁ ≡ (if hp_parent a h = None then arr else hp_update_child' (node (the (hp_parent a h))) (map_option node (hp_next a h)) arr)› defines ‹arr₂ ≡ (if hp_prev a h = None then arr₁ else hp_update_nxt' (node (the (hp_prev a h))) (map_option node (hp_next a h)) arr₁)› defines ‹arr₃ ≡ (if hp_next a h = None then arr₂ else hp_update_prev' (node (the (hp_next a h))) (map_option node (hp_prev a h)) arr₂)› defines ‹arr₄ ≡ (if hp_next a h = None then arr₃ else hp_update_parents' (node (the (hp_next a h))) (map_option node (hp_parent a h)) arr₃)› defines ‹arr' ≡ hp_update_parents' a None (hp_update_prev' a None (hp_update_nxt' a None arr₄))› assumes enc: ‹encoded_hp_prop_mset2_conc arr (𝒱, add_mset h {#})› shows ‹encoded_hp_prop_mset2_conc arr' (𝒱, (if remove_key a h = None then {#} else {#the (remove_key a h)#}) + (if find_key a h = None then {#} else {#the (find_key a h)#}))› using encoded_hp_prop_list_remove_find[of 𝒱 h ‹fst (snd arr)› a] enc unfolding assms(1-5) apply - unfolding encoded_hp_prop_mset2_conc_def case_prod_beta hp_update_fst_snd apply (subst hp_update_fst_snd[symmetric]) apply (subst hp_update_fst_snd[symmetric]) apply (subst hp_update_fst_snd[symmetric]) unfolding maybe_hp_update_fst_snd[symmetric] maybe_hp_update_parents'_def[symmetric] maybe_hp_update_nxt'_def[symmetric] maybe_hp_update_prev'_def[symmetric] maybe_hp_update_child'_def[symmetric] encoded_hp_prop_mset2_conc_def case_prod_beta hp_update_fst_snd maybe_hp_update_fst_snd2[symmetric] maybe_hp_update_fst_snd[symmetric] by auto lemma hp_read_fst_snd_simps[simp]: ‹hp_read_nxt j (fst (snd arr)) = hp_read_nxt' j arr› ‹hp_read_prev j (fst (snd arr)) = hp_read_prev' j arr› ‹hp_read_child j (fst (snd arr)) = hp_read_child' j arr› ‹hp_read_parent j (fst (snd arr)) = hp_read_parent' j arr› ‹hp_read_score j (fst (snd arr)) = hp_read_score' j arr› by (solves ‹cases arr; auto›)+ lemma unroot_hp_tree: fixes h :: ‹(nat, nat)hp option› assumes enc: ‹encoded_hp_prop_list_conc arr (𝒱, h)› ‹a ∈# fst arr› ‹h ≠ None› shows ‹unroot_hp_tree arr a ≤ SPEC (λarr'. fst arr' = fst arr ∧ encoded_hp_prop_list2_conc arr' (𝒱, (if find_key a (the h) = None then [] else [the (find_key a (the h))]) @ (if remove_key a (the h) = None then [] else [the (remove_key a (the h))])))› proof - obtain prevs nxts childs parents scores k where arr: ‹arr = (𝒱, (prevs, nxts, childs, parents, scores), k)› and dist: ‹distinct_mset (mset_nodes (the h))› and k: ‹k = Some (node (the h))›‹the k ∈# 𝒱› and 𝒱: ‹set_mset ((mset_nodes (the h))) ⊆ set_mset 𝒱› by (cases arr; cases ‹the h›) (use assms in ‹auto simp: ac_simps encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def encoded_hp_prop_list_conc_def encoded_hp_prop_def›) have K1: ‹fst (snd (maybe_hp_update_child' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_child' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_prev' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_prev' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_nxt' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_nxt' (node (the b)) x arr)))› ‹fst (snd (maybe_hp_update_parents' (map_option node b) x arr)) = (if b = None then fst (snd arr) else fst (snd (hp_update_parents' (node (the b)) x arr)))› for x b arr apply (solves ‹cases arr; auto simp: maybe_hp_update_child'_def maybe_hp_update_parents'_def maybe_hp_update_prev'_def maybe_hp_update_nxt'_def maybe_hp_update_prev'_def maybe_hp_update_nxt'_def›)+ done have source_node_alt: ‹snd (snd arr) = source_node arr› by (cases arr) auto have KK: ‹a∈#mset_nodes (the h) ⟹ nxts a = map_option node (hp_next a (the h))› ‹a∈#mset_nodes (the h) ⟹ prevs a = map_option node (hp_prev a (the h))› ‹a∈#mset_nodes (the h) ⟹ parents a = map_option node (hp_parent a (the h))› ‹a∈#mset_nodes (the h) ⟹ childs a = map_option node (hp_child a (the h))› using enc unfolding arr encoded_hp_prop_list_conc_def by (auto simp: encoded_hp_prop_def) have KK': ‹a∈#mset_nodes (the h) ⟹ nxts a ≠ None ⟹ the (nxts a) ∈# 𝒱› ‹a∈#mset_nodes (the h) ⟹ prevs a ≠ None ⟹ the (prevs a) ∈# 𝒱› ‹a∈#mset_nodes (the h) ⟹ parents a ≠ None ⟹ the (parents a) ∈# 𝒱› ‹a∈#mset_nodes (the h) ⟹ childs a ≠ None ⟹ the (childs a) ∈# 𝒱› using enc 𝒱 KK hp_next_in_nodes2[of a ‹the h› ‹the (hp_next a (the h))›] dist hp_parent_None_notin[of a ‹the h›] hp_prev_in_nodes[of a ‹the h›] hp_parent_in_nodes[of a ‹the h›] hp_parent_hp_child[of ‹the h› a] unfolding arr encoded_hp_prop_list_conc_def apply (auto simp: encoded_hp_prop_def) by (metis hp_parent_None_notin mset_set_set_mset_msubset mset_subset_eqD option.simps(3)) have KK2: ‹fst (hp_update_parents' a None (hp_update_prev' a None (hp_update_nxt' a None (maybe_hp_update_parents' (nxts a) (parents a) (maybe_hp_update_prev' (nxts a) (Some (node z)) (maybe_hp_update_nxt' (Some (node z)) (nxts a) (maybe_hp_update_child' (parents a) (nxts a) (𝒱, (prevs, nxts, childs, parents, scores), Some (node y))))))))) = 𝒱› by auto have HH: ‹encoded_hp_prop_list 𝒱 {#the h#} [] (fst (snd (arr)))› ‹encoded_hp_prop_mset2_conc arr (𝒱, {#the h#})› using assms unfolding encoded_hp_prop_list_def encoded_hp_prop_list_conc_def encoded_hp_prop_mset2_conc_def by auto have KK3: ‹a∈#mset_nodes (the h) ⟹ remove_key a (the h) = None ∨ node (the (remove_key a (the h))) = node (the h)› by (cases ‹the h›; auto simp: ) let ?arr = ‹hp_update_parents' a None (hp_update_prev' a None (hp_update_nxt' a None (maybe_hp_update_parents' (map_option node (hp_next a (the h))) (map_option node (hp_parent a (the h))) (maybe_hp_update_prev' (map_option node (hp_next a (the h))) (map_option node (hp_prev a (the h))) (maybe_hp_update_nxt' (map_option node (hp_prev a (the h))) (map_option node (hp_next a (the h))) (maybe_hp_update_child' (map_option node (hp_parent a (the h))) (map_option node (hp_next a (the h))) arr))))))› have update_source_node_None_alt: ‹update_source_node None x = (fst x, fst (snd x), None)› for x by (cases x) auto show ?thesis using assms unfolding unroot_hp_tree_alt_def apply refine_vcg subgoal using k unfolding arr by auto subgoal using k unfolding arr by auto subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr ‹(𝒱, h)› a] unfolding source_node_alt by (auto simp add: find_key_None_remove_key_ident encoded_hp_prop_mset2_conc_def arr) (solves ‹auto simp: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_conc_def›)+ subgoal using k unfolding arr by auto subgoal unfolding hp_update_fst_snd K1[symmetric] arr encoded_hp_prop_list_conc_def encoded_hp_prop_mset2_conc_def by (auto simp: remove_key_None_iff encoded_hp_prop_list2_conc_def) subgoal unfolding hp_update_fst_snd K1[symmetric] arr encoded_hp_prop_list_conc_def encoded_hp_prop_mset2_conc_def by clarsimp subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr ‹(𝒱, h)› a] KK' unfolding arr by auto subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr ‹(𝒱, h)› a] KK' unfolding arr by auto subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr ‹(𝒱, h)› a] KK' unfolding arr by auto subgoal using k unfolding arr by auto subgoal apply ((split if_splits)+; intro impI conjI) subgoal by (simp add: find_key_None_remove_key_ident) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr ‹(𝒱, h)› a] KK' unfolding arr apply (simp add: find_key_None_remove_key_ident arr) by (metis find_key_None_remove_key_ident in_remove_key_changed option.sel option.simps(3)) subgoal by (auto simp: remove_key_None_iff encoded_hp_prop_list2_conc_def encoded_hp_prop_list_conc_def) subgoal unfolding append.append_Cons append.append_Nil apply (insert encoded_hp_prop_list_remove_find2[of ‹arr› 𝒱 ‹the h› a, OF HH(2)]) unfolding K1[symmetric] maybe_hp_update_child'_def[symmetric] maybe_hp_update_parents'_def[symmetric] maybe_hp_update_prev'_def[symmetric] maybe_hp_update_nxt'_def[symmetric] hp_update_fst_snd unfolding maybe_hp_update_fst_snd[symmetric] maybe_hp_update_parents'_def[symmetric] maybe_hp_update_nxt'_def[symmetric] maybe_hp_update_prev'_def[symmetric] maybe_hp_update_child'_def[symmetric] hp_update_fst_snd maybe_hp_update_fst_snd2[symmetric] maybe_hp_update_fst_snd[symmetric] apply (subst arg_cong[of _ _ ‹λarr. encoded_hp_prop_list2_conc arr _›]) defer apply (rule encoded_hp_prop_mset2_conc_combine_list2_conc[of ?arr 𝒱 ‹the (find_key a (the h))› ‹the (remove_key a (the h))›]) subgoal using HH(2) by (auto simp: add_mset_commute) subgoal using KK[symmetric] KK3 encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of ‹arr› ‹(𝒱, h)› a] arr k by auto done done done qed definition rescale_and_reroot where ‹rescale_and_reroot h w' arr = do { ASSERT (h ∈# fst arr); let nnext = hp_read_nxt' h arr; let parent = hp_read_parent' h arr; let prev = hp_read_prev' h arr; if source_node arr = None then RETURN (hp_update_score' h (Some w') arr) else if prev = None ∧ parent = None ∧ Some h ≠ source_node arr then RETURN (hp_update_score' h (Some w') arr) else if Some h = source_node arr then RETURN (hp_update_score' h (Some w') arr) else do { arr ← unroot_hp_tree arr h; ASSERT (h ∈# fst arr); let arr = (hp_update_score' h (Some w') arr); merge_pairs arr h } }› lemma fst_update2[simp]: ‹fst (hp_update_score' a b h) = fst h› by (cases h; auto; fail)+ lemma encoded_hp_prop_list2_conc_update_score: ‹encoded_hp_prop_list2_conc h (𝒱, [x,y]) ⟹ node x = a ⟹ encoded_hp_prop_list2_conc (hp_update_score' a (Some w') h) (𝒱, [Hp (node x) w' (hps x), y])› unfolding encoded_hp_prop_list2_conc_alt_def case_prod_beta encoded_hp_prop_list_def apply (intro conjI conjI allI impI ballI) subgoal by auto subgoal by (cases x) auto subgoal by (cases x) auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal apply (cases x; cases h) apply (clarsimp simp add: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def hp_update_score_def) by (smt (verit, ccfv_threshold) add_diff_cancel_left' add_diff_cancel_right' distinct_mset_in_diff hp.sel(1) hp_next_children.simps(2) hp_next_children_simps(1) hp_next_children_simps(2) hp_next_children_simps(3) hp_next_simps option.map(2) set_mset_union) subgoal apply (cases x; cases h) apply (clarsimp simp add: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def hp_update_score_def) by (metis (no_types, lifting) None_eq_map_option_iff Un_iff hp.sel(1) hp_prev_None_notin hp_prev_None_notin_children hp_prev_children.simps(2) hp_prev_children_simps hp_prev_simps node_in_mset_nodes option.map(2)) subgoal apply (cases x; cases h) apply (clarsimp simp add: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def hp_update_score_def) by (metis (no_types, opaque_lifting) hp_child_None_notin hp_child_children_hp_child hp_child_children_simps(2) hp_child_children_simps(3) hp_child_hd hp_child_hp_children_simps2 set_mset_union union_iff) subgoal by (cases x; cases h) (auto simp add: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def hp_update_score_def hp_parent_children_cons hp_parent_simps_single_if) subgoal apply (cases x; cases h) apply (clarsimp simp add: encoded_hp_prop_list2_conc_def encoded_hp_prop_list_def hp_update_score_def) by (metis hp_node_children_Cons_if hp_node_children_simps2) subgoal by (cases h; cases x) (auto simp: hp_update_score_def) subgoal by (cases h; cases x) (auto simp: hp_update_score_def) subgoal by (cases h; cases x) (auto simp: hp_update_score_def) done lemma encoded_hp_prop_list_conc_update_score: ‹encoded_hp_prop_list_conc arr (𝒱, Some (Hp a x2 x3)) ⟹ encoded_hp_prop_list_conc (hp_update_score' a (Some w') arr) (𝒱, Some (Hp a w' x3))› supply [simp] = hp_update_score_def unfolding encoded_hp_prop_list_conc_alt_def case_prod_beta encoded_hp_prop_list_def option.case snd_conv apply (intro conjI conjI allI impI ballI) subgoal by auto subgoal by (cases arr) auto subgoal by (cases arr) auto subgoal by (cases arr) auto subgoal by (cases arr) auto subgoal apply (cases arr) apply auto by (metis hp_child_hp_children_simps2) subgoal by (cases arr) (auto simp add: hp_parent_simps_single_if) subgoal by (cases arr) auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (cases arr) auto subgoal by (cases arr) auto subgoal by (cases arr) auto done lemma encoded_hp_prop_list_conc_update_outside: ‹(snd h ≠ None ⟹ a ∉# mset_nodes (the (snd h))) ⟹ encoded_hp_prop_list_conc arr h ⟹ encoded_hp_prop_list_conc (hp_update_score' a w' arr) h› by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_list_def hp_update_score_def split: option.splits) definition ACIDS_decrease_key' where ‹ACIDS_decrease_key' = (λa w (𝒱, h). (𝒱, ACIDS.decrease_key a w (the h)))› lemma rescale_and_reroot: fixes h :: ‹nat multiset × (nat, nat)hp option› assumes enc: ‹encoded_hp_prop_list_conc arr h› (*‹snd h ≠ None›*) shows ‹rescale_and_reroot a w' arr ≤ ⇓ {(arr, h). encoded_hp_prop_list_conc arr h} (ACIDS.mop_hm_decrease_key a w' h)› proof - let ?h = ‹snd h› have 1: ‹encoded_hp_prop_list_conc arr h ⟹ encoded_hp_prop_list_conc arr (fst h, snd h)› by (cases h) auto have src: ‹source_node arr = map_option node ?h› using enc by (auto simp: encoded_hp_prop_list_conc_def split: option.splits) show ?thesis using assms unfolding rescale_and_reroot_def ACIDS.decrease_key_def ACIDS_decrease_key'_def ACIDS.mop_hm_decrease_key_def case_prod_beta[of _ h] prod.collapse apply (refine_vcg unroot_hp_tree vsids_merge_pairs) subgoal by (auto simp: encoded_hp_prop_list_conc_def split: option.splits) subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def hp_update_score_def split: option.splits) subgoal by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def hp_update_score_def split: option.splits) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] apply (auto split: option.splits hp.splits intro!: encoded_hp_prop_list_conc_update_outside) apply (metis prod.collapse source_node.simps)+ done subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] src encoded_hp_prop_list_conc_update_score[of arr ‹fst h› a ‹score (the ?h)› ‹hps (the ?h)› w'] apply (auto split: option.splits hp.splits simp: find_key_None_remove_key_ident) apply (metis prod.collapse source_node.simps)+ done apply (rule 1; assumption) subgoal by auto subgoal by auto apply (rule encoded_hp_prop_list2_conc_update_score[of _ ‹fst h› ‹the (find_key a (the ?h))› ‹the (remove_key a (the ?h))›]) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] by (auto split: if_splits simp add: find_key_None_remove_key_ident encoded_hp_prop_list_conc_def) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] find_key_None_or_itself[of a ‹the ?h›] find_key_None_remove_key_ident[of a ‹the ?h›] by (cases ‹find_key a (the ?h)›) (auto simp del: find_key_None_or_itself) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] by (auto split: if_splits simp add: find_key_None_remove_key_ident encoded_hp_prop_list_conc_def) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] node_remove_key_itself_iff[of a ‹the ?h›] by (auto split: if_splits simp add: find_key_None_remove_key_ident encoded_hp_prop_list_conc_def) subgoal using encoded_hp_prop_list_in_node_iff_prev_parent_or_root[of arr h a] in_remove_key_changed[of a ‹the ?h›] remove_key_None_iff[of a ‹the ?h›] src find_key_None_or_itself[of a ‹the ?h›] by (cases ‹the (find_key a (the ?h))›) (clarsimp split: if_splits simp add: find_key_None_remove_key_ident simp del: ACIDS.merge_pairs.simps find_key_None_or_itself) done qed definition acids_encoded_hmrel where ‹acids_encoded_hmrel = {(arr, h). encoded_hp_prop_list_conc arr h} O ACIDS.hmrel› lemma hp_insert_spec_mop_prio_insert: assumes ‹(arr, h) ∈ acids_encoded_hmrel› shows ‹hp_insert i w arr ≤ ⇓acids_encoded_hmrel (ACIDS.mop_prio_insert i w h)› proof - obtain j where i: ‹ encoded_hp_prop_list_conc arr j› ‹(j, h) ∈ ACIDS.hmrel› using assms unfolding acids_encoded_hmrel_def by auto show ?thesis unfolding ACIDS.mop_prio_insert_def case_prod_beta acids_encoded_hmrel_def apply (refine_vcg hp_insert_spec[THEN order_trans] i) subgoal using i by (auto simp: encoded_hp_prop_list_conc_def ACIDS.hmrel_def) subgoal using i by (auto simp: encoded_hp_prop_list_conc_def ACIDS.hmrel_def) apply (rule order_trans, rule ref_two_step') apply (rule ACIDS.mop_prio_insert) apply (rule i) apply (auto simp: conc_fun_chain conc_fun_RES ACIDS.mop_prio_insert_def case_prod_beta RETURN_def) done qed lemma hp_insert_spec_mop_prio_insert2: ‹(uncurry2 hp_insert, uncurry2 ACIDS.mop_prio_insert) ∈ nat_rel ×_f nat_rel ×_f acids_encoded_hmrel →_f ⟨acids_encoded_hmrel⟩nres_rel› by (intro frefI nres_relI) (auto intro!: hp_insert_spec_mop_prio_insert[THEN order_trans]) lemma rescale_and_reroot_mop_prio_change_weight: assumes ‹(arr, h) ∈ acids_encoded_hmrel› shows ‹rescale_and_reroot a w arr ≤ ⇓acids_encoded_hmrel (ACIDS.mop_prio_change_weight a w h)› proof - obtain j where i: ‹encoded_hp_prop_list_conc arr j› ‹(j, h) ∈ ACIDS.hmrel› using assms unfolding acids_encoded_hmrel_def by auto show ?thesis apply (refine_vcg rescale_and_reroot[THEN order_trans] i) apply (rule order_trans, rule ref_two_step') apply (rule ACIDS.decrease_key_mop_prio_change_weight i)+ apply (auto simp: conc_fun_chain conc_fun_RES case_prod_beta RETURN_def acids_encoded_hmrel_def) done qed lemma rescale_and_reroot_mop_prio_change_weight2: ‹(uncurry2 rescale_and_reroot, uncurry2 ACIDS.mop_prio_change_weight) ∈ nat_rel ×_f nat_rel ×_f acids_encoded_hmrel →_f ⟨acids_encoded_hmrel⟩nres_rel› by (intro frefI nres_relI) (auto intro!: rescale_and_reroot_mop_prio_change_weight[THEN order_trans]) context hmstruct_with_prio begin definition mop_hm_is_in :: ‹_› where ‹mop_hm_is_in w = (λ(𝒜, xs). do { ASSERT (w ∈# 𝒜); RETURN (xs ≠ None ∧ w ∈# mset_nodes (the xs)) })› lemma mop_hm_is_in_mop_prio_is_in: assumes ‹(xs, ys) ∈ hmrel› shows ‹mop_hm_is_in w xs ≤ ⇓bool_rel (mop_prio_is_in w ys)› using assms unfolding mop_hm_is_in_def mop_prio_is_in_def apply (refine_vcg) subgoal by (auto simp: hmrel_def) subgoal by (auto simp: hmrel_def) done lemma del_min_None_iff: ‹del_min (Some ya) = None ⟷ mset_nodes ya = {#node ya#}› and del_min_Some_mset_nodes: ‹del_min (Some ya) = Some yb ⟹ mset_nodes ya = add_mset (node ya) (mset_nodes yb)› apply (cases ya; auto; fail) apply (cases ya; use mset_nodes_pass₂[of ‹pass₁ (hps ya)›] in auto) done lemma mset_nodes_del_min[simp]: ‹del_min (Some ya) ≠ None ⟹ mset_nodes (the (del_min (Some ya))) = remove1_mset (node ya) (mset_nodes ya)› by (cases ya; auto) lemma hp_score_del_min: ‹h ≠ None ⟹ del_min h ≠ None ⟹ distinct_mset (mset_nodes (the h)) ⟹ hp_score a (the (del_min h)) = (if a = get_min2 h then None else hp_score a (the h))› using mset_nodes_pass₂[of ‹pass₁ (hps (the h))›] apply (cases h; cases ‹the h›; cases ‹hps (the h) = []›) apply (auto simp del: mset_nodes_pass₂) by (metis hp_score_merge_pairs option.sel option.simps(2) pairing_heap_assms.pass12_merge_pairs) lemma del_min_prio_del: ‹(j, h) ∈ hmrel ⟹ fst (snd h) ≠ {#}⟹ ((fst j, del_min (snd j)), prio_del (get_min2 (snd j)) h) ∈ hmrel› using hp_score_del_min[of ‹snd j›] apply (cases ‹del_min (snd j)›) apply (auto simp: hmrel_def ACIDS.prio_del_def del_min_None_iff get_min2_alt_def del_min_Some_mset_nodes intro: invar_del_min dest: multi_member_split) apply (metis invar_del_min) apply (metis None_eq_map_option_iff option.map_sel option.sel snd_conv) done definition mop_hm_old_weight :: ‹_› where ‹mop_hm_old_weight w = (λ(𝒜, xs). do { ASSERT (w ∈# 𝒜); if xs ≠ None ∧ w ∈# mset_nodes (the xs) then RETURN (the (hp_score w (the xs))) else RES UNIV })› text ‹This requires a stronger invariant than what we want to do.› lemma mop_hm_old_weight_mop_prio_old_weight: ‹(xs, ys) ∈ hmrel ⟹ mop_hm_old_weight w xs ≤ ⇓Id (mop_prio_old_weight w ys)› unfolding mop_prio_old_weight_def mop_hm_old_weight_def mop_prio_is_in_def nres_monad3 apply refine_vcg subgoal by (auto simp: hmrel_def) subgoal by (cases ‹hp_node w (the (snd xs))›) (auto simp: union_single_eq_member hmrel_def dest!: multi_member_split[of w]) done end definition hp_is_in :: ‹_› where ‹hp_is_in w = (λbw. do { ASSERT (w ∈# fst bw); RETURN (source_node bw ≠ None ∧ (hp_read_prev' w bw ≠ None ∨ hp_read_parent' w bw ≠ None ∨ the (source_node bw) = w)) })› lemma hp_is_in: assumes ‹encoded_hp_prop_list_conc arr h› shows ‹hp_is_in i arr ≤ ⇓bool_rel (ACIDS.mop_hm_is_in i h)› proof - have dist: ‹source_node arr ≠ None ⟹ distinct_mset (mset_nodes (the (snd h)))› ‹source_node arr = None ⟷ snd h = None› using assms by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def split: option.splits) have rel: ‹hp_read_prev' i arr = map_option node (hp_prev i (the (snd h)))› ‹hp_read_parent' i arr = map_option node (hp_parent i (the (snd h)))› if ‹i ∈# fst arr› ‹snd h ≠ None› using assms that by (cases ‹i ∈# mset_nodes (the (snd h))›; auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_notin_None split: option.splits; fail)+ show ?thesis unfolding hp_is_in_def ACIDS.mop_hm_is_in_def case_prod_beta[of _ h] apply refine_vcg subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def) subgoal using rel dist assms in_node_iff_prev_parent_or_root[of ‹the (snd h)› i] apply (cases ‹source_node arr = None›) apply simp apply (simp only:) by (smt (verit, best) None_eq_map_option_iff encoded_hp_prop_list_in_node_iff_prev_parent_or_root hp_read_fst_snd_simps(2) hp_read_fst_snd_simps(4) option.collapse option.map_sel pair_in_Id_conv prod.collapse source_node.simps) done qed lemma hp_is_in_mop_prio_is_in: assumes ‹(arr, h) ∈ acids_encoded_hmrel› shows ‹hp_is_in a arr ≤ ⇓bool_rel (ACIDS.mop_prio_is_in a h)› proof - obtain j where i: ‹encoded_hp_prop_list_conc arr j› ‹(j, h) ∈ ACIDS.hmrel› using assms unfolding acids_encoded_hmrel_def by auto show ?thesis apply (refine_vcg hp_is_in[THEN order_trans] i) apply (rule order_trans, rule ref_two_step') apply (rule ACIDS.mop_hm_is_in_mop_prio_is_in i)+ apply (auto simp: conc_fun_chain conc_fun_RES case_prod_beta RETURN_def acids_encoded_hmrel_def) done qed lemma hp_is_in_mop_prio_is_in2: ‹(uncurry hp_is_in, uncurry ACIDS.mop_prio_is_in) ∈ nat_rel ×_f acids_encoded_hmrel →_f ⟨bool_rel⟩nres_rel› by (intro frefI nres_relI) (auto intro!: hp_is_in_mop_prio_is_in[THEN order_trans]) lemma vsids_pop_min2_mop_prio_pop_min: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹(arr, h) ∈ acids_encoded_hmrel› shows ‹vsids_pop_min2 arr ≤ ⇓(Id×_racids_encoded_hmrel)(ACIDS.mop_prio_pop_min h)› proof - obtain j where i: ‹encoded_hp_prop_list_conc arr j› ‹encoded_hp_prop_list_conc arr (fst j, snd j)› ‹(j, h) ∈ ACIDS.hmrel› using assms unfolding acids_encoded_hmrel_def by auto have 1: ‹SPEC (λ(ja, arr). ja = get_min2 (snd j) ∧ encoded_hp_prop_list_conc arr (fst j, ACIDS.del_min (snd j))) ≤ ⇓ (Id ×_f acids_encoded_hmrel) (do { v ← SPEC (ACIDS.prio_peek_min (fst h, fst (snd h), snd (snd h))); x ← ASSERT (v ∈# fst (snd h) ∧ v ∈# fst h); bw ← RETURN (ACIDS.prio_del v (fst h, fst (snd h), snd (snd h))); RETURN (v, bw) })› (is ‹?A ≤ ⇓ _ ?B›) if ‹fst (snd h) ≠ {#}› proof - have A: ‹?A = do { let ja = get_min2 (snd j); bw ← SPEC (λbw. encoded_hp_prop_list_conc bw (fst j, ACIDS.del_min (snd j))); RETURN (ja, bw) }› by (auto simp: RETURN_def conc_fun_RES RES_RES_RETURN_RES) have 1: ‹(get_min2 (snd j), v) ∈ Id ⟹ v ∈# fst (snd h) ∧ v ∈# fst h ⟹ encoded_hp_prop_list_conc x (fst j, ACIDS.del_min (snd j)) ⟹ (x, ACIDS.prio_del v (fst h, fst (snd h), snd (snd h))) ∈ acids_encoded_hmrel› for v x using ACIDS.del_min_prio_del[of j h] i that by (auto simp: acids_encoded_hmrel_def) show ?thesis unfolding A apply refine_vcg subgoal using i that apply (cases ‹the (snd j)›) apply (auto simp: ACIDS.prio_peek_min_def ACIDS.hmrel_def ACIDS.invar_def in_mset_sum_list_iff encoded_hp_prop_list_conc_def ACIDS.set_hp_is_hp_score_mset_nodes) apply (drule bspec, assumption) apply (subst (asm) ACIDS.set_hp_is_hp_score_mset_nodes) apply (auto simp: encoded_hp_prop_def distinct_mset_add dest!: split_list multi_member_split) by (metis hp_node_None_notin2 member_add_mset option.map_sel) apply (rule 1; assumption) subgoal by auto done qed show ?thesis unfolding ACIDS.mop_prio_pop_min_def ACIDS.mop_prio_peek_min_def ACIDS.mop_prio_del_def nres_monad2 case_prod_beta[of _ h] case_prod_beta[of _ ‹snd h›] nres_monad3 apply (refine_vcg vsids_pop_min2[THEN order_trans] i 1) subgoal using i by (auto simp: ACIDS.hmrel_def) done qed lemma vsids_pop_min2_mop_prio_pop_min2: ‹(vsids_pop_min2, ACIDS.mop_prio_pop_min) ∈ acids_encoded_hmrel →_f ⟨nat_rel ×_r acids_encoded_hmrel⟩nres_rel› by (intro frefI nres_relI) (auto intro!: vsids_pop_min2_mop_prio_pop_min[THEN order_trans]) definition mop_hp_read_score :: ‹_› where ‹mop_hp_read_score x = (λ(𝒜, w, h). do { ASSERT (x ∈# 𝒜); if hp_read_score x w ≠ None then RETURN (the (hp_read_score x w)) else RES UNIV }) › lemma mop_hp_read_score_mop_hm_old_weight: assumes ‹encoded_hp_prop_list_conc arr h› shows ‹mop_hp_read_score w arr ≤ ⇓Id (ACIDS.mop_hm_old_weight w h)› proof - show ?thesis unfolding mop_hp_read_score_def ACIDS.mop_hm_old_weight_def RETURN_def RES_RES_RETURN_RES Many_More.if_f apply refine_vcg subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def) subgoal using assms by (auto simp: encoded_hp_prop_list_conc_def encoded_hp_prop_def split: option.splits) done qed lemma mop_hp_read_score_mop_prio_old_weight: fixes arr :: ‹'a::linorder multiset × ('a, nat) hp_fun × 'a option› assumes ‹(arr, h) ∈ acids_encoded_hmrel› shows ‹mop_hp_read_score w arr ≤ ⇓(Id)(ACIDS.mop_prio_old_weight w h)› proof - obtain j where i: ‹encoded_hp_prop_list_conc arr j› ‹encoded_hp_prop_list_conc arr (fst j, snd j)› ‹(j, h) ∈ ACIDS.hmrel› using assms unfolding acids_encoded_hmrel_def by auto show ?thesis apply (rule mop_hp_read_score_mop_hm_old_weight[THEN order_trans] i)+ subgoal by (rule ref_two_step' ACIDS.mop_hm_old_weight_mop_prio_old_weight[THEN order_trans] i)+ auto done qed lemma mop_hp_read_score_mop_prio_old_weight2: ‹(uncurry mop_hp_read_score, uncurry ACIDS.mop_prio_old_weight) ∈ nat_rel ×_r acids_encoded_hmrel →_f ⟨Id⟩nres_rel› by (intro frefI nres_relI) (auto intro!: mop_hp_read_score_mop_prio_old_weight[THEN order_trans]) thm ACIDS.mop_prio_insert_raw_unchanged_def thm ACIDS.mop_prio_insert_maybe_def (*covered by ACIDS.mop_prio_change_weight and ACIDS.mop_prio_insert *) term ACIDS.prio_peek_min (*TODO remove: unused as acids_get_min*) thm ACIDS.mop_prio_old_weight_def thm ACIDS.mop_prio_insert_raw_unchanged_def term ACIDS.mop_prio_insert_unchanged(*covered by the two previous ones*) end

Theory Pairing_Heap_LLVM.Relational_Pairing_Heaps