(* Title: ResiduatedTransitionSystem Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2022 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter "Residuated Transition Systems" theory ResiduatedTransitionSystem imports Main begin section "Basic Definitions and Properties" subsection "Partial Magmas" text ‹ A \emph{partial magma} consists simply of a partial binary operation. We represent the partiality by assuming the existence of a unique value ‹null› that behaves as a zero for the operation. › (* * TODO: This is currently identical with Category3.partial_magma. * This may get to be a problem for future theories that develop category-theoretic * properties of residuated transition systems, but for now I don't want this theory * to depend on the Category3 session just because of this. *) locale partial_magma = fixes OP :: "'a ⇒ 'a ⇒ 'a" assumes ex_un_null: "∃!n. ∀t. OP n t = n ∧ OP t n = n" begin definition null :: 'a where "null = (THE n. ∀t. OP n t = n ∧ OP t n = n)" lemma null_eqI: assumes "⋀t. OP n t = n ∧ OP t n = n" shows "n = null" using assms null_def ex_un_null the1_equality [of "λn. ∀t. OP n t = n ∧ OP t n = n"] by auto lemma null_is_zero [simp]: shows "OP null t = null" and "OP t null = null" using null_def ex_un_null theI' [of "λn. ∀t. OP n t = n ∧ OP t n = n"] by auto end subsection "Residuation" text ‹ A \emph{residuation} is a partial magma subject to three axioms. The first, ‹con_sym_ax›, states that the domain of a residuation is symmetric. The second, ‹con_imp_arr_resid›, constrains the results of residuation either to be ‹null›, which indicates inconsistency, or something that is self-consistent, which we will define below to be an ``arrow''. The ``cube axiom'', ‹cube_ax›, states that if ‹v› can be transported by residuation around one side of the ``commuting square'' formed by ‹t› and ‹u \ t›, then it can also be transported around the other side, formed by ‹u› and ‹t \ u›, with the same result. › type_synonym 'a resid = "'a ⇒ 'a ⇒ 'a" locale residuation = partial_magma resid for resid :: "'a resid" (infix "\\" 70) + assumes con_sym_ax: "t \\ u ≠ null ⟹ u \\ t ≠ null" and con_imp_arr_resid: "t \\ u ≠ null ⟹ (t \\ u) \\ (t \\ u) ≠ null" and cube_ax: "(v \\ t) \\ (u \\ t) ≠ null ⟹ (v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)" begin text ‹ The axiom ‹cube_ax› is equivalent to the following unconditional form. The locale assumptions use the weaker form to avoid having to treat the case ‹(v \ t) \ (u \ t) = null› specially for every interpretation. › lemma cube: shows "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)" using cube_ax by metis text ‹ We regard ‹t› and ‹u› as \emph{consistent} if the residuation ‹t \ u› is defined. It is convenient to make this a definition, with associated notation. › definition con (infix "⌢" 50) where "t ⌢ u ≡ t \\ u ≠ null" lemma conI [intro]: assumes "t \\ u ≠ null" shows "t ⌢ u" using assms con_def by blast lemma conE [elim]: assumes "t ⌢ u" and "t \\ u ≠ null ⟹ T" shows T using assms con_def by simp lemma con_sym: assumes "t ⌢ u" shows "u ⌢ t" using assms con_def con_sym_ax by blast text ‹ We call ‹t› an \emph{arrow} if it is self-consistent. › definition arr where "arr t ≡ t ⌢ t" lemma arrI [intro]: assumes "t ⌢ t" shows "arr t" using assms arr_def by simp lemma arrE [elim]: assumes "arr t" and "t ⌢ t ⟹ T" shows T using assms arr_def by simp lemma not_arr_null [simp]: shows "¬ arr null" by (auto simp add: con_def) lemma con_implies_arr: assumes "t ⌢ u" shows "arr t" and "arr u" using assms by (metis arrI con_def con_imp_arr_resid cube null_is_zero(2))+ lemma arr_resid [simp]: assumes "t ⌢ u" shows "arr (t \\ u)" using assms con_imp_arr_resid by blast lemma arr_resid_iff_con: shows "arr (t \\ u) ⟷ t ⌢ u" by auto lemma con_arr_self [simp]: assumes "arr f" shows "f ⌢ f" using assms arrE by auto lemma not_con_null [simp]: shows "con null t = False" and "con t null = False" by auto text ‹ The residuation of an arrow along itself is the \emph{canonical target} of the arrow. › definition trg where "trg t ≡ t \\ t" lemma resid_arr_self: shows "t \\ t = trg t" using trg_def by auto text ‹ An \emph{identity} is an arrow that is its own target. › definition ide where "ide a ≡ a ⌢ a ∧ a \\ a = a" lemma ideI [intro]: assumes "a ⌢ a" and "a \\ a = a" shows "ide a" using assms ide_def by auto lemma ideE [elim]: assumes "ide a" and "⟦a ⌢ a; a \\ a = a⟧ ⟹ T" shows T using assms ide_def by blast lemma ide_implies_arr [simp]: assumes "ide a" shows "arr a" using assms by blast lemma not_ide_null [simp]: shows "ide null = False" by auto end subsection "Residuated Transition System" text ‹ A \emph{residuated transition system} consists of a residuation subject to additional axioms that concern the relationship between identities and residuation. These axioms make it possible to sensibly associate with each arrow certain nonempty sets of identities called the \emph{sources} and \emph{targets} of the arrow. Axiom ‹ide_trg› states that the canonical target ‹trg t› of an arrow ‹t› is an identity. Axiom ‹resid_arr_ide› states that identities are right units for residuation, when it is defined. Axiom ‹resid_ide_arr› states that the residuation of an identity along an arrow is again an identity, assuming that the residuation is defined. Axiom ‹con_imp_coinitial_ax› states that if arrows ‹t› and ‹u› are consistent, then there is an identity that is consistent with both of them (\emph{i.e.}~they have a common source). Axiom ‹con_target› states that an identity of the form ‹t \ u› (which may be regarded as a ``target'' of ‹u›) is consistent with any other arrow ‹v \ u› obtained by residuation along ‹u›. We note that replacing the premise ‹ide (t \ u)› in this axiom by either ‹arr (t \ u)› or ‹t ⌢ u› would result in a strictly stronger statement. › locale rts = residuation + assumes ide_trg [simp]: "arr t ⟹ ide (trg t)" and resid_arr_ide: "⟦ide a; t ⌢ a⟧ ⟹ t \\ a = t" and resid_ide_arr [simp]: "⟦ide a; a ⌢ t⟧ ⟹ ide (a \\ t)" and con_imp_coinitial_ax: "t ⌢ u ⟹ ∃a. ide a ∧ a ⌢ t ∧ a ⌢ u" and con_target: "⟦ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u" begin text ‹ We define the \emph{sources} of an arrow ‹t› to be the identities that are consistent with ‹t›. › definition sources where "sources t = {a. ide a ∧ t ⌢ a}" text ‹ We define the \emph{targets} of an arrow ‹t› to be the identities that are consistent with the canonical target ‹trg t›. › definition targets where "targets t = {b. ide b ∧ trg t ⌢ b}" lemma in_sourcesI [intro, simp]: assumes "ide a" and "t ⌢ a" shows "a ∈ sources t" using assms sources_def by simp lemma in_sourcesE [elim]: assumes "a ∈ sources t" and "⟦ide a; t ⌢ a⟧ ⟹ T" shows T using assms sources_def by auto lemma in_targetsI [intro, simp]: assumes "ide b" and "trg t ⌢ b" shows "b ∈ targets t" using assms targets_def resid_arr_self by simp lemma in_targetsE [elim]: assumes "b ∈ targets t" and "⟦ide b; trg t ⌢ b⟧ ⟹ T" shows T using assms targets_def resid_arr_self by force lemma trg_in_targets: assumes "arr t" shows "trg t ∈ targets t" using assms by (meson ideE ide_trg in_targetsI) lemma source_is_ide: assumes "a ∈ sources t" shows "ide a" using assms by blast lemma target_is_ide: assumes "a ∈ targets t" shows "ide a" using assms by blast text ‹ Consistent arrows have a common source. › lemma con_imp_common_source: assumes "t ⌢ u" shows "sources t ∩ sources u ≠ {}" using assms by (meson disjoint_iff in_sourcesI con_imp_coinitial_ax con_sym) text ‹ Arrows are characterized by the property of having a nonempty set of sources, or equivalently, by that of having a nonempty set of targets. › lemma arr_iff_has_source: shows "arr t ⟷ sources t ≠ {}" using con_imp_common_source con_implies_arr(1) sources_def by blast lemma arr_iff_has_target: shows "arr t ⟷ targets t ≠ {}" using trg_def trg_in_targets by fastforce text ‹ The residuation of a source of an arrow along that arrow gives a target of the same arrow. However, it is \emph{not} true that every target of an arrow ‹t› is of the form ‹u \ t› for some ‹u› with ‹t ⌢ u›. › lemma resid_source_in_targets: assumes "a ∈ sources t" shows "a \\ t ∈ targets t" by (metis arr_resid assms con_target con_sym resid_arr_ide ide_trg in_sourcesE resid_ide_arr in_targetsI resid_arr_self) text ‹ Residuation along an identity reflects identities. › lemma ide_backward_stable: assumes "ide a" and "ide (t \\ a)" shows "ide t" by (metis assms ideE resid_arr_ide arr_resid_iff_con) lemma resid_reflects_con: assumes "t ⌢ v" and "u ⌢ v" and "t \\ v ⌢ u \\ v" shows "t ⌢ u" using assms cube by (elim conE) auto lemma con_transitive_on_ide: assumes "ide a" and "ide b" and "ide c" shows "⟦a ⌢ b; b ⌢ c⟧ ⟹ a ⌢ c" using assms by (metis resid_arr_ide con_target con_sym) lemma sources_are_con: assumes "a ∈ sources t" and "a' ∈ sources t" shows "a ⌢ a'" using assms by (metis (no_types, lifting) CollectD con_target con_sym resid_ide_arr sources_def resid_reflects_con) lemma sources_con_closed: assumes "a ∈ sources t" and "ide a'" and "a ⌢ a'" shows "a' ∈ sources t" using assms by (metis (no_types, lifting) con_target con_sym resid_arr_ide mem_Collect_eq sources_def) lemma sources_eqI: assumes "sources t ∩ sources t' ≠ {}" shows "sources t = sources t'" using assms sources_def sources_are_con sources_con_closed by blast (* 3 sec *) lemma targets_are_con: assumes "b ∈ targets t" and "b' ∈ targets t" shows "b ⌢ b'" using assms sources_are_con sources_def targets_def by blast lemma targets_con_closed: assumes "b ∈ targets t" and "ide b'" and "b ⌢ b'" shows "b' ∈ targets t" using assms sources_con_closed sources_def targets_def by blast lemma targets_eqI: assumes "targets t ∩ targets t' ≠ {}" shows "targets t = targets t'" using assms targets_def targets_are_con targets_con_closed by blast (* 2 sec *) text ‹ Arrows are \emph{coinitial} if they have a common source, and \emph{coterminal} if they have a common target. › definition coinitial where "coinitial t u ≡ sources t ∩ sources u ≠ {}" definition coterminal where "coterminal t u ≡ targets t ∩ targets u ≠ {}" lemma coinitialI [intro]: assumes "arr t" and "sources t = sources u" shows "coinitial t u" using assms coinitial_def arr_iff_has_source by simp lemma coinitialE [elim]: assumes "coinitial t u" and "⟦arr t; arr u; sources t = sources u⟧ ⟹ T" shows T using assms coinitial_def sources_eqI arr_iff_has_source by auto lemma con_imp_coinitial: assumes "t ⌢ u" shows "coinitial t u" using assms by (simp add: coinitial_def con_imp_common_source) lemma coinitial_iff: shows "coinitial t t' ⟷ arr t ∧ arr t' ∧ sources t = sources t'" by (metis arr_iff_has_source coinitial_def inf_idem sources_eqI) lemma coterminal_iff: shows "coterminal t t' ⟷ arr t ∧ arr t' ∧ targets t = targets t'" by (metis arr_iff_has_target coterminal_def inf_idem targets_eqI) lemma coterminal_iff_con_trg: shows "coterminal t u ⟷ trg t ⌢ trg u" by (metis coinitial_iff con_imp_coinitial coterminal_iff in_targetsE trg_in_targets resid_arr_self arr_resid_iff_con sources_def targets_def) lemma coterminalI [intro]: assumes "arr t" and "targets t = targets u" shows "coterminal t u" using assms coterminal_iff arr_iff_has_target by auto lemma coterminalE [elim]: assumes "coterminal t u" and "⟦arr t; arr u; targets t = targets u⟧ ⟹ T" shows T using assms coterminal_iff by auto lemma sources_resid [simp]: assumes "t ⌢ u" shows "sources (t \\ u) = targets u" unfolding targets_def trg_def using assms conI conE by (metis con_imp_arr_resid assms coinitial_iff con_imp_coinitial cube ex_un_null sources_def) lemma targets_resid_sym: assumes "t ⌢ u" shows "targets (t \\ u) = targets (u \\ t)" using assms apply (intro targets_eqI) by (metis (no_types, opaque_lifting) assms cube inf_idem arr_iff_has_target arr_def arr_resid_iff_con sources_resid) text ‹ Arrows ‹t› and ‹u› are \emph{sequential} if the set of targets of ‹t› equals the set of sources of ‹u›. › definition seq where "seq t u ≡ arr t ∧ arr u ∧ targets t = sources u" lemma seqI [intro]: shows "⟦arr t; targets t = sources u⟧ ⟹ seq t u" and "⟦arr u; targets t = sources u⟧ ⟹ seq t u" using seq_def arr_iff_has_source arr_iff_has_target by metis+ lemma seqE [elim]: assumes "seq t u" and "⟦arr t; arr u; targets t = sources u⟧ ⟹ T" shows T using assms seq_def by blast subsubsection "Congruence of Transitions" text ‹ Residuation induces a preorder ‹≲› on transitions, defined by ‹t ≲ u› if and only if ‹t \ u› is an identity. › abbreviation prfx (infix "≲" 50) where "t ≲ u ≡ ide (t \\ u)" lemma prfxE: assumes "t ≲ u" and "ide (t \\ u) ⟹ T" shows T using assms by fastforce lemma prfx_implies_con: assumes "t ≲ u" shows "t ⌢ u" using assms arr_resid_iff_con by blast lemma prfx_reflexive: assumes "arr t" shows "t ≲ t" by (simp add: assms resid_arr_self) lemma prfx_transitive [trans]: assumes "t ≲ u" and "u ≲ v" shows "t ≲ v" using assms con_target resid_ide_arr ide_backward_stable cube conI by metis lemma source_is_prfx: assumes "a ∈ sources t" shows "a ≲ t" using assms resid_source_in_targets by blast text ‹ The equivalence ‹∼› associated with ‹≲› is substitutive with respect to residuation. › abbreviation cong (infix "∼" 50) where "t ∼ u ≡ t ≲ u ∧ u ≲ t" lemma congE: assumes "t ∼ u " and "⟦t ⌢ u; ide (t \\ u); ide (u \\ t)⟧ ⟹ T" shows T using assms prfx_implies_con by blast lemma cong_reflexive: assumes "arr t" shows "t ∼ t" using assms prfx_reflexive by simp lemma cong_symmetric: assumes "t ∼ u" shows "u ∼ t" using assms by simp lemma cong_transitive [trans]: assumes "t ∼ u" and "u ∼ v" shows "t ∼ v" using assms prfx_transitive by auto lemma cong_subst_left: assumes "t ∼ t'" and "t ⌢ u" shows "t' ⌢ u" and "t \\ u ∼ t' \\ u" apply (meson assms con_sym con_target prfx_implies_con resid_reflects_con) by (metis assms con_sym con_target cube prfx_implies_con resid_ide_arr resid_reflects_con) lemma cong_subst_right: assumes "u ∼ u'" and "t ⌢ u" shows "t ⌢ u'" and "t \\ u ∼ t \\ u'" proof - have 1: "t ⌢ u' ∧ t \\ u' ⌢ u \\ u' ∧ (t \\ u) \\ (u' \\ u) = (t \\ u') \\ (u \\ u')" using assms cube con_sym con_target cong_subst_left(1) by meson show "t ⌢ u'" using 1 by simp show "t \\ u ∼ t \\ u'" by (metis 1 arr_resid_iff_con assms(1) cong_reflexive resid_arr_ide) qed lemma cong_implies_coinitial: assumes "u ∼ u'" shows "coinitial u u'" using assms con_imp_coinitial prfx_implies_con by simp lemma cong_implies_coterminal: assumes "u ∼ u'" shows "coterminal u u'" using assms by (metis con_implies_arr(1) coterminalI ideE prfx_implies_con sources_resid targets_resid_sym) lemma ide_imp_con_iff_cong: assumes "ide t" and "ide u" shows "t ⌢ u ⟷ t ∼ u" using assms by (metis con_sym resid_ide_arr prfx_implies_con) lemma sources_are_cong: assumes "a ∈ sources t" and "a' ∈ sources t" shows "a ∼ a'" using assms sources_are_con by (metis CollectD ide_imp_con_iff_cong sources_def) lemma sources_cong_closed: assumes "a ∈ sources t" and "a ∼ a'" shows "a' ∈ sources t" using assms sources_def by (meson in_sourcesE in_sourcesI cong_subst_right(1) ide_backward_stable) lemma targets_are_cong: assumes "b ∈ targets t" and "b' ∈ targets t" shows "b ∼ b'" using assms(1-2) sources_are_cong sources_def targets_def by blast lemma targets_cong_closed: assumes "b ∈ targets t" and "b ∼ b'" shows "b' ∈ targets t" using assms targets_def sources_cong_closed sources_def by blast lemma targets_char: shows "targets t = {b. arr t ∧ t \\ t ∼ b}" unfolding targets_def by (metis (no_types, lifting) con_def con_implies_arr(2) con_sym cong_reflexive ide_def resid_arr_ide trg_def) lemma coinitial_ide_are_cong: assumes "ide a" and "ide a'" and "coinitial a a'" shows "a ∼ a'" using assms coinitial_def by (metis ideE in_sourcesI coinitialE sources_are_cong) lemma cong_respects_seq: assumes "seq t u" and "cong t t'" and "cong u u'" shows "seq t' u'" by (metis assms coterminalE rts.coinitialE rts.cong_implies_coinitial rts.cong_implies_coterminal rts_axioms seqE seqI) end subsection "Weakly Extensional RTS" text ‹ A \emph{weakly extensional} RTS is an RTS that satisfies the additional condition that identity arrows have trivial congruence classes. This axiom has a number of useful consequences, including that each arrow has a unique source and target. › locale weakly_extensional_rts = rts + assumes weak_extensionality: "⟦t ∼ u; ide t; ide u⟧ ⟹ t = u" begin lemma con_ide_are_eq: assumes "ide a" and "ide a'" and "a ⌢ a'" shows "a = a'" using assms ide_imp_con_iff_cong weak_extensionality by blast lemma coinitial_ide_are_eq: assumes "ide a" and "ide a'" and "coinitial a a'" shows "a = a'" using assms coinitial_def con_ide_are_eq by blast lemma arr_has_un_source: assumes "arr t" shows "∃!a. a ∈ sources t" using assms by (meson arr_iff_has_source con_ide_are_eq ex_in_conv in_sourcesE sources_are_con) lemma arr_has_un_target: assumes "arr t" shows "∃!b. b ∈ targets t" using assms by (metis arrE arr_has_un_source arr_resid sources_resid) definition src where "src t ≡ if arr t then THE a. a ∈ sources t else null" lemma src_in_sources: assumes "arr t" shows "src t ∈ sources t" using assms src_def arr_has_un_source the1I2 [of "λa. a ∈ sources t" "λa. a ∈ sources t"] by simp lemma src_eqI: assumes "ide a" and "a ⌢ t" shows "src t = a" using assms src_in_sources by (metis arr_has_un_source resid_arr_ide in_sourcesI arr_resid_iff_con con_sym) lemma sources_char: shows "sources t = {a. arr t ∧ src t = a}" using src_in_sources arr_has_un_source arr_iff_has_source by auto lemma targets_char⇩_{W}⇩_{E}: shows "targets t = {b. arr t ∧ trg t = b}" using trg_in_targets arr_has_un_target arr_iff_has_target by auto lemma arr_src_iff_arr: shows "arr (src t) ⟷ arr t" by (metis arrI conE null_is_zero(2) sources_are_con arrE src_def src_in_sources) lemma arr_trg_iff_arr: shows "arr (trg t) ⟷ arr t" by (metis arrI arrE arr_resid_iff_con resid_arr_self) lemma arr_src_if_arr [simp]: assumes "arr t" shows "arr (src t)" using assms arr_src_iff_arr by blast lemma arr_trg_if_arr [simp]: assumes "arr t" shows "arr (trg t)" using assms arr_trg_iff_arr by blast lemma con_imp_eq_src: assumes "t ⌢ u" shows "src t = src u" using assms by (metis con_imp_coinitial_ax src_eqI) lemma src_resid [simp]: assumes "t ⌢ u" shows "src (t \\ u) = trg u" using assms by (metis arr_resid_iff_con con_implies_arr(2) arr_has_un_source trg_in_targets sources_resid src_in_sources) lemma apex_sym: shows "trg (t \\ u) = trg (u \\ t)" by (metis arr_has_un_target con_sym_ax residuation.arr_resid_iff_con residuation.conI residuation_axioms targets_resid_sym trg_in_targets) lemma apex_arr_prfx: assumes "prfx t u" shows "trg (u \\ t) = trg u" and "trg (t \\ u) = trg u" using assms apply (metis apex_sym arr_resid_iff_con ideE src_resid) by (metis arr_resid_iff_con assms ideE src_resid) lemma seqI⇩_{W}⇩_{E}[intro, simp]: shows "⟦arr t; trg t = src u⟧ ⟹ seq t u" and "⟦arr u; trg t = src u⟧ ⟹ seq t u" by (metis arrE arr_src_iff_arr arr_trg_iff_arr in_sourcesE rts.resid_arr_ide rts_axioms seqI(1) sources_resid src_in_sources trg_def)+ lemma seqE⇩_{W}⇩_{E}[elim]: assumes "seq t u" and "⟦arr u; arr t; trg t = src u⟧ ⟹ T" shows T using assms by (metis arr_has_un_source seq_def src_in_sources trg_in_targets) lemma coinitial_iff⇩_{W}⇩_{E}: shows "coinitial t u ⟷ arr t ∧ arr u ∧ src t = src u" by (metis arr_has_un_source coinitial_def coinitial_iff disjoint_iff_not_equal src_in_sources) lemma coterminal_iff⇩_{W}⇩_{E}: shows "coterminal t u ⟷ arr t ∧ arr u ∧ trg t = trg u" by (metis arr_has_un_target coterminal_iff_con_trg coterminal_iff trg_in_targets) lemma coinitialI⇩_{W}⇩_{E}[intro]: assumes "arr t" and "src t = src u" shows "coinitial t u" using assms coinitial_iff⇩_{W}⇩_{E}by (metis arr_src_iff_arr) lemma coinitialE⇩_{W}⇩_{E}[elim]: assumes "coinitial t u" and "⟦arr t; arr u; src t = src u⟧ ⟹ T" shows T using assms coinitial_iff⇩_{W}⇩_{E}by blast lemma coterminalI⇩_{W}⇩_{E}[intro]: assumes "arr t" and "trg t = trg u" shows "coterminal t u" using assms coterminal_iff⇩_{W}⇩_{E}by (metis arr_trg_iff_arr) lemma coterminalE⇩_{W}⇩_{E}[elim]: assumes "coterminal t u" and "⟦arr t; arr u; trg t = trg u⟧ ⟹ T" shows T using assms coterminal_iff⇩_{W}⇩_{E}by blast lemma ide_src [simp]: assumes "arr t" shows "ide (src t)" using assms by (metis arrE con_imp_coinitial_ax src_eqI) lemma src_ide [simp]: assumes "ide a" shows "src a = a" using arrI assms src_eqI by blast lemma trg_ide [simp]: assumes "ide a" shows "trg a = a" using assms resid_arr_self by auto lemma ide_iff_src_self: assumes "arr a" shows "ide a ⟷ src a = a" using assms by (metis ide_src src_ide) lemma ide_iff_trg_self: assumes "arr a" shows "ide a ⟷ trg a = a" using assms ide_def resid_arr_self ide_trg by metis lemma src_src [simp]: shows "src (src t) = src t" using ide_src src_def src_ide by auto lemma trg_trg [simp]: shows "trg (trg t) = trg t" by (metis con_def con_implies_arr(2) cong_reflexive ide_def null_is_zero(2) resid_arr_self) lemma src_trg [simp]: shows "src (trg t) = trg t" by (metis con_def not_arr_null src_def src_resid trg_def) lemma trg_src [simp]: shows "trg (src t) = src t" by (metis ide_src null_is_zero(2) resid_arr_self src_def trg_ide) lemma resid_ide: assumes "ide a" and "coinitial a t" shows (* [simp]: *) "t \\ a = t" and "a \\ t = trg t" using assms resid_arr_ide apply blast using assms by (metis con_def con_sym_ax ideE in_sourcesE in_sourcesI resid_ide_arr coinitialE src_ide src_resid) lemma con_arr_src [simp]: assumes "arr f" shows "f ⌢ src f" and "src f ⌢ f" using assms src_in_sources con_sym by blast+ lemma resid_src_arr [simp]: assumes "arr f" shows "src f \\ f = trg f" using assms by (simp add: con_imp_coinitial resid_ide(2)) lemma resid_arr_src [simp]: assumes "arr f" shows "f \\ src f = f" using assms by (simp add: resid_arr_ide) end subsection "Extensional RTS" text ‹ An \emph{extensional} RTS is an RTS in which all arrows have trivial congruence classes; that is, congruent arrows are equal. › locale extensional_rts = rts + assumes extensional: "t ∼ u ⟹ t = u" begin sublocale weakly_extensional_rts using extensional by unfold_locales auto lemma cong_char: shows "t ∼ u ⟷ arr t ∧ t = u" by (metis arrI cong_reflexive prfx_implies_con extensional) end subsection "Composites of Transitions" text ‹ Residuation can be used to define a notion of composite of transitions. Composites are not unique, but they are unique up to congruence. › context rts begin definition composite_of where "composite_of u t v ≡ u ≲ v ∧ v \\ u ∼ t" lemma composite_ofI [intro]: assumes "u ≲ v" and "v \\ u ∼ t" shows "composite_of u t v" using assms composite_of_def by blast lemma composite_ofE [elim]: assumes "composite_of u t v" and "⟦u ≲ v; v \\ u ∼ t⟧ ⟹ T" shows T using assms composite_of_def by auto lemma arr_composite_of: assumes "composite_of u t v" shows "arr v" using assms by (meson composite_of_def con_implies_arr(2) prfx_implies_con) lemma composite_of_unq_upto_cong: assumes "composite_of u t v" and "composite_of u t v'" shows "v ∼ v'" using assms cube ide_backward_stable prfx_transitive by (elim composite_ofE) metis lemma composite_of_ide_arr: assumes "ide a" shows "composite_of a t t ⟷ t ⌢ a" using assms by (metis composite_of_def con_implies_arr(1) con_sym resid_arr_ide resid_ide_arr prfx_implies_con prfx_reflexive) lemma composite_of_arr_ide: assumes "ide b" shows "composite_of t b t ⟷ t \\ t ⌢ b" using assms by (metis arr_resid_iff_con composite_of_def ide_imp_con_iff_cong con_implies_arr(1) prfx_implies_con prfx_reflexive) lemma composite_of_source_arr: assumes "arr t" and "a ∈ sources t" shows "composite_of a t t" using assms composite_of_ide_arr sources_def by auto lemma composite_of_arr_target: assumes "arr t" and "b ∈ targets t" shows "composite_of t b t" by (metis arrE assms composite_of_arr_ide in_sourcesE sources_resid) lemma composite_of_ide_self: assumes "ide a" shows "composite_of a a a" using assms composite_of_ide_arr by blast lemma con_prfx_composite_of: assumes "composite_of t u w" shows "t ⌢ w" and "w ⌢ v ⟹ t ⌢ v" using assms apply force using assms composite_of_def con_target prfx_implies_con resid_reflects_con con_sym by meson lemma sources_composite_of: assumes "composite_of u t v" shows "sources v = sources u" using assms by (meson arr_resid_iff_con composite_of_def con_imp_coinitial cong_implies_coinitial coinitial_iff) lemma targets_composite_of: assumes "composite_of u t v" shows "targets v = targets t" proof - have "targets t = targets (v \\ u)" using assms composite_of_def by (meson cong_implies_coterminal coterminal_iff) also have "... = targets (u \\ v)" using assms targets_resid_sym con_prfx_composite_of by metis also have "... = targets v" using assms composite_of_def by (metis prfx_implies_con sources_resid ideE) finally show ?thesis by auto qed lemma resid_composite_of: assumes "composite_of t u w" and "w ⌢ v" shows "v \\ t ⌢ w \\ t" and "v \\ t ⌢ u" and "v \\ w ∼ (v \\ t) \\ u" and "composite_of (t \\ v) (u \\ (v \\ t)) (w \\ v)" proof - show 0: "v \\ t ⌢ w \\ t" using assms con_def by (metis con_target composite_ofE conE con_sym cube) show 1: "v \\ w ∼ (v \\ t) \\ u" proof - have "v \\ w = (v \\ w) \\ (t \\ w)" using assms composite_of_def by (metis (no_types, opaque_lifting) con_target con_sym resid_arr_ide) also have "... = (v \\ t) \\ (w \\ t)" using assms cube by metis also have "... ∼ (v \\ t) \\ u" using assms 0 cong_subst_right(2) [of "w \\ t" u "v \\ t"] by blast finally show ?thesis by blast qed show 2: "v \\ t ⌢ u" using assms 1 by force show "composite_of (t \\ v) (u \\ (v \\ t)) (w \\ v)" proof (unfold composite_of_def, intro conjI) show "t \\ v ≲ w \\ v" using assms cube con_target composite_of_def resid_ide_arr by metis show "(w \\ v) \\ (t \\ v) ≲ u \\ (v \\ t)" by (metis assms(1) 2 composite_ofE con_sym cong_subst_left(2) cube) thus "u \\ (v \\ t) ≲ (w \\ v) \\ (t \\ v)" using assms by (metis composite_of_def con_implies_arr(2) cong_subst_left(2) prfx_implies_con arr_resid_iff_con cube) qed qed lemma con_composite_of_iff: assumes "composite_of t u v" shows "w ⌢ v ⟷ w \\ t ⌢ u" by (meson arr_resid_iff_con assms composite_ofE con_def con_implies_arr(1) con_sym_ax cong_subst_right(1) resid_composite_of(2) resid_reflects_con) definition composable where "composable t u ≡ ∃v. composite_of t u v" lemma composableD [dest]: assumes "composable t u" shows "arr t" and "arr u" and "targets t = sources u" using assms arr_composite_of arr_iff_has_source composable_def sources_composite_of arr_composite_of arr_iff_has_target composable_def targets_composite_of apply auto[2] by (metis assms composable_def composite_ofE con_prfx_composite_of(1) con_sym cong_implies_coinitial coinitial_iff sources_resid) lemma composable_imp_seq: assumes "composable t u" shows "seq t u" using assms by blast lemma bounded_imp_con: assumes "composite_of t u v" and "composite_of t' u' v" shows "con t t'" by (meson assms composite_of_def con_prfx_composite_of prfx_implies_con arr_resid_iff_con con_implies_arr(2)) lemma composite_of_cancel_left: assumes "composite_of t u v" and "composite_of t u' v" shows "u ∼ u'" using assms composite_of_def cong_transitive by blast end subsubsection "RTS with Composites" locale rts_with_composites = rts + assumes has_composites: "seq t u ⟹ composable t u" begin lemma composable_iff_seq: shows "composable g f ⟷ seq g f" using composable_imp_seq has_composites by blast lemma composableI [intro]: assumes "seq g f" shows "composable g f" using assms composable_iff_seq by auto lemma composableE [elim]: assumes "composable g f" and "seq g f ⟹ T" shows T using assms composable_iff_seq by blast lemma obtains_composite_of: assumes "seq g f" obtains h where "composite_of g f h" using assms has_composites composable_def by blast lemma diamond_commutes_upto_cong: assumes "composite_of t (u \\ t) v" and "composite_of u (t \\ u) v'" shows "v ∼ v'" using assms cube ide_backward_stable prfx_transitive by (elim composite_ofE) metis end subsection "Joins of Transitions" context rts begin text ‹ Transition ‹v› is a \emph{join} of ‹u› and ‹v› when ‹v› is the diagonal of the square formed by ‹u›, ‹v›, and their residuals. As was the case for composites, joins in an RTS are not unique, but they are unique up to congruence. › definition join_of where "join_of t u v ≡ composite_of t (u \\ t) v ∧ composite_of u (t \\ u) v" lemma join_ofI [intro]: assumes "composite_of t (u \\ t) v" and "composite_of u (t \\ u) v" shows "join_of t u v" using assms join_of_def by simp lemma join_ofE [elim]: assumes "join_of t u v" and "⟦composite_of t (u \\ t) v; composite_of u (t \\ u) v⟧ ⟹ T" shows T using assms join_of_def by simp definition joinable where "joinable t u ≡ ∃v. join_of t u v" lemma joinable_implies_con: assumes "joinable t u" shows "t ⌢ u" by (meson assms bounded_imp_con join_of_def joinable_def) lemma joinable_implies_coinitial: assumes "joinable t u" shows "coinitial t u" using assms by (simp add: con_imp_coinitial joinable_implies_con) lemma join_of_un_upto_cong: assumes "join_of t u v" and "join_of t u v'" shows "v ∼ v'" using assms join_of_def composite_of_unq_upto_cong by auto lemma join_of_symmetric: assumes "join_of t u v" shows "join_of u t v" using assms join_of_def by simp lemma join_of_arr_self: assumes "arr t" shows "join_of t t t" by (meson assms composite_of_arr_ide ideE join_of_def prfx_reflexive) lemma join_of_arr_src: assumes "arr t" and "a ∈ sources t" shows "join_of a t t" and "join_of t a t" proof - show "join_of a t t" by (meson assms composite_of_arr_target composite_of_def composite_of_source_arr join_of_def prfx_transitive resid_source_in_targets) thus "join_of t a t" using join_of_symmetric by blast qed lemma sources_join_of: assumes "join_of t u v" shows "sources t = sources v" and "sources u = sources v" using assms join_of_def sources_composite_of by blast+ lemma targets_join_of: assumes "join_of t u v" shows "targets (t \\ u) = targets v" and "targets (u \\ t) = targets v" using assms join_of_def targets_composite_of by blast+ lemma join_of_resid: assumes "join_of t u w" and "con v w" shows "join_of (t \\ v) (u \\ v) (w \\ v)" using assms con_sym cube join_of_def resid_composite_of(4) by fastforce lemma con_with_join_of_iff: assumes "join_of t u w" shows "u ⌢ v ∧ v \\ u ⌢ t \\ u ⟹ w ⌢ v" and "w ⌢ v ⟹ t ⌢ v ∧ v \\ t ⌢ u \\ t" proof - have *: "t ⌢ v ∧ v \\ t ⌢ u \\ t ⟷ u ⌢ v ∧ v \\ u ⌢ t \\ u" by (metis arr_resid_iff_con con_implies_arr(1) con_sym cube) show "u ⌢ v ∧ v \\ u ⌢ t \\ u ⟹ w ⌢ v" by (meson assms con_composite_of_iff con_sym join_of_def) show "w ⌢ v ⟹ t ⌢ v ∧ v \\ t ⌢ u \\ t" by (meson assms con_prfx_composite_of join_of_def resid_composite_of(2)) qed end subsubsection "RTS with Joins" locale rts_with_joins = rts + assumes has_joins: "t ⌢ u ⟹ joinable t u" subsection "Joins and Composites in a Weakly Extensional RTS" context weakly_extensional_rts begin lemma src_composite_of: assumes "composite_of u t v" shows "src v = src u" using assms by (metis con_imp_eq_src con_prfx_composite_of(1)) lemma trg_composite_of: assumes "composite_of u t v" shows "trg v = trg t" by (metis arr_composite_of arr_has_un_target arr_iff_has_target assms targets_composite_of trg_in_targets) lemma src_join_of: assumes "join_of t u v" shows "src t = src v" and "src u = src v" by (metis assms join_ofE src_composite_of)+ lemma trg_join_of: assumes "join_of t u v" shows "trg (t \\ u) = trg v" and "trg (u \\ t) = trg v" by (metis assms join_of_def trg_composite_of)+ end subsection "Joins and Composites in an Extensional RTS" context extensional_rts begin lemma composite_of_unique: assumes "composite_of t u v" and "composite_of t u v'" shows "v = v'" using assms composite_of_unq_upto_cong extensional by fastforce text ‹ Here we define composition of transitions. Note that we compose transitions in diagram order, rather than in the order used for function composition. This may eventually lead to confusion, but here (unlike in the case of a category) transitions are typically not functions, so we don't have the constraint of having to conform to the order of function application and composition, and diagram order seems more natural. › definition comp (infixr "⋅" 55) where "t ⋅ u ≡ if composable t u then THE v. composite_of t u v else null" lemma comp_is_composite_of: shows "composable t u ⟹ composite_of t u (t ⋅ u)" and "composite_of t u v ⟹ t ⋅ u = v" proof - show "composable t u ⟹ composite_of t u (t ⋅ u)" using comp_def composite_of_unique the1I2 [of "composite_of t u" "composite_of t u"] composable_def by metis thus "composite_of t u v ⟹ t ⋅ u = v" using composite_of_unique composable_def by auto qed lemma comp_null [simp]: shows "null ⋅ t = null" and "t ⋅ null = null" by (meson composableD not_arr_null comp_def)+ lemma composable_iff_arr_comp: shows "composable t u ⟷ arr (t ⋅ u)" by (metis arr_composite_of comp_is_composite_of(2) composable_def comp_def not_arr_null) lemma composable_iff_comp_not_null: shows "composable t u ⟷ t ⋅ u ≠ null" by (metis composable_iff_arr_comp comp_def not_arr_null) lemma comp_src_arr [simp]: assumes "arr t" and "src t = a" shows "a ⋅ t = t" using assms comp_is_composite_of(2) composite_of_source_arr src_in_sources by blast lemma comp_arr_trg [simp]: assumes "arr t" and "trg t = b" shows "t ⋅ b = t" using assms comp_is_composite_of(2) composite_of_arr_target trg_in_targets by blast lemma comp_ide_self: assumes "ide a" shows "a ⋅ a = a" using assms comp_is_composite_of(2) composite_of_ide_self by fastforce lemma arr_comp [intro, simp]: assumes "composable t u" shows "arr (t ⋅ u)" using assms composable_iff_arr_comp by blast lemma trg_comp [simp]: assumes "composable t u" shows "trg (t ⋅ u) = trg u" by (metis arr_has_un_target assms comp_is_composite_of(2) composable_def composable_imp_seq arr_iff_has_target seq_def targets_composite_of trg_in_targets) lemma src_comp [simp]: assumes "composable t u" shows "src (t ⋅ u) = src t" using assms comp_is_composite_of arr_iff_has_source sources_composite_of src_def composable_def by auto lemma con_comp_iff: shows "w ⌢ t ⋅ u ⟷ composable t u ∧ w \\ t ⌢ u" by (meson comp_is_composite_of(1) composable_iff_arr_comp con_composite_of_iff con_implies_arr(2)) lemma con_compI [intro]: assumes "composable t u" and "w \\ t ⌢ u" shows "w ⌢ t ⋅ u" and "t ⋅ u ⌢ w" using assms con_comp_iff con_sym by blast+ lemma resid_comp: assumes "t ⋅ u ⌢ w" shows "w \\ (t ⋅ u) = (w \\ t) \\ u" and "(t ⋅ u) \\ w = (t \\ w) ⋅ (u \\ (w \\ t))" proof - have 1: "composable t u" using assms composable_iff_comp_not_null by force show "w \\ (t ⋅ u) = (w \\ t) \\ u" using 1 by (meson assms cong_char composable_def resid_composite_of(3) comp_is_composite_of(1)) show "(t ⋅ u) \\ w = (t \\ w) ⋅ (u \\ (w \\ t))" using assms 1 composable_def comp_is_composite_of(2) resid_composite_of by metis qed lemma prfx_decomp: assumes "t ≲ u" shows "t ⋅ (u \\ t) = u" by (meson assms arr_resid_iff_con comp_is_composite_of(2) composite_of_def con_sym cong_reflexive prfx_implies_con) lemma prfx_comp: assumes "arr u" and "t ⋅ v = u" shows "t ≲ u" by (metis assms comp_is_composite_of(2) composable_def composable_iff_arr_comp composite_of_def) lemma comp_eqI: assumes "t ≲ v" and "u = v \\ t" shows "t ⋅ u = v" by (metis assms prfx_decomp) lemma comp_assoc: assumes "composable (t ⋅ u) v" shows "t ⋅ (u ⋅ v) = (t ⋅ u) ⋅ v" proof - have 1: "t ≲ (t ⋅ u) ⋅ v" by (meson assms composable_iff_arr_comp composableD prfx_comp prfx_transitive) moreover have "((t ⋅ u) ⋅ v) \\ t = u ⋅ v" proof - have "((t ⋅ u) ⋅ v) \\ t = ((t ⋅ u) \\ t) ⋅ (v \\ (t \\ (t ⋅ u)))" by (meson assms calculation con_sym prfx_implies_con resid_comp(2)) also have "... = u ⋅ v" proof - have 2: "(t ⋅ u) \\ t = u" by (metis assms comp_is_composite_of(2) composable_def composable_iff_arr_comp composable_imp_seq composite_of_def extensional seqE) moreover have "v \\ (t \\ (t ⋅ u)) = v" using assms by (meson 1 con_comp_iff con_sym composable_imp_seq resid_arr_ide prfx_implies_con prfx_comp seqE) ultimately show ?thesis by simp qed finally show ?thesis by blast qed ultimately show "t ⋅ (u ⋅ v) = (t ⋅ u) ⋅ v" by (metis comp_eqI) qed text ‹ We note the following assymmetry: ‹composable (t ⋅ u) v ⟹ composable u v› is true, but ‹composable t (u ⋅ v) ⟹ composable t u› is not. › lemma comp_cancel_left: assumes "arr (t ⋅ u)" and "t ⋅ u = t ⋅ v" shows "u = v" using assms by (metis composable_def composable_iff_arr_comp composite_of_cancel_left extensional comp_is_composite_of(2)) lemma comp_resid_prfx [simp]: assumes "arr (t ⋅ u)" shows "(t ⋅ u) \\ t = u" using assms by (metis comp_cancel_left comp_eqI prfx_comp) lemma bounded_imp_con⇩_{E}: assumes "t ⋅ u ∼ t' ⋅ u'" shows "t ⌢ t'" by (metis arr_resid_iff_con assms con_comp_iff con_implies_arr(2) prfx_implies_con con_sym) lemma join_of_unique: assumes "join_of t u v" and "join_of t u v'" shows "v = v'" using assms join_of_def composite_of_unique by blast definition join (infix "⊔" 52) where "t ⊔ u ≡ if joinable t u then THE v. join_of t u v else null" lemma join_is_join_of: assumes "joinable t u" shows "join_of t u (t ⊔ u)" using assms joinable_def join_def join_of_unique the1I2 [of "join_of t u" "join_of t u"] by force lemma joinable_iff_arr_join: shows "joinable t u ⟷ arr (t ⊔ u)" by (metis cong_char join_is_join_of join_of_un_upto_cong not_arr_null join_def) lemma joinable_iff_join_not_null: shows "joinable t u ⟷ t ⊔ u ≠ null" by (metis join_def joinable_iff_arr_join not_arr_null) lemma join_sym: shows "t ⊔ u = u ⊔ t" by (metis extensional_rts.join_def extensional_rts.join_of_unique extensional_rts_axioms join_is_join_of join_of_symmetric joinable_def) lemma src_join: assumes "joinable t u" shows "src (t ⊔ u) = src t" using assms by (metis con_imp_eq_src con_prfx_composite_of(1) join_is_join_of join_of_def) lemma trg_join: assumes "joinable t u" shows "trg (t ⊔ u) = trg (t \\ u)" using assms by (metis arr_resid_iff_con join_is_join_of joinable_iff_arr_join joinable_implies_con in_targetsE src_eqI targets_join_of(1) trg_in_targets) lemma resid_join⇩_{E}[simp]: assumes "joinable t u" and "v ⌢ t ⊔ u" shows "v \\ (t ⊔ u) = (v \\ u) \\ (t \\ u)" and "v \\ (t ⊔ u) = (v \\ t) \\ (u \\ t)" and "(t ⊔ u) \\ v = (t \\ v) ⊔ (u \\ v)" proof - show 1: "v \\ (t ⊔ u) = (v \\ u) \\ (t \\ u)" by (meson assms con_sym join_of_def resid_composite_of(3) extensional join_is_join_of) show "v \\ (t ⊔ u) = (v \\ t) \\ (u \\ t)" by (metis "1" cube) show "(t ⊔ u) \\ v = (t \\ v) ⊔ (u \\ v)" using assms joinable_def join_of_resid join_is_join_of extensional by (meson join_of_unique) qed lemma join_eqI: assumes "t ≲ v" and "u ≲ v" and "v \\ u = t \\ u" and "v \\ t = u \\ t" shows "t ⊔ u = v" using assms composite_of_def cube ideE join_of_def joinable_def join_of_unique join_is_join_of trg_def by metis lemma comp_join: assumes "joinable (t ⋅ u) (t ⋅ u')" shows "composable t (u ⊔ u')" and "t ⋅ (u ⊔ u') = t ⋅ u ⊔ t ⋅ u'" proof - have "t ≲ t ⋅ u ⊔ t ⋅ u'" using assms by (metis composable_def composite_of_def join_of_def join_is_join_of joinable_implies_con prfx_transitive comp_is_composite_of(2) con_comp_iff) moreover have "(t ⋅ u ⊔ t ⋅ u') \\ t = u ⊔ u'" by (metis arr_resid_iff_con assms calculation comp_resid_prfx con_implies_arr(2) joinable_implies_con resid_join⇩_{E}(3) con_implies_arr(1) ide_implies_arr) ultimately show "t ⋅ (u ⊔ u') = t ⋅ u ⊔ t ⋅ u'" by (metis comp_eqI) thus "composable t (u ⊔ u')" by (metis assms joinable_iff_join_not_null comp_def) qed lemma join_src: assumes "arr t" shows "src t ⊔ t = t" using assms joinable_def join_of_arr_src join_is_join_of join_of_unique src_in_sources by meson lemma join_arr_self: assumes "arr t" shows "t ⊔ t = t" using assms joinable_def join_of_arr_self join_is_join_of join_of_unique by blast lemma arr_prfx_join_self: assumes "joinable t u" shows "t ≲ t ⊔ u" using assms by (meson composite_of_def join_is_join_of join_of_def) lemma con_prfx: shows "⟦t ⌢ u; v ≲ u⟧ ⟹ t ⌢ v" and "⟦t ⌢ u; v ≲ t⟧ ⟹ v ⌢ u" apply (metis arr_resid con_arr_src(1) ide_iff_src_self prfx_implies_con resid_reflects_con src_resid) by (metis arr_resid_iff_con comp_eqI con_comp_iff con_implies_arr(1) con_sym) lemma join_prfx: assumes "t ≲ u" shows "t ⊔ u = u" and "u ⊔ t = u" proof - show "t ⊔ u = u" using assms by (metis (no_types, lifting) join_eqI ide_iff_src_self ide_implies_arr resid_arr_self prfx_implies_con src_resid) thus "u ⊔ t = u" by (metis join_sym) qed lemma con_with_join_if [intro, simp]: assumes "joinable t u" and "u ⌢ v" and "v \\ u ⌢ t \\ u" shows "t ⊔ u ⌢ v" and "v ⌢ t ⊔ u" proof - show "t ⊔ u ⌢ v" using assms con_with_join_of_iff [of t u "join t u" v] join_is_join_of by simp thus "v ⌢ t ⊔ u" using assms con_sym by blast qed lemma join_assoc⇩_{E}: assumes "arr ((t ⊔ u) ⊔ v)" and "arr (t ⊔ (u ⊔ v))" shows "(t ⊔ u) ⊔ v = t ⊔ (u ⊔ v)" proof (intro join_eqI) have tu: "joinable t u" by (metis arr_src_iff_arr assms(1) joinable_iff_arr_join src_join) have uv: "joinable u v" by (metis assms(2) joinable_iff_arr_join joinable_iff_join_not_null joinable_implies_con not_con_null(2)) have tu_v: "joinable (t ⊔ u) v" by (simp add: assms(1) joinable_iff_arr_join) have t_uv: "joinable t (u ⊔ v)" by (simp add: assms(2) joinable_iff_arr_join) show 0: "t ⊔ u ≲ t ⊔ (u ⊔ v)" proof - have "(t ⊔ u) \\ (t ⊔ (u ⊔ v)) = ((u \\ t) \\ (u \\ t)) \\ ((v \\ t) \\ (u \\ t))" proof - have "(t ⊔ u) \\ (t ⊔ (u ⊔ v)) = ((t ⊔ u) \\ t) \\ ((u ⊔ v) \\ t)" by (metis t_uv tu arr_prfx_join_self conI con_with_join_if(2) join_sym joinable_iff_join_not_null not_ide_null resid_join⇩_{E}(2)) also have "... = (t \\ t ⊔ u \\ t) \\ ((u ⊔ v) \\ t)" by (simp add: tu con_sym joinable_implies_con) also have "... = (t \\ t ⊔ u \\ t) \\ (u \\ t ⊔ v \\ t)" by (simp add: t_uv uv joinable_implies_con) also have "... = (u \\ t) \\ join (u \\ t) (v \\ t)" by (metis tu con_implies_arr(1) cong_subst_left(2) cube join_eqI join_sym joinable_iff_join_not_null joinable_implies_con prfx_reflexive trg_def trg_join) also have "... = ((u \\ t) \\ (u \\ t)) \\ ((v \\ t) \\ (u \\ t))" proof - have 1: "joinable (u \\ t) (v \\ t)" by (metis t_uv uv con_sym joinable_iff_join_not_null joinable_implies_con resid_join⇩_{E}(3) conE) moreover have "u \\ t ⌢ u \\ t ⊔ v \\ t" using arr_prfx_join_self 1 prfx_implies_con by blast ultimately show ?thesis using resid_join⇩_{E}(2) [of "u \\ t" "v \\ t" "u \\ t"] by blast qed finally show ?thesis by blast qed moreover have "ide ..." by (metis tu_v tu arr_resid_iff_con con_sym cube joinable_implies_con prfx_reflexive resid_join⇩_{E}(2)) ultimately show ?thesis by simp qed show 1: "v ≲ t ⊔ (u ⊔ v)" by (metis arr_prfx_join_self join_sym joinable_iff_join_not_null prfx_transitive t_uv uv) show "(t ⊔ (u ⊔ v)) \\ v = (t ⊔ u) \\ v" proof - have "(t ⊔ (u ⊔ v)) \\ v = t \\ v ⊔ (u ⊔ v) \\ v" by (metis 1 assms(2) join_def not_arr_null resid_join⇩_{E}(3) prfx_implies_con) also have "... = t \\ v ⊔ (u \\ v ⊔ v \\ v)" by (metis 1 conE conI con_sym join_def resid_join⇩_{E}(1) resid_join⇩_{E}(3) null_is_zero(2) prfx_implies_con) also have "... = t \\ v ⊔ u \\ v" by (metis arr_resid_iff_con con_sym cube cong_char join_prfx(2) joinable_implies_con uv) also have "... = (t ⊔ u) \\ v" by (metis 0 1 con_implies_arr(1) con_prfx(1) joinable_iff_arr_join resid_join⇩_{E}(3) prfx_implies_con) finally show ?thesis by blast qed show "(t ⊔ (u ⊔ v)) \\ (t ⊔ u) = v \\ (t ⊔ u)" proof - have 2: "(t ⊔ (u ⊔ v)) \\ (t ⊔ u) = t \\ (t ⊔ u) ⊔ (u ⊔ v) \\ (t ⊔ u)" by (metis 0 assms(2) join_def not_arr_null resid_join⇩_{E}(3) prfx_implies_con) also have 3: "... = (t \\ t) \\ (u \\ t) ⊔ (u ⊔ v) \\ (t ⊔ u)" by (metis tu arr_prfx_join_self prfx_implies_con resid_join⇩_{E}(2)) also have 4: "... = (u ⊔ v) \\ (t ⊔ u)" proof - have "(t \\ t) \\ (u \\ t) = src ((u ⊔ v) \\ (t ⊔ u))" using src_resid trg_join by (metis (full_types) t_uv tu 0 arr_resid_iff_con con_implies_arr(1) con_sym cube prfx_implies_con resid_join⇩_{E}(1) trg_def) thus ?thesis by (metis tu arr_prfx_join_self conE join_src prfx_implies_con resid_join⇩_{E}(2) src_def) qed also have "... = u \\ (t ⊔ u) ⊔ v \\ (t ⊔ u)" by (metis 0 2 3 4 uv conI con_sym_ax not_ide_null resid_join⇩_{E}(3)) also have "... = (u \\ u) \\ (t \\ u) ⊔ v \\ (t ⊔ u)" by (metis tu arr_prfx_join_self join_sym joinable_iff_join_not_null prfx_implies_con resid_join⇩_{E}(1)) also have "... = v \\ (t ⊔ u)" proof - have "(u \\ u) \\ (t \\ u) = src (v \\ (t ⊔ u))" by (metis tu_v tu con_sym cube joinable_implies_con src_resid trg_def trg_join apex_sym) thus ?thesis using tu_v arr_resid_iff_con con_sym join_src joinable_implies_con by presburger qed finally show ?thesis by blast qed qed lemma join_prfx_monotone: assumes "t ≲ u" and "u ⊔ v ⌢ t ⊔ v" shows "t ⊔ v ≲ u ⊔ v" proof - have "(t ⊔ v) \\ (u ⊔ v) = (t \\ u) \\ (v \\ u)" proof - have "(t ⊔ v) \\ (u ⊔ v) = t \\ (u ⊔ v) ⊔ v \\ (u ⊔ v)" using assms join_sym resid_join⇩_{E}(3) [of t v "join u v"] joinable_iff_join_not_null by fastforce also have "... = (t \\ u) \\ (v \\ u) ⊔ (v \\ u) \\ (v \\ u)" by (metis (full_types) assms(2) conE conI joinable_iff_join_not_null null_is_zero(1) resid_join⇩_{E}(1-2) con_sym_ax) also have "... = (t \\ u) \\ (v \\ u) ⊔ trg (v \\ u)" using trg_def by fastforce also have "... = (t \\ u) \\ (v \\ u) ⊔ src ((t \\ u) \\ (v \\ u))" by (metis assms(1-2) con_implies_arr(1) con_target joinable_iff_arr_join joinable_implies_con src_resid) also have "... = (t \\ u) \\ (v \\ u)" by (metis arr_resid_iff_con assms(2) con_implies_arr(1) con_sym join_def join_src join_sym not_arr_null resid_join⇩_{E}(2)) finally show ?thesis by blast qed moreover have "ide ..." by (metis arr_resid_iff_con assms(1-2) calculation con_sym resid_ide_arr) ultimately show ?thesis by presburger qed lemma join_eqI': assumes "t ≲ v" and "u ≲ v" and "v \\ u = t \\ u" and "v \\ t = u \\ t" shows "v = t ⊔ u" using assms composite_of_def cube ideE join_of_def joinable_def join_of_unique join_is_join_of trg_def by metis text ‹ We note that it is not the case that the existence of either of ‹t ⊔ (u ⊔ v)› or ‹(t ⊔ u) ⊔ v› implies that of the other. For example, if ‹(t ⊔ u) ⊔ v ≠ null›, then it is not necessarily the case that ‹u ⊔ v ≠ null›. › end subsubsection "Extensional RTS with Joins" locale extensional_rts_with_joins = rts_with_joins + extensional_rts begin lemma joinable_iff_con [iff]: shows "joinable t u ⟷ t ⌢ u" by (meson has_joins joinable_implies_con) lemma joinableE [elim]: assumes "joinable t u" and "t ⌢ u ⟹ T" shows T using assms joinable_iff_con by blast lemma src_join⇩_{E}⇩_{J}[simp]: assumes "t ⌢ u" shows "src (t ⊔ u) = src t" using assms by (meson has_joins src_join) lemma trg_join⇩_{E}⇩_{J}: assumes "t ⌢ u" shows "trg (t ⊔ u) = trg (t \\ u)" using assms by (meson has_joins trg_join) lemma resid_join⇩_{E}⇩_{J}[simp]: assumes "t ⌢ u" and "v ⌢ t ⊔ u" shows "v \\ (t ⊔ u) = (v \\ t) \\ (u \\ t)" and "(t ⊔ u) \\ v = (t \\ v) ⊔ (u \\ v)" using assms has_joins resid_join⇩_{E}[of t u v] by blast+ lemma join_assoc: shows "t ⊔ (u ⊔ v) = (t ⊔ u) ⊔ v" proof - have *: "⋀t u v. con (t ⊔ u) v ⟹ t ⊔ (u ⊔ v) = (t ⊔ u) ⊔ v" proof - fix t u v assume 1: "con (t ⊔ u) v" have vt_ut: "v \\ t ⌢ u \\ t" using 1 by (metis con_with_join_of_iff(2) join_def join_is_join_of not_con_null(1)) have tv_uv: "t \\ v ⌢ u \\ v" using vt_ut cube con_sym by (metis arr_resid_iff_con) have 2: "(t ⊔ u) ⊔ v = (t ⋅ (u \\ t)) ⋅ (v \\ (t ⋅ (u \\ t)))" using 1 by (metis comp_is_composite_of(2) con_implies_arr(1) has_joins join_is_join_of join_of_def joinable_iff_arr_join) also have "... = t ⋅ ((u \\ t) ⋅ (v \\ (t ⋅ (u \\ t))))" using 1 by (metis calculation has_joins joinable_iff_join_not_null comp_assoc comp_def) also have "... = t ⋅ ((u \\ t) ⋅ ((v \\ t) \\ (u \\ t)))" using 1 by (metis 2 comp_null(2) con_compI(2) con_comp_iff has_joins resid_comp(1) conI joinable_iff_join_not_null) also have "... = t ⋅ ((v \\ t) ⊔ (u \\ t))" by (metis vt_ut comp_is_composite_of(2) has_joins join_of_def join_is_join_of) also have "... = t ⋅ ((u \\ t) ⊔ (v \\ t))" using join_sym by metis also have "... = t ⋅ ((u ⊔ v) \\ t)" by (metis tv_uv vt_ut con_implies_arr(2) con_sym con_with_join_of_iff(1) has_joins join_is_join_of arr_resid_iff_con resid_join⇩_{E}(3)) also have "... = t ⊔ (u ⊔ v)" by (metis comp_is_composite_of(2) comp_null(2) conI has_joins join_is_join_of join_of_def joinable_iff_join_not_null) finally show "t ⊔ (u ⊔ v) = (t ⊔ u) ⊔ v" by simp qed thus ?thesis by (metis (full_types) has_joins joinable_iff_join_not_null joinable_implies_con con_sym) qed lemma join_is_lub: assumes "t ≲ v" and "u ≲ v" shows "t ⊔ u ≲ v" proof - have "(t ⊔ u) \\ v = (t \\ v) ⊔ (u \\ v)" using assms resid_join⇩_{E}(3) [of t u v] by (metis arr_prfx_join_self con_target con_sym join_assoc joinable_iff_con joinable_iff_join_not_null prfx_implies_con resid_reflects_con) also have "... = trg v ⊔ trg v" using assms by (metis ideE prfx_implies_con src_resid trg_ide) also have "... = trg v" by (metis assms(2) ide_iff_src_self ide_implies_arr join_arr_self prfx_implies_con src_resid) finally have "(t ⊔ u) \\ v = trg v" by blast moreover have "ide (trg v)" using assms by (metis con_implies_arr(2) prfx_implies_con cong_char trg_def) ultimately show ?thesis by simp qed end subsubsection "Extensional RTS with Composites" text ‹ If an extensional RTS is assumed to have composites for all composable pairs of transitions, then the ``semantic'' property of transitions being composable can be replaced by the ``syntactic'' property of transitions being sequential. This results in simpler statements of a number of properties. › locale extensional_rts_with_composites = rts_with_composites + extensional_rts begin lemma seq_implies_arr_comp: assumes "seq t u" shows "arr (t ⋅ u)" using assms by (meson composable_iff_arr_comp composable_iff_seq) lemma arr_comp⇩_{E}⇩_{C}[intro, simp]: assumes "arr t" and "arr u" and "trg t = src u" shows "arr (t ⋅ u)" using assms by (simp add: seq_implies_arr_comp) lemma arr_compE⇩_{E}⇩_{C}[elim]: assumes "arr (t ⋅ u)" and "⟦arr t; arr u; trg t = src u⟧ ⟹ T" shows T using assms composable_iff_arr_comp composable_iff_seq by blast lemma trg_comp⇩_{E}⇩_{C}[simp]: assumes "seq t u" shows "trg (t ⋅ u) = trg u" by (meson assms has_composites trg_comp) lemma src_comp⇩_{E}⇩_{C}[simp]: assumes "seq t u" shows "src (t ⋅ u) = src t" using assms src_comp has_composites by simp lemma con_comp_iff⇩_{E}⇩_{C}[simp]: shows "w ⌢ t ⋅ u ⟷ seq t u ∧ u ⌢ w \\ t" and "t ⋅ u ⌢ w ⟷ seq t u ∧ u ⌢ w \\ t" using composable_iff_seq con_comp_iff con_sym by meson+ lemma comp_assoc⇩_{E}⇩_{C}: shows "t ⋅ (u ⋅ v) = (t ⋅ u) ⋅ v" apply (cases "seq t u") apply (metis arr_comp comp_assoc comp_def not_arr_null arr_compE⇩_{E}⇩_{C}arr_comp⇩_{E}⇩_{C}seq_implies_arr_comp trg_comp⇩_{E}⇩_{C}) by (metis comp_def composable_iff_arr_comp seqI⇩_{W}⇩_{E}(1) src_comp arr_compE⇩_{E}⇩_{C}) lemma diamond_commutes: shows "t ⋅ (u \\ t) = u ⋅ (t \\ u)" proof (cases "t ⌢ u") show "¬ t ⌢ u ⟹ ?thesis" by (metis comp_null(2) conI con_sym) assume con: "t ⌢ u" have "(t ⋅ (u \\ t)) \\ u = (t \\ u) ⋅ ((u \\ t) \\ (u \\ t))" using con by (metis (no_types, lifting) arr_resid_iff_con con_compI(2) con_implies_arr(1) resid_comp(2) con_imp_arr_resid con_sym comp_def arr_comp⇩_{E}⇩_{C}src_resid conI) moreover have "u ≲ t ⋅ (u \\ t)" by (metis arr_resid_iff_con calculation con cong_reflexive comp_arr_trg resid_arr_self resid_comp(1) apex_sym) ultimately show ?thesis by (metis comp_eqI con comp_arr_trg resid_arr_self arr_resid apex_sym) qed lemma mediating_transition: assumes "t ⋅ v = u ⋅ w" shows "v \\ (u \\ t) = w \\ (t \\ u)" proof (cases "seq t v") assume 1: "seq t v" hence 2: "arr (u ⋅ w)" using assms by (metis arr_comp⇩_{E}⇩_{C}seqE⇩_{W}⇩_{E}) have 3: "v \\ (u \\ t) = ((t ⋅ v) \\ t) \\ (u \\ t)" by (metis 2 assms comp_resid_prfx) also have "... = (t ⋅ v) \\ (t ⋅ (u \\ t))" by (metis (no_types, lifting) "2" assms con_comp_iff⇩_{E}⇩_{C}(2) con_imp_eq_src con_implies_arr(2) con_sym comp_resid_prfx prfx_comp resid_comp(1) arr_compE⇩_{E}⇩_{C}arr_comp⇩_{E}⇩_{C}prfx_implies_con) also have "... = (u ⋅ w) \\ (u ⋅ (t \\ u))" using assms diamond_commutes by presburger also have "... = ((u ⋅ w) \\ u) \\ (t \\ u)" by (metis 3 assms calculation cube) also have "... = w \\ (t \\ u)" using 2 by simp finally show ?thesis by blast next assume 1: "¬ seq t v" have "v \\ (u \\ t) = null" using 1 by (metis (mono_tags, lifting) arr_resid_iff_con coinitial_iff⇩_{W}⇩_{E}con_imp_coinitial seqI⇩_{W}⇩_{E}(2) src_resid conI) also have "... = w \\ (t \\ u)" by (metis (no_types, lifting) "1" arr_comp⇩_{E}⇩_{C}assms composable_imp_seq con_imp_eq_src con_implies_arr(1) con_implies_arr(2) comp_def not_arr_null conI src_resid) finally show ?thesis by blast qed lemma induced_arrow: assumes "seq t u" and "t ⋅ u = t' ⋅ u'" shows "(t' \\ t) ⋅ (u \\ (t' \\ t)) = u" and "(t \\ t') ⋅ (u \\ (t' \\ t)) = u'" and "(t' \\ t) ⋅ v = u ⟹ v = u \\ (t' \\ t)" apply (metis assms comp_eqI arr_compE⇩_{E}⇩_{C}prfx_comp resid_comp(1) arr_resid_iff_con seq_implies_arr_comp) apply (metis assms comp_resid_prfx arr_compE⇩_{E}⇩_{C}resid_comp(2) arr_resid_iff_con seq_implies_arr_comp) by (metis assms(1) comp_resid_prfx seq_def) text ‹ If an extensional RTS has composites, then it automatically has joins. › sublocale extensional_rts_with_joins proof fix t u assume con: "t ⌢ u" have 1: "con u (t ⋅ (u \\ t))" using con_compI(1) [of t "u \\ t" u] by (metis con con_implies_arr(1) con_sym diamond_commutes prfx_implies_con arr_resid prfx_comp src_resid arr_comp⇩_{E}⇩_{C}) have "t ⊔ u = t ⋅ (u \\ t)" proof (intro join_eqI) show "t ≲ t ⋅ (u \\ t)" by (metis 1 composable_def comp_is_composite_of(2) composite_of_def con_comp_iff) moreover show 2: "u ≲ t ⋅ (u \\ t)" using 1 arr_resid con con_sym prfx_reflexive resid_comp(1) by metis moreover show "(t ⋅ (u \\ t)) \\ u = t \\ u" using 1 diamond_commutes induced_arrow(2) resid_comp(2) by force ultimately show "(t ⋅ (u \\ t)) \\ t = u \\ t" by (metis con_comp_iff⇩_{E}⇩_{C}(1) con_sym prfx_implies_con resid_comp(2) induced_arrow(1)) qed thus "joinable t u" by (metis "1" con_implies_arr(2) joinable_iff_join_not_null not_arr_null) qed lemma comp_join⇩_{E}⇩_{C}: assumes "composable t u" and "joinable u u'" shows "composable t (u ⊔ u')" and "t ⋅ (u ⊔ u') = t ⋅ u ⊔ t ⋅ u'" proof - have 1: "u ⊔ u' = u ⋅ (u' \\ u) ∧ u ⊔ u' = u' ⋅ (u \\ u')" using assms joinable_implies_con diamond_commutes by (metis comp_is_composite_of(2) join_is_join_of join_ofE) show 2: "composable t (u ⊔ u')" using assms 1 composable_iff_seq arr_comp src_join arr_compE⇩_{E}⇩_{C}joinable_iff_arr_join seqI⇩_{W}⇩_{E}(1) by metis have "con (t ⋅ u) (t ⋅ u')" using 1 2 arr_comp arr_compE⇩_{E}⇩_{C}assms(2) comp_assoc⇩_{E}⇩_{C}comp_resid_prfx con_comp_iff joinable_implies_con comp_def not_arr_null by metis thus "t ⋅ (u ⊔ u') = t ⋅ u ⊔ t ⋅ u'" using assms comp_join(2) joinable_iff_con by blast qed lemma join_expansion: assumes "t ⌢ u" shows "t ⊔ u = t ⋅ (u \\ t)" and "seq t (u \\ t)" proof - show "t ⊔ u = t ⋅ (u \\ t)" by (metis assms comp_is_composite_of(2) has_joins join_is_join_of join_of_def) thus "seq t (u \\ t)" by (meson assms composable_def composable_iff_seq has_joins join_is_join_of join_of_def) qed lemma join3_expansion: assumes "t ⌢ u" and "t ⌢ v" and "u ⌢ v" shows "(t ⊔ u) ⊔ v = (t ⋅ (u \\ t)) ⋅ ((v \\ t) \\ (u \\ t))" proof (cases "v \\ t ⌢ u \\ t") show "¬ v \\ t ⌢ u \\ t ⟹ ?thesis" by (metis assms(1) comp_null(2) join_expansion(1) joinable_implies_con resid_comp(1) join_def conI) assume 1: "v \\ t ⌢ u \\ t " have "(t ⊔ u) ⊔ v = (t ⊔ u) ⋅ (v \\ (t ⊔ u))" by (metis comp_null(1) diamond_commutes ex_un_null join_expansion(1) joinable_implies_con null_is_zero(2) join_def conI) also have "... = (t ⋅ (u \\ t)) ⋅ (v \\ (t ⊔ u))" using join_expansion [of t u] assms(1) by presburger also have "... = (t ⋅ (u \\ t)) ⋅ ((v \\ u) \\ (t \\ u))" using assms 1 join_of_resid(1) [of t u v] cube [of v t u] by (metis con_compI(2) con_implies_arr(2) join_expansion(1) not_arr_null resid_comp(1) con_sym comp_def src_resid arr_comp⇩_{E}⇩_{C}) also have "... = (t ⋅ (u \\ t)) ⋅ ((v \\ t) \\ (u \\ t))" by (metis cube) finally show ?thesis by blast qed lemma resid_common_prefix: assumes "t ⋅ u ⌢ t ⋅ v" shows "(t ⋅ u) \\ (t ⋅ v) = u \\ v" using assms by (