Theory Pairing_Heap_LLVM.Pairing_Heaps

theory Pairing_Heaps
  imports Ordered_Pairing_Heap_List2
    Isabelle_LLVM.IICF
    More_Sepref.WB_More_Refinement
    Heaps_Abs
begin

section ‹Pairing Heaps›

subsection ‹Genealogy Over Pairing Heaps›

text ‹We first tried to use the heapmap, but this attempt was a terrible failure, because as useful
the heapmap is parametrized by the size. This might be useful in some contexts, but I consider this
to be the most terrible idea ever, based on past experience. So instead I went for a modification
of the pairing heaps.

To increase fun, we reuse the trick from VSIDS to represent the pairing heap inside an array in
order to avoid allocation yet another array. As a side effect, it also avoids including the label
inside the node (because per definition, the label is exactly the index).
But maybe pointers are actually better, because by definition in Isabelle no graph is shared.
›

fun mset_nodes :: "('b, 'a) hp ⇒'b multiset" where
"mset_nodes (Hp x _ hs) = {#x#} + ∑⇩# (mset_nodes `# mset hs)"

context pairing_heap_assms
begin

lemma mset_nodes_link[simp]: ‹mset_nodes (link a b) = mset_nodes a + mset_nodes b›
  by (cases a; cases b)
   auto

lemma mset_nodes_merge_pairs: ‹merge_pairs a ≠ None ⟹ mset_nodes (the (merge_pairs a)) = sum_list (map mset_nodes a)›
  apply (induction a rule: merge_pairs.induct)
  subgoal by auto
  subgoal by auto
  subgoal for h1 h2 hs
    by (cases hs)
     (auto simp: Let_def split: option.splits)
  done

lemma mset_nodes_pass⇩1[simp]: ‹sum_list (map mset_nodes (pass⇩1 a)) = sum_list (map mset_nodes a)›
  apply (induction a rule: pass⇩1.induct)
  subgoal by auto
  subgoal by auto
  subgoal for h1 h2 hs
    by (cases hs)
     (auto simp: Let_def split: option.splits)
  done


lemma mset_nodes_pass⇩2[simp]: ‹pass⇩2 a ≠ None ⟹ mset_nodes (the (pass⇩2 a)) = sum_list (map mset_nodes a)›
  apply (induction a rule: pass⇩1.induct)
  subgoal by auto
  subgoal by auto
  subgoal for h1 h2 hs
    by (cases hs)
     (auto simp: Let_def split: option.splits)
  done

end

