Theory IKKBZ

(* Author: Bernhard Stöckl *)

theory IKKBZ
  imports Complex_Main "CostFunctions" "QueryGraph" "List_Dtree" "HOL-Library.Sorting_Algorithms"
begin

section ‹IKKBZ›

subsection ‹Additional Proofs for Merging Lists›

lemma merge_comm_if_not_equiv: "∀x ∈ set xs. ∀y ∈ set ys. compare cmp x y ≠ Equiv ⟹
  Sorting_Algorithms.merge cmp xs ys = Sorting_Algorithms.merge cmp ys xs"
  apply(induction xs ys rule: Sorting_Algorithms.merge.induct)
  by(auto intro: compare.quasisym_not_greater simp: compare.asym_greater)

lemma set_merge: "set xs ∪ set ys = set (Sorting_Algorithms.merge cmp xs ys)"
  using mset_merge set_mset_mset set_mset_union by metis

lemma input_empty_if_merge_empty: "Sorting_Algorithms.merge cmp xs ys = [] ⟹ xs = [] ∧ ys = []"
  using Un_empty set_empty2 set_merge by metis

lemma merge_assoc:
  "Sorting_Algorithms.merge cmp xs (Sorting_Algorithms.merge cmp ys zs)
  = Sorting_Algorithms.merge cmp (Sorting_Algorithms.merge cmp xs ys) zs"
  (is "?merge _ xs (?merge cmp _ zs) = _")
proof(induction xs "?merge cmp ys zs" arbitrary: ys zs taking: cmp rule: Sorting_Algorithms.merge.induct)
  case (2 cmp v vs)
  show ?case using input_empty_if_merge_empty[OF 2[symmetric]] by simp
next
  case ind: (3 x xs r rs)
  then show ?case
  proof(induction ys zs taking: cmp rule: Sorting_Algorithms.merge.induct)
    case (3 y ys z zs)
    then show ?case
      using ind compare.asym_greater
      by (smt (verit, best) compare.trans_not_greater list.inject merge.simps(3))
  qed (auto)
qed (simp)

lemma merge_comp_commute:
  assumes "∀x ∈ set xs. ∀y ∈ set ys. compare cmp x y ≠ Equiv"
  shows "Sorting_Algorithms.merge cmp xs (Sorting_Algorithms.merge cmp ys zs)
        = Sorting_Algorithms.merge cmp ys (Sorting_Algorithms.merge cmp xs zs)"
  using assms merge_assoc merge_comm_if_not_equiv by metis

lemma wf_list_arcs_merge:
  "⟦wf_list_arcs xs; wf_list_arcs ys; snd ` set xs ∩ snd ` set ys = {}⟧
    ⟹ wf_list_arcs (Sorting_Algorithms.merge cmp xs ys)"
proof(induction xs ys taking: cmp rule: Sorting_Algorithms.merge.induct)
  case (3 x xs y ys)
  obtain v1 e1 where v1_def[simp]: "x = (v1,e1)" by force
  obtain v2 e2 where v2_def[simp]: "y = (v2,e2)" by force
  show ?case
  proof(cases "compare cmp x y = Greater")
    case True
    have "e2 ∉ snd ` set (x#xs)" using "3.prems"(3) by auto
    moreover have "e2 ∉ snd ` set ys" using "3.prems"(2) by simp
    ultimately have "e2 ∉ snd ` set (Sorting_Algorithms.merge cmp (x#xs) ys)"
      using set_merge by fast
    then show ?thesis using True 3 by force
  next
    case False
    have "e1 ∉ snd `set (y#ys)" using "3.prems"(3) by auto
    moreover have "e1 ∉ snd ` set xs" using "3.prems"(1) by simp
    ultimately have "e1 ∉ snd `set (Sorting_Algorithms.merge cmp xs (y#ys))"
      using set_merge by fast
    then show ?thesis using False 3 by force
  qed
qed (auto)

lemma wf_list_lverts_merge:
  "⟦wf_list_lverts xs; wf_list_lverts ys;
    ∀v1 ∈ fst ` set xs. ∀v2 ∈ fst ` set ys. set v1 ∩ set v2 = {}⟧
    ⟹ wf_list_lverts (Sorting_Algorithms.merge cmp xs ys)"
proof(induction xs ys taking: cmp rule: Sorting_Algorithms.merge.induct)
  case (3 x xs y ys)
  obtain v1 e1 where v1_def[simp]: "x = (v1,e1)" by force
  obtain v2 e2 where v2_def[simp]: "y = (v2,e2)" by force
  show ?case
  proof(cases "compare cmp x y = Greater")
    case True
    have "∀v ∈ fst ` set (x#xs). set v2 ∩ set v = {}" using "3.prems"(3) by auto
    moreover have "∀v ∈ fst ` set ys. set v2 ∩ set v = {}" using "3.prems"(2) by simp
    ultimately have "∀v ∈ fst ` set (Sorting_Algorithms.merge cmp (x#xs) ys). set v2 ∩ set v = {}"
      using set_merge[of "x#xs"] by blast
    then show ?thesis using True 3 by force
  next
    case False
    have "∀v ∈ fst ` set (y#ys). set v1 ∩ set v = {}" using "3.prems"(3) by auto
    moreover have "∀v ∈ fst ` set xs. set v1 ∩ set v = {}" using "3.prems"(1) by simp
    ultimately have "∀v ∈ fst ` set (Sorting_Algorithms.merge cmp xs (y#ys)). set v1 ∩ set v = {}"
      using set_merge[of xs] by auto
    then show ?thesis using False 3 by force
  qed
qed (auto)

lemma merge_hd_exists_preserv:
  "⟦∃(t1,e1) ∈ fset xs. hd as = (root t1,e1); ∃(t1,e1) ∈ fset xs. hd bs = (root t1,e1)⟧
    ⟹ ∃(t1,e1) ∈ fset xs. hd (Sorting_Algorithms.merge cmp as bs) = (root t1,e1)"
  by(induction as bs rule: Sorting_Algorithms.merge.induct) auto

lemma merge_split_supset:
  assumes "as@r#bs = (Sorting_Algorithms.merge cmp xs ys)"
    shows "∃bs' as'. set bs' ⊆ set bs ∧ (as'@r#bs' = xs ∨ as'@r#bs' = ys)"
using assms proof(induction xs ys arbitrary: as taking: cmp rule: Sorting_Algorithms.merge.induct)
  case (3 x xs y ys)
  let ?merge = "Sorting_Algorithms.merge cmp"
  show ?case
  proof(cases "compare cmp x y = Greater")
    case True
    then show ?thesis
    proof(cases as)
      case Nil
      have "set ys ⊆ set (?merge (x#xs) ys)" using set_merge by fast
      then show ?thesis using Nil True "3.prems" by auto
    next
      case (Cons c cs)
      then have "cs@r#bs = ?merge (x#xs) ys" using True "3.prems" by simp
      then obtain as' bs' where as_def: "set bs' ⊆ set bs" "as'@r#bs' = x#xs ∨ as'@r#bs' = ys"
        using "3.IH"(1)[OF True] by blast
      have "as'@r#bs' = x#xs ∨ (y#as')@r#bs' = y#ys" using as_def(2) by simp
      then show ?thesis using as_def(1) by blast
    qed
  next
    case False
    then show ?thesis
    proof(cases as)
      case Nil
      have "set xs ⊆ set (?merge xs (y#ys))" using set_merge by fast
      then show ?thesis using Nil False "3.prems" by auto
    next
      case (Cons c cs)
      then have "cs@r#bs = ?merge xs (y#ys)" using False "3.prems" by simp
      then obtain as' bs' where as_def: "set bs' ⊆ set bs" "as'@r#bs' = xs ∨ as'@r#bs' = y#ys"
        using "3.IH"(2)[OF False] by blast
      have "(x#as')@r#bs' = x#xs ∨ as'@r#bs' = y#ys" using as_def(2) by simp
      then show ?thesis using as_def(1) by blast
    qed
  qed
qed(auto)

lemma merge_split_supset_fst:
  assumes "as@(r,e)#bs = (Sorting_Algorithms.merge cmp xs ys)"
  shows "∃as' bs'. set bs' ⊆ set bs ∧ (as'@(r,e)#bs' = xs ∨ as'@(r,e)#bs' = ys)"
  using merge_split_supset[OF assms] by blast

lemma merge_split_supset':
  assumes "r ∈ set (Sorting_Algorithms.merge cmp xs ys)"
  shows "∃as bs as' bs'. as@r#bs = (Sorting_Algorithms.merge cmp xs ys)
          ∧ set bs' ⊆ set bs ∧ (as'@r#bs' = xs ∨ as'@r#bs' = ys)"
  using merge_split_supset split_list[OF assms] by metis

lemma merge_split_supset_fst':
  assumes "r ∈ fst ` set (Sorting_Algorithms.merge cmp xs ys)"
  shows "∃as e bs as' bs'. as@(r,e)#bs = (Sorting_Algorithms.merge cmp xs ys)
        ∧ set bs' ⊆ set bs ∧ (as'@(r,e)#bs' = xs ∨ as'@(r,e)#bs' = ys)"
proof -
  obtain e where "(r,e) ∈ set (Sorting_Algorithms.merge cmp xs ys)" using assms by auto
  then show ?thesis using merge_split_supset'[of "(r,e)"] by blast
qed

