Theory Confluence

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Properties of Binary Relations›

theory Confluence
  imports "Abstract-Rewriting.Abstract_Rewriting" "Open_Induction.Restricted_Predicates"
begin

text ‹This theory formalizes some general properties of binary relations, in particular a very weak
  sufficient condition for a relation to be Church-Rosser.›

(* Maybe one could build upon "Decreasing_Diagrams" / "Decreasing_Diagrams_II" from the AFP? *)

subsection @{const wfp_on}

(* Probably the converse direction holds, too. *)
lemma wfp_on_imp_wfP:
  assumes "wfp_on r A"
  shows "wfP (λx y. r x y  x  A  y  A)" (is "wfP ?r")
proof (simp add: wfP_def wf_def, intro allI impI)
  fix P x
  assume "x. (y. r y x  y  A  x  A  P y)  P x"
  hence *: "x. (y. x  A  y  A  r y x  P y)  P x" by blast
  from assms have **: "a. a  A  (x. x  A  (y. y  A  r y x  P y)  P x)  P a"
    by (rule wfp_on_induct) blast+
  show "P x"
  proof (cases "x  A")
    case True
    from this * show ?thesis by (rule **)
  next
    case False
    show ?thesis
    proof (rule *)
      fix y
      assume "x  A"
      with False show "P y" ..
    qed
  qed
qed

lemma wfp_onI_min:
  assumes "x Q. x  Q  Q  A  zQ. yA. r y z  y  Q"
  shows "wfp_on r A"
proof (intro inductive_on_imp_wfp_on minimal_imp_inductive_on allI impI)
  fix Q x
  assume "x  Q  Q  A"
  hence "x  Q" and "Q  A" by simp_all
  hence "zQ. yA. r y z  y  Q" by (rule assms)
  then obtain z where "z  Q" and 1: "y. y  A  r y z  y  Q" by blast
  show "zQ. y. r y z  y  Q"
  proof (intro bexI allI impI)
    fix y
    assume "r y z"
    show "y  Q"
    proof (cases "y  A")
      case True
      thus ?thesis using r y z by (rule 1)
    next
      case False
      with Q  A show ?thesis by blast
    qed
  qed fact
qed

lemma wfp_onE_min:
  assumes "wfp_on r A" and "x  Q" and "Q  A"
  obtains z where "z  Q" and "y. r y z  y  Q"
  using wfp_on_imp_minimal[OF assms(1)] assms(2, 3) by blast

lemma wfp_onI_chain: "¬ (f. i. f i  A  r (f (Suc i)) (f i))  wfp_on r A"
  by (simp add: wfp_on_def)

lemma finite_minimalE:
  assumes "finite A" and "A  {}" and "irreflp rel" and "transp rel"
  obtains a where "a  A" and "b. rel b a  b  A"
  using assms(1, 2)
proof (induct arbitrary: thesis)
  case empty
  from empty(2) show ?case by simp
next
  case (insert a A)
  show ?case
  proof (cases "A = {}")
    case True
    show ?thesis
    proof (rule insert(4))
      fix b
      assume "rel b a"
      with assms(3) show "b  insert a A" by (auto simp: True irreflp_def)
    qed simp
  next
    case False
    with insert(3) obtain z where "z  A" and *: "b. rel b z  b  A" by blast
    show ?thesis
    proof (cases "rel a z")
      case True
      show ?thesis
      proof (rule insert(4))
        fix b
        assume "rel b a"
        with assms(4) have "rel b z" using rel a z by (rule transpD)
        hence "b  A" by (rule *)
        moreover from rel b a assms(3) have "b  a" by (auto simp: irreflp_def)
        ultimately show "b  insert a A" by simp
      qed simp
    next
      case False
      show ?thesis
      proof (rule insert(4))
        fix b
        assume "rel b z"
        hence "b  A" by (rule *)
        moreover from rel b z False have "b  a" by blast
        ultimately show "b  insert a A" by simp
      next
        from z  A show "z  insert a A" by simp
      qed
    qed
  qed
qed

lemma wfp_on_finite:
  assumes "irreflp rel" and "transp rel" and "finite A"
  shows "wfp_on rel A"
proof (rule wfp_onI_min)
  fix x Q
  assume "x  Q" and "Q  A"
  from this(2) assms(3) have "finite Q" by (rule finite_subset)
  moreover from x  Q have "Q  {}" by blast
  ultimately obtain z where "z  Q" and "y. rel y z  y  Q" using assms(1, 2)
    by (rule finite_minimalE) blast
  thus "zQ. yA. rel y z  y  Q" by blast
