Theory Decreasing_Diagrams_II

(*
 * Title:      Decreasing Diagrams II  
 * Author:     Bertram Felgenhauer (2015)
 * Maintainer: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at>
 * License:    LGPL
 *)
section ‹Decreasing Diagrams›

theory Decreasing_Diagrams_II
imports
  Decreasing_Diagrams_II_Aux
  "HOL-Cardinals.Wellorder_Extension"
  "Abstract-Rewriting.Abstract_Rewriting"
begin

subsection ‹Greek accents›

datatype accent = Acute | Grave | Macron

lemma UNIV_accent: "UNIV = { Acute, Grave, Macron }"
using accent.nchotomy by blast

lemma finite_accent: "finite (UNIV :: accent set)"
by (simp add: UNIV_accent)

type_synonym 'a letter = "accent × 'a"

definition letter_less :: "('a × 'a) set ⇒ ('a letter × 'a letter) set" where
  [simp]: "letter_less R = {(a,b). (snd a, snd b) ∈ R}"

lemma mono_letter_less: "mono letter_less"
by (auto simp add: mono_def)


subsection ‹Comparing Greek strings›

type_synonym 'a greek = "'a letter list"

definition adj_msog :: "'a greek ⇒ 'a greek ⇒ ('a letter × 'a greek) ⇒ ('a letter × 'a greek)"
where
  "adj_msog xs zs l ≡
    case l of (y,ys) ⇒ (y, case fst y of Acute ⇒ ys @ zs | Grave ⇒ xs @ ys | Macron ⇒ ys)"

definition ms_of_greek :: "'a greek ⇒ ('a letter × 'a greek) multiset" where
  "ms_of_greek as = mset
    (map (λ(xs, y, zs) ⇒ adj_msog xs zs (y, [])) (list_splits as))"

lemma adj_msog_adj_msog[simp]:
  "adj_msog xs zs (adj_msog xs' zs' y) = adj_msog (xs @ xs') (zs' @ zs) y"
by (auto simp: adj_msog_def split: accent.splits prod.splits)

lemma compose_adj_msog[simp]: "adj_msog xs zs ∘ adj_msog xs' zs' = adj_msog (xs @ xs') (zs' @ zs)"
by (simp add: comp_def)

lemma adj_msog_single:
  "adj_msog xs zs (x,[]) = (x, (case fst x of Grave ⇒ xs | Acute ⇒ zs | Macron ⇒ []))"
by (simp add: adj_msog_def split: accent.splits)

lemma ms_of_greek_elem:
  assumes "(x,xs) ∈ set_mset (ms_of_greek ys)"
  shows "x ∈ set ys"
using assms by (auto dest: elem_list_splits_elem simp: adj_msog_def ms_of_greek_def)

lemma ms_of_greek_shorter:
  assumes "(x, t) ∈# ms_of_greek s"
  shows "length s > length t"
using assms[unfolded ms_of_greek_def in_multiset_in_set]
by (auto simp: elem_list_splits_length adj_msog_def split: accent.splits)

lemma msog_append: "ms_of_greek (xs @ ys) = image_mset (adj_msog [] ys) (ms_of_greek xs) +
  image_mset (adj_msog xs []) (ms_of_greek ys)"
by (auto simp: ms_of_greek_def list_splits_append multiset.map_comp comp_def prod.case_distrib)

definition nest :: "('a × 'a) set ⇒ ('a greek × 'a greek) set ⇒ ('a greek × 'a greek) set" where
  [simp]: "nest r s = {(a,b). (ms_of_greek a, ms_of_greek b) ∈ mult (letter_less r <*lex*> s)}"

lemma mono_nest: "mono (nest r)"
unfolding mono_def
proof (intro allI impI subsetI)
  fix R S x
  assume 1: "R ⊆ S" and 2: "x ∈ nest r R"
  from 1 have "mult (letter_less r <*lex*> R) ⊆ mult (letter_less r <*lex*> S)"
  using mono_mult mono_lex2[of "letter_less r"] unfolding mono_def by blast
  with 2 show "x ∈ nest r S" by auto
qed

lemma nest_mono[mono_set]: "x ⊆ y ⟹ (a,b) ∈ nest r x ⟶ (a,b) ∈ nest r y"
using mono_nest[unfolded mono_def, rule_format, of x y r] by blast

definition greek_less :: "('a × 'a) set ⇒ ('a greek × 'a greek) set" where
  "greek_less r = lfp (nest r)"

lemma greek_less_unfold:
  "greek_less r = nest r (greek_less r)"
using mono_nest[of r] lfp_unfold[of "nest r"] by (simp add: greek_less_def)


subsection ‹Preservation of strict partial orders›

lemma strict_order_letter_less:
  assumes "strict_order r"
  shows "strict_order (letter_less r)"
using assms unfolding irrefl_def trans_def letter_less_def by fast

lemma strict_order_nest:
  assumes r: "strict_order r" and R: "strict_order R"
  shows "strict_order (nest r R)"
proof -
  have "strict_order (mult (letter_less r <*lex*> R))"
  using strict_order_letter_less[of r] irrefl_lex_prod[of "letter_less r" R]
    trans_lex_prod[of "letter_less r" R] strict_order_mult[of "letter_less r <*lex*> R"] assms
  by fast
  from this show "strict_order (nest r R)" unfolding nest_def trans_def irrefl_def by fast
qed

lemma strict_order_greek_less:
  assumes "strict_order r"
  shows "strict_order (greek_less r)"
by (simp add: greek_less_def strict_order_lfp[OF mono_nest strict_order_nest[OF assms]])

lemma trans_letter_less:
  assumes "trans r"
  shows "trans (letter_less r)"
using assms unfolding trans_def letter_less_def by fast

lemma trans_order_nest: "trans (nest r R)"
using trans_mult unfolding nest_def trans_def by fast

lemma trans_greek_less[simp]: "trans (greek_less r)"
by (subst greek_less_unfold) (rule trans_order_nest)

lemma mono_greek_less: "mono greek_less"
unfolding greek_less_def mono_def
proof (intro allI impI lfp_mono)
  fix r s :: "('a × 'a) set" and R :: "('a greek × 'a greek) set"
  assume "r ⊆ s"
  then have "letter_less r <*lex*> R ⊆ letter_less s <*lex*> R"
  using mono_letter_less mono_lex1 unfolding mono_def by metis
  then show "nest r R ⊆ nest s R" using mono_mult unfolding nest_def mono_def by blast
qed


subsection ‹Involution›

definition inv_letter :: "'a letter ⇒ 'a letter" where
  "inv_letter l ≡
    case l of (a, x) ⇒ (case a of Grave ⇒ Acute | Acute ⇒ Grave | Macron ⇒ Macron, x)"

lemma inv_letter_pair[simp]:
  "inv_letter (a, x) = (case a of Grave ⇒ Acute | Acute ⇒ Grave | Macron ⇒ Macron, x)"
