Theory ConcreteRTSCategory

(*  Title:       ConcreteRTSCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2024
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

theory ConcreteRTSCategory
imports Main RTSCategory
begin

  section "Concrete RTS-Categories"

  text‹
    If we are given a set ‹Obj› of ``objects'', a mapping ‹Hom› that assigns to every two
    objects ‹A› and ‹B› an extensional ``hom-RTS'' RTS ‹Hom A B›, a mapping ‹Id› that assigns
    to each object ‹A› an ``identity arrow'' ‹Id A› of ‹Hom A B›, and a mapping ‹Comp› that
    assigns to every three objects ‹A›, ‹B›, ‹C› a ``composition law''
    ‹Comp A B C› from ‹Hom B C × Hom A B› to ‹Hom A B›, subject to suitable identity and
    associativity conditions, then we can form from this data an RTS-category whose
    underlying set of arrows is the disjoint union of the sets of arrows of the hom-RTS's.
  ›

  locale concrete_rts_category =
  fixes obj_type :: "'O itself"
  and arr_type :: "'A itself"
  and Obj :: "'O set"
  and Hom :: "'O ⇒ 'O ⇒ 'A resid"
  and Id :: "'O ⇒ 'A"
  and Comp :: "'O ⇒ 'O ⇒ 'O ⇒ 'A ⇒ 'A ⇒ 'A"
  assumes rts_Hom: "⟦ A ∈ Obj; B ∈ Obj ⟧ ⟹ extensional_rts (Hom A B)"
  and binary_simulation_Comp:
        "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj ⟧
            ⟹ binary_simulation
                  (Hom B C) (Hom A B) (Hom A C) (λ(t, u). Comp A B C t u)"
  and ide_Id: "A ∈ Obj ⟹ residuation.ide (Hom A A) (Id A)"
  and Comp_Hom_Id: "⟦ A ∈ Obj; B ∈ Obj; residuation.arr (Hom A B) t ⟧
                       ⟹ Comp A A B t (Id A) = t"
  and Comp_Id_Hom: "⟦ A ∈ Obj; B ∈ Obj; residuation.arr (Hom A B) u ⟧
                       ⟹ Comp A B B (Id B) u = u"
  and Comp_assoc: "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; D ∈ Obj;
                     residuation.arr (Hom C D) t; residuation.arr (Hom B C) u;
                     residuation.arr (Hom A B) v ⟧ ⟹
                      Comp A B D (Comp B C D t u) v =
                      Comp A C D t (Comp A B C u v)"
  begin

    datatype ('o, 'a) arr =
      Null
    | MkArr 'o 'o 'a

    fun Dom :: "('O, 'A) arr ⇒ 'O"
    where "Dom (MkArr a _ _) = a"
        | "Dom _ = undefined"

    fun Cod :: "('O, 'A) arr ⇒ 'O"
    where "Cod (MkArr _ b _) = b"
        | "Cod _ = undefined"

    fun Trn :: "('O, 'A) arr ⇒ 'A"
    where "Trn (MkArr _ _ t) = t"
        | "Trn _ = undefined"

    abbreviation Arr :: "('O, 'A) arr ⇒ bool"
    where "Arr ≡ λt. t ≠ Null ∧ Dom t ∈ Obj ∧ Cod t ∈ Obj ∧
                     residuation.arr (Hom (Dom t) (Cod t)) (Trn t)"

    abbreviation Ide :: "('O, 'A) arr ⇒ bool"
    where "Ide ≡ λt. t ≠ Null ∧ Dom t ∈ Obj ∧ Cod t ∈ Obj ∧
                     residuation.ide (Hom (Dom t) (Cod t)) (Trn t)"

    abbreviation Con :: "('O, 'A) arr ⇒ ('O, 'A) arr ⇒ bool"
    where "Con t u ≡ Arr t ∧ Arr u ∧ Dom t = Dom u ∧ Cod t = Cod u ∧
                     residuation.con (Hom (Dom t) (Cod t)) (Trn t) (Trn u)"

    fun resid  (infix "\\" 70)
    where "resid Null u = Null"
        | "resid t Null = Null"
        | "resid t u =
           (if Con t u
            then MkArr (Dom t) (Cod t) (Hom (Dom t) (Cod t) (Trn t) (Trn u))
            else Null)"

    sublocale V: ResiduatedTransitionSystem.partial_magma resid
      apply unfold_locales
      by (metis Trn.cases resid.simps(1-2))

    lemma null_char:
    shows "V.null = Null"
      by (metis V.null_is_zero(2) resid.simps(1))

    sublocale V: residuation resid
    proof
      fix t u :: "('O, 'A) arr"
      assume tu: "t \\ u ≠ V.null"
      interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
        using tu null_char rts_Hom
        by (metis arr.exhaust V.null_is_zero(2) resid.simps(1,3))
      show "t \\ u ≠ V.null ⟹ u \\ t ≠ V.null"
        using null_char hom.con_sym
        apply (cases t; cases u)
           apply auto[3]
        by (metis arr.simps(2) resid.simps(3))
      show "(t \\ u) \\ (t \\ u) ≠ V.null"
        using tu null_char hom.arr_resid hom.con_arr_self
        apply (cases "t \\ u")
         apply force
        apply (cases t; cases u)
           apply auto[3]
        by (metis Cod.simps(1) Dom.simps(1) Trn.simps(1)
            arr.simps(2) resid.simps(3))
      next
      fix t u v :: "('O, 'A) arr"
      assume tuv: "(v \\ t) \\ (u \\ t) ≠ V.null"
      have tu: "Con t u"
        using tuv null_char V.null_is_zero(2) resid.simps(3)
        apply (cases t; cases u; cases v)
               apply auto[7]
        by (metis extensional_rts_def residuation.con_sym
            rts_Hom rts_def)
      have tv: "Con t v"
        using tu tuv null_char resid.simps(1,3)
        apply (cases t; cases u; cases v)
               apply auto[7]
        by (metis extensional_rts_def residuation.con_sym
            rts_Hom rts_def)
      interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
        using tu null_char rts_Hom by metis
      have uv: "Con u v"
        using tu tv tuv null_char hom.con_sym
              resid.simps(1,3) rts_Hom
        apply (cases t; cases u; cases v)
               apply auto[7]
        apply (intro conjI)
                  apply auto[10]
        by auto (metis Cod.simps(1) Dom.simps(1) hom.resid_reflects_con)
      interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
        using tu null_char rts_Hom by blast
      show "(v \\ t) \\ (u \\ t) = (v \\ u) \\ (t \\ u)"
        using tu tv uv null_char hom.arr_resid_iff_con
              hom.con_sym hom.cube
        apply (cases t; cases u; cases v)
        by auto metis+
    qed

    notation V.con  (infix "⌢" 50)

    lemma con_char:
    shows "t ⌢ u ⟷ Con t u"
    proof
      show "t ⌢ u ⟹ Con t u"
        using V.con_def V.not_con_null(2) null_char
        apply (cases t; cases u)
           apply auto[3]
        by fastforce
      show "Con t u ⟹ t ⌢ u"
        using null_char
        by (cases t; cases u) auto
    qed

    lemma arr_char:
    shows "V.arr t ⟷ Arr t"
      by (metis V.arr_def con_char extensional_rts_def
          residuation.arr_def rts_Hom rts_def)

    lemma arrI [intro]:
    assumes "t ≠ V.null" and "Dom t ∈ Obj" and "Cod t ∈ Obj"
    and "residuation.arr (Hom (Dom t) (Cod t)) (Trn t)"
    shows "V.arr t"
      using assms arr_char null_char by auto

    lemma arrE [elim]:
    assumes "V.arr t"
    and "⟦t ≠ V.null; Dom t ∈ Obj; Cod t ∈ Obj;
          residuation.arr (Hom (Dom t) (Cod t)) (Trn t)⟧
            ⟹ T"
    shows T
      using assms arr_char by fastforce

    lemma sta_char:
    shows "V.ide t ⟷ Ide t"
    proof
      assume t: "V.ide t"
      interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
        using t
        by (meson V.ide_implies_arr arrE rts_Hom)
      show "Ide t"
        using t null_char V.not_ide_null
        apply (cases t)
         apply force
        by (metis Trn.simps(1) V.ideE hom.ideI resid.simps(3))
      next
      assume t: "Ide t"
      show "V.ide t"
      proof (cases t)
        show "t = Null ⟹ ?thesis"
          using t V.ide_def con_char by blast
        fix A B F
        assume 1: "t = MkArr A B F"
        interpret hom: extensional_rts ‹Hom A B›
          using t 1 rts_Hom by simp
        show "V.ide t"
          using t 1 V.con_def V.ide_def null_char by auto
      qed
    qed

    lemma staI [intro]:
    assumes "t ≠ V.null" and "Dom t ∈ Obj" and "Cod t ∈ Obj"
    and "residuation.ide (Hom (Dom t) (Cod t)) (Trn t)"
    shows "V.ide t"
      using assms sta_char null_char by auto

    lemma staE [elim]:
    assumes "V.ide t"
    and "⟦t ≠ V.null; Dom t ∈ Obj; Cod t ∈ Obj;
          residuation.ide (Hom (Dom t) (Cod t)) (Trn t)⟧
             ⟹ T"
    shows T
      using assms sta_char by fastforce

    lemma trg_char:
    shows "V.trg t =
           (if V.arr t
            then MkArr (Dom t) (Cod t)
                   (residuation.trg (Hom (Dom t) (Cod t)) (Trn t))
            else Null)"
    proof (cases "V.arr t")
      show "¬ V.arr t ⟹ ?thesis"
        using V.trg_def null_char V.con_def by auto
      assume t: "V.arr t"
      interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
        using t
        by (meson V.ide_implies_arr arrE rts_Hom)
      show ?thesis
          using t null_char
          apply (cases t)
           apply fastforce
          by (metis V.trg_def arrE hom.conI hom.ide_trg
              hom.not_ide_null hom.trg_def resid.simps(3))
    qed

    lemma con_implies_Par:
    assumes "t ⌢ u"
    shows "Dom t = Dom u" and "Cod t = Cod u"
      using assms con_char by blast+

    lemma Dom_resid [simp]:
    assumes "t ⌢ u"
    shows "Dom (t \\ u) = Dom t"
      using assms con_char
      by (cases t; cases u) auto

    lemma Cod_resid [simp]:
    assumes "t ⌢ u"
    shows "Cod (t \\ u) = Cod t"
      using assms con_char
      by (cases t; cases u) auto

    lemma Trn_resid [simp]:
    assumes "t ⌢ u"
    shows "Trn (t \\ u) = Hom (Dom t) (Cod t) (Trn t) (Trn u)"
      using assms con_char
      by (cases t; cases u) auto

    sublocale rts resid
    proof
      show "⋀t. V.arr t ⟹ V.ide (V.trg t)"
        by (simp add: arr_char extensional_rts.axioms(1) rts.ide_trg
            rts_Hom sta_char trg_char)
      show 1: "⋀a t. ⟦V.ide a; t ⌢ a⟧ ⟹ t \\ a = t"
      proof -
        fix a t
        assume a: "V.ide a"
        assume con: "t ⌢ a"
        have "t \\ a ≠ Null ∧ t ≠ Null"
          using con null_char by auto
        moreover have "Dom (t \\ a) = Dom t"
          using a con by simp
        moreover have "Cod (t \\ a) = Cod t"
          using a con by simp
        moreover have "Trn (t \\ a) = Trn t"
          using a con apply simp
          by (metis con_char extensional_rts_def sta_char rts.resid_arr_ide rts_Hom)
        ultimately show "t \\ a = t"
          by (metis Cod.elims Dom.simps(1) Trn.simps(1))
      qed
      show "⋀a t. ⟦V.ide a; a ⌢ t⟧ ⟹ V.ide (a \\ t)"
        using sta_char con_char
        by (metis 1 V.arr_resid V.con_arr_self V.con_sym V.cube V.ideE V.ideI)
      show "⋀t u. t ⌢ u ⟹ ∃a. V.ide a ∧ a ⌢ t ∧ a ⌢ u"
      proof -
        fix t u
        assume tu: "t ⌢ u"
        interpret hom: extensional_rts ‹Hom (Dom t) (Cod t)›
          using tu con_char arr_char [of t] rts_Hom by auto
        have 1: "hom.con (Trn t) (Trn u)"
          using tu con_char by auto
        obtain α where α: "hom.ide α ∧ hom.con α (Trn t) ∧ hom.con α (Trn u)"
          using 1 hom.con_imp_coinitial_ax by auto
        have "V.ide (MkArr (Dom t) (Cod t) α)"
          using tu α V.con_implies_arr arr_char sta_char by auto
        moreover have "MkArr (Dom t) (Cod t) α ⌢ t"
          using α tu con_char hom.ide_implies_arr by auto
        moreover have "MkArr (Dom t) (Cod t) α ⌢ u"
          using α tu con_char hom.ide_implies_arr by auto
        ultimately show "∃a. V.ide a ∧ a ⌢ t ∧ a ⌢ u" by blast
      qed
      show "⋀t u v. ⟦V.ide (t \\ u); u ⌢ v⟧ ⟹ t \\ u ⌢ v \\ u"
      proof -
        fix t u v
        assume tu: "V.ide (t \\ u)"
        assume uv: "u ⌢ v"
        have 1: "t \\ u ≠ V.null"
          using tu by auto
        interpret HOM: extensional_rts ‹Hom (Dom t) (Cod t)›
          using 1 con_char arr_char [of t] rts_Hom by auto
        have 2: "HOM.con (Hom (Dom t) (Cod t) (Trn t) (Trn u))
                         (Hom (Dom t) (Cod t) (Trn v) (Trn u))"
          by (metis (no_types, lifting) Cod_resid Dom_resid HOM.con_target
              Trn_resid V.conI con_char staE tu uv)
        have 3: "Con t u"
          using 1 con_char by blast
        have 4: "Con v u"
          using uv con_char V.con_sym by blast
        have 5: "t \\ u = MkArr (Dom t) (Cod t)
                                (Hom (Dom t) (Cod t) (Trn t) (Trn u))"
          using 1 3
          by (cases t; cases u) auto
        have 6: "v \\ u = MkArr (Dom v) (Cod v)
                                (Hom (Dom v) (Cod t) (Trn v) (Trn u))"
          using 3 4
          by (cases v; cases u) auto
        show "t \\ u ⌢ v \\ u"
          using 2 3 4 5 6 HOM.con_implies_arr(1-2) con_char by auto
      qed
    qed

    lemma is_rts:
    shows "rts resid"
      ..

    sublocale V: extensional_rts resid
    proof
      fix t u
      assume tu: "cong t u"
      have 1: "t \\ u ≠ V.null"
        using tu by auto
      interpret HOM: extensional_rts ‹Hom (Dom t) (Cod t)›
        using 1 con_char arr_char [of t] rts_Hom by auto
      have "t ≠ Null ∧ u ≠ Null"
        using tu con_char by blast
      moreover have "Dom t = Dom u"
        using tu con_char by blast
      moreover have "Cod t = Cod u"
        using tu con_char by blast
      moreover have "Trn t = Trn u"
        by (metis calculation(2-3) Cod_resid Dom_resid Trn_resid sta_char
            congE HOM.cong_char tu)
      ultimately show "t = u"
        by (metis Cod.elims Dom.simps(1) Trn.simps(1))
    qed

    lemma is_extensional_rts:
    shows "extensional_rts resid"
      ..

    lemma arr_MkArr [intro]:
    assumes "a ∈ Obj" and "b ∈ Obj"
    and "residuation.arr (Hom a b) t"
    shows "V.arr (MkArr a b t)"
      using assms arr_char by auto

    lemma arr_eqI:
    assumes "t ≠ Null" and "u ≠ Null"
    and "Dom t = Dom u" and "Cod t = Cod u" and "Trn t = Trn u"
    shows "t = u"
      using assms null_char
      by (metis Cod.elims Dom.simps(1) Trn.simps(1))

    lemma MkArr_Trn:
    assumes "V.arr t"
    shows "MkArr (Dom t) (Cod t) (Trn t) = t"
      using assms null_char V.not_arr_null
      by (intro arr_eqI) auto

    lemma src_char:
    shows "V.src t = (if V.arr t
                      then MkArr (Dom t) (Cod t)
                             (weakly_extensional_rts.src (Hom (Dom t) (Cod t)) (Trn t))
                      else Null)"
    proof (cases "V.arr t")
      show "¬ V.arr t ⟹ ?thesis"
        by (simp add: V.src_def null_char)
      assume t: "V.arr t"
      interpret HOM: extensional_rts ‹Hom (Dom t) (Cod t)›
        using t con_char arr_char rts_Hom by auto
      show ?thesis
        using t
        by (metis (no_types, lifting) Cod.simps(1) Dom.simps(1) HOM.src_eqI
            Trn.simps(1) V.con_arr_src(2) V.ide_src arr.simps(2) arr_eqI
            con_char staE)
    qed

    definition hcomp  (infixr "⋆" 53)
    where "t ⋆ u ≡ if V.arr t ∧ V.arr u ∧ Dom t = Cod u
                    then MkArr (Dom u) (Cod t)
                               (Comp (Dom u) (Cod u) (Cod t) (Trn t) (Trn u))
                    else V.null"

    lemma arr_hcomp⇩C⇩R⇩C:
    assumes "V.arr t" and "V.arr u" and "Dom t = Cod u"
    shows "V.arr (t ⋆ u)"
    proof -
      let ?a = "Dom u" and ?b = "Cod u" and ?c = "Cod t"
      interpret Comp: binary_simulation ‹Hom ?b ?c› ‹Hom ?a ?b› ‹Hom ?a ?c›
                        ‹λ(t, u). Comp ?a ?b ?c t u›
        using assms arr_char binary_simulation_Comp by auto
      let ?tu = "MkArr ?a ?c (Comp ?a ?b ?c (Trn t) (Trn u))"
      have "V.arr ?tu"
        using assms arr_char Comp.preserves_reflects_arr [of "(Trn t, Trn u)"]
        by simp
      thus ?thesis
        using assms hcomp_def by simp
    qed

    lemma Dom_hcomp [simp]:
    assumes "V.arr t" and "V.arr u" and "Dom t = Cod u"
    shows "Dom (t ⋆ u) = Dom u"
      using assms hcomp_def by auto

    lemma Cod_hcomp [simp]:
    assumes "V.arr t" and "V.arr u" and "Dom t = Cod u"
    shows "Cod (t ⋆ u) = Cod t"
      using assms hcomp_def by auto

    lemma Trn_hcomp [simp]:
    assumes "V.arr t" and "V.arr u" and "Dom t = Cod u"
    shows "Trn (t ⋆ u) = Comp (Dom u) (Cod u) (Cod t) (Trn t) (Trn u)"
      using assms hcomp_def by auto

    lemma hcomp_Null [simp]:
    shows "t ⋆ Null = Null" and "Null ⋆ u = Null"
      using hcomp_def null_char by fastforce+

    sublocale H: Category.partial_magma hcomp
      using hcomp_def V.not_arr_null
      by unfold_locales metis

    lemma null_coincidence⇩C⇩R⇩C [simp]:
    shows "H.null = V.null"
      using hcomp_def
      by (metis H.null_eqI V.not_arr_null)

    sublocale H: partial_composition hcomp ..

    lemma H_composable_char:
    shows "t ⋆ u ≠ V.null ⟷ V.arr t ∧ V.arr u ∧ Dom t = Cod u"
      using hcomp_def null_char by auto

    lemma objI [intro]:
    assumes "t ≠ V.null"
    and "Dom t ∈ Obj" and "Cod t = Dom t" and "Trn t = Id (Dom t)"
    shows "H.ide t"
      using assms
      by (metis Comp_Hom_Id Comp_Id_Hom H.ide_def MkArr_Trn
          V.ide_implies_arr arrE hcomp_def ide_Id null_coincidence⇩C⇩R⇩C staI)

    lemma objE [elim]:
    assumes "H.ide a"
    and "⟦a ≠ V.null; Dom a ∈ Obj; Cod a = Dom a; Trn a = Id (Dom a)⟧ ⟹ T"
    shows T
      using assms
      by (metis Cod.simps(1) Dom.simps(1) H.ide_def H_composable_char
          Trn.simps(1) arr.simps(2) arr_char null_char null_coincidence⇩C⇩R⇩C objI)

    definition mkobj
    where "mkobj A ≡ MkArr A A (Id A)"

    lemma mkobj_simps [simp]:
    shows "Dom (mkobj A) = A" and "Cod (mkobj A) = A"
    and "Trn (mkobj A) = Id A"
      using mkobj_def by auto

    lemma obj_mkobj:
    assumes "A ∈ Obj"
    shows "H.ide (mkobj A)"
      using assms
      by (simp add: mkobj_def null_char objI)

    lemma obj_char:
    shows "H.ide a ⟷ V.arr a ∧ mkobj (Dom a) = a"
      by (metis H.ide_def H_composable_char MkArr_Trn arrE mkobj_def
          objE obj_mkobj)

    lemma obj_is_sta:
    assumes "H.ide a"
    shows "V.ide a"
      using assms ide_Id by fastforce

    lemma obj_simps:
    assumes "H.ide a"
    shows "Cod a = Dom a" and "Trn a = Id (Dom a)"
      using assms by auto

    lemma domains_char:
    shows "H.domains t = {a. V.arr t ∧ mkobj (Dom t) = a}"
      unfolding H.domains_def
      using H_composable_char obj_char obj_mkobj obj_simps(1) by auto

    lemma codomains_char:
    shows "H.codomains t = {a. V.arr t ∧ mkobj (Cod t) = a}"
      unfolding H.codomains_def
      using H_composable_char obj_char obj_mkobj obj_simps(1) by auto

    lemma H_arr_char:
    shows "H.arr t ⟷ t ≠ Null ∧ Dom t ∈ Obj ∧ Cod t ∈ Obj ∧
                       residuation.arr (Hom (Dom t) (Cod t)) (Trn t)"
      using H.arr_def codomains_char domains_char arr_char by force

    lemma H_arrI [intro]:
    assumes "t ≠ V.null" and "Dom t ∈ Obj" and "Cod t ∈ Obj"
    and "residuation.arr (Hom (Dom t) (Cod t)) (Trn t)"
    shows "H.arr t"
      using assms H_arr_char null_char by auto

    lemma H_seq_char:
    shows "H.seq t u ⟷ V.arr t ∧ V.arr u ∧ Dom t = Cod u"
      by (metis H_arr_char H_composable_char arr_char arr_hcomp⇩C⇩R⇩C null_char)

    lemma H_seqI [intro]:
    assumes "V.arr t" and "V.arr u" and "Dom t = Cod u"
    shows "H.seq t u"
      using assms H_seq_char by blast

    sublocale H: category hcomp
    proof
      show "⋀t u. hcomp t u ≠ H.null ⟹ H.seq t u"
        using hcomp_def H_seq_char null_char
        by (metis null_coincidence⇩C⇩R⇩C)
      show "⋀t. (H.domains t ≠ {}) = (H.codomains t ≠ {})"
        by (simp add: codomains_char domains_char)
      show "⋀h g f. ⟦H.seq h g; H.seq (h ⋆ g) f⟧ ⟹ H.seq g f"
        using H_seq_char
        by (metis Dom.simps(1) hcomp_def)
      show "⋀h g f. ⟦H.seq h (g ⋆ f); H.seq g f⟧ ⟹ H.seq h g"
        using H_seq_char
        by (metis Cod.simps(1) hcomp_def)
      show "⋀g f h. ⟦H.seq g f; H.seq h g⟧ ⟹ H.seq (h ⋆ g) f"
        using H_seq_char
        by (metis Dom.simps(1) arr_hcomp⇩C⇩R⇩C hcomp_def)
      show "⋀t u v. ⟦H.seq u v; H.seq t u⟧ ⟹ (t ⋆ u) ⋆ v = t ⋆ u ⋆ v"
        using arr_hcomp⇩C⇩R⇩C H_seq_char H_composable_char null_char Comp_assoc
        apply (intro arr_eqI)
            apply auto[4]
        apply auto
        using H_arr_char arr_char by auto
    qed

    lemma is_category:
    shows "category hcomp"
      ..

    lemma arr_coincidence⇩C⇩R⇩C [simp]:
    shows "H.arr = V.arr"
      using H_arr_char arr_char by blast

    lemma dom_char:
    shows "H.dom = (λt. if H.arr t then mkobj (Dom t) else V.null)"
      using domains_char H.dom_in_domains H.has_domain_iff_arr H.dom_def
      by auto

    lemma dom_mkobj [simp]:
    assumes "A ∈ Obj"
    shows "H.dom (mkobj A) = mkobj A"
      using assms obj_mkobj by auto

    lemma mkobj_Dom [simp]:
    assumes "H.ide a"
    shows "mkobj (Dom a) = H.dom a"
      using assms obj_char by auto

    lemma cod_char:
    shows "H.cod = (λt. if H.arr t then mkobj (Cod t) else V.null)"
      using codomains_char H.cod_in_codomains H.has_codomain_iff_arr H.cod_def
      by auto

    lemma cod_mkobj [simp]:
    assumes "A ∈ Obj"
    shows "H.cod (mkobj A) = mkobj A"
      using assms obj_mkobj by auto

    lemma Dom_dom [simp]:
    assumes "V.arr t"
    shows "Dom (H.dom t) = Dom t"
      using assms dom_char mkobj_def by auto

    lemma Dom_cod [simp]:
    assumes "V.arr t"
    shows "Dom (H.cod t) = Cod t"
      using assms cod_char mkobj_def by auto

    lemma Cod_dom [simp]:
    assumes "V.arr t"
    shows "Cod (H.dom t) = Dom t"
      using assms dom_char mkobj_def by auto

    lemma Cod_cod [simp]:
    assumes "V.arr t"
    shows "Cod (H.cod t) = Cod t"
      using assms cod_char mkobj_def by auto

    lemma con_implies_par:
    assumes "V.con t u"
    shows "H.par t u"
      using assms cod_char dom_char V.con_implies_arr(1-2) con_implies_Par(1-2)
      by auto

    lemma par_resid:
    assumes "V.con t u"
    shows "H.par t (resid t u)"
      using assms cod_char dom_char V.con_implies_arr(1-2) con_implies_Par(1-2)
      by auto

    lemma simulation_dom:
    shows "simulation resid resid H.dom"
      using dom_char arr_char H_arr_char con_char
      apply unfold_locales
        apply presburger
       apply (metis (no_types, lifting) H.arr_dom V.arrE)
      by (metis (no_types, lifting) H.ide_dom par_resid V.ideE obj_is_sta)

    lemma simulation_cod:
    shows "simulation resid resid H.cod"
      using cod_char arr_char H_arr_char con_char
      apply unfold_locales
        apply presburger
       apply (metis (no_types, lifting) H.arr_cod V.arr_def)
      by (metis (no_types, lifting) H.ide_cod par_resid V.ideE obj_is_sta)

    sublocale dom: simulation resid resid H.dom
      using simulation_dom by blast
    sublocale cod: simulation resid resid H.cod
      using simulation_cod by blast

    sublocale VV: fibered_product_rts resid resid resid H.dom H.cod ..

    sublocale H⇩V⇩V: simulation VV.resid resid
                     ‹λt. if VV.arr t then fst t ⋆ snd t else V.null›
    proof
      let ?C = "λt. if VV.arr t then fst t ⋆ snd t else V.null"
      show "⋀t. ¬ VV.arr t ⟹ ?C t = V.null"
        by simp
      fix t u
      assume tu: "VV.con t u"
      have arr_t: "VV.arr t" and arr_u: "VV.arr u"
        using tu VV.con_implies_arr by blast+
      have t: "V.arr (fst t) ∧ V.arr (snd t) ∧ Dom (fst t) = Cod (snd t)"
        by (metis Cod_cod Cod_dom VV.arr_char arr_t)
      have u: "V.arr (fst u) ∧ V.arr (snd u) ∧ Dom (fst u) = Cod (snd u)"
        by (metis Cod_cod Cod_dom VV.arr_char arr_u)
      let ?a = "Dom (snd t)" and ?b = "Cod (snd t)" and ?c = "Cod (fst t)"
      have a: "?a ∈ Obj" and b: "?b ∈ Obj" and c: "?c ∈ Obj"
        using tu VV.con_char VV.con_implies_arr sta_char arr_char by fast+
      interpret AB: extensional_rts ‹Hom ?a ?b›
        using a b rts_Hom by simp
      interpret BC: extensional_rts ‹Hom ?b ?c›
        using b c rts_Hom by simp
      interpret AC: extensional_rts ‹Hom ?a ?c›
        using a c rts_Hom by simp
      interpret BCxAB: product_rts ‹Hom ?b ?c› ‹Hom ?a ?b› ..
      interpret Comp: binary_simulation ‹Hom ?b ?c› ‹Hom ?a ?b› ‹Hom ?a ?c›
                        ‹λ(t', u'). Comp ?a ?b ?c t' u'›
        using a b c binary_simulation_Comp by simp
      have 0: "BCxAB.con (Trn (fst t), Trn (snd t)) (Trn (fst u), Trn (snd u))"
        by (metis BCxAB.con_char VV.con_char con_char fst_conv snd_conv t tu)
      have 1: "Dom (snd u) = ?a" and 2: "Cod (fst u) = ?c"
      and 3: "Cod (snd u) = ?b"
        using VV.con_char con_char tu by metis+
      show 4: "?C t ⌢ ?C u"
        using a c t u tu 0 1 2 3 VV.arr_char VV.con_char hcomp_def
             AC.con_implies_arr con_char
              Comp.preserves_con
                [of "(Trn (fst t), Trn (snd t))" "(Trn (fst u), Trn (snd u))"]
        by simp
      show "?C (VV.resid t u) = ?C t \\ ?C u"
      proof -
        have Con: "VV.Con t u"
          using tu VV.con_char by blast
        have "?C (VV.resid t u) = fst t \\ fst u ⋆ snd t \\ snd u"
          using tu Con VV.arr_char VV.arr_resid VV.resid_def by auto
        also have "... = (fst t ⋆ snd t) \\ (fst u ⋆ snd u)"
            using t u tu arr_t arr_u 0 1 2 3 4 Con VV.con_char null_char
                  H_composable_char BCxAB.resid_def Comp.preserves_resid
            by (intro arr_eqI) auto
        also have "... = ?C t \\ ?C u"
          using arr_t arr_u by auto
        finally show ?thesis by blast
      qed
    qed

    lemma simulation_hcomp:
    shows "simulation VV.resid resid (λt. if VV.arr t then fst t ⋆ snd t else V.null)"
      ..

    lemma Dom_src [simp]:
    assumes "V.arr t"
    shows "Dom (V.src t) = Dom t"
      using assms con_implies_Par(1) by simp

    lemma Dom_trg [simp]:
    assumes "V.arr t"
    shows "Dom (V.trg t) = Dom t"
      using assms V.trg_def by simp

    lemma Cod_src [simp]:
    assumes "V.arr t"
    shows "Cod (V.src t) = Cod t"
      using assms con_implies_Par(2) by simp

    lemma Cod_trg [simp]:
    assumes "V.arr t"
    shows "Cod (V.trg t) = Cod t"
      using assms V.trg_def by simp

    lemma dom_src⇩C⇩R⇩C [simp]:
    shows "H.dom (V.src t) = H.dom t"
      by (metis V.arr_src_iff_arr V.con_arr_src(2) con_implies_par dom.extensional)

    lemma dom_trg⇩C⇩R⇩C [simp]:
    shows "H.dom (V.trg t) = H.dom t"
      by (metis H.dom_dom V.arr_def V.trg_def dom.extensional null_char
          par_resid trg_char)

    lemma cod_src⇩C⇩R⇩C [simp]:
    shows "H.cod (V.src t) = H.cod t"
      by (simp add: cod_char V.arr_src_iff_arr)

    lemma cod_trg⇩C⇩R⇩C [simp]:
    shows "H.cod (V.trg t) = H.cod t"
      by (simp add: cod_char V.arr_trg_iff_arr)

    lemma src_dom⇩C⇩R⇩C [simp]:
    shows "V.src (H.dom t) = H.dom t"
      by (metis H.ide_dom dom_char V.src_ide arr_char src_char null_char obj_is_sta)

    lemma trg_dom⇩C⇩R⇩C [simp]:
    shows "V.trg (H.dom t) = H.dom t"
      by (metis H.cod_dom V.ide_iff_src_self V.trg_ide cod.extensional
          null_char src_dom⇩C⇩R⇩C trg_char)

    lemma src_cod⇩C⇩R⇩C [simp]:
    shows "V.src (H.cod t) = H.cod t"
      by (metis H.dom_cod src_dom⇩C⇩R⇩C)

    lemma trg_cod⇩C⇩R⇩C [simp]:
    shows "V.trg (H.cod t) = H.cod t"
      by (metis cod.extensional cod.preserves_trg cod_trg⇩C⇩R⇩C dom.extensional
          trg_dom⇩C⇩R⇩C)

    sublocale rts_category resid hcomp
      by unfold_locales auto

    proposition is_rts_category:
    shows "rts_category resid hcomp"
      ..

    text‹
      The elements of the originally given set ‹Obj› are in bijective correspondence
      with the objects of the constructed RTS-category.
    ›

    lemma bij_mkobj:
    shows "mkobj ∈ Obj → Collect obj"
    and "Dom ∈ Collect obj → Obj"
    and "⋀A. Dom (mkobj A) = A"
    and "⋀a. obj a ⟹ mkobj (Dom a) = a"
    and "bij_betw mkobj Obj (Collect obj)"
    and "bij_betw Dom (Collect obj) Obj"
      using obj_mkobj obj_char arr_char
      apply auto[6]
      by (intro bij_betwI, auto)+

    abbreviation MkArr⇩e⇩x⇩t
    where "MkArr⇩e⇩x⇩t A B ≡
           λt. if residuation.arr (Hom A B) t then MkArr A B t else Null"

    abbreviation Trn⇩e⇩x⇩t
    where "Trn⇩e⇩x⇩t a b ≡
           λt. if residuation.arr (HOM a b) t then Trn t
               else ResiduatedTransitionSystem.partial_magma.null
                     (Hom (Dom a) (Dom b))"

    lemma inverse_simulations_Trn_MkArr:
    assumes "A ∈ Obj" and "B ∈ Obj"
    shows "inverse_simulations (Hom A B) (HOM (mkobj A) (mkobj B))
             (Trn⇩e⇩x⇩t (mkobj A) (mkobj B)) (MkArr⇩e⇩x⇩t A B)"
    proof -
      interpret Hom_AB: rts ‹Hom A B›
        using assms
        by (simp add: extensional_rts.axioms(1) rts_Hom)
      let ?a = "mkobj A" and ?b = "mkobj B"
      let ?F = "MkArr⇩e⇩x⇩t A B"
      let ?G = "Trn⇩e⇩x⇩t (mkobj A) (mkobj B)"
      have a: "obj ?a" and b: "obj ?b"
        using assms obj_char obj_mkobj by auto
      interpret HOM_ab: sub_rts resid ‹λt. «t : ?a → ?b»›
        using assms sub_rts_HOM by simp
      interpret F: simulation ‹Hom A B› ‹HOM ?a ?b› ?F
        using assms a b HOM_ab.con_char HOM_ab.null_char null_char
              Hom_AB.con_implies_arr(1-2) H.in_homI cod_char dom_char arr_char
              HOM_ab.resid_def con_char
        by unfold_locales auto
      interpret G: simulation ‹HOM ?a ?b› ‹Hom A B› ?G
      proof
        show "⋀t. ¬ HOM_ab.arr t ⟹ Trn⇩e⇩x⇩t ?a ?b t = Hom_AB.null"
          by simp
        fix t u
        assume tu: "HOM_ab.con t u"
        show con: "Hom_AB.con (?G t) (?G u)"
          using assms a b tu HOM_ab.arr_char HOM_ab.con_char con_char
          apply auto[1]
          by (metis Cod.simps(1) Cod_cod Cod_dom H.in_homE arr_char mkobj_def)
        show "?G (HOM ?a ?b t u) = Hom A B (?G t) (?G u)"
          using assms tu con HOM_ab.con_char HOM_ab.resid_def HOM_ab.resid_closed
          apply auto[1]
          by (metis Cod_dom Dom_cod H.in_homE HOM_ab.inclusion mkobj_simps(1-2))
      qed
      show "inverse_simulations (Hom A B) (HOM ?a ?b) ?G ?F"
      proof
        show "?F ∘ ?G = I HOM_ab.resid"
        proof
          fix t
          show "(?F ∘ ?G) t = I HOM_ab.resid t"
            using assms a b MkArr_Trn HOM_ab.arr_char HOM_ab.null_char
                  arr_char null_char
            apply auto[1]
             apply (metis Cod_dom Dom_cod H.in_homE HOM_ab.inclusion mkobj_simps(1-2))
            by (metis Cod_dom Dom_cod H.in_homE H_arr_char mkobj_simps(1-2))
        qed
        show "?G ∘ ?F = I (Hom A B)"
          using assms a b by auto
      qed
    qed

    text‹
      Each hom-RTS of the constructed RTS-category is isomorphic to the corresponding
      RTS given by ‹Hom›.
    ›

    lemma isomorphic_rts_Hom_HOM:
    assumes "A ∈ Obj" and "B ∈ Obj"
    shows "isomorphic_rts (Hom A B) (HOM (mkobj A) (mkobj B))"
      using assms inverse_simulations_Trn_MkArr isomorphic_rts_def by blast

  end

end