lemma mset_nodes_simps[simp]: ‹mset_nodes (Hp x n hs) = {#x#} + (sum_list (map mset_nodes hs))›
  by auto

lemmas [simp del] = mset_nodes.simps

fun hp_next where
  ‹hp_next a (Hp m s (x # y # children)) = (if a = node x then Some y else (case hp_next a x of Some a ⇒ Some a | None ⇒ hp_next a (Hp m s (y # children))))› |
  ‹hp_next a (Hp m s [b]) = hp_next a b› |
  ‹hp_next a (Hp m s []) = None›

lemma [simp]: ‹size_list size (hps x) < Suc (size x + a)›
  by (cases x) auto

fun hp_prev where
  ‹hp_prev a (Hp m s (x # y # children)) = (if a = node y then Some x else (case hp_prev a x of Some a ⇒ Some a | None ⇒ hp_prev a (Hp m s (y # children))))› |
  ‹hp_prev a (Hp m s [b]) = hp_prev a b› |
  ‹hp_prev a (Hp m s []) = None›

fun hp_child where
  ‹hp_child a (Hp m s (x # children)) = (if a = m then Some x else (case hp_child a x of None ⇒ hp_child a (Hp m s children) | Some a ⇒ Some a))› |
  ‹hp_child a (Hp m s _) = None›

fun hp_node where
  ‹hp_node a (Hp m s (x#children)) = (if a = m then Some (Hp m s (x#children)) else (case hp_node a x of None ⇒ hp_node a (Hp m s children) | Some a ⇒ Some a))› |
  ‹hp_node a (Hp m s []) = (if a = m then Some (Hp m s []) else None)›

lemma node_in_mset_nodes[simp]: ‹node x ∈# mset_nodes x›
  by (cases x; auto)

lemma hp_next_None_notin[simp]: ‹m ∉# mset_nodes a ⟹ hp_next m a = None›
  by (induction m a rule: hp_next.induct) auto

lemma hp_prev_None_notin[simp]: ‹m ∉# mset_nodes a ⟹ hp_prev m a = None›
  by (induction m a rule: hp_prev.induct) auto

lemma hp_child_None_notin[simp]: ‹m ∉# mset_nodes a ⟹ hp_child m a = None›
  by (induction m a rule: hp_child.induct) auto

lemma hp_node_None_notin2[iff]: ‹hp_node m a = None ⟷ m ∉# mset_nodes a›
  by (induction m a rule: hp_node.induct) auto

lemma hp_node_None_notin[simp]: ‹m ∉# mset_nodes a ⟹ hp_node m a = None›
  by auto

lemma hp_node_simps[simp]: ‹hp_node m (Hp m w⇩m ch⇩m) = Some (Hp m w⇩m ch⇩m)›
  by (cases ch⇩m) auto

lemma hp_next_None_notin_children[simp]: ‹a ∉# sum_list (map mset_nodes children) ⟹
  hp_next a (Hp m w⇩m (children)) = None›
  by (induction a ‹Hp m w⇩m children› arbitrary:children rule: hp_next.induct) auto

lemma hp_prev_None_notin_children[simp]: ‹a ∉# sum_list (map mset_nodes children) ⟹
  hp_prev a (Hp m w⇩m (children)) = None›
  by (induction a ‹Hp m w⇩m children› arbitrary:children rule: hp_prev.induct) auto

lemma hp_child_None_notin_children[simp]: ‹a ∉# sum_list (map mset_nodes children) ⟹ a ≠ m ⟹
  hp_child a (Hp m w⇩m (children)) = None›
  by (induction a ‹Hp m w⇩m children› arbitrary:children rule: hp_next.induct) auto

text ‹The function above are nicer for definition than for usage. Instead we define the list version
and change the simplification lemmas. We initially tried to use a recursive function, but the
proofs did not go through (and it seemed that the induction principle were to weak).›
fun hp_next_children where
  ‹hp_next_children a (x # y # children) = (if a = node x then Some y else (case hp_next a x of Some a ⇒ Some a | None ⇒ hp_next_children a (y # children)))› |
  ‹hp_next_children a [b] = hp_next a b› |
  ‹hp_next_children a [] = None›

lemma hp_next_simps[simp]:
  ‹hp_next a (Hp m s children) = hp_next_children a children›
  by (induction a children rule: hp_next_children.induct) (auto split: option.splits)

lemma hp_next_children_None_notin[simp]: ‹m ∉# ∑⇩# (mset_nodes `# mset children) ⟹ hp_next_children m children = None›
  by (induction m children rule: hp_next_children.induct) auto

lemma [simp]: ‹distinct_mset (mset_nodes a) ⟹ hp_next (node a) a = None›
  by (induction a) auto

lemma [simp]:
  ‹ch⇩m ≠ [] ⟹ hp_next_children (node a) (a # ch⇩m) = Some (hd ch⇩m)›
  by (cases ch⇩m) auto

fun hp_prev_children where
  ‹hp_prev_children a (x # y # children) = (if a = node y then Some x else (case hp_prev a x of Some a ⇒ Some a | None ⇒ hp_prev_children a (y # children)))› |
  ‹hp_prev_children a [b] = hp_prev a b› |
  ‹hp_prev_children a [] = None›

lemma hp_prev_simps[simp]:
  ‹hp_prev a (Hp m s children) = hp_prev_children a children›
  by (induction a children rule: hp_prev_children.induct) (auto split: option.splits)

lemma hp_prev_children_None_notin[simp]: ‹m ∉# ∑⇩# (mset_nodes `# mset children) ⟹ hp_prev_children m children = None›
  by (induction m children rule: hp_prev_children.induct) auto

lemma [simp]: ‹distinct_mset (mset_nodes a) ⟹ hp_prev (node a) a = None›
  by (induction a) auto

lemma hp_next_in_first_child [simp]: ‹distinct_mset (sum_list (map mset_nodes ch⇩m) + (mset_nodes a)) ⟹
  xa ∈# mset_nodes a ⟹ xa ≠ node a ⟹
  hp_next_children xa (a # ch⇩m) = (hp_next xa a)›
  by (cases ch⇩m) (auto split: option.splits dest!: multi_member_split)

lemma hp_next_skip_hd_children:
  ‹distinct_mset (sum_list (map mset_nodes ch⇩m) + (mset_nodes a)) ⟹ xa ∈# ∑⇩# (mset_nodes `# mset ch⇩m) ⟹
  xa ≠ node a ⟹ hp_next_children xa (a # ch⇩m) = hp_next_children xa (ch⇩m)›
  apply (cases ch⇩m)
  apply (auto split: option.splits dest!: multi_member_split)
  done

lemma hp_prev_in_first_child [simp]: ‹distinct_mset
  (sum_list (map mset_nodes ch⇩m) + (mset_nodes a)) ⟹ xa ∈# mset_nodes a ⟹ hp_prev_children xa (a # ch⇩m) = hp_prev xa a›
  by (cases ch⇩m) (auto split: option.splits dest!: multi_member_split)

lemma hp_prev_skip_hd_children:
  ‹distinct_mset (sum_list (map mset_nodes ch⇩m) + (mset_nodes a)) ⟹ xa ∈# ∑⇩# (mset_nodes `# mset ch⇩m) ⟹
  xa ≠ node (hd ch⇩m) ⟹ hp_prev_children xa (a # ch⇩m) = hp_prev_children xa ch⇩m›
  apply (cases ch⇩m)
  apply (auto split: option.splits dest!: multi_member_split)
  done

lemma node_hd_in_sum[simp]: ‹ch⇩m ≠ [] ⟹ node (hd ch⇩m) ∈# sum_list (map mset_nodes ch⇩m)›
  by (cases ch⇩m) auto

lemma hp_prev_cadr_node[simp]: ‹ch⇩m ≠ [] ⟹ hp_prev_children (node (hd ch⇩m)) (a # ch⇩m) = Some a›
  by (cases ch⇩m) auto

lemma hp_next_children_simps[simp]:
   ‹a = node x ⟹ hp_next_children a (x # y # children) = Some y›
   ‹a ≠ node x ⟹ hp_next a x ≠ None ⟹ hp_next_children a (x # children) = hp_next a x›
   ‹a ≠ node x ⟹ hp_next a x = None ⟹ hp_next_children a (x # children) = hp_next_children a (children)›
  apply (solves auto)
  apply (solves ‹cases children; auto›)+
  done

lemma hp_prev_children_simps[simp]:
   ‹a = node y ⟹ hp_prev_children a (x # y # children) = Some x›
   ‹a ≠ node y ⟹ hp_prev a x ≠ None ⟹ hp_prev_children a (x # y # children) = hp_prev a x›
   ‹a ≠ node y ⟹ hp_prev a x = None ⟹ hp_prev_children a (x # y # children) = hp_prev_children a (y # children)›
  by auto

lemmas [simp del] =  hp_next_children.simps(1) hp_next.simps(1) hp_prev.simps(1) hp_prev_children.simps(1)

lemma hp_next_children_skip_first_append[simp]:
  ‹xa ∉# ∑⇩# (mset_nodes `# mset ch) ⟹ hp_next_children xa (ch @ ch') = hp_next_children xa ch'›
  apply (induction xa ch rule: hp_next_children.induct)
  subgoal
    by (auto simp: hp_next_children.simps(1))
  subgoal
    by (cases ch')
      (auto simp: hp_next_children.simps(1))
  subgoal by auto
  done

lemma hp_prev_children_skip_first_append[simp]:
  ‹xa ∉# ∑⇩# (mset_nodes `# mset ch) ⟹ xa ≠ node m ⟹ hp_prev_children xa (ch @ m # ch') = hp_prev_children xa (m#ch')›
  apply (induction xa ch rule: hp_prev_children.induct)
  subgoal
    by (auto simp: hp_prev_children.simps(1))
  subgoal
    by (auto simp: hp_prev_children.simps(1))
  subgoal by auto
  done

lemma hp_prev_children_skip_Cons[simp]:
  ‹xa ∉# ∑⇩# (mset_nodes `# mset ch') ⟹ xa ∈# mset_nodes m ⟹ hp_prev_children xa (m # ch') = hp_prev xa m›
  apply (induction ch')
  subgoal
    by (auto simp: hp_prev_children.simps(1) split: option.splits)
  subgoal
    by (auto simp: hp_prev_children.simps(1) split: option.splits)
  done

definition hp_child_children where
  ‹hp_child_children a = option_hd o (List.map_filter (hp_child a))›

lemma hp_child_children_Cons_if:
  ‹hp_child_children a (x # y) = (if hp_child a x = None then hp_child_children a y else hp_child a x)›
  by (auto simp: hp_child_children_def List.map_filter_def split: list.splits)

lemma hp_child_children_simps[simp]:
  ‹hp_child_children a [] = None›
  ‹hp_child a x =None ⟹ hp_child_children a (x # y) = hp_child_children a y›
  ‹hp_child a x ≠ None ⟹ hp_child_children a (x # y) = hp_child a x›
  by (auto simp: hp_child_children_def List.map_filter_def split: list.splits)

lemma hp_child_hp_children_simps2[simp]:
  ‹x ≠ a ⟹ hp_child x (Hp a b child) = hp_child_children x child›
  by (induction child) (auto split: option.splits)

lemma hp_child_children_None_notin[simp]: ‹m ∉# ∑⇩# (mset_nodes `# mset children) ⟹ hp_child_children m children = None›
  by (induction children) auto

definition hp_node_children where
  ‹hp_node_children a = option_hd o (List.map_filter (hp_node a))›

lemma hp_node_children_Cons_if:
  ‹hp_node_children a (x # y) = (if hp_node a x = None then hp_node_children a y else hp_node a x)›
  by (auto simp: hp_node_children_def List.map_filter_def split: list.splits)

lemma hp_node_children_simps[simp]:
  ‹hp_node_children a [] = None›
  ‹hp_node a x =None ⟹ hp_node_children a (x # y) = hp_node_children a y›
  ‹hp_node a x ≠ None ⟹ hp_node_children a (x # y) = hp_node a x›
  by (auto simp: hp_node_children_def List.map_filter_def split: list.splits)

lemma hp_node_children_simps2[simp]:
  ‹x ≠ a ⟹ hp_node x (Hp a b child) = hp_node_children x child›
  by (induction child) (auto split: option.splits)

lemma hp_node_children_None_notin2: ‹hp_node_children m children = None ⟷ m ∉# ∑⇩# (mset_nodes `# mset children)›
  apply (induction children)
  apply auto
  by (metis hp_node_children_simps(2) hp_node_children_simps(3) option_last_Nil option_last_Some_iff(2))

lemma hp_node_children_None_notin[simp]: ‹m ∉# ∑⇩# (mset_nodes `# mset children) ⟹ hp_node_children m children = None›
  by (induction children) auto


lemma hp_next_children_hd_simps[simp]:
  ‹a = node x ⟹ distinct_mset (sum_list (map mset_nodes (x # children))) ⟹
  hp_next_children a (x # children) = option_hd children›
  by (cases children) auto

lemma hp_next_children_simps_if:
  ‹ distinct_mset (sum_list (map mset_nodes (x # children))) ⟹
  hp_next_children a (x # children) = (if a = node x then option_hd children else case hp_next a x of None ⇒ hp_next_children a children | a ⇒ a)›
  by (cases children) (auto split: if_splits option.splits)


lemma hp_next_children_skip_end[simp]:
  ‹n ∈# mset_nodes a ⟹ n ≠ node a ⟹ n ∉# sum_list (map mset_nodes b) ⟹ 
  distinct_mset (mset_nodes a) ⟹
  hp_next_children n (a # b) = hp_next n a›
  by (induction b) (auto simp add: hp_next_children.simps(1) split: option.splits)

lemma hp_next_children_append2[simp]:
  ‹x ≠ n ⟹ x ∉# sum_list (map mset_nodes ch⇩m) ⟹ hp_next_children x (Hp n w⇩n ch⇩n # ch⇩m) = hp_next_children x ch⇩n›
  by (cases ch⇩m) (auto simp: hp_next_children.simps(1) split: option.splits)

lemma hp_next_children_skip_Cons_append[simp]:
  ‹NO_MATCH [] b ⟹ x ∈# sum_list (map mset_nodes a) ⟹
  distinct_mset (sum_list (map mset_nodes (a @ m # b))) ⟹
  hp_next_children x (a @ m # b) = hp_next_children x (a @ m # [])›
  apply (induction x a rule: hp_next_children.induct)
  apply (auto simp: hp_next_children.simps(1) distinct_mset_add split: option.splits)
  apply (metis (no_types, lifting) add_mset_disjoint(1) hp_next_children.simps(2)
    hp_next_children_None_notin hp_next_children_simps(2) hp_next_children_simps(3)
    hp_next_children_skip_first_append mset_add node_in_mset_nodes sum_image_mset_sum_map union_iff)
  by (metis add_mset_disjoint(1) hp_next_None_notin hp_next_children_None_notin
    hp_next_children_simps(3) insert_DiffM node_in_mset_nodes sum_image_mset_sum_map union_iff)

lemma hp_next_children_append_single_remove_children:
  ‹NO_MATCH [] ch⇩m ⟹ x ∈# sum_list (map mset_nodes a) ⟹
     distinct_mset (sum_list (map mset_nodes (a @ [Hp m w⇩m ch⇩m]))) ⟹
     map_option node (hp_next_children x (a @ [Hp m w⇩m ch⇩m])) =
     map_option node (hp_next_children x (a @ [Hp m w⇩m []]))›
  apply (induction x a rule: hp_next_children.induct)
  apply (auto simp: hp_next_children.simps(1) distinct_mset_add split: option.splits)
  apply (smt (verit, ccfv_threshold) distinct_mset_add hp_next_None_notin hp_next_children.simps(2)
    hp_next_children_simps(3) hp_next_children_skip_first_append hp_next_in_first_child hp_next_simps
    node_in_mset_nodes sum_image_mset_sum_map union_assoc union_commute)
  apply (simp add: disjunct_not_in)
  done

lemma hp_prev_children_first_child[simp]:
  ‹m ≠ n ⟹ n ∉# sum_list (map mset_nodes b) ⟹  n ∉# sum_list (map mset_nodes ch⇩n) ⟹
   n ∈# sum_list (map mset_nodes child) ⟹
  hp_prev_children n (Hp m w⇩m child # b) = hp_prev_children n child›
  by (cases b) (auto simp: hp_prev_children.simps(1) split: option.splits)

lemma hp_prev_children_skip_last_append[simp]:
  ‹NO_MATCH [] ch' ⟹
     distinct_mset (sum_list (map mset_nodes (ch @ch'))) ⟹
  xa ∉# ∑⇩# (mset_nodes `# mset ch') ⟹ xa ∈# ∑⇩# (mset_nodes `# mset (ch )) ⟹ hp_prev_children xa (ch @ ch') = hp_prev_children xa (ch)›
  apply (induction xa ch rule: hp_prev_children.induct)
  subgoal for a x y children
    by (subgoal_tac ‹distinct_mset (sum_list (map mset_nodes ((y # children) @ ch')))›)
     (auto simp: hp_prev_children.simps(1) dest!: multi_member_split split: option.splits
      dest: WB_List_More.distinct_mset_union2)
  subgoal
    by (auto simp: hp_prev_children.simps(1) split: option.splits dest: multi_member_split)
  subgoal by auto
  done

lemma hp_prev_children_Cons_append_found[simp]:
  ‹m ∉# sum_list (map mset_nodes a) ⟹ m ∉# sum_list (map mset_nodes ch) ⟹  m ∉# sum_list (map mset_nodes b) ⟹ hp_prev_children m (a @ Hp m w⇩m ch # b) = option_last a›
  by (induction m a rule: hp_prev_children.induct)
   (auto simp: hp_prev_children.simps(1))


lemma hp_prev_children_append_single_remove_children:
  ‹NO_MATCH [] ch⇩m ⟹ x ∈# sum_list (map mset_nodes a) ⟹
     distinct_mset (sum_list (map mset_nodes (Hp m w⇩m ch⇩m # a))) ⟹
     map_option node (hp_prev_children x (Hp m w⇩m ch⇩m # a)) =
     map_option node (hp_prev_children x (Hp m w⇩m [] # a))›
  by (induction a) (auto simp: hp_prev_children.simps(1) distinct_mset_add split: option.splits
    dest!: multi_member_split)

lemma map_option_skip_in_child:
  ‹distinct_mset (sum_list (map mset_nodes ch⇩m) + (sum_list (map mset_nodes ch⇩n) + sum_list (map mset_nodes a))) ⟹ m ∉# sum_list (map mset_nodes ch⇩m) ⟹
  ch⇩m ≠ [] ⟹
  hp_prev_children (node (hd ch⇩m)) (a @ [Hp m w⇩m (Hp n w⇩n ch⇩n # ch⇩m)]) = Some (Hp n w⇩n ch⇩n)›
  apply (induction ‹node (hd ch⇩m)› a rule: hp_prev_children.induct)
  subgoal for x y children
    by (cases x; cases y)
     (auto simp add: hp_prev_children.simps(1) disjunct_not_in distinct_mset_add
      split: option.splits)
  subgoal for b
    by (cases b)
     (auto simp: hp_prev_children.simps(1) disjunct_not_in distinct_mset_add
      split: option.splits)
  subgoal by auto
  done



lemma hp_child_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_child_children x (ch @ ch') = hp_child_children x ch'›
  apply (induction ch)
  apply (auto simp: hp_child_children_Cons_if dest!: multi_member_split)
  by (metis WB_List_More.distinct_mset_union2 union_ac(1))

lemma hp_child_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_child_children x (ch @ ch') = hp_child_children x ch›
  apply (induction ch)
  apply (auto simp: hp_child_children_Cons_if dest!: multi_member_split)
  by (metis WB_List_More.distinct_mset_union2 union_ac(1))

lemma hp_child_children_skip_last_in_first:
  ‹distinct_mset (sum_list (map mset_nodes (Hp m w⇩m (Hp n w⇩n ch⇩n # ch⇩m) # b))) ⟹
  hp_child_children n (Hp m w⇩m (Hp n w⇩n ch⇩n # ch⇩m) # b) = hp_child n (Hp m w⇩m (Hp n w⇩n ch⇩n # ch⇩m))›
  by (auto simp: hp_child_children_Cons_if split: option.splits)

lemma hp_child_children_hp_child[simp]: ‹hp_child_children x [a] = hp_child x a›
  by (auto simp: hp_child_children_def List.map_filter_def)

lemma hp_next_children_last[simp]:
  ‹distinct_mset (sum_list (map mset_nodes a)) ⟹ a ≠ [] ⟹
  hp_next_children (node (last a)) (a @ b) = option_hd b›
  apply (induction ‹node (last a)› a rule: hp_next_children.induct)
  apply (auto simp: hp_next_children.simps(1) dest: multi_member_split)
  apply (metis add_diff_cancel_right' distinct_mset_in_diff node_in_mset_nodes)
  apply (metis add_diff_cancel_right' distinct_mset_in_diff node_in_mset_nodes)
  apply (metis Duplicate_Free_Multiset.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff empty_append_eq_id hp_next_None_notin node_in_mset_nodes option.simps(4))
  apply (metis Misc.last_in_set add_diff_cancel_left' distinct_mem_diff_mset node_in_mset_nodes sum_list_map_remove1 union_iff)
  apply (metis (no_types, lifting) add_diff_cancel_left' append_butlast_last_id distinct_mem_diff_mset distinct_mset_add inter_mset_empty_distrib_right list.distinct(2) list.sel(1) map_append node_hd_in_sum node_in_mset_nodes sum_list.append)
  apply (metis add_diff_cancel_right' append_butlast_last_id distinct_mset_add distinct_mset_in_diff hp_next_None_notin list.sel(1) map_append node_hd_in_sum not_Cons_self2 option.case(1) sum_list.append union_iff)
  by (metis (no_types, lifting) arith_simps(50) hp_next_children_hd_simps hp_next_children_simps(1) list.exhaust list.sel(1) list.simps(8) list.simps(9) option_hd_Some_iff(1) sum_list.Cons sum_list.Nil)



lemma hp_next_children_skip_last_not_last:
  ‹distinct_mset (sum_list (map mset_nodes a) + sum_list (map mset_nodes b))  ⟹
  a ≠ [] ⟹
     x ≠ node (last a) ⟹ x ∈# sum_list (map mset_nodes a) ⟹
  hp_next_children x (a @ b) = hp_next_children x a›
  apply (cases a rule: rev_cases)
  subgoal by auto
  subgoal for ys y
    apply (cases ‹x ∉# mset_nodes (last a)›)
    subgoal by (auto simp: ac_simps)
    subgoal
      apply auto
      apply (subst hp_next_children_skip_first_append)
      apply (auto simp: ac_simps)
      using distinct_mset_in_diff apply fastforce
      using distinct_mset_in_diff distinct_mset_union by fastforce
      done
  done

lemma hp_node_children_append_case:
  ‹hp_node_children x (a @ b) = (case hp_node_children x a of None ⇒ hp_node_children x b | x ⇒ x)›
   by (auto simp: hp_node_children_def List.map_filter_def split: option.splits)

lemma hp_node_children_append[simp]:
  ‹hp_node_children x a = None ⟹ hp_node_children x (a @ b) = hp_node_children x b›
  ‹hp_node_children x a ≠ None ⟹ hp_node_children x (a @ b) = hp_node_children x a›
   by (auto simp: hp_node_children_append_case)

lemma ex_hp_node_children_Some_in_mset_nodes:
  ‹(∃y. hp_node_children xa a = Some y) ⟷ xa ∈# sum_list (map mset_nodes a)›
  using hp_node_children_None_notin2[of xa a] by auto

hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC

lemma hp_node_node_itself[simp]: ‹hp_node (node x2) x2 = Some x2›
  by (cases x2; cases ‹hps x2›) auto

lemma hp_child_hd[simp]: ‹hp_child x1 (Hp x1 x2 x3) = option_hd x3›
  by (cases x3) auto

(*TODO Move*)
lemma drop_is_single_iff: ‹drop e xs = [a] ⟷ last xs = a ∧ e = length xs - 1 ∧ xs ≠ []›
  apply auto
  apply (metis append_take_drop_id last_snoc)
  by (metis diff_diff_cancel diff_is_0_eq' length_drop length_list_Suc_0 n_not_Suc_n nat_le_linear)

(*TODO this is the right ordering for the theorems*)
lemma distinct_mset_mono': ‹distinct_mset D ⟹ D' ⊆# D ⟹ distinct_mset D'›
  by (metis distinct_mset_union subset_mset.le_iff_add)

context pairing_heap_assms
begin

lemma pass⇩1_append_even: ‹even (length xs) ⟹ pass⇩1 (xs @ ys) = pass⇩1 xs @ pass⇩1 ys›
  by (induction xs rule: pass⇩1.induct) auto

lemma pass⇩2_None_iff[simp]: ‹pass⇩2 list = None ⟷ list = []›
  by (cases list)
   auto

lemma last_pass⇩1[simp]: "odd (length xs) ⟹ last (pass⇩1 xs) = last xs"
  by (metis pass⇩1.simps(2) append_butlast_last_id even_Suc last_snoc length_append_singleton
    length_greater_0_conv odd_pos pass⇩1_append_even)
end

lemma get_min2_alt_def: ‹get_min2 (Some h) = node h›
  by (cases h) auto

fun hp_parent :: ‹'a ⇒ ('a, 'b) hp ⇒ ('a, 'b)hp option› where
  ‹hp_parent n (Hp a sc (x # children)) = (if n = node x then Some (Hp a sc (x # children)) else map_option the (option_hd (filter ((≠) None) (map (hp_parent n) (x#children)))))› |
  ‹hp_parent n _ = None›

definition hp_parent_children :: ‹'a ⇒ ('a, 'b) hp list ⇒ ('a, 'b)hp option› where
  ‹hp_parent_children n xs =  map_option the (option_hd (filter ((≠) None) (map (hp_parent n) xs)))›


lemma hp_parent_None_notin[simp]: ‹m ∉# mset_nodes a ⟹ hp_parent m a = None›
  apply (induction m a rule: hp_parent.induct)
  apply (auto simp: filter_empty_conv)
  by (metis node_in_mset_nodes sum_list_map_remove1 union_iff)

lemma hp_parent_children_None_notin[simp]: ‹(m) ∉# sum_list (map mset_nodes a) ⟹ hp_parent_children m a = None›
  by (induction a)
   (auto simp: filter_empty_conv hp_parent_children_def)

lemma hp_parent_children_cons: ‹hp_parent_children a (x # children) = (case hp_parent a x of None ⇒ hp_parent_children a children | Some a ⇒ Some a)›
  by (auto simp: hp_parent_children_def)

lemma hp_parent_simps_if:
  ‹hp_parent n (Hp a sc (x # children)) = (if n = node x then Some (Hp a sc (x # children)) else hp_parent_children n (x#children))›
  by (auto simp: hp_parent_children_def)

lemmas [simp del] = hp_parent.simps(1)

lemma hp_parent_simps:
  ‹n = node x ⟹ hp_parent n (Hp a sc (x # children)) = Some (Hp a sc (x # children))›
  ‹n ≠ node x ⟹ hp_parent n (Hp a sc (x # children)) = hp_parent_children n (x # children)›
  by (auto simp: hp_parent_simps_if)

lemma hp_parent_itself[simp]: ‹distinct_mset (mset_nodes x) ⟹ hp_parent (node x) x = None›
  by (cases ‹(node x, x)› rule: hp_parent.cases)
   (auto simp: hp_parent.simps hp_parent_children_def filter_empty_conv sum_list_map_remove1)

lemma hp_parent_children_itself[simp]:
  ‹distinct_mset (mset_nodes x + sum_list (map mset_nodes children)) ⟹ hp_parent_children (node x) (x # children) = None›
  by (auto simp: hp_parent_children_def filter_empty_conv disjunct_not_in distinct_mset_add sum_list_map_remove1 dest: distinct_mset_union)

lemma hp_parent_in_nodes: ‹hp_parent n x ≠ None ⟹ node (the (hp_parent n x)) ∈# mset_nodes x›
  apply (induction n x rule: hp_parent.induct)
  subgoal premises p for n a sc x children
    using p p(1)[of xa]
    apply (auto simp: hp_parent.simps)
    apply (cases ‹filter (λy. ∃ya. y = Some ya) (map (hp_parent n) children)›)
    apply (fastforce simp: filter_empty_conv filter_eq_Cons_iff map_eq_append_conv)+
    done
  subgoal for n v va
    by (auto simp: hp_parent.simps filter_empty_conv)
  done

lemma hp_parent_children_Some_iff:
  ‹hp_parent_children a xs = Some y ⟷ (∃u b as. xs = u @ b # as ∧ (∀x∈set u. hp_parent a x = None) ∧ hp_parent a b = Some y)›
  by (cases ‹(filter (λy. ∃ya. y = Some ya) (map (hp_parent a) xs))›)
   (fastforce simp: hp_parent_children_def filter_empty_conv filter_eq_Cons_iff map_eq_append_conv)+

lemma hp_parent_children_in_nodes:
  ‹hp_parent_children b xs ≠ None ⟹ node (the (hp_parent_children b xs)) ∈# ∑⇩# (mset_nodes `# mset xs)›
  by (metis hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_append(1)
    hp_node_children_append(2) hp_node_children_simps(3) hp_parent_children_Some_iff
    hp_parent_in_nodes option.collapse)

lemma hp_parent_hp_child:
  ‹distinct_mset ((mset_nodes (a::('a,nat)hp))) ⟹ hp_child n a ≠ None ⟹ map_option node (hp_parent (node (the (hp_child n a))) a) = Some n›
  apply (induction n a rule: hp_child.induct)
  subgoal for  n a sc x children
    apply (simp add: hp_parent_simps_if)
    apply auto
    subgoal for y
      apply (auto simp add: hp_parent_simps_if hp_parent_children_Some_iff 
        split: option.splits dest: distinct_mset_union)
      apply (metis (no_types, lifting) diff_single_trivial disjunct_not_in distinct_mem_diff_mset
        distinct_mset_add hp_parent_None_notin mset_cancel_union(2) mset_nodes_simps node_in_mset_nodes
        option_last_Nil option_last_Some_iff(2) sum_mset_sum_list)
      done
    subgoal for y
      using distinct_mset_union[of ‹mset_nodes x› ‹sum_list (map mset_nodes children)›]
        distinct_mset_union[of ‹sum_list (map mset_nodes children)› ‹mset_nodes x› ]
      apply (auto simp add: hp_parent_simps_if ac_simps hp_parent_children_cons
        split: option.splits dest: distinct_mset_union)
      apply (metis Groups.add_ac(2) add_mset_add_single disjunct_not_in distinct_mset_add hp_parent_None_notin member_add_mset mset_nodes_simps
        option_last_Nil option_last_Some_iff(2) sum_mset_sum_list)
      by (metis hp.sel(1) hp_parent.simps(2) hp_parent_simps_if option.sel option.simps(3) pairing_heap_assms.pass⇩2.cases)
    done
  subgoal by auto
  done


lemma hp_child_hp_parent:
  ‹distinct_mset ((mset_nodes (a::('a,nat)hp))) ⟹ hp_parent n a ≠ None ⟹ map_option node (hp_child (node (the (hp_parent n a))) a) = Some n›
  apply (induction n a rule: hp_parent.induct)
  subgoal for  n a sc x children
    apply (simp add: hp_parent_simps_if)
    apply auto
    subgoal for y
      using distinct_mset_union[of ‹mset_nodes x› ‹sum_list (map mset_nodes children)›]
        distinct_mset_union[of ‹sum_list (map mset_nodes children)› ‹mset_nodes x› ]
      apply (auto simp add: hp_parent_simps_if hp_parent_children_cons ac_simps
        split: option.splits)
      apply (smt (verit, del_insts) hp_parent_children_Some_iff hp_parent_in_nodes list.map(2) map_append option.sel option_last_Nil option_last_Some_iff(2) sum_list.append sum_list_simps(2) union_iff)
      by fastforce
    subgoal premises p for yy
      using p(2-) p(1)[of x]
      using distinct_mset_union[of ‹mset_nodes x› ‹sum_list (map mset_nodes children)›]
        distinct_mset_union[of ‹sum_list (map mset_nodes children)› ‹mset_nodes x› ]
      apply (auto simp add: hp_parent_simps_if hp_parent_children_cons ac_simps
        split: option.splits)
      apply (smt (verit, del_insts) disjunct_not_in distinct_mset_add hp_child_None_notin
        hp_parent_children_Some_iff hp_parent_in_nodes list.map(2) map_append option.sel
        option_last_Nil option_last_Some_iff(2) sum_list.Cons sum_list.append union_iff)

      using p(1)
      apply (auto simp: hp_parent_children_Some_iff)
      by (metis WB_List_More.distinct_mset_union2 distinct_mset_union hp_child_children_simps(3)
        hp_child_children_skip_first hp_child_hp_children_simps2 hp_parent_in_nodes list.map(2)
        option.sel option_last_Nil option_last_Some_iff(2) sum_list.Cons union_iff)
    done
  subgoal by auto
  done

lemma hp_parent_children_append_case:
  ‹hp_parent_children a (xs @ ys) = (case hp_parent_children a xs of None ⇒ hp_parent_children a ys | Some a ⇒ Some a)›
  by (auto simp: hp_parent_children_def comp_def option_hd_def)

lemma hp_parent_children_append_skip_first[simp]:
  ‹a ∉# ∑⇩# (mset_nodes `# mset xs) ⟹ hp_parent_children a (xs @ ys) = hp_parent_children a ys›
  by (auto simp: hp_parent_children_append_case split: option.splits)

lemma hp_parent_children_append_skip_second[simp]:
  ‹a ∉# ∑⇩# (mset_nodes `# mset ys) ⟹ hp_parent_children a (xs @ ys) = hp_parent_children a xs›
  by (auto simp: hp_parent_children_append_case split: option.splits)

lemma hp_parent_simps_single_if:
 ‹hp_parent n (Hp a sc (children)) =
  (if children = [] then None else if n = node (hd children) then Some (Hp a sc (children))
  else hp_parent_children n children)›
 by (cases children)
   (auto simp: hp_parent_simps)

lemma hp_parent_children_remove_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset xs)) ⟹ hp_parent_children a (remove_key_children a xs) = None›
  apply (induction a xs rule: remove_key_children.induct)
  subgoal by auto
  subgoal for k x n c xs
    apply (auto simp: hp_parent_simps_if hp_parent_children_cons
      split: option.split
      dest: WB_List_More.distinct_mset_union2)
    apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in
      distinct_mset_add hp.sel(1) hp_parent_simps_single_if list.map(2) list.sel(1) list.simps(3)
      node_hd_in_sum node_in_mset_nodes option_last_Nil option_last_Some_iff(2) sum_list_simps(2)) 
    apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in
      distinct_mset_add hp.sel(1) hp_parent_simps_single_if list.map(2) list.sel(1) list.simps(3)
      node_hd_in_sum node_in_mset_nodes option_last_Nil option_last_Some_iff(2) sum_list_simps(2))
   done
  done

lemma remove_key_children_notin_unchanged[simp]: ‹x ∉# sum_list (map mset_nodes c) ⟹ remove_key_children x c = c›
  by (induction x c rule: remove_key_children.induct)
     auto

lemma remove_key_notin_unchanged[simp]: ‹x ∉# mset_nodes c ⟹ remove_key x c = Some c›
  by (induction x c rule: remove_key.induct)
     auto

lemma remove_key_remove_all: ‹k ∉# ∑⇩# (mset_nodes `# mset (remove_key_children k c))›
  by (induction k c rule: remove_key_children.induct) auto

lemma hd_remove_key_node_same: ‹c ≠ [] ⟹ remove_key_children k c ≠ [] ⟹
  node (hd (remove_key_children k c)) = node (hd c) ⟷ node (hd c) ≠ k›
  using remove_key_remove_all[of k]
  apply (induction k c rule: remove_key_children.induct)
  apply (auto)[]
  by fastforce

lemma hd_remove_key_node_same': ‹c ≠ [] ⟹ remove_key_children k c ≠ [] ⟹
  node (hd c) = node (hd (remove_key_children k c)) ⟷ node (hd c) ≠ k›
  using hd_remove_key_node_same[of c k] by auto

lemma remove_key_children_node_hd[simp]: ‹c ≠ [] ⟹ remove_key_children (node (hd c)) c= remove_key_children (node (hd c)) (tl c)›
  by (cases c; cases ‹tl c›; cases ‹hd c›)
     (auto simp: )

lemma remove_key_children_alt_def:
  ‹remove_key_children k xs = map (λx. case x of Hp a b c ⇒ Hp a b (remove_key_children k c)) (filter (λn. node n ≠ k) xs)›
  by (induction k xs rule: remove_key_children.induct) auto

lemma not_orig_notin_remove_key: ‹b ∉# sum_list (map mset_nodes xs) ⟹
  b ∉# sum_list (map mset_nodes (remove_key_children a xs))›
  by (induction a xs rule: remove_key_children.induct) auto

lemma hp_parent_None_notin_same_hd[simp]: ‹b ∉# sum_list (map mset_nodes x3) ⟹ hp_parent b (Hp b x2 x3) = None›
  by (induction x3 rule: induct_list012)
   (auto simp: hp_parent_children_cons hp_parent.simps(1) filter_empty_conv split: if_splits)

(*does not hold for the children of a*)
lemma hp_parent_children_remove_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset xs)) ⟹ a ≠ b ⟹  hp_parent_children b (remove_key_children a xs) = hp_parent_children b xs›
  oops


lemma hp_parent_remove_key:
  ‹distinct_mset ((mset_nodes xs)) ⟹ a ≠ node xs ⟹ hp_parent a (the (remove_key a xs)) = None›
  apply (induction a xs rule: remove_key.induct)
  subgoal for a b sc children
    apply (cases ‹remove_key_children a children›)
    apply (auto simp: hp_parent_simps_if)
    apply (smt (verit, ccfv_threshold) remove_key_children.elims distinct_mset_add empty_iff
        hp.sel(1) inter_iff list.map(2) list.sel(1) list.simps(3) node_hd_in_sum node_in_mset_nodes set_mset_empty sum_list_simps(2))
    by (metis hp_parent_children_remove_key_children mset_map sum_mset_sum_list)
  done

lemma find_key_children_None_or_itself[simp]:
  ‹find_key_children a h ≠ None ⟹ node (the (find_key_children a h)) = a›
  by (induction a h rule: find_key_children.induct)
   (auto split: option.splits)

lemma find_key_None_or_itself[simp]:
  ‹find_key a h ≠ None ⟹ node (the (find_key a h)) = a›
  apply (induction a h rule: find_key.induct)
  apply auto
  using find_key_children_None_or_itself by fastforce

lemma find_key_children_notin[simp]:
  ‹a ∉#  ∑⇩# (mset_nodes `# mset xs) ⟹ find_key_children a xs = None›
  by (induction a xs rule: find_key_children.induct) auto


lemma find_key_notin[simp]:
  ‹a ∉# mset_nodes h ⟹ find_key a h = None›
  by (induction a h rule: find_key.induct) auto

lemma mset_nodes_find_key_children_subset:
  ‹find_key_children a h ≠ None ⟹ mset_nodes (the (find_key_children a h)) ⊆# ∑⇩# (mset_nodes `# mset h)›
  apply (induction a h rule: find_key_children.induct)
  apply (auto split: option.splits simp: ac_simps intro: mset_le_incr_right)
  apply (metis mset_le_incr_right union_commute union_mset_add_mset_right)+
  done

lemma hp_parent_None_iff_children_None:
  ‹hp_parent z (Hp x n c) = None ⟷ (c ≠ [] ⟶ z ≠ node (hd c)) ∧ hp_parent_children (z) c = None›
  by (cases c; cases ‹tl c›)
  (auto simp: hp_parent_children_cons hp_parent_simps_if hp_parent.simps(1) filter_empty_conv split: option.splits)


lemma mset_nodes_find_key_subset:
  ‹find_key a h ≠ None ⟹ mset_nodes (the (find_key a h)) ⊆# mset_nodes h›
  apply (induction a h rule: find_key.induct)
  apply (auto intro: mset_nodes_find_key_children_subset)
  by (metis mset_nodes_find_key_children_subset option.distinct(2) option.sel subset_mset_imp_subset_add_mset sum_image_mset_sum_map)

lemma find_key_none_iff[simp]:
  ‹find_key_children a h = None ⟷ a ∉# ∑⇩# (mset_nodes `# mset h)›
  by (induction a h rule: find_key_children.induct) auto

lemma find_key_noneD:
  ‹find_key_children a h = Some x ⟹  a ∈# ∑⇩# (mset_nodes `# mset h)›
  using find_key_none_iff by (metis option.simps(2))

lemma hp_parent_children_hd_None[simp]:
  ‹xs ≠ [] ⟹ distinct_mset (∑⇩# (mset_nodes `# mset xs)) ⟹ hp_parent_children (node (hd xs)) xs = None›
  by (cases xs; cases ‹hd xs›)
    (auto simp: hp_parent_children_def filter_empty_conv sum_list_map_remove1)

lemma hp_parent_hd_None[simp]:
  ‹x ∉# (∑⇩# (mset_nodes `# mset xs)) ⟹x ∉# sum_list (map mset_nodes c) ⟹ hp_parent_children x (Hp x n c # xs) = None›
  by (cases xs; cases ‹hd xs›; cases c)
    (auto simp: hp_parent_children_def filter_empty_conv sum_list_map_remove1 hp_parent.simps(1))

lemma hp_parent_none_children: ‹hp_parent_children z c = None ⟹
    hp_parent z (Hp x n c) = Some x2a ⟷ (c ≠ [] ∧ z = node (hd c) ∧ x2a = Hp x n c)›
  by (cases c)
   (auto simp:  filter_empty_conv sum_list_map_remove1 hp_parent_simps_if)

(* does not hold for Hp x _ (a # b # ...)  *)
lemma hp_parent_children_remove_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset xs)) ⟹ a ≠ b ⟹  hp_parent_children b (remove_key_children a xs) =
  (if find_key_children b xs ≠ None then None else hp_parent_children b xs)›
  oops

lemma in_the_default_empty_iff: ‹b ∈# the_default {#} M ⟷ M ≠ None ∧ b ∈# the M›
  by (cases M) auto

lemma remove_key_children_hd_tl: ‹distinct_mset (sum_list (map mset_nodes c)) ⟹ c ≠ [] ⟹ remove_key_children (node (hd c)) (tl c) = tl c›
  by (cases c) (auto simp add: disjunct_not_in distinct_mset_add)

lemma in_find_key_children_notin_remove_key:
  ‹find_key_children k c = Some x2 ⟹ distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹
      b ∈# mset_nodes x2 ⟹
      b ∉# ∑⇩#(mset_nodes `# mset (remove_key_children k c))›
  apply (induction k c rule: remove_key_children.induct)
  subgoal by auto
  subgoal for k x n c xs
    using find_key_children_None_or_itself[of b c] find_key_children_None_or_itself[of b xs]
    using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
      distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
     apply (auto dest: multi_member_split[of b] split: option.splits)
     apply (auto dest!: multi_member_split[of b])[]
     apply (metis mset_nodes_find_key_children_subset option.distinct(1) option.sel subset_mset.le_iff_add sum_image_mset_sum_map union_iff)
     apply (metis add_diff_cancel_right' distinct_mset_in_diff mset_nodes_find_key_children_subset option.distinct(1) option.sel subset_mset.le_iff_add
           sum_image_mset_sum_map)
     apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(2) option.sel sum_image_mset_sum_map)
     by (metis add_diff_cancel_right' distinct_mset_in_diff mset_nodes_find_key_children_subset not_orig_notin_remove_key option.distinct(1)
  option.sel subset_mset.le_iff_add sum_image_mset_sum_map)
   done

lemma hp_parent_children_None_hp_parent_iff: ‹hp_parent_children b list = None ⟹ hp_parent b (Hp x n list) = Some x2a ⟷ list ≠ [] ∧ node (hd list) = b ∧ x2a = Hp x n list›
  by (cases list; cases ‹tl list›) (auto simp: hp_parent_simps_if)

lemma hp_parent_children_not_hd_node:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹ node (hd c) = node x2a ⟹ c ≠ [] ⟹  remove_key_children (node x2a) c ≠ [] ⟹
    hp_parent_children (node (hd (remove_key_children (node x2a) c))) c = Some x2a ⟹ False›
  apply (cases c; cases ‹tl c›; cases ‹hd c›)
  apply (auto simp: hp_parent_children_cons
    split: option.splits)
  apply (simp add:  disjunct_not_in distinct_mset_add)
  apply (metis hp_parent_in_nodes option.distinct(1) option.sel)
  by (smt (verit, ccfv_threshold) WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp.sel(1) hp_parent_children_in_nodes hp_parent_simps_single_if list.sel(1) node_hd_in_sum node_in_mset_nodes option.sel option_last_Nil option_last_Some_iff(2) remove_key_children.elims sum_image_mset_sum_map)

lemma hp_parent_children_hd_tl_None[simp]: ‹distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹ c ≠ [] ⟹ a ∈ set (tl c)⟹  hp_parent_children (node a) c = None›
  apply (cases c)
    apply (auto simp: hp_parent_children_def filter_empty_conv dest!: split_list[of a])
    apply (metis add_diff_cancel_left' add_diff_cancel_right' distinct_mset_add distinct_mset_in_diff hp_parent_None_notin node_in_mset_nodes)
  apply (simp add: distinct_mset_add)
  apply (simp add: distinct_mset_add)
  apply (metis (no_types, opaque_lifting) disjunct_not_in hp_parent_None_notin mset_subset_eqD mset_subset_eq_add_right node_in_mset_nodes sum_list_map_remove1 union_commute)
  by (metis WB_List_More.distinct_mset_union2 add_diff_cancel_left' distinct_mem_diff_mset hp_parent_None_notin node_in_mset_nodes sum_list_map_remove1 union_iff)


lemma hp_parent_hp_parent_remove_key_not_None_same:
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset c))› and
    ‹x ∉# ∑⇩# (mset_nodes `# mset c)› and
    ‹hp_parent b (Hp x n c) = Some x2a› ‹b ∉# mset_nodes x2a›
    ‹hp_parent b (Hp x n (remove_key_children k c)) = Some x2b›
  shows ‹remove_key k x2a ≠ None ∧ (case remove_key k x2a of Some a ⇒ (x2b) = a | None ⇒ node x2a = k)›
proof -
  show ?thesis
    using assms
  proof (induction k c rule: remove_key_children.induct)
    case (1 k)
    then show ?case by (auto simp: hp_parent_children_cons split: if_splits)
  next
    case (2 k x n c xs)
    moreover have ‹c ≠ [] ⟹ xs ≠ [] ⟹ node (hd xs) ≠ node (hd c)›
      using 2(4) by  (cases c; cases ‹hd c›; cases xs; auto)
    moreover have ‹xs ≠ [] ⟹ hp_parent_children (node (hd xs)) c = None›
      by (metis (no_types, lifting) add_diff_cancel_left' calculation(4) distinct_mset_in_diff
        distinct_mset_union hp_parent_children_None_notin list.map(2) mset_nodes.simps
        node_hd_in_sum sum_image_mset_sum_map sum_list.Cons)
    moreover have ‹c ≠ [] ⟹ hp_parent_children (node (hd c)) xs = None›
      by (metis calculation(4) disjunct_not_in distinct_mset_add hp_parent_None_iff_children_None
        hp_parent_None_notin hp_parent_children_None_notin list.simps(9) sum_image_mset_sum_map
        sum_list.Cons)
    moreover have [simp]: ‹remove_key (node x2a) x2a = None›
      by (cases x2a) auto
    moreover have
      ‹hp_parent_children b xs ≠ None ⟹ hp_parent_children b c = None›
      ‹hp_parent_children b c ≠ None ⟹ hp_parent_children b xs = None›
      ‹node x2a ∈# sum_list (map mset_nodes c) ⟹ node x2a ∉# sum_list (map mset_nodes xs)›
      using hp_parent_children_in_nodes[of b xs] hp_parent_children_in_nodes[of b c] 2(4)
      apply auto
      apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin option.distinct(1))
      apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin option.distinct(1))
      apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin option.distinct(1))
      done
    ultimately show ?case
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
        hp_parent_children_in_nodes[of b c]  hp_parent_children_in_nodes[of b xs]
      apply (auto simp: hp_parent_children_cons remove_key_None_iff split: if_splits option.splits)
      apply (auto simp: hp_parent_simps_single_if hp_parent_children_cons split: option.splits if_splits)[]
      apply (auto simp: hp_parent_simps_single_if hp_parent_children_cons split: option.splits if_splits)[]
      apply (auto simp: hp_parent_children_cons hp_parent_simps_single_if  handy_if_lemma split: if_splits option.splits )[]
      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma split: if_splits option.splits )
      apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in distinct_mset_add hp.sel(1) hp_parent_children_hd_None list.sel(1)
        list.simps(9) node_in_mset_nodes option_last_Nil option_last_Some_iff(2) remove_key_children_notin_unchanged sum_image_mset_sum_map sum_list.Cons)
      apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in distinct_mset_add hp.sel(1) hp_parent_children_hd_None list.sel(1)
        list.simps(9) node_in_mset_nodes option_last_Nil option_last_Some_iff(2) remove_key_children_notin_unchanged sum_image_mset_sum_map sum_list.Cons)
      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma split: if_splits option.splits )
      apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in distinct_mset_add hp.sel(1) hp_parent_children_hd_None list.sel(1)
        list.simps(9) node_in_mset_nodes option_last_Nil option_last_Some_iff(2) remove_key_children_notin_unchanged sum_image_mset_sum_map sum_list.Cons)
      apply (smt (verit, ccfv_threshold) remove_key_children.elims disjunct_not_in distinct_mset_add hp.sel(1) hp_parent_children_hd_None list.sel(1)
        list.simps(9) node_in_mset_nodes option_last_Nil option_last_Some_iff(2) remove_key_children_notin_unchanged sum_image_mset_sum_map sum_list.Cons)
      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        cases ‹node x2a ∈# sum_list (map mset_nodes c)›; auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma split: if_splits option.splits)

      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma hd_remove_key_node_same[of c ‹node x2a›]
        intro: hp_parent_children_not_hd_node
        split: if_splits option.splits)

      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma hd_remove_key_node_same
        dest: hp_parent_children_not_hd_node split: if_splits option.splits
        intro: hp_parent_children_not_hd_node)

      apply (cases ‹xs = []›; cases ‹b = node (hd xs)›; cases ‹remove_key_children (node x2a) xs = []›;
        cases ‹b = node (hd (remove_key_children (node x2a) xs))›; cases ‹Hp x n (remove_key_children (node x2a) xs) = x2b›;
        cases ‹node x2a ∈# sum_list (map mset_nodes c)›;
        auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma split: if_splits option.splits)

      apply (cases ‹xs = []›)
      apply (auto simp: hp_parent_children_cons hp_parent_simps_single_if handy_if_lemma hd_remove_key_node_same remove_key_children_hd_tl
        dest: hp_parent_children_not_hd_node split: if_splits option.splits)[2]
      apply (smt (verit, best) hd_remove_key_node_same' hp_parent_None_iff_children_None hp_parent_children_hd_None hp_parent_children_hd_tl_None hp_parent_simps_single_if in_hd_or_tl_conv mset_map option_hd_Nil option_hd_Some_iff(1) remove_key_children_hd_tl remove_key_children_node_hd sum_mset_sum_list)
      apply (smt (verit, best) hd_remove_key_node_same' hp_parent_None_iff_children_None hp_parent_children_hd_None hp_parent_children_hd_tl_None hp_parent_simps_single_if in_hd_or_tl_conv mset_map option_hd_Nil option_hd_Some_iff(1) remove_key_children_hd_tl remove_key_children_node_hd sum_mset_sum_list)
      apply (metis add_diff_cancel_right' distinct_mset_in_diff hp_parent_children_None_notin not_orig_notin_remove_key option_hd_Nil option_hd_Some_iff(2))
      apply (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin node_hd_in_sum not_orig_notin_remove_key option_last_Nil option_last_Some_iff(1) remove_key_children_hd_tl remove_key_children_node_hd)
      apply (smt (verit, del_insts) remove_key_children.simps(1) hd_remove_key_node_same' hp_parent_children_None_notin hp_parent_children_hd_None hp_parent_children_hd_tl_None in_hd_or_tl_conv option.distinct(1) remove_key_children_hd_tl remove_key_children_node_hd remove_key_remove_all sum_image_mset_sum_map)
      apply (metis add_diff_cancel_right' distinct_mset_in_diff hp_parent_children_None_notin not_orig_notin_remove_key option_hd_Nil option_hd_Some_iff(2))
      by (metis disjunct_not_in distinct_mset_add hp_parent_children_None_notin not_orig_notin_remove_key option_hd_Nil option_hd_Some_iff(2))
  qed
qed

lemma in_remove_key_children_changed: ‹k ∈# sum_list (map mset_nodes c) ⟹ remove_key_children k c ≠ c›
  apply (induction k c rule: remove_key_children.induct)
  apply auto
  apply (metis hp.sel(1) list.sel(1) mset_map neq_Nil_conv node_hd_in_sum remove_key_remove_all sum_mset_sum_list)+
  done

lemma hp_parent_in_nodes2: ‹hp_parent (z) xs = Some a ⟹ node a ∈# mset_nodes xs›
  apply (induction z xs rule: hp_parent.induct)
  apply (auto simp: hp_parent_children_def filter_empty_conv)
  by (metis empty_iff hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps(2) hp_parent_in_nodes
    member_add_mset mset_nodes_simps option.discI option.sel set_mset_empty sum_image_mset_sum_map sum_mset_sum_list union_iff)

lemma hp_parent_children_in_nodes2: ‹hp_parent_children z xs = Some a ⟹ node a ∈# ∑⇩# (mset_nodes `# mset xs)›
    apply (induction xs)
    apply (auto simp: hp_parent_children_cons filter_empty_conv split: option.splits)
    using hp_parent_in_nodes by fastforce

lemma hp_next_in_nodes2: ‹hp_next (z) xs = Some a ⟹ node a ∈# mset_nodes xs›
  apply (induction z xs rule: hp_next.induct)
  apply (auto simp: )
  by (metis hp_next_children.simps(1) hp_next_children_simps(2) hp_next_children_simps(3) node_in_mset_nodes option.sel)

lemma hp_next_children_in_nodes2: ‹hp_next_children (z) xs = Some a ⟹ node a ∈# ∑⇩# (mset_nodes `# mset xs)›
  apply (induction z xs rule: hp_next_children.induct)
  apply (auto simp:  hp_next_in_nodes2 split: option.splits)
  by (metis hp_next_children_simps(1) hp_next_children_simps(2) hp_next_children_simps(3) hp_next_in_nodes2 node_in_mset_nodes option.inject)

lemma in_remove_key_changed: ‹remove_key k a ≠ None ⟹ a = the (remove_key k a) ⟷ k ∉# mset_nodes a›
  apply (induction k a rule: remove_key.induct)
  apply (auto simp: in_remove_key_children_changed)
  by (metis in_remove_key_children_changed)

lemma node_remove_key_children_in_mset_nodes: ‹∑⇩# (mset_nodes `# mset (remove_key_children k c)) ⊆# (∑⇩# (mset_nodes `# mset c))›
  apply (induction k c rule: remove_key_children.induct)
  apply auto
  apply (metis mset_le_incr_right(2) union_commute union_mset_add_mset_right)
  using subset_mset.add_mono by blast

lemma remove_key_children_hp_parent_children_hd_None: ‹remove_key_children k c = a # list ⟹
  distinct_mset (sum_list (map mset_nodes c)) ⟹
  hp_parent_children (node a) (a # list) = None›
  using node_remove_key_children_in_mset_nodes[of k c]
  apply (auto simp: hp_parent_children_def filter_empty_conv)
  apply (meson WB_List_More.distinct_mset_mono distinct_mset_union hp_parent_itself)
  by (metis WB_List_More.distinct_mset_mono add_diff_cancel_left' distinct_mem_diff_mset hp_parent_None_notin node_in_mset_nodes sum_list_map_remove1 union_iff)


lemma hp_next_not_same_node: ‹distinct_mset (mset_nodes b) ⟹ hp_next x b = Some y ⟹ x ≠ node y›
  apply (induction x b rule: hp_next.induct)
  apply auto
    by (metis disjunct_not_in distinct_mset_add hp_next_children_simps(1) hp_next_children_simps(2) hp_next_children_simps(3) inter_mset_empty_distrib_right node_in_mset_nodes option.sel)

lemma hp_next_children_not_same_node: ‹distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹ hp_next_children x c = Some y ⟹ x ≠ node y›
  apply (induction x c rule: hp_next_children.induct)
  subgoal
    apply (auto simp: hp_next_children.simps(1) split: if_splits option.splits dest: hp_next_not_same_node)
    apply (metis (no_types, opaque_lifting) distinct_mset_iff hp.exhaust_sel mset_nodes_simps union_mset_add_mset_left union_mset_add_mset_right)
    apply (metis Duplicate_Free_Multiset.distinct_mset_mono mset_subset_eq_add_left union_commute)
      by (meson distinct_mset_union hp_next_not_same_node)
  subgoal apply auto
    by (meson hp_next_not_same_node)
  subgoal by auto
  done

lemma hp_next_children_hd_is_hd_tl: ‹c ≠ [] ⟹ distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹ hp_next_children (node (hd c)) c = option_hd (tl c)›
  by (cases c; cases ‹tl c›) auto

lemma hp_parent_children_remove_key_children_other:
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset xs))›
  shows ‹hp_parent_children b (remove_key_children a xs) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key_children a xs))) then None
    else if map_option node (hp_next_children a xs) = Some b then map_option (the o remove_key a) (hp_parent_children a xs)
    else map_option (the o remove_key a) (hp_parent_children b xs))›
  using assms
proof (induction a xs rule: remove_key_children.induct)
  case (1 k)
  then show ?case by auto
next
  case (2 k x n c xs)
  have [intro]: ‹b ∈# sum_list (map mset_nodes c) ⟹ hp_parent_children b xs = None›
    using 2(4) by (auto simp: in_the_default_empty_iff dest!: multi_member_split split: if_splits)
  consider
    (kx) ‹k=x› |
    (inc) ‹k ≠ x› ‹find_key_children k c ≠ None› |
    (inxs) ‹k ≠ x› ‹find_key_children k c = None›
    by blast
  then show ?case
  proof (cases)
    case kx
    then show ?thesis 
      apply (auto simp: in_the_default_empty_iff)
      using find_key_children_None_or_itself[of b c] find_key_children_None_or_itself[of b xs] 2
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
      by (auto simp: not_orig_notin_remove_key in_the_default_empty_iff hp_parent_children_cons
        split: option.split if_splits)
  next
    case inc
    moreover have ‹b ∈# mset_nodes (the (find_key_children k c)) ⟹ b ∈# ∑⇩# (mset_nodes `# mset c)›
      using inc by (meson mset_nodes_find_key_children_subset mset_subset_eqD)
    moreover have c: ‹c ≠ []›
      using inc by auto
    moreover have [simp]: ‹remove_key_children (node (hd c)) (tl c) = tl c›
      using c 2(4) by (cases c; cases ‹hd c›) auto
    moreover have [simp]: ‹find_key_children (node (hd c)) c = Some (hd c)›
      using c 2(4) by (cases c; cases ‹hd c›) auto
    moreover have [simp]: ‹k ∈# sum_list (map mset_nodes c) ⟹ k ∉# sum_list (map mset_nodes xs)› for k
      using 2(4) by (auto dest!: multi_member_split)
    moreover have KK[iff]: ‹remove_key_children k c = [] ⟷ c = [] ∨ (c ≠ [] ∧  tl c = [] ∧ node (hd c) = k)›
      using 2(4)
      by (induction k c rule: remove_key_children.induct) (auto simp: dest: multi_member_split)
    ultimately show ?thesis
      using find_key_children_None_or_itself[of b c] find_key_children_None_or_itself[of b xs] 2
        find_key_children_None_or_itself[of k c] find_key_children_None_or_itself[of k xs]
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
      apply (auto simp: not_orig_notin_remove_key in_the_default_empty_iff split: option.split if_splits)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      apply (metis hp_parent_None_iff_children_None in_find_key_children_notin_remove_key mset_map node_hd_in_sum sum_mset_sum_list)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      apply (metis hp_parent_None_iff_children_None in_find_key_children_notin_remove_key mset_map node_hd_in_sum sum_mset_sum_list)
        defer

      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff hp_parent_None_iff_children_None
        hp_parent_children_None_hp_parent_iff split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      apply (metis KK ‹remove_key_children (node (hd c)) (tl c) = tl c›
        hd_remove_key_node_same' hp_next_children_hd_simps list.exhaust_sel option_hd_def remove_key_children_node_hd)
      apply (metis KK hd_remove_key_node_same')
      apply (metis KK find_key_children_None_or_itself hd_remove_key_node_same inc(2) node_in_mset_nodes option.sel)
      apply (smt (verit) remove_key.simps ‹remove_key_children (node (hd c)) (tl c) = tl c› ‹b ∈# sum_list (map mset_nodes c) ⟹ hp_parent_children b xs = None›
        hd_remove_key_node_same hp_next_children.elims hp_parent_None_iff_children_None hp_parent_children_hd_None hp_parent_none_children
        hp_parent_simps_single_if list.sel(1) list.sel(3) o_apply option.map_sel option.sel remove_key_children_node_hd sum_image_mset_sum_map)


      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff hp_parent_None_iff_children_None
        hp_parent_children_None_hp_parent_iff in_remove_key_changed split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      apply (metis ‹b ∈# sum_list (map mset_nodes c) ⟹ hp_parent_children b xs = None› hp_next_children_in_nodes2 sum_image_mset_sum_map)

      apply (smt (verit, ccfv_threshold) remove_key_children.elims WB_List_More.distinct_mset_mono ‹find_key_children (node (hd c)) c = Some (hd c)› ‹remove_key_children (node (hd c)) (tl c) = tl c› add_diff_cancel_left' distinct_mset_in_diff hp.exhaust_sel hp.inject hp_next_children_in_nodes2
        hp_next_children_simps(2) hp_next_children_simps(3) hp_next_simps in_remove_key_children_changed list.exhaust_sel list.sel(1) mset_nodes_simps
        mset_nodes_find_key_children_subset option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map sum_mset_sum_list union_single_eq_member)
      apply (smt (verit, ccfv_threshold) remove_key_children.elims WB_List_More.distinct_mset_mono ‹find_key_children (node (hd c)) c = Some (hd c)›
        ‹remove_key_children (node (hd c)) (tl c) = tl c› add_diff_cancel_left' distinct_mset_in_diff hp.exhaust_sel hp.inject hp_next_children_in_nodes2
        hp_next_children_simps(2) hp_next_children_simps(3) hp_next_simps in_remove_key_children_changed list.exhaust_sel list.sel(1) mset_nodes_simps
        mset_nodes_find_key_children_subset option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map sum_mset_sum_list union_single_eq_member)
      apply (metis handy_if_lemma hp_next_children_hd_simps list.exhaust_sel option_hd_def)
      apply (metis hp_next_children_hd_is_hd_tl mset_map option_hd_Some_iff(1) sum_mset_sum_list)
      by (smt (verit, best) None_eq_map_option_iff remove_key.simps hp_parent_None_iff_children_None hp_parent_children_hd_None hp_parent_none_children hp_parent_simps_single_if list.exhaust_sel o_apply option.map_sel option.sel remove_key_children_hp_parent_children_hd_None sum_image_mset_sum_map)
  next
    case inxs
    moreover have True
      by auto
    ultimately show ?thesis
      using find_key_children_None_or_itself[of b c] find_key_children_None_or_itself[of b xs] 2
        find_key_children_None_or_itself[of k c] find_key_children_None_or_itself[of k xs]
        hp_next_children_in_nodes2[of k xs]
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
      apply (auto simp: not_orig_notin_remove_key in_the_default_empty_iff split: option.split if_splits)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff ex_hp_node_children_Some_in_mset_nodes
        split: option.split intro!: hp_parent_None_notin
        dest: in_find_key_children_notin_remove_key multi_member_split
        mset_nodes_find_key_children_subset)[2]
      apply (cases ‹hp_next_children k xs›)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff ex_hp_node_children_Some_in_mset_nodes
        split: option.split intro!: hp_parent_None_notin
        dest: in_find_key_children_notin_remove_key multi_member_split
        mset_nodes_find_key_children_subset)[2]
      apply (metis (no_types, lifting)  find_key_none_iff mset_map
        mset_nodes_find_key_children_subset mset_subset_eqD  option.map_sel sum_mset_sum_list)
      apply (metis (no_types, lifting)  find_key_none_iff mset_map
        mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel sum_mset_sum_list)
      apply (metis (no_types, lifting) distinct_mset_add find_key_none_iff in_the_default_empty_iff inter_iff mset_map
        mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel sum_mset_sum_list the_default.simps(2))
      apply (smt (verit) add_diff_cancel_left' distinct_mem_diff_mset hp_next_children_in_nodes2 hp_parent_None_iff_children_None hp_parent_children_None_notin hp_parent_children_append_case hp_parent_children_append_skip_first hp_parent_children_cons mset_map node_hd_in_sum sum_mset_sum_list)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      apply (metis (mono_tags, opaque_lifting) remove_key.simps comp_def hp_parent_None_iff_children_None hp_parent_children_None_hp_parent_iff hp_parent_simps_single_if option.map_sel option.sel remove_key_children_notin_unchanged)
      apply (auto simp: hp_parent_children_cons in_the_default_empty_iff split: option.split
        dest: in_find_key_children_notin_remove_key)[]
      by (metis (no_types, opaque_lifting) remove_key.simps hp_parent_simps_single_if option.distinct(1) option.map(2) option.map_comp option.sel remove_key_children_notin_unchanged)
  qed
qed


lemma hp_parent_remove_key_other:
  assumes ‹distinct_mset ((mset_nodes  xs))› ‹(remove_key a xs) ≠ None›
  shows ‹hp_parent b (the (remove_key a xs)) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key a xs))) then None
    else if map_option node (hp_next a xs) = Some b then map_option (the o remove_key a) (hp_parent a xs)
    else map_option (the o remove_key a) (hp_parent b xs))›
  using assms hp_parent_children_remove_key_children_other[of ‹hps xs› b a]
  apply (cases xs)
  apply (auto simp: in_the_default_empty_iff hp_parent_None_iff_children_None
    dest: in_find_key_children_notin_remove_key split: if_splits)
  apply (metis (no_types, lifting) in_find_key_children_notin_remove_key  node_hd_in_sum sum_image_mset_sum_map)
  apply (metis hp_parent_None_notin_same_hd hp_parent_simps_single_if in_find_key_children_notin_remove_key option.simps(2) sum_image_mset_sum_map)
  apply (smt (verit, ccfv_threshold) None_eq_map_option_iff remove_key.simps remove_key_children.elims distinct_mset_add distinct_mset_add_mset
    hd_remove_key_node_same hp.sel(1) hp_child.simps(1) hp_child_hd hp_next_children_hd_is_hd_tl hp_next_children_in_nodes2 hp_next_children_simps(2)
    hp_next_children_simps(3) hp_next_simps hp_parent_None_iff_children_None hp_parent_simps_single_if inter_iff list.simps(9) mset_nodes_simps
    node_in_mset_nodes o_apply option.collapse option.map_sel option.sel option_hd_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd
    sum_image_mset_sum_map sum_list_simps(2) sum_mset_sum_list union_single_eq_member)
  apply (simp add: hp_parent_simps_single_if; fail)
  apply (simp add: hp_parent_simps_single_if; fail)
  apply (smt (verit) find_key_children.elims remove_key.simps remove_key_children.elims find_key_none_iff hp.sel(1) hp_next_children_hd_is_hd_tl
    hp_parent_children_None_notin hp_parent_simps_single_if list.sel(1) list.sel(3) list.simps(3) map_option_eq_Some node_in_mset_nodes o_apply option.map_sel
    option.sel option_hd_def remove_key_children_hd_tl sum_image_mset_sum_map)
  apply (simp add: hp_parent_simps_single_if)
  apply (simp add: hp_parent_simps_single_if)
  done

lemma hp_prev_in_nodes: ‹hp_prev k c≠ None ⟹ node (the (hp_prev k c)) ∈# ((mset_nodes c))›
  by (induction k c rule: hp_prev.induct) (auto simp: hp_prev_children.simps(1) split: option.splits)

lemma hp_prev_children_in_nodes: ‹hp_prev_children k c≠ None ⟹ node (the (hp_prev_children k c)) ∈# (∑⇩# (mset_nodes `# mset c))›
  apply (induction k c rule: hp_prev_children.induct)
  subgoal for a x y children
    using hp_prev_in_nodes[of a x]
    by (auto simp: hp_prev_children.simps(1) split: option.splits)
  subgoal for a x
    using hp_prev_in_nodes[of a x]
    by (auto simp: hp_prev_children.simps(1) split: option.splits)
  subgoal by auto
  done

lemma hp_next_children_notin_end:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset (x#xs))) ⟹ hp_next_children a xs = None ⟹ hp_next_children a (x # xs) = (if a = node x then option_hd xs else hp_next a x)›
  by (cases xs)
   (auto simp: hp_next_children.simps(1) split: option.splits)

lemma hp_next_children_remove_key_children_other:
  fixes xs :: "('b, 'a) hp list"
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset xs))›
  shows ‹hp_next_children b (remove_key_children a xs) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key_children a xs))) then None
    else if map_option node (hp_prev_children a xs) = Some b then (hp_next_children a xs)
    else map_option (the o remove_key a) (hp_next_children b xs))›
  using assms
proof (induction a xs rule: remove_key_children.induct)
    case (1 k)
    then show ?case by auto
  next
    case (2 k x n c xs)
    have dist_c_rem_y_xs: ‹distinct_mset
     (sum_list (map mset_nodes c) +
          sum_list (map mset_nodes (remove_key_children y xs)))› for y
      by (smt (verit, del_insts) "2"(4) distinct_mset_add inter_mset_empty_distrib_right mset.simps(2)
        mset_nodes.simps node_remove_key_children_in_mset_nodes subset_mset.add_diff_inverse
        sum_image_mset_sum_map sum_mset.insert union_ac(2))
    have ‹distinct_mset
      (sum_list (map mset_nodes c) + sum_list (map mset_nodes (remove_key_children k xs)))›
      ‹x ∉# sum_list (map mset_nodes (remove_key_children k xs))›
      using 2(4) apply auto
      apply (metis distinct_mset_mono' mset_map mset_subset_eq_mono_add_left_cancel node_remove_key_children_in_mset_nodes sum_mset_sum_list)
      by (simp add: not_orig_notin_remove_key)
    moreover have ‹distinct_mset (sum_list
      (map mset_nodes (Hp x n (remove_key_children k c) # remove_key_children k xs)))›
      using 2(4) apply (auto simp: not_orig_notin_remove_key)
      by (metis calculation(1) distinct_mset_mono' mset_map node_remove_key_children_in_mset_nodes subset_mset.add_right_mono sum_mset_sum_list)
    moreover have ‹hp_prev_children k xs ≠ None ⟹ remove_key_children k xs ≠ []›
      using 2(4) by (cases xs; cases ‹hd xs›; cases ‹tl xs›) (auto)
    moreover have ‹x = node z ⟹ hp_prev_children k (Hp (node z) n c # xs) = Some z ⟷
      z = Hp x n c ∧ xs ≠ [] ∧ k = node (hd (xs))› for z
      using 2(4) hp_prev_children_in_nodes[of _ c] apply -
      apply (cases ‹xs›; cases z; cases ‹hd xs›)
      using hp_prev_children_in_nodes[of _ c] apply fastforce
      apply (auto simp:  )
      apply (metis "2"(4) hp.inject hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(1) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps list.distinct(1) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl remove_key_remove_all sum_image_mset_sum_map)
      apply (metis "2"(4) hp.inject hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(1) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps in_remove_key_children_changed list.distinct(2) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl sum_image_mset_sum_map)
      by (metis "2"(4) hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps in_remove_key_children_changed list.distinct(2) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl sum_image_mset_sum_map)
    moreover have ‹xs ≠ [] ⟹ find_key_children (node (hd xs)) xs = Some (hd xs)›
      by (metis find_key_children.simps(2) hp.exhaust_sel list.exhaust_sel)
    moreover have ‹find_key_children k c = Some y ⟹
      option_hd (remove_key_children k xs) =
      map_option (λa. the (remove_key k a)) (option_hd xs)› for y
      using 2(4) by (cases xs; cases ‹hd xs›) auto
    moreover have ‹find_key_children k c = Some x2 ⟹ k ∉# ∑⇩# (mset_nodes `# mset xs)› for x2
      by (metis (no_types, lifting) "2"(4) Un_iff add_diff_cancel_left' distinct_mset_in_diff
        find_key_noneD list.simps(9) mset_nodes.simps set_mset_union sum_image_mset_sum_map sum_list_simps(2))
    moreover have ‹k ∉# sum_list (map mset_nodes xs) ⟹ k ≠ x ⟹
      ∀za. hp_prev_children k (Hp x n c # xs) = Some za ⟶ node za ≠ node z ⟹
      hp_prev_children k c = Some z ⟹ hp_next_children (node z) (Hp x n (remove_key_children k c) # xs) =
      map_option (λa. the (remove_key k a)) (hp_next_children (node z) (Hp x n c # xs))› for z
      by (metis hp_prev_children_None_notin hp_prev_children_first_child option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map)
    moreover have ‹find_key_children k c = Some x2 ⟹
      b ∈# mset_nodes x2 ⟹
      b∉# ∑⇩# (mset_nodes `# mset (Hp x n (remove_key_children k c) # xs))› for x2
      by (smt (verit, ccfv_threshold) "2"(4) add_diff_cancel_right' distinct_mset_add distinct_mset_in_diff
        find_key_noneD find_key_none_iff in_find_key_children_notin_remove_key mset.simps(2)
        mset_left_cancel_union mset_nodes.simps mset_nodes_find_key_children_subset mset_subset_eqD
        mset_subset_eq_add_right option.sel sum_mset.insert)
    moreover have ‹ find_key_children k c = Some x2 ⟹ k ≠ x ⟹ k ∈# sum_list (map mset_nodes c)› for x2
      by (metis find_key_none_iff option.distinct(1) sum_image_mset_sum_map)
    moreover have [simp]: ‹z ∈# sum_list (map mset_nodes c) ⟹ hp_next_children (z) xs = None› for z
      using "2.prems" distinct_mset_in_diff by fastforce
    moreover have ‹∀z. hp_prev_children k (Hp x n c # xs) = Some z ⟶ node z ≠ x ⟹
      xs = [] ∨ (xs ≠ [] ∧ node (hd xs) ≠ k)›
      by (smt (verit, ccfv_SIG) remove_key.simps remove_key_children.elims hp.sel(1)
        hp_prev_children_simps(1) list.sel(1) list.simps(3) option.map(1) option.map(2) option.sel
        option_hd_Nil option_hd_Some_hd)
    moreover have ‹xs ≠ [] ⟹ node (hd xs) ≠ k ⟹ remove_key_children k xs ≠ []› and
      [simp]: ‹xs ≠ [] ⟹ node (hd xs) ≠ k ⟹ hd (remove_key_children k xs) = the (remove_key k (hd xs))›
      ‹xs ≠ [] ⟹ node (hd xs) ≠ k ⟹ k ∉# sum_list (map mset_nodes c) ⟹ hp_prev_children k (Hp x n c # xs) = Some z ⟷ hp_prev_children k (xs) =Some z›
      ‹k ∉# sum_list (map mset_nodes xs) ⟹ xs ≠ [] ⟹ the (remove_key k (hd xs)) = hd xs›
      for z
      by (cases xs; cases ‹hd xs›; auto; fail)+
    moreover have‹mset_nodes y ⊆# sum_list (map mset_nodes xs)⟹
      distinct_mset (sum_list (map mset_nodes c) + sum_list (map mset_nodes xs)) ⟹ b ∈# mset_nodes y ⟹
      b ∉# (sum_list (map mset_nodes c))› for y :: "('b, 'a) hp"
      by (metis (no_types, lifting) add_diff_cancel_right' distinct_mset_in_diff mset_subset_eqD)
    moreover have ‹hp_prev_children k xs = Some z ⟹ hp_next_children (node z) c = None› for z
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
      by (metis "2.prems" disjunct_not_in dist_c_rem_y_xs distinct_mset_add hp_next_children_None_notin
        hp_prev_children_in_nodes list.sel(3) list.simps(3) option.sel option.simps(2) remove_key_children_hd_tl sum_image_mset_sum_map)
    ultimately show ?case
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›] 2
        find_key_children_None_or_itself[of k c] find_key_children_None_or_itself[of k xs] hp_prev_children_in_nodes[of b c]
        hp_prev_children_in_nodes[of k c] mset_nodes_find_key_children_subset[of k xs]
      supply [simp del] = find_key_children_None_or_itself
      apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl comp_def
        in_the_default_empty_iff)
      apply (simp add: disjunct_not_in distinct_mset_add)
      apply (auto simp: hp_next_children_simps_if remove_key_children_hd_tl
        dist_c_rem_y_xs hp_next_children_notin_end
        hp_next_children_hd_is_hd_tl
        split: option.splits)
      by (metis (no_types, lifting) "2.prems" remove_key_children.simps(1)
        hp_prev_children_None_notin hp_prev_children_skip_Cons hp_prev_in_nodes hp_prev_skip_hd_children
        list.exhaust_sel mset.simps(2) node_in_mset_nodes option.map_sel option.sel option_last_Nil
        option_last_Some_iff(2) remove_key_children_hd_tl remove_key_remove_all sum_image_mset_sum_map sum_mset.insert union_commute)
qed

lemma hp_next_remove_key_other:
  assumes ‹distinct_mset (mset_nodes xs)› ‹remove_key a xs ≠ None›
  shows ‹hp_next b (the (remove_key a xs)) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key a xs))) then None
    else if map_option node (hp_prev a xs) = Some b then (hp_next a xs)
    else map_option (the o remove_key a) (hp_next b xs))›
  using hp_next_children_remove_key_children_other[of ‹hps xs› b a] assms
  by (cases xs) (auto)


lemma hp_prev_children_cons_if:
  ‹hp_prev_children b (a # xs) = (if map_option node (option_hd xs) = Some b then Some a
    else (case hp_prev_children b (hps a) of None ⇒ hp_prev_children b xs | Some a ⇒ Some a))›
  apply (cases xs)
  apply (auto split: option.splits simp: hp_prev_children.simps(1))
  apply (metis hp.collapse hp_prev_simps)
  apply (metis hp.exhaust_sel hp_prev_simps)
  apply (metis hp.exhaust_sel hp_prev_simps option.simps(2))
  apply (metis hp.exhaust_sel hp_prev_simps option.simps(2))
  by (metis hp.exhaust_sel hp_prev_simps the_default.simps(1))


lemma hp_prev_children_remove_key_children_other:
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset xs))›
  shows ‹hp_prev_children b (remove_key_children a xs) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key_children a xs))) then None
    else if map_option node (hp_next_children a xs) = Some b then (hp_prev_children a xs)
    else map_option (the o remove_key a) (hp_prev_children b xs))›
  using assms
proof (induction a xs rule: remove_key_children.induct)
    case (1 k)
    then show ?case by auto
  next
    case (2 k x n c xs)
    have find_None_not_other: ‹find_key_children k c ≠ None ⟹ find_key_children k xs = None›
       ‹find_key_children k xs ≠ None ⟹ find_key_children k c = None›
      using "2"(4) distinct_mset_in_diff apply fastforce
      using "2"(4) distinct_mset_in_diff by fastforce

    have [simp]: ‹remove_key_children k xs ≠ [] ⟹ xs ≠ []›
      by auto

    have [simp]: ‹hp_prev_children (node (hd xs)) xs = None›
      using 2(4)
      by (cases xs; cases "hd xs"; cases "tl xs")
        auto
    have remove_key_children_empty_iff: ‹(remove_key_children k xs = []) = (∀x. x ∈ set xs ⟶ node x = k)›
      by (auto simp: remove_key_children_alt_def filter_empty_conv)
    have [simp]: ‹find_key_children k c = Some x2 ⟹ remove_key_children k xs = xs› for x2
      by (metis ‹find_key_children k c ≠ None ⟹ find_key_children k xs = None› find_key_none_iff option.distinct(1) remove_key_children_notin_unchanged sum_image_mset_sum_map)

    have dist: ‹distinct_mset
      (sum_list (map mset_nodes c) + sum_list (map mset_nodes (remove_key_children k xs)))›
      ‹x ∉# sum_list (map mset_nodes (remove_key_children k xs))›
      using 2(4) apply auto
      apply (metis distinct_mset_mono' mset_map mset_subset_eq_mono_add_left_cancel node_remove_key_children_in_mset_nodes sum_mset_sum_list)
      by (simp add: not_orig_notin_remove_key)
    moreover have ‹distinct_mset
    (sum_list
      (map mset_nodes (Hp x n (remove_key_children k c) # remove_key_children k xs)))›
      ‹distinct_mset (sum_list (map mset_nodes (remove_key_children k xs)))›
      using 2(4) apply (auto simp: not_orig_notin_remove_key)
      apply (metis dist(1) distinct_mset_mono' mset_map node_remove_key_children_in_mset_nodes subset_mset.add_right_mono sum_mset_sum_list)
      using WB_List_More.distinct_mset_union2 calculation by blast
    moreover have ‹hp_next_children k xs ≠ None ⟹ remove_key_children k xs ≠ []›
      using 2(4) by (cases xs; cases ‹hd xs›; cases ‹tl xs›) (auto)
    moreover have ‹xs ≠ [] ⟹ find_key_children (node (hd xs)) xs = Some (hd xs)›
      by (metis find_key_children.simps(2) hp.exhaust_sel list.exhaust_sel)
    moreover have [simp]: ‹distinct_mset (∑⇩# (mset_nodes `# mset a)) ⟹ hp_prev_children (node (hd a)) a = None› for a
      by (cases ‹(node (hd a), a)› rule: hp_prev_children.cases; cases ‹hd a›)
       (auto simp: hp_prev_children.simps(1) split: option.splits)
    moreover have
      ‹remove_key_children k xs ≠ [] ⟹ hp_prev_children (node (hd (remove_key_children k xs))) (remove_key_children k c) = None›
      ‹xs ≠ [] ⟹ hp_prev_children (node (hd xs)) (remove_key_children k c) = None›
      apply (metis dist(1) disjunct_not_in distinct_mset_add hp_prev_children_None_notin node_hd_in_sum not_orig_notin_remove_key sum_image_mset_sum_map)
      by (smt (verit, ccfv_threshold) remove_key_children.elims add_diff_cancel_right' dist(1) distinct_mem_diff_mset hp.sel(1)
        hp_prev_children_None_notin list.distinct(2) list.sel(1) mset_subset_eqD node_hd_in_sum node_remove_key_children_in_mset_nodes remove_key_remove_all sum_image_mset_sum_map)
    have ‹hp_next_children k c = Some z ⟹
    hp_prev_children (node z) (Hp x n (remove_key_children k c) # remove_key_children k xs) =
      hp_prev_children (node z) (remove_key_children k c)› for z
      apply (auto simp: hp_prev_children_cons_if split: option.splits simp del: )
      apply (metis add_diff_cancel_right' calculation(1) distinct_mset_in_diff hp_next_children_in_nodes2 node_hd_in_sum sum_image_mset_sum_map)
      apply (metis add_diff_cancel_right' calculation(1) distinct_mset_in_diff hp_next_children_in_nodes2 hp_prev_children_None_notin sum_image_mset_sum_map)
      by (metis ‹remove_key_children k xs ≠ [] ⟹ hp_prev_children (node (hd (remove_key_children k xs))) (remove_key_children k c) = None› option.simps(2))
    moreover have ‹b ∈# sum_list (map mset_nodes c) ⟹ hp_prev_children b xs = None› for b
      by (metis (no_types, lifting) "2"(4) add_diff_cancel_left' distinct_mset_add distinct_mset_in_diff hp_prev_children_None_notin list.map(2) mset_nodes_simps sum_image_mset_sum_map sum_list.Cons)

    moreover have ‹find_key_children k c ≠ None ⟹ xs ≠ [] ⟹ node (hd xs) ∉# mset_nodes (the (find_key_children k c))›
      by (metis (no_types, opaque_lifting) ‹⋀x2. find_key_children k c = Some x2 ⟹ remove_key_children k xs = xs›
        add_diff_cancel_right' calculation(1) calculation(6) distinct_mset_in_diff mset_nodes_find_key_children_subset
        mset_subset_eqD node_in_mset_nodes option.distinct(1) option.exhaust_sel option.sel sum_image_mset_sum_map)
    ultimately show ?case
      supply [[goals_limit=1]]
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›] 2
      apply (simp_all add: remove_key_children_hd_tl split: option.splits if_splits)
      apply (intro conjI impI allI)
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
        done
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
          by (metis (mono_tags, lifting) fun_comp_eq_conv hp_prev_children.simps(2) hp_prev_children.simps(3) hp_prev_children_None_notin hp_prev_children_simps(3) hp_prev_simps list.collapse sum_image_mset_sum_map)
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
        by (smt (verit, ccfv_threshold) None_eq_map_option_iff ‹distinct_mset (sum_list (map mset_nodes (Hp x n (remove_key_children k c) # remove_key_children k xs)))› distinct_mset_add hp_next_children_in_nodes2 hp_prev_children_None_notin hp_prev_in_first_child hp_prev_simps in_find_key_children_notin_remove_key in_the_default_empty_iff inter_iff list.map(2) option.exhaust_sel option.map_sel remove_key_children_notin_unchanged sum_image_mset_sum_map sum_list_simps(2) union_commute union_iff)
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
          apply (simp add: hp_prev_children_cons_if)
          apply (intro conjI impI)
        apply (metis (no_types, lifting) remove_key_children.simps(1) WB_List_More.distinct_mset_mono add_diff_cancel_left' distinct_mset_in_diff hd_remove_key_node_same
          hp.exhaust_sel hp_next_children_in_nodes2 hp_next_children_simps(2) hp_next_children_simps(3) hp_next_simps list.exhaust_sel mset_nodes_simps
          mset_nodes_find_key_children_subset option.sel option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_remove_all sum_image_mset_sum_map
          union_single_eq_member)
          apply (simp add: hp_prev_children_cons_if split: option.splits if_splits)
          apply (metis ‹remove_key_children k xs ≠ [] ⟹ xs ≠ []› hp_next_children_hd_is_hd_tl option_hd_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
          by (metis add_diff_cancel_right' distinct_mset_in_diff hp_next_children_in_nodes2 hp_prev_children_None_notin option.case_eq_if sum_image_mset_sum_map)
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
        apply (auto simp: hp_prev_children_cons_if split: option.splits if_splits)[]
        apply (metis (no_types, lifting) None_eq_map_option_iff in_find_key_children_notin_remove_key in_the_default_empty_iff node_hd_in_sum option.exhaust_sel option.map_sel sum_image_mset_sum_map)
        apply (metis (no_types, lifting) distinct_mset_add hp_prev_children_None_notin in_the_default_empty_iff inter_iff map_option_is_None mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel option_last_Nil option_last_Some_iff(1) sum_mset_sum_list the_default.simps(2))
        by (metis (no_types, lifting) None_eq_map_option_iff add_diff_cancel_right' distinct_mset_in_diff hp_prev_children_None_notin in_the_default_empty_iff mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map)+
      subgoal
        apply (auto split: option.splits if_splits simp: remove_key_children_empty_iff remove_key_children_hd_tl)
        apply (auto simp: hp_prev_children_cons_if hd_remove_key_node_same' remove_key_children_empty_iff comp_def split: option.splits if_splits)[]
        apply (metis list.set_sel(1) node_in_mset_nodes)
        apply (smt (verit, best) Nil_is_map_conv remove_key_children_alt_def filter_empty_conv hd_in_set hd_remove_key_node_same' node_in_mset_nodes option.map(2) the_default.simps(1))
        apply (metis hd_remove_key_node_same hp_next_children_hd_is_hd_tl option_hd_Some_iff(2) remove_key_children_empty_iff remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
        apply (metis ‹xs ≠ [] ⟹ hp_prev_children (node (hd xs)) (remove_key_children k c) = None› option.distinct(1) remove_key_children_notin_unchanged)
        by (metis ‹remove_key_children k xs ≠ [] ⟹ hp_prev_children (node (hd (remove_key_children k xs))) (remove_key_children k c) = None› option.distinct(1) remove_key_children_empty_iff remove_key_children_notin_unchanged)
      subgoal
        by (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
      subgoal
        by (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
      subgoal
        using find_None_not_other
        by (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
      subgoal
        using find_None_not_other find_key_noneD[of k c]
        by (auto split: option.splits if_splits simp: remove_key_children_hd_tl)
      subgoal
        using find_None_not_other
        apply (cases ‹k ∈# sum_list (map mset_nodes c)›)
        apply (auto split: option.splits if_split simp: comp_def remove_key_children_hd_tl)
        apply (auto simp: hp_prev_children_cons_if dest: mset_nodes_find_key_children_subset split: option.splits if_splits)[]
        apply (metis mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.sel option_last_Nil option_last_Some_iff(1) sum_mset_sum_list)
        done
      subgoal
        using find_None_not_other
        apply (auto split: option.splits if_splits
          simp: hp_prev_children_cons_if comp_def remove_key_children_hd_tl)
        done
      done
qed

lemma hp_prev_remove_key_other:
  assumes ‹distinct_mset (mset_nodes xs)› ‹remove_key a xs ≠ None›
  shows ‹hp_prev b (the (remove_key a xs)) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key a xs))) then None
    else if map_option node (hp_next a xs) = Some b then (hp_prev a xs)
    else map_option (the o remove_key a) (hp_prev b xs))›
  using assms hp_prev_children_remove_key_children_other[of ‹hps xs› b a]
  by (cases xs) auto

lemma hp_next_find_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset h)) ⟹ find_key_children a h ≠ None ⟹
  x ∈# mset_nodes (the (find_key_children a h)) ⟹ x ≠a ⟹
  hp_next x (the (find_key_children a h)) = hp_next_children x h›
  apply (induction a h arbitrary: x rule: find_key_children.induct)
  subgoal
    by auto
  subgoal for k xa n c xs y
    apply (auto simp: split: option.splits)
    apply (metis add_diff_cancel_left' distinct_mem_diff_mset hp_next_children_append2)
    apply (metis disjunct_not_in distinct_mset_add find_key_noneD find_key_none_iff hp.sel(1)
      hp_next_None_notin_children hp_next_children_simps(3) mset_map mset_nodes_find_key_children_subset
      mset_subset_eqD option.sel sum_mset_sum_list)
    by (metis (no_types, lifting) add_diff_cancel_left' distinct_mset_add distinct_mset_in_diff
      find_key_noneD find_key_none_iff hp_next_children_append2 mset_nodes_find_key_children_subset
      mset_subset_eqD option.sel sum_image_mset_sum_map)
  done

lemma hp_next_find_key:
  ‹distinct_mset (mset_nodes h) ⟹  find_key a h ≠ None ⟹ x ∈# mset_nodes (the (find_key a h)) ⟹ x ≠a ⟹
  hp_next x (the (find_key a h)) = hp_next x h›
  using hp_next_find_key_children[of ‹hps h› a x]
  by (cases ‹(a,h)› rule: find_key.cases;
    cases ‹a ∈# sum_list (map mset_nodes (hps h))›)
   clarsimp_all

lemma hp_next_find_key_itself:
  ‹distinct_mset (mset_nodes h) ⟹ (find_key a h) ≠ None ⟹ hp_next a (the (find_key a h)) = None›
  using find_key_None_or_itself[of a h]
  apply (cases ‹find_key a h›)
  apply auto
  by (metis add_diff_cancel_left' distinct_mset_add_mset distinct_mset_in_diff distinct_mset_mono'
    hp.exhaust_sel hp_next_None_notin_children mset_nodes_simps mset_nodes_find_key_subset option.sel
    option.simps(2) sum_mset_sum_list union_mset_add_mset_left)


lemma hp_prev_find_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset h)) ⟹ find_key_children a h ≠ None ⟹
  x ∈# mset_nodes (the (find_key_children a h)) ⟹ x ≠a ⟹
  hp_prev x (the (find_key_children a h)) = hp_prev_children x h›
  apply (induction a h arbitrary: x rule: find_key_children.induct)
  subgoal
    by auto
  subgoal for k xa n c xs y
    apply (auto simp: split: option.splits)
    apply (simp add: disjunct_not_in distinct_mset_add)
    apply (smt (verit, ccfv_SIG) find_key_children.elims remove_key_children.simps(2) WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mem_diff_mset find_key_noneD hp.sel(1) hp_prev_None_notin_children hp_prev_children_simps(3) in_find_key_children_notin_remove_key list.distinct(2) list.sel(1) mset_nodes_find_key_children_subset mset_subset_eqD option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map)
    by (metis (no_types, lifting) disjunct_not_in distinct_mset_add find_key_noneD find_key_none_iff hp_prev_children_first_child mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_image_mset_sum_map)
  done

lemma hp_prev_find_key:
  ‹distinct_mset (mset_nodes h) ⟹  find_key a h ≠ None ⟹ x ∈# mset_nodes (the (find_key a h)) ⟹ x ≠a ⟹
  hp_prev x (the (find_key a h)) = hp_prev x h›
  using hp_prev_find_key_children[of ‹hps h› a x]
  by (cases ‹(a,h)› rule: find_key.cases;
    cases ‹a ∈# sum_list (map mset_nodes (hps h))›)
   clarsimp_all

lemma hp_prev_find_key_itself:
  ‹distinct_mset (mset_nodes h) ⟹ (find_key a h) ≠ None ⟹ hp_prev a (the (find_key a h)) = None›
  using find_key_None_or_itself[of a h]
  apply (cases ‹find_key a h›)
  apply auto
  by (metis add_diff_cancel_left' distinct_mset_add_mset distinct_mset_in_diff distinct_mset_mono'
    hp.exhaust_sel hp_prev_None_notin_children mset_nodes_simps mset_nodes_find_key_subset option.sel
    option.simps(2) sum_mset_sum_list union_mset_add_mset_left)

lemma hp_child_find_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset h)) ⟹ find_key_children a h ≠ None ⟹
  x ∈# mset_nodes (the (find_key_children a h)) ⟹
  hp_child x (the (find_key_children a h)) = hp_child_children x h›
  apply (induction a h arbitrary: x rule: find_key_children.induct)
  subgoal
    by auto
  subgoal for k xa n c xs y
    apply (auto simp: hp_child_children_Cons_if split: option.splits)
    using distinct_mem_diff_mset apply fastforce
    apply (metis Groups.add_ac(2) distinct_mset_union find_key_none_iff option.simps(2) sum_image_mset_sum_map)
    apply (metis disjunct_not_in distinct_mset_add hp_child_None_notin_children if_Some_None_eq_None mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_mset_sum_list)
      apply (metis distinct_mset_union find_key_noneD hp_child_children_None_notin hp_child_children_skip_first hp_child_children_skip_last
        hp_child_hp_children_simps2 mset_map mset_subset_eqD option.sel find_key_none_iff mset_nodes_find_key_children_subset
        sum_mset_sum_list)
     by (metis (no_types, lifting) distinct_mset_add find_key_noneD find_key_none_iff hp_child_hp_children_simps2
      mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_image_mset_sum_map)
  done

lemma hp_child_find_key:
  ‹distinct_mset (mset_nodes h) ⟹  find_key a h ≠ None ⟹ x ∈# mset_nodes (the (find_key a h)) ⟹
  hp_child x (the (find_key a h)) = hp_child x h›
  using hp_child_find_key_children[of ‹hps h› a x]
  apply (cases ‹(a,h)› rule: find_key.cases;
    cases ‹a ∈# sum_list (map mset_nodes (hps h))›)
  apply clarsimp_all
  by (metis find_key_none_iff hp_child_hp_children_simps2 mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_image_mset_sum_map)+

lemma find_remove_children_mset_nodes_full:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset h)) ⟹  find_key_children a h = Some x ⟹
  (∑⇩# (mset_nodes `# mset (remove_key_children a h))) + mset_nodes x = ∑⇩# (mset_nodes `# mset h)›
  apply (induction a h rule: find_key_children.induct)
  apply (auto split: if_splits option.splits)
  using distinct_mset_add apply blast
    by (metis (no_types, lifting) disjunct_not_in distinct_mset_add find_key_noneD remove_key_children_notin_unchanged sum_image_mset_sum_map union_assoc union_commute)

lemma find_remove_mset_nodes_full:
  ‹distinct_mset (mset_nodes h) ⟹  remove_key a h = Some y ⟹
  find_key a h = Some ya ⟹  (mset_nodes y + mset_nodes ya) = mset_nodes h›
  apply (induction a h rule: remove_key.induct)
  subgoal for k x n c
    using find_remove_children_mset_nodes_full[of c k ya]
    by (auto split: if_splits)
  done

lemma in_remove_key_in_nodes: ‹remove_key a h ≠ None ⟹ x' ∈# mset_nodes (the (remove_key a h)) ⟹ x' ∈# mset_nodes h›
  by (metis remove_key.simps hp.exhaust_sel mset_nodes.simps not_orig_notin_remove_key option.sel sum_image_mset_sum_map union_iff)

lemma in_find_key_in_nodes: ‹find_key a h ≠ None ⟹ x' ∈# mset_nodes (the (find_key a h)) ⟹ x' ∈# mset_nodes h›
  by (meson mset_nodes_find_key_subset mset_subset_eqD)

lemma in_find_key_notin_remove_key_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset h)) ⟹ find_key_children a h ≠ None ⟹ x ∈# mset_nodes (the (find_key_children a h))⟹ x ∉# ∑⇩# (mset_nodes `# mset (remove_key_children a h))›
  apply (induction a h rule: find_key_children.induct)
  subgoal
    by (auto split: if_splits)
  subgoal for k xa n c xs
          using distinct_mset_union[of ‹sum_list (map mset_nodes c)› ‹sum_list (map mset_nodes xs)›]
        distinct_mset_union[of ‹sum_list (map mset_nodes c)› ‹sum_list (map mset_nodes xs)› ]

    apply (auto 4 3 simp: remove_key_remove_all[simplified] ac_simps dest: find_key_noneD multi_member_split split: option.splits)
    apply (metis find_key_noneD find_key_none_iff mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_image_mset_sum_map)
    apply (metis add_diff_cancel_left' distinct_mset_in_diff mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(1) option.sel sum_image_mset_sum_map)
    apply (metis distinct_mset_union find_key_none_iff option.distinct(1) sum_image_mset_sum_map union_commute)
    apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.sel option.simps(2) sum_image_mset_sum_map)
    apply (metis find_key_none_iff option.simps(2) sum_image_mset_sum_map)
    by (metis add_diff_cancel_right' distinct_mset_in_diff mset_nodes_find_key_children_subset mset_subset_eqD not_orig_notin_remove_key option.sel option.simps(2) sum_image_mset_sum_map)
  done

lemma in_find_key_notin_remove_key:
  ‹distinct_mset (mset_nodes h) ⟹ find_key a h ≠ None ⟹ remove_key a h ≠ None ⟹ x ∈# mset_nodes (the (find_key a h))⟹ x ∉# mset_nodes (the (remove_key a h))›
  using in_find_key_notin_remove_key_children[of ‹hps h› a x]
  apply (cases h)
  apply auto
  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)
  by fastforce

lemma map_option_node_hp_next_remove_key:
  ‹distinct_mset (mset_nodes h) ⟹  map_option node (hp_prev a h) ≠ Some x' ⟹ map_option node (hp_next x' h) =
  map_option (λx. node (the (remove_key a x))) (hp_next x' h)›
  apply (induction x' h rule:hp_next.induct)
  subgoal for aa m s x y children
    apply (auto simp: split: option.splits)
    by (smt (z3) remove_key.simps add_mset_add_single distinct_mset_add_mset distinct_mset_union hp.exhaust_sel hp.sel(1) hp_next_children_simps(1-3)
      hp_prev_None_notin_children hp_prev_children_None_notin hp_prev_children_simps(1) hp_prev_in_first_child hp_prev_skip_hd_children list.map(2) list.sel(1)
      map_option_cong member_add_mset mset_nodes.simps option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map sum_list_simps(2) union_ac(2))
  subgoal by auto
  subgoal by auto
  done

lemma has_prev_still_in_remove_key: ‹distinct_mset (mset_nodes h) ⟹ hp_prev a h ≠ None ⟹ 
  remove_key a h ≠ None ⟹ node (the (hp_prev a h)) ∈# mset_nodes (the (remove_key a h))›
  apply (induction a h rule: hp_prev.induct)
  subgoal for a m s x y children
    apply (cases x)
    apply (auto simp: hp_prev_children.simps(1) split: option.splits)
    using Duplicate_Free_Multiset.distinct_mset_union2 apply blast
    using distinct_mset_add by blast
  subgoal apply auto
    by (smt (verit, del_insts) remove_key.simps remove_key_children.elims
      add_diff_cancel_left' distinct_mset_add_mset hp_prev_children_None_notin hp_prev_simps
      insert_DiffM list.distinct(2) list.sel(1) list.simps(9) mset_nodes.simps option.sel
      option_last_Nil option_last_Some_iff(2) sum_list_simps(2) union_iff)
  subgoal by auto
  done
lemma find_key_head_node_iff: ‹node h = node m' ⟹ find_key (node m') h = Some m' ⟷ h = m'›
  by (cases h) auto

lemma map_option_node_hp_prev_remove_key:
  ‹distinct_mset (mset_nodes h) ⟹  map_option node (hp_next a h) ≠ Some x' ⟹ map_option node (hp_prev x' h) =
  map_option (λx. node (the (remove_key a x))) (hp_prev x' h)›
  apply (induction x' h rule:hp_prev.induct)
  subgoal for aa m s x y children
    apply (auto simp: hp_prev_children.simps(1) split: option.splits)
    apply (metis remove_key.simps hp.exhaust_sel hp.sel(1) hp_next_children_simps(1) option.sel)
    apply (metis add_diff_cancel_right' distinct_mset_add distinct_mset_in_diff hp_next_None_notin hp_next_children_None_notin hp_next_children_simps(3) node_in_mset_nodes option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map union_ac(2))
    apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp_prev_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
    by (metis distinct_mset_add find_key_head_node_iff hp_next_children_simps(2) hp_next_find_key_itself option.distinct(1) option.sel)
  subgoal by auto
  subgoal by auto
  done

lemma ‹distinct_mset (mset_nodes h) ⟹ node y ∈# mset_nodes h ⟹ find_key (node y) h = Some y⟹
  mset_nodes (the (find_key (node y) h)) = mset_nodes y›
  apply (induction ‹node y› h rule: find_key.induct)
  apply auto
  oops

lemma distinct_mset_find_node_next:
  ‹distinct_mset (mset_nodes h) ⟹ find_key n h = Some y ⟹
  distinct_mset (mset_nodes y + (if hp_next n h = None then {#} else (mset_nodes (the (hp_next n h)))))›
  apply (induction n h rule: hp_next.induct)
  subgoal for a m s x ya children
    apply (cases x)
    apply (auto simp: hp_next_children.simps(1)
      split: if_splits option.splits)
    apply (metis distinct_mset_union union_ac(1))
    using distinct_mset_add apply blast
    using distinct_mset_add apply blast
    using distinct_mset_add apply blast
    apply (metis (no_types, opaque_lifting) add_diff_cancel_right' distinct_mset_add distinct_mset_in_diff find_key_noneD hp_next_None_notin hp_next_children_None_notin hp_next_children_simps(3) node_in_mset_nodes option.simps(2) sum_image_mset_sum_map union_lcomm)
    using distinct_mset_add by blast
  subgoal apply (auto simp: hp_next_children.simps(1)
      split: if_splits option.splits)
    apply (metis (no_types, opaque_lifting) remove_key_children.simps(1) WB_List_More.distinct_mset_mono arith_extra_simps(5) ex_Melem_conv list.simps(9) mset_nodes_find_key_children_subset option.distinct(2) option.sel remove_key_remove_all sum_image_mset_sum_map sum_list_simps(2) union_ac(2))
    by (smt (verit, del_insts) find_key.simps find_key_children.elims find_key_children.simps(1) list_tail_coinc option.case_eq_if option.collapse option.discI)
  subgoal
    by (auto simp: split: if_splits)
  done

lemma hp_child_node_itself[simp]: ‹hp_child (node a) a = option_hd (hps a)›
  by (cases a; auto)

lemma find_key_children_itself_hd[simp]:
  ‹find_key_children (node a) [a]  = Some a›
  by (cases a; auto)

lemma hp_prev_and_next_same_node:
  fixes y  h :: ‹('b, 'a) hp›
  assumes ‹distinct_mset (mset_nodes h)› ‹hp_prev x' y ≠ None›
    ‹node yb = x'›
    ‹hp_next (node y) h = Some yb›
    ‹find_key (node y) h = Some y›
  shows ‹False›
proof -
  have x'y: ‹x' ∈# mset_nodes y›
    by (metis assms(2) hp_prev_None_notin)
  have ‹x' ≠ node y›
    using assms(1,2) by (metis assms(3) assms(4) hp_next_not_same_node)
  have ‹remove_key (node y) h ≠ None›
    by (metis remove_key_None_iff find_key_head_node_iff handy_if_lemma hp_next_find_key_itself option.sel assms(1,4))
  moreover have neq: ‹find_key (node y) h ≠ None›
    by (metis find_key.elims find_key_none_iff hp_next_children_None_notin hp_next_simps option.discI assms(4))
  ultimately have ‹node (the (hp_next (node y) h)) ≠ x'›
    using hp_next_remove_key_other[of h ‹node y› x']
      distinct_mset_find_node_next[of h ‹node y›] assms
    by (cases yb) auto
  then show False
    using assms by (auto split: if_splits simp: )
qed

lemma hp_child_children_remove_is_remove_hp_child_children:
  ‹distinct_mset (∑⇩# (mset_nodes `# mset c)) ⟹
   hp_child_children b (c) ≠ None ⟹
   hp_parent_children k (c) = None ⟹
    hp_child_children b ((remove_key_children k c)) ≠ None ⟹
    (hp_child_children b (remove_key_children k c)) = (remove_key k (the (hp_child_children b (c))))›
  apply (induction k c rule: remove_key_children.induct)
  subgoal by auto
  subgoal for k x n c xs
    using distinct_mset_union[of ‹sum_list (map mset_nodes c)› ‹sum_list (map mset_nodes xs)›]
    apply auto
    apply (metis disjunct_not_in distinct_mset_add hp_child_None_notin_children hp_child_children_None_notin hp_child_children_simps(2) option.sel option_last_Nil option_last_Some_iff(2) sum_image_mset_sum_map)
    apply (auto simp: hp_parent_children_cons split: option.splits)
    by (smt (verit) remove_key.simps remove_key_children.elims disjunct_set_mset_diff distinct_mset_add
        distinct_mset_in_diff hp.sel(1) hp_child_children_Cons_if hp_child_children_None_notin hp_child_hd hp_child_hp_children_simps2
        hp_parent_None_iff_children_None list.sel(1) mset_subset_eqD node_remove_key_children_in_mset_nodes option.sel option_hd_Some_iff(2) sum_image_mset_sum_map)
  done

lemma hp_child_remove_is_remove_hp_child:
  ‹distinct_mset (mset_nodes (Hp x n c)) ⟹
   hp_child b (Hp x n c) ≠ None ⟹
   hp_parent k (Hp x n c) = None ⟹
  remove_key k (Hp x n c) ≠ None ⟹
    hp_child b (the (remove_key k (Hp x n c))) ≠ None ⟹
    hp_child b (the (remove_key k (Hp x n c))) = remove_key k (the (hp_child b (Hp x n c)))›
  using hp_child_children_remove_is_remove_hp_child_children[of c b k]
  apply auto
  by (smt (z3) remove_key.elims remove_key_children.elims hp.exhaust_sel hp.inject hp_child_hd
    hp_child_hp_children_simps2 hp_parent_None_iff_children_None list.sel(1) option.sel option_hd_Some_iff(2))


lemma remove_key_children_itself_hd[simp]: ‹distinct_mset (mset_nodes a + sum_list (map mset_nodes list)) ⟹
    remove_key_children (node a) (a # list) = list›
  by (cases a; auto)

lemma hp_child_children_remove_key_children_other_helper:
  assumes
    K: ‹hp_child_children b (remove_key_children k c) = map_option ((the ∘∘ remove_key) k) (hp_child_children b c)› and
    H: ‹node x2a ≠ b›
    ‹hp_parent k (Hp x n c) = Some x2a›
    ‹hp_child b (Hp x n c) = Some y›
    ‹hp_child b (Hp x n (remove_key_children k c)) = Some ya›
  shows
    ‹ya = the (remove_key k y)›
  using  K H
  apply (cases c; cases y)
  apply (auto split: option.splits if_splits)
  apply (metis get_min2.simps get_min2_alt_def hp_parent_simps(1))
  by (metis get_min2.simps get_min2_alt_def hp_parent_simps(1))

lemma hp_child_children_remove_key_children_other:
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset xs))›
  shows ‹hp_child_children b (remove_key_children a xs) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key_children a xs))) then None
    else if map_option node (hp_parent_children a xs) = Some b then (hp_next_children a xs)
    else map_option (the o remove_key a) (hp_child_children b xs))›
  using assms
proof (induction a xs rule: remove_key_children.induct)
    case (1 k)
    then show ?case by auto
  next
    case (2 k x n c xs)
    moreover have ‹distinct_mset
      (sum_list (map mset_nodes c) + sum_list (map mset_nodes (remove_key_children k xs)))›
      ‹x ∉# sum_list (map mset_nodes (remove_key_children k xs))›
      using 2(4) apply auto
      apply (metis distinct_mset_mono' mset_map mset_subset_eq_mono_add_left_cancel node_remove_key_children_in_mset_nodes sum_mset_sum_list)
      by (simp add: not_orig_notin_remove_key)
    moreover have ‹distinct_mset
    (sum_list
      (map mset_nodes (Hp x n (remove_key_children k c) # remove_key_children k xs)))›
      using 2(4) apply (auto simp: not_orig_notin_remove_key)
      by (metis calculation(5) distinct_mset_mono' mset_map node_remove_key_children_in_mset_nodes subset_mset.add_right_mono sum_mset_sum_list)
    moreover have ‹hp_prev_children k xs ≠ None ⟹ remove_key_children k xs ≠ []›
      using 2(4) by (cases xs; cases ‹hd xs›; cases ‹tl xs›) (auto)
    moreover have ‹x = node z ⟹ hp_prev_children k (Hp (node z) n c # xs) = Some z ⟷
      z = Hp x n c ∧ xs ≠ [] ∧ k = node (hd (xs))› for z
      using 2(4) hp_prev_children_in_nodes[of _ c] apply -
      apply (cases ‹xs›; cases z; cases ‹hd xs›)
      using hp_prev_children_in_nodes[of _ c] apply fastforce
      apply (auto simp:  )
      apply (metis "2"(4) hp.inject hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(1) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps list.distinct(1) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl remove_key_remove_all sum_image_mset_sum_map)
      apply (metis "2"(4) hp.inject hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(1) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps in_remove_key_children_changed list.distinct(2) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl sum_image_mset_sum_map)
      by (metis "2"(4) hp.sel(1) hp_prev_children_in_nodes hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps in_remove_key_children_changed list.distinct(2) list.sel(1) list.sel(3) option.sel remove_key_children_hd_tl sum_image_mset_sum_map)
    moreover have ‹xs ≠ [] ⟹ find_key_children (node (hd xs)) xs = Some (hd xs)›
      by (metis find_key_children.simps(2) hp.exhaust_sel list.exhaust_sel)
    ultimately show ?case
      using distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset xs)›  ‹∑⇩# (mset_nodes `# mset c)›, unfolded add.commute[of  ‹∑⇩# (mset_nodes `# mset xs)›]]
        distinct_mset_union[of ‹∑⇩# (mset_nodes `# mset c)›  ‹∑⇩# (mset_nodes `# mset xs)›]
      apply (auto split: option.splits if_splits simp: remove_key_children_hd_tl in_the_default_empty_iff)
      apply (simp add: disjunct_not_in distinct_mset_add)
      apply (auto simp add: hp_parent_children_cons hp_child_children_Cons_if)[]
      apply (metis disjunct_not_in distinct_mset_add hp_child_children_None_notin hp_child_hp_children_simps2 hp_parent_children_in_nodes2 option.distinct(1) sum_image_mset_sum_map)
      apply (metis add_diff_cancel_left' distinct_mset_in_diff hp_child_None_notin_children hp_child_children_simps(2) hp_parent_children_in_nodes2 sum_image_mset_sum_map)
      apply (simp add: hp_parent_children_cons)
      apply (simp add: hp_child_children_Cons_if)
      apply (metis disjunct_not_in distinct_mset_add find_key_none_iff hp_child_None_notin_children mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.sel sum_mset_sum_list)
      apply (smt (verit, del_insts) hp_child.simps(2) hp_child_children_Cons_if hp_child_hd hp_child_hp_children_simps2 list.exhaust_sel list.simps(9) o_apply option.map(2) option.sel option_hd_Some_hd remove_key_notin_unchanged sum_list_simps(2) union_iff)
      apply (metis hp_parent_None_iff_children_None hp_parent_children_None_notin hp_parent_children_append_case hp_parent_children_append_skip_first hp_parent_children_cons mset_map node_hd_in_sum sum_mset_sum_list)


      apply (auto simp add: hp_child_children_Cons_if)[]
      apply (smt (verit, best) ex_hp_node_children_Some_in_mset_nodes hp.sel(1) hp_child_children_remove_is_remove_hp_child_children hp_child_hd hp_child_hp_children_simps2 hp_node_children_None_notin2 hp_parent_children_remove_key_children list.sel(1) option.sel option_hd_Some_iff(2) hd_remove_key_node_same remove_key.simps remove_key_children.elims remove_key_children_notin_unchanged sum_image_mset_sum_map)
      apply (metis add_diff_cancel_left' distinct_mset_in_diff)
      apply (metis add_diff_cancel_left' distinct_mset_in_diff hp_parent_children_None_notin option_last_Nil option_last_Some_iff(2))
      apply (metis (mono_tags, lifting) add_diff_cancel_right' distinct_mset_in_diff hp_child_None_notin_children hp_child_children_None_notin hp_child_children_simps(2) in_find_key_children_notin_remove_key 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 (smt (verit, del_insts) arith_simps(49) disjunct_not_in distinct_mset_add hp_child_None_notin hp_child_children_None_notin hp_child_children_simps(2) in_find_key_notin_remove_key_children member_add_mset mset_nodes_find_key_children_subset mset_nodes_simps option.distinct(1) option.sel subset_mset.le_iff_add sum_image_mset_sum_map union_iff)
      apply (metis add_diff_cancel_right' distinct_mset_in_diff find_key_noneD sum_image_mset_sum_map)
      apply (metis disjunct_not_in distinct_mset_add hp_parent_children_in_nodes2 sum_image_mset_sum_map)
      apply (metis add_diff_cancel_right' distinct_mset_in_diff hp_child_children_Cons_if hp_child_children_None_notin hp_child_hp_children_simps2 hp_parent_children_in_nodes2 sum_image_mset_sum_map)
      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2)[]
      apply (metis disjunct_not_in distinct_mset_add find_key_noneD hp_child_children_None_notin hp_child_hp_children_simps2 hp_next_children_append2 hp_parent_children_in_nodes2 mset_map sum_mset_sum_list)
      apply (metis hp.sel(1) hp_child_hp_children_simps2 hp_next_children_simps(2) hp_next_simps hp_parent_children_in_nodes option.distinct(1) option.sel sum_image_mset_sum_map)
      apply (metis add_diff_cancel_right' distinct_mset_in_diff find_key_noneD sum_image_mset_sum_map)
      apply (metis disjunct_not_in distinct_mset_add find_key_noneD hp_parent_children_None_notin option.distinct(1) sum_image_mset_sum_map)
      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis get_min2.simps get_min2_alt_def hp_child_children_None_notin hp_child_hd hp_next_children_hd_is_hd_tl hp_parent_simps_single_if option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
      apply (metis get_min2.simps get_min2_alt_def hp_child_hd hp_next_children_hd_is_hd_tl hp_parent_simps_single_if option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (smt (z3) add_diff_cancel_right' distinct_mset_in_diff find_key_children_notin get_min2.simps get_min2_alt_def hp.sel(3) hp_child.elims hp_child_children_None_notin hp_next_children_append2 hp_next_children_hd_is_hd_tl hp_parent_simps_single_if option_hd_Nil option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
      apply (metis get_min2.simps get_min2_alt_def hp_child_hd hp_next_children_hd_is_hd_tl hp_next_children_simps(2) hp_next_simps hp_parent_simps_single_if option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (smt (z3) add_diff_cancel_right' distinct_mset_in_diff find_key_children_notin get_min2.simps get_min2_alt_def hp.sel(3) hp_child.elims hp_child_children_None_notin hp_next_children_append2 hp_next_children_hd_is_hd_tl hp_parent_simps_single_if option_hd_Nil option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
      apply (meson disjunct_not_in distinct_mset_add)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis disjunct_not_in distinct_mset_add hp_next_children_None_notin sum_image_mset_sum_map)
      apply (metis hp_child_hp_children_simps2 hp_parent_children_in_nodes option.distinct(1) option.sel sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis (no_types, lifting) add_diff_cancel_left' distinct_mset_in_diff hp_child_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 hp_child_hp_children_simps2 mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(1) option.sel sum_image_mset_sum_map)
      apply (metis (no_types, lifting) add_diff_cancel_left' distinct_mset_in_diff hp_child_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 hp_child_hp_children_simps2 mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(1) option.sel sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis disjunct_not_in distinct_mset_add hp_child_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 hp_child_hp_children_simps2 mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(1) option.sel sum_image_mset_sum_map)
      apply (metis disjunct_not_in distinct_mset_add hp_child_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 hp_child_hp_children_simps2 mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(1) option.sel sum_image_mset_sum_map)


      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)

      apply (metis add_diff_cancel_right' distinct_mset_in_diff hp_parent_children_None_notin option_last_Nil option_last_Some_iff(2))


      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis hp_parent_None_iff_children_None option.distinct(1))
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)
      apply (metis get_min2_alt_def hp_parent_children_hd_None hp_parent_simps_single_if option.distinct(1) sum_image_mset_sum_map)

      apply (metis add_diff_cancel_right' distinct_mset_in_diff find_key_noneD sum_image_mset_sum_map)

      apply (metis disjunct_not_in distinct_mset_add find_key_noneD hp_parent_children_None_notin option.distinct(1) sum_image_mset_sum_map)

      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis find_key_children.simps(1) hp_child_hd hp_child_hp_children_simps2 option.distinct(1) option.simps(8) option_hd_None_iff(2))
      apply (smt (verit, best) find_key_children.elims find_key_children_None_or_itself find_key_noneD
        find_key_none_iff hp.inject hp_child_hd hp_child_hp_children_simps2 hp_parent_None_iff_children_None list.discI list.sel(1)
        map_option_is_None mset_map option.sel option_hd_None_iff(1) remove_key_children.elims sum_mset_sum_list)
      apply (metis (no_types, lifting) remove_key.simps ex_hp_node_children_Some_in_mset_nodes hp_child_remove_is_remove_hp_child
        hp_node_children_None_notin2 is_mset_set_add mset_nodes.simps option.sel sum_image_mset_sum_map union_ac(2))
      apply (metis remove_key_children.simps(1) hp_child.simps(1) hp_child_hp_children_simps2 neq_NilE option.distinct(1) option.simps(8))
      apply (smt (verit, ccfv_SIG) remove_key_children.elims find_key_children_None_or_itself find_key_noneD find_key_none_iff get_min2.simps
        get_min2_alt_def hp.inject hp_child_hd hp_child_hp_children_simps2 hp_parent_simps_single_if list.discI option.map_disc_iff option_hd_None_iff(2)
        option_last_Nil option_last_Some_iff(1) remove_key_children_hp_parent_children_hd_None remove_key_children_notin_unchanged)
      apply (meson hp_child_children_remove_key_children_other_helper)


      apply (auto simp add: hp_child_children_Cons_if hp_parent_children_in_nodes2 hp_parent_children_cons split: option.splits if_splits)[]
      apply (metis find_key_children.simps(1) hp_child_hd hp_child_hp_children_simps2 option.distinct(1) option.simps(8) option_hd_None_iff(2))
        apply (smt (verit) find_key_children_None_or_itself hp.inject hp_child_hd hp_child_hp_children_simps2 hp_parent_simps(1) list_tail_coinc map_option_is_None neq_Nil_conv not_Some_eq option.sel option_hd_None_iff(1) find_key_children.elims remove_key_children.elims)

      apply (metis (no_types, lifting) remove_key.simps ex_hp_node_children_Some_in_mset_nodes hp_child_remove_is_remove_hp_child hp_node_children_None_notin2 is_mset_set_add mset_nodes.simps option.sel sum_image_mset_sum_map union_ac(2))
      apply (metis find_key_children.simps(1) hp_child_hd hp_child_hp_children_simps2 option.distinct(1) option.simps(8) option_hd_None_iff(2))
      apply (smt (verit) find_key_children.elims find_key_children_None_or_itself find_key_noneD find_key_none_iff get_min2.simps get_min2_alt_def hp.inject hp_child_hd hp_child_hp_children_simps2 hp_parent_simps_single_if if_Some_None_eq_None list_tail_coinc map_option_is_None neq_Nil_conv option.sel option_hd_None_iff(1) find_key_children.elims remove_key_children.elims remove_key_children_hp_parent_children_hd_None remove_key_children_notin_unchanged)
      by (meson hp_child_children_remove_key_children_other_helper)
qed

lemma hp_child_remove_key_other:
  assumes ‹distinct_mset (mset_nodes xs)› ‹remove_key a xs ≠ None›
  shows ‹hp_child b (the (remove_key a xs)) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key a xs))) then None
    else if map_option node (hp_parent a xs) = Some b then (hp_next a xs)
    else map_option (the o remove_key a) (hp_child b xs))›
  using assms hp_child_children_remove_key_children_other[of ‹hps xs› b a]
  apply (cases xs)
  apply auto
  apply (metis hp_child_hp_children_simps2 in_the_default_empty_iff mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.map_disc_iff option.map_sel sum_mset_sum_list)
  apply (metis get_min2.simps get_min2_alt_def hp.sel(3) hp_child_hd hp_child_hp_children_simps2 hp_next_children_hd_is_hd_tl hp_parent_children_in_nodes2 hp_parent_simps_single_if option_last_Nil option_last_Some_iff(2) remove_key_children_hd_tl remove_key_children_node_hd sum_image_mset_sum_map)
  apply (metis hp_child_hp_children_simps2 in_the_default_empty_iff map_option_is_None mset_map mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel sum_mset_sum_list)
  apply (case_tac x3; case_tac ‹hd x3›)
  apply (auto simp add: hp_parent_simps_single_if split: option.splits if_splits)
  done

abbreviation hp_score_children where
  ‹hp_score_children a xs ≡ map_option score (hp_node_children a xs)›

lemma hp_score_children_remove_key_children_other:
  assumes ‹distinct_mset (∑⇩# (mset_nodes `# mset xs))›
  shows ‹hp_score_children b (remove_key_children a xs) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key_children a xs))) then None
    else (hp_score_children b xs))›
  using assms apply (induction a xs rule: remove_key_children.induct)
  apply (auto split: option.splits if_splits simp: hp_node_children_Cons_if in_the_default_empty_iff)
  apply (metis find_key_none_iff mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel sum_image_mset_sum_map)
  apply (simp add: disjunct_not_in distinct_mset_add)
  apply (metis disjunct_not_in distinct_mset_add find_key_none_iff mset_nodes_find_key_children_subset mset_subset_eqD option.map_sel sum_image_mset_sum_map)
  apply (metis None_eq_map_option_iff distinct_mset_add find_key_noneD sum_image_mset_sum_map)
  using distinct_mset_add apply blast
  apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(2) option.sel sum_image_mset_sum_map)
  apply (meson not_orig_notin_remove_key)
  apply (metis disjunct_not_in distinct_mset_add hp_node_children_None_notin2 not_orig_notin_remove_key sum_image_mset_sum_map)
  apply (metis distinct_mset_add hp_node_children_None_notin2 sum_image_mset_sum_map)
  apply (metis Duplicate_Free_Multiset.distinct_mset_union2 None_eq_map_option_iff find_key_noneD hp_node_children_None_notin2 sum_image_mset_sum_map union_commute)
  apply (metis None_eq_map_option_iff distinct_mset_add hp_node_children_None_notin2 sum_image_mset_sum_map)
  apply (metis mset_nodes_find_key_children_subset mset_subset_eqD option.distinct(2) option.sel sum_image_mset_sum_map)
  apply (metis add_diff_cancel_right' distinct_mset_add distinct_mset_in_diff find_key_noneD sum_image_mset_sum_map)
  apply (meson not_orig_notin_remove_key)
  by (meson not_orig_notin_remove_key)

abbreviation hp_score where
  ‹hp_score a xs ≡ map_option score (hp_node a xs)›

lemma hp_score_remove_key_other:
  assumes ‹distinct_mset (mset_nodes xs)› ‹remove_key a xs ≠ None›
  shows ‹hp_score b (the (remove_key a xs)) =
    (if b ∈# (the_default {#} (map_option mset_nodes (find_key a xs))) then None
    else (hp_score b xs))›
  using hp_score_children_remove_key_children_other[of ‹hps xs› b a] assms
  apply (cases xs)
  apply (auto split: if_splits simp: in_the_default_empty_iff)
  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 (simp add: hp_node_children_None_notin2)
  by (metis hp.sel(2) hp_node_children_simps2 hp_node_simps option.simps(9))

lemma map_option_node_remove_key_iff:
  ‹(h ≠ None ⟹ distinct_mset (mset_nodes (the h))) ⟹ (h ≠ None ⟹ remove_key a (the h) ≠ None) ⟹
  map_option node h = map_option node (map_option (λx. the (remove_key a x)) h) ⟷ h = None ∨ (h ≠ None ∧ a ≠ node (the h))›
  apply (cases h; cases ‹the h›)
  apply simp
  apply (rule iffI)
  apply simp
  apply auto
  done

lemma sum_next_prev_child_subset:
  ‹distinct_mset (mset_nodes h) ⟹
   ((if hp_next n h = None then {#} else (mset_nodes (the (hp_next n h)))) +
  (if hp_prev n h = None then {#} else (mset_nodes (the (hp_prev n h)))) +
  (if hp_child n h = None then {#} else (mset_nodes (the (hp_child n h))))) ⊆# mset_nodes h›
  apply (induction n h rule: hp_next.induct)
  apply (auto split: option.splits if_splits)
  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) split: if_splits option.splits intro: distinct_mset_mono')[]
  apply (metis distinct_mset_add mset_le_incr_right(2) union_mset_add_mset_right)
  apply (smt (verit, ccfv_threshold) distinct_mset_add hp_next_children_simps(1) hp_next_children_simps(2) hp_prev_children_simps(1) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps mset_subset_eq_add_right option.sel option_last_Nil option_last_Some_iff(2) subset_mset.dual_order.trans union_commute union_mset_add_mset_right)
  apply (smt (verit, ccfv_threshold) Duplicate_Free_Multiset.distinct_mset_union2 Groups.add_ac(2) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' distinct_mem_diff_mset hp_child_children_None_notin hp_next_children_simps(2) hp_prev_children_simps(2) hp_prev_children_simps(3) hp_prev_simps mset_le_subtract_right mset_map mset_subset_eq_mono_add node_in_mset_nodes option.sel option_last_Nil option_last_Some_iff(1) sum_mset_sum_list union_mset_add_mset_right)
  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) split: if_splits option.splits intro: distinct_mset_mono')[]
  apply (metis distinct_mset_add mset_le_incr_right(2) union_mset_add_mset_right)
  apply (metis distinct_mset_add mset_le_incr_right(1) union_mset_add_mset_right)
    
  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right)[]
  apply (metis mset_le_incr_right(2) union_mset_add_mset_right)
  apply (metis hp_child_children_None_notin hp_next_None_notin option.simps(2) sum_image_mset_sum_map)
  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right)[]
  apply (metis hp_next_None_notin node_in_mset_nodes option.simps(2))
  apply (metis mset_le_incr_right(2) union_mset_add_mset_right)
  subgoal
    by (metis hp_next_None_notin hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps(2) hp_prev_None_notin_children hp_prev_simps mset_map option.simps(2) sum_mset_sum_list)
  subgoal
    by (metis hp_prev_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis subset_mset.add_mono union_ac(2) union_mset_add_mset_right)
  subgoal
    by (metis hp_next_None_notin hp_next_children_simps(3) hp_next_children_skip_end hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2))
  subgoal
    by (metis mset_le_incr_right(1) union_mset_add_mset_right)

  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right)[]
  subgoal
    by (metis mset_le_incr_right(2) union_mset_add_mset_right)
  subgoal
    by (metis hp_child_children_None_notin hp_next_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_children_None_notin hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_children_None_notin hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_children_None_notin hp_next_None_notin mset_map option.simps(2) sum_mset_sum_list)

  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]


  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis hp_child_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis subset_mset.add_mono union_ac(2) union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_child_children_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))



  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  subgoal
    by (smt (verit, del_insts) hp.collapse list.exhaust_sel list.simps(9) mset_le_decr_left(1) mset_map mset_nodes.simps subset_mset.dual_order.refl subset_mset_trans_add_mset sum_list_simps(2) sum_mset_sum_list union_ac(2))
  subgoal
    by (metis subset_mset.add_mono union_ac(2) union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_child_children_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)



  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis node_in_mset_nodes)
  subgoal
    by (metis hp_child_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis hp_child_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis subset_mset.add_mono union_commute union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_child_children_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_None_notin hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps(2) hp_prev_children_None_notin mset_map option.distinct(1) sum_mset_sum_list)
  subgoal
    by (metis hp_prev_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis hp_prev_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis hp_child_None_notin hp_next_None_notin hp_next_children_None_notin hp_next_children_simps(3) option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_next_None_notin hp_next_children_None_notin hp_next_children_simps(3) hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_children_None_notin hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)
  subgoal
    by (metis hp_child_None_notin hp_child_children_None_notin option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map)


  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  apply (metis mset_le_incr_right2 union_mset_add_mset_right)
  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis mset_le_incr_right2 union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_prev_None_notin option.distinct(1))
  subgoal
    by (metis hp_child_None_notin hp_prev_None_notin option.distinct(1))
   

  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono'
    intro: mset_le_incr_right mset_le_incr_right subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis mset_le_incr_right2 union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_next_None_notin option.distinct(1))
  

  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono' union_mset_add_mset_right
    intro: mset_le_incr_right mset_le_incr_right2 subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis hp_next_None_notin node_in_mset_nodes option_last_Nil option_last_Some_iff(2))
  subgoal
    by (metis mset_le_incr_right2 union_mset_add_mset_right)
  subgoal
    by (metis hp_child_None_notin hp_next_None_notin option_hd_Nil option_hd_Some_iff(2))
  subgoal
    by (metis hp_next_None_notin node_in_mset_nodes option.simps(2))
  subgoal
    by (metis hp_child_None_notin hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2))
  subgoal
    by (metis hp_child_None_notin hp_prev_None_notin option_hd_Nil option_hd_Some_iff(2))
  subgoal
    by (metis hp_child_None_notin hp_next_None_notin option.simps(2))

  apply (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono' union_mset_add_mset_right
    intro: mset_le_incr_right mset_le_incr_right2 subset_mset_imp_subset_add_mset)[]
  subgoal
    by (metis add_diff_cancel_left' distinct_mset_in_diff hp_child_None_notin option.distinct(1) union_iff)
  subgoal
    by (metis add_diff_cancel_left' distinct_mset_in_diff hp_child_None_notin option.distinct(1) union_iff)
  subgoal
    by (metis add_diff_cancel_left' distinct_mset_in_diff hp_child_None_notin option.distinct(1) union_iff)

  by (auto simp add: hp_next_children.simps(1) hp_prev_children.simps(1) distinct_mset_add disjunct_not_in ac_simps
    split: if_splits option.splits intro: distinct_mset_mono' union_mset_add_mset_right
    intro: mset_le_incr_right mset_le_incr_right2 subset_mset_imp_subset_add_mset)


lemma distinct_sum_next_prev_child:
  ‹distinct_mset (mset_nodes h) ⟹
   distinct_mset ((if hp_next n h = None then {#} else (mset_nodes (the (hp_next n h)))) +
  (if hp_prev n h = None then {#} else (mset_nodes (the (hp_prev n h)))) +
  (if hp_child n h = None then {#} else (mset_nodes (the (hp_child n h)))))›
  using sum_next_prev_child_subset[of h n] by (auto intro: distinct_mset_mono)


lemma node_remove_key_in_mset_nodes:
  ‹remove_key a h ≠ None ⟹ mset_nodes (the (remove_key a h)) ⊆# mset_nodes h›
  apply (induction a h rule: remove_key.induct)
  apply (auto intro: )
  by (metis node_remove_key_children_in_mset_nodes sum_image_mset_sum_map)


lemma no_relative_ancestor_or_notin: ‹hp_parent ( m') h = None ⟹ hp_prev m' h = None ⟹
  hp_next m' h = None ⟹  m' = node h ∨ m' ∉# mset_nodes h›
  apply (induction m' h rule: hp_next.induct)
  apply (auto simp: hp_prev_children_cons_if
    split:option.splits )
  apply (metis hp.exhaust_sel hp_next_children_simps(1) hp_next_children_simps(2) hp_parent_children_cons hp_parent_simps(2) hp_prev_simps option.collapse option.simps(5) option_last_Some_iff(2))
  apply (metis hp_next_children_simps(1) hp_next_children_simps(2) hp_next_children_simps(3) hp_parent_children_cons hp_parent_simps(2) hp_prev_cadr_node hp_prev_children_cons_if option.collapse option.simps(2) option.simps(4) option.simps(5))
  apply (metis hp_next_children_simps(1) hp_next_children_simps(2) hp_next_children_simps(3) hp_parent_children_cons hp_parent_simps(2) hp_prev_cadr_node hp_prev_children_cons_if option.case(1) option.collapse option.simps(2) option.simps(5))
  apply (metis option.simps(2))
  apply (metis option.simps(2))
  apply (metis option.simps(2))
  by (metis hp.exhaust_sel hp_parent_None_iff_children_None hp_parent_children_cons hp_prev_simps list.sel(1) list.simps(3) option.case_eq_if option.simps(2))

lemma hp_node_in_find_key_children:
  "distinct_mset (sum_list (map mset_nodes h)) ⟹ find_key_children x h = Some m' ⟹ a ∈# mset_nodes m' ⟹
  hp_node a m' = hp_node_children a h"
  apply (induction x h arbitrary: m' rule: find_key_children.induct)
  apply (auto split: if_splits option.splits simp: hp_node_children_Cons_if
    disjunct_not_in distinct_mset_add)
  by (metis hp_node_children_simps2)

lemma hp_node_in_find_key0:
  "distinct_mset (mset_nodes h) ⟹ find_key x h = Some m' ⟹ a ∈# mset_nodes m' ⟹
  hp_node a m' = hp_node a h"
  using hp_node_in_find_key_children[of ‹hps h› x m' a]
  apply (cases h)
  apply (auto split: if_splits simp: hp_node_children_Cons_if)
  by (metis hp_node_None_notin2 hp_node_children_None_notin hp_node_children_simps2 sum_image_mset_sum_map)

lemma hp_node_in_find_key:
  "distinct_mset (mset_nodes h) ⟹ find_key x h ≠ None ⟹ a ∈# mset_nodes (the (find_key x h)) ⟹
  hp_node a (the (find_key x h)) = hp_node a h"
  using hp_node_in_find_key0[of h x _ a]
  by auto


context hmstruct_with_prio
begin

definition hmrel :: ‹(('a multiset × ('a, 'v) hp option) × ('a multiset × 'a multiset × ('a ⇒ 'v))) set› where
  ‹hmrel = {((ℬ, xs), (𝒜, b, w)). invar xs ∧ distinct_mset b ∧ 𝒜 = ℬ ∧
     ((xs = None ∧ b = {#}) ∨
       (xs ≠ None ∧ b = mset_nodes (the xs) ∧
       (∀v∈#b. hp_node v (the xs) ≠ None) ∧
       (∀v∈#b. score (the (hp_node v (the xs))) = w v)))}›

lemma hp_score_children_iff_hp_score: ‹xa ∈# sum_list (map mset_nodes list) ⟹ distinct_mset (sum_list (map mset_nodes list)) ⟹
  hp_score_children xa list ≠ None ⟷ (∃x∈set list. hp_score xa x ≠ None ∧ hp_score_children xa list = hp_score xa x ∧ (∀x∈set list - {x}. hp_score xa x = None))›
  apply (induction list)
  apply (auto simp: hp_node_children_Cons_if)
  apply (metis disjunct_not_in distinct_mset_add mset_subset_eqD mset_subset_eq_add_left sum_list_map_remove1)
  apply (metis disjunct_not_in distinct_mset_add mset_subset_eqD mset_subset_eq_add_left sum_list_map_remove1)
  using WB_List_More.distinct_mset_union2 apply blast
  done

lemma hp_score_children_in_iff: ‹xa ∈# sum_list (map mset_nodes list) ⟹ distinct_mset (sum_list (map mset_nodes list)) ⟹
  the (hp_score_children xa list) ∈ A ⟷ (∃x∈set list. hp_score xa x ≠ None ∧ the (hp_score xa x) ∈ A)›
  using hp_score_children_iff_hp_score[of xa list]
  by (auto simp: hp_node_children_Cons_if hp_node_children_None_notin2)

lemma set_hp_is_hp_score_mset_nodes:
  assumes ‹distinct_mset (mset_nodes a)›
  shows ‹set_hp a =  (λv'. the (hp_score v' a)) ` set_mset (mset_nodes a)›
    using assms
  proof (induction a rule: mset_nodes.induct)
    case (1 x1a x2a x3a) note p = this(1) and dist = this(2)
    show ?case (is "?A = ?B")
    proof (standard; standard)
      fix x
      assume xA: ‹x ∈ ?A›
      moreover have ‹⋃ (set_hp ` set x3a) = (λv'. the (hp_score_children v' x3a)) ` set_mset (∑⇩# (mset_nodes `# mset x3a))› (is ‹?X = ?Y›)
      proof -
        have [simp]: ‹x ∈ set x3a ⟹ distinct_mset (mset_nodes x)› for x
          using dist by (simp add: distinct_mset_add sum_list_map_remove1)
        have ‹?X =  (⋃x∈set x3a. (λv'. the (hp_score v' x)) ` set_mset (mset_nodes x))›
          using p dist by (simp add: distinct_mset_add sum_list_map_remove1)
        also have ‹... = (⋃x∈set x3a. (λv'. the (hp_score_children v' x3a)) ` set_mset (mset_nodes x))›
          apply (rule SUP_cong)
          apply simp
          apply (auto intro!: imageI dest!: split_list_first simp: image_Un cong: image_cong)
          apply (subst image_cong)
          apply (rule refl)
          apply (subst hp_node_children_append(1))
          using dist apply auto[]
          apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp_node_children_None_notin2 sum_image_mset_sum_map)
          apply (rule refl)
          apply auto[]
          apply (subst hp_node_children_append(1))
          using dist apply auto[]
          apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp_node_children_None_notin2 sum_image_mset_sum_map)
          apply auto
          done
        also have ‹... = ?Y›
          apply (auto simp add: sum_list_map_remove1)
          by (metis (no_types, lifting) dist distinct_mset_add hp_node_None_notin2 hp_node_children_None_notin2
            hp_score_children_iff_hp_score image_iff mset_nodes.simps option.map_disc_iff sum_image_mset_sum_map)
        finally show ?thesis .
      qed
      ultimately have ‹x=x2a ∨ x ∈ ?Y›
        by simp
      then show ‹x ∈ ?B›
        apply auto
        by (metis (no_types, lifting) "1"(2) add_mset_disjoint(1) distinct_mset_add hp_node_children_simps2 mset_nodes_simps rev_image_eqI)
    next
      fix x
      assume xA: ‹x ∈ ?B›
      moreover have ‹⋃ (set_hp ` set x3a) = (λv'. the (hp_score_children v' x3a)) ` set_mset (∑⇩# (mset_nodes `# mset x3a))› (is ‹?X = ?Y›)
      proof -
        have [simp]: ‹x ∈ set x3a ⟹ distinct_mset (mset_nodes x)› for x
          using dist by (simp add: distinct_mset_add sum_list_map_remove1)
        have ‹?X =  (⋃x∈set x3a. (λv'. the (hp_score v' x)) ` set_mset (mset_nodes x))›
          using p dist by (simp add: distinct_mset_add sum_list_map_remove1)
        also have ‹... = (⋃x∈set x3a. (λv'. the (hp_score_children v' x3a)) ` set_mset (mset_nodes x))›
          apply (rule SUP_cong)
          apply simp
          apply (auto intro!: imageI dest!: split_list_first simp: image_Un cong: image_cong)
          apply (subst image_cong)
          apply (rule refl)
          apply (subst hp_node_children_append(1))
          using dist apply auto[]
          apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp_node_children_None_notin2 sum_image_mset_sum_map)
          apply (rule refl)
          apply auto[]
          apply (subst hp_node_children_append(1))
          using dist apply auto[]
          apply (metis WB_List_More.distinct_mset_union2 add_diff_cancel_right' distinct_mset_in_diff hp_node_children_None_notin2 sum_image_mset_sum_map)
          apply auto
          done
        also have ‹... = ?Y›
          apply (auto simp add: sum_list_map_remove1)
          by (metis (no_types, lifting) dist distinct_mset_add hp_node_None_notin2 hp_node_children_None_notin2
            hp_score_children_iff_hp_score image_iff mset_nodes.simps option.map_disc_iff sum_image_mset_sum_map)
        finally show ?thesis .
      qed
      ultimately have ‹x=x2a ∨ x ∈ ?X›
        apply auto
        by (metis (no_types, lifting) "1"(2) add_mset_disjoint(1) distinct_mset_add hp_node_children_simps2 image_iff mset_nodes.simps sum_image_mset_sum_map)
      then show ‹x ∈ ?A›
        by auto
    qed
qed

definition mop_get_min2 :: ‹_› where
  ‹mop_get_min2 = (λ(ℬ, x). do {
    ASSERT (x ≠ None);
    RETURN (get_min2 x)
  })›

lemma get_min2_mop_prio_peek_min:
  ‹(xs, ys) ∈ hmrel ⟹ fst ys ≠ {#} ⟹
  mop_get_min2 xs ≤ ⇓(Id) (mop_prio_peek_min ys)›
  unfolding mop_prio_peek_min_def hmrel_def prio_peek_min_def mop_get_min2_def
  apply refine_vcg
  subgoal
    by (cases xs; cases ‹the (snd xs)›) auto
  subgoal
    by (cases xs; cases ‹the (snd xs)›) auto
  subgoal
    using set_hp_is_hp_score_mset_nodes[of ‹hd (hps (the (snd xs)))›]
    apply (cases xs; cases ‹the (snd xs)›)
    apply (auto simp: invar_def)
    using le apply blast
    apply (cases ‹hps (the (snd xs))›)
    apply simp
    apply (auto split: if_splits option.splits simp: distinct_mset_union in_mset_sum_list_iff
      dest!: split_list)
    apply (metis (no_types, lifting) hp_node_None_notin2 mem_simps(3) option.exhaust_sel option.map_sel)
    by (smt (z3) diff_union_cancelR distinct_mset_add distinct_mset_in_diff hp_node_None_notin2
      hp_node_children_None_notin2 hp_node_children_append(1) hp_node_children_simps(3)
      hp_node_children_simps2 mset_map option.map_sel rev_image_eqI set_hp_is_hp_score_mset_nodes set_mset_union sum_mset_sum_list union_iff)
  done

lemma get_min2_mop_prio_peek_min2:
  ‹(xs, ys) ∈ hmrel ⟹
  mop_get_min2 xs ≤ ⇓{(a,b). (a,b)∈Id ∧ b = get_min2 (snd xs)} (mop_prio_peek_min ys)›
  unfolding mop_prio_peek_min_def hmrel_def prio_peek_min_def mop_get_min2_def
  apply refine_vcg
  subgoal
    by (cases xs; cases ‹the (snd xs)›) auto
  subgoal
    using set_hp_is_hp_score_mset_nodes[of ‹hd (hps (the (snd xs)))›]
    unfolding conc_fun_RES
    apply (cases xs; cases ‹the (snd xs)›)
    apply (auto simp: invar_def)
    using le apply blast
    apply (cases ‹hps (the (snd xs))›)
    apply simp
    apply (auto split: if_splits option.splits simp: distinct_mset_union in_mset_sum_list_iff
      dest!: split_list)
    apply (metis (no_types, lifting) hp_node_None_notin2 mem_simps(3) option.exhaust_sel option.map_sel)
    by (smt (z3) diff_union_cancelR distinct_mset_add distinct_mset_in_diff hp_node_None_notin2
      hp_node_children_None_notin2 hp_node_children_append(1) hp_node_children_simps(3)
      hp_node_children_simps2 mset_map option.map_sel rev_image_eqI set_hp_is_hp_score_mset_nodes set_mset_union sum_mset_sum_list union_iff)
  done

lemma del_min_None_iff: ‹del_min a = None ⟷ a = None ∨ hps (the a) = []›
  by (cases a; cases ‹the a›) (auto simp: pass12_merge_pairs)

lemma score_hp_node_pass⇩1: ‹distinct_mset (sum_list (map mset_nodes x3)) ⟹ score (the (hp_node_children v (pass⇩1 x3))) = score (the (hp_node_children v x3))›
  apply (induction x3 rule: pass⇩1.induct)
  subgoal by auto
  subgoal by auto
  subgoal for h1 h2 hs
    apply (cases h1; cases h2)
    apply (auto simp: hp_node_children_Cons_if split: option.splits)
    using WB_List_More.distinct_mset_union2 apply blast
    apply (metis hp_node_children_None_notin2 sum_image_mset_sum_map)
    by (metis diff_union_cancelL distinct_mset_in_diff union_iff)
  done

lemma node_pass⇩2_in_nodes: ‹pass⇩2 hs ≠ None ⟹ mset_nodes (the (pass⇩2 hs)) ⊆# sum_list (map mset_nodes hs)›
  by (induction hs rule: pass⇩2.induct) (fastforce split: option.splits simp del: mset_nodes_pass⇩2)+

lemma score_pass2_same:
  ‹distinct_mset (sum_list (map mset_nodes x3)) ⟹ pass⇩2 x3 ≠ None ⟹v ∈# sum_list (map mset_nodes x3) ⟹
  score (the (hp_node v (the (pass⇩2 x3)))) = score (the (hp_node_children v x3))›
  apply (induction x3 rule: pass⇩2.induct)
  subgoal by auto
  subgoal for h hs
    using node_pass⇩2_in_nodes[of hs]
    apply (cases h; cases ‹the (pass⇩2 hs)›)
    apply (auto split: option.splits simp: hp_node_children_None_notin2 hp_node_children_Cons_if distinct_mset_add)
    apply (metis mset_subset_eq_insertD option_last_Nil option_last_Some_iff(1) pass⇩2.simps(1))
    apply (metis disjunct_not_in mset_subset_eq_insertD not_Some_eq pass⇩2.simps(1))
    apply (metis mset_subset_eq_insertD option_last_Nil option_last_Some_iff(1) pass⇩2.simps(1))
    apply (metis disjunct_not_in mset_subset_eq_insertD not_Some_eq pass⇩2.simps(1))
    apply (metis disjunct_not_in hp_node_None_notin2 hp_node_children_simps2 mset_nodes_pass⇩2 not_Some_eq option.sel)
    apply (metis option.distinct(2) pass⇩2.simps(1))
    apply (metis option.distinct(2) pass⇩2.simps(1))
    apply (metis option.distinct(2) pass⇩2.simps(1))
    apply (metis option.distinct(2) pass⇩2.simps(1))
    apply (meson disjunct_not_in insert_subset_eq_iff)
    apply (meson disjunct_not_in insert_subset_eq_iff)
    apply (meson disjunct_not_in insert_subset_eq_iff)
    apply (meson disjunct_not_in ex_hp_node_children_Some_in_mset_nodes mset_le_add_mset mset_subset_eqD)
    done
  done

lemma score_hp_node_merge_pairs_same: ‹distinct_mset (sum_list (map mset_nodes x3)) ⟹ v ∈# sum_list (map mset_nodes x3) ⟹
  score (the (hp_node v (the (merge_pairs x3)))) = score (the (hp_node_children v x3))›
  unfolding pass12_merge_pairs[symmetric]
  apply (subst score_pass2_same score_hp_node_pass⇩1)
  apply simp_all
  apply (metis in_multiset_nempty list.map(1) mset_nodes_pass⇩1 sum_list.Nil)
  by (meson score_hp_node_pass⇩1)
term mop_get_min2

definition mop_hm_pop_min :: ‹_› where
  ‹mop_hm_pop_min = (λ(ℬ, x). do {
    ASSERT (x ≠ None);
    m ← mop_get_min2 (ℬ, x);
    RETURN (m, (ℬ, del_min x))
  })›

lemma get_min2_del_min2_mop_prio_pop_min:
  assumes ‹(xs, ys) ∈ hmrel›
  shows ‹mop_hm_pop_min xs ≤ ⇓(Id ×⇩r hmrel) (mop_prio_pop_min ys)›
proof -
  have mop_prio_pop_min_def: ‹mop_prio_pop_min ys = do {
    ASSERT (fst (snd ys)≠{#});
   v ← local.mop_prio_peek_min ys;
   bw ← mop_prio_del v ys;
   RETURN (v, bw)
    }›
    unfolding mop_prio_pop_min_def local.mop_prio_peek_min_def nres_monad3
    by (cases ys) (auto simp: summarize_ASSERT_conv)
  show ?thesis
    (*  using get_min2_mop_prio_peek_min[of xs ys]*)
    using assms
    unfolding mop_prio_pop_min_def mop_prio_del_def prio_peek_min_def prio_peek_min_def
      nres_monad3 case_prod_beta mop_hm_pop_min_def 
    apply (refine_vcg get_min2_mop_prio_peek_min2)
    subgoal by (auto simp: hmrel_def)
    subgoal by auto
    subgoal
      apply (cases ‹the (snd xs)›; cases xs)
      apply (auto simp: hmrel_def invar_del_min del_min_None_iff pass12_merge_pairs prio_del_def
        mset_nodes_merge_pairs invar_Some intro!: invar_merge_pairs)
      apply (metis hp_node_children_simps2 score_hp_node_merge_pairs_same)
      apply (metis list.map(1) mset_nodes_merge_pairs pairing_heap_assms.merge_pairs_None_iff sum_list.Nil)
      apply (metis list.map(1) mset_nodes_merge_pairs pairing_heap_assms.merge_pairs_None_iff sum_list.Nil)
      by (metis hp_node_children_simps2 score_hp_node_merge_pairs_same)
    done
qed

definition mop_hm_insert :: ‹_› where
  ‹mop_hm_insert = (λw v (ℬ, xs). do {
    ASSERT (w ∈# ℬ ∧ (xs ≠ None ⟶ w ∉# mset_nodes (the xs)));
    RETURN (ℬ, insert w v xs)
  })›

lemma mop_prio_insert:
  ‹(xs, ys) ∈ hmrel ⟹
  mop_hm_insert w v xs ≤ ⇓(hmrel) (mop_prio_insert w v ys)›
  unfolding mop_prio_insert_def mop_hm_insert_def
  apply refine_vcg
  subgoal by (auto simp: hmrel_def)
  subgoal by (auto simp: hmrel_def)
  subgoal for a b
    apply (auto simp: hmrel_def invar_Some php_link le)
    apply (smt (verit, del_insts) hp.exhaust_sel hp.inject hp_node_children_simps(3) hp_node_children_simps2
      hp_node_simps link.simps node_in_mset_nodes option.sel option_last_Nil option_last_Some_iff(2))
    by (smt (verit, ccfv_threshold) add.right_neutral diff_single_trivial distinct_mset_in_diff hp.sel(1,2) hp_node_None_notin2
      hp_node_children_simps(2) hp_node_children_simps(3) hp_node_children_simps2 hp_node_node_itself
      list.simps(8) mset_nodes_simps option.sel link.simps php.elims(2) sum_list_simps(1))
  done

lemma find_key_node_itself[simp]: ‹find_key (node y) y = Some y›
  by (cases y) auto

lemma invar_decrease_key: ‹le v x ⟹
      invar (Some (Hp w x x3)) ⟹ invar (Some (Hp w v x3))›
  by (auto simp: invar_def intro!: transpD[OF trans, of v x])

lemma find_key_children_single[simp]: ‹find_key_children k [x] = find_key k x›
  by (cases x; auto split: option.splits)

lemma hp_node_find_key_children:
  ‹distinct_mset (sum_list (map mset_nodes a)) ⟹ find_key_children x a ≠ None ⟹
  hp_node x (the (find_key_children x a)) ≠ None ⟹
  hp_node x (the (find_key_children x a)) = hp_node_children x a›
  apply (induction x a rule: find_key_children.induct)
  apply (auto split: option.splits)
  apply (metis WB_List_More.distinct_mset_union2 find_key_noneD sum_image_mset_sum_map)
  by (metis distinct_mset_add find_key_noneD hp_node_None_notin2 hp_node_children_Cons_if hp_node_children_simps2 sum_image_mset_sum_map)

lemma hp_node_find_key:
  ‹distinct_mset (mset_nodes a) ⟹ find_key x a ≠ None ⟹ hp_score x (the (find_key x a)) ≠ None ⟹
  hp_score x (the (find_key x a)) = hp_score x a›
  using hp_node_find_key_children[of ‹hps a› x]
  apply (cases a)
  apply auto
  by (metis find_key_noneD sum_image_mset_sum_map)

lemma score_hp_node_link:
  ‹distinct_mset (mset_nodes a + mset_nodes b) ⟹
  map_option score (hp_node w (link a b)) = (case hp_node w a of Some a ⇒ Some (score a)
  | _ ⇒ map_option score (hp_node w b))›
  apply (cases a; cases b)
  apply (auto split: option.splits)
  by (metis (no_types, opaque_lifting) distinct_mset_iff ex_hp_node_children_Some_in_mset_nodes mset_add union_mset_add_mset_left union_mset_add_mset_right)

lemma hp_node_link_none_iff_parents: ‹hp_node va (link a b) = None ⟷ hp_node va a = None ∧ hp_node va b = None›
  by auto

lemma score_hp_node_link2:
  ‹distinct_mset (mset_nodes a + mset_nodes b) ⟹ (hp_node w (link a b)) ≠ None ⟹
  score (the (hp_node w (link a b))) = (case hp_node w a of Some a ⇒ (score a)
  | _ ⇒ score (the (hp_node w b)))›
  using score_hp_node_link[of a b w] by (cases ‹hp_node w (link a b)›; cases ‹hp_node w b›)
   (auto split: option.splits)


definition mop_hm_decrease_key :: ‹_› where
  ‹mop_hm_decrease_key = (λw v (ℬ, xs). do {
  ASSERT (w ∈# ℬ);
    if xs = None then RETURN (ℬ, xs)
    else RETURN (ℬ, decrease_key w v (the xs))
  })›

lemma decrease_key_mop_prio_change_weight:
  assumes ‹(xs, ys) ∈ hmrel›
  shows ‹mop_hm_decrease_key w v xs ≤ ⇓(hmrel) (mop_prio_change_weight w v ys)›
proof -
  let ?w = ‹snd (snd ys)›
  let ?xs = ‹snd xs›
  have K: ‹xs' = ?xs ⟹ node (the xs') ≠ w ⟷ remove_key w (the ?xs)≠ None› for xs'
    using assms by (cases xs; cases ‹the ?xs›) (auto simp: hmrel_def)
  have [simp]: ‹add_mset (node x2a) (sum_list (map mset_nodes (hps x2a))) = mset_nodes x2a› for x2a
    by (cases x2a) auto
  have f: ‹w ∈# fst (snd ys) ⟹ find_key w (the ?xs) = Some (Hp w (?w w) (hps (the (find_key w (the ?xs)))))›
    using assms invar_find_key[of ‹the ?xs› w] find_key_None_or_itself[of w ‹the ?xs›]
       find_key_none_iff[of w ‹[the ?xs]›]
       hp_node_find_key[of ‹the ?xs› w]
    apply (cases ‹the (find_key w (the ?xs))›; cases ‹find_key w (the ?xs)›)
    apply simp_all
    apply (auto simp: hmrel_def invar_Some)
    by (metis hp_node_None_notin2 option.map_sel option.sel)

  then have ‹w ∈# fst (snd ys) ⟹ invar (Some (Hp w (?w w) (hps (the (find_key w (the ?xs))))))›
    using assms invar_find_key[of ‹the ?xs› w] by (auto simp: hmrel_def invar_Some)
  moreover have ‹w ∈# fst (snd ys) ⟹ find_key w (the ?xs) ≠ None ⟹ remove_key w (the ?xs) ≠ None ⟹
    distinct_mset (mset_nodes (Hp w v (hps (the (find_key w (the ?xs))))) + mset_nodes (the (remove_key w (the ?xs))))›
    using assms distinct_mset_find_node_next[of ‹the ?xs› w ‹the (find_key w (the ?xs))›]
    apply (subst ‹w ∈# fst (snd ys) ⟹ find_key w (the ?xs) = Some (Hp w (?w w) (hps (the (find_key w (the ?xs)))))›) apply (auto simp: hmrel_def)
    apply (metis ‹⋀x2a. add_mset (node x2a) (sum_list (map mset_nodes (hps x2a))) = mset_nodes x2a› distinct_mset_add distinct_mset_add_mset find_key_None_or_itself option.distinct(1) option.sel)
    apply (metis find_key_None_or_itself in_find_key_notin_remove_key node_in_mset_nodes option.distinct(1) option.sel)
    by (metis (no_types, opaque_lifting) Groups.add_ac(2) ‹⋀x2a. add_mset (node x2a) (sum_list (map mset_nodes (hps x2a))) = mset_nodes x2a› distinct_mset_add_mset find_remove_mset_nodes_full union_mset_add_mset_right)
  ultimately show ?thesis
    using assms
    unfolding mop_prio_change_weight_def mop_hm_decrease_key_def
    apply refine_vcg
    subgoal by (auto simp: hmrel_def)
    subgoal by (auto simp: hmrel_def)
    subgoal
      using invar_decrease_key[of v ‹?w w› w ‹hps (the (find_key w (the ?xs)))›]
        find_key_none_iff[of w ‹[the ?xs]›] find_key_None_or_itself[of w ‹the ?xs›]
        invar_find_key[of ‹the ?xs› w] hp_node_find_key[of ‹the ?xs› w] f
        find_remove_mset_nodes_full[of ‹the ?xs› w ‹the (remove_key w (the ?xs))› ‹the(find_key w (the ?xs))›]
        hp_node_in_find_key0[of ‹the ?xs› w ‹the(find_key w (the ?xs))›]
      apply (auto simp: hmrel_def decrease_key_def remove_key_None_iff invar_def score_hp_node_link2
        simp del: find_key_none_iff php.simps
        intro:
        split: option.splits hp.splits)
      apply (metis hp_node_None_notin2 hp_node_children_None_notin2 hp_node_children_simps2 sum_image_mset_sum_map)
      apply (metis hp_node_children_simps2)
      apply (metis invar_Some php_link php_remove_key)
      apply (metis union_ac(2))
      apply (metis member_add_mset union_iff)

      using K apply (solves ‹simp add: score_hp_node_link2 del: php.simps›)

      using K apply (simp add: score_hp_node_link2 del: php.simps)
      apply (subst score_hp_node_link2)
      apply (solves simp)
      apply (simp add: hp_node_link_none_iff_parents)
      apply (auto split: option.splits)
      apply (metis member_add_mset mset_cancel_union(2))
      apply (smt (verit, ccfv_threshold) hp_node_None_notin2 hp_node_children_None_notin2
        hp_score_remove_key_other map_option_is_None member_add_mset option.map_sel
        option.sel option_hd_Nil option_hd_Some_iff(2) sum_image_mset_sum_map union_iff)
      by (metis hp_node_None_notin2 hp_node_children_simps2 hp_node_in_find_key0 option.sel option_hd_Nil option_hd_Some_iff(2))
    done
qed

lemma pass⇩1_empty_iff[simp]: ‹pass⇩1 x = [] ⟷ x= []›
  by (cases x rule: pass⇩1.cases) auto

lemma sum_list_map_mset_nodes_empty_iff[simp]: ‹sum_list (map mset_nodes x3) = {#} ⟷ x3 = []›
  by (cases x3; cases ‹hd x3›) auto

lemma hp_score_link:
  ‹a ∈# mset_nodes h1 ⟹ distinct_mset (mset_nodes h1 + mset_nodes h2) ⟹ hp_score a (link h1 h2) = hp_score a h1›
  apply (cases h1; cases h2)
  apply (auto split: option.splits simp add: hp_node_children_None_notin2)
 by (metis diff_union_cancelL distinct_mem_diff_mset ex_hp_node_children_Some_in_mset_nodes hp_node_children_simps2)

lemma hp_score_link_skip_first[simp]:
  ‹a ∉# mset_nodes h1 ⟹ hp_score a (link h1 h2) = hp_score a h2›
  by (cases h1; cases h2)
   (auto split: option.splits simp add: hp_node_children_None_notin2)

lemma hp_score_merge_pairs:
  ‹distinct_mset (sum_list (map mset_nodes ys)) ⟹ merge_pairs ys ≠ None ⟹
    hp_score a (the (merge_pairs (ys))) = hp_score_children a (ys)›
  apply (induction ys rule: pass⇩1.induct)
  apply (auto simp add: hp_node_children_Cons_if Let_def
    split: option.splits)
  apply (simp add: disjunct_not_in distinct_mset_add hp_score_link)
  apply (subst hp_score_link)
    apply simp
    apply simp
  apply (metis mset_nodes_merge_pairs option.sel option_hd_Nil option_hd_Some_iff(2) union_assoc)
  apply (metis Groups.add_ac(1) distinct_mset_union hp_score_link)
  apply (subst hp_score_link)
    apply simp
    apply simp
  apply (metis mset_nodes_merge_pairs option.sel option_hd_Nil option_hd_Some_iff(2) union_assoc)
    apply (meson hp_score_link_skip_first)
  apply (subst hp_score_link)
    apply simp
    apply simp
  apply (metis mset_nodes_merge_pairs option.sel option_hd_Nil option_hd_Some_iff(2) union_assoc)
  apply (metis Groups.add_ac(1) distinct_mset_union hp_score_link)
  by (metis Duplicate_Free_Multiset.distinct_mset_union2 merge_pairs_None_iff option.simps(2))


definition decrease_key2 where
  ‹decrease_key2 a w h = (if h = None then None else decrease_key a w (the h))›
lemma hp_mset_rel_def:  ‹hmrel = {((ℬ, h), (𝒜, m, w)). distinct_mset m ∧ 𝒜=ℬ ∧
  (h = None ⟷ m = {#}) ∧
  (m ≠ {#} ⟶ (mset_nodes (the h) = m ∧ (∀a∈#m. Some (w a) = hp_score a (the h)) ∧ invar h))}›
  unfolding hmrel_def
  apply (auto simp:)
  apply (metis in_multiset_nempty node_in_mset_nodes)
  apply (simp add: option.expand option.map_sel)
  apply (metis Some_to_the hp_node_None_notin2 option.map_sel)
  by (metis Some_to_the hp_node_None_notin2 option.map_sel)


lemma (in -)find_key_None_remove_key_ident: ‹find_key a h = None ⟹ remove_key a h = Some h›
  by (induction a h rule: find_key.induct)
   (auto split: if_splits)

lemma decrease_key2:
  assumes ‹(x, m) ∈ hmrel› ‹(a,a')∈Id› ‹(w,w')∈Id› ‹le w (snd (snd m) a)›
  shows ‹mop_hm_decrease_key a w x ≤ ⇓ (hmrel) (mop_prio_change_weight a' w' m)›
proof -
  show ?thesis
    using assms
    unfolding decrease_key2_def
      mop_prio_insert_def mop_prio_change_weight_def mop_hm_decrease_key_def
    apply refine_rcg
    subgoal by (auto simp: hmrel_def)
    subgoal
       using php_decrease_key[of ‹the (snd x)› w a]
      apply (auto simp: hp_mset_rel_def decrease_key_def invar_def split: option.splits hp.splits)
       apply (metis find_key_None_remove_key_ident in_remove_key_changed option.sel option.simps(2))
       apply (metis empty_neutral(1) find_key_head_node_iff hp.sel(1) mset_map mset_nodes.simps option.simps(1) remove_key_None_iff sum_mset_sum_list union_mset_add_mset_left)
       apply (metis find_key_node_itself hp.sel(1) hp_node_children_simps2 option.sel remove_key_None_iff)
      apply (metis find_key_node_itself find_key_notin hp.sel(2) hp_node_node_itself option.distinct(1) option.map_sel option.sel remove_key_None_iff)
      apply (metis invar_Some invar_find_key php.simps)
       apply (metis (no_types, lifting) add_mset_add_single find_key_None_or_itself find_remove_mset_nodes_full hp.sel(1) mset_nodes_simps option.sel option.simps(2) union_commute union_mset_add_mset_left)
      apply (smt (verit) Duplicate_Free_Multiset.distinct_mset_mono disjunct_not_in distinct_mset_add find_key_None_or_itself hp.sel(1) hp.sel(2) hp_node_simps hp_score_link in_find_key_notin_remove_key mset_nodes.simps mset_nodes_find_key_subset node_remove_key_in_mset_nodes option.distinct(1) option.sel option.simps(9) union_iff union_single_eq_member)
      apply (smt (verit) disjunct_not_in distinct_mset_add find_key_None_or_itself find_remove_mset_nodes_full hp.sel(1) hp_node_None_notin2 hp_node_children_simps2 hp_node_in_find_key0 hp_score_link hp_score_link_skip_first hp_score_remove_key_other map_option_is_None mset_nodes_simps option.distinct(1) option.sel union_iff)
      by (metis find_key_None_or_itself find_key_notin hp.sel(1) hp.sel(2) hp_node_find_key hp_node_simps option.distinct(1) option.sel option.simps(9))
    done
qed

end

interpretation ACIDS: hmstruct_with_prio where
  le = ‹(≥) :: nat ⇒ nat ⇒ bool› and
  lt = ‹(>)›
  apply unfold_locales
  subgoal by auto
  subgoal by auto
  subgoal by (auto simp: transp_def)
  subgoal by (auto simp: totalp_on_def)
  done

end