lemma merge_split_supset_subtree:
  assumes "∀as bs. as@(r,e)#bs = xs ⟶
            (∃zs. is_subtree (Node r zs) t ∧ dverts (Node r zs) ⊆ fst ` set ((r,e)#bs))"
      and "∀as bs. as@(r,e)#bs = ys ⟶
            (∃zs. is_subtree (Node r zs) t ∧ dverts (Node r zs) ⊆ fst ` set ((r,e)#bs))"
      and "as@(r,e)#bs = (Sorting_Algorithms.merge cmp xs ys)"
    shows "∃zs. is_subtree (Node r zs) t ∧ dverts (Node r zs) ⊆ (fst ` set ((r,e)#bs))"
proof -
  obtain as' bs' where bs'_def: "set bs' ⊆ set bs" "as'@(r,e)#bs' = xs ∨ as'@(r,e)#bs' = ys"
    using merge_split_supset[OF assms(3)] by blast
  obtain zs where zs_def: "is_subtree (Node r zs) t" "dverts (Node r zs) ⊆ fst ` set ((r,e)#bs')"
    using assms(1,2) bs'_def(2) by blast
  then have "dverts (Node r zs) ⊆ fst ` set ((r,e)#bs)" using bs'_def(1) by auto
  then show ?thesis using zs_def(1) by blast
qed

lemma merge_split_supset_strict_subtree:
  assumes "∀as bs. as@(r,e)#bs = xs ⟶ (∃zs. strict_subtree (Node r zs) t
            ∧ dverts (Node r zs) ⊆ fst ` set ((r,e)#bs))"
      and "∀as bs. as@(r,e)#bs = ys ⟶ (∃zs. strict_subtree (Node r zs) t
            ∧ dverts (Node r zs) ⊆ fst ` set ((r,e)#bs))"
      and "as@(r,e)#bs = (Sorting_Algorithms.merge cmp xs ys)"
    shows "∃zs. strict_subtree (Node r zs) t
            ∧ dverts (Node r zs) ⊆ (fst ` set ((r,e)#bs))"
proof -
  obtain as' bs' where bs'_def: "set bs' ⊆ set bs" "as'@(r,e)#bs' = xs ∨ as'@(r,e)#bs' = ys"
    using merge_split_supset[OF assms(3)] by blast
  obtain zs where zs_def:
      "strict_subtree (Node r zs) t" "dverts (Node r zs) ⊆ fst ` set ((r,e)#bs')"
    using assms(1,2) bs'_def(2) by blast
  then have "dverts (Node r zs) ⊆ fst ` set ((r,e)#bs)" using bs'_def(1) by auto
  then show ?thesis using zs_def(1,2) by blast
qed

lemma sorted_app_l: "sorted cmp (xs@ys) ⟹ sorted cmp xs"
  by(induction xs rule: sorted.induct) auto

lemma sorted_app_r: "sorted cmp (xs@ys) ⟹ sorted cmp ys"
  by(induction xs) (auto simp: sorted_Cons_imp_sorted)

subsection ‹Merging Subtrees of Ranked Dtrees›

locale ranked_dtree = list_dtree t for t :: "('a list,'b) dtree" +
  fixes rank :: "'a list ⇒ real"
  fixes cmp :: "('a list×'b) comparator"
  assumes cmp_antisym:
    "⟦v1 ≠ []; v2 ≠ []; compare cmp (v1,e1) (v2,e2) = Equiv⟧ ⟹ set v1 ∩ set v2 ≠ {} ∨ e1=e2"
begin

lemma ranked_dtree_rec: "⟦Node r xs = t; (x,e) ∈ fset xs⟧ ⟹ ranked_dtree x cmp"
  using wf_arcs wf_lverts by(unfold_locales) (auto dest: cmp_antisym)

lemma ranked_dtree_rec_suc: "(x,e) ∈ fset (sucs t) ⟹ ranked_dtree x cmp"
  using ranked_dtree_rec[of "root t"] by force

lemma ranked_dtree_subtree: "is_subtree x t ⟹ ranked_dtree x cmp"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret ranked_dtree "Node r xs" by blast
  show ?case using Node ranked_dtree_rec by (cases "x = Node r xs") auto
qed

subsubsection ‹Definitions›

lift_definition cmp' :: "('a list×'b) comparator" is
  "(λx y. if rank (rev (fst x)) < rank (rev (fst y)) then Less
    else if rank (rev (fst x)) > rank (rev (fst y)) then Greater
    else compare cmp x y)"
  by (smt (z3) comp.distinct(3) compare.less_iff_sym_greater compare.refl compare.trans_equiv
      compare.trans_less comparator_def)

abbreviation disjoint_sets :: "(('a list, 'b) dtree × 'b) fset ⇒ bool" where
  "disjoint_sets xs ≡ disjoint_darcs xs ∧ disjoint_dlverts xs ∧ (∀(t,e) ∈ fset xs. [] ∉ dverts t)"

abbreviation merge_f :: "'a list ⇒ (('a list, 'b) dtree × 'b) fset
        ⇒ ('a list, 'b) dtree × 'b ⇒ ('a list × 'b) list ⇒ ('a list × 'b) list" where
  "merge_f r xs ≡ λ(t,e) b. if (t,e) ∈ fset xs ∧ list_dtree (Node r xs)
        ∧ (∀(v,e') ∈ set b. set v ∩ dlverts t = {} ∧ v ≠ [] ∧ e' ∉ darcs t ∪ {e})
      then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t,e)|})) b else b"

definition merge :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "merge t1 ≡ dtree_from_list (root t1) (ffold (merge_f (root t1) (sucs t1)) [] (sucs t1))"

subsubsection ‹Commutativity Proofs›

lemma cmp_sets_not_dsjnt_if_equiv:
  "⟦v1 ≠ []; v2 ≠ []⟧ ⟹ compare cmp' (v1,e1) (v2,e2) = Equiv ⟹ set v1 ∩ set v2 ≠ {} ∨ e1=e2"
  by(auto simp: cmp'.rep_eq dest: cmp_antisym split: if_splits)

lemma dtree_to_list_x_in_dverts:
  "x ∈ fst ` set (dtree_to_list (Node r {|(t1,e1)|})) ⟹ x ∈ dverts t1"
  using dtree_to_list_sub_dverts_ins by auto

lemma dtree_to_list_x_in_dlverts:
  "x ∈ fst ` set (dtree_to_list (Node r {|(t1,e1)|})) ⟹ set x ⊆ dlverts t1"
  using dtree_to_list_x_in_dverts lverts_if_in_verts by fast

lemma dtree_to_list_x1_disjoint:
  "dlverts t1 ∩ dlverts t2 = {}
    ⟹ ∀x1 ∈ fst ` set (dtree_to_list (Node r {|(t1,e1)|})). set x1 ∩ dlverts t2 = {}"
  using dtree_to_list_x_in_dlverts by fast

lemma dtree_to_list_xs_disjoint:
  "dlverts t1 ∩ dlverts t2 = {}
    ⟹ ∀x1 ∈ fst ` set (dtree_to_list (Node r {|(t1,e1)|})).
          ∀x2 ∈ fst ` set (dtree_to_list (Node r' {|(t2,e2)|})). set x1 ∩ set x2 = {}"
  using dtree_to_list_x_in_dlverts by (metis inf_mono subset_empty)

lemma dtree_to_list_e_in_darcs:
  "e ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})) ⟹ e ∈ darcs t1 ∪ {e1}"
  using dtree_to_list_sub_darcs by fastforce

lemma dtree_to_list_e_disjoint:
  "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}
    ⟹ ∀e ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})). e ∉ darcs t2 ∪ {e2}"
  using dtree_to_list_e_in_darcs by fast

lemma dtree_to_list_es_disjoint:
  "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}
    ⟹ ∀e3 ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})).
          ∀e4 ∈ snd ` set (dtree_to_list (Node r' {|(t2,e2)|})). e3 ≠ e4"
  using dtree_to_list_e_disjoint dtree_to_list_e_in_darcs by fast

lemma dtree_to_list_xs_not_equiv:
  assumes "dlverts t1 ∩ dlverts t2 = {}"
      and "(darcs t1 ∪ {e3}) ∩ (darcs t2 ∪ {e4}) = {}"
      and "(x1,e1) ∈ set (dtree_to_list (Node r {|(t1,e3)|}))" and "x1 ≠ []"
      and "(x2,e2) ∈ set (dtree_to_list (Node r' {|(t2,e4)|}))" and "x2 ≠ []"
    shows "compare cmp' (x1,e1) (x2,e2) ≠ Equiv"
  using dtree_to_list_xs_disjoint[OF assms(1)] cmp_sets_not_dsjnt_if_equiv[of x1 x2 e1 e2]
    dtree_to_list_es_disjoint[OF assms(2)] assms(3-6) by fastforce

lemma merge_dtree1_not_equiv:
  assumes "dlverts t1 ∩ dlverts t2 = {}"
      and "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}"
      and "[] ∉ dverts t1"
      and "[] ∉ dverts t2"
      and "xs = dtree_to_list (Node r {|(t1,e1)|})"
      and "ys = dtree_to_list (Node r' {|(t2,e2)|})"
    shows "∀(x1,e1)∈set xs. ∀(x2,e2)∈set ys. compare cmp' (x1,e1) (x2,e2) ≠ Equiv"
proof -
  have "∀(x1,e1)∈set xs. x1 ≠ []"
    using assms(3,5) dtree_to_list_x_in_dverts
    by (smt (verit) case_prod_conv case_prod_eta fst_conv pair_imageI surj_pair)
  moreover have "∀(x1,e1)∈set ys. x1 ≠ []"
    using assms(4,6) dtree_to_list_x_in_dverts
    by (smt (verit) case_prod_conv case_prod_eta fst_conv pair_imageI surj_pair)
  ultimately show ?thesis using dtree_to_list_xs_not_equiv[of t1 t2] assms(1,2,5,6) by fast
qed

lemma merge_commute_aux1:
  assumes "dlverts t1 ∩ dlverts t2 = {}"
      and "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}"
      and "[] ∉ dverts t1"
      and "[] ∉ dverts t2"
      and "xs = dtree_to_list (Node r {|(t1,e1)|})"
      and "ys = dtree_to_list (Node r' {|(t2,e2)|})"
    shows "Sorting_Algorithms.merge cmp' xs ys = Sorting_Algorithms.merge cmp' ys xs"
  using merge_dtree1_not_equiv merge_comm_if_not_equiv assms by fast

lemma dtree_to_list_x1_list_disjoint:
  "set x2 ∩ dlverts t1 = {}
    ⟹ ∀x1 ∈ fst ` set (dtree_to_list (Node r {|(t1,e1)|})). set x1 ∩ set x2 = {}"
  using dtree_to_list_x_in_dlverts by fast

lemma dtree_to_list_e1_list_disjoint':
  "set x2 ∩ darcs t1 ∪ {e1} = {}
    ⟹ ∀x1 ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})). x1 ∉ set x2"
  using dtree_to_list_e_in_darcs by blast

lemma dtree_to_list_e1_list_disjoint:
  "e2 ∉ darcs t1 ∪ {e1}
    ⟹ ∀x1 ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})). x1 ≠ e2"
  using dtree_to_list_e_in_darcs by fast

lemma dtree_to_list_xs_list_not_equiv:
  assumes "(x1,e1) ∈ set (dtree_to_list (Node r {|(t1,e3)|}))"
      and "x1 ≠ []"
      and "∀(v,e) ∈ set ys. set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e3}"
      and "(x2,e2) ∈ set ys"
    shows "compare cmp' (x1,e1) (x2,e2) ≠ Equiv"
proof -
  have "set x1 ∩ set x2 = {}" using dtree_to_list_x1_list_disjoint assms(1,3,4) by fastforce
  moreover have "e1 ≠ e2" using dtree_to_list_e1_list_disjoint assms(1,3,4) by fastforce
  ultimately show ?thesis using cmp_sets_not_dsjnt_if_equiv assms(2-4) by auto
qed

lemma merge_commute_aux2:
  assumes "[] ∉ dverts t1"
      and "xs = dtree_to_list (Node r {|(t1,e1)|})"
      and "∀(v,e) ∈ set ys. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1}"
    shows "Sorting_Algorithms.merge cmp' xs ys = Sorting_Algorithms.merge cmp' ys xs"
proof -
  have "∀(x1,e1)∈set xs. x1 ≠ []"
    using assms(1,2) dtree_to_list_x_in_dverts
    by (smt (verit) case_prod_conv case_prod_eta fst_conv pair_imageI surj_pair)
  then have "∀(x1,e1)∈set xs. ∀(x2,e2)∈set ys. compare cmp' (x1,e1) (x2,e2) ≠ Equiv"
    using assms(2,3) dtree_to_list_xs_list_not_equiv by force
  then show ?thesis using merge_comm_if_not_equiv by fast
qed

lemma merge_inter_preserv':
  assumes "f = (merge_f r xs)"
      and "¬(∀(v,_) ∈ set z. set v ∩ dlverts t1 = {})"
    shows "¬(∀(v,_) ∈ set (f (t2,e2) z). set v ∩ dlverts t1 = {})"
proof(cases "f (t2,e2) z = z")
  case False
  then have "f (t2,e2) z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) z"
    by(simp add: assms(1)) meson
  then show ?thesis using assms(2) set_merge by force
qed (simp add: assms(2))

lemma merge_inter_preserv:
  assumes "f = (merge_f r xs)"
      and "¬(∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ e ∉ darcs t1 ∪ {e1})"
    shows "¬(∀(v,e) ∈ set (f (t2,e2) z). set v ∩ dlverts t1 = {} ∧ e ∉ darcs t1 ∪ {e1})"
proof(cases "f (t2,e2) z = z")
  case True
  then show ?thesis using assms(2) by simp
next
  case False
  then have "f (t2,e2) z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) z"
    by(simp add: assms(1)) meson
  then show ?thesis
    using assms(2) set_merge[of "dtree_to_list (Node r {|(t2,e2)|})"] by simp blast
qed

lemma merge_f_eq_z_if_inter':
  "¬(∀(v,_) ∈ set z. set v ∩ dlverts t1 = {}) ⟹ (merge_f r xs) (t1,e1) z = z"
  by auto

lemma merge_f_eq_z_if_inter:
  "¬(∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ e ∉ darcs t1 ∪ {e1})
    ⟹ (merge_f r xs) (t1,e1) z = z"
  by auto

lemma merge_empty_inter_preserv_aux:
  assumes "f = (merge_f r xs)"
      and "(t2,e2) ∈ fset xs"
      and "∀(v,e) ∈ set z. set v ∩ dlverts t2 = {} ∧ v≠[] ∧ e ∉ darcs t2 ∪ {e2}"
      and "list_dtree (Node r xs)"
      and "(t1,e1) ∈ fset xs"
      and "(t1,e1) ≠ (t2,e2)"
      and "∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1}"
    shows "∀(v,e) ∈ set (f (t2,e2) z). set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1}"
proof -
  have 0: "f (t2,e2) z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) z"
    using assms(1-6) by simp
  let ?ys = "dtree_to_list (Node r {|(t2,e2)|})"
  interpret list_dtree "Node r xs" using assms(4) .
  have "disjoint_dlverts xs" using wf_lverts by simp
  then have "∀v∈fst ` set ?ys. set v ∩ dlverts t1 = {}"
    using dtree_to_list_x1_disjoint assms(2,5,6) by fast
  then have 1: "∀v∈fst ` set (Sorting_Algorithms.merge cmp' ?ys z). set v ∩ dlverts t1 = {}"
    using assms(7) set_merge[of ?ys] by fastforce
  have "disjoint_darcs xs" using disjoint_darcs_if_wf_xs[OF wf_arcs] .
  then have 2: "(darcs t2 ∪ {e2}) ∩ (darcs t1 ∪ {e1}) = {}" using assms(2,5,6) by fast
  have "∀e∈snd ` set ?ys. e ∉ darcs t1 ∪ {e1}" using dtree_to_list_e_disjoint[OF 2] by blast
  then have 2: "∀e∈snd ` set (Sorting_Algorithms.merge cmp' ?ys z). e ∉ darcs t1 ∪ {e1}"
    using assms(7) set_merge[of ?ys] by fastforce
  have "[] ∉ dverts t2" using assms(2) empty_notin_wf_dlverts wf_lverts by fastforce
  then have "∀v∈fst ` set ?ys. v ≠ []" by (metis dtree_to_list_x_in_dverts)
  then have "∀v∈fst ` set (Sorting_Algorithms.merge cmp' ?ys z). v ≠ []"
    using assms(7) set_merge[of ?ys] by fastforce
  then show ?thesis using 0 1 2 by fastforce
qed

lemma merge_empty_inter_preserv:
  assumes "f = (merge_f r xs)"
      and "∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1}"
      and "(t1,e1) ∈ fset xs"
      and "(t1,e1) ≠ (t2,e2)"
    shows "∀(v,e) ∈ set (f (t2,e2) z). set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1}"
proof(cases "f (t2,e2) z = z")
  case True
  then show ?thesis using assms(2) by simp
next
  case False
  have "(t2,e2) ∈ fset xs" using False assms(1) by simp argo
  moreover have "list_dtree (Node r xs)" using False assms(1) by simp argo
  moreover have "∀(v,e) ∈ set z. set v ∩ dlverts t2 = {} ∧ v≠[] ∧ e ∉ darcs t2 ∪ {e2}"
    using False assms(1) by simp argo
  ultimately show ?thesis using merge_empty_inter_preserv_aux assms by presburger
qed

lemma merge_commute_aux3:
  assumes "f = (merge_f r xs)"
      and "list_dtree (Node r xs)"
      and "(t1,e1) ≠ (t2,e2)"
      and "(∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
      and "(∀(v,e) ∈ set z. set v ∩ dlverts t2 = {} ∧ v ≠ [] ∧ e ∉ darcs t2 ∪ {e2})"
      and "(t1,e1) ∈ fset xs"
      and "(t2,e2) ∈ fset xs"
    shows "(f (t2, e2) ∘ f (t1, e1)) z = (f (t1, e1) ∘ f (t2, e2)) z"
proof -
  let ?merge = "Sorting_Algorithms.merge"
  let ?xs = "dtree_to_list (Node r {|(t1, e1)|})"
  let ?ys = "dtree_to_list (Node r {|(t2, e2)|})"
  interpret list_dtree "Node r xs" using assms(2) .
  have disj: "dlverts t1 ∩ dlverts t2 = {}" "[] ∉ dverts t1" "[] ∉ dverts t2"
    using assms(3,6,7) disjoint_dlverts_if_wf[OF wf_lverts] empty_notin_wf_dlverts[OF wf_lverts]
    by fastforce+
  have disj2: "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}"
    using assms(2,3,6,7) disjoint_darcs_if_wf_aux5[OF wf_arcs] by blast
  have "f (t2, e2) z = Sorting_Algorithms.merge cmp' ?ys z" using assms(1,2,5,7) by simp
  moreover have "∀(v,e)∈set (f (t2,e2) z). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1}"
    using merge_empty_inter_preserv[OF assms(1)] assms(3,4,6) by simp
  ultimately have 2: "(f (t1, e1) ∘ f (t2, e2)) z = ?merge cmp' ?xs (?merge cmp' ?ys z)"
    using assms(1-2,6) by auto
  have "f (t1, e1) z = Sorting_Algorithms.merge cmp' ?xs z" using assms(1-2,4,6) by simp
  moreover have "∀(v,e)∈set (f (t1, e1) z). set v ∩ dlverts t2 = {} ∧ v≠[] ∧ e ∉ darcs t2 ∪ {e2}"
    using merge_empty_inter_preserv[OF assms(1)] assms(3,5,7) by presburger
  ultimately have 3: "(f (t2, e2) ∘ f (t1,e1)) z = ?merge cmp' ?ys (?merge cmp' ?xs z)"
    using assms(1-2,7) by simp
  have "∀x∈set ?xs. ∀y∈set ?ys. compare cmp' x y ≠ Equiv"
    using merge_dtree1_not_equiv[OF disj(1) disj2] disj(2,3) by fast
  then have "?merge cmp' ?xs (?merge cmp' ?ys z) = ?merge cmp' ?ys (?merge cmp' ?xs z)"
    using merge_comp_commute by blast
  then show ?thesis using 2 3 by simp
qed

lemma merge_commute_aux:
  assumes "f = (merge_f r xs)"
  shows "(f y ∘ f x) z = (f x ∘ f y) z"
proof -
  obtain t1 e1 where y_def[simp]: "x = (t1, e1)" by fastforce
  obtain t2 e2 where x_def[simp]: "y = (t2, e2)" by fastforce
  show ?thesis
  proof(cases "(t1,e1) ∈ fset xs ∧ (t2,e2) ∈ fset xs")
    case True
    then consider "list_dtree (Node r xs)" "(t1,e1) ≠ (t2,e2)"
        "(∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
        "(∀(v,e) ∈ set z. set v ∩ dlverts t2 = {} ∧ v ≠ [] ∧ e ∉ darcs t2 ∪ {e2})"
      | "(t1,e1) = (t2,e2)"
      | "¬list_dtree (Node r xs)"
      | "¬(∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ e ∉ darcs t1 ∪ {e1})"
      | "¬(∀(v,e) ∈ set z. set v ∩ dlverts t2 = {} ∧ e ∉ darcs t2 ∪ {e2})"
      | "¬(∀(v,_) ∈ set z. v ≠ [])"
      by fast
    then show ?thesis
    proof(cases)
      case 1
      then show ?thesis using merge_commute_aux3[OF assms] True by simp
    next
      case 4
      then have "f x z = z" by(auto simp: assms)
      then have 0: "(f y ∘ f x) z = f y z" by simp
      have "¬(∀(v,e) ∈ set (f y z). set v ∩ dlverts t1 = {} ∧ e ∉ darcs t1 ∪ {e1})"
        using merge_inter_preserv[OF assms 4] by simp
      then have "(f x ∘ f y) z = f y z" using assms merge_f_eq_z_if_inter by auto
      then show ?thesis using 0 by simp
    next
      case 5
      then have "f y z = z" by(auto simp: assms)
      then have 0: "(f x ∘ f y) z = f x z" by simp
      have "¬(∀(v,e) ∈ set (f x z). set v ∩ dlverts t2 = {} ∧ e ∉ darcs t2 ∪ {e2})"
        using merge_inter_preserv[OF assms 5] by simp
      then have "(f y ∘ f x) z = f x z" using assms merge_f_eq_z_if_inter by simp
      then show ?thesis using 0 by simp
    next
      case 6
      then have "(f x ∘ f y) z = z" by(auto simp: assms)
      also have "z = (f y ∘ f x) z" using 6 by(auto simp: assms)
      finally show ?thesis by simp
    qed(auto simp: assms)
  next
    case False
    then have "(∀z. f x z = z) ∨ (∀z. f y z = z)" by(auto simp: assms)
    then show ?thesis by force
  qed
qed

lemma merge_commute: "comp_fun_commute (merge_f r xs)"
  using comp_fun_commute_def merge_commute_aux by blast

interpretation Comm: comp_fun_commute "merge_f r xs" by (rule merge_commute)

subsubsection ‹Merging Preserves Arcs and Verts›

lemma empty_list_valid_merge:
  "(∀(v,e) ∈ set []. set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
  by simp

lemma disjoint_sets_sucs: "disjoint_sets (sucs t)"
  using empty_notin_wf_dlverts list_dtree.wf_lverts list_dtree_rec dtree.collapse
    disjoint_dlverts_if_wf[OF wf_lverts] disjoint_darcs_if_wf[OF wf_arcs] by blast

lemma empty_not_elem_subset:
  "⟦xs |⊆| ys; ∀(t,e) ∈ fset ys. [] ∉ dverts t⟧ ⟹ ∀(t,e) ∈ fset xs. [] ∉ dverts t"
  by (meson less_eq_fset.rep_eq subset_iff)

lemma disjoint_sets_subset:
  assumes "xs |⊆| ys" and "disjoint_sets ys"
  shows " disjoint_sets xs"
  using disjoint_darcs_subset[OF assms(1)] disjoint_dlverts_subset[OF assms(1)]
    empty_not_elem_subset[OF assms(1)] assms by fast

lemma merge_mdeg_le_1: "max_deg (merge t1) ≤ 1"
  unfolding merge_def by (rule dtree_from_list_deg_le_1)

lemma merge_mdeg_le1_sub: "is_subtree t1 (merge t2) ⟹ max_deg t1 ≤ 1"
  using merge_mdeg_le_1 le_trans mdeg_ge_sub by fast

lemma merge_fcard_le1: "fcard (sucs (merge t1)) ≤ 1"
  unfolding merge_def by (rule dtree_from_list_fcard_le1)

lemma merge_fcard_le1_sub: "is_subtree t1 (merge t2) ⟹ fcard (sucs t1) ≤ 1"
  using merge_mdeg_le1_sub mdeg_ge_fcard[of "sucs t1" "root t1"] by force

lemma merge_f_alt:
  assumes "P = (λxs. list_dtree (Node r xs))"
      and "Q = (λ(t,e) b. (∀(v,e') ∈ set b. set v ∩ dlverts t = {} ∧ v≠[] ∧ e' ∉ darcs t ∪ {e}))"
      and "R = (λ(t,e) b. Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t,e)|})) b)"
    shows "merge_f r xs = (λa b. if a ∉ fset xs ∨ ¬ Q a b ∨ ¬ P xs then b else R a b)"
  using assms by force

lemma merge_f_alt_commute:
  assumes "P = (λxs. list_dtree (Node r xs))"
      and "Q = (λ(t,e) b. (∀(v,e') ∈ set b. set v ∩ dlverts t = {} ∧ v ≠ [] ∧ e' ∉ darcs t ∪ {e}))"
      and "R = (λ(t,e) b. Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t,e)|})) b)"
    shows "comp_fun_commute (λa b. if a ∉ fset xs ∨ ¬ Q a b ∨ ¬ P xs then b else R a b)"
proof -
  have "comp_fun_commute (merge_f r xs)" using merge_commute by fast
  then show ?thesis using merge_f_alt[OF assms] by simp
qed

lemma merge_ffold_supset:
  assumes "xs |⊆| ys" and "list_dtree (Node r ys)"
  shows "ffold (merge_f r ys) acc xs = ffold (merge_f r xs) acc xs"
proof -
  let ?P = "λxs. list_dtree (Node r xs)"
  let ?Q = "λ(t,e) b. (∀(v,e') ∈ set b. set v ∩ dlverts t = {} ∧ v ≠ [] ∧ e' ∉ darcs t ∪ {e})"
  let ?R = "λ(t,e) b. Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t,e)|})) b"
  have 0: "⋀xs. comp_fun_commute (λa b. if a ∉ fset xs ∨ ¬ ?Q a b ∨ ¬ ?P xs then b else ?R a b)"
    using merge_f_alt_commute by blast
  have "ffold (λa b. if a ∉ fset ys ∨ ¬ ?Q a b ∨ ¬ ?P ys then b else ?R a b) acc xs
      = ffold (λa b. if a ∉ fset xs ∨ ¬ ?Q a b ∨ ¬ ?P xs then b else ?R a b) acc xs"
    using ffold_commute_supset[OF assms(1), of ?P ?Q ?R, OF assms(2) list_dtree_subset 0] by auto
  then show ?thesis using merge_f_alt by presburger
qed

lemma merge_f_merge_if_not_snd:
  "merge_f r xs (t1,e1) z ≠ z ⟹
  merge_f r xs (t1,e1) z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t1,e1)|})) z"
  by(simp) meson

lemma merge_f_merge_if_conds:
  "⟦list_dtree (Node r xs); ∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1};
     (t1,e1) ∈ fset xs⟧
  ⟹ merge_f r xs (t1,e1) z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t1,e1)|})) z"
  by force

lemma merge_f_merge_if_conds_empty:
  "⟦list_dtree (Node r xs); (t1,e1) ∈ fset xs⟧
  ⟹ merge_f r xs (t1,e1) []
      = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t1,e1)|})) []"
  using merge_f_merge_if_conds by simp

lemma merge_ffold_empty_inter_preserv:
  "⟦list_dtree (Node r ys); xs |⊆| ys;
    ∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1};
    (t1,e1) ∈ fset ys; (t1,e1) ∉ fset xs; (v,e) ∈ set (ffold (merge_f r xs) z xs)⟧
      ⟹ set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1}"
proof(induction xs)
  case (insert x xs)
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge"
  interpret list_dtree "Node r ys" using insert.prems(1) .
  have 0: "list_dtree (Node r (finsert x xs))" using list_dtree_subset insert.prems(1,2) by blast
  show ?case
  proof(cases "ffold ?f z (finsert x xs) = ffold ?f' z xs")
    case True
    then have "(v,e) ∈ set (ffold ?f' z xs)" using insert.prems(6) by argo
    then show ?thesis using insert.IH insert.prems by force
  next
    case not_right: False
    obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
    show ?thesis
    proof(cases "(v,e) ∈ set (dtree_to_list (Node r {|(t2,e2)|}))")
      case True
      have uneq: "(t2,e2) ≠ (t1,e1)" using insert.prems(5) t2_def by fastforce
      moreover have 1: "(t2,e2) ∈ fset ys" using insert.prems(2) by fastforce
      ultimately have "dlverts t1 ∩ dlverts t2 = {}" using insert.prems(4) wf_lverts by fastforce
      then have 2: "∀x1∈fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 ∩ dlverts t1 = {}"
        using dtree_to_list_x1_disjoint by fast
      have "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}"
        using insert.prems(4) uneq 1 disjoint_darcs_if_wf_aux5 wf_arcs by fast
      then have 3: "∀e∈snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e ∉ darcs t1 ∪ {e1}"
        using dtree_to_list_e_disjoint by fast
      have "[] ∉ dverts t2" using 1 wf_lverts empty_notin_wf_dlverts by auto
      then have "∀x1∈fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 ≠ []"
        using 1 dtree_to_list_x_in_dverts by metis
      then show ?thesis using True 2 3 by fastforce
    next
      case False
      have "xs |⊆| finsert x xs" by blast
      then have f_xs: "ffold ?f z xs = ffold ?f' z xs"
        using merge_ffold_supset 0 by presburger
      have "ffold ?f z (finsert x xs) = ?f x (ffold ?f z xs)"
        using Comm.ffold_finsert[OF insert.hyps] by blast
      then have 0: "ffold ?f z (finsert x xs) = ?f x (ffold ?f' z xs)" using f_xs by argo
      then have "?f x (ffold ?f' z xs) ≠ ffold ?f' z xs" using not_right by argo
      then have "?f (t2,e2) (ffold ?f' z xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using merge_f_merge_if_not_snd t2_def by blast
      then have "ffold ?f z (finsert x xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using 0 t2_def by argo
      then have "(v,e) ∈ set (?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs))"
        using insert.prems(6) by argo
      then have "(v,e) ∈ set (ffold ?f' z xs)" using set_merge False by fast
      then show ?thesis using insert.IH insert.prems by force
    qed
  qed
qed (auto simp: ffold.rep_eq)