qed

subsection ‹Relations›

locale relation = fixes r::"'a  'a  bool" (infixl "" 50)
begin

abbreviation rtc::"'a  'a  bool" (infixl "*" 50)
  where "rtc a b  r** a b"

abbreviation sc::"'a  'a  bool" (infixl "" 50)
  where "sc a b  a  b  b  a"

definition is_final::"'a  bool" where
  "is_final a  ¬ (b. r a b)"

definition srtc::"'a  'a  bool" (infixl "*" 50) where
  "srtc a b  sc** a b"
definition cs::"'a  'a  bool" (infixl "*" 50) where
  "cs a b  (s. (a * s)  (b * s))"

definition is_confluent_on :: "'a set  bool"
  where "is_confluent_on A  (aA. b1 b2. (a * b1  a * b2)  b1 * b2)"

definition is_confluent :: bool
  where "is_confluent  is_confluent_on UNIV"

definition is_loc_confluent :: bool
  where "is_loc_confluent  (a b1 b2. (a  b1  a  b2)  b1 * b2)"

definition is_ChurchRosser :: bool
  where "is_ChurchRosser  (a b. a * b  a * b)"

definition dw_closed :: "'a set  bool"
  where "dw_closed A  (aA. b. a  b  b  A)"

lemma dw_closedI [intro]:
  assumes "a b. a  A  a  b  b  A"
  shows "dw_closed A"
  unfolding dw_closed_def using assms by auto

lemma dw_closedD:
  assumes "dw_closed A" and "a  A" and "a  b"
  shows "b  A"
  using assms unfolding dw_closed_def by auto

lemma dw_closed_rtrancl:
  assumes "dw_closed A" and "a  A" and "a * b"
  shows "b  A"
  using assms(3)
proof (induct b)
  case base
  from assms(2) show ?case .
next
  case (step y z)
  from assms(1) step(3) step(2) show ?case by (rule dw_closedD)
qed

lemma dw_closed_empty: "dw_closed {}"
  by (rule, simp)

lemma dw_closed_UNIV: "dw_closed UNIV"
  by (rule, intro UNIV_I)

subsection ‹Setup for Connection to Theory @{theory "Abstract-Rewriting.Abstract_Rewriting"}

abbreviation (input) relset::"('a * 'a) set" where
  "relset  {(x, y). x  y}"

lemma rtc_rtranclI:
  assumes "a * b"
  shows "(a, b)  relset*"
using assms by (simp only: Enum.rtranclp_rtrancl_eq)

lemma final_NF: "(is_final a) = (a  NF relset)"
unfolding is_final_def NF_def by simp

lemma sc_symcl: "(a  b) = ((a, b)  relset)"
by simp

lemma srtc_conversion: "(a * b) = ((a, b)  relset*)"
proof -
  have "{(a, b). (a, b)  {(x, y). x  y}} = {(a, b). a  b}" by auto
  thus ?thesis unfolding srtc_def conversion_def sc_symcl Enum.rtranclp_rtrancl_eq by simp
qed

lemma cs_join: "(a * b) = ((a, b)  relset)"
  unfolding cs_def join_def by (auto simp add: Enum.rtranclp_rtrancl_eq rtrancl_converse)

lemma confluent_CR: "is_confluent = CR relset"
  by (auto simp add: is_confluent_def is_confluent_on_def CR_defs Enum.rtranclp_rtrancl_eq cs_join)

lemma ChurchRosser_conversion: "is_ChurchRosser = (relset*  relset)"
  by (auto simp add: is_ChurchRosser_def cs_join srtc_conversion)

lemma loc_confluent_WCR:
  shows "is_loc_confluent = WCR relset"
unfolding is_loc_confluent_def WCR_defs by (auto simp add: cs_join)

lemma wf_converse:
  shows "(wfP r^--1) = (wf (relset¯))"
unfolding wfP_def converse_def by simp

lemma wf_SN:
  shows "(wfP r^--1) = (SN relset)"
unfolding wf_converse wf_iff_no_infinite_down_chain SN_on_def by auto

subsection ‹Simple Lemmas›

lemma rtrancl_is_final:
  assumes "a * b" and "is_final a"
  shows "a = b"
