Theory Confluence
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.›
subsection ‹@{const wfp_on}›
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
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
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