# Theory ResiduatedTransitionSystem

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 transitions, 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 binary operation 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"

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

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

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

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]:
assumes "arr t" and "arr u" and "targets t = sources u"
shows "seq t u"
using assms seq_def by auto

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"

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 [iff]:
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 [iff]:
shows "arr (trg t) ⟷ arr t"
by (metis arrI arrE arr_resid_iff_con resid_arr_self)

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 trg_resid_sym:
assumes "t ⌢ u"
shows "trg (t \\ u) = trg (u \\ t)"
using assms
by (metis arr_has_un_target arr_resid con_sym targets_resid_sym trg_in_targets)

lemma apex_sym:
shows "trg (t \\ u) = trg (u \\ t)"
using trg_resid_sym con_def by metis

lemma seqI⇩W⇩E [intro, simp]:
assumes "arr u" and "arr t" and "trg t = src u"
shows "seq t u"
using assms
by (metis (mono_tags, lifting) arrE in_sourcesE resid_arr_ide sources_resid
resid_arr_self seqI sources_are_con src_in_sources)

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 force

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 cong_reflexive ide_def null_is_zero(2) resid_arr_self
residuation.con_implies_arr(1) residuation_axioms)

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

lemma resid_arr_src [simp]:
assumes "arr f"
shows "f \\ src f = f"
using assms

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

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  (infixl "⋅" 55)
where "t ⋅ u ≡ if composable t u then THE v. composite_of t u v else null"

lemma comp_is_composite_of:
assumes "composite_of t u v"
shows "composite_of t u (t ⋅ u)" and "t ⋅ u = v"
proof -
show "composite_of t u (t ⋅ u)"
using assms comp_def composite_of_unique the1I2 [of "composite_of t u" "composite_of t u"]
composable_def
by metis
thus "t ⋅ u = v"
using assms composite_of_unique by simp
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) con_composite_of_iff con_sym con_implies_arr(2)
composable_def composable_iff_arr_comp)

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:
assumes "t ⊔ u ≠ null"
shows "t ⊔ u = u ⊔ t"
using assms
by (meson join_def join_is_join_of join_of_symmetric join_of_unique 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_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"
have t_uv: "joinable t (u ⊔ v)"
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
trg_resid_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:
shows "joinable t u ⟷ t ⌢ u"
by (meson has_joins joinable_implies_con)

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 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_implies_arr(1) con_with_join_of_iff(2) join_is_join_of not_arr_null
join_def)
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_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

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 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) trg_resid_sym)
ultimately show ?thesis
by (metis comp_eqI con comp_arr_trg resid_arr_self arr_resid trg_resid_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 "1" comp_is_composite_of(1) composite_of_def obtains_composite_of extensional)
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 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 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 (metis con_comp_iff con_sym con_comp_iff⇩E⇩C(2) con_implies_arr(2) induced_arrow(1)
resid_comp(1) resid_comp(2) residuation.arr_resid_iff_con residuation_axioms)

end

subsection "Confluence"

text ‹
An RTS is \emph{confluent} if every coinitial pair of transitions is consistent.
›

locale confluent_rts = rts +
assumes confluence: "coinitial t u ⟹ con t u"

section "Simulations"

text ‹
\emph{Simulations} are morphisms of residuated transition systems.
They are assumed to preserve consistency and residuation.
›

locale simulation =
A: rts A +
B: rts B
for A :: "'a resid"      (infixr "\\⇩A" 70)
and B :: "'b resid"      (infixr "\\⇩B" 70)
and F :: "'a ⇒ 'b" +
assumes extensional: "¬ A.arr t ⟹ F t = B.null"
and preserves_con [simp]: "A.con t u ⟹ B.con (F t) (F u)"
and preserves_resid [simp]: "A.con t u ⟹ F (t \\⇩A u) = F t \\⇩B F u"
begin

lemma preserves_reflects_arr [iff]:
shows "B.arr (F t) ⟷ A.arr t"
by (metis A.arr_def B.con_implies_arr(2) B.not_arr_null extensional preserves_con)

lemma preserves_ide [simp]:
assumes "A.ide a"
shows "B.ide (F a)"
by (metis A.ideE assms preserves_con preserves_resid B.ideI)

lemma preserves_sources:
shows "F  A.sources t ⊆ B.sources (F t)"
using A.sources_def B.sources_def preserves_con preserves_ide by auto

lemma preserves_targets:
shows "F  A.targets t ⊆ B.targets (F t)"
by (metis A.arrE B.arrE A.sources_resid B.sources_resid equals0D image_subset_iff
A.arr_iff_has_target preserves_reflects_arr preserves_resid preserves_sources)

lemma preserves_trg:
assumes "A.arr t"
shows "F (A.trg t) = B.trg (F t)"
using assms A.trg_def B.trg_def by auto

lemma preserves_composites:
assumes "A.composite_of t u v"
shows "B.composite_of (F t) (F u) (F v)"
using assms
by (metis A.composite_ofE A.prfx_implies_con