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 ⟹ ∃z∈Q. ∀y∈A. 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 "∃z∈Q. ∀y∈A. 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 "∃z∈Q. ∀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 "∃z∈Q. ∀y∈A. 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 ⟷ (∀a∈A. ∀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 ⟷ (∀a∈A. ∀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 = "{b∈A. 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 ⟷ (∀a∈A. ∀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 x≡a 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 \<^cite>‹Winkler1983›:›

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 "∀a∈A. ∀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