lemma merge_ffold_empty_inter_preserv':
  "⟦list_dtree (Node r (finsert x xs));
    ∀(v,e) ∈ set z. set v ∩ dlverts t1 = {} ∧ v≠[] ∧ e ∉ darcs t1 ∪ {e1};
    (t1,e1) ∈ fset (finsert x xs); (t1,e1) ∉ fset xs; (v,e) ∈ set (ffold (merge_f r xs) z xs)⟧
    ⟹ set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1}"
  using merge_ffold_empty_inter_preserv[of r "finsert x xs" xs z t1 e1 v e] by fast

lemma merge_ffold_set_sub_union:
  "list_dtree (Node r xs)
    ⟹ set (ffold (merge_f r xs) [] xs) ⊆ (⋃x∈fset xs. set (dtree_to_list (Node r {|x|})))"
proof(induction xs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems empty_list_valid_merge] by blast
  have 0: "list_dtree (Node r xs)" using list_dtree_subset insert.prems by blast
  have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] by blast
  also have "… = ?f x (ffold ?f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems by fastforce
  finally have "ffold ?f [] (finsert x xs)
              = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
    using merge_f_merge_if_conds[OF insert.prems xs_val] by simp
  then have "set (ffold ?f [] (finsert x xs))
        = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs))"
    by argo
  then have "set (ffold ?f [] (finsert x xs))
        = (set (dtree_to_list (Node r {|x|})) ∪ set (ffold ?f' [] xs))" using set_merge by fast
  then show ?case using 0 insert.IH insert.prems by auto
qed (simp add: ffold.rep_eq)

lemma merge_ffold_nempty:
  "⟦list_dtree (Node r xs); xs ≠ {||}⟧ ⟹ ffold (merge_f r xs) [] xs ≠ []"
proof(induction xs)
  case (insert x xs)
  define f where "f = merge_f r (finsert x xs)"
  define f' where "f' = merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge cmp'"
  have 0: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(1) by blast
  obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
  have "(t2, e2) ∈ fset (finsert x xs)" by simp
  moreover have "(t2, e2) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold f' [] xs). set v ∩ dlverts t2 = {} ∧ v ≠ [] ∧ e ∉ darcs t2 ∪ {e2})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge] f'_def
    by blast
  have "ffold f [] (finsert x xs) = f x (ffold f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] f_def by blast
  also have "… = f x (ffold f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1) f_def f'_def by fastforce
  finally have "ffold f [] (finsert x xs) = ?merge (dtree_to_list (Node r {|x|})) (ffold f' [] xs)"
    using xs_val insert.prems f_def by simp
  then have merge: "ffold f [] (finsert x xs)
              = ?merge (dtree_to_list (Node r {|(t2,e2)|})) (ffold f'[] xs)"
    using t2_def by blast
  then show ?case
    using input_empty_if_merge_empty[of cmp' "dtree_to_list (Node r {|(t2,e2)|})"] f_def by auto
qed(simp)

lemma merge_f_ndisjoint_sets_aux:
  "¬disjoint_sets xs
    ⟹ ¬((t,e) ∈ fset xs ∧ disjoint_sets xs ∧ (∀(v,_) ∈ set b. set v ∩ dlverts t = {} ∧ v ≠ []))"
  by blast

lemma merge_f_not_list_dtree: "¬list_dtree (Node r xs) ⟹ (merge_f r xs) a b = b"
  using merge_f_alt by simp

lemma merge_ffold_empty_if_nwf: "¬list_dtree (Node r ys) ⟹ ffold (merge_f r ys) [] xs = []"
proof(induction xs)
  case (insert x xs)
  define f where "f = merge_f r ys"
  let ?f = "merge_f r ys"
  let ?merge = "Sorting_Algorithms.merge cmp'"
  obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
  have "ffold f [] (finsert x xs) = ?f x (ffold f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] f_def by blast
  then have "ffold f [] (finsert x xs) = ffold f [] xs"
    using insert.prems merge_f_not_list_dtree by force
  then show ?case using insert f_def by argo
qed (simp add: ffold.rep_eq)

lemma merge_empty_if_nwf: "¬list_dtree (Node r xs) ⟹ merge (Node r xs) = Node r {||}"
  unfolding merge_def using merge_ffold_empty_if_nwf by simp

lemma merge_empty_if_nwf_sucs: "¬list_dtree t1 ⟹ merge t1 = Node (root t1) {||}"
  using merge_empty_if_nwf[of "root t1" "sucs t1"] by simp

lemma merge_empty: "merge (Node r {||}) = Node r {||}"
proof -
  have "comp_fun_commute (λ(t, e) b. b)"
    by (simp add: comp_fun_commute_const cond_case_prod_eta)
  hence "dtree_from_list r (ffold (λ(t, e) b. b) [] {||}) = Node r {||}"
    using comp_fun_commute.ffold_empty
    by (smt (verit, best) dtree_from_list.simps(1))
  thus ?thesis
    unfolding merge_def by simp
qed

lemma merge_empty_sucs:
  assumes "sucs t1 = {||}"
  shows "merge t1 = Node (root t1) {||}"
proof -
  have "dtree_from_list (dtree.root t1) (ffold (λ(t, e) b. b) [] {||}) = Node (dtree.root t1) {||}"
    by (simp add: ffold.rep_eq)
  with assms show ?thesis
    unfolding merge_def by simp
qed

lemma merge_singleton_sucs:
  assumes "list_dtree (Node (root t1) (sucs t1))" and "sucs t1 ≠ {||}"
  shows "∃t e. merge t1 = Node (root t1) {|(t,e)|}"
  unfolding merge_def using merge_ffold_nempty[OF assms] dtree_from_list_singleton by fast

lemma merge_singleton:
  assumes "list_dtree (Node r xs)" and "xs ≠ {||}"
  shows "∃t e. merge (Node r xs) = Node r {|(t,e)|}"
  unfolding merge_def dtree.sel(1) using merge_ffold_nempty[OF assms] dtree_from_list_singleton
  by fastforce

lemma merge_cases: "∃t e. merge (Node r xs) = Node r {|(t,e)|} ∨ merge (Node r xs) = Node r {||}"
  using merge_singleton merge_empty_if_nwf merge_empty by blast

lemma merge_cases_sucs:
  "∃t e. merge t1 = Node (root t1) {|(t,e)|} ∨ merge t1 = Node (root t1) {||}"
  using merge_singleton_sucs[of t1] merge_empty_if_nwf_sucs merge_empty_sucs by auto

lemma merge_single_root:
  "(t2,e2) ∈ fset (sucs (merge (Node r xs))) ⟹ merge (Node r xs) = Node r {|(t2,e2)|}"
  using merge_cases[of r xs] by fastforce

lemma merge_single_root_sucs:
  "(t2,e2) ∈ fset (sucs (merge t1)) ⟹ merge t1 = Node (root t1) {|(t2,e2)|}"
  using merge_cases_sucs[of t1] by auto

lemma merge_single_root1:
  "t2 ∈ fst ` fset (sucs (merge (Node r xs))) ⟹ ∃e2. merge (Node r xs) = Node r {|(t2,e2)|}"
  using merge_single_root by fastforce

lemma merge_single_root1_sucs:
  "t2 ∈ fst ` fset (sucs (merge t1)) ⟹ ∃e2. merge t1 = Node (root t1) {|(t2,e2)|}"
  using merge_single_root_sucs by fastforce

lemma merge_nempty_sucs: "⟦list_dtree t1; sucs t1 ≠ {||}⟧ ⟹ sucs (merge t1) ≠ {||}"
  using merge_singleton_sucs by fastforce

lemma merge_nempty: "⟦list_dtree (Node r xs); xs ≠ {||}⟧ ⟹ sucs (merge (Node r xs)) ≠ {||}"
  using merge_singleton by fastforce

lemma merge_xs: "merge (Node r xs) = dtree_from_list r (ffold (merge_f r xs) [] xs)"
  unfolding merge_def dtree.sel(1) dtree.sel(2) by blast

lemma merge_root_eq[simp]: "root (merge t1) = root  t1"
  unfolding merge_def by simp

lemma merge_ffold_fsts_in_childverts:
  "⟦list_dtree (Node r xs); y ∈ fst ` set (ffold (merge_f r xs) [] xs)⟧
    ⟹ ∃t1 ∈ fst `  fset xs. y ∈ dverts t1"
proof(induction xs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge] by blast
  have 0: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(1) by blast
  then show ?case
  proof(cases "y ∈ fst ` set (ffold (merge_f r xs) [] xs)")
    case True
    then show ?thesis using insert.IH[OF 0] by simp
  next
    case False
    have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
      using Comm.ffold_finsert[OF insert.hyps] by blast
    also have "… = ?f x (ffold ?f' [] xs)"
      using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1) by fastforce
    finally have "ffold ?f [] (finsert x xs)
                = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
      using xs_val insert.prems by simp
    then have "set (ffold ?f [] (finsert x xs))
          = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs))"
      by argo
    then have "set (ffold ?f [] (finsert x xs))
          = (set (dtree_to_list (Node r {|x|})) ∪ set (ffold ?f' [] xs))"
      using set_merge by fast
    then have "y ∈ fst ` set (dtree_to_list (Node r {|x|}))" using False insert.prems by fast
    then show ?thesis by (simp add: dtree_to_list_x_in_dverts)
  qed
qed (simp add: ffold.rep_eq)

lemma verts_child_if_merge_child:
  assumes "t1 ∈ fst ` fset (sucs (merge t0))" and "x ∈ dverts t1"
  shows "∃t2 ∈ fst ` fset (sucs t0). x ∈ dverts t2"
proof -
  have 0: "list_dtree t0" using assms(1) merge_empty_if_nwf_sucs by fastforce
  have "merge t0 ≠ Node (root t0) {||}" using assms(1) by force
  then obtain e1 where e1_def: "merge t0 = Node (root t0) {|(t1,e1)|}"
    using assms(1) merge_single_root1_sucs by blast
  then obtain ys where ys_def:
      "(root t1, e1) # ys = ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)"
    unfolding merge_def by (metis (no_types, lifting) dtree_to_list.simps(1) dtree_to_from_list_id)
  then have "merge t0 = dtree_from_list (root t0) ((root t1, e1) # ys)" unfolding merge_def by simp
  then have "t1 = dtree_from_list (root t1) ys" using e1_def by simp
  then have "dverts t1 = (fst ` set ((root t1, e1) # ys))"
    using dtree_from_list_eq_dverts[of "root t1" ys] by simp
  then have "x ∈ fst ` set (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0))"
    using assms(2) ys_def by simp
  then show ?thesis using merge_ffold_fsts_in_childverts[of "root t0"] 0 by simp
qed

lemma sucs_dverts_eq_dtree_list:
  assumes "(t1,e1) ∈ fset (sucs t)" and "max_deg t1 ≤ 1"
  shows "dverts (Node (root t) {|(t1,e1)|}) - {root t}
        = fst ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
proof -
  have "{|(t1,e1)|} |⊆| sucs t" using assms(1) by fast
  then have wf: "wf_dverts (Node (root t) {|(t1,e1)|})"
    using wf_verts wf_dverts_sub by (metis dtree.exhaust_sel)
  have "∀(t1,e1) ∈ fset (sucs t) . fcard {|(t1,e1)|} = 1" using fcard_single_1 by fast
  moreover have "max_deg (Node (root t) {|(t1,e1)|}) = max (max_deg t1) (fcard {|(t1,e1)|})"
    using mdeg_singleton by fast
  ultimately have "max_deg (Node (root t) {|(t1,e1)|}) ≤ 1"
    using assms by fastforce
  then show ?thesis using dtree_to_list_eq_dverts[OF wf] by simp
qed

lemma merge_ffold_set_eq_union:
  "list_dtree (Node r xs)
    ⟹ set (ffold (merge_f r xs) [] xs) = (⋃x∈fset xs. set (dtree_to_list (Node r {|x|})))"
proof(induction xs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge] by blast
  have 1: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(1) by blast
  have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] by blast
  also have "… = ?f x (ffold ?f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1) by fastforce
  finally have "ffold ?f [] (finsert x xs)
              = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
    using xs_val insert.prems by simp
  then have "set (ffold ?f [] (finsert x xs))
        = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs))"
    by argo
  then have "set (ffold ?f [] (finsert x xs))
        = (set (dtree_to_list (Node r {|x|})) ∪ set (ffold ?f' [] xs))" using set_merge by fast
  then show ?case using 1 insert.IH by simp
qed (simp add: ffold.rep_eq)

lemma sucs_dverts_no_root:
  "(t1,e1) ∈ fset (sucs t) ⟹ dverts (Node (root t) {|(t1,e1)|}) - {root t} = dverts t1"
  using wf_verts wf_dverts'.simps unfolding wf_dverts_iff_dverts' by fastforce

lemma dverts_merge_sub:
  assumes "∀t ∈ fst ` fset (sucs t0). max_deg t ≤ 1"
  shows "dverts (merge t0) ⊆ dverts t0"
proof
  fix x
  assume asm: "x ∈ dverts (merge t0)"
  show "x ∈ dverts t0"
  proof(cases "x = root (merge t0)")
    case True
    then show ?thesis by (simp add: dtree.set_sel(1))
  next
    case False
    then obtain t1 e1 where t1_def: "merge t0 = Node (root t0) ({|(t1,e1)|})"
      using merge_cases_sucs asm by fastforce
    then have 0: "list_dtree (Node (root t0) (sucs t0))"
      using merge_empty_if_nwf_sucs by fastforce
    have "x ∈ fst ` set (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0))"
      using t1_def unfolding merge_def using False asm t1_def
        dtree_from_list_eq_dverts[of "root t0" "ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)"]
      by auto
    then obtain t2 e2 where t2_def:
        "(t2,e2) ∈ fset (sucs t0)" "x ∈ fst ` set (dtree_to_list (Node (root t0) {|(t2,e2)|}))"
      using merge_ffold_set_sub_union[OF 0] by fast
    then have "x ∈ dverts t2" by (simp add: dtree_to_list_x_in_dverts)
    then show ?thesis using t2_def(1) dtree.set_sel(2) by fastforce
  qed
qed

lemma dverts_merge_eq[simp]:
  assumes "∀t ∈ fst ` fset (sucs t). max_deg t ≤ 1"
  shows "dverts (merge t) = dverts t"
proof -
  have "∀(t1,e1) ∈ fset (sucs t). dverts (Node (root t) {|(t1,e1)|}) - {root t}
        = fst ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
    using sucs_dverts_eq_dtree_list assms
    by (smt (verit, ccfv_threshold) case_prodI2 fst_conv image_iff)
  then have "∀(t1,e1) ∈ fset (sucs t). dverts t1
              = fst ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
    by (metis (mono_tags, lifting) sucs_dverts_no_root case_prodD case_prodI2)
  then have "(⋃x∈fset (sucs t). ⋃ (dverts ` Basic_BNFs.fsts x))
          = (⋃x∈fset (sucs t). fst ` set (dtree_to_list (Node (root t) {|x|})))"
    by force
  then have "dverts t
          = insert (root t) (⋃x∈fset (sucs t). fst ` set (dtree_to_list (Node (root t) {|x|})))"
    using dtree.simps(6)[of "root t" "sucs t"] by auto
  also have "… = insert (root t) (fst ` set (ffold (merge_f (root t) (sucs t)) [] (sucs t)))"
    using merge_ffold_set_eq_union[of "root t" "sucs t"] list_dtree_axioms by auto
  also have "… = dverts (dtree_from_list (root t) (ffold (merge_f (root t) (sucs t)) [] (sucs t)))"
    using dtree_from_list_eq_dverts[of "root t"] by blast
  finally show ?thesis unfolding merge_def by blast
qed

lemma dlverts_merge_eq[simp]:
  assumes "∀t ∈ fst ` fset (sucs t). max_deg t ≤ 1"
  shows "dlverts (merge t) = dlverts t"
  using dverts_merge_eq[OF assms] by (simp add: dlverts_eq_dverts_union)

lemma sucs_darcs_eq_dtree_list:
  assumes "(t1,e1) ∈ fset (sucs t)" and "max_deg t1 ≤ 1"
  shows "darcs (Node (root t) {|(t1,e1)|}) = snd ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
proof -
  have "∀(t1,e1) ∈ fset (sucs t) . fcard {|(t1,e1)|} = 1" using fcard_single_1 by fast
  moreover have "max_deg (Node (root t) {|(t1,e1)|}) = max (max_deg t1) (fcard {|(t1,e1)|})"
    using mdeg_singleton by fast
  ultimately have "max_deg (Node (root t) {|(t1,e1)|}) ≤ 1"
    using assms by fastforce
  then show ?thesis using dtree_to_list_eq_darcs by blast
qed

lemma darcs_merge_eq[simp]:
  assumes "∀t ∈ fst ` fset (sucs t). max_deg t ≤ 1"
  shows "darcs (merge t) = darcs t"
proof -
  have 0: "list_dtree (Node (root t) (sucs t))" using list_dtree_axioms by simp
  have "∀(t1,e1) ∈ fset (sucs t). darcs (Node (root t) {|(t1,e1)|})
        = snd ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
    using sucs_darcs_eq_dtree_list assms
    by (smt (verit, ccfv_threshold) case_prodI2 fst_conv image_iff)
  then have "∀(t1,e1) ∈ fset (sucs t). darcs t1 ∪ {e1}
              = snd ` set (dtree_to_list (Node (root t) {|(t1,e1)|}))"
    by simp
  moreover have "darcs t = (⋃(t1,e1)∈fset (sucs t). darcs t1 ∪ {e1})"
    using dtree.simps(7)[of "root t" "sucs t"] by force
  ultimately have "darcs t
            = (⋃(t1,e1)∈fset (sucs t). snd ` set (dtree_to_list (Node (root t) {|(t1,e1)|})))"
    by (smt (verit, best) Sup.SUP_cong case_prodE case_prod_conv)
  also have "… = (snd ` set (ffold (merge_f (root t) (sucs t)) [] (sucs t)))"
    using merge_ffold_set_eq_union[OF 0] by blast
  also have "… = darcs (dtree_from_list (root t) (ffold (merge_f (root t) (sucs t)) [] (sucs t)))"
    using dtree_from_list_eq_darcs[of "root t"] by fast
  finally show ?thesis unfolding merge_def by blast
qed

subsubsection ‹Merging Preserves Well-Formedness›

lemma dtree_to_list_x_in_darcs:
  "x ∈ snd ` set (dtree_to_list (Node r {|(t1,e1)|})) ⟹ x ∈ (darcs t1 ∪ {e1})"
  using dtree_to_list_sub_darcs by fastforce

lemma dtree_to_list_snds_disjoint:
  "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}
    ⟹ snd ` set (dtree_to_list (Node r {|(t1,e1)|})) ∩ (darcs t2 ∪ {e2}) = {}"
  using dtree_to_list_x_in_darcs by fast

lemma dtree_to_list_snds_disjoint2:
  "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}
    ⟹ snd ` set (dtree_to_list (Node r {|(t1,e1)|}))
      ∩ snd ` set (dtree_to_list (Node r {|(t2,e2)|})) = {}"
  using disjoint_iff dtree_to_list_x_in_darcs by metis

lemma merge_ffold_arc_inter_preserv:
  "⟦list_dtree (Node r ys); xs |⊆| ys; (darcs t1 ∪ {e1}) ∩ (snd ` set z) = {};
    (t1,e1) ∈ fset ys; (t1,e1) ∉ fset xs⟧
    ⟹ (darcs t1 ∪ {e1}) ∩ (snd ` set (ffold (merge_f r xs) z xs)) = {}"
proof(induction xs)
  case (insert x xs)
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge"
  show ?case
  proof(cases "ffold ?f z (finsert x xs) = ffold ?f' z xs")
    case True
    then show ?thesis using insert.IH insert.prems by auto
  next
    case False
    obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
    have 0: "list_dtree (Node r (finsert x xs))" using list_dtree_subset insert.prems(1,2) by blast
    have "(t2,e2) ≠ (t1,e1)" using insert.prems(5) t2_def by fastforce
    moreover have "(t2,e2) ∈ fset ys" using insert.prems(2) by fastforce
    moreover have "disjoint_darcs ys"
      using disjoint_darcs_if_wf[OF list_dtree.wf_arcs [OF insert.prems(1)]] by simp
    ultimately have "(darcs t1 ∪ {e1}) ∩ (darcs t2 ∪ {e2}) = {}"
      using insert.prems(4) by fast
    then have 1: "(darcs t1 ∪ {e1}) ∩ snd ` set (dtree_to_list (Node r {|(t2, e2)|})) = {}"
      using dtree_to_list_snds_disjoint by fast
    have 2: "(darcs t1 ∪ {e1}) ∩ snd ` set (ffold ?f' z xs) = {}"
      using insert.IH insert.prems by simp
    have "xs |⊆| finsert x xs" by blast
    then have f_xs: "ffold ?f z xs = ffold ?f' z xs"
      using merge_ffold_supset 0 by presburger
    have "ffold ?f z (finsert x xs) = ?f x (ffold ?f z xs)"
      using Comm.ffold_finsert[OF insert.hyps] by blast
    then have 0: "ffold ?f z (finsert x xs) = ?f x (ffold ?f' z xs)" using f_xs by argo
    then have "?f x (ffold ?f' z xs) ≠ ffold ?f' z xs" using False by argo
    then have "?f (t2,e2) (ffold ?f' z xs)
              = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
      using merge_f_merge_if_not_snd t2_def by blast
    then have "ffold ?f z (finsert x xs)
              = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
      using 0 t2_def by argo
    then have "set (ffold ?f z (finsert x xs))
        = set (dtree_to_list (Node r {|(t2,e2)|})) ∪ set (ffold ?f' z xs)"
      using set_merge[of "dtree_to_list (Node r {|(t2,e2)|})"] by presburger
    then show ?thesis using 1 2 by fast
  qed
qed (auto simp: ffold.rep_eq)

lemma merge_ffold_wf_list_arcs:
  "⟦⋀x. x ∈ fset xs ⟹ wf_darcs (Node r {|x|}); list_dtree (Node r xs)⟧
    ⟹ wf_list_arcs (ffold (merge_f r xs) [] xs)"
proof(induction xs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have 0: "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have t1_not_xs: "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(2) empty_list_valid_merge] by blast
  have 1: "wf_list_arcs (dtree_to_list (Node r {|x|}))"
    using insert.prems(1) 0 t1_def wf_list_arcs_if_wf_darcs by fast
  have "list_dtree (Node r xs)" using list_dtree_subset insert.prems(2) by blast
  then have 2: "wf_list_arcs (ffold ?f' [] xs)" using insert.IH insert.prems by auto
  have "darcs (Node r {|x|}) ∩ snd ` set (ffold ?f' [] xs) = {}"
    using merge_ffold_arc_inter_preserv[OF insert.prems(2), of xs t1 e1 "[]"] t1_not_xs by auto
  then have 3: "snd ` set (dtree_to_list (Node r {|x|})) ∩ snd ` set (ffold ?f' [] xs) = {}"
    using dtree_to_list_sub_darcs by fast
  have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] by blast
  also have "… = ?f x (ffold ?f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(2) by fastforce
  finally have "ffold ?f [] (finsert x xs)
              = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
    using xs_val insert.prems by simp
  then show ?case using wf_list_arcs_merge[OF 1 2 3] by presburger
qed (simp add: ffold.rep_eq)

lemma merge_wf_darcs: "wf_darcs (merge t)"
proof -
  have "wf_list_arcs (ffold (merge_f (root t) (sucs t)) [] (sucs t))"
    using merge_ffold_wf_list_arcs[OF wf_darcs_sucs[OF wf_arcs]] list_dtree_axioms by simp
  then show ?thesis using wf_darcs_iff_wf_list_arcs merge_def by fastforce
qed

lemma merge_ffold_wf_list_lverts:
  "⟦⋀x. x ∈ fset xs ⟹ wf_dlverts (Node r {|x|}); list_dtree (Node r xs)⟧
    ⟹ wf_list_lverts (ffold (merge_f r xs) [] xs)"
proof(induction xs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have 0: "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(2) empty_list_valid_merge] by blast
  have 1: "wf_list_lverts (dtree_to_list (Node r {|x|}))"
    using insert.prems(1) 0 t1_def wf_list_lverts_if_wf_dlverts by fast
  have "list_dtree (Node r xs)" using list_dtree_subset insert.prems(2) by blast
  then have 2: "wf_list_lverts (ffold ?f' [] xs)" using insert.IH insert.prems by auto
  have "∀v2∈fst ` set (ffold ?f' [] xs). set v2 ∩ dlverts t1 = {}"
    using xs_val by fastforce
  then have 3: "∀v1∈fst ` set (dtree_to_list (Node r {|x|})). ∀v2∈fst ` set (ffold ?f' [] xs).
                  set v1 ∩ set v2 = {}"
    using dtree_to_list_x1_list_disjoint t1_def by fast
  have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] by blast
  also have "… = ?f x (ffold ?f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(2) by fastforce
  finally have "ffold ?f [] (finsert x xs)
              = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
    using xs_val insert.prems by simp
  then show ?case using wf_list_lverts_merge[OF 1 2 3] by presburger
qed (simp add: ffold.rep_eq)

lemma merge_ffold_root_inter_preserv:
  "⟦list_dtree (Node r xs); ∀t1 ∈ fst ` fset xs. set r' ∩ dlverts t1 = {};
    ∀v1 ∈ fst ` set z. set r' ∩ set v1 = {}; (v,e) ∈ set (ffold (merge_f r xs) z xs)⟧
    ⟹ set r' ∩ set v = {}"
proof(induction xs)
  case (insert x xs)
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge"
  have 0: "list_dtree (Node r xs)" using insert.prems(1) list_dtree_subset by blast
  show ?case
  proof(cases "ffold ?f z (finsert x xs) = ffold ?f' z xs")
    case True
    then show ?thesis using insert.IH[OF 0] insert.prems(2-4) by simp
  next
    case not_right: False
    obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
    show ?thesis
    proof(cases "(v,e) ∈ set (dtree_to_list (Node r {|(t2,e2)|}))")
      case True
      then show ?thesis using dtree_to_list_x1_list_disjoint insert.prems(2) by fastforce
    next
      case False
      have "xs |⊆| finsert x xs" by blast
      then have f_xs: "ffold ?f z xs = ffold ?f' z xs"
        using merge_ffold_supset[of xs "finsert x xs"] insert.prems(1) by blast
      have "ffold ?f z (finsert x xs) = ?f x (ffold ?f z xs)"
        using Comm.ffold_finsert[OF insert.hyps] by blast
      then have 1: "ffold ?f z (finsert x xs) = ?f x (ffold ?f' z xs)" using f_xs by argo
      then have "?f x (ffold ?f' z xs) ≠ ffold ?f' z xs" using not_right by argo
      then have "?f (t2,e2) (ffold ?f' z xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using merge_f_merge_if_not_snd t2_def by blast
      then have "ffold ?f z (finsert x xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using 1 t2_def by argo
      then have "(v,e) ∈ set (?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs))"
        using insert.prems(4) by argo
      then have "(v,e) ∈ set (ffold ?f' z xs)" using set_merge False by fast
      then show ?thesis using insert.IH insert.prems(2-3) 0 by auto
    qed
  qed
qed (fastforce simp: ffold.rep_eq)

lemma merge_wf_dlverts: "wf_dlverts (merge t)"
proof -
  have 0: "list_dtree (Node (root t) (sucs t))" using list_dtree_axioms by simp
  have 1: "∀t1∈fst ` fset (sucs t). set (root t) ∩ dlverts t1 = {}"
    using wf_lverts wf_dlverts.simps[of "root t"] by fastforce
  have "∀v∈fst ` set (ffold (merge_f (root t) (sucs t)) [] (sucs t)). set (root t) ∩ set v = {}"
    using wf_lverts merge_ffold_root_inter_preserv[OF 0 1] by force
  moreover have "wf_list_lverts (ffold (merge_f (root t) (sucs t)) [] (sucs t))"
    using merge_ffold_wf_list_lverts[OF wf_dlverts_sucs[OF wf_lverts] 0] by simp
  moreover have "root t ≠ []" using wf_lverts wf_dlverts.elims(2) by fastforce
  ultimately show ?thesis unfolding merge_def using wf_dlverts_iff_wf_list_lverts by blast
qed

theorem merge_list_dtree: "list_dtree (merge t)"
  using merge_wf_dlverts merge_wf_darcs list_dtree_def by blast

corollary merge_ranked_dtree: "ranked_dtree (merge t) cmp"
  using merge_list_dtree ranked_dtree_def ranked_dtree_axioms by auto

subsubsection ‹Additional Merging Properties›

lemma merge_ffold_distinct:
  "⟦list_dtree (Node r xs); ∀t1 ∈ fst ` fset xs. ∀v∈dverts t1. distinct v;
    ∀v1 ∈ fst ` set z. distinct v1; v ∈ fst ` set (ffold (merge_f r xs) z xs)⟧
    ⟹ distinct v"
proof(induction xs)
  case (insert x xs)
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge"
  have 0: "list_dtree (Node r xs)" using insert.prems(1) list_dtree_subset by blast
  show ?case
  proof(cases "ffold ?f z (finsert x xs) = ffold ?f' z xs")
    case True
    then show ?thesis using insert.IH[OF 0] insert.prems(2-4) by simp
  next
    case not_right: False
    obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
    show ?thesis
    proof(cases "v ∈ fst ` set (dtree_to_list (Node r {|(t2,e2)|}))")
      case True
      have "∀v∈dverts t2. distinct v" using insert.prems(2) by simp
      then have 2: "∀v∈fst ` set (dtree_to_list (Node r {|(t2,e2)|})). distinct v"
        by (simp add: dtree_to_list_x_in_dverts)
      then show ?thesis using True by auto
    next
      case False
      have "xs |⊆| finsert x xs" by blast
      then have f_xs: "ffold ?f z xs = ffold ?f' z xs"
        using merge_ffold_supset insert.prems(1) by presburger
      have "ffold ?f z (finsert x xs) = ?f x (ffold ?f z xs)"
        using Comm.ffold_finsert[OF insert.hyps] by blast
      then have 1: "ffold ?f z (finsert x xs) = ?f x (ffold ?f' z xs)" using f_xs by argo
      then have "?f x (ffold ?f' z xs) ≠ ffold ?f' z xs" using not_right by argo
      then have "?f (t2,e2) (ffold ?f' z xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using merge_f_merge_if_not_snd t2_def by blast
      then have "ffold ?f z (finsert x xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
        using 1 t2_def by argo
      then have "v ∈ fst ` set (?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs))"
        using insert.prems(4) by argo
      then have "v ∈ fst ` set (ffold ?f' z xs)" using set_merge False by fast
      then show ?thesis using insert.IH[OF 0] insert.prems(2-3) by simp
    qed
  qed
qed (fastforce simp: ffold.rep_eq)

lemma distinct_merge:
  assumes "∀v∈dverts t. distinct v" and "v∈dverts (merge t)"
  shows "distinct v"
proof(cases "v = root t")
  case True
  then show ?thesis by (simp add: dtree.set_sel(1) assms(1))
next
  case False
  then have 0: "v ∈ fst ` set (ffold (merge_f (root t) (sucs t)) [] (sucs t))"
    using merge_def assms(2) dtree_from_list_eq_dverts[of "root t"] by auto
  moreover have "∀t1∈fst ` fset (sucs t). ∀v∈dverts t1. distinct v"
    using assms(1) dverts_child_subset[of "root t" "sucs t"] by auto
  moreover have "∀v1∈fst ` set []. distinct v1" by simp
  moreover have 0: "list_dtree (Node (root t) (sucs t))" using list_dtree_axioms by simp
  ultimately show ?thesis using merge_ffold_distinct by fast
qed

lemma merge_hd_root_eq[simp]: "hd (root (merge t1)) = hd (root t1)"
  unfolding merge_def by auto

lemma merge_ffold_hd_is_child:
  "⟦list_dtree (Node r xs); xs ≠ {||}⟧
    ⟹ ∃(t1,e1) ∈ fset xs. hd (ffold (merge_f r xs) [] xs) = (root t1,e1)"
proof(induction xs)
  case (insert x xs)
  interpret Comm: comp_fun_commute "merge_f r (finsert x xs)" by (rule merge_commute)
  define f where "f = merge_f r (finsert x xs)"
  define f' where "f' = merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge cmp'"
  have 0: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(1) by blast
  obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
  have i1: "∃(t1, e1)∈fset (finsert x xs). hd (dtree_to_list (Node r {|(t2,e2)|})) = (root t1, e1)"
    by simp
  have "(t2, e2) ∈ fset (finsert x xs)" by simp
  moreover have "(t2, e2) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold f' [] xs). set v ∩ dlverts t2 = {} ∧ v ≠ [] ∧ e ∉ darcs t2 ∪ {e2})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge] f'_def
    by blast
  have "ffold f [] (finsert x xs) = f x (ffold f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] f_def by blast
  also have "… = f x (ffold f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1) f_def f'_def by fastforce
  finally have "ffold f [] (finsert x xs) = ?merge (dtree_to_list (Node r {|x|})) (ffold f' [] xs)"
    using xs_val insert.prems f_def by simp
  then have merge: "ffold f [] (finsert x xs)
              = ?merge (dtree_to_list (Node r {|(t2,e2)|})) (ffold f'[] xs)"
    using t2_def by blast
  show ?case
  proof(cases "xs = {||}")
    case True
    then show ?thesis using merge i1 f_def by (auto simp: ffold.rep_eq)
  next
    case False
    then have i2: "∃(t1,e1) ∈ fset (finsert x xs). hd (ffold f' [] xs) = (root t1,e1)"
      using insert.IH[OF 0] f'_def by simp
    show ?thesis using merge_hd_exists_preserv[OF i1 i2] merge f_def by simp
  qed
qed(simp)

lemma merge_ffold_nempty_if_child:
  assumes "(t1,e1) ∈ fset (sucs (merge t0))"
  shows "ffold (merge_f (root t0) (sucs t0)) [] (sucs t0) ≠ []"
  using assms unfolding merge_def by auto

lemma merge_ffold_hd_eq_child:
  assumes "(t1,e1) ∈ fset (sucs (merge t0))"
  shows "hd (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)) = (root t1,e1)"
proof -
  have "merge t0 = (dtree_from_list (root t0) (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)))"
    unfolding merge_def by blast
  have "merge t0 = (Node (root t0) {|(t1,e1)|})" using merge_cases_sucs[of t0] assms by auto
  have 0: "(Node (root t0) {|(t1,e1)|})
      = (dtree_from_list (root t0) (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)))"
    using merge_cases_sucs[of t0] assms unfolding merge_def by fastforce
  then obtain ys where "(root t1, e1) # ys = ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)"
    using dtree_from_list_eq_singleton[OF 0] by blast
  then show ?thesis using list.sel(1)[of "(root t1, e1)" ys] by simp
qed

lemma merge_child_in_orig:
  assumes "(t1,e1) ∈ fset (sucs (merge t0))"
  shows "∃(t2,e2) ∈ fset (sucs t0). (root t2,e2) = (root t1,e1)"
proof -
  have 0: "list_dtree (Node (root t0) (sucs t0))" using assms merge_empty_if_nwf_sucs by fastforce
  have "sucs t0 ≠ {||}" using assms merge_empty_sucs by fastforce
  then obtain t2 e2 where t2_def: "(t2,e2) ∈ fset (sucs t0)"
    "hd (ffold (merge_f (root t0) (sucs t0)) [] (sucs t0)) = (root t2,e2)"
    using merge_ffold_hd_is_child[OF 0] by blast
  then show ?thesis using merge_ffold_hd_eq_child[OF assms] by auto
qed

lemma ffold_singleton: "comp_fun_commute f ⟹ ffold f z {|x|} = f x z"
  using comp_fun_commute.ffold_finsert
  by (metis comp_fun_commute.ffold_empty finsert_absorb finsert_not_fempty)

lemma ffold_singleton1:
  "⟦comp_fun_commute (λa b. if P a b then Q a b else R a b); P x z⟧
    ⟹ ffold (λa b. if P a b then Q a b else R a b) z {|x|} = Q x z"
  using ffold_singleton by fastforce

lemma ffold_singleton2:
  "⟦comp_fun_commute (λa b. if P a b then Q a b else R a b); ¬P x z⟧
    ⟹ ffold (λa b. if P a b then Q a b else R a b) z {|x|} = R x z"
  using ffold_singleton by fastforce

lemma merge_ffold_singleton_if_wf:
  assumes "list_dtree (Node r {|(t1,e1)|})"
  shows "ffold (merge_f r {|(t1,e1)|}) [] {|(t1,e1)|} = dtree_to_list (Node r {|(t1,e1)|})"
proof -
  interpret Comm: comp_fun_commute "merge_f r {|(t1,e1)|}" by (rule merge_commute)
  define f where "f = merge_f r {|(t1,e1)|}"
  have "ffold f [] {|(t1,e1)|} = f (t1,e1) (ffold f [] {||})"
    using Comm.ffold_finsert f_def by blast
  then show ?thesis using f_def assms by (simp add: ffold.rep_eq)
qed

lemma merge_singleton_if_wf:
  assumes "list_dtree (Node r {|(t1,e1)|})"
  shows "merge (Node r {|(t1,e1)|}) = dtree_from_list r (dtree_to_list (Node r {|(t1,e1)|}))"
  using merge_ffold_singleton_if_wf[OF assms] merge_xs by simp

lemma merge_disjoint_if_child:
  "merge (Node r {|(t1,e1)|}) = Node r {|(t2,e2)|} ⟹ list_dtree (Node r {|(t1,e1)|})"
  using merge_empty_if_nwf by fastforce

lemma merge_root_child_eq:
  "merge (Node r {|(t1,e1)|}) = Node r {|(t2,e2)|} ⟹ root t1 = root t2"
  using merge_singleton_if_wf[OF merge_disjoint_if_child] by fastforce

lemma merge_ffold_split_subtree:
  "⟦∀t ∈ fst ` fset xs. max_deg t ≤ 1; list_dtree (Node r xs);
    as@(v,e)#bs = ffold (merge_f r xs) [] xs⟧
    ⟹ ∃ys. strict_subtree (Node v ys) (Node r xs) ∧ dverts (Node v ys) ⊆ (fst ` set ((v,e)#bs))"
proof(induction xs arbitrary: as bs)
  case (insert x xs)
  obtain t1 e1 where t1_def[simp]: "x = (t1,e1)" by fastforce
  define f' where "f' = merge_f r xs"
  let ?f = "merge_f r (finsert x xs)"
  let ?f' = "merge_f r xs"
  have "(t1, e1) ∈ fset (finsert x xs)" by simp
  moreover have "(t1, e1) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold ?f' [] xs). set v ∩ dlverts t1 = {} ∧ v ≠ [] ∧ e ∉ darcs t1 ∪ {e1})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(2) empty_list_valid_merge] by blast
  have 0: "∀t ∈ fst ` fset xs. max_deg t ≤ 1" using insert.prems(1) by simp
  have 1: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(2) by blast
  have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] by blast
  also have "… = ?f x (ffold ?f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(2) by fastforce
  finally have ind: "ffold ?f [] (finsert x xs)
              = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold f' [] xs)"
    using insert.prems(2) xs_val f'_def by simp
  have "max_deg (fst x) ≤ 1" using insert.prems(1) by simp
  then have "max_deg (Node r {|x|}) ≤ 1"
    using mdeg_child_sucs_eq_if_gt1[of r "fst x" "snd x" "root (fst x)"] by fastforce
  then have "∀as bs. as@(v,e)#bs = dtree_to_list (Node r {|x|}) ⟶
        (∃zs. strict_subtree (Node v zs) (Node r {|x|})
          ∧ dverts (Node v zs) ⊆ fst ` set ((v,e)#bs))"
    using dtree_to_list_split_subtree_dverts_eq_fsts' by fast
  then have left: "∀as bs. as@(v,e)#bs = dtree_to_list (Node r {|x|}) ⟶
        (∃zs. strict_subtree (Node v zs) (Node r (finsert x xs))
          ∧ dverts (Node v zs) ⊆ fst ` set ((v,e)#bs))"
    using strict_subtree_singleton[where xs="finsert x xs"] by blast
  have "∀as bs. as@(v,e)#bs = ffold f' [] xs ⟶
        (∃zs. strict_subtree (Node v zs) (Node r xs)
          ∧ dverts (Node v zs) ⊆ fst ` set ((v,e)#bs))"
    using insert.IH[OF 0 1] f'_def by blast
  then have right: "∀as bs. as@(v,e)#bs = ffold f' [] xs ⟶
        (∃zs. strict_subtree (Node v zs) (Node r (finsert x xs))
          ∧ dverts (Node v zs) ⊆ fst ` set ((v,e)#bs))"
    using strict_subtree_subset[where r=r and xs=xs and ys="finsert x xs"] by fast
  then show ?case using merge_split_supset_strict_subtree[OF left right] ind insert.prems(3) by simp
qed (simp add: ffold.rep_eq)

lemma merge_strict_subtree_dverts_sup:
  assumes "∀t ∈ fst ` fset (sucs t). max_deg t ≤ 1"
      and "strict_subtree (Node r xs) (merge t)"
    shows "∃ys. is_subtree (Node r ys) t ∧ dverts (Node r ys) ⊆ dverts (Node r xs)"
proof -
  have 0: "list_dtree (Node (root t) (sucs t))" using list_dtree_axioms by simp
  have "∀as r e bs. as@(r,e)#bs = ffold (merge_f (root t) (sucs t)) [] (sucs t)
    ⟶ (∃ys. strict_subtree (Node r ys) (Node (root t) (sucs t))
         ∧ dverts (Node r ys) ⊆ fst ` set ((r,e)#bs))"
    using merge_ffold_split_subtree[OF assms(1) 0] by blast
  then have "∀as r e bs. as@(r,e)#bs = ffold (merge_f (root t) (sucs t)) [] (sucs t) ⟶
    (∃ys. strict_subtree (Node r ys) t ∧ dverts (Node r ys) ⊆ fst ` set ((r,e)#bs))"
    by simp
  obtain as e bs where bs_def: "as@(r,e)#bs = ffold (merge_f (root t) (sucs t)) [] (sucs t)"
    using assms(2) dtree_from_list_uneq_sequence_xs[of r] unfolding merge_def by blast
  have "wf_dverts (merge t)" by (simp add: merge_wf_dlverts wf_dverts_if_wf_dlverts)
  then have wf: "wf_dverts (dtree_from_list (root t) (as@(r,e)#bs))"
    unfolding merge_def bs_def .
  moreover obtain ys where
      "strict_subtree (Node r ys) t" "dverts (Node r ys) ⊆ fst ` set ((r,e)#bs)"
    using merge_ffold_split_subtree[OF assms(1) 0 bs_def] by auto
  moreover have "strict_subtree (Node r xs) (dtree_from_list (root t) (as@(r,e)#bs))"
    using assms(2) unfolding bs_def merge_def .
  ultimately show ?thesis
    using dtree_from_list_dverts_subset_wfdverts1 unfolding strict_subtree_def by fast
qed

lemma merge_subtree_dverts_supset:
  assumes "∀t∈fst ` fset (sucs t). max_deg t ≤ 1" and "is_subtree (Node r xs) (merge t)"
  shows "∃ys. is_subtree (Node r ys) t ∧ dverts (Node r ys) ⊆ dverts (Node r xs)"
proof(cases "Node r xs = merge t")
  case True
  then obtain ys where "t = Node r ys" using merge_root_eq dtree.exhaust_sel dtree.sel(1) by metis
  then show ?thesis using dverts_merge_eq[OF assms(1)] True by auto
next
  case False
  then show ?thesis using merge_strict_subtree_dverts_sup assms strict_subtree_def by blast
qed

lemma merge_subtree_dlverts_supset:
  assumes "∀t∈fst ` fset (sucs t). max_deg t ≤ 1" and "is_subtree (Node r xs) (merge t)"
  shows "∃ys. is_subtree (Node r ys) t ∧ dlverts (Node r ys) ⊆ dlverts (Node r xs)"
proof -
  obtain ys where "is_subtree (Node r ys) t" "dverts (Node r ys) ⊆ dverts (Node r xs)"
    using merge_subtree_dverts_supset[OF assms] by blast
  then show ?thesis using dlverts_eq_dverts_union[of "Node r ys"] dlverts_eq_dverts_union by fast
qed

end

subsection ‹Normalizing Dtrees›

context ranked_dtree
begin

subsubsection ‹Definitions›

function normalize1 :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "normalize1 (Node r {|(t1,e)|}) =
    (if rank (rev (root t1)) < rank (rev r) then Node (r@root t1) (sucs t1)
    else Node r {|(normalize1 t1,e)|})"
| "∀x. xs ≠ {|x|} ⟹ normalize1 (Node r xs) = Node r ((λ(t,e). (normalize1 t,e)) |`| xs)"
  by (metis darcs_mset.cases old.prod.exhaust) fast+
termination by lexicographic_order

lemma normalize1_size_decr[termination_simp]:
  "normalize1 t1 ≠ t1 ⟹ size (normalize1 t1) < size t1"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  then show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then show ?thesis using dtree_size_eq_root[of "root t" "sucs t"] by simp
  next
    case False
    then show ?thesis using dtree_size_img_le 1 by auto
  qed
next
  case (2 xs r)
  then have 0: "∀t ∈ fst ` fset xs. size (normalize1 t) ≤ size t" by fastforce
  moreover have "∃t ∈ fst ` fset xs. size (normalize1 t) < size t"
    using elem_neq_if_fset_neq[of normalize1 xs] 2 by fastforce
  ultimately show ?case using dtree_size_img_lt "2.hyps" by auto
qed

lemma normalize1_size_le: "size (normalize1 t1) ≤ size t1"
  by(cases "normalize1 t1=t1") (auto dest: normalize1_size_decr)

fun normalize :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "normalize t1 = (let t2 = normalize1 t1 in if t1 = t2 then t2 else normalize t2)"

subsubsection ‹Basic Proofs›

lemma root_normalize1_eq1:
  "¬rank (rev (root t1)) < rank (rev r) ⟹ root (normalize1 (Node r {|(t1,e1)|})) = r"
  by simp

lemma root_normalize1_eq1':
  "¬rank (rev (root t1)) ≤ rank (rev r) ⟹ root (normalize1 (Node r {|(t1,e1)|})) = r"
  by simp

lemma root_normalize1_eq2: "∀x. xs ≠ {|x|} ⟹ root (normalize1 (Node r xs)) = r"
  by simp

lemma fset_img_eq: "∀x ∈ fset xs. f x = x ⟹ f |`| xs = xs"
  using fset_inject[of xs "f |`| xs"] by simp

lemma fset_img_uneq: "f |`| xs ≠ xs ⟹ ∃x ∈ fset xs. f x ≠ x"
  using fset_img_eq by fastforce

lemma fset_img_uneq_prod: "(λ(t,e). (f t, e)) |`| xs ≠ xs ⟹ ∃(t,e) ∈ fset xs. f t ≠ t"
  using fset_img_uneq[of "λ(t,e). (f t, e)" xs] by auto

lemma contr_if_normalize1_uneq:
  "normalize1 t1 ≠ t1
    ⟹ ∃v t2 e2. is_subtree (Node v {|(t2,e2)|}) t1 ∧ rank (rev (root t2)) < rank (rev v)"
proof(induction t1 rule: normalize1.induct)
  case (2 xs r)
  then show ?case using fset_img_uneq_prod[of normalize1 xs] by fastforce
qed(fastforce)

lemma contr_before_normalize1:
  "⟦is_subtree (Node v {|(t1,e1)|}) (normalize1 t3); rank (rev (root t1)) < rank (rev v)⟧
    ⟹ ∃v' t2 e2. is_subtree (Node v' {|(t2,e2)|}) t3 ∧ rank (rev (root t2)) < rank (rev v')"
  using contr_if_normalize1_uneq by force

subsubsection ‹Normalizing Preserves Well-Formedness›

lemma normalize1_darcs_sub: "darcs (normalize1 t1) ⊆ darcs t1"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  then show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then have "darcs (normalize1 (Node r {|(t,e)|})) = darcs (Node (r@root t) (sucs t))" by simp
    also have "… = darcs (Node (root t) (sucs t))" using darcs_sub_if_children_sub by fast
    finally show ?thesis by auto
  next
    case False
    then show ?thesis using 1 by auto
  qed
qed (fastforce)

lemma disjoint_darcs_normalize1:
  "wf_darcs t1 ⟹ disjoint_darcs ((λ(t,e). (normalize1 t,e)) |`| (sucs t1))"
  using disjoint_darcs_img[OF disjoint_darcs_if_wf, of t1 normalize1]
  by (simp add: normalize1_darcs_sub)

lemma wf_darcs_normalize1: "wf_darcs t1 ⟹ wf_darcs (normalize1 t1)"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then show ?thesis
      using "1.prems" dtree.collapse singletonI finsert.rep_eq case_prodD
      unfolding wf_darcs_iff_darcs'
      by (metis (no_types, lifting) wf_darcs'.simps bot_fset.rep_eq normalize1.simps(1))
  next
    case False
    have "disjoint_darcs {|(normalize1 t,e)|}"
      using normalize1_darcs_sub disjoint_darcs_if_wf_xs[OF "1.prems"] by auto
    then show ?thesis using 1 False unfolding wf_darcs_iff_darcs' by force
  qed
next
  case (2 xs r)
  then show ?case
    using disjoint_darcs_normalize1[OF "2.prems"]
    by (fastforce simp: wf_darcs_iff_darcs')
qed

lemma normalize1_dlverts_eq[simp]: "dlverts (normalize1 t1) = dlverts t1"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  then show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then show ?thesis using dlverts.simps[of "root t" "sucs t"] by force
  next
    case False
    then show ?thesis using 1 by auto
  qed
qed (fastforce)

lemma normalize1_dverts_contr_subtree:
  "⟦v ∈ dverts (normalize1 t1); v ∉ dverts t1⟧
    ⟹ ∃v2 t2 e2. is_subtree (Node v2 {|(t2,e2)|}) t1
        ∧ v2 @ root t2 = v ∧ rank (rev (root t2)) < rank (rev v2)"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then show ?thesis using "1.prems" dverts_suc_subseteq by fastforce
  next
    case False
    then show ?thesis using 1 by auto
  qed
qed(fastforce)

lemma normalize1_dverts_app_contr:
  "⟦v ∈ dverts (normalize1 t1); v ∉ dverts t1⟧
    ⟹ ∃v1∈dverts t1. ∃v2∈dverts t1. v1 @ v2 = v ∧ rank (rev v2) < rank (rev v1)"
  using normalize1_dverts_contr_subtree
  by (fastforce simp: single_subtree_root_dverts single_subtree_child_root_dverts)

lemma disjoint_dlverts_img:
  assumes "disjoint_dlverts xs" and "∀(t,e) ∈ fset xs. dlverts (f t) ⊆ dlverts t"
  shows "disjoint_dlverts ((λ(t,e). (f t,e)) |`| xs)" (is "disjoint_dlverts ?xs")
proof (rule ccontr)
  assume "¬ disjoint_dlverts ?xs"
  then obtain x1 e1 y1 e2 where asm: "(x1,e1) ∈ fset ?xs" "(y1,e2) ∈ fset ?xs"
      "dlverts x1 ∩ dlverts y1 ≠ {} ∧ (x1,e1)≠(y1,e2)" by blast
  then obtain x2 where x2_def: "f x2 = x1" "(x2,e1) ∈ fset xs" by auto
  obtain y2 where y2_def: "f y2 = y1" "(y2,e2) ∈ fset xs" using asm(2) by auto
  have "dlverts x1 ⊆ dlverts x2" using assms(2) x2_def by fast
  moreover have "dlverts y1 ⊆ dlverts y2" using assms(2) y2_def by fast
  ultimately have "¬ disjoint_dlverts xs" using asm(3) x2_def y2_def by blast
  then show False using assms(1) by blast
qed

lemma disjoint_dlverts_normalize1:
  "disjoint_dlverts xs ⟹ disjoint_dlverts ((λ(t,e). (normalize1 t,e)) |`| xs)"
  using disjoint_dlverts_img[of xs] by simp

lemma disjoint_dlverts_normalize1_sucs:
  "disjoint_dlverts (sucs t1) ⟹ disjoint_dlverts ((λ(t,e). (normalize1 t,e)) |`| (sucs t1))"
  using disjoint_dlverts_img[of "sucs t1"] by simp

lemma disjoint_dlverts_normalize1_wf:
  "wf_dlverts t1 ⟹ disjoint_dlverts ((λ(t,e). (normalize1 t,e)) |`| (sucs t1))"
  using disjoint_dlverts_img[OF disjoint_dlverts_if_wf, of t1] by simp

lemma disjoint_dlverts_normalize1_wf':
  "wf_dlverts (Node r xs) ⟹ disjoint_dlverts ((λ(t,e). (normalize1 t,e)) |`| xs)"
  using disjoint_dlverts_img[OF disjoint_dlverts_if_wf, of "Node r xs"] by simp

lemma root_empty_inter_dlverts_normalize1:
  assumes "wf_dlverts t1" and "(x1,e1) ∈ fset  ((λ(t,e). (normalize1 t,e)) |`| (sucs t1))"
  shows "set (root t1) ∩ dlverts x1 = {}"
proof (rule ccontr)
  assume asm: "set (root t1) ∩ dlverts x1 ≠ {}"
  obtain x2 where x2_def: "normalize1 x2 = x1" "(x2,e1) ∈ fset (sucs t1)" using assms(2) by auto
  have "set (root t1) ∩ dlverts x2 ≠ {}" using x2_def(1) asm by force
  then show False using x2_def(2) assms(1) wf_dlverts.simps[of "root t1" "sucs t1"] by auto
qed

lemma wf_dlverts_normalize1: "wf_dlverts t1 ⟹ wf_dlverts (normalize1 t1)"
proof(induction t1 rule: normalize1.induct)
  case (1 r t e)
  show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    have 0: "∀(t1,e1) ∈ fset (sucs t). wf_dlverts t1"
      using "1.prems" wf_dlverts.simps[of "root t" "sucs t"] by auto
    have "∀(t1,e1) ∈ fset (sucs t). set (root t) ∩ dlverts t1 = {}"
      using "1.prems" wf_dlverts.simps[of "root t"] by fastforce
    then have "∀(t1,e1) ∈ fset (sucs t). set (r@root t) ∩ dlverts t1 = {}"
      using suc_in_dlverts "1.prems" by fastforce
    then show ?thesis using True 0 disjoint_dlverts_if_wf[of t] "1.prems" by auto
  next
    case False
    then show ?thesis
      using root_empty_inter_dlverts_normalize1[OF "1.prems"] disjoint_dlverts_normalize1 1 by auto
  qed
next
  case (2 xs r)
  have "∀(t1,e1) ∈ fset ((λ(t, e). (normalize1 t, e)) |`| xs). set r ∩ dlverts t1 = {}"
    using root_empty_inter_dlverts_normalize1[OF "2.prems"] by force
  then show ?case using disjoint_dlverts_normalize1 2 by auto
qed

corollary list_dtree_normalize1: "list_dtree (normalize1 t)"
  using wf_dlverts_normalize1[OF wf_lverts] wf_darcs_normalize1[OF wf_arcs] list_dtree_def by blast

corollary ranked_dtree_normalize1: "ranked_dtree (normalize1 t) cmp"
  using list_dtree_normalize1 ranked_dtree_def ranked_dtree_axioms by blast

lemma normalize_darcs_sub: "darcs (normalize t1) ⊆ darcs t1"
  apply(induction t1 rule: normalize.induct)
  by (smt (verit) normalize1_darcs_sub normalize.simps subset_trans)

lemma normalize_dlverts_eq: "dlverts (normalize t1) = dlverts t1"
  by(induction t1 rule: normalize.induct) (metis (full_types) normalize.elims normalize1_dlverts_eq)

theorem ranked_dtree_normalize: "ranked_dtree (normalize t) cmp"
  using ranked_dtree_axioms apply(induction t rule: normalize.induct)
  by (smt (verit) ranked_dtree.normalize.elims ranked_dtree.ranked_dtree_normalize1)

subsubsection ‹Distinctness and hd preserved›

lemma distinct_normalize1: "⟦∀v∈dverts t. distinct v; v∈dverts (normalize1 t)⟧ ⟹ distinct v"
using ranked_dtree_axioms proof(induction t rule: normalize1.induct)
  case (1 r t e)
  then interpret R: ranked_dtree "Node r {|(t, e)|}" rank by blast
  show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    interpret T: ranked_dtree t rank using R.ranked_dtree_rec by auto
    have "set r ∩ set (root t) = {}"
      using R.wf_lverts dlverts.simps[of "root t" "sucs t"] by auto
    then have "distinct (r@root t)" by (auto simp: dtree.set_sel(1) "1.prems"(1))
    moreover have "∀v ∈ (⋃(t, e)∈fset (sucs t). dverts t). distinct v"
      using "1.prems"(1) dtree.set(1)[of "root t" "sucs t"] by fastforce
    ultimately show ?thesis using dverts_root_or_child "1.prems"(2) True by auto
  next
    case False
    then show ?thesis using R.ranked_dtree_rec 1 by auto
  qed
next
  case (2 xs r)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case using R.ranked_dtree_rec 2 by fastforce
qed

lemma distinct_normalize: "∀v∈dverts t. distinct v ⟹ ∀v∈dverts (normalize t). distinct v"
using ranked_dtree_axioms proof(induction t rule: normalize.induct)
  case (1 t)
  then interpret T1: ranked_dtree "t" rank by blast
  interpret T2: ranked_dtree "normalize1 t" rank by (simp add: T1.ranked_dtree_normalize1)
  show ?case
    by (smt (verit, del_insts) 1 T1.distinct_normalize1 T2.ranked_dtree_axioms normalize.simps)
qed

lemma normalize1_hd_root_eq[simp]:
  assumes "root t1 ≠ []"
  shows "hd (root (normalize1 t1)) = hd (root t1)"
proof(cases "∀x. sucs t1 ≠ {|x|}")
  case True
  then show ?thesis using normalize1.simps(2)[of "sucs t1" "root t1"] by simp
next
  case False
  then obtain t e where "{|(t, e)|} = sucs t1" by auto
  then show ?thesis using normalize1.simps(1)[of "root t1" t e] assms by simp
qed

corollary normalize1_hd_root_eq':
  "wf_dlverts t1 ⟹ hd (root (normalize1 t1)) = hd (root t1)"
  using normalize1_hd_root_eq[of t1] wf_dlverts.simps[of "root t1" "sucs t1"] by simp

lemma normalize1_root_nempty:
  assumes "root t1 ≠ []"
  shows "root (normalize1 t1) ≠ []"
proof(cases "∀x. sucs t1 ≠ {|x|}")
  case True
  then show ?thesis using normalize1.simps(2)[of "sucs t1" "root t1"] assms by simp
next
  case False
  then obtain t e where "{|(t, e)|} = sucs t1" by auto
  then show ?thesis using normalize1.simps(1)[of "root t1" t e] assms by simp
qed

lemma normalize_hd_root_eq[simp]: "root t1 ≠ [] ⟹ hd (root (normalize t1)) = hd (root t1)"
using ranked_dtree_axioms proof(induction t1 rule: normalize.induct)
  case (1 t)
  then show ?case
  proof(cases "t = normalize1 t")
    case False
    then have "normalize t = normalize (normalize1 t)" by (simp add: Let_def)
    then show ?thesis using 1 normalize1_root_nempty by force
  qed(simp)
qed

corollary normalize_hd_root_eq'[simp]: "wf_dlverts t1 ⟹ hd (root (normalize t1)) = hd (root t1)"
  using normalize_hd_root_eq wf_dlverts.simps[of "root t1" "sucs t1"] by simp

subsubsection ‹Normalize and Sorting›

lemma normalize1_uneq_if_contr:
  "⟦is_subtree (Node r1 {|(t1,e1)|}) t2; rank (rev (root t1)) < rank (rev r1); wf_darcs t2⟧
    ⟹ t2 ≠ normalize1 t2"
proof(induction t2 rule: normalize1.induct)
  case (1 r t e)
  then show ?case
  proof(cases "rank (rev (root t)) < rank (rev r)")
    case True
    then show ?thesis using combine_uneq by fastforce
  next
    case False
    then show ?thesis using 1 by auto
  qed
next
  case (2 xs r)
  then obtain t e where t_def: "(t,e) ∈ fset xs" "is_subtree (Node r1 {|(t1,e1)|}) t" by auto
  then have "t ≠ normalize1 t" using 2 by fastforce
  then have "(normalize1 t, e) ∉ fset xs"
    using "2.prems"(3) t_def(1) by (auto simp: wf_darcs_iff_darcs')
  moreover have "(normalize1 t, e) ∈ fset ((λ(t,e). (normalize1 t,e)) |`| xs)"
    using t_def(1) by auto
  ultimately have "(λ(t,e). (normalize1 t,e)) |`| xs ≠ xs" using t_def(1) by fastforce
  then show ?case using "2.hyps" by simp
qed

lemma sorted_ranks_if_normalize1_eq:
  "⟦wf_darcs t2; is_subtree (Node r1 {|(t1,e1)|}) t2; t2 = normalize1 t2⟧
    ⟹ rank (rev r1) ≤ rank (rev (root t1))"
  using normalize1_uneq_if_contr by fastforce

lemma normalize_sorted_ranks:
  "⟦is_subtree (Node r {|(t1,e1)|}) (normalize t)⟧ ⟹ rank (rev r) ≤ rank (rev (root t1))"
using ranked_dtree_axioms proof(induction t rule: normalize.induct)
  case (1 t)
  then interpret T: ranked_dtree t by blast
  show ?case
    using 1 sorted_ranks_if_normalize1_eq[OF T.wf_arcs]
    by (smt (verit, ccfv_SIG) T.ranked_dtree_normalize1 normalize.simps)
qed

lift_definition cmp'' :: "('a list×'b) comparator" is
  "(λx y. if rank (rev (fst x)) < rank (rev (fst y)) then Less
    else if rank (rev (fst x)) > rank (rev (fst y)) then Greater
    else Equiv)"
  by (simp add: comparator_def)

lemma dtree_to_list_sorted_if_no_contr:
  "⟦⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) t2 ⟹ rank (rev r1) ≤ rank (rev (root t1))⟧
    ⟹ sorted cmp'' (dtree_to_list (Node r {|(t2,e2)|}))"
proof(induction cmp'' "dtree_to_list (Node r {|(t2,e2)|})" arbitrary: r t2 e2 rule: sorted.induct)
  case (2 x)
  then show ?case using sorted_single[of cmp'' x] by simp
next
  case (3 y x xs)
  then obtain r1 t1 e1 where r1_def: "t2 = Node r1 {|(t1,e1)|}"
    using dtree_to_list.elims[of t2] by fastforce
  have "y = (root t2,e2)" using "3.hyps"(2) r1_def by simp
  moreover have "x = (root t1,e1)" using "3.hyps"(2) r1_def by simp
  moreover have "rank (rev (root t2)) ≤ rank (rev (root t1))" using "3.prems" r1_def by auto
  ultimately have "compare cmp'' y x ≠ Greater" using cmp''.rep_eq by simp
  moreover have "sorted cmp'' (dtree_to_list t2)" using 3 r1_def by auto
  ultimately show ?case using 3 r1_def by simp
qed(simp)

lemma dtree_to_list_sorted_if_no_contr':
  "⟦⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) t2 ⟹ rank (rev r1) ≤ rank (rev (root t1))⟧
    ⟹ sorted cmp'' (dtree_to_list t2)"
  using dtree_to_list_sorted_if_no_contr[of t2] sorted_Cons_imp_sorted by fastforce

lemma dtree_to_list_sorted_if_subtree:
  "⟦is_subtree t1 t2;
    ⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) t2 ⟹ rank (rev r1) ≤ rank (rev (root t1))⟧
    ⟹ sorted cmp'' (dtree_to_list (Node r {|(t1,e1)|}))"
  using dtree_to_list_sorted_if_no_contr subtree_trans by blast

lemma dtree_to_list_sorted_if_subtree':
  "⟦is_subtree t1 t2;
    ⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) t2 ⟹ rank (rev r1) ≤ rank (rev (root t1))⟧
    ⟹ sorted cmp'' (dtree_to_list t1)"
  using dtree_to_list_sorted_if_no_contr' subtree_trans by blast

lemma normalize_dtree_to_list_sorted:
  "is_subtree t1 (normalize t) ⟹ sorted cmp'' (dtree_to_list (Node r {|(t1,e1)|}))"
  using dtree_to_list_sorted_if_subtree normalize_sorted_ranks by blast

lemma normalize_dtree_to_list_sorted':
  "is_subtree t1 (normalize t) ⟹ sorted cmp'' (dtree_to_list t1)"
  using dtree_to_list_sorted_if_subtree' normalize_sorted_ranks by blast

lemma gt_if_rank_contr: "rank (rev r0) < rank (rev r) ⟹ compare cmp'' (r, e) (r0, e0) = Greater"
  by (auto simp: cmp''.rep_eq)

lemma rank_le_if_ngt: "compare cmp'' (r, e) (r0, e0) ≠ Greater ⟹ rank (rev r) ≤ rank (rev r0)"
  using gt_if_rank_contr by force

lemma rank_le_if_sorted_from_list:
  assumes "sorted cmp'' ((v1,e1)#ys)" and "is_subtree (Node r0 {|(t0,e0)|}) (dtree_from_list v1 ys)"
  shows "rank (rev r0) ≤ rank (rev (root t0))"
proof -
  obtain e as bs where e_def: "as @ (r0, e) # (root t0, e0) # bs = ((v1,e1)#ys)"
    using dtree_from_list_sequence[OF assms(2)] by blast
  then have "sorted cmp'' (as @ (r0, e) # (root t0, e0) # bs)" using assms(1) by simp
  then have "sorted cmp'' ((r0, e) # (root t0, e0) # bs)" using sorted_app_r by blast
  then show ?thesis using rank_le_if_ngt by auto
qed

lemma cmp'_gt_if_cmp''_gt: "compare cmp'' x y = Greater ⟹ compare cmp' x y = Greater"
  by (auto simp: cmp'.rep_eq cmp''.rep_eq split: if_splits)

lemma cmp'_lt_if_cmp''_lt: "compare cmp'' x y = Less ⟹ compare cmp' x y = Less"
  by (auto simp: cmp'.rep_eq cmp''.rep_eq)

lemma cmp''_ge_if_cmp'_gt:
  "compare cmp' x y = Greater ⟹ compare cmp'' x y = Greater ∨ compare cmp'' x y = Equiv"
  by (auto simp: cmp'.rep_eq cmp''.rep_eq split: if_splits)

lemma cmp''_nlt_if_cmp'_gt: "compare cmp' x y = Greater ⟹ compare cmp'' y x ≠ Greater"
  by (auto simp: cmp'.rep_eq cmp''.rep_eq)

interpretation Comm: comp_fun_commute "merge_f r xs" by (rule merge_commute)

lemma sorted_cmp''_merge:
  "⟦sorted cmp'' xs; sorted cmp'' ys⟧ ⟹ sorted cmp'' (Sorting_Algorithms.merge cmp' xs ys)"
proof(induction xs ys taking: cmp' rule: Sorting_Algorithms.merge.induct)
  case (3 x xs y ys)
  let ?merge = "Sorting_Algorithms.merge cmp'"
  show ?case
  proof(cases "compare cmp' x y = Greater")
    case True
    have "?merge (x # xs) (y#ys) = y # (?merge (x # xs) ys)" using True by simp
    moreover have "sorted cmp'' (?merge (x # xs) ys)" using 3 True sorted_Cons_imp_sorted by fast
    ultimately show ?thesis
      using cmp''_nlt_if_cmp'_gt[OF True] "3.prems" sorted_rec[of cmp'' y]
        merge.elims[of cmp' "x#xs" ys "?merge (x # xs) ys"]
      by metis
  next
    case False
    have "?merge (x#xs) (y#ys) = x # (?merge xs (y#ys))" using False by simp
    moreover have "sorted cmp'' (?merge xs (y#ys))" using 3 False sorted_Cons_imp_sorted by fast
    ultimately show ?thesis
      using cmp'_gt_if_cmp''_gt False "3.prems" sorted_rec[of cmp'' x]
        merge.elims[of cmp' xs "y#ys" "?merge xs (y#ys)"]
      by metis
  qed
qed(auto)

lemma merge_ffold_sorted:
  "⟦list_dtree (Node r xs); ⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1,e1)|}) t2⟧
    ⟹ rank (rev r1) ≤ rank (rev (root t1))⟧
    ⟹ sorted cmp'' (ffold (merge_f r xs) [] xs)"
proof(induction xs)
  case (insert x xs)
  interpret Comm: comp_fun_commute "merge_f r (finsert x xs)" by (rule merge_commute)
  define f where "f = merge_f r (finsert x xs)"
  define f' where "f' = merge_f r xs"
  let ?merge = "Sorting_Algorithms.merge cmp'"
  have 0: "list_dtree (Node r xs)" using list_dtree_subset insert.prems(1) by blast
  obtain t2 e2 where t2_def[simp]: "x = (t2,e2)" by fastforce
  have ind1: "sorted cmp'' (dtree_to_list (Node r {|(t2,e2)|}))"
    using dtree_to_list_sorted_if_no_contr insert.prems(2) by fastforce
  have "⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1, e1)|}) t2⟧
        ⟹ rank (rev r1) ≤ rank (rev (root t1))"
    using insert.prems(2) by fastforce
  then have ind2: "sorted cmp'' (ffold f' [] xs)" using insert.IH[OF 0] f'_def by blast
  have "(t2, e2) ∈ fset (finsert x xs)" by simp
  moreover have "(t2, e2) ∉ fset xs" using insert.hyps by fastforce
  ultimately have xs_val:
    "(∀(v,e) ∈ set (ffold f' [] xs). set v ∩ dlverts t2 = {} ∧ v ≠ [] ∧ e ∉ darcs t2 ∪ {e2})"
    using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge] f'_def
    by blast
  have "ffold f [] (finsert x xs) = f x (ffold f [] xs)"
    using Comm.ffold_finsert[OF insert.hyps] f_def by blast
  also have "… = f x (ffold f' [] xs)"
    using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1) f_def f'_def by fastforce
  finally have "ffold f [] (finsert x xs) = ?merge (dtree_to_list (Node r {|x|})) (ffold f' [] xs)"
    using xs_val insert.prems f_def by simp
  then have merge: "ffold f [] (finsert x xs)
              = ?merge (dtree_to_list (Node r {|(t2,e2)|})) (ffold f'[] xs)"
    using t2_def by blast
  then show ?case using sorted_cmp''_merge[OF ind1 ind2] f_def by auto
qed (simp add: ffold.rep_eq)

lemma not_single_subtree_if_nwf:
  "¬list_dtree (Node r xs) ⟹ ¬is_subtree (Node r1 {|(t1,e1)|}) (merge (Node r xs))"
  using merge_empty_if_nwf by simp

lemma not_single_subtree_if_nwf_sucs:
  "¬list_dtree t2 ⟹ ¬is_subtree (Node r1 {|(t1,e1)|}) (merge t2)"
  using merge_empty_if_nwf_sucs by simp

lemma merge_strict_subtree_nocontr:
  assumes "⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1,e1)|}) t2⟧
            ⟹ rank (rev r1) ≤ rank (rev (root t1))"
      and "strict_subtree (Node r1 {|(t1,e1)|}) (merge (Node r xs))"
    shows "rank (rev r1) ≤ rank (rev (root t1))"
proof(cases "list_dtree (Node r xs)")
  case True
  obtain e as bs where e_def: "as @ (r1, e) # (root t1, e1) # bs = ffold (merge_f r xs) [] xs"
    using dtree_from_list_uneq_sequence assms(2) unfolding merge_def dtree.sel strict_subtree_def
    by fast
  have "sorted cmp'' (ffold (merge_f r xs) [] xs)"
    using merge_ffold_sorted[OF True assms(1)] by simp
  then have "sorted cmp'' ((r1, e) # (root t1, e1) # bs)"
    using e_def sorted_app_r[of cmp'' as "(r1, e) # (root t1, e1) # bs"] by simp
  then show ?thesis using rank_le_if_sorted_from_list by fastforce
next
  case False
  then show ?thesis using not_single_subtree_if_nwf assms(2) by (simp add: strict_subtree_def)
qed

lemma merge_strict_subtree_nocontr2:
  assumes "⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) (Node r xs)
            ⟹ rank (rev r1) ≤ rank (rev (root t1))"
      and "strict_subtree (Node r1 {|(t1,e1)|}) (merge (Node r xs))"
    shows "rank (rev r1) ≤ rank (rev (root t1))"
  using merge_strict_subtree_nocontr[OF assms] by fastforce

lemma merge_strict_subtree_nocontr_sucs:
  assumes "⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset (sucs t0); is_subtree (Node r1 {|(t1,e1)|}) t2⟧
            ⟹ rank (rev r1) ≤ rank (rev (root t1))"
      and "strict_subtree (Node r1 {|(t1,e1)|}) (merge t0)"
    shows "rank (rev r1) ≤ rank (rev (root t1))"
  using merge_strict_subtree_nocontr[of "sucs t0" r1 t1 e1 "root t0"] assms by simp

lemma merge_strict_subtree_nocontr_sucs2:
  assumes "⋀r1 t1 e1. is_subtree (Node r1 {|(t1,e1)|}) t2 ⟹ rank (rev r1) ≤ rank (rev (root t1))"
      and "strict_subtree (Node r1 {|(t1,e1)|}) (merge t2)"
    shows "rank (rev r1) ≤ rank (rev (root t1))"
  using merge_strict_subtree_nocontr2[of "root t2" "sucs t2"] assms by auto

lemma no_contr_imp_parent:
  "⟦is_subtree (Node r1 {|(t1,e1)|}) (Node r xs) ⟹ rank (rev r1) ≤ rank (rev (root t1));
    t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1,e1)|}) t2⟧
      ⟹ rank (rev r1) ≤ rank (rev (root t1))"
  using subtree_if_child subtree_trans by fast

lemma no_contr_imp_subtree:
  "⟦⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1,e1)|}) t2⟧
      ⟹ rank (rev r1) ≤ rank (rev (root t1));
    is_subtree (Node r1 {|(t1,e1)|}) (Node r xs); ∀x. xs ≠ {|x|}⟧
    ⟹ rank (rev r1) ≤ rank (rev (root t1))"
  by fastforce

lemma no_contr_imp_subtree_fcard:
  "⟦⋀t2 r1 t1 e1. ⟦t2 ∈ fst ` fset xs; is_subtree (Node r1 {|(t1,e1)|}) t2⟧
      ⟹ rank (rev r1) ≤ rank (rev (root t1));
    is_subtree (Node r1 {|(t1,e1)|}) (Node r xs); fcard xs ≠ 1⟧
    ⟹ rank (rev r1) ≤ rank (rev (root t1))"
  using fcard_single_1_iff[of xs] by fastforce

end

subsection ‹Removing Wedges›

context ranked_dtree
begin

fun merge1 :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "merge1 (Node r xs) = (
    if fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1) then merge (Node r xs)
    else Node r ((λ(t,e). (merge1 t,e)) |`| xs))"

lemma merge1_dverts_eq[simp]: "dverts (merge1 t) = dverts t"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis using Node.IH R.ranked_dtree_rec by auto
  qed
qed

lemma merge1_dlverts_eq[simp]: "dlverts (merge1 t) = dlverts t"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis using Node.IH R.ranked_dtree_rec by auto
  qed
qed

lemma dverts_merge1_img_sub:
  "∀(t2,e2) ∈ fset xs. dverts (merge1 t2) ⊆ dverts t2
    ⟹ dverts (Node r ((λ(t,e). (merge1 t,e)) |`| xs)) ⊆ dverts (Node r xs)"
  by fastforce

lemma merge1_dverts_sub: "dverts (merge1 t1) ⊆ dverts t1"
proof(induction t1)
  case (Node r xs)
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis using dverts_merge_sub by force
  next
    case False
    then have "∀(t2,e2) ∈ fset xs. dverts (merge1 t2) ⊆ dverts t2" using Node by fastforce
    then show ?thesis using False dverts_merge1_img_sub by auto
  qed
qed

lemma disjoint_dlverts_merge1: "disjoint_dlverts ((λ(t,e). (merge1 t,e)) |`| (sucs t))"
proof -
  have "∀(t, e)∈fset (sucs t). dlverts (merge1 t) ⊆ dlverts t"
    using ranked_dtree.merge1_dlverts_eq ranked_dtree_rec[of "root t"] by force
  then show ?thesis using disjoint_dlverts_img[OF disjoint_dlverts_if_wf[OF wf_lverts]] by simp
qed

lemma root_empty_inter_dlverts_merge1:
  assumes "(x1,e1) ∈ fset  ((λ(t,e). (merge1 t,e)) |`| (sucs t))"
  shows "set (root t) ∩ dlverts x1 = {}"
proof (rule ccontr)
  assume asm: "set (root t) ∩ dlverts x1 ≠ {}"
  obtain x2 where x2_def: "merge1 x2 = x1" "(x2,e1) ∈ fset (sucs t)" using assms by auto
  then interpret X: ranked_dtree x2 using ranked_dtree_rec dtree.collapse by blast
  have "set (root t) ∩ dlverts x2 ≠ {}" using X.merge1_dlverts_eq x2_def(1) asm by argo
  then show False using x2_def(2) wf_lverts wf_dlverts.simps[of "root t" "sucs t"] by auto
qed

lemma wf_dlverts_merge1: "wf_dlverts (merge1 t)"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis using R.merge_wf_dlverts by simp
  next
    case False
    have "(∀(t,e) ∈ fset ((λ(t,e). (merge1 t,e)) |`| xs). set r ∩ dlverts t = {} ∧ wf_dlverts t)"
      using R.ranked_dtree_rec Node.IH R.root_empty_inter_dlverts_merge1 by fastforce
    then show ?thesis using R.disjoint_dlverts_merge1 R.wf_lverts False by auto
  qed
qed

lemma merge1_darcs_eq[simp]: "darcs (merge1 t) = darcs t"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case using Node.IH R.ranked_dtree_rec by auto
qed

lemma disjoint_darcs_merge1: "disjoint_darcs ((λ(t,e). (merge1 t,e)) |`| (sucs t))"
proof -
  have "∀(t, e)∈fset (sucs t). darcs (merge1 t) ⊆ darcs t"
    using ranked_dtree.merge1_darcs_eq ranked_dtree_rec[of "root t"] by force
  then show ?thesis using disjoint_darcs_img[OF disjoint_darcs_if_wf[OF wf_arcs]] by simp
qed

lemma wf_darcs_merge1: "wf_darcs (merge1 t)"
using ranked_dtree_axioms proof(induction t)
  case (Node r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis using R.merge_wf_darcs by simp
  next
    case False
    then show ?thesis
      using R.disjoint_darcs_merge1 R.ranked_dtree_rec Node.IH
      by (auto simp: wf_darcs_iff_darcs')
  qed
qed

theorem ranked_dtree_merge1: "ranked_dtree (merge1 t) cmp"
  by(unfold_locales) (auto simp: wf_darcs_merge1 wf_dlverts_merge1 dest: cmp_antisym)

lemma distinct_merge1:
  "⟦∀v∈dverts t. distinct v; v∈dverts (merge1 t)⟧ ⟹ distinct v"
using ranked_dtree_axioms proof(induction t arbitrary: v rule: merge1.induct)
  case (1 r xs)
  then interpret R: ranked_dtree "Node r xs" rank by blast
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis using R.distinct_merge[OF "1.prems"(1)] "1.prems"(2) by simp
  next
    case ind: False
    then show ?thesis
    proof(cases "v = r")
      case False
      have "v∈dverts (merge1 (Node r xs)) ⟷ v ∈ dverts (Node r ((λ(t,e). (merge1 t,e)) |`| xs))"
        using ind by auto
      then obtain t e where t_def: "(t,e) ∈ fset xs" "v ∈ dverts (merge1 t)"
        using False "1.prems"(2) by auto
      then have "∀v∈dverts t. distinct v" using "1.prems"(1) by force
      then show ?thesis using "1.IH"[OF ind] t_def R.ranked_dtree_rec by fast
    qed(simp add: "1.prems"(1))
  qed
qed

lemma merge1_root_eq[simp]: "root (merge1 t1) = root t1"
  by(induction t1) simp

lemma merge1_hd_root_eq[simp]: "hd (root (merge1 t1)) = hd (root t1)"
  by simp

lemma merge1_mdeg_le: "max_deg (merge1 t1) ≤ max_deg t1"
proof(induction t1)
  case (Node r xs)
  then show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then have "max_deg (merge1 (Node r xs)) ≤ 1" using merge_mdeg_le_1 by simp
    then show ?thesis using mdeg_ge_fcard[of xs] True by simp
  next
    case False
    have 0: "∀(t,e) ∈ fset xs. max_deg (merge1 t) ≤ max_deg t" using Node by force
    have "merge1 (Node r xs) = (Node r ((λ(t, e). (merge1 t, e)) |`| xs))"
      using False by auto
    then show ?thesis using mdeg_img_le'[OF 0] by simp
  qed
qed

lemma merge1_childdeg_gt1_if_fcard_gt1:
  "fcard (sucs (merge1 t1)) > 1 ⟹ ∃t ∈ fst ` fset (sucs t1). max_deg t > 1"
proof(induction t1)
  case (Node r xs)
  have 0: "¬(fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1))"
      using merge_fcard_le1[of "Node r xs"] Node.prems(1) by fastforce
  then have "fcard (sucs (merge1 (Node r xs))) ≤ fcard xs" using fcard_image_le by auto
  then show ?case using 0 Node.prems(1) by fastforce
qed

lemma merge1_fcard_le: "fcard (sucs (merge1 (Node r xs))) ≤ fcard xs"
  using fcard_image_le merge_fcard_le1[of "Node r xs"] by auto

lemma merge1_subtree_if_fcard_gt1:
  "⟦is_subtree (Node r xs) (merge1 t1); fcard xs > 1⟧
    ⟹ ∃ys. merge1 (Node r ys) = Node r xs ∧ is_subtree (Node r ys) t1 ∧ fcard xs ≤ fcard ys"
proof(induction t1)
  case (Node r1 xs1)
  have 0: "¬(fcard xs1 > 1 ∧ (∀t ∈ fst ` fset xs1. max_deg t ≤ 1))"
    using merge_fcard_le1_sub Node.prems by fastforce
  then have eq: "merge1 (Node r1 xs1) = Node r1 ((λ(t,e). (merge1 t,e)) |`| xs1)" by auto
  show ?case
  proof(cases "Node r xs = merge1 (Node r1 xs1)")
    case True
    moreover have "r = r1" using True eq by auto
    moreover have "fcard xs ≤ fcard xs1" using merge1_fcard_le True dtree.sel(2)[of r xs] by auto
    ultimately show ?thesis using self_subtree Node.prems(2) by auto
  next
    case False
    then obtain t2 e2 where "(t2,e2) ∈ fset xs1" "is_subtree (Node r xs) (merge1 t2)"
      using eq Node.prems(1) by auto
    then show ?thesis using Node.IH[of "(t2,e2)" t2] Node.prems(2) by fastforce
  qed
qed

lemma merge1_childdeg_gt1_if_fcard_gt1_sub:
  "⟦is_subtree (Node r xs) (merge1 t1); fcard xs > 1⟧
    ⟹ ∃ys. merge1 (Node r ys) = Node r xs ∧ is_subtree (Node r ys) t1
          ∧ (∃t ∈ fst ` fset ys. max_deg t > 1)"
  using merge1_subtree_if_fcard_gt1 merge1_childdeg_gt1_if_fcard_gt1 dtree.sel(2) by metis

lemma merge1_img_eq: "∀(t2,e2) ∈ fset xs. merge1 t2 = t2 ⟹ ((λ(t,e). (merge1 t,e)) |`| xs) = xs"
  using fset_img_eq[of xs "λ(t,e). (merge1 t,e)"] by force

lemma merge1_wedge_if_uneq:
  "merge1 t1 ≠ t1
    ⟹ ∃r xs. is_subtree (Node r xs) t1 ∧ fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)"
proof(induction t1)
  case (Node r xs)
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then show ?thesis by auto
  next
    case False
    then have "merge1 (Node r xs) = Node r ((λ(t,e). (merge1 t,e)) |`| xs)" by auto
    then obtain t2 e2 where "(t2,e2) ∈ fset xs" "merge1 t2 ≠ t2"
      using Node.prems merge1_img_eq[of xs] by auto
    then show ?thesis using Node.IH[of "(t2,e2)"] by auto
  qed
qed

lemma merge1_mdeg_gt1_if_uneq:
  assumes "merge1 t1 ≠ t1"
  shows "max_deg t1 > 1"
proof -
  obtain r xs where r_def: "is_subtree (Node r xs) t1" "1 < fcard xs"
    using merge1_wedge_if_uneq[OF assms] by fast
  then show ?thesis using mdeg_ge_fcard[of xs] mdeg_ge_sub by force
qed

corollary merge1_eq_if_mdeg_le1: "max_deg t1 ≤ 1 ⟹ merge1 t1 = t1"
  using merge1_mdeg_gt1_if_uneq by fastforce

lemma merge1_not_merge_if_fcard_gt1:
  "⟦merge1 (Node r ys) = Node r xs; fcard xs > 1⟧ ⟹ merge (Node r ys) ≠ Node r xs"
  using merge_fcard_le1[of "Node r ys"] by auto

lemma merge1_img_if_not_merge:
  "merge1 (Node r xs) ≠ merge (Node r xs)
    ⟹ merge1 (Node r xs) = Node r ((λ(t,e). (merge1 t,e)) |`| xs)"
  by auto

lemma merge1_img_if_fcard_gt1:
  "⟦merge1 (Node r ys) = Node r xs; fcard xs > 1⟧
    ⟹ merge1 (Node r ys) = Node r ((λ(t,e). (merge1 t,e)) |`| ys)"
  using merge1_img_if_not_merge merge1_not_merge_if_fcard_gt1[of r ys] by simp

lemma merge1_elem_in_img_if_fcard_gt1:
  "⟦merge1 (Node r ys) = Node r xs; fcard xs > 1; (t2,e2) ∈ fset xs⟧
    ⟹ ∃t1. (t1,e2) ∈ fset ys ∧ merge1 t1 = t2"
  using merge1_img_if_fcard_gt1 by fastforce

lemma child_mdeg_gt1_if_sub_fcard_gt1:
  "⟦is_subtree (Node r xs) (Node v ys); Node r xs ≠ Node v ys; fcard xs > 1⟧
    ⟹ ∃t1 e2. (t1,e2) ∈ fset ys ∧ max_deg t1 > 1"
  using mdeg_ge_fcard[of xs] mdeg_ge_sub by force

lemma merge1_subtree_if_mdeg_gt1:
  "⟦is_subtree (Node r xs) (merge1 t1); max_deg (Node r xs) > 1⟧
    ⟹ ∃ys. merge1 (Node r ys) = Node r xs ∧ is_subtree (Node r ys) t1"
proof(induction t1)
  case (Node r1 xs1)
  then have 0: "¬(fcard xs1 > 1 ∧ (∀t ∈ fst ` fset xs1. max_deg t ≤ 1))"
    using merge_mdeg_le1_sub by fastforce
  then have eq: "merge1 (Node r1 xs1) = Node r1 ((λ(t,e). (merge1 t,e)) |`| xs1)" by auto
  show ?case
  proof(cases "Node r xs = merge1 (Node r1 xs1)")
    case True
    moreover have "r = r1" using True eq by auto
    moreover have "fcard xs ≤ fcard xs1" using merge1_fcard_le True dtree.sel(2)[of r xs] by auto
    ultimately show ?thesis using self_subtree Node.prems(2) by auto
  next
    case False
    then obtain t2 e2 where "(t2,e2) ∈ fset xs1" "is_subtree (Node r xs) (merge1 t2)"
      using eq Node.prems(1) by auto
    then show ?thesis using Node.IH[of "(t2,e2)" t2] Node.prems(2) by fastforce
  qed
qed

lemma merge1_child_in_orig:
  assumes "merge1 (Node r ys) = Node r xs" and "(t1,e1) ∈ fset xs"
  shows "∃t2. (t2,e1) ∈ fset ys ∧ root t2 = root t1"
proof(cases "fcard ys > 1 ∧ (∀t ∈ fst ` fset ys. max_deg t ≤ 1)")
  case True
  then show ?thesis using merge_child_in_orig[of t1 e1 "Node r ys"] assms by auto
next
  case False
  then have "merge1 (Node r ys) = Node r ((λ(t,e). (merge1 t,e)) |`| ys)" by auto
  then show ?thesis using assms by fastforce
qed

lemma dverts_if_subtree_merge1:
  "is_subtree (Node r xs) (merge1 t1) ⟹ r ∈ dverts t1"
  using merge1_dverts_sub dverts_subtree_subset by fastforce

lemma subtree_merge1_orig:
  "is_subtree (Node r xs) (merge1 t1) ⟹ ∃ys. is_subtree (Node r ys) t1"
  using dverts_if_subtree_merge1 subtree_root_if_dverts by fast

lemma merge1_subtree_dlverts_supset:
  "is_subtree (Node r xs) (merge1 t)
    ⟹ ∃ys. is_subtree (Node r ys) t ∧ dlverts (Node r ys) ⊆ dlverts (Node r xs)"
using ranked_dtree_axioms proof(induction t)
  case (Node r1 xs1)
  then interpret R: ranked_dtree "Node r1 xs1" by simp
  show ?case
  proof(cases "Node r xs = merge1 (Node r1 xs1)")
    case True
    then have "dlverts (Node r1 xs1) ⊆ dlverts (Node r xs)" using R.merge1_dlverts_eq by simp
    moreover have "r = r1" using True dtree.sel(1)[of r xs] by auto
    ultimately show ?thesis by auto
  next
    case uneq: False
    show ?thesis
    proof(cases "fcard xs1 > 1 ∧ (∀t ∈ fst ` fset xs1. max_deg t ≤ 1)")
      case True
      then show ?thesis using R.merge_subtree_dlverts_supset Node.prems by simp
    next
      case False
      then have eq: "merge1 (Node r1 xs1) = Node r1 ((λ(t,e). (merge1 t,e)) |`| xs1)" by auto
      then obtain t2 e2 where "(t2,e2) ∈ fset xs1" "is_subtree (Node r xs) (merge1 t2)"
        using Node.prems(1) uneq by auto
      then show ?thesis using Node.IH[of "(t2,e2)"] R.ranked_dtree_rec by auto
    qed
  qed
qed

end

subsection ‹IKKBZ-Sub›

function denormalize :: "('a list, 'b) dtree ⇒ 'a list" where
  "denormalize (Node r {|(t,e)|}) = r @ denormalize t"
| "∀x. xs ≠ {|x|} ⟹ denormalize (Node r xs) = r"
  using dtree_to_list.cases by blast+
termination by lexicographic_order

lemma denormalize_set_eq_dlverts: "max_deg t1 ≤ 1 ⟹ set (denormalize t1) = dlverts t1"
proof(induction t1 rule: denormalize.induct)
  case (1 r t e)
  then show ?case using mdeg_ge_child[of t e "{|(t, e)|}"] by force
next
  case (2 xs r)
  then have "max_deg (Node r xs) = 0" using mdeg_1_singleton[of r xs] by fastforce
  then have "xs = {||}" by (auto intro!: empty_if_mdeg_0)
  then show ?case using 2 by auto
qed

lemma denormalize_set_sub_dlverts: "set (denormalize t1) ⊆ dlverts t1"
  by(induction t1 rule: denormalize.induct) auto

lemma denormalize_distinct:
  "⟦∀v ∈ dverts t1. distinct v; wf_dlverts t1⟧ ⟹ distinct (denormalize t1)"
proof(induction t1 rule: denormalize.induct)
  case (1 r t e)
  then have "set r ∩ set (denormalize t) = {}" using denormalize_set_sub_dlverts by fastforce
  then show ?case using 1 by auto
next
  case (2 xs r)
  then show ?case by simp
qed

lemma denormalize_hd_root:
  assumes "root t ≠ []"
  shows "hd (denormalize t) = hd (root t)"
proof(cases "∀x. sucs t ≠ {|x|}")
  case True
  then show ?thesis using denormalize.simps(2)[of "sucs t" "root t"] by simp
next
  case False
  then obtain t1 e where "{|(t1, e)|} = sucs t" by auto
  then show ?thesis using denormalize.simps(1)[of "root t" t1 e] assms by simp
qed

lemma denormalize_hd_root_wf: "wf_dlverts t ⟹ hd (denormalize t) = hd (root t)"
  using denormalize_hd_root empty_notin_wf_dlverts dtree.set_sel(1)[of t] by force

lemma denormalize_nempty_if_wf: "wf_dlverts t ⟹ denormalize t ≠ []"
  by (induction t rule: denormalize.induct) auto

context ranked_dtree
begin

lemma fcard_normalize_img_if_disjoint:
  "disjoint_darcs xs ⟹ fcard ((λ(t,e). (normalize1 t,e)) |`| xs) = fcard xs"
  using snds_neq_img_card_eq[of xs] by fast

lemma fcard_merge1_img_if_disjoint:
  "disjoint_darcs xs ⟹ fcard ((λ(t,e). (merge1 t,e)) |`| xs) = fcard xs"
  using snds_neq_img_card_eq[of xs] by fast

lemma fsts_uneq_if_disjoint_lverts_nempty:
  "⟦disjoint_dlverts xs; ∀(t, e)∈fset xs. dlverts t ≠ {}⟧
    ⟹ ∀(t, e)∈fset xs. ∀(t2, e2)∈fset xs. t ≠ t2 ∨ (t, e) = (t2, e2)"
  by fast

lemma normalize1_dlverts_nempty:
  "∀(t, e)∈fset xs. dlverts t ≠ {}
    ⟹ ∀(t, e)∈fset ((λ(t, e). (normalize1 t, e)) |`| xs). dlverts t ≠ {}"
  by auto

lemma normalize1_fsts_uneq:
  assumes "disjoint_dlverts xs" and "∀(t, e)∈fset xs. dlverts t ≠ {}"
  shows "∀(t, e)∈fset xs. ∀(t2, e2)∈fset xs. normalize1 t ≠ normalize1 t2 ∨ (t,e) = (t2,e2)"
  by (smt (verit) assms Int_absorb case_prodD case_prodI2 normalize1_dlverts_eq)

lemma fcard_normalize_img_if_disjoint_lverts:
  "⟦disjoint_dlverts xs; ∀(t, e)∈fset xs. dlverts t ≠ {}⟧
    ⟹ fcard ((λ(t,e). (normalize1 t,e)) |`| xs) = fcard xs"
  using fst_neq_img_card_eq[of xs normalize1] normalize1_fsts_uneq by auto

lemma fcard_normalize_img_if_wf_dlverts:
  "wf_dlverts (Node r xs) ⟹ fcard ((λ(t,e). (normalize1 t,e)) |`| xs) = fcard xs"
  using dlverts_nempty_if_wf fcard_normalize_img_if_disjoint_lverts[of xs] by force

lemma fcard_normalize_img_if_wf_dlverts_sucs:
  "wf_dlverts t1 ⟹ fcard ((λ(t,e). (normalize1 t,e)) |`| (sucs t1)) = fcard (sucs t1)"
  using fcard_normalize_img_if_wf_dlverts[of "root t1" "sucs t1"] by simp

lemma singleton_normalize1:
  assumes "disjoint_darcs xs" and "∀x. xs ≠ {|x|}"
  shows "∀x. (λ(t,e). (normalize1 t,e)) |`| xs ≠ {|x|}"
proof (rule ccontr)
  assume "¬(∀x. (λ(t,e). (normalize1 t,e)) |`| xs ≠ {|x|})"
  then obtain x where "(λ(t,e). (normalize1 t,e)) |`| xs = {|x|}" by blast
  then have "fcard ((λ(t,e). (normalize1 t,e)) |`| xs) = 1" using fcard_single_1 by force
  then have "fcard xs = 1" using fcard_normalize_img_if_disjoint[OF assms(1)] by simp
  then have "∃x. xs = {|x|}" using fcard_single_1_iff by fast
  then show False using assms(2) by simp
qed

lemma num_leaves_normalize1_eq[simp]: "wf_darcs t1 ⟹ num_leaves (normalize1 t1) = num_leaves t1"
proof(induction t1)
  case (Node r xs)
  then show ?case
  proof(cases "∀x. xs ≠ {|x|}")
    case True
    have "fcard ((λ(t,e). (normalize1 t,e)) |`| xs) = fcard xs"
      using fcard_normalize_img_if_disjoint Node.prems
      by (auto simp: wf_darcs_iff_darcs')
    moreover have "∀t∈fst ` fset xs. num_leaves (normalize1 t) = num_leaves t"
      using Node by fastforce
    ultimately show ?thesis using Node sum_img_eq[of xs] True by force
  next
    case False
    then obtain t e where t_def: "xs = {|(t,e)|}" by auto
    show ?thesis
    proof(cases "rank (rev (root t)) < rank (rev r)")
      case True
      then show ?thesis
        using t_def num_leaves_singleton num_leaves_root[of "root t" "sucs t"] by simp
    next
      case False
      then show ?thesis
        using num_leaves_singleton t_def Node by (simp add: wf_darcs_iff_darcs')
    qed
  qed
qed

lemma num_leaves_normalize_eq[simp]: "wf_darcs t1 ⟹ num_leaves (normalize t1) = num_leaves t1"
proof(induction t1 rule: normalize.induct)
  case (1 t)
  then have "num_leaves (normalize1 t) = num_leaves t" using num_leaves_normalize1_eq by blast
  then show ?case using 1 wf_darcs_normalize1 by (smt (verit, best) normalize.simps)
qed

lemma num_leaves_normalize1_le: "num_leaves (normalize1 t1) ≤ num_leaves t1"
proof(induction t1)
  case (Node r xs)
  then show ?case
  proof(cases "∀x. xs ≠ {|x|}")
    case True
    have fcard_le: "fcard ((λ(t,e). (normalize1 t,e)) |`| xs) ≤ fcard xs"
      by (simp add: fcard_image_le)
    moreover have xs_le: "∀t∈fst ` fset xs. num_leaves (normalize1 t) ≤ num_leaves t"
      using Node by fastforce
    ultimately show ?thesis using Node sum_img_le[of xs] xs_le ‹∀x. xs ≠ {|x|}› by simp
  next
    case False
    then obtain t e where t_def: "xs = {|(t,e)|}" by auto
    show ?thesis
    proof(cases "rank (rev (root t)) < rank (rev r)")
      case True
      then show ?thesis
        using t_def num_leaves_singleton num_leaves_root[of "root t" "sucs t"] by simp
    next
      case False
      then show ?thesis using num_leaves_singleton t_def Node by simp
    qed
  qed
qed

lemma num_leaves_normalize_le: "num_leaves (normalize t1) ≤ num_leaves t1"
proof(induction t1 rule: normalize.induct)
  case (1 t)
  then have "num_leaves (normalize1 t) ≤ num_leaves t" using num_leaves_normalize1_le by blast
  then show ?case using 1 by (smt (verit) le_trans normalize.simps)
qed

lemma num_leaves_merge1_le: "num_leaves (merge1 t1) ≤ num_leaves t1"
proof(induction t1)
  case (Node r xs)
  then show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then have "merge1 (Node r xs) = merge (Node r xs)" by simp
    then have "num_leaves (merge1 (Node r xs)) = 1"
      unfolding merge_def using dtree_from_list_1_leaf by fastforce
    also have "… < fcard xs" using True by blast
    also have "… ≤ num_leaves (Node r xs)" using num_leaves_ge_card by fast
    finally show ?thesis by simp
  next
    case False
    have "∀t ∈ fst ` fset xs. num_leaves (merge1 t) ≤ num_leaves t" using Node by force
    then show ?thesis using sum_img_le False by auto
  qed
qed

lemma num_leaves_merge1_lt: "max_deg t1 > 1 ⟹ num_leaves (merge1 t1) < num_leaves t1"
proof(induction t1)
  case (Node r xs)
  show ?case
  proof(cases "fcard xs > 1 ∧ (∀t ∈ fst ` fset xs. max_deg t ≤ 1)")
    case True
    then have "merge1 (Node r xs) = merge (Node r xs)" by simp
    then have "num_leaves (merge1 (Node r xs)) = 1"
      unfolding merge_def using dtree_from_list_1_leaf by fastforce
    also have "… < fcard xs" using True by blast
    finally show ?thesis using num_leaves_ge_card less_le_trans by fast
  next
    case False
    have 0: "xs ≠ {||}" using Node.prems by (metis nempty_if_mdeg_n0 not_one_less_zero)
    have 1: "∀t ∈ fst ` fset xs. num_leaves (merge1 t) ≤ num_leaves t"
      using num_leaves_merge1_le by blast
    have "∃t ∈ fst ` fset xs. max_deg t > 1" using Node.prems False mdeg_child_if_wedge by auto
    then have 2: "∃t ∈ fst ` fset xs. num_leaves (merge1 t) < num_leaves t" using Node.IH by force
    have 3: "∀t∈fst ` fset xs. 0 < num_leaves t"
      using num_leaves_ge1 by (metis neq0_conv not_one_le_zero)
    from False have "merge1 (Node r xs) = Node r ((λ(t,e). (merge1 t,e)) |`| xs)" by auto
    then have "num_leaves (merge1 (Node r xs))
            = (∑(t,e)∈ fset ((λ(t,e). (merge1 t,e)) |`| xs). num_leaves t)" using 0 by auto
    then show ?thesis using 0 sum_img_lt[OF 1 2 3] by simp
  qed
qed

lemma ikkbz_num_leaves_decr:
  "max_deg t1 > 1 ⟹ num_leaves (merge1 (normalize t1)) < num_leaves t1"
  using num_leaves_merge1_lt num_leaves_normalize_le num_leaves_1_if_mdeg_1 num_leaves_ge1
  by (metis antisym_conv2 dual_order.antisym dual_order.trans not_le_imp_less num_leaves_merge1_le)

function ikkbz_sub :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "ikkbz_sub t1 = (if max_deg t1 ≤ 1 then t1 else ikkbz_sub (merge1 (normalize t1)))"
  by auto
termination using ikkbz_num_leaves_decr by(relation "measure (λt. num_leaves t)") auto

lemma ikkbz_sub_darcs_sub: "darcs (ikkbz_sub t) ⊆ darcs t"
using ranked_dtree_axioms proof(induction t rule: ikkbz_sub.induct)
  case (1 t)
  show ?case
  proof(cases "max_deg t ≤ 1")
    case False
    have "darcs (merge1 (normalize t)) = darcs (normalize t)"
      using ranked_dtree.merge1_darcs_eq ranked_dtree.ranked_dtree_normalize "1.prems" by blast
    moreover have "ranked_dtree (merge1 (normalize t)) cmp"
      using ranked_dtree.ranked_dtree_normalize "1.prems" ranked_dtree.ranked_dtree_merge1 by blast
    moreover have "¬ (max_deg t ≤ 1 ∨ ¬ list_dtree t)" using False ranked_dtree_def "1.prems" by blast
    ultimately show ?thesis using "1.IH" normalize_darcs_sub by force
  qed(simp)
qed

lemma ikkbz_sub_dlverts_eq[simp]: "dlverts (ikkbz_sub t) = dlverts t"
using ranked_dtree_axioms proof(induction t rule: ikkbz_sub.induct)
  case (1 t)
  show ?case
  proof(cases "max_deg t ≤ 1")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis
      using 1 ranked_dtree.merge1_dlverts_eq[of "normalize t"] normalize_dlverts_eq
      ranked_dtree.ranked_dtree_normalize ranked_dtree.ranked_dtree_merge1 ikkbz_sub.elims by metis
  qed
qed

lemma ikkbz_sub_wf_darcs: "wf_darcs (ikkbz_sub t)"
using ranked_dtree_axioms proof(induction t rule: ikkbz_sub.induct)
  case (1 t)
  then show ?case
  proof(cases "max_deg t ≤ 1")
    case True
    then show ?thesis using "1.prems" list_dtree_def ranked_dtree_def by auto
  next
    case False
    then show ?thesis
      using 1 ranked_dtree.ranked_dtree_normalize ranked_dtree.ranked_dtree_merge1
      by (metis ikkbz_sub.simps)
  qed
qed

lemma ikkbz_sub_wf_dlverts: "wf_dlverts (ikkbz_sub t)"
using ranked_dtree_axioms proof(induction t rule: ikkbz_sub.induct)
  case (1 t)
  then show ?case
  proof(cases "max_deg t ≤ 1")
    case True
    then show ?thesis using "1.prems" list_dtree_def ranked_dtree_def by auto
  next
    case False
    then show ?thesis
      using 1 ranked_dtree.ranked_dtree_normalize ranked_dtree.ranked_dtree_merge1
      by (metis ikkbz_sub.simps)
  qed
qed

theorem ikkbz_sub_list_dtree: "list_dtree (ikkbz_sub t)"
  using ikkbz_sub_wf_darcs ikkbz_sub_wf_dlverts list_dtree_def by blast

corollary ikkbz_sub_ranked_dtree: "ranked_dtree (ikkbz_sub t) cmp"
  using ikkbz_sub_list_dtree ranked_dtree_def ranked_dtree_axioms by blast

lemma ikkbz_sub_mdeg_le1: "max_deg (ikkbz_sub t1) ≤ 1"
  by (induction t1 rule: ikkbz_sub.induct) simp

corollary denormalize_ikkbz_eq_dlverts: "set (denormalize (ikkbz_sub t)) = dlverts t"
  using denormalize_set_eq_dlverts ikkbz_sub_mdeg_le1 ikkbz_sub_dlverts_eq by blast

lemma distinct_ikkbz_sub: "⟦∀v∈dverts t. distinct v; v∈dverts (ikkbz_sub t)⟧ ⟹ distinct v"
using list_dtree_axioms proof(induction t arbitrary: v rule: ikkbz_sub.induct)
  case (1 t)
  then interpret T1: ranked_dtree t rank cmp
    using ranked_dtree_axioms by (simp add: ranked_dtree_def)
  show ?case
    using 1 T1.ranked_dtree_normalize T1.distinct_normalize ranked_dtree.merge1_dverts_eq
      ranked_dtree.wf_dlverts_merge1 ranked_dtree.wf_darcs_merge1
    by (metis ikkbz_sub.elims list_dtree_def)
qed

corollary distinct_denormalize_ikkbz_sub:
  "∀v∈dverts t. distinct v ⟹ distinct (denormalize (ikkbz_sub t))"
  using distinct_ikkbz_sub ikkbz_sub_wf_dlverts denormalize_distinct by blast

lemma ikkbz_sub_hd_root[simp]: "hd (root (ikkbz_sub t)) = hd (root t)"
using list_dtree_axioms proof(induction t rule: ikkbz_sub.induct)
  case (1 t)
  then interpret T1: ranked_dtree t rank cmp
    using ranked_dtree_axioms by (simp add: ranked_dtree_def)
  show ?case
    using 1 merge1_hd_root_eq ranked_dtree.axioms(1) ranked_dtree.ranked_dtree_merge1
    by (metis T1.ranked_dtree_normalize T1.wf_lverts ikkbz_sub.simps normalize_hd_root_eq')
qed

corollary denormalize_ikkbz_sub_hd_root[simp]: "hd (denormalize (ikkbz_sub t)) = hd (root t)"
  using ikkbz_sub_hd_root denormalize_hd_root
  by (metis dtree.set_sel(1) empty_notin_wf_dlverts ikkbz_sub_wf_dlverts)

end

locale precedence_graph = finite_directed_tree +
  fixes rank :: "'a list ⇒ real"
  fixes cost :: "'a list ⇒ real"
  fixes cmp :: "('a list×'b) comparator"
  assumes asi_rank: "asi rank root cost"
      and cmp_antisym:
    "⟦v1 ≠ []; v2 ≠ []; compare cmp (v1,e1) (v2,e2) = Equiv⟧ ⟹ set v1 ∩ set v2 ≠ {} ∨ e1=e2"
begin

definition to_list_dtree :: "('a list, 'b) dtree" where
  "to_list_dtree = finite_directed_tree.to_dtree to_list_tree [root]"

lemma to_list_dtree_single: "v ∈ dverts to_list_dtree ⟹ ∃x. v = [x] ∧ x ∈ verts T"
  unfolding to_list_dtree_def using to_list_tree_single
  by (simp add: finite_directed_tree.dverts_eq_verts to_list_tree_finite_directed_tree)

lemma to_list_dtree_wf_dverts: "wf_dverts to_list_dtree"
  using finite_directed_tree.wf_dverts_to_dtree[OF to_list_tree_finite_directed_tree]
  by(simp add: to_list_dtree_def)

lemma to_list_dtree_wf_dlverts: "wf_dlverts to_list_dtree"
  unfolding to_list_dtree_def
  by (simp add: to_list_tree_fin_list_directed_tree fin_list_directed_tree.wf_dlverts_to_dtree)

lemma to_list_dtree_wf_darcs: "wf_darcs to_list_dtree"
  using finite_directed_tree.wf_darcs_to_dtree[OF to_list_tree_finite_directed_tree]
  by(simp add: to_list_dtree_def)

lemma to_list_dtree_list_dtree: "list_dtree to_list_dtree"
  by(simp add: list_dtree_def to_list_dtree_wf_dlverts to_list_dtree_wf_darcs)

lemma to_list_dtree_ranked_dtree: "ranked_dtree to_list_dtree cmp"
  by(auto simp: ranked_dtree_def to_list_dtree_list_dtree ranked_dtree_axioms_def dest: cmp_antisym)

interpretation t: ranked_dtree to_list_dtree by (rule to_list_dtree_ranked_dtree)

definition ikkbz_sub :: "'a list" where
  "ikkbz_sub = denormalize (t.ikkbz_sub to_list_dtree)"

lemma dverts_eq_verts_to_list_tree: "dverts to_list_dtree = pre_digraph.verts to_list_tree"
  unfolding to_list_dtree_def
  by (simp add: finite_directed_tree.dverts_eq_verts to_list_tree_finite_directed_tree)

lemma dverts_eq_verts_img: "dverts to_list_dtree = (λx. [x]) ` verts T"
  by (simp add: dverts_eq_verts_to_list_tree to_list_tree_def)

lemma dlverts_eq_verts: "dlverts to_list_dtree = verts T"
  by (simp add: dverts_eq_verts_img dlverts_eq_dverts_union)

theorem ikkbz_set_eq_verts: "set ikkbz_sub = verts T"
  using dlverts_eq_verts ikkbz_sub_def t.denormalize_ikkbz_eq_dlverts by simp

lemma distinct_to_list_tree: "∀v∈verts to_list_tree. distinct v"
  unfolding to_list_tree_def by simp

lemma distinct_to_list_dtree: "∀v∈dverts to_list_dtree. distinct v"
  using distinct_to_list_tree dverts_eq_verts_to_list_tree by blast

theorem distinct_ikkbz_sub: "distinct ikkbz_sub"
  unfolding ikkbz_sub_def
  using distinct_to_list_dtree t.distinct_denormalize_ikkbz_sub by blast

lemma to_list_dtree_root_eq_root: "Dtree.root (to_list_dtree) = [root]"
  unfolding to_list_dtree_def
  by (simp add: finite_directed_tree.to_dtree_root_eq_root to_list_tree_finite_directed_tree)

lemma to_list_dtree_hd_root_eq_root[simp]: "hd (Dtree.root to_list_dtree) = root"
  by (simp add: to_list_dtree_root_eq_root)

theorem ikkbz_sub_hd_eq_root[simp]: "hd ikkbz_sub = root"
  unfolding ikkbz_sub_def using t.denormalize_ikkbz_sub_hd_root to_list_dtree_root_eq_root by simp

end

subsection ‹Full IKKBZ›

locale tree_query_graph = undir_tree_todir G + query_graph G for G

locale cmp_tree_query_graph = tree_query_graph +
  fixes cmp :: "('a list×'b) comparator"
  assumes cmp_antisym:
    "⟦v1 ≠ []; v2 ≠ []; compare cmp (v1,e1) (v2,e2) = Equiv⟧ ⟹ set v1 ∩ set v2 ≠ {} ∨ e1=e2"

locale ikkbz_query_graph = cmp_tree_query_graph +
  fixes cost :: "'a joinTree ⇒ real"
  fixes cost_r :: "'a ⇒ ('a list ⇒ real)"
  fixes rank_r :: "'a ⇒ ('a list ⇒ real)"
  assumes asi_rank: "r ∈ verts G ⟹ asi (rank_r r) r (cost_r r)"
      and cost_correct:
        "⟦valid_tree t; no_cross_products t; left_deep t⟧
          ⟹ cost_r (first_node t) (revorder t) = cost t"
begin

abbreviation ikkbz_sub :: "'a ⇒ 'a list" where
  "ikkbz_sub r ≡ precedence_graph.ikkbz_sub (dir_tree_r r) r (rank_r r) cmp"

abbreviation cost_l :: "'a list ⇒ real" where
  "cost_l xs ≡ cost (create_ldeep xs)"

lemma precedence_graph_r:
  "r ∈ verts G ⟹ precedence_graph (dir_tree_r r) r (rank_r r) (cost_r r) cmp"
  using fin_directed_tree_r cmp_antisym
  by (simp add: precedence_graph_def precedence_graph_axioms_def asi_rank)

lemma nempty_if_set_eq_verts: "set xs = verts G ⟹ xs ≠ []"
  using verts_nempty by force

lemma revorder_if_set_eq_verts: "set xs = verts G ⟹ revorder (create_ldeep xs) = rev xs"
  using nempty_if_set_eq_verts create_ldeep_order unfolding revorder_eq_rev_inorder by blast

lemma cost_correct':
  "⟦set xs = verts G; distinct xs; no_cross_products (create_ldeep xs)⟧
    ⟹ cost_r (hd xs) (rev xs) = cost_l xs"
  using cost_correct[of "create_ldeep xs"] revorder_if_set_eq_verts create_ldeep_ldeep[of xs]
  unfolding valid_tree_def distinct_relations_def
  by (simp add: create_ldeep_order create_ldeep_relations first_node_eq_hd nempty_if_set_eq_verts)

lemma ikkbz_sub_verts_eq: "r ∈ verts G ⟹ set (ikkbz_sub r) = verts G"
  using precedence_graph.ikkbz_set_eq_verts precedence_graph_r verts_dir_tree_r_eq by fast

lemma ikkbz_sub_distinct: "r ∈ verts G ⟹ distinct (ikkbz_sub r)"
  using precedence_graph.distinct_ikkbz_sub precedence_graph_r by fast

lemma ikkbz_sub_hd_eq_root: "r ∈ verts G ⟹ hd (ikkbz_sub r) = r"
  using precedence_graph.ikkbz_sub_hd_eq_root precedence_graph_r by fast

definition ikkbz :: "'a list" where
  "ikkbz ≡ arg_min_on cost_l {ikkbz_sub r|r. r ∈ verts G}"

lemma ikkbz_sub_set_fin: "finite {ikkbz_sub r|r. r ∈ verts G}"
  by simp

lemma ikkbz_sub_set_nempty: "{ikkbz_sub r|r. r ∈ verts G} ≠ {}"
  by (simp add: verts_nempty)

lemma ikkbz_in_ikkbz_sub_set: "ikkbz ∈ {ikkbz_sub r|r. r ∈ verts G}"
  unfolding ikkbz_def using ikkbz_sub_set_fin ikkbz_sub_set_nempty arg_min_if_finite by blast

lemma ikkbz_eq_ikkbz_sub: "∃r ∈ verts G. ikkbz = ikkbz_sub r"
  using ikkbz_in_ikkbz_sub_set by blast

lemma ikkbz_min_ikkbz_sub: "r ∈ verts G ⟹ cost_l ikkbz ≤ cost_l (ikkbz_sub r)"
  unfolding ikkbz_def using ikkbz_sub_set_fin arg_min_least by fast

lemma ikkbz_distinct: "distinct ikkbz"
  using ikkbz_eq_ikkbz_sub ikkbz_sub_distinct by fastforce

lemma ikkbz_set_eq_verts: "set ikkbz = verts G"
  using ikkbz_eq_ikkbz_sub ikkbz_sub_verts_eq by force

lemma ikkbz_nempty: "ikkbz ≠ []"
  using ikkbz_set_eq_verts verts_nempty by fastforce

lemma ikkbz_hd_in_verts: "hd ikkbz ∈ verts G"
  using ikkbz_nempty ikkbz_set_eq_verts by fastforce

lemma inorder_ikkbz: "inorder (create_ldeep ikkbz) = ikkbz"
  using create_ldeep_order ikkbz_nempty by blast

lemma inorder_ikkbz_distinct: "distinct (inorder (create_ldeep ikkbz))"
  using ikkbz_distinct inorder_ikkbz by simp

lemma inorder_relations_eq_verts: "relations (create_ldeep ikkbz) = verts G"
  using ikkbz_set_eq_verts create_ldeep_relations ikkbz_nempty by blast

theorem ikkbz_valid_tree: "valid_tree (create_ldeep ikkbz)"
  unfolding valid_tree_def distinct_relations_def
  using inorder_ikkbz_distinct inorder_relations_eq_verts by blast

end

(* non commutative merging based on inserting (INCOMPLETE) *)

locale old = list_dtree t for t :: "('a list,'b) dtree" +
  fixes rank :: "'a list ⇒ real"
begin

function find_pos_aux :: "'a list ⇒ 'a list ⇒ ('a list,'b) dtree ⇒ ('a list × 'a list)" where
  "find_pos_aux v p (Node r {|(t1,_)|}) =
    (if rank (rev v) ≤ rank (rev r) then (p,r) else find_pos_aux v r t1)"
| "∀x. xs ≠ {|x|} ⟹ find_pos_aux v p (Node r xs) =
    (if rank (rev v) ≤ rank (rev r) then (p,r) else (r,r))"
  by (metis combine.cases old.prod.exhaust) auto
termination by lexicographic_order

function find_pos :: "'a list ⇒ ('a list,'b) dtree ⇒ ('a list × 'a list)" where
  "find_pos v (Node r {|(t1,_)|}) = find_pos_aux v r t1"
| "∀x. xs ≠ {|x|} ⟹ find_pos v (Node r xs) = (r,r)"
  by (metis dtree.exhaust surj_pair) auto
termination by lexicographic_order

abbreviation insert_chain :: "('a list×'b) list ⇒ ('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "insert_chain xs t1 ≡
    foldr (λ(v,e) t2. case find_pos v t2 of (x,y) ⇒ insert_between v e x y t2) xs t1"

fun merge :: "('a list,'b) dtree ⇒ ('a list,'b) dtree" where
  "merge (Node r xs) = ffold (λ(t,e) b. case b of Node r xs ⇒
      if xs = {||} then Node r {|(t,e)|} else insert_chain (dtree_to_list t) b)
    (Node r {||}) xs"

lemma ffold_if_False_eq_acc:
  "⟦∀a. ¬P a; comp_fun_commute (λa b. if ¬P a then b else Q a b)⟧
    ⟹ ffold (λa b. if ¬P a then b else Q a b) acc xs = acc"
proof(induction xs)
  case (insert x xs)
  let ?f = "λa b. if ¬P a then b else Q a b"
  have "ffold ?f acc (finsert x xs) = ?f x (ffold ?f acc xs)"
    using insert.hyps by (simp add: comp_fun_commute.ffold_finsert insert.prems(2))
  then have "ffold ?f acc (finsert x xs) = ffold ?f acc xs" using insert.prems by simp
  then show ?case using insert.IH insert.prems by simp
qed(simp add: comp_fun_commute.ffold_empty)

lemma find_pos_rank_less: "rank (rev v) ≤ rank (rev r) ⟹ find_pos_aux v p (Node r xs) = (p,r)"
  by(cases "∃x. xs = {|x|}") auto

lemma find_pos_y_in_dverts: "(x,y) = find_pos_aux v p t1 ⟹ y ∈ dverts t1"
proof(induction t1 arbitrary: p)
  case (Node r xs)
  then show ?case
  proof(cases "rank (rev v) ≤ rank (rev r)")
    case True
    then show ?thesis using Node.prems by(cases "∃x. xs = {|x|}") auto
  next
    case False
    then show ?thesis using Node by(cases "∃x. xs = {|x|}") fastforce+
  qed
qed

lemma find_pos_x_in_dverts: "(x,y) = find_pos_aux v p t1 ⟹ x ∈ dverts t1 ∨ p=x"
proof(induction t1 arbitrary: p)
  case (Node r xs)
  then show ?case
  proof(cases "rank (rev v) ≤ rank (rev r)")
    case True
    then show ?thesis using Node.prems by(cases "∃x. xs = {|x|}") auto
  next
    case False
    then show ?thesis using Node by(cases "∃x. xs = {|x|}") fastforce+
  qed
qed

end

end