Theory Joinable

(* 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