# Theory Joinable

theory Joinable
imports Main
```(* Author: Joshua Schneider, ETH Zurich *)

section ‹Formalisation of idiomatic terms and lifting›

subsection ‹Immediate joinability under a relation›

theory Joinable
imports Main
begin

subsubsection ‹Definition and basic properties›

definition joinable :: "('a × 'b) set ⇒ ('a × 'a) set"
where "joinable R = {(x, y). ∃z. (x, z) ∈ R ∧ (y, z) ∈ R}"

lemma joinable_simp: "(x, y) ∈ joinable R ⟷ (∃z. (x, z) ∈ R ∧ (y, z) ∈ R)"
unfolding joinable_def by simp

lemma joinableI: "(x, z) ∈ R ⟹ (y, z) ∈ R ⟹ (x, y) ∈ joinable R"
unfolding joinable_simp by blast

lemma joinableD: "(x, y) ∈ joinable R ⟹ ∃z. (x, z) ∈ R ∧ (y, z) ∈ R"
unfolding joinable_simp .

lemma joinableE:
assumes "(x, y) ∈ joinable R"
obtains z where "(x, z) ∈ R" and "(y, z) ∈ R"
using assms unfolding joinable_simp by blast

lemma refl_on_joinable: "refl_on {x. ∃y. (x, y) ∈ R} (joinable R)"
by (auto intro!: refl_onI simp only: joinable_simp)

lemma refl_joinable_iff: "(∀x. ∃y. (x, y) ∈ R) = refl (joinable R)"
by (auto intro!: refl_onI dest: refl_onD simp add: joinable_simp)

lemma refl_joinable: "refl R ⟹ refl (joinable R)"
using refl_joinable_iff by (blast dest: refl_onD)

lemma joinable_refl: "refl R ⟹ (x, x) ∈ joinable R"
using refl_joinable by (blast dest: refl_onD)

lemma sym_joinable: "sym (joinable R)"
by (auto intro!: symI simp only: joinable_simp)

lemma joinable_sym: "(x, y) ∈ joinable R ⟹ (y, x) ∈ joinable R"
using sym_joinable by (rule symD)

lemma joinable_mono: "R ⊆ S ⟹ joinable R ⊆ joinable S"
by (rule subrelI) (auto simp only: joinable_simp)

lemma refl_le_joinable:
assumes "refl R"
shows "R ⊆ joinable R"
proof (rule subrelI)
fix x y
assume "(x, y) ∈ R"
moreover from ‹refl R› have "(y, y) ∈ R" by (blast dest: refl_onD)
ultimately show "(x, y) ∈ joinable R" by (rule joinableI)
qed

lemma joinable_subst:
assumes R_subst: "⋀x y. (x, y) ∈ R ⟹ (P x, P y) ∈ R"
assumes joinable: "(x, y) ∈ joinable R"
shows "(P x, P y) ∈ joinable R"
proof -
from joinable obtain z where xz: "(x, z) ∈ R" and yz: "(y, z) ∈ R" by (rule joinableE)
from R_subst xz have "(P x, P z) ∈ R" .
moreover from R_subst yz have "(P y, P z) ∈ R" .
ultimately show ?thesis by (rule joinableI)
qed

subsubsection ‹Confluence›

definition confluent :: "'a rel ⇒ bool"
where "confluent R ⟷ (∀x y y'. (x, y) ∈ R ∧ (x, y') ∈ R ⟶ (y, y') ∈ joinable R)"

lemma confluentI:
"(⋀x y y'. (x, y) ∈ R ⟹ (x, y') ∈ R ⟹ ∃z. (y, z) ∈ R ∧ (y', z) ∈ R) ⟹ confluent R"
unfolding confluent_def by (blast intro: joinableI)

lemma confluentD:
"confluent R ⟹ (x, y) ∈ R ⟹ (x,y') ∈ R ⟹ (y, y') ∈ joinable R"
unfolding confluent_def by blast

lemma confluentE:
assumes "confluent R" and "(x, y) ∈ R" and "(x, y') ∈ R"
obtains z where "(y, z) ∈ R" and "(y', z) ∈ R"
using assms unfolding confluent_def by (blast elim: joinableE)

lemma trans_joinable:
assumes "trans R" and "confluent R"
shows "trans (joinable R)"
proof (rule transI)
fix x y z
assume "(x, y) ∈ joinable R"
then obtain u where xu: "(x, u) ∈ R" and yu: "(y, u) ∈ R" by (rule joinableE)
assume "(y, z) ∈ joinable R"
then obtain v where yv: "(y, v) ∈ R" and zv: "(z, v) ∈ R" by (rule joinableE)
from yu yv ‹confluent R› obtain w where uw: "(u, w) ∈ R" and vw: "(v, w) ∈ R"
by (blast elim: confluentE)
from xu uw ‹trans R› have "(x, w) ∈ R" by (blast elim: transE)
moreover from zv vw ‹trans R› have "(z, w) ∈ R" by (blast elim: transE)
ultimately show "(x, z) ∈ joinable R" by (rule joinableI)
qed

subsubsection ‹Relation to reflexive transitive symmetric closure›

lemma joinable_le_rtscl: "joinable (R⇧*) ⊆ (R ∪ R¯)⇧*"
proof (rule subrelI)
fix x y
assume "(x, y) ∈ joinable (R⇧*)"
then obtain z where xz: "(x, z) ∈ R⇧*" and yz: "(y,z) ∈ R⇧*" by (rule joinableE)
from xz have "(x, z) ∈ (R ∪ R¯)⇧*" by (blast intro: in_rtrancl_UnI)
moreover from yz have "(z, y) ∈ (R ∪ R¯)⇧*" by (blast intro: in_rtrancl_UnI rtrancl_converseI)
ultimately show "(x, y) ∈ (R ∪ R¯)⇧*" by (rule rtrancl_trans)
qed

theorem joinable_eq_rtscl:
assumes "confluent (R⇧*)"
shows "joinable (R⇧*) = (R ∪ R¯)⇧*"
proof
show "joinable (R⇧*) ⊆ (R ∪ R¯)⇧*" using joinable_le_rtscl .
next
show "joinable (R⇧*) ⊇ (R ∪ R¯)⇧*" proof (rule subrelI)
fix x y
assume "(x, y) ∈ (R ∪ R¯)⇧*"
thus "(x, y) ∈ joinable (R⇧*)" proof (induction set: rtrancl)
case base
show "(x, x) ∈ joinable (R⇧*)" using joinable_refl refl_rtrancl .
next
case (step y z)
have "R ⊆ joinable (R⇧*)" using refl_le_joinable refl_rtrancl by fast
with ‹(y, z) ∈ R ∪ R¯› have "(y, z) ∈ joinable (R⇧*)" using joinable_sym by fast
with ‹(x, y) ∈ joinable (R⇧*)› show "(x, z) ∈ joinable (R⇧*)"
using trans_joinable trans_rtrancl ‹confluent (R⇧*)› by (blast dest: transD)
qed
qed
qed

subsubsection ‹Predicate version›

definition joinablep :: "('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where "joinablep P x y ⟷ (∃z. P x z ∧ P y z)"

lemma joinablep_joinable[pred_set_conv]:
"joinablep (λx y. (x, y) ∈ R) = (λx y. (x, y) ∈ joinable R)"
by (fastforce simp only: joinablep_def joinable_simp)

lemma reflp_joinablep: "reflp P ⟹ reflp (joinablep P)"
by (blast intro: reflpI joinable_refl[to_pred] refl_onI[to_pred] dest: reflpD)

lemma joinablep_refl: "reflp P ⟹ joinablep P x x"
using reflp_joinablep by (rule reflpD)

lemma reflp_le_joinablep: "reflp P ⟹ P ≤ joinablep P"
by (blast intro!: refl_le_joinable[to_pred] refl_onI[to_pred] dest: reflpD)

end
```