proof -
  from rtranclpD[OF a * b] show ?thesis
  proof
    assume "a  b  (→)++ a b"
    hence "(→)++ a b" by simp
    from is_final a final_NF have "a  NF relset" by simp
    from NF_no_trancl_step[OF this] have "(a, b)  {(x, y). x  y}+" ..
    thus ?thesis using (→)++ a b unfolding tranclp_unfold ..
  qed
qed

lemma cs_refl:
  shows "x * x"
unfolding cs_def
proof
  show "x * x  x * x" by simp
qed

lemma cs_sym:
  assumes "x * y"
  shows "y * x"
using assms unfolding cs_def
proof
  fix z
  assume a: "x * z  y * z"
  show "s. y * s  x * s"
  proof
    from a show "y * z  x * z" by simp
  qed
qed

lemma rtc_implies_cs:
  assumes "x * y"
  shows "x * y"
proof -
  from joinI_left[OF rtc_rtranclI[OF assms]] cs_join show ?thesis by simp
qed

lemma rtc_implies_srtc:
  assumes "a * b"
  shows "a * b"
proof -
  from conversionI'[OF rtc_rtranclI[OF assms]] srtc_conversion show ?thesis by simp
qed

lemma srtc_symmetric:
  assumes "a * b"
  shows "b * a"
proof -
  from symD[OF conversion_sym[of relset], of a b] assms srtc_conversion show ?thesis by simp
qed

lemma srtc_transitive:
  assumes "a * b" and "b * c"
  shows "a * c"
proof -
  from rtranclp_trans[of "(↔)" a b c] assms show "a * c" unfolding srtc_def .
qed

lemma cs_implies_srtc:
  assumes "a * b"
  shows "a * b"
proof -
  from assms cs_join have "(a, b)  relset" by simp
  hence "(a, b)  relset*" using join_imp_conversion by auto
  thus ?thesis using srtc_conversion by simp
qed

lemma confluence_equiv_ChurchRosser: "is_confluent = is_ChurchRosser"
  by (simp only: ChurchRosser_conversion confluent_CR, fact CR_iff_conversion_imp_join)

corollary confluence_implies_ChurchRosser:
  assumes is_confluent
  shows is_ChurchRosser
  using assms by (simp only: confluence_equiv_ChurchRosser)

lemma ChurchRosser_unique_final:
  assumes "is_ChurchRosser" and "a * b1" and "a * b2" and "is_final b1" and "is_final b2"
  shows "b1 = b2"
proof -
  from is_ChurchRosser confluence_equiv_ChurchRosser confluent_CR have "CR relset" by simp
  from CR_imp_UNF[OF this] assms show ?thesis unfolding UNF_defs normalizability_def
    by (auto simp add: Enum.rtranclp_rtrancl_eq final_NF)
qed

lemma wf_on_imp_nf_ex:
  assumes "wfp_on ((→)¯¯) A" and "dw_closed A" and "a  A"
  obtains b where "a * b" and "is_final b"
proof -
  let ?A = "{bA. a * b}"
  note assms(1)
  moreover from assms(3) have "a  ?A" by simp
  moreover have "?A  A" by auto
  ultimately show ?thesis
  proof (rule wfp_onE_min)
    fix z
    assume "z  ?A" and "y. (→)¯¯ y z  y  ?A"
    from this(2) have *: "y. z  y  y  ?A" by simp
    from z  ?A have "z  A" and "a * z" by simp_all
    show thesis
    proof (rule, fact)
      show "is_final z" unfolding is_final_def
      proof
        assume "y. z  y"
        then obtain y where "z  y" ..
        hence "y  ?A" by (rule *)
        moreover from assms(2) z  A z  y have "y  A" by (rule dw_closedD)
        ultimately have "¬ (a * y)" by simp
        with rtranclp_trans[OF a * z, of y] z  y show False by auto
      qed
    qed
  qed
qed
  
lemma unique_nf_imp_confluence_on:
  assumes major: "a b1 b2. a  A  (a * b1)  (a * b2)  is_final b1  is_final b2  b1 = b2"
    and wf: "wfp_on ((→)¯¯) A" and dw: "dw_closed A"
  shows "is_confluent_on A"
  unfolding is_confluent_on_def
