Theory LS_Modularity

(*
Author:  Franziska Rapp <franziska.rapp@uibk.ac.at> (2015-2017)
Author:  Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at> (2015-2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Modularity of confluence›

theory LS_Modularity
  imports LS_General
begin

text ‹Here we instantiate the layer framework for modularity of confluence. See @{cite ‹Section 5.1› FMZvO15}.›

fun max_top_modular :: "('f × nat) set ⇒ ('f, 'v) term ⇒ ('f, 'v) mctxt" where
  "max_top_modular ℱ (Var x) = MVar x"
| "max_top_modular ℱ (Fun f ts) = (if (f, length ts) ∈ ℱ
    then MFun f (map (max_top_modular ℱ) ts)
    else MHole)"

locale modular_cr =
  fixes ℱ⇩1 ℱ⇩2 :: "('f × nat) set" and ℛ⇩1 ℛ⇩2 :: "('f, 'v :: infinite) trs"
  assumes
    wf1: "wf_trs ℛ⇩1" and wf2: "wf_trs ℛ⇩2" and
    sig1: "funas_trs ℛ⇩1 ⊆ ℱ⇩1" and sig2: "funas_trs ℛ⇩2 ⊆ ℱ⇩2" and disjoint: "ℱ⇩1 ∩ ℱ⇩2 = {}"
begin

definition 𝔏⇩1 :: "('f, 'v) mctxt set" where
  "𝔏⇩1 ≡ { C. funas_mctxt C ⊆ ℱ⇩1 }"
  
definition 𝔏⇩2 :: "('f, 'v) mctxt set" where
  "𝔏⇩2 ≡ { C. funas_mctxt C ⊆ ℱ⇩2 }"

abbreviation 𝒯⇩1 where "𝒯⇩1 ≡ { t :: ('f, 'v) term. funas_term t ⊆ ℱ⇩1 }"
abbreviation 𝒯⇩2 where "𝒯⇩2 ≡ { t :: ('f, 'v) term. funas_term t ⊆ ℱ⇩2 }"
abbreviation max_top_mod where "max_top_mod t ≡ max_top_modular ℱ⇩1 t ⊔ max_top_modular ℱ⇩2 t"


lemma modular_cr_symmetric: "modular_cr ℱ⇩2 ℱ⇩1 ℛ⇩2 ℛ⇩1"
using disjoint
by (auto simp: modular_cr_def wf1 wf2 sig1 sig2 infinite_UNIV)

lemma wf_union_trs: "wf_trs (ℛ⇩1 ∪ ℛ⇩2)"
using wf1 wf2 by (auto simp: wf_trs_def)

lemma subm_at_sig:
  fixes L :: "('f, 'v) mctxt" and p :: pos and ℱ :: "('f × nat) set"
  assumes "funas_mctxt L ⊆ ℱ" and "p ∈ all_poss_mctxt L"
  shows "funas_mctxt (subm_at L p) ⊆ ℱ"
proof
  fix f :: 'f and a :: nat 
  assume "(f, a) ∈ funas_mctxt (subm_at L p)"
  thus "(f, a) ∈ ℱ" using assms
  proof (induction "L :: ('f, 'v) mctxt" p rule: subm_at.induct)
    case (1 L) thus ?case by (induction L) auto
  next
    case (2 f' Cs i p)
    consider (i_valid) "i < List.length Cs" | (i_invalid) "i ≥ List.length Cs" 
      using not_less by auto
    thus ?thesis
    proof cases
      case i_valid
      from ‹funas_mctxt (MFun f' Cs) ⊆ ℱ› have "funas_mctxt (Cs ! i) ⊆ ℱ"
        proof -
          have "(⋃x∈set Cs. funas_mctxt x) ⊆ ℱ ⟹ i < List.length Cs ⟹ 
                funas_mctxt (Cs ! i) ⊆ ℱ" using List.nth_mem by auto
          thus ?thesis using ‹funas_mctxt (MFun f' Cs) ⊆ ℱ› i_valid
            by (induction "Cs ! i" rule: funas_mctxt.induct) auto
        qed
      moreover have "p ∈ all_poss_mctxt (Cs ! i)" using 2 by simp
      ultimately show "(f, a) ∈ ℱ" using 2 by simp
    next
      case i_invalid thus ?thesis using 2 by auto
    qed
  next
    case ("3_1" x i p) thus ?case by simp
  next
    case ("3_2" i p) thus ?case by simp
  qed
qed

lemma fun_poss_subm_at:
  assumes "p ∈ funposs_mctxt C"
  shows "∃f Cs. subm_at C p = MFun f Cs"
using assms by (induction C arbitrary: p) (auto simp: funposs_mctxt_def)

lemma fun_poss_all_poss_mctxt:
  assumes "p ∈ funposs_mctxt C"
  shows "p ∈ all_poss_mctxt C"
using assms by (induction C arbitrary: p) (auto simp: funposs_mctxt_def)

lemma subm_at_fun:
  assumes "i < length Cs"
  shows "subm_at (MFun f Cs) <i> = Cs ! i" and "<i> ∈ all_poss_mctxt (MFun f Cs)"
using assms by auto

lemma funas_sub_mctxt:
  fixes f :: 'f and Cs :: "('f, 'v) mctxt list"
  assumes "funas_mctxt (MFun f Cs) ⊆ ℱ"
          "i < length Cs"
  shows "funas_mctxt (Cs ! i) ⊆ ℱ"
using assms subm_at_fun[of i Cs f] subm_at_sig[of "MFun f Cs" ℱ "<i>"] by simp

lemma funas_sup_mctxt:
  fixes L N :: "('f, 'v) mctxt"
  assumes cmp: "(L, N) ∈ comp_mctxt" and
      funas_L: "funas_mctxt L ⊆ ℱ" and
      funas_N: "funas_mctxt N ⊆ ℱ"
  shows "funas_mctxt (L ⊔ N) ⊆ ℱ"
proof -
  have "comp_mctxtp L N" using cmp by (auto simp: comp_mctxt_def)
  thus ?thesis using funas_L funas_N
  by (induction L N rule: comp_mctxtp.induct)
     (auto simp: funas_sub_mctxt set_zip, blast)
qed

lemma modular_layer_system: "layer_system (ℱ⇩1 ∪ ℱ⇩2) (𝔏⇩1 ∪ 𝔏⇩2)"
proof
  show "𝔏⇩1 ∪ 𝔏⇩2 ⊆ layer_system_sig.𝒞 (ℱ⇩1 ∪ ℱ⇩2)"
    by (auto simp: 𝔏⇩1_def 𝔏⇩2_def layer_system_sig.𝒞_def)
next (* L1 *)
  fix t :: "('f, 'v) term"
  assume funas_t: "funas_term t ⊆ ℱ⇩1 ∪ ℱ⇩2"
  thus "∃L∈𝔏⇩1 ∪ 𝔏⇩2. L ≠ MHole ∧ L ≤ mctxt_of_term t"
  proof (cases t)
    case (Var x)
    hence cond: "mctxt_of_term t ≠ MHole ∧ mctxt_of_term t ≤ mctxt_of_term t" by simp
    have "mctxt_of_term t ∈ 𝔏⇩1 ∪ 𝔏⇩2" using Var 𝔏⇩1_def by simp
    thus ?thesis using cond by blast
  next
    case (Fun f Cs)
    let ?top = "MFun f (replicate (List.length Cs) MHole)"
    have cond: "?top ≠ MHole ∧ ?top ≤ mctxt_of_term t"
      using Fun by (auto simp: less_eq_mctxt_def o_def map_replicate_const)
    have "?top ∈ 𝔏⇩1 ∪ 𝔏⇩2" using Fun funas_t 𝔏⇩1_def 𝔏⇩2_def by simp
    thus ?thesis using cond by blast
  qed
next (* L2 *)
  fix C :: "('f, 'v) mctxt" and p :: pos and x :: 'v
  assume p_in_possC: "p ∈ poss_mctxt C"
  have "(mreplace_at C p (MVar x) ∈ 𝔏⇩1) = (mreplace_at C p MHole ∈ 𝔏⇩1)"
    using 𝔏⇩1_def p_in_possC
    by (induction C p "MVar x :: ('f, 'v) mctxt" rule: mreplace_at.induct) auto
  moreover have "(mreplace_at C p (MVar x) ∈ 𝔏⇩2) = (mreplace_at C p MHole ∈ 𝔏⇩2)"
    using 𝔏⇩2_def p_in_possC
    by (induction C p "MVar x :: ('f, 'v) mctxt" rule: mreplace_at.induct) auto
  ultimately show "(mreplace_at C p (MVar x) ∈ 𝔏⇩1 ∪ 𝔏⇩2) = (mreplace_at C p MHole ∈ 𝔏⇩1 ∪ 𝔏⇩2)" by auto
next (* L3 *)
  fix L N :: "('f, 'v) mctxt" and p :: pos
  assume L_in_𝔏: "L ∈ 𝔏⇩1 ∪ 𝔏⇩2" and
         N_in_𝔏: "N ∈ 𝔏⇩1 ∪ 𝔏⇩2" and 
         "p ∈ funposs_mctxt L" and 
         comp_context:"(subm_at L p, N) ∈ comp_mctxt"
  consider "L ∈ 𝔏⇩1" | "L ∈ 𝔏⇩2" using L_in_𝔏 by auto
  thus "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏⇩1 ∪ 𝔏⇩2"
  proof cases
    case 1
    hence root_in_ℱ⇩1: "the (root_mctxt (subm_at L p)) ∈ ℱ⇩1" 
      using ‹p ∈ funposs_mctxt L› fun_poss_subm_at[of p L] subm_at_sig[of L ℱ⇩1 p]
            𝔏⇩1_def fun_poss_all_poss_mctxt[of p L]
      by auto
    from this obtain f :: 'f and Cs :: "('f, 'v) mctxt list"
    where "comp_mctxtp (MFun f Cs) N" and "(f, length Cs) ∈ ℱ⇩1" 
      using comp_context fun_poss_subm_at[of p L] ‹p ∈ funposs_mctxt L›
      by (auto simp: comp_mctxt_def)
    hence "N ∈ 𝔏⇩1" using 𝔏⇩1_def N_in_𝔏
    proof (induction "(MFun f Cs)" N arbitrary: f Cs rule: comp_mctxtp.induct)
      case (MHole2 f Cs) thus ?case by simp
    next
      case (MFun f g Cs Ds)
        thus ?case using MFun 𝔏⇩2_def disjoint by auto
    qed
    hence "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏⇩1" 
      using 1 𝔏⇩1_def ‹p ∈ funposs_mctxt L› fun_poss_all_poss_mctxt[of p L] 
            subm_at_sig[of L ℱ⇩1 p] comp_context funas_sup_mctxt[of "subm_at L p" N ℱ⇩1]
            funas_mctxt_mreplace_at[of p L "subm_at L p ⊔ N"]
      by blast
    thus ?thesis by simp
  next
    case 2 (* analogously to case 1 *)
    hence root_in_ℱ⇩2: "the (root_mctxt (subm_at L p)) ∈ ℱ⇩2" 
      using ‹p ∈ funposs_mctxt L› fun_poss_subm_at[of p L] subm_at_sig[of L ℱ⇩2 p]
            𝔏⇩2_def fun_poss_all_poss_mctxt[of p L]
      by auto
    from this obtain f :: 'f and Cs :: "('f, 'v) mctxt list"
    where "comp_mctxtp (MFun f Cs) N" and "(f, length Cs) ∈ ℱ⇩2" 
      using comp_context fun_poss_subm_at[of p L] ‹p ∈ funposs_mctxt L›
      by (auto simp: comp_mctxt_def)
    hence "N ∈ 𝔏⇩2" using 𝔏⇩2_def N_in_𝔏
    proof (induction "(MFun f Cs)" N arbitrary: f Cs rule: comp_mctxtp.induct)
      case (MHole2 f Cs) thus ?case by simp
    next
      case (MFun f g Cs Ds)
        thus ?case using MFun 𝔏⇩1_def disjoint by auto
    qed
    hence "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏⇩2" 
      using 2 𝔏⇩2_def ‹p ∈ funposs_mctxt L› fun_poss_all_poss_mctxt[of p L] 
            subm_at_sig[of L ℱ⇩2 p] comp_context funas_sup_mctxt[of "subm_at L p" N ℱ⇩2]
            funas_mctxt_mreplace_at[of p L "subm_at L p ⊔ N"]
      by blast
    thus ?thesis by simp
  qed
qed

interpretation layer_system "ℱ⇩1 ∪ ℱ⇩2" "𝔏⇩1 ∪ 𝔏⇩2" using modular_layer_system .

lemma sig_subset_layers: "F⇩1 ⊆ F⇩2 ⟹ {C. funas_mctxt C = F⇩1} ⊆ {C. funas_mctxt C ⊆ F⇩2}"
by auto

context
begin

interpretation z : modular_cr ℱ⇩1 "{}" "{}" "{} :: ('f, 'v) trs" 
  by standard (auto simp: infinite_UNIV wf_trs_def)

interpretation x : layer_system ℱ⇩1 𝔏⇩1
  using z.modular_layer_system 
        Un_absorb2[of "{C :: ('f,'v) mctxt. funas_mctxt C = {}}" 
                      "{C. funas_mctxt C ⊆ ℱ⇩1}", OF sig_subset_layers]
  unfolding z.𝔏⇩1_def z.𝔏⇩2_def by auto

lemma max_top_modular_in_layers1: "max_top_modular ℱ⇩1 t ∈ z.𝔏⇩1"
using 𝔏⇩1_def by (induction t) auto

lemma top_less_eq1: "max_top_modular ℱ⇩1 t ≤ mctxt_of_term t"
proof (induction t)
  case (Var x) thus ?case by simp
next
  case (Fun f ts) thus ?case using less_eq_mctxt_intros(3)[of _ "(map mctxt_of_term ts)"] by simp
qed

lemma max_top_modular_correct1: "max_top_modular ℱ⇩1 t = layer_system_sig.max_top 𝔏⇩1 t"
proof (induction t)
  case (Var x) thus ?case using x.max_top_var by simp
next
  case (Fun f ts) thus ?case
  proof (cases "(f, length ts) ∈ ℱ⇩1")
    case True
    { fix L
      assume "L ∈ z.𝔏⇩1" and "L ≤ MFun f (map mctxt_of_term ts)"
      hence "L ≤ MFun f (map (max_top_modular ℱ⇩1) ts)"
        using Fun.IH x.max_topC_props(2) x.topsC_def z.funas_sub_mctxt
        by (cases L) (auto elim!: less_eq_mctxtE1 intro!: less_eq_mctxtI1 simp: z.𝔏⇩1_def)
    }
    hence less_than_max_top_modular: "L ∈ z.𝔏⇩1 ∧ L ≤ MFun f (map mctxt_of_term ts)
            ⟶ L ≤ MFun f (map (max_top_modular ℱ⇩1) ts)" for L by auto
    have unfold_max_top_mod: "max_top_modular ℱ⇩1 (Fun f ts) = MFun f (map (max_top_modular ℱ⇩1) ts)"
      by (simp add: True)
    hence in_𝔏⇩1: "MFun f (map (max_top_modular ℱ⇩1) ts) ∈ z.𝔏⇩1"
      by (metis (full_types) max_top_modular_in_layers1)
    have is_top: "MFun f (map (max_top_modular ℱ⇩1) ts) ≤ MFun f (map mctxt_of_term ts)"
      using unfold_max_top_mod by (metis (full_types) mctxt_of_term.simps(2) top_less_eq1)
    have max_top_lt_max_top_mod: "(THE m. m ∈ x.tops (Fun f ts) ∧ 
         (∀ma. ma ∈ x.tops (Fun f ts) ⟶ ma ≤ m)) ≤ MFun f (map (max_top_modular ℱ⇩1) ts)"
      using less_than_max_top_modular x.max_topC_def x.max_topC_props(1) x.topsC_def by force
    have "MFun f (map (max_top_modular ℱ⇩1) ts) ≤ x.max_topC (MFun f (map mctxt_of_term ts))"
      using is_top in_𝔏⇩1 by (simp add: x.topsC_def)
    thus ?thesis
      using max_top_lt_max_top_mod unfold_max_top_mod by (simp add: Ball_def_raw x.max_topC_def)
  next
    case False 
    hence "length cs = length ts ⟶ MFun f cs ∉ z.𝔏⇩1" for cs using 𝔏⇩1_def by simp
    hence "L ∈ z.𝔏⇩1 ∧ L ≤ MFun f (map mctxt_of_term ts) ⟶ L = MHole" for L 
      by (auto elim: less_eq_mctxt_MFunE2)
    thus ?thesis using Fun False x.max_topC_def x.topsC_def
      bot.extremum_uniqueI x.max_topC_props(1) by fastforce
  qed
qed
end

context
begin
interpretation z : modular_cr "{}" ℱ⇩2 "{}" "{} :: ('f, 'v) trs" 
  by standard (auto simp: infinite_UNIV wf_trs_def)
interpretation x : layer_system ℱ⇩2 𝔏⇩2
  using z.modular_layer_system 
        Un_absorb1[of "{C :: ('f,'v) mctxt. funas_mctxt C = {}}"
                      "{C. funas_mctxt C ⊆ ℱ⇩2}", OF sig_subset_layers]
  unfolding z.𝔏⇩1_def z.𝔏⇩2_def by auto

lemma max_top_modular_in_layers2: "max_top_modular ℱ⇩2 t ∈ z.𝔏⇩2"
using 𝔏⇩2_def by (induction t) auto

lemma top_less_eq2: "max_top_modular ℱ⇩2 t ≤ mctxt_of_term t"
proof (induction t)
  case (Var x) thus ?case by simp
next
  case (Fun f ts) thus ?case using less_eq_mctxt_intros(3)[of _ "(map mctxt_of_term ts)"] by simp
qed

lemma max_top_modular_correct2: "max_top_modular ℱ⇩2 t = layer_system_sig.max_top 𝔏⇩2 t"
proof (induction t)
  case (Var x) thus ?case using x.max_top_var by simp
next
  case (Fun f ts) thus ?case
  proof (cases "(f, length ts) ∈ ℱ⇩2")
    case True
    hence less_than_max_top_modular: "L ∈ z.𝔏⇩2 ∧ L ≤ MFun f (map mctxt_of_term ts)
            ⟶ L ≤ MFun f (map (max_top_modular ℱ⇩2) ts)" for L
      using Fun.IH x.max_top_props(2) x.topsC_def z.funas_sub_mctxt
      by (cases L) (auto elim!: less_eq_mctxtE1 intro!: less_eq_mctxtI1 simp: z.𝔏⇩2_def)
    hence unfold_max_top_mod: "max_top_modular ℱ⇩2 (Fun f ts) = MFun f (map (max_top_modular ℱ⇩2) ts)"
      by (simp add: True)
    hence in_𝔏⇩2: "MFun f (map (max_top_modular ℱ⇩2) ts) ∈ z.𝔏⇩2"
      by (metis (full_types) max_top_modular_in_layers2)
    have is_top: "MFun f (map (max_top_modular ℱ⇩2) ts) ≤ MFun f (map mctxt_of_term ts)"
      using unfold_max_top_mod by (metis (full_types) mctxt_of_term.simps(2) top_less_eq2)
    have max_top_lt_max_top_mod: "(THE m. m ∈ x.tops (Fun f ts) ∧ 
         (∀ma. ma ∈ x.tops (Fun f ts) ⟶ ma ≤ m)) ≤ MFun f (map (max_top_modular ℱ⇩2) ts)"
      using less_than_max_top_modular x.max_topC_def x.max_topC_props(1) x.topsC_def by force
    have "MFun f (map (max_top_modular ℱ⇩2) ts) ≤ x.max_topC (MFun f (map mctxt_of_term ts))"
      using is_top in_𝔏⇩2 by (simp add: x.topsC_def)
    thus ?thesis
      using max_top_lt_max_top_mod unfold_max_top_mod by (simp add: Ball_def_raw x.max_topC_def)
  next
    case False 
    hence "length cs = length ts ⟶ MFun f cs ∉ z.𝔏⇩2" for cs using 𝔏⇩2_def by simp
    hence "L ∈ z.𝔏⇩2 ∧ L ≤ MFun f (map mctxt_of_term ts) ⟶ L = MHole" for L 
      by (auto elim: less_eq_mctxt_MFunE2)
    thus ?thesis using Fun False x.max_topC_def x.topsC_def
      bot.extremum_uniqueI x.max_topC_props(1) by fastforce
  qed
qed
end

lemma L_not_in_𝔏⇩2: 
  assumes f_in_ℱ⇩1: "(f, length ts) ∈ ℱ⇩1"
  shows "(L ∈ 𝔏⇩1 ∨ L ∈ 𝔏⇩2) ∧ L ≤ MFun f (map mctxt_of_term ts) 
            ⟷ L ∈ 𝔏⇩1 ∧ L ≤ MFun f (map mctxt_of_term ts)"
proof (cases "L ≤ MFun f (map mctxt_of_term ts)")
  case True thus ?thesis
  proof (cases "L")
    case MVar thus ?thesis using 𝔏⇩1_def by auto
  next
    case MHole thus ?thesis using 𝔏⇩1_def by auto
  next
    case (MFun f' Cs) 
    hence "f' = f" using True less_eq_mctxt_MFunE2 by fastforce
    hence "length ts = length Cs" 
      using True MFun less_eq_mctxt_MFunE2 length_map mctxt.distinct(5) mctxt.inject(2)
      by metis
    hence "(f', length Cs) ∉ ℱ⇩2" using MFun f_in_ℱ⇩1 disjoint ‹f' = f› by auto
    hence "L ∉ 𝔏⇩2" using MFun 𝔏⇩2_def disjoint by auto
    thus ?thesis by simp
  qed
next
  case False thus ?thesis by simp
qed

lemma max_top_modular_correct_ℱ⇩1: "(f, n) ∈ ℱ⇩1 ⟹ length ts = n ⟹ 
      max_top_modular ℱ⇩1 (Fun f ts) = max_top (Fun f ts) ∧ max_top_modular ℱ⇩2 (Fun f ts) = MHole"
using max_top_modular_correct1[of "Fun f ts"] disjoint 
by (auto simp: layer_system_sig.max_topC_def layer_system_sig.topsC_def L_not_in_𝔏⇩2)

lemma L_not_in_𝔏⇩1: 
  assumes f_in_ℱ⇩1: "(f, length ts) ∈ ℱ⇩2"
  shows "(L ∈ 𝔏⇩1 ∨ L ∈ 𝔏⇩2) ∧ L ≤ MFun f (map mctxt_of_term ts) 
            ⟷ L ∈ 𝔏⇩2 ∧ L ≤ MFun f (map mctxt_of_term ts)"
proof (cases "L ≤ MFun f (map mctxt_of_term ts)")
  case True thus ?thesis
  proof (cases "L")
    case MVar thus ?thesis using 𝔏⇩2_def by auto
  next
    case MHole thus ?thesis using 𝔏⇩2_def by auto
  next
    case (MFun f' Cs) 
    hence "f' = f" using True less_eq_mctxt_MFunE2 by fastforce
    hence "length ts = length Cs" 
      using True MFun less_eq_mctxt_MFunE2 length_map mctxt.distinct(5) mctxt.inject(2)
      by metis
    hence "(f', length Cs) ∉ ℱ⇩1" using MFun f_in_ℱ⇩1 disjoint ‹f' = f› by auto
    hence "L ∉ 𝔏⇩1" using MFun 𝔏⇩1_def disjoint by auto
    thus ?thesis by simp
  qed
next
  case False thus ?thesis by simp
qed

lemma max_top_modular_correct_ℱ⇩2: "(f, n) ∈ ℱ⇩2 ⟹ length ts = n ⟹ 
      max_top_modular ℱ⇩2 (Fun f ts) = max_top (Fun f ts) ∧ max_top_modular ℱ⇩1 (Fun f ts) = MHole"
using max_top_modular_correct2[of "Fun f ts"] disjoint 
by (auto simp: layer_system_sig.max_topC_def layer_system_sig.topsC_def L_not_in_𝔏⇩1)

lemma max_top_var_weak1:
  "max_top t = MVar x ⟷ Var x = t"
by (metis (no_types, lifting) less_eq_mctxt_MVarE1 max_topC_props(1)  
    max_top_var mem_Collect_eq term_of_mctxt_mctxt_of_term_id topsC_def)

(* important lemma *)
lemma max_top_modular_correct:
  shows "max_top t = max_top_mod t"
proof (cases t)
  case (Var x) thus ?thesis using max_top_var by simp
next
  case (Fun f ts)
  thus ?thesis 
  proof (cases "(f, length ts) ∈ (ℱ⇩1 ∪ ℱ⇩2)")
    case True thus ?thesis using max_top_modular_correct_ℱ⇩1[of f "length ts"] disjoint
          max_top_modular_correct_ℱ⇩2[of f "length ts"] sup_mctxt.simps(1) sup_mctxt_MHole
          Fun by auto
  next
    case False
    hence not_MVar: "∀x. max_top t ≠ MVar x" 
      using Fun max_topC_def topsC_def 𝔏⇩1_def 𝔏⇩2_def max_top_var_weak1 term.simps(4) 
      by fastforce
    { fix Cs :: "('f, 'v) mctxt list"
      assume "length Cs = length ts"
      hence "(f, length Cs) ∉ ℱ⇩1 ∪ ℱ⇩2" using False 𝔏⇩1_def 𝔏⇩2_def by simp
      hence "MFun f Cs ∉ 𝔏⇩1 ∪ 𝔏⇩2" using 𝔏⇩1_def 𝔏⇩2_def funas_mctxt.simps(1)[of f Cs] by blast
    }
    hence "max_top t = MHole" using False Fun not_MVar max_topC_def topsC_def 
          less_eq_mctxt_MFunE2 max_topC_props(1) length_map mctxt_of_term.simps(2) mem_Collect_eq
      by (metis (no_types, lifting))
    thus ?thesis using Fun False by auto
  qed
qed

lemma var_some_subst_correct:
  assumes "funas_term t ⊆ ℱ" 
  shows "mctxt_term_conv (max_top_modular ℱ t) = t ⋅ (Var ∘ Some)"
using assms by (induction t) auto

lemma subm_at_max_top_modular_consistent:
  assumes "subm_at (max_top_modular ℱ⇩1 t) p = C" and
          "p ∈ poss_mctxt (max_top_modular ℱ⇩1 t)"
  shows "max_top_modular ℱ⇩1 (t |_ p) = C"
using assms
by (induct t p rule: subt_at.induct) auto

text ‹main lemma for condition C_1 in proof of layered›
lemma lemma_C⇩1:
  fixes p :: pos and s t :: "('f, 'v) term" and r and σ
  assumes "s ∈ 𝒯" and "t ∈ 𝒯" and "p ∈ funposs_mctxt (max_top s)" and
          rstep_s_t: "(s, t) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p σ" and
          s_def_t_def: "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "r ∈ ℛ⇩1 ∪ ℛ⇩2" and
          p_def: "p = hole_pos C" and
          root_s: "∃f ts. s = Fun f ts ∧ (f, length ts) ∈ ℱ⇩1"
  shows "∃τ. (mctxt_term_conv (max_top s), mctxt_term_conv (max_top t)) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ ∨
             (mctxt_term_conv (max_top s), mctxt_term_conv MHole) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ"
proof -
  let ?M = "max_top s" and ?L = "max_top t"
  obtain f ts where "s = Fun f ts" and root_s: "root s = Some (f, length ts)"
                   and f_in_ℱ⇩1: "(f, length ts) ∈ ℱ⇩1" using root_s by auto
  hence max_top_mod_ℱ⇩1: "max_top_modular ℱ⇩1 s = max_top s" 
    using max_top_modular_correct_ℱ⇩1 by blast
  let ?mtm = "λt. mctxt_term_conv (max_top_modular ℱ⇩1 t)"
  have p_funposs_max_top: "p ∈ funposs_mctxt (max_top_modular ℱ⇩1 s)" 
    using max_top_mod_ℱ⇩1 ‹p ∈ funposs_mctxt ?M› by simp
  hence p_in_poss_max_top: "p ∈ all_poss_mctxt (max_top_modular ℱ⇩1 C⟨t⟩)" for t
    unfolding s_def_t_def p_def using funposs_mctxt_subset_all_poss_mctxt[of "max_top_modular ℱ⇩1 t"]
    by (induct C) (auto simp: funposs_mctxt_def 
        nth_append_length[of "map f xs" for f xs, unfolded length_map] split: if_splits)
  moreover have funas_max_top_ℱ⇩1: "funas_term (?mtm C⟨t⟩) ⊆ ℱ⇩1" for t
    using 𝔏⇩1_def max_top_modular_in_layers1 by simp
  ultimately have "∃D. (∀t. ?mtm C⟨t⟩ = D⟨?mtm t⟩) ∧ hole_pos C = hole_pos D"
   unfolding s_def_t_def p_def
  proof (induction C)
    case Hole thus ?case by (metis ctxt_apply_term.simps(1) hole_pos.simps(1))
  next
    case (More g ss1 C' ss2)
    from More(2)[of undefined] have "(g, Suc (length ss1 + length ss2)) ∈ ℱ⇩1"
      by (auto split: if_splits)
    with More show ?case
      by (auto simp: funposs_mctxt_def 
          nth_append_length[of "map f xs" for f xs, unfolded length_map])
         (metis ctxt_apply_term.simps(2) hole_pos.simps(2) length_map)
  qed
  then obtain D where D_assm: "∀t. ?mtm C⟨t⟩ = D⟨?mtm t⟩" and "hole_pos C = hole_pos D" by auto
  have push_in_subst: "funas_term t' ⊆ ℱ⇩1 ⟶ ?mtm (t' ⋅ σ) = t' ⋅ (?mtm ∘ σ)" for t'
  by (induction t') auto
  have funas_r_ℱ⇩1:"funas_term (fst r) ⊆ ℱ⇩1 ∧ funas_term (snd r) ⊆ ℱ⇩1"
  proof (cases "r ∈ ℛ⇩1")
    case True thus ?thesis
    using sig1 lhs_wf[of "fst r" "snd r"] rhs_wf[of "fst r" "snd r"] by simp
  next
    case False
    hence "r ∈ ℛ⇩2" using ‹r ∈ ℛ⇩1 ∪ ℛ⇩2› by simp
    then obtain f' ts' where l_def: "fst r = Fun f' ts'" using wf2 wf_trs_def by (metis prod.collapse)
    hence f'_in_ℱ⇩2: "(f', length ts') ∈ ℱ⇩2" using sig2
      by (metis ‹r ∈ ℛ⇩2› contra_subsetD defined_def defined_funas_trs prod.collapse root.simps(2))
    have p_in_poss: "p ∈ poss_mctxt ?M"
      using ‹p ∈ funposs_mctxt ?M› funposs_mctxt_subset_poss_mctxt by auto
    have max_top_MHole: "max_top_modular ℱ⇩1 (fst r ⋅ σ) = MHole"
      using max_top_modular_correct_ℱ⇩2[OF f'_in_ℱ⇩2] l_def by simp
    have "p ∉ funposs_mctxt (max_top_modular ℱ⇩1 s)"
    proof
      assume "p ∈ funposs_mctxt (max_top_modular ℱ⇩1 s)"
      then obtain f' ts' where "subm_at (max_top_modular ℱ⇩1 s) p = MFun f' ts'"
        using fun_poss_subm_at by blast
      thus False using max_top_MHole max_top_mod_ℱ⇩1 p_def p_in_poss 
                       s_def_t_def(1) subm_at_max_top_modular_consistent by fastforce
    qed
    thus ?thesis using p_funposs_max_top by auto
  qed
  hence part2: "?mtm (fst r ⋅ σ) = fst r ⋅ (?mtm ∘ σ)" using push_in_subst by simp
  have part3: "snd r ⋅ (?mtm ∘ σ) = ?mtm (snd r ⋅ σ)"
    using push_in_subst funas_r_ℱ⇩1 by simp
  have part4: "?mtm C⟨snd r ⋅ σ⟩ = D⟨?mtm (snd r ⋅ σ)⟩" using D_assm by auto
  have first_half: "mctxt_term_conv (max_top s) = D⟨fst r ⋅ (?mtm ∘ σ)⟩"
    using s_def_t_def(1) max_top_mod_ℱ⇩1 D_assm part2 by metis
  have second_half: "D⟨snd r ⋅ (?mtm ∘ σ)⟩ = mctxt_term_conv (max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩))"
    using part3 part4 D_assm by metis
  hence "(mctxt_term_conv (max_top C⟨fst r ⋅ σ⟩), 
                      mctxt_term_conv (max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩))) 
                                 ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p (?mtm ∘ σ)" 
    using max_top_mod_ℱ⇩1 first_half rstep_s_t ‹r ∈ (ℛ⇩1 ∪ ℛ⇩2)› 
          ‹hole_pos C = hole_pos D› p_def
    by (metis rstep_r_p_s'.rstep_r_p_s' s_def_t_def(1))
  hence W: "∃ τ. max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩) ∈ 𝔏⇩1 ∪ 𝔏⇩2 ∧
            (mctxt_term_conv ?M, mctxt_term_conv (max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩))) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ"
    using max_top_modular_in_layers1 Un_iff s_def_t_def(1) [folded p_def] by blast
  then obtain τ where step_to_L: "(mctxt_term_conv ?M, mctxt_term_conv 
                (max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩))) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ" by auto
  thus ?thesis
  proof (cases "max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩)")
    case MHole thus ?thesis using step_to_L by auto
  next
    case (MVar x)
    hence "p = ε" using step_to_L all_poss_mctxt.simps(1) p_in_poss_max_top
      by (metis singletonD)
    then obtain y where "snd r = Var y" and "Var y ⋅ τ = Var (Some x)"
      using MVar step_to_L rstep_r_p_s'.cases subst_apply_eq_Var 
            ctxt_supteq supteq_var_imp_eq mctxt_term_conv.simps(2)
      by (metis (no_types, lifting))
    hence "max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩) = max_top t"
    using s_def_t_def(2)
      by (metis less_eq_mctxt_MVarE1 local.MVar max_top_var mctxt_of_term.simps(1) top_less_eq1) 
    thus ?thesis using step_to_L by auto
  next
    case MFun
    then obtain f ts where t_def: "t = Fun f ts"
      using s_def_t_def(2) max_top_modular.simps by (cases t) auto
    hence "(f, length ts) ∈ ℱ⇩1"
      using ‹t ∈ 𝒯› 𝒯_def disjoint max_top_modular_correct_ℱ⇩2 MFun s_def_t_def(2)
      by auto
    hence "max_top_modular ℱ⇩1 (C⟨snd r ⋅ σ⟩) = max_top t"
      using max_top_modular_correct_ℱ⇩1 s_def_t_def(2) t_def by simp
    thus ?thesis using step_to_L by auto
  qed
qed


interpretation layered "ℱ⇩1 ∪ ℱ⇩2" "𝔏⇩1 ∪ 𝔏⇩2" "ℛ⇩1 ∪ ℛ⇩2"
text ‹done (Franziska)›
proof (* trs *)
  show "wf_trs (ℛ⇩1 ∪ ℛ⇩2)" using wf1 wf2 by (auto simp: wf_trs_def)
next (* ℛ_sig *)
  show "funas_trs (ℛ⇩1 ∪ ℛ⇩2) ⊆ ℱ⇩1 ∪ ℱ⇩2" using sig1 sig2 by auto
next (* C1 *)
  fix p :: pos and s t :: "('f, 'v) term" and r and σ
  let ?M = "max_top s" and ?L = "max_top t"
  assume assms: "s ∈ 𝒯" "t ∈ 𝒯" "p ∈ funposs_mctxt ?M" and
         rstep_s_t: "(s, t) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p σ"
  then obtain C where
    s_def_t_def: "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "r ∈ ℛ⇩1 ∪ ℛ⇩2" and
    p_def: "p = hole_pos C"
    by auto
  show "∃τ. (mctxt_term_conv ?M, mctxt_term_conv ?L) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ ∨
            (mctxt_term_conv ?M, mctxt_term_conv MHole) ∈ rstep_r_p_s' (ℛ⇩1 ∪ ℛ⇩2) r p τ"
  proof -
    consider "∃f ts. s = Fun f ts ∧ (f, length ts) ∈ ℱ⇩1" 
           | "∃f ts. s = Fun f ts ∧ (f, length ts) ∈ ℱ⇩2"
           | "∃x. s = Var x" using ‹s ∈ 𝒯› 𝒯_def by (cases s) auto
    thus ?thesis
    proof cases
      case 1 thus ?thesis using lemma_C⇩1 assms rstep_s_t s_def_t_def p_def by auto
    next
      case 2 thus ?thesis using modular_cr.lemma_C⇩1[OF modular_cr_symmetric] assms
                                rstep_s_t s_def_t_def p_def
        by (metis inf_sup_aci(5) modular_cr.𝔏⇩1_def modular_cr.𝔏⇩2_def modular_cr_axioms modular_cr_symmetric)
    next
      case 3 thus ?thesis 
      using rstep_s_t wf_union_trs NF_Var[of "ℛ⇩1 ∪ ℛ⇩2"] rstep_eq_rstep' 
            rstep'_iff_rstep_r_p_s' prod.collapse
      by metis
    qed
  qed
next (* C2 *)
  fix L N :: "('f, 'v) mctxt" and p :: pos
  assume N_in_𝔏: "N ∈ 𝔏⇩1 ∪ 𝔏⇩2" and
         L_in_𝔏: "L ∈ 𝔏⇩1 ∪ 𝔏⇩2" and 
         "L ≤ N" and
         "p ∈ hole_poss L"
  consider "N ∈ 𝔏⇩1" | "N ∈ 𝔏⇩2" using N_in_𝔏 by auto
  thus "mreplace_at L p (subm_at N p) ∈ 𝔏⇩1 ∪ 𝔏⇩2"
  proof cases
    case 1
    hence "L ∈ 𝔏⇩1" using ‹L ≤ N› 𝔏⇩1_def by auto
    have "p ∈ all_poss_mctxt N"
      using ‹p ∈ hole_poss L› ‹L ≤ N› all_poss_mctxt_conv all_poss_mctxt_mono[of L N]
      by auto
    hence "mreplace_at L p (subm_at N p) ∈ 𝔏⇩1"
      using 1 ‹p ∈ hole_poss L› ‹L ≤ N› ‹L ∈ 𝔏⇩1› 𝔏⇩1_def
      proof (induction "N :: ('f, 'v) mctxt" p rule: subm_at.induct)
        case (2 f Cs i p)
        hence "funas_mctxt (MFun f Cs) ⊆ ℱ⇩1" by simp
        hence "funas_mctxt (subm_at (MFun f Cs) (i <# p)) ⊆ ℱ⇩1" 
          using subm_at_sig[of "MFun f Cs" ℱ⇩1 "i <# p"] 2 by simp
        thus ?case using 2
          proof (induction L "(i <# p)" 
               "(subm_at (MFun f Cs) (i <# p)) :: ('f, 'v) mctxt"
                rule: mreplace_at.induct)
            case (2 f' Cs') thus ?case 
            using funas_mctxt_mreplace_at_hole[of "i <# p" "MFun f' Cs'" 
                                               "subm_at (MFun f Cs) (i <# p)"] by auto
          qed auto
      qed auto
    thus ?thesis by simp
  next
    case 2 (* analogously to case 1 *)
    hence "L ∈ 𝔏⇩2" using ‹L ≤ N› 𝔏⇩2_def by auto
    have "p ∈ all_poss_mctxt N"
      using ‹p ∈ hole_poss L› ‹L ≤ N› all_poss_mctxt_conv all_poss_mctxt_mono[of L N]
      by auto
    hence "mreplace_at L p (subm_at N p) ∈ 𝔏⇩2"
      using 2 ‹p ∈ hole_poss L› ‹L ≤ N› ‹L ∈ 𝔏⇩2› 𝔏⇩2_def
      proof (induction "N :: ('f, 'v) mctxt" p rule: subm_at.induct)
        case (2 f Cs i p)
        hence "funas_mctxt (MFun f Cs) ⊆ ℱ⇩2" by simp
        hence "funas_mctxt (subm_at (MFun f Cs) (i <# p)) ⊆ ℱ⇩2" 
          using subm_at_sig[of "MFun f Cs" ℱ⇩2 "i <# p"] 2 by simp
        thus ?case using 2
          proof (induction L "(i <# p)" 
               "(subm_at (MFun f Cs) (i <# p)) :: ('f, 'v) mctxt"
                rule: mreplace_at.induct)
            case (2 f' Cs') thus ?case
            using funas_mctxt_mreplace_at_hole[of "i <# p" "MFun f' Cs'" 
                                               "subm_at (MFun f Cs) (i <# p)"] by auto
          qed auto
      qed auto
    thus ?thesis by simp
  qed
qed

lemma conserv_subst: "funas_term (t ⋅ σ) ⊆ ℱ ⟹ funas_term t ⊆ ℱ"
proof -
  assume "funas_term (t ⋅ σ) ⊆ ℱ"
  from this show "funas_term t ⊆ ℱ"
  proof (induction t)
    case (Var x) thus ?case by simp
  next
    case (Fun f Cs) thus ?case using funas_term_subst by blast
  qed
qed

lemma conserv_T1:
  assumes "a ∈ 𝒯⇩1"
  shows "(a, b) ∈ rstep ℛ⇩1 ⟹ b ∈ 𝒯⇩1"
proof -
  assume "(a, b) ∈ rstep ℛ⇩1"
  from this and assms show "b ∈ 𝒯⇩1"
  proof (induction rule: rstep_induct)
    case (IH C σ l r)
    hence "funas_rule (l, r) ⊆ ℱ⇩1" using sig1 by (auto simp: funas_trs_def)
    hence "funas_term r ⊆ ℱ⇩1" by (auto simp: funas_rule_def)
    have "vars_term r ⊆ vars_term l" using IH wf1 by (simp add: wf_trs_def)
    thus ?case using IH ‹funas_term r ⊆ ℱ⇩1› by (auto simp: funas_term_subst) blast
  qed
qed

lemma incomparable_T1R2:
  assumes a_in_T1: "a ∈ 𝒯⇩1"
  shows "(a, b) ∉ rstep ℛ⇩2"
proof
  assume "(a, b) ∈ rstep ℛ⇩2"
  from this and assms show False
  proof (induction rule: rstep.induct)
    case (rule a b) 
      hence "a ∈ 𝒯⇩2" using sig2 funas_rule_def[of "(a, b)"] by (auto simp: funas_trs_def)
      hence is_var_a: "∃v. a = Var v" using rule disjoint 
      proof (induction a)
        case (Var x) thus ?case by simp
      next
        case (Fun f Cs) 
          hence False by auto 
          thus ?case by simp
      qed
      thus ?case using rule is_var_a wf2 by (auto simp: wf_trs_def)
  next
    case (subst a b σ) thus ?case using conserv_subst[of a σ ℱ⇩1] by simp
  next
    case ctxt thus ?case by simp
  qed
qed

thm rtrancl_induct
thm converse_rtrancl_induct

lemma conserv_star_T1:
  assumes "(a, b) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*" and "a ∈ 𝒯⇩1"
  shows "b ∈ 𝒯⇩1"
using assms conserv_T1
by (induction rule: converse_rtrancl_induct) (auto simp: rstep_union incomparable_T1R2)

lemma unapplicable_T1R2:
  assumes "(a, b) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*" and "a ∈ 𝒯⇩1"
  shows "(a, b) ∈ (rstep ℛ⇩1)⇧*"
using assms conserv_T1 incomparable_T1R2
by (induction rule: converse_rtrancl_induct) (auto simp: rstep_union)

lemma unapplicable_T2R1:
  assumes "(a, b) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*" and "a ∈ 𝒯⇩2"
  shows "(a, b) ∈ (rstep ℛ⇩2)⇧*"
using assms modular_cr.unapplicable_T1R2[OF modular_cr_symmetric]
by (auto simp: ac_simps)

lemma rstep_union_sub: "(rstep ℛ⇩1)⇧* ⊆ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧* ∧ (rstep ℛ⇩2)⇧* ⊆ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*"
 by (simp add: rstep_union rtrancl_mono)

lemma CR_on_union:
  assumes CR1: "CR_on (rstep ℛ⇩1) 𝒯⇩1"
  and CR2: "CR_on (rstep ℛ⇩2) 𝒯⇩2"
  shows "CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) { t. mctxt_of_term t ∈ 𝔏⇩1 ∪ 𝔏⇩2 }"
text ‹done (Franziska)›
proof
  fix a b c
  assume a_in_L1L2:"a ∈ {t. mctxt_of_term t ∈ 𝔏⇩1 ∪ 𝔏⇩2}" 
         and a_to_b: "(a, b) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*"
         and a_to_c: "(a, c) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*"
  hence "a ∈ {t. mctxt_of_term t ∈ 𝔏⇩1} ∨ a ∈ {t. mctxt_of_term t ∈ 𝔏⇩2}" by simp
  then consider "a ∈ {t. mctxt_of_term t ∈ 𝔏⇩1}" | "a ∈ {t. mctxt_of_term t ∈ 𝔏⇩2}" by rule
  thus "(b, c) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧↓"
  proof cases
      case 1
      hence "a ∈ 𝒯⇩1" using 𝔏⇩1_def by simp
      hence a_to_b_R1:"(a, b) ∈ (rstep ℛ⇩1)⇧*" and a_to_c_R1:"(a, c) ∈ (rstep ℛ⇩1)⇧*" 
        using a_to_b a_to_c by (auto simp: unapplicable_T1R2)
      hence "(b, c) ∈ (rstep ℛ⇩1)⇧↓" 
        using CR1 ‹a ∈ 𝒯⇩1› CR_on_def[of "rstep ℛ⇩1" 𝒯⇩1] by simp
      thus ?thesis using rstep_union_sub joinD[of b c "rstep ℛ⇩1"] by auto
    next
      case 2
      hence "a ∈ 𝒯⇩2" using 𝔏⇩2_def by simp
      hence a_to_b_R2:"(a, b) ∈ (rstep ℛ⇩2)⇧*" and a_to_c_R2:"(a, c) ∈ (rstep ℛ⇩2)⇧*"
        using a_to_b a_to_c by (auto simp: unapplicable_T2R1)
      hence "(b, c) ∈ (rstep ℛ⇩2)⇧↓" 
        using CR2 ‹a ∈ 𝒯⇩2› a_to_b_R2 a_to_c_R2 CR_on_def[of "rstep ℛ⇩2" 𝒯⇩2] by simp
      thus ?thesis using rstep_union_sub joinD[of b c "rstep ℛ⇩2"] by auto
  qed
qed                                                            

lemma CR_mod1:
  assumes CR_union: "CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) 𝒯"
  shows "CR_on (rstep ℛ⇩1) 𝒯⇩1"
proof -
  have "𝒯⇩1 ⊆ 𝒯" unfolding 𝒯_def by auto
  hence "CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) 𝒯⇩1" unfolding CR_defs
        using CR_union CR_onI[of 𝒯⇩1 ℛ⇩1] CR_defs[of "rstep (ℛ⇩1 ∪ ℛ⇩2)" 𝒯] by auto
  have "(⋀a b c. a ∈ 𝒯⇩1 ⟹ (a, b) ∈ (rstep ℛ⇩1)⇧* ⟹ (a, c) ∈ (rstep ℛ⇩1)⇧*
           ⟹ (b, c) ∈ (rstep ℛ⇩1)⇧↓)"
  proof -
    fix a b c
    assume a_T1: "a ∈ 𝒯⇩1" and ab_R1: "(a, b) ∈ (rstep ℛ⇩1)⇧*" 
                          and ac_R1: "(a, c) ∈ (rstep ℛ⇩1)⇧*"
    hence "(b, c) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧↓" using ‹CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) 𝒯⇩1›
          by (meson CR_on_def rstep_union_sub subset_eq)
    then obtain d 
         where join_R1R2:"(b, d) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧* ∧ (c, d) ∈ (rstep (ℛ⇩1 ∪ ℛ⇩2))⇧*" 
         using joinD by auto
    have "b ∈ 𝒯⇩1" using a_T1 ab_R1 conserv_star_T1[of a b] rstep_union_sub by auto
    have "c ∈ 𝒯⇩1" using a_T1 ac_R1 conserv_star_T1[of a c] rstep_union_sub by auto
    show "(b, c) ∈ (rstep ℛ⇩1)⇧↓" 
      using join_R1R2 ‹b ∈ 𝒯⇩1› ‹c ∈ 𝒯⇩1› unapplicable_T1R2[of b d] 
            unapplicable_T1R2[of c d] rtrancl_converseD
      by auto
  qed
  thus ?thesis using CR_onI[of 𝒯⇩1 "(rstep ℛ⇩1)"] by simp
qed

lemmas CR_mod2 = modular_cr.CR_mod1[OF modular_cr_symmetric]

text ‹The following lemma establishes the easy direction of modularity of confluence.›
lemma CR_mod':
  assumes CR_union: "CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) 𝒯"
  shows "CR_on (rstep ℛ⇩1) 𝒯⇩1" and "CR_on (rstep ℛ⇩2) 𝒯⇩2"
  by (auto simp: assms CR_mod1 CR_mod2 sup_commute)

text ‹The following lemma is the interesting direction of modularity of confluence @{cite ‹Theorem 5.1› FMZvO15}.›
lemma CR_mod:
  assumes "CR_on (rstep ℛ⇩1) 𝒯⇩1"  "CR_on (rstep ℛ⇩2) 𝒯⇩2"
  shows "CR_on (rstep (ℛ⇩1 ∪ ℛ⇩2)) 𝒯"
  using assms by (rule CR[OF CR_on_union])

end

text ‹As a test, we show that modularity implies signature extension.›

lemma CR_on_imp_CR:
  fixes ℛ :: "('f, 'v :: infinite) trs"
  assumes "wf_trs ℛ" and "funas_trs ℛ ⊆ ℱ"
  and "CR_on (rstep ℛ) { t :: ('f, 'v) term. funas_term t ⊆ ℱ }"
  shows "CR (rstep ℛ)"
proof -
  define ℱ⇩c where "ℱ⇩c = { (f,n). (f,n) ∉ ℱ }"
  hence disjoint_1: "ℱ ∩ ℱ⇩c = {}" by auto
  have *: "layer_system_sig.𝒯 (ℱ ∪ ℱ⇩c) = UNIV" by (auto simp: ℱ⇩c_def layer_system_sig.𝒯_def)
  have mod_cr: "modular_cr ℱ ℱ⇩c ℛ {}" using assms disjoint_1 wf_trs_def
    by (metis Int_lower2 empty_iff funas_empty modular_cr.intro)
  have CR_empty: "CR_on (rstep {}) { t :: ('f, 'v) term. funas_term t ⊆ ℱ⇩c }" by fastforce
  thus ?thesis using modular_cr.CR_on_union[OF mod_cr assms(3) CR_empty] modular_cr.CR_mod
    by (metis * assms(3) mod_cr sup_bot.right_neutral)
qed

end