# Theory Partial_Order_Reduction.Relation_Extensions

```section ‹Relations›

theory Relation_Extensions
imports
Basic_Extensions
begin

abbreviation rev_lex_prod (infixr "<*rlex*>" 80)
where "r⇩1 <*rlex*> r⇩2 ≡ inv_image (r⇩2 <*lex*> r⇩1) swap"

lemmas sym_rtranclp[intro] = sym_rtrancl[to_pred]

definition liftablep :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
where "liftablep r f ≡ ∀ x y. r x y ⟶ r (f x) (f y)"

lemma liftablepI[intro]:
assumes "⋀ x y. r x y ⟹ r (f x) (f y)"
shows "liftablep r f"
using assms
unfolding liftablep_def
by simp
lemma liftablepE[elim]:
assumes "liftablep r f"
assumes "r x y"
obtains "r (f x) (f y)"
using assms
unfolding liftablep_def
by simp

lemma liftablep_rtranclp:
assumes "liftablep r f"
shows "liftablep r⇧*⇧* f"
proof
fix x y
assume "r⇧*⇧* x y"
thus "r⇧*⇧* (f x) (f y)"
using assms
by (induct rule: rtranclp_induct, force+)
qed

definition confluentp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
where "confluentp r ≡ ∀ x y1 y2. r⇧*⇧* x y1 ⟶ r⇧*⇧* x y2 ⟶ (∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z)"

lemma confluentpI[intro]:
assumes "⋀ x y1 y2. r⇧*⇧* x y1 ⟹ r⇧*⇧* x y2 ⟹ ∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z"
shows "confluentp r"
using assms
unfolding confluentp_def
by simp

lemma confluentpE[elim]:
assumes "confluentp r"
assumes "r⇧*⇧* x y1" "r⇧*⇧* x y2"
obtains z
where "r⇧*⇧* y1 z" "r⇧*⇧* y2 z"
using assms
unfolding confluentp_def
by blast

lemma confluentpI'[intro]:
assumes "⋀ x y1 y2. r⇧*⇧* x y1 ⟹ r x y2 ⟹ ∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z"
shows "confluentp r"
proof
fix x y1 y2
assume "r⇧*⇧* x y1" "r⇧*⇧* x y2"
thus "∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z" using assms by (induct rule: rtranclp_induct, force+)
qed

lemma transclp_eq_implies_confluent_imp:
assumes "r1⇧*⇧* = r2⇧*⇧*"
assumes "confluentp r1"
shows "confluentp r2"
using assms
by force

lemma transclp_eq_implies_confluent_eq:
assumes "r1⇧*⇧* = r2⇧*⇧*"
shows "confluentp r1 ⟷ confluentp r2"
using assms transclp_eq_implies_confluent_imp
by metis

definition diamondp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
where "diamondp r ≡ ∀ x y1 y2. r x y1 ⟶ r x y2 ⟶ (∃ z. r y1 z ∧ r y2 z)"

lemma diamondpI[intro]:
assumes "⋀ x y1 y2. r x y1 ⟹ r x y2 ⟹ ∃ z. r y1 z ∧ r y2 z"
shows "diamondp r"
using assms
unfolding diamondp_def
by simp

lemma diamondpE[elim]:
assumes "diamondp r"
assumes "r x y1" "r x y2"
obtains z
where "r y1 z" "r y2 z"
using assms
unfolding diamondp_def
by blast

lemma diamondp_implies_confluentp:
assumes "diamondp r"
shows "confluentp r"
proof (rule confluentpI')
fix x y1 y2
assume "r⇧*⇧* x y1" "r x y2"
hence "∃ z. r y1 z ∧ r⇧*⇧* y2 z" using assms by (induct rule: rtranclp_induct, force+)
thus "∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z" by blast
qed

locale wellfounded_relation =
fixes R :: "'a ⇒ 'a ⇒ bool"
assumes wellfounded: "wfP R"

end

```