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