by (simp add: inv_letter_def)

lemma snd_inv_letter[simp]:
  "snd (inv_letter x) = snd x"
by (simp add: inv_letter_def split: prod.splits)

lemma inv_letter_invol[simp]:
  "inv_letter (inv_letter x) = x"
by (simp add: inv_letter_def split: prod.splits accent.splits)

lemma inv_letter_mono[simp]:
  assumes "(x, y) ∈ letter_less r"
  shows "(inv_letter x, inv_letter y) ∈ letter_less r"
using assms by simp

definition inv_greek :: "'a greek ⇒ 'a greek" where
  "inv_greek s = rev (map inv_letter s)"

lemma inv_greek_invol[simp]:
  "inv_greek (inv_greek s) = s"
by (simp add: inv_greek_def rev_map comp_def)

lemma inv_greek_append:
  "inv_greek (s @ t) = inv_greek t @ inv_greek s"
by (simp add: inv_greek_def)

definition inv_msog :: "('a letter × 'a greek) multiset ⇒ ('a letter × 'a greek) multiset" where
  "inv_msog M = image_mset (λ(x, t). (inv_letter x, inv_greek t)) M"

lemma inv_msog_invol[simp]:
  "inv_msog (inv_msog M) = M"
by (simp add: inv_msog_def multiset.map_comp comp_def prod.case_distrib)

lemma ms_of_greek_inv_greek:
  "ms_of_greek (inv_greek M) = inv_msog (ms_of_greek M)"
unfolding inv_msog_def inv_greek_def ms_of_greek_def list_splits_rev list_splits_map mset_map
  multiset.map_comp mset_rev inv_letter_def adj_msog_def
by (rule cong[OF cong[OF refl[of "image_mset"]] refl]) (auto split: accent.splits)

lemma inv_greek_mono:
  assumes "trans r" and "(s, t) ∈ greek_less r"
  shows "(inv_greek s, inv_greek t) ∈ greek_less r"
using assms(2)
proof (induct "length s + length t" arbitrary: s t rule: less_induct)
  note * = trans_lex_prod[OF trans_letter_less[OF ‹trans r›] trans_greek_less[of r]]
  case (less s t)
  have "(inv_msog (ms_of_greek s), inv_msog (ms_of_greek t)) ∈ mult (letter_less r <*lex*> greek_less r)"
  unfolding inv_msog_def
  proof (induct rule: mult_of_image_mset[OF * *])
    case (1 x y) thus ?case
    by (auto intro: less(1) split: prod.splits dest!: ms_of_greek_shorter)
  next
    case 2 thus ?case using less(2) by (subst(asm) greek_less_unfold) simp
  qed
  thus ?case by (subst greek_less_unfold) (auto simp: ms_of_greek_inv_greek)
qed


subsection ‹Monotonicity of @{term "greek_less r"}›

lemma greek_less_rempty[simp]:
  "(a,[]) ∈ greek_less r ⟷ False"
by (subst greek_less_unfold) (auto simp: ms_of_greek_def)

lemma greek_less_nonempty:
  assumes "b ≠ []"
  shows "(a,b) ∈ greek_less r ⟷ (a,b) ∈ nest r (greek_less r)"
by (subst greek_less_unfold) simp

lemma greek_less_lempty[simp]:
  "([],b) ∈ greek_less r ⟷ b ≠ []"
proof
  assume "([],b) ∈ greek_less r"
  then show "b ≠ []" using greek_less_rempty by fast
next
  assume "b ≠ []"
  then show "([],b) ∈ greek_less r"
  unfolding greek_less_nonempty[OF ‹b ≠ []›] by (simp add: ms_of_greek_def)
qed

lemma greek_less_singleton:
  "(a, b) ∈ letter_less r ⟹ ([a], [b]) ∈ greek_less r"
by (subst greek_less_unfold) (auto split: accent.splits simp: adj_msog_def ms_of_greek_def)

lemma ms_of_greek_cons:
  "ms_of_greek (x # s) = {# adj_msog [] s (x,[]) #} + image_mset (adj_msog [x] []) (ms_of_greek s)"
using msog_append[of "[x]" s]
by (auto simp add: adj_msog_def ms_of_greek_def accent.splits)

lemma greek_less_cons_mono:
  assumes "trans r"
  shows "(s, t) ∈ greek_less r ⟹ (x # s, x # t) ∈ greek_less r"
proof (induct "length s + length t" arbitrary: s t rule: less_induct)
  note * = trans_lex_prod[OF trans_letter_less[OF ‹trans r›] trans_greek_less[of r]]
  case (less s t)
  {
    fix M have "(M + image_mset (adj_msog [x] []) (ms_of_greek s),
      M + image_mset (adj_msog [x] []) (ms_of_greek t)) ∈ mult (letter_less r <*lex*> greek_less r)"
    proof (rule mult_on_union, induct rule: mult_of_image_mset[OF * *])
      case (1 x y) thus ?case unfolding adj_msog_def
      by (auto intro: less(1) split: prod.splits accent.splits dest!: ms_of_greek_shorter)
    next
      case 2 thus ?case using less(2) by (subst(asm) greek_less_unfold) simp
    qed
  }
  moreover {
    fix N have "({# adj_msog [] s (x,[]) #} + N,{# adj_msog [] t (x,[]) #} + N) ∈
      (mult (letter_less r <*lex*> greek_less r))⇧="
    by (auto simp: adj_msog_def less split: accent.splits) }
  ultimately show ?case using transD[OF trans_mult]
  by (subst greek_less_unfold) (fastforce simp: ms_of_greek_cons)
qed

lemma greek_less_app_mono2:
  assumes "trans r" and "(s, t) ∈ greek_less r"
  shows "(p @ s, p @ t) ∈ greek_less r"
using assms by (induct p) (auto simp add: greek_less_cons_mono)

lemma greek_less_app_mono1:
  assumes "trans r" and "(s, t) ∈ greek_less r"
  shows "(s @ p, t @ p) ∈ greek_less r"
using inv_greek_mono[of r "inv_greek p @ inv_greek s" "inv_greek p @ inv_greek t"]
by (simp add: assms inv_greek_append inv_greek_mono greek_less_app_mono2)


subsection ‹Well-founded-ness of @{term "greek_less r"}›

lemma greek_embed:
  assumes "trans r"
  shows "list_emb (λa b. (a, b): reflcl (letter_less r)) a b ⟹ (a, b) ∈ reflcl (greek_less r)"
proof (induct rule: list_emb.induct)
  case (list_emb_Cons a b y) thus ?case
  using trans_greek_less[unfolded trans_def] ‹trans r›
    greek_less_app_mono1[of r "[]" "[y]" a] greek_less_app_mono2[of r a b "[y]"] by auto
next
  case (list_emb_Cons2 x y a b) thus ?case
  using trans_greek_less[unfolded trans_def] ‹trans r› greek_less_singleton[of x y r]
    greek_less_app_mono1[of r "[x]" "[y]" a] greek_less_app_mono2[of r a b "[y]"] by auto
qed simp

lemma wqo_letter_less:
  assumes t: "trans r" and w: "wqo_on (λa b. (a, b) ∈ r⇧=) UNIV"
  shows "wqo_on (λa b. (a, b) ∈ (letter_less r)⇧=) UNIV"
proof (rule wqo_on_hom[of id _ _ "prod_le (=) (λa b. (a, b) ∈ r⇧=)", unfolded image_id id_apply])
  show "wqo_on (prod_le ((=) :: accent ⇒ accent ⇒ bool) (λa b. (a, b) ∈ r⇧=)) UNIV"
  by (rule dickson[OF finite_eq_wqo_on[OF finite_accent] w, unfolded UNIV_Times_UNIV])
qed (insert t, auto simp: transp_on_def trans_def prod_le_def)

lemma wf_greek_less:
  assumes "wf r" and "trans r"
  shows "wf (greek_less r)"
proof -
  obtain q where "r ⊆ q" and "well_order q" by (metis total_well_order_extension ‹wf r›)
  define q' where "q' = q - Id"
  from ‹well_order q› have "reflcl q' = q"
  by (auto simp add: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def
      refl_on_def q'_def)
  from ‹well_order q› have "trans q'" and "irrefl q'"
  unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def antisym_def
    trans_def irrefl_def q'_def by blast+
  from ‹r ⊆ q› ‹wf r› have "r ⊆ q'" by (auto simp add: q'_def)
  have "wqo_on (λa b. (a,b) ∈ (greek_less q')⇧=) UNIV"
  proof (intro wqo_on_hom[of id UNIV "(λa b. (a, b) ∈ (greek_less q')⇧=)"
         "list_emb (λa b. (a, b) ∈ (letter_less q')⇧=)", unfolded surj_id])
    show "transp (λa b. (a, b) ∈ (greek_less q')⇧=)"
    using trans_greek_less[of q'] unfolding trans_def transp_on_def by blast
  next
    show "∀x∈UNIV. ∀y∈UNIV. list_emb (λa b. (a, b) ∈ (letter_less q')⇧=) x y ⟶
          (id x, id y) ∈ (greek_less q')⇧="
    using greek_embed[OF ‹trans q'›] by auto
  next
    show "wqo_on (list_emb (λa b. (a, b) ∈ (letter_less q')⇧=)) UNIV"
    using higman[OF wqo_letter_less[OF ‹trans q'›]] ‹well_order q› ‹reflcl q' = q›
    by (auto simp: well_order_implies_wqo)
  qed
  with wqo_on_imp_wfp_on[OF this] strict_order_strict[OF strict_order_greek_less]
    ‹irrefl q'› ‹trans q'›
  have "wfp_on (λa b. (a, b) ∈ greek_less q') UNIV" by force
  then show ?thesis
  using mono_greek_less ‹r ⊆ q'› wf_subset unfolding wf_iff_wfp_on[symmetric] mono_def by metis
qed


subsection ‹Basic Comparisons›

lemma pairwise_imp_mult:
  assumes "N ≠ {#}" and "∀x ∈ set_mset M. ∃y ∈ set_mset N. (x, y) ∈ r"
  shows "(M, N) ∈ mult r"
using assms one_step_implies_mult[of _ _ _ "{#}"] by auto

lemma singleton_greek_less:
  assumes as: "snd ` set as ⊆ under r b"
  shows "(as, [(a,b)]) ∈ greek_less r"
proof -
  {
    fix e assume "e ∈ set_mset (ms_of_greek as)"
    with as ms_of_greek_elem[of _ _ as]
    have "(e, ((a,b),[])) ∈ letter_less r <*lex*> greek_less r"
    by (cases e) (fastforce simp: adj_msog_def under_def)
  }
  moreover have "ms_of_greek [(a,b)] = {# ((a,b),[]) #}"
  by (auto simp: ms_of_greek_def adj_msog_def split: accent.splits)
  ultimately show ?thesis
  by (subst greek_less_unfold) (auto intro!: pairwise_imp_mult)
qed

lemma peak_greek_less:
  assumes as: "snd ` set as ⊆ under r a" and b': "b' ∈ {[(Grave,b)],[]}"
  and cs: "snd ` set cs ⊆ under r a ∪ under r b" and a': "a' ∈ {[(Acute,a)],[]}"
  and bs: "snd ` set bs ⊆ under r b"
  shows "(as @ b' @ cs @ a' @ bs, [(Acute,a),(Grave,b)]) ∈ greek_less r"
proof -
  let ?A = "(Acute,a)" and ?B = "(Grave,b)"
  have "(ms_of_greek (as @ b' @ cs @ a' @ bs), ms_of_greek [?A,?B]) ∈ mult (letter_less r <*lex*> greek_less r)"
  proof (intro pairwise_imp_mult)
    (* we distinguish 5 cases depending on where in xs an element e originates *)
    {
      fix e assume "e ∈ set_mset (ms_of_greek as)"
      with as ms_of_greek_elem[of _ _ as]
      have "(adj_msog [] (b' @ cs @ a' @ bs) e, (?A,[?B])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def under_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek b')"
      with b' singleton_greek_less[OF as] ms_of_greek_elem[of _ _ b']
      have "(adj_msog as (cs @ a' @ bs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek cs)"
      with cs ms_of_greek_elem[of _ _ cs]
      have "(adj_msog (as @ b') (a' @ bs) e, (?A,[?B])) ∈ letter_less r <*lex*> greek_less r ∨
            (adj_msog (as @ b') (a' @ bs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def under_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek a')"
      with a' singleton_greek_less[OF bs] ms_of_greek_elem[of _ _ a']
      have "(adj_msog (as @ b' @ cs) bs e, (?A,[?B])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek bs)"
      with bs ms_of_greek_elem[of _ _ bs]
      have "(adj_msog (as @ b' @ cs @ a') [] e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def under_def)
    }
    moreover have "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[?B]) #}"
    by (simp add: adj_msog_def ms_of_greek_def)
    ultimately show "∀x∈set_mset (ms_of_greek (as @ b' @ cs @ a' @ bs)).
      ∃y∈set_mset (ms_of_greek [?A,?B]). (x, y) ∈ letter_less r <*lex*> greek_less r"
    by (auto simp: msog_append) blast
  qed (auto simp: ms_of_greek_def)
  then show ?thesis by (subst greek_less_unfold) auto
qed

lemma rcliff_greek_less1:
  assumes "trans r" (* unused assumption kept for symmetry with lcliff_greek_less1 *)
  and as: "snd ` set as ⊆ under r a ∩ under r b" and b': "b' ∈ {[(Grave,b)],[]}"
  and cs: "snd ` set cs ⊆ under r b" and a': "a' = [(Macron,a)]"
  and bs: "snd ` set bs ⊆ under r b"
  shows "(as @ b' @ cs @ a' @ bs, [(Macron,a),(Grave,b)]) ∈ greek_less r"
proof -
  let ?A = "(Macron,a)" and ?B = "(Grave,b)"
  have *: "ms_of_greek [?A,?B] = {#(?B,[?A]), (?A,[])#}" "ms_of_greek [?A] = {#(?A,[])#}"
  by (simp_all add: ms_of_greek_def adj_msog_def)
  then have **: "ms_of_greek [(Macron, a), (Grave, b)] - {#((Macron, a), [])#} ≠ {#}"
  by (auto)
  (* we distinguish 5 cases depending on where in xs an element e originates *)
  {
    fix e assume "e ∈ set_mset (ms_of_greek as)"
    with as ms_of_greek_elem[of _ _ as]
    have "(adj_msog [] (b' @ cs @ a' @ bs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
    by (cases e) (force simp: adj_msog_def under_def)
  }
  moreover {
    fix e assume "e ∈ set_mset (ms_of_greek b')"
    with b' singleton_greek_less as ms_of_greek_elem[of _ _ b']
    have "(adj_msog as (cs @ a' @ bs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
    by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def)
  }
  moreover {
    fix e assume "e ∈ set_mset (ms_of_greek cs)"
    with cs ms_of_greek_elem[of _ _ cs]
    have "(adj_msog (as @ b') (a' @ bs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
    by (cases e) (fastforce simp: adj_msog_def under_def)
  }
  moreover {
    fix e assume "e ∈ set_mset (ms_of_greek bs)"
    with bs ms_of_greek_elem[of _ _ bs]
    have "(adj_msog (as @ b' @ cs @ a') [] e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
    by (cases e) (fastforce simp: adj_msog_def under_def)
  }
  moreover have "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[]) #}"
  by (simp add: adj_msog_def ms_of_greek_def)
  ultimately have "∀x∈set_mset (ms_of_greek (as @ b' @ cs @ a' @ bs) - {#(?A,[])#}).
    ∃y∈set_mset (ms_of_greek [?A,?B] - {#(?A,[])#}). (x, y) ∈ letter_less r <*lex*> greek_less r"
  unfolding msog_append by (auto simp: a' msog_append ac_simps * adj_msog_single)
  from one_step_implies_mult[OF ** this,of "{#(?A,[])#}"]
  have "(ms_of_greek (as @ b' @ cs @ a' @ bs), ms_of_greek [?A,?B]) ∈ mult (letter_less r <*lex*> greek_less r)"
  unfolding a' msog_append by (auto simp: a' ac_simps * adj_msog_single)
  then show ?thesis
  by (subst greek_less_unfold) auto
qed

lemma rcliff_greek_less2:
  assumes "trans r" (* unused assumption kept for symmetry with lcliff_greek_less2 *)
  and as: "snd ` set as ⊆ under r a" and b': "b' ∈ {[(Grave,b)],[]}"
  and cs: "snd ` set cs ⊆ under r a ∪ under r b"
  shows "(as @ b' @ cs, [(Macron,a),(Grave,b)]) ∈ greek_less r"
proof -
  let ?A = "(Macron,a)" and ?B = "(Grave,b)"
  have "(ms_of_greek (as @ b' @ cs), ms_of_greek [?A,?B]) ∈ mult (letter_less r <*lex*> greek_less r)"
  proof (intro pairwise_imp_mult)
    (* we distinguish 3 cases depending on where in xs an element e originates *)
    {
      fix e assume "e ∈ set_mset (ms_of_greek as)"
      with as ms_of_greek_elem[of _ _ as]
      have "(adj_msog [] (b' @ cs) e, (?A,[])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def under_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek b')"
      with b' singleton_greek_less[OF as] ms_of_greek_elem[of _ _ b']
      have "(adj_msog as (cs) e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def)
    }
    moreover {
      fix e assume "e ∈ set_mset (ms_of_greek cs)"
      with cs ms_of_greek_elem[of _ _ cs]
      have "(adj_msog (as @ b') [] e, (?A,[])) ∈ letter_less r <*lex*> greek_less r ∨
            (adj_msog (as @ b') [] e, (?B,[?A])) ∈ letter_less r <*lex*> greek_less r"
      by (cases e) (fastforce simp: adj_msog_def under_def)
    }
    moreover have *: "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[]) #}"
    by (simp add: adj_msog_def ms_of_greek_def)
    ultimately show "∀x∈set_mset (ms_of_greek (as @ b' @ cs)).
      ∃y∈set_mset (ms_of_greek [?A,?B]). (x, y) ∈ letter_less r <*lex*> greek_less r"
    by (auto simp: msog_append adj_msog_single ac_simps *) blast
  qed (auto simp: ms_of_greek_def)
  then show ?thesis by (subst greek_less_unfold) auto
qed

lemma snd_inv_greek [simp]: "snd ` set (inv_greek as) = snd ` set as"
by (force simp: inv_greek_def)

lemma lcliff_greek_less1:
  assumes "trans r"
  and as: "snd ` set as ⊆ under r a" and b': "b' = [(Macron,b)]"
  and cs: "snd ` set cs ⊆ under r a" and a': "a' ∈ {[(Acute,a)],[]}"
  and bs: "snd ` set bs ⊆ under r a ∩ under r b"
  shows "(as @ b' @ cs @ a' @ bs, [(Acute,a),(Macron,b)]) ∈ greek_less r"
proof -
  have *: "inv_greek [(Acute,a),(Macron,b)] = [(Macron,b),(Grave,a)]" by (simp add: inv_greek_def)
  have "(inv_greek (inv_greek (as @ b' @ cs @ a' @ bs)),
   inv_greek (inv_greek ([(Acute,a),(Macron,b)]))) ∈ greek_less r"
   apply (rule inv_greek_mono[OF ‹trans r›])
   apply (unfold inv_greek_append append_assoc *)
   apply (insert assms)
   apply (rule rcliff_greek_less1, auto simp: inv_greek_def)
  done
  then show ?thesis by simp
qed

lemma lcliff_greek_less2:
  assumes "trans r"
  and cs: "snd ` set cs ⊆ under r a ∪ under r b" and a': "a' ∈ {[(Acute,a)],[]}"
  and bs: "snd ` set bs ⊆ under r b"
  shows "(cs @ a' @ bs, [(Acute,a),(Macron,b)]) ∈ greek_less r"
proof -
  have *: "inv_greek [(Acute,a),(Macron,b)] = [(Macron,b),(Grave,a)]" by (simp add: inv_greek_def)
  have "(inv_greek (inv_greek (cs @ a' @ bs)),
    inv_greek (inv_greek ([(Acute,a),(Macron,b)]))) ∈ greek_less r"
   apply (rule inv_greek_mono[OF ‹trans r›])
   apply (unfold inv_greek_append append_assoc *)
   apply (insert assms)
   apply (rule rcliff_greek_less2, auto simp: inv_greek_def)
  done
  then show ?thesis by simp
qed


subsection ‹Labeled abstract rewriting›

context
  fixes L R E :: "'b ⇒ 'a rel"
begin

definition lstep :: "'b letter ⇒ 'a rel" where
  [simp]: "lstep x = (case x of (a, i) ⇒ (case a of Acute ⇒ (L i)¯ | Grave ⇒ R i | Macron ⇒ E i))"

fun lconv :: "'b greek ⇒ 'a rel" where
  "lconv [] = Id"
| "lconv (x # xs) = lstep x O lconv xs"

lemma lconv_append[simp]:
  "lconv (xs @ ys) = lconv xs O lconv ys"
by (induct xs) auto

lemma conversion_join_or_peak_or_cliff:
  obtains (join) as bs cs where "set as ⊆ {Grave}" and "set bs ⊆ {Macron}" and "set cs ⊆ {Acute}"
    and "ds = as @ bs @ cs"
  | (peak) as bs where "ds = as @ ([Acute] @ [Grave]) @ bs"
  | (lcliff) as bs where "ds = as @ ([Acute] @ [Macron]) @ bs"
  | (rcliff) as bs where "ds = as @ ([Macron] @ [Grave]) @ bs"
proof (induct ds arbitrary: thesis)
  case (Cons d ds thesis) note IH = this show ?case
  proof (rule IH(1))
    fix as bs assume "ds = as @ ([Acute] @ [Grave]) @ bs" then show ?case
    using IH(3)[of "d # as" bs] by simp
  next
    fix as bs assume "ds = as @ ([Acute] @ [Macron]) @ bs" then show ?case
    using IH(4)[of "d # as" bs] by simp
  next
    fix as bs assume "ds = as @ ([Macron] @ [Grave]) @ bs" then show ?case
    using IH(5)[of "d # as" bs] by simp
  next
    fix as bs cs assume *: "set as ⊆ {Grave}" "set bs ⊆ {Macron}" "set cs ⊆ {Acute}" "ds = as @ bs @ cs"
    show ?case
    proof (cases d)
      case Grave thus ?thesis using * IH(2)[of "d # as" bs cs] by simp
    next
      case Macron show ?thesis
      proof (cases as)
        case Nil thus ?thesis using * Macron IH(2)[of as "d # bs" cs] by simp
      next
        case (Cons a as) thus ?thesis using * Macron IH(5)[of "[]" "as @ bs @ cs"] by simp
      qed
    next
      case Acute show ?thesis
      proof (cases as)
        case Nil note as = this show ?thesis
        proof (cases bs)
          case Nil thus ?thesis using * as Acute IH(2)[of "[]" "[]" "d # cs"] by simp
        next
          case (Cons b bs) thus ?thesis using * as Acute IH(4)[of "[]" "bs @ cs"] by simp
        qed
      next
        case (Cons a as) thus ?thesis using * Acute IH(3)[of "[]" "as @ bs @ cs"] by simp
      qed
    qed
  qed
qed auto

lemma map_eq_append_split:
  assumes "map f xs = ys1 @ ys2"
  obtains xs1 xs2 where "ys1 = map f xs1" "ys2 = map f xs2" "xs = xs1 @ xs2"
proof (insert assms, induct ys1 arbitrary: xs thesis)
  case (Cons y ys) note IH = this show ?case
  proof (cases xs)
    case (Cons x xs') show ?thesis
    proof (rule IH(1))
      fix xs1 xs2 assume "ys = map f xs1" "ys2 = map f xs2" "xs' = xs1 @ xs2" thus ?thesis
      using Cons IH(2)[of "x # xs1" xs2] IH(3) by simp
    next
      show "map f xs' = ys @ ys2" using Cons IH(3) by simp
    qed
  qed (insert Cons, simp)
qed auto

lemmas map_eq_append_splits = map_eq_append_split map_eq_append_split[OF sym]

abbreviation "conversion' M ≡ ((⋃i ∈ M. R i) ∪ (⋃i ∈ M. E i) ∪ (⋃i ∈ M. L i)¯)⇧*"
abbreviation "valley' M ≡  (⋃i ∈ M. R i)⇧* O (⋃i ∈ M. E i)⇧* O ((⋃i ∈ M. L i)¯)⇧*"

lemma conversion_to_lconv:
  assumes "(u, v) ∈ conversion' M"
  obtains xs where "snd ` set xs ⊆ M" and "(u, v) ∈ lconv xs"
using assms
proof (induct arbitrary: thesis rule: converse_rtrancl_induct)
  case base show ?case using base[of "[]"] by simp
next
  case (step u' x)
  from step(1) obtain p where "snd p ∈ M" and "(u', x) ∈ lstep p"
  by (force split: accent.splits)
  moreover obtain xs where "snd ` set xs ⊆ M" "(x, v) ∈ lconv xs" by (rule step(3))
  ultimately show ?case using step(4)[of "p # xs"] by auto
qed

definition lpeak :: "'b rel ⇒ 'b ⇒ 'b ⇒ 'b greek ⇒ bool" where
  "lpeak r a b xs ⟷ (∃as b' cs a' bs. snd ` set as ⊆ under r a ∧ b' ∈ {[(Grave,b)],[]} ∧
    snd ` set cs ⊆ under r a ∪ under r b ∧ a' ∈ {[(Acute,a)],[]} ∧
    snd ` set bs ⊆ under r b ∧ xs = as @ b' @ cs @ a' @ bs)"

definition lcliff :: "'b rel ⇒ 'b ⇒ 'b ⇒ 'b greek ⇒ bool" where
  "lcliff r a b xs ⟷ (∃as b' cs a' bs. snd ` set as ⊆ under r a ∧ b' = [(Macron,b)] ∧
    snd ` set cs ⊆ under r a ∧ a' ∈ {[(Acute,a)],[]} ∧
    snd ` set bs ⊆ under r a ∩ under r b ∧ xs = as @ b' @ cs @ a' @ bs) ∨
    (∃cs a' bs. snd ` set cs ⊆ under r a ∪ under r b ∧ a' ∈ {[(Acute,a)],[]} ∧
    snd ` set bs ⊆ under r b ∧ xs = cs @ a' @ bs)"
    
definition rcliff :: "'b rel ⇒ 'b ⇒ 'b ⇒ 'b greek ⇒ bool" where
  "rcliff r a b xs ⟷ (∃as b' cs a' bs. snd ` set as ⊆ under r a ∩ under r b ∧ b' ∈ {[(Grave,b)],[]} ∧
    snd ` set cs ⊆ under r b ∧ a' = [(Macron,a)] ∧
    snd ` set bs ⊆ under r b ∧ xs = as @ b' @ cs @ a' @ bs) ∨
    (∃as b' cs. snd ` set as ⊆ under r a ∧ b' ∈ {[(Grave,b)],[]} ∧
    snd ` set cs ⊆ under r a ∪ under r b ∧ xs = as @ b' @ cs)"

lemma dd_commute_modulo_conv[case_names wf trans peak lcliff rcliff]:
  assumes "wf r" and "trans r"
  and pk: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ R b ⟹ ∃xs. lpeak r a b xs ∧ (t, u) ∈ lconv xs"
  and lc: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ E b ⟹ ∃xs. lcliff r a b xs ∧ (t, u) ∈ lconv xs"
  and rc: "⋀a b s t u. (s, t) ∈ (E a)¯ ⟹ (s, u) ∈ R b ⟹ ∃xs. rcliff r a b xs ∧ (t, u) ∈ lconv xs"
  shows "conversion' UNIV ⊆ valley' UNIV"
proof (intro subrelI)
  fix u v
  assume "(u,v) ∈ conversion' UNIV"
  then obtain xs where "(u, v) ∈ lconv xs" by (auto intro: conversion_to_lconv[of u v])
  then show "(u, v) ∈ valley' UNIV"
  proof (induct xs rule: wf_induct[of "greek_less r"])
    case 1 thus ?case using wf_greek_less[OF ‹wf r› ‹trans r›] .
  next
    case (2 xs) show ?case
    proof (rule conversion_join_or_peak_or_cliff[of "map fst xs"])
      fix as bs cs
      assume *: "set as ⊆ {Grave}" "set bs ⊆ {Macron}" "set cs ⊆ {Acute}" "map fst xs = as @ bs @ cs"
      then show "(u, v) ∈ valley' UNIV"
      proof (elim map_eq_append_splits)
        fix as' bs' cs' bcs'
        assume as: "set as ⊆ {Grave}" "as = map fst as'" and
          bs: "set bs ⊆ {Macron}" "bs = map fst bs'" and
          cs: "set cs ⊆ {Acute}" "cs = map fst cs'" and
          xs: "xs = as' @ bcs'" "bcs' = bs' @ cs'"
        from as(1)[unfolded as(2)] have as': "⋀x y. (x,y) ∈ lconv as' ⟹ (x,y) ∈ (⋃a. R a)⇧*"
        proof (induct as')
          case (Cons x' xs)
          have "⋀x y z i. (x,y) ∈ R i ⟹ (y,z) ∈ (⋃a. R a)⇧* ⟹ (x,z) ∈ (⋃a. R a)⇧*"
          by (rule rtrancl_trans) auto
          with Cons show ?case by auto
        qed simp
        from bs(1)[unfolded bs(2)] have bs': "⋀x y. (x,y) ∈ lconv bs' ⟹ (x,y) ∈ (⋃a. E a)⇧*"
        proof (induct bs')
          case (Cons x' xs)
          have "⋀x y z i. (x,y) ∈ E i ⟹ (y,z) ∈ (⋃a. E a)⇧* ⟹ (x,z) ∈ (⋃a. E a)⇧*"
          by (rule rtrancl_trans) auto 
          with Cons show ?case by auto
        qed simp
        from cs(1)[unfolded cs(2)] have cs': "⋀x y. (x,y) ∈ lconv cs' ⟹ (x,y) ∈ ((⋃a. L a)¯)⇧*"
        proof (induct cs')
          case (Cons x' xs)
          have "⋀x y z i. (x,y) ∈ (L i)¯ ⟹ (y,z) ∈ ((⋃a. L a)¯)⇧* ⟹ (x,z) ∈ ((⋃a. L a)¯)⇧*"
          by (rule rtrancl_trans) auto 
          with Cons show ?case by auto
        qed simp
        from 2(2) as' bs' cs' show "(u, v) ∈ valley' UNIV"
        unfolding xs lconv_append by auto (meson relcomp.simps) 
      qed
    next
      fix as bs assume *: "map fst xs = as @ ([Acute] @ [Grave]) @ bs"
      {
        fix p a b q t' s' u'
        assume xs: "xs = p @ [(Acute,a),(Grave,b)] @ q" and p: "(u,t') ∈ lconv p"
          and a: "(s',t') ∈ L a" and b: "(s',u') ∈ R b" and q: "(u',v) ∈ lconv q"
        obtain js where lp: "lpeak r a b js" and js: "(t',u') ∈ lconv js" using pk[OF a b] by auto
        from lp have "(js, [(Acute,a),(Grave,b)]) ∈ greek_less r"
        unfolding lpeak_def using peak_greek_less[of _ r a _ b] by fastforce
        then have "(p @ js @ q, xs) ∈ greek_less r" unfolding xs
        by (intro greek_less_app_mono1 greek_less_app_mono2 ‹trans r›) auto
        moreover have "(u, v) ∈ lconv (p @ js @ q)"
        using p q js by auto
        ultimately have "(u, v) ∈ valley' UNIV" using 2(1) by blast
      }
      with * show "(u, v) ∈ valley' UNIV" using 2(2)
      by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp
    next
      fix as bs assume *: "map fst xs = as @ ([Acute] @ [Macron]) @ bs"
      {
        fix p a b q t' s' u'
        assume xs: "xs = p @ [(Acute,a),(Macron,b)] @ q" and p: "(u,t') ∈ lconv p"
          and a: "(s',t') ∈ L a" and b: "(s',u') ∈ E b" and q: "(u',v) ∈ lconv q"
        obtain js where lp: "lcliff r a b js" and js: "(t',u') ∈ lconv js" using lc[OF a b] by auto
        from lp have "(js, [(Acute,a),(Macron,b)]) ∈ greek_less r"
        unfolding lcliff_def
        using lcliff_greek_less1[OF ‹trans r›, of _ a _ b] lcliff_greek_less2[OF ‹trans r›, of _ a b]
        by fastforce
        then have "(p @ js @ q, xs) ∈ greek_less r" unfolding xs
        by (intro greek_less_app_mono1 greek_less_app_mono2 ‹trans r›) auto
        moreover have "(u, v) ∈ lconv (p @ js @ q)"
        using p q js by auto
        ultimately have "(u, v) ∈ valley' UNIV" using 2(1) by blast
      }
      with * show "(u, v) ∈ valley' UNIV" using 2(2)
      by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp
    next
      fix as bs assume *: "map fst xs = as @ ([Macron] @ [Grave]) @ bs"
      {
        fix p a b q t' s' u'
        assume xs: "xs = p @ [(Macron,a),(Grave,b)] @ q" and p: "(u,t') ∈ lconv p"
          and a: "(s',t') ∈ (E a)¯" and b: "(s',u') ∈ R b" and q: "(u',v) ∈ lconv q"
        obtain js where lp: "rcliff r a b js" and js: "(t',u') ∈ lconv js" using rc[OF a b] by auto
        from lp have "(js, [(Macron,a),(Grave,b)]) ∈ greek_less r"
        unfolding rcliff_def
        using rcliff_greek_less1[OF ‹trans r›, of _ a b] rcliff_greek_less2[OF ‹trans r›, of _ a _ b]
        by fastforce
        then have "(p @ js @ q, xs) ∈ greek_less r" unfolding xs
        by (intro greek_less_app_mono1 greek_less_app_mono2 ‹trans r›) auto
        moreover have "(u, v) ∈ lconv (p @ js @ q)"
        using p q js by auto
        ultimately have "(u, v) ∈ valley' UNIV" using 2(1) by blast
      }
      with * show "(u, v) ∈ valley' UNIV" using 2(2)
      by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp
    qed
  qed
qed


section ‹Results›

subsection ‹Church-Rosser modulo›

text ‹Decreasing diagrams for Church-Rosser modulo, commutation version.›

lemma dd_commute_modulo[case_names wf trans peak lcliff rcliff]:
  assumes "wf r" and "trans r"
  and pk: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ R b ⟹
    (t, u) ∈ conversion' (under r a) O (R b)⇧= O conversion' (under r a ∪ under r b) O
      ((L a)¯)⇧= O conversion' (under r b)"
  and lc: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ E b ⟹
    (t, u) ∈ conversion' (under r a) O E b O conversion' (under r a) O
      ((L a)¯)⇧= O conversion' (under r a ∩ under r b) ∨
    (t, u) ∈ conversion' (under r a ∪ under r b) O ((L a )¯)⇧= O conversion' (under r b)"
  and rc: "⋀a b s t u. (s, t) ∈ (E a)¯ ⟹ (s, u) ∈ R b ⟹
    (t, u) ∈ conversion' (under r a ∩ under r b) O (R b)⇧= O conversion' (under r b) O
      E a O conversion' (under r b) ∨
    (t, u) ∈ conversion' (under r a) O (R b)⇧= O conversion' (under r a ∪ under r b)"
  shows "conversion' UNIV ⊆ valley' UNIV"
proof (cases rule: dd_commute_modulo_conv[of r])
  case (peak a b s t u)
  {
    fix w x y z
    assume "(t, w) ∈ conversion' (under r a)"
    from conversion_to_lconv[OF this]
    obtain as where "snd ` set as ⊆ under r a" "(t, w) ∈ lconv as" by auto
    moreover assume "(w, x) ∈ (R b)⇧="
    then obtain b' where "b' ∈ {[(Grave,b)],[]}" "(w, x) ∈ lconv b'" by fastforce
    moreover assume "(x, y) ∈ conversion' (under r a ∪ under r b)"
    from conversion_to_lconv[OF this]
    obtain cs where "snd ` set cs ⊆ under r a ∪ under r b" "(x, y) ∈ lconv cs" by auto
    moreover assume "(y, z) ∈ ((L a)¯)⇧="
    then obtain a' where "a' ∈ {[(Acute,a)],[]}" "(y, z) ∈ lconv a'" by fastforce
    moreover assume "(z, u) ∈ conversion' (under r b)"
    from conversion_to_lconv[OF this]
    obtain bs where "snd ` set bs ⊆ under r b" "(z, u) ∈ lconv bs" by auto
    ultimately have "∃xs. lpeak r a b xs ∧ (t, u) ∈ lconv xs"
    by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append lpeak_def) blast
  }
  then show ?case using pk[OF peak] by blast
next
  case (lcliff a b s t u)
  {
    fix w x y z
    assume "(t, w) ∈ conversion' (under r a)"
    from conversion_to_lconv[OF this]
    obtain as where "snd ` set as ⊆ under r a" "(t, w) ∈ lconv as" by auto
    moreover assume "(w, x) ∈ E b"
    then obtain b' where "b' = [(Macron,b)]" "(w, x) ∈ lconv b'" by fastforce
    moreover assume "(x, y) ∈ conversion' (under r a)"
    from conversion_to_lconv[OF this]
    obtain cs where "snd ` set cs ⊆ under r a" "(x, y) ∈ lconv cs" by auto
    moreover assume "(y, z) ∈ ((L a)¯)⇧="
    then obtain a' where "a' ∈ {[(Acute,a)],[]}" "(y, z) ∈ lconv a'" by fastforce
    moreover assume "(z, u) ∈ conversion' (under r a ∩ under r b)"
    from conversion_to_lconv[OF this]
    obtain bs where "snd ` set bs ⊆ under r a ∩ under r b" "(z, u) ∈ lconv bs" by auto
    ultimately have "∃xs. lcliff r a b xs ∧ (t, u) ∈ lconv xs"
    by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append lcliff_def) blast
  }
  moreover {
    fix w x
    assume "(t, w) ∈ conversion' (under r a ∪ under r b)"
    from conversion_to_lconv[OF this]
    obtain cs where "snd ` set cs ⊆ under r a ∪ under r b" "(t, w) ∈ lconv cs" by auto
    moreover assume "(w, x) ∈ ((L a)¯)⇧="
    then obtain a' where "a' ∈ {[(Acute,a)],[]}" "(w, x) ∈ lconv a'" by fastforce
    moreover assume "(x, u) ∈ conversion' (under r b)"
    from conversion_to_lconv[OF this]
    obtain bs where "snd ` set bs ⊆ under r b" "(x, u) ∈ lconv bs" by auto
    ultimately have "∃xs. lcliff r a b xs ∧ (t, u) ∈ lconv xs"
    by (intro exI[of _ "cs @ a' @ bs"], unfold lconv_append lcliff_def) blast
  }
  ultimately show ?case using lc[OF lcliff] by blast
next
  case (rcliff a b s t u)
  {
    fix w x y z
    assume "(t, w) ∈ conversion' (under r a ∩ under r b)"
    from conversion_to_lconv[OF this]
    obtain as where "snd ` set as ⊆ under r a ∩ under r b" "(t, w) ∈ lconv as" by auto
    moreover assume "(w, x) ∈ (R b)⇧="
    then obtain b' where "b' ∈ {[(Grave,b)],[]}" "(w, x) ∈ lconv b'" by fastforce
    moreover assume "(x, y) ∈ conversion' (under r b)"
    from conversion_to_lconv[OF this]
    obtain cs where "snd ` set cs ⊆ under r b" "(x, y) ∈ lconv cs" by auto
    moreover assume "(y, z) ∈ E a"
    then obtain a' where "a' = [(Macron,a)]" "(y, z) ∈ lconv a'" by fastforce
    moreover assume "(z, u) ∈ conversion' (under r b)"
    from conversion_to_lconv[OF this]
    obtain bs where "snd ` set bs ⊆ under r b" "(z, u) ∈ lconv bs" by auto
    ultimately have "∃xs. rcliff r a b xs ∧ (t, u) ∈ lconv xs"
    by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append rcliff_def) blast
  }
  moreover {
    fix w x
    assume "(t, w) ∈ conversion' (under r a)"
    from conversion_to_lconv[OF this]
    obtain as where "snd ` set as ⊆ under r a" "(t, w) ∈ lconv as" by auto
    moreover assume "(w, x) ∈ (R b)⇧="
    then obtain b' where "b' ∈ {[(Grave,b)],[]}" "(w, x) ∈ lconv b'" by fastforce
    moreover assume "(x, u) ∈ conversion' (under r a ∪ under r b)"
    from conversion_to_lconv[OF this]
    obtain cs where "snd ` set cs ⊆ under r a ∪ under r b" "(x, u) ∈ lconv cs" by auto
    ultimately have "∃xs. rcliff r a b xs ∧ (t, u) ∈ lconv xs"
    by (intro exI[of _ "as @ b' @ cs"], unfold lconv_append rcliff_def) blast
  }
  ultimately show ?case using rc[OF rcliff] by blast
qed fact+

end (* context *)

text ‹Decreasing diagrams for Church-Rosser modulo.›

lemma dd_cr_modulo[case_names wf trans symE peak cliff]:
  assumes "wf r" and "trans r" and E: "⋀i. sym (E i)"
  and pk: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ L b ⟹
    (t, u) ∈ conversion' L L E (under r a) O (L b)⇧= O conversion' L L E (under r a ∪ under r b) O
      ((L a)¯)⇧= O conversion' L L E (under r b)"
  and cl: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ E b ⟹
    (t, u) ∈ conversion' L L E (under r a) O E b O conversion' L L E (under r a) O
      ((L a)¯)⇧= O conversion' L L E (under r a ∩ under r b) ∨
    (t, u) ∈ conversion' L L E (under r a ∪ under r b) O ((L a )¯)⇧= O conversion' L L E (under r b)"
  shows "conversion' L L E UNIV ⊆ valley' L L E UNIV"
proof (induct rule: dd_commute_modulo[of r])
  note E' = E[unfolded sym_conv_converse_eq]
  case (rcliff a b s t u) show ?case
    using cl[OF rcliff(2) rcliff(1)[unfolded E'], unfolded converse_iff[of t u,symmetric]]
    by (auto simp only: E' converse_inward) (auto simp only: ac_simps)
qed fact+

subsection ‹Commutation and confluence›

abbreviation "conversion'' L R M ≡ ((⋃i ∈ M. R i) ∪ (⋃i ∈ M. L i)¯)⇧*"
abbreviation "valley'' L R M ≡ (⋃i ∈ M. R i)⇧* O ((⋃i ∈ M. L i)¯)⇧*"

text ‹Decreasing diagrams for commutation.›

lemma dd_commute[case_names wf trans peak]:
  assumes "wf r" and "trans r"
  and pk: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ R b ⟹
    (t, u) ∈ conversion'' L R (under r a) O (R b)⇧= O conversion'' L R (under r a ∪ under r b) O
      ((L a)¯)⇧= O conversion'' L R (under r b)"
  shows "commute (⋃i. L i) (⋃i. R i)"
proof -
  have "((⋃i. L i)¯)⇧* O (⋃i. R i)⇧* ⊆ conversion'' L R UNIV" by regexp
  also have "… ⊆ valley'' L R UNIV"
  using dd_commute_modulo[OF assms(1,2), of L R "λ_. {}"] pk by auto
  finally show ?thesis by (simp only: commute_def)
qed

text ‹Decreasing diagrams for confluence.›

lemmas dd_cr[case_names wf trans peak] =
  dd_commute[of _ L L for L, unfolded CR_iff_self_commute[symmetric]]


subsection ‹Extended decreasing diagrams›

context
  fixes r q :: "'b rel"
  assumes "wf r" and "trans r" and "trans q" and "refl q" and compat: "r O q ⊆ r"
begin

private abbreviation (input) down :: "('b ⇒ 'a rel) ⇒ ('b ⇒ 'a rel)" where
  "down L ≡ λi. ⋃j ∈ under q i. L j"

private lemma Union_down: "(⋃i. down L i) = (⋃i. L i)"
using ‹refl q› by (auto simp: refl_on_def under_def)

text ‹Extended decreasing diagrams for commutation.›

lemma edd_commute[case_names wf transr transq reflq compat peak]:
  assumes pk: "⋀a b s t u. (s, t) ∈ L a ⟹ (s, u) ∈ R b ⟹
    (t, u) ∈ conversion'' L R (under r a) O (down R b)⇧= O conversion'' L R (under r a ∪ under r b) O
      ((down L a)¯)⇧= O conversion'' L R (under r b)"
  shows "commute (⋃i. L i) (⋃i. R i)"
unfolding Union_down[of L, symmetric] Union_down[of R, symmetric]
proof (induct rule: dd_commute[of r "down L" "down R"])
  case (peak a b s t u)
  then obtain a' b' where a': "(a', a) ∈ q" "(s, t) ∈ L a'" and b': "(b', b) ∈ q" "(s, u) ∈ R b'"
  by (auto simp: under_def)
  have "⋀a' a. (a',a) ∈ q ⟹ under r a' ⊆ under r a" using compat by (auto simp: under_def)
  then have aux1: "⋀a' a L. (a',a) ∈ q ⟹ (⋃i ∈ under r a'. L i) ⊆ (⋃i ∈ under r a. L i)" by auto
  have aux2: "⋀a' a L. (a',a) ∈ q ⟹ down L a' ⊆ down L a" 
    using ‹trans q› by (auto simp: under_def trans_def)
  have aux3: "⋀a L. (⋃i ∈ under r a. L i) ⊆ (⋃i ∈ under r a. down L i)"
    using ‹refl q› by (auto simp: under_def refl_on_def)
  from aux1[OF a'(1), of L] aux1[OF a'(1), of R] aux2[OF a'(1), of L]
       aux1[OF b'(1), of L] aux1[OF b'(1), of R] aux2[OF b'(1), of R]
       aux3[of L] aux3[of R]
  show ?case
  by (intro subsetD[OF _ pk[OF ‹(s, t) ∈ L a'› ‹(s, u) ∈ R b'›]], unfold UN_Un)
     (intro relcomp_mono rtrancl_mono Un_mono iffD2[OF converse_mono]; fast)
qed fact+

text ‹Extended decreasing diagrams for confluence.›

lemmas edd_cr[case_names wf transr transq reflq compat peak] =
  edd_commute[of L L for L, unfolded CR_iff_self_commute[symmetric]]

end (* context *)

end (* Decreasing_Diagrams_II *)