proof (intro ballI allI impI)
  fix a b1 b2
  assume "a * b1  a * b2"
  hence "a * b1" and "a * b2" by simp_all
  assume "a  A"
  from dw this a * b1 have "b1  A" by (rule dw_closed_rtrancl)
  from wf dw this obtain c1 where "b1 * c1" and "is_final c1" by (rule wf_on_imp_nf_ex)
  from dw a  A a * b2 have "b2  A" by (rule dw_closed_rtrancl)
  from wf dw this obtain c2 where "b2 * c2" and "is_final c2" by (rule wf_on_imp_nf_ex)
  have "c1 = c2"
    by (rule major, fact, rule rtranclp_trans[OF a * b1], fact, rule rtranclp_trans[OF a * b2], fact+)
  show "b1 * b2" unfolding cs_def
  proof (intro exI, intro conjI)
    show "b1 * c1" by fact
  next
    show "b2 * c1" unfolding c1 = c2 by fact
  qed
qed

corollary wf_imp_nf_ex:
  assumes "wfP ((→)¯¯)"
  obtains b where "a * b" and "is_final b"
proof -
  from assms have "wfp_on (r^--1) UNIV" by simp
  moreover note dw_closed_UNIV
  moreover have "a  UNIV" ..
  ultimately obtain b where "a * b" and "is_final b" by (rule wf_on_imp_nf_ex)
  thus ?thesis ..
qed

corollary unique_nf_imp_confluence:
  assumes "a b1 b2. (a * b1)  (a * b2)  is_final b1  is_final b2  b1 = b2"
    and "wfP ((→)¯¯)"
  shows "is_confluent"
  unfolding is_confluent_def
  by (rule unique_nf_imp_confluence_on, erule assms(1), assumption+, simp add: assms(2), fact dw_closed_UNIV)

end (*relation*)

subsection ‹Advanced Results and the Generalized Newman Lemma›

definition relbelow_on :: "'a set  ('a  'a  bool)  'a  ('a  'a  bool)  ('a  'a  bool)"
  where "relbelow_on A ord z rel a b  (a  A  b  A  rel a b  ord a z  ord b z)"

definition cbelow_on_1 :: "'a set  ('a  'a  bool)  'a  ('a  'a  bool)  ('a  'a  bool)"
  where "cbelow_on_1 A ord z rel  (relbelow_on A ord z rel)++"

definition cbelow_on :: "'a set  ('a  'a  bool)  'a  ('a  'a  bool)  ('a  'a  bool)"
  where "cbelow_on A ord z rel a b  (a = b  b  A  ord b z)  cbelow_on_1 A ord z rel a b"

text ‹Note that @{const cbelow_on} cannot be defined as the reflexive-transitive closure of
  @{const relbelow_on}, since it is in general not reflexive!›

definition is_loc_connective_on :: "'a set  ('a  'a  bool)  ('a  'a  bool)  bool"
  where "is_loc_connective_on A ord r  (aA. b1 b2. r a b1  r a b2  cbelow_on A ord a (relation.sc r) b1 b2)"

text ‹Note that @{const wfp_on} is @{emph ‹not›} the same as @{const SN_on}, since in the definition
  of @{const SN_on} only the @{emph ‹first›} element of the chain must be in the set.›

lemma cbelow_on_first_below:
  assumes "cbelow_on A ord z rel a b"
  shows "ord a z"
  using assms unfolding cbelow_on_def
proof
  assume "cbelow_on_1 A ord z rel a b"
  thus "ord a z" unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp add: relbelow_on_def)
qed simp

lemma cbelow_on_second_below:
  assumes "cbelow_on A ord z rel a b"
  shows "ord b z"
  using assms unfolding cbelow_on_def
proof
  assume "cbelow_on_1 A ord z rel a b"
  thus "ord b z" unfolding cbelow_on_1_def
    by (induct rule: tranclp_induct, simp_all add: relbelow_on_def)
qed simp

lemma cbelow_on_first_in:
  assumes "cbelow_on A ord z rel a b"
  shows "a  A"
  using assms unfolding cbelow_on_def
proof
  assume "cbelow_on_1 A ord z rel a b"
  thus ?thesis unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp add: relbelow_on_def)
qed simp

lemma cbelow_on_second_in:
  assumes "cbelow_on A ord z rel a b"
  shows "b  A"
  using assms unfolding cbelow_on_def
proof
  assume "cbelow_on_1 A ord z rel a b"
  thus ?thesis unfolding cbelow_on_1_def
    by (induct rule: tranclp_induct, simp_all add: relbelow_on_def)
qed simp

lemma cbelow_on_intro [intro]:
  assumes main: "cbelow_on A ord z rel a b" and "c  A" and "rel b c" and "ord c z"
  shows "cbelow_on A ord z rel a c"
proof -
  from main have "b  A" by (rule cbelow_on_second_in)
  from main show ?thesis unfolding cbelow_on_def
  proof (intro disjI2)
    assume cases: "(a = b  b  A  ord b z)  cbelow_on_1 A ord z rel a b"
    from b  A c  A rel b c ord c z cbelow_on_second_below[OF main]
      have bc: "relbelow_on A ord z rel b c" by (simp add: relbelow_on_def)
    from cases show "cbelow_on_1 A ord z rel a c"
    proof
      assume "a = b  b  A  ord b z"
      from this bc have "relbelow_on A ord z rel a c" by simp
      thus ?thesis by (simp add: cbelow_on_1_def)
    next
      assume "cbelow_on_1 A ord z rel a b"
      from this bc show ?thesis unfolding cbelow_on_1_def by (rule tranclp.intros(2))
    qed
  qed
qed

lemma cbelow_on_induct [consumes 1, case_names base step]:
  assumes a: "cbelow_on A ord z rel a b"
    and base: "a  A  ord a z  P a"
    and ind: "b c. [| cbelow_on A ord z rel a b; rel b c; c  A; ord c z; P b |] ==> P c"
  shows "P b"
  using a unfolding cbelow_on_def
proof
  assume "a = b  b  A  ord b z"
  from this base show "P b" by simp
next
  assume "cbelow_on_1 A ord z rel a b"
  thus "P b" unfolding cbelow_on_1_def
  proof (induct xa b)
    fix b
    assume "relbelow_on A ord z rel a b"
    hence "rel a b" and "a  A" and "b  A" and "ord a z" and "ord b z"
      by (simp_all add: relbelow_on_def)
    hence "cbelow_on A ord z rel a a" by (simp add: cbelow_on_def)
    from this rel a b b  A ord b z base[OF a  A ord a z] show "P b" by (rule ind)
  next
    fix b c
    assume IH: "(relbelow_on A ord z rel)++ a b" and "P b" and "relbelow_on A ord z rel b c"
    hence "rel b c" and "b  A" and "c  A" and "ord b z" and "ord c z"
      by (simp_all add: relbelow_on_def)
    from IH have "cbelow_on A ord z rel a b" by (simp add: cbelow_on_def cbelow_on_1_def)
    from this rel b c c  A ord c z P b show "P c" by (rule ind)
  qed
qed

lemma cbelow_on_symmetric:
  assumes main: "cbelow_on A ord z rel a b" and "symp rel"
  shows "cbelow_on A ord z rel b a"
  using main unfolding cbelow_on_def
proof
  assume a1: "a = b  b  A  ord b z"
  show "b = a  a  A  ord a z  cbelow_on_1 A ord z rel b a"
  proof
    from a1 show "b = a  a  A  ord a z" by simp
  qed
next
  assume a2: "cbelow_on_1 A ord z rel a b"
  show "b = a  a  A  ord a z  cbelow_on_1 A ord z rel b a"
  proof (rule disjI2)
    from symp rel have "symp (relbelow_on A ord z rel)" unfolding symp_def
    proof (intro allI impI)
      fix x y
      assume rel_sym: "x y. rel x y  rel y x"
      assume "relbelow_on A ord z rel x y"
      hence "rel x y" and "x  A" and "y  A" and "ord x z" and "ord y z"
        by (simp_all add: relbelow_on_def)
      show "relbelow_on A ord z rel y x" unfolding relbelow_on_def
      proof (intro conjI)
        from rel_sym rel x y show "rel y x" by simp
      qed fact+
    qed
    from sym_trancl[to_pred, OF this] a2 show "cbelow_on_1 A ord z rel b a"
      by (simp add: symp_def cbelow_on_1_def)
  qed
qed

lemma cbelow_on_transitive:
  assumes "cbelow_on A ord z rel a b" and "cbelow_on A ord z rel b c"
  shows "cbelow_on A ord z rel a c"
proof (induct rule: cbelow_on_induct[OF cbelow_on A ord z rel b c])
  from cbelow_on A ord z rel a b show "cbelow_on A ord z rel a b" .
next
  fix c0 c
  assume "cbelow_on A ord z rel b c0" and "rel c0 c" and "c  A" and "ord c z" and "cbelow_on A ord z rel a c0"
  show "cbelow_on A ord z rel a c" by (rule, fact+)
qed

lemma cbelow_on_mono:
  assumes "cbelow_on A ord z rel a b" and "A  B"
  shows "cbelow_on B ord z rel a b"
  using assms(1)
proof (induct rule: cbelow_on_induct)
  case base
  show ?case by (simp add: cbelow_on_def, intro disjI1 conjI, rule, fact+)
next
  case (step b c)
  from step(3) assms(2) have "c  B" ..
  from step(5) this step(2) step (4) show ?case ..
qed

locale relation_order = relation +
  fixes ord::"'a  'a  bool"
  fixes A::"'a set"
  assumes trans: "ord x y  ord y z  ord x z"
  assumes wf: "wfp_on ord A"
  assumes refines: "(→)  ord¯¯"
begin

lemma relation_refines:
  assumes "a  b"
  shows "ord b a"
  using refines assms by auto

lemma relation_wf: "wfp_on (→)¯¯ A"
  using subset_refl _ wf
proof (rule wfp_on_mono)
  fix x y
  assume "(→)¯¯ x y"
  hence "y  x" by simp
  with refines have "(ord)¯¯ y x" ..
  thus "ord x y" by simp
qed

lemma rtc_implies_cbelow_on:
  assumes "dw_closed A" and main: "a * b" and "a  A" and "ord a c"
  shows "cbelow_on A ord c (↔) a b"
  using main
proof (induct rule: rtranclp_induct)
  from assms(3) assms(4) show "cbelow_on A ord c (↔) a a" by (simp add: cbelow_on_def)
next
  fix b0 b
  assume "a * b0" and "b0  b" and IH: "cbelow_on A ord c (↔) a b0"
  from assms(1) assms(3) a * b0 have "b0  A" by (rule dw_closed_rtrancl)
  from assms(1) this b0  b have "b  A" by (rule dw_closedD)
  show "cbelow_on A ord c (↔) a b"
  proof
    from b0  b show "b0  b" by simp
  next
    from relation_refines[OF b0  b] cbelow_on_second_below[OF IH] show "ord b c" by (rule trans)
  qed fact+
qed

lemma cs_implies_cbelow_on:
  assumes "dw_closed A" and "a * b" and "a  A" and "b  A" and "ord a c" and "ord b c"
  shows "cbelow_on A ord c (↔) a b"
proof -
  from a * b obtain s where "a * s" and "b * s" unfolding cs_def by auto
  have sym: "symp (↔)" unfolding symp_def
  proof (intro allI, intro impI)
    fix x y
    assume "x  y"
    thus "y  x" by auto
  qed
  from assms(1) a * s assms(3) assms(5) have "cbelow_on A ord c (↔) a s"
    by (rule rtc_implies_cbelow_on)
  also have "cbelow_on A ord c (↔) s b"
  proof (rule cbelow_on_symmetric)
    from assms(1) b * s assms(4) assms(6) show "cbelow_on A ord c (↔) b s"
      by (rule rtc_implies_cbelow_on)
  qed fact
  finally(cbelow_on_transitive) show ?thesis .
qed

text ‹The generalized Newman lemma, taken from citeWinkler1983:›

lemma loc_connectivity_implies_confluence:
  assumes "is_loc_connective_on A ord (→)" and "dw_closed A"
  shows "is_confluent_on A"
  using assms(1) unfolding is_loc_connective_on_def is_confluent_on_def
proof (intro ballI allI impI)
  fix z x y::'a
  assume "aA. b1 b2. a  b1  a  b2  cbelow_on A ord a (↔) b1 b2"
  hence A: "a b1 b2. a  A  a  b1  a  b2  cbelow_on A ord a (↔) b1 b2" by simp
  assume "z  A" and "z * x  z * y"
  with wf show "x * y"
  proof (induct z arbitrary: x y rule: wfp_on_induct)
    fix z x y::'a
    assume IH: "z0 x0 y0. z0  A  ord z0 z  z0 * x0  z0 * y0  x0 * y0"
      and "z * x  z * y"
    hence "z * x" and "z * y" by auto
    assume "z  A"
    from converse_rtranclpE[OF z * x] obtain x1 where "x = z  (z  x1  x1 * x)" by auto
    thus "x * y"
    proof
      assume "x = z"
      show ?thesis unfolding cs_def
      proof
        from x = z z * y show "x * y  y * y" by simp
      qed
    next
      assume "z  x1  x1 * x"
      hence "z  x1" and "x1 * x" by auto
      from assms(2) z  A this(1) have "x1  A" by (rule dw_closedD)
      from converse_rtranclpE[OF z * y] obtain y1 where "y = z  (z  y1  y1 * y)" by auto
      thus ?thesis
      proof
        assume "y = z"
        show ?thesis unfolding cs_def
        proof
          from y = z z * x show "x * x  y * x" by simp
        qed
      next
        assume "z  y1  y1 * y"
        hence "z  y1" and "y1 * y" by auto
        from assms(2) z  A this(1) have "y1  A" by (rule dw_closedD)
        have "x1 * y1"
        proof (induct rule: cbelow_on_induct[OF A[OF z  A z  x1 z  y1]])
          from cs_refl[of x1] show "x1 * x1" .
        next
          fix b c
          assume "cbelow_on A ord z (↔) x1 b" and "b  c" and "c  A" and "ord c z" and "x1 * b"
          from this(1) have "b  A" by (rule cbelow_on_second_in)
          from x1 * b obtain w1 where "x1 * w1" and "b * w1" unfolding cs_def by auto
          from b  c show "x1 * c"
          proof
            assume "b  c"
            hence "b * c" by simp
            from cbelow_on A ord z (↔) x1 b have "ord b z" by (rule cbelow_on_second_below)
            from IH[OF b  A this] b * c b * w1 have "c * w1" by simp
            then obtain w2 where "c * w2" and "w1 * w2" unfolding cs_def by auto
            show ?thesis unfolding cs_def
            proof
              from rtranclp_trans[OF x1 * w1 w1 * w2] c * w2
                show "x1 * w2  c * w2" by simp
            qed
          next
            assume "c  b"
            hence "c * b" by simp
            show ?thesis unfolding cs_def
            proof
              from rtranclp_trans[OF c * b b * w1] x1 * w1
                show "x1 * w1  c * w1" by simp
            qed
          qed
        qed
        then obtain w1 where "x1 * w1" and "y1 * w1" unfolding cs_def by auto
        from IH[OF x1  A relation_refines[OF z  x1]] x1 * x x1 * w1
          have "x * w1" by simp
        then obtain v where "x * v" and "w1 * v" unfolding cs_def by auto
        from IH[OF y1  A relation_refines[OF z  y1]]
             rtranclp_trans[OF y1 * w1 w1 * v] y1 * y
          have "v * y" by simp
        then obtain w where "v * w" and "y * w" unfolding cs_def by auto
        show ?thesis unfolding cs_def
        proof
          from rtranclp_trans[OF x * v v * w] y * w show "x * w  y * w" by simp
        qed
      qed
    qed
  qed
qed

end (* relation_order *)

theorem loc_connectivity_equiv_ChurchRosser:
  assumes "relation_order r ord UNIV"
  shows "relation.is_ChurchRosser r = is_loc_connective_on UNIV ord r"
proof                                                                
  assume "relation.is_ChurchRosser r"
  show "is_loc_connective_on UNIV ord r" unfolding is_loc_connective_on_def
  proof (intro ballI allI impI)
    fix a b1 b2
    assume "r a b1  r a b2"
    hence "r a b1" and "r a b2" by simp_all
    hence "r** a b1" and "r** a b2" by simp_all
    from relation.rtc_implies_srtc[OF r** a b1] have "relation.srtc r b1 a" by (rule relation.srtc_symmetric)
    from relation.srtc_transitive[OF this relation.rtc_implies_srtc[OF r** a b2]] have "relation.srtc r b1 b2" .
    with relation.is_ChurchRosser r have "relation.cs r b1 b2" by (simp add: relation.is_ChurchRosser_def)
    from relation_order.cs_implies_cbelow_on[OF assms relation.dw_closed_UNIV this]
      relation_order.relation_refines[OF assms, of a] r a b1 r a b2
      show "cbelow_on UNIV ord a (relation.sc r) b1 b2" by simp
  qed
next
  assume "is_loc_connective_on UNIV ord r"
  from assms this relation.dw_closed_UNIV have "relation.is_confluent_on r UNIV"
    by (rule relation_order.loc_connectivity_implies_confluence)
  hence "relation.is_confluent r" by (simp only: relation.is_confluent_def)
  thus "relation.is_ChurchRosser r" by (simp add: relation.confluence_equiv_ChurchRosser)
qed

end