Theory ResiduatedTransitionSystem

(*  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_charWE:
    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 seqIWE [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 seqEWE [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_iffWE:
    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_iffWE:
    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 coinitialIWE [intro]:
    assumes "arr t" and "src t = src u"
    shows "coinitial t u"
      using assms coinitial_iffWE by (metis arr_src_iff_arr)

    lemma coinitialEWE [elim]:
    assumes "coinitial t u"
    and "arr t; arr u; src t = src u  T"
    shows T
      using assms coinitial_iffWE by blast

    lemma coterminalIWE [intro]:
    assumes "arr t" and "trg t = trg u"
    shows "coterminal t u"
      using assms coterminal_iffWE by (metis arr_trg_iff_arr)

    lemma coterminalEWE [elim]:
    assumes "coterminal t u"
    and "arr t; arr u; trg t = trg u  T"
    shows T
      using assms coterminal_iffWE 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_conE:
    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_joinE [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_joinE(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_assocE:
    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_joinE(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_joinE(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_joinE(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_joinE(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_joinE(3) prfx_implies_con)
        also have "... = t \\ v  (u \\ v  v \\ v)"
          by (metis 1 conE conI con_sym join_def resid_joinE(1) resid_joinE(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_joinE(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_joinE(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_joinE(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_joinE(1) trg_def)
          thus ?thesis
            by (metis tu arr_prfx_join_self conE join_src prfx_implies_con resid_joinE(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_joinE(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_joinE(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_joinE(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_joinE(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_joinE(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_joinEJ [simp]:
    assumes "t  u"
    shows "src (t  u) = src t"
      using assms
      by (meson has_joins src_join)

    lemma trg_joinEJ:
    assumes "t  u"
    shows "trg (t  u) = trg (t \\ u)"
      using assms
      by (meson has_joins trg_join)

    lemma resid_joinEJ [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_joinE [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_joinE(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_joinE(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_compEC [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_compEEC [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_compEC [simp]:
    assumes "seq t u"
    shows "trg (t  u) = trg u"
      by (meson assms has_composites trg_comp)

    lemma src_compEC [simp]:
    assumes "seq t u"
    shows "src (t  u) = src t"
      using assms src_comp has_composites by simp

    lemma con_comp_iffEC [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_assocEC:
    shows "t  (u  v) = (t  u)  v"
      apply (cases "seq t u")
       apply (metis arr_comp comp_assoc comp_def not_arr_null arr_compEEC arr_compEC
                    seq_implies_arr_comp trg_compEC)
      by (metis comp_def composable_iff_arr_comp seqIWE(1) src_comp arr_compEEC)

    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_compEC 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_compEC seqEWE)
      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_iffEC(2) con_imp_eq_src
            con_implies_arr(2) con_sym comp_resid_prfx prfx_comp resid_comp(1)
            arr_compEEC arr_compEC 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_iffWE con_imp_coinitial
            seqIWE(2) src_resid conI)
      also have "... = w \\ (t \\ u)"
        by (metis (no_types, lifting) "1" arr_compEC 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_compEEC prfx_comp resid_comp(1) arr_resid_iff_con
                   seq_implies_arr_comp)
       apply (metis assms comp_resid_prfx arr_compEEC 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_compEC)
      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_iffEC(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_joinEC:
    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_compEEC joinable_iff_arr_join
              seqIWE(1)
        by metis
      have "con (t  u) (t  u')"
        using 1 2 arr_comp arr_compEEC assms(2) comp_assocEC 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_compEC)
      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 (