Theory FreeCategory

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

chapter FreeCategory

theory FreeCategory
imports Category ConcreteCategory
begin

  text‹
    This theory defines locales for constructing the free category generated by
    a graph, as well as some special cases, including the discrete category generated
    by a set of objects, the ``quiver'' generated by a set of arrows, and a ``parallel pair''
    of arrows, which is the diagram shape required for equalizers.
    Other diagram shapes can be constructed in a similar fashion.
›

  section Graphs

  text‹
    The following locale gives a definition of graphs in a traditional style.
›

  locale graph =
  fixes Obj :: "'obj set"
  and Arr :: "'arr set"
  and Dom :: "'arr  'obj"
  and Cod :: "'arr  'obj"
  assumes dom_is_obj: "x  Arr  Dom x  Obj"
  and cod_is_obj: "x  Arr  Cod x  Obj"
  begin

    text‹
      The list of arrows @{term p} forms a path from object @{term x} to object @{term y}
      if the domains and codomains of the arrows match up in the expected way.
›

    definition path
    where "path x y p  (p = []  x = y  x  Obj) 
                        (p  []  x = Dom (hd p)  y = Cod (last p) 
                        (n. n  0  n < length p  nth p n  Arr) 
                        (n. n  0  n < (length p)-1  Cod (nth p n) = Dom (nth p (n+1))))"

    lemma path_Obj:
    assumes "x  Obj"
    shows "path x x []"
      using assms path_def by simp

    lemma path_single_Arr:
    assumes "x  Arr"
    shows "path (Dom x) (Cod x) [x]"
      using assms path_def by simp

    lemma path_concat:
    assumes "path x y p" and "path y z q"
    shows "path x z (p @ q)"
    proof -
      have "p = []  q = []  ?thesis"
        using assms path_def by auto
      moreover have "p  []  q  []  ?thesis"
      proof -
        assume pq: "p  []  q  []"
        have Cod_last: "Cod (last p) = Cod (nth (p @ q) ((length p)-1))"
          using assms pq by (simp add: last_conv_nth nth_append)
        moreover have Dom_hd: "Dom (hd q) = Dom (nth (p @ q) (length p))"
          using assms pq by (simp add: hd_conv_nth less_not_refl2 nth_append)
        show ?thesis
        proof -
          have 1: "n. n  0  n < length (p @ q)  nth (p @ q) n  Arr"
          proof -
            fix n
            assume n: "n  0  n < length (p @ q)"
            have "(n  0  n < length p)  (n  length p  n < length (p @ q))"
              using n by auto
            thus "nth (p @ q) n  Arr"
              using assms pq nth_append path_def le_add_diff_inverse length_append
                    less_eq_nat.simps(1) nat_add_left_cancel_less
              by metis
          qed
          have 2: "n. n  0  n < length (p @ q) - 1 
                                    Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
          proof -
            fix n
            assume n: "n  0  n < length (p @ q) - 1"
            have 1: "(n  0  n < (length p) - 1)  (n  length p  n < length (p @ q) - 1)
                        n = (length p) - 1"
              using n by auto
            thus "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
            proof -
              have "n  0  n < (length p) - 1  ?thesis"
                using assms pq nth_append path_def by (metis add_lessD1 less_diff_conv)
              moreover have "n = (length p) - 1  ?thesis"
                using assms pq nth_append path_def Dom_hd Cod_last by simp
              moreover have "n  length p  n < length (p @ q) - 1  ?thesis"
              proof -
                assume 1: "n  length p  n < length (p @ q) - 1"
                have "Cod (nth (p @ q) n) = Cod (nth q (n - length p))"
                  using 1 nth_append leD by metis
                also have "... = Dom (nth q (n - length p + 1))"
                  using 1 assms(2) path_def by auto
                also have "... = Dom (nth (p @ q) (n + 1))"
                  using 1 nth_append
                  by (metis Nat.add_diff_assoc2 ex_least_nat_le le_0_eq le_add1 le_neq_implies_less
                            le_refl le_trans length_0_conv pq)
                finally show "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n + 1))" by auto
              qed
              ultimately show ?thesis using 1 by auto
            qed
          qed
          show ?thesis
            unfolding path_def using assms pq path_def hd_append2 Cod_last Dom_hd 1 2
            by simp
        qed
      qed
      ultimately show ?thesis by auto
    qed

  end

  section "Free Categories"

  text‹
    The free category generated by a graph has as its arrows all triples @{term "MkArr x y p"},
    where @{term x} and @{term y} are objects and @{term p} is a path from @{term x} to @{term y}.
    We construct it here an instance of the general construction given by the
    @{locale concrete_category} locale.
›

  locale free_category =
    G: graph Obj Arr D C
  for Obj :: "'obj set"
  and Arr :: "'arr set"
  and D :: "'arr  'obj"
  and C :: "'arr  'obj"
  begin

    type_synonym ('o, 'a) arr = "('o, 'a list) concrete_category.arr"

    sublocale concrete_category Obj :: 'obj set λx y. Collect (G.path x y)
      λ_. [] λ_ _ _ g f. f @ g
      using G.path_Obj G.path_concat
      by (unfold_locales, simp_all)

    abbreviation comp      (infixr "" 55)
    where "comp  COMP"
    notation in_hom     ("«_ : _  _»")

    abbreviation Path
    where "Path  Map"

    lemma arr_single [simp]:
    assumes "x  Arr"
    shows "arr (MkArr (D x) (C x) [x])"
      using assms
      by (simp add: G.cod_is_obj G.dom_is_obj G.path_single_Arr)

  end

  section "Discrete Categories"

  text‹
    A discrete category is a category in which every arrow is an identity.
    We could construct it as the free category generated by a graph with no
    arrows, but it is simpler just to apply the @{locale concrete_category}
    construction directly.
›

  locale discrete_category =
  fixes Obj :: "'obj set"
  begin

    type_synonym 'o arr = "('o, unit) concrete_category.arr"

    sublocale concrete_category Obj :: 'obj set λx y. if x = y then {x} else {}
      λx. x λ_ _ x _ _. x
      apply unfold_locales
          apply simp_all
        apply (metis empty_iff)
      by (metis empty_iff singletonD)

    abbreviation comp      (infixr "" 55)
    where "comp  COMP"
    notation in_hom        ("«_ : _  _»")

    lemma is_discrete:
    shows "arr f  ide f"
      using ide_charCC arr_char by simp

    lemma arr_char:
    shows "arr f  Dom f  Obj  f = MkIde (Dom f)"
      using is_discrete
      by (metis (no_types, lifting) cod_char dom_char ide_MkIde ide_charCC ide_char')

    lemma arr_char':
    shows "arr f  f  MkIde ` Obj"
      using arr_char image_iff by auto

    lemma dom_char:
    shows "dom f = (if arr f then f else null)"
      using dom_char is_discrete by simp

    lemma cod_char:
    shows "cod f = (if arr f then f else null)"
      using cod_char is_discrete by simp

    lemma in_hom_char:
    shows "«f : a  b»  arr f  f = a  f = b"
      using is_discrete by auto

    lemma seq_char:
    shows "seq g f  arr f  f = g"
      using is_discrete
      by (metis (no_types, lifting) comp_arr_dom seqE dom_char)
    
    lemma comp_char:
    shows "g  f = (if seq g f then f else null)"
    proof -
      have "¬ seq g f  ?thesis"
        using comp_char by presburger
      moreover have "seq g f  ?thesis"
        using seq_char comp_char comp_arr_ide is_discrete
        by (metis (no_types, lifting))
      ultimately show ?thesis by blast
    qed

  end

  text‹
    The empty category is the discrete category generated by an empty set of objects.
›

  locale empty_category =
    discrete_category "{} :: unit set"
  begin

    lemma is_empty:
    shows "¬arr f"
      using arr_char by simp

  end

  section "Quivers"

  text‹
    A quiver is a two-object category whose non-identity arrows all point in the
    same direction.  A quiver is specified by giving the set of these non-identity arrows.
›

  locale quiver =
  fixes Arr :: "'arr set"
  begin

    type_synonym 'a arr = "(unit, 'a) concrete_category.arr"

    sublocale free_category "{False, True}" Arr "λ_. False" "λ_. True"
      by (unfold_locales, simp_all)

    notation comp                  (infixr "" 55)
    notation in_hom                ("«_ : _  _»")

    definition Zero
    where "Zero  MkIde False"

    definition One
    where "One  MkIde True"

    definition fromArr
    where "fromArr x  if x  Arr then MkArr False True [x] else null"

    definition toArr
    where "toArr f  hd (Path f)"

    lemma ide_char:
    shows "ide f  f = Zero  f = One"
    proof -
      have "ide f  f = MkIde False  f = MkIde True"
        using ide_charCC concrete_category.MkIde_Dom' concrete_category_axioms by fastforce
      thus ?thesis
        using comp_def Zero_def One_def by simp
    qed

    lemma arr_char':
    shows "arr f  f =
           MkIde False  f = MkIde True  f  (λx. MkArr False True [x]) ` Arr"
    proof
      assume f: "f = MkIde False  f = MkIde True  f  (λx. MkArr False True [x]) ` Arr"
      show "arr f" using f by auto
      next
      assume f: "arr f"
      have "¬(f = MkIde False  f = MkIde True)  f  (λx. MkArr False True [x]) ` Arr"
      proof -
        assume f': "¬(f = MkIde False  f = MkIde True)"
        have 0: "Dom f = False  Cod f = True"
          using f f' arr_char G.path_def MkArr_Map by fastforce
        have 1: "f = MkArr False True (Path f)"
          using f 0 arr_char MkArr_Map by force
        moreover have "length (Path f) = 1"
        proof -
          have "length (Path f)  0"
            using f f' 0 arr_char G.path_def by simp
          moreover have "x y p. length p > 1  ¬ G.path x y p"
            using G.path_def less_diff_conv by fastforce
          ultimately show ?thesis
            using f arr_char
            by (metis less_one linorder_neqE_nat mem_Collect_eq)
        qed
        moreover have "p. length p = 1  (x. p = [x])"
          by (auto simp: length_Suc_conv)
        ultimately have "x. x  Arr  Path f = [x]"
          using f G.path_def arr_char
          by (metis (no_types, lifting) Cod.simps(1) Dom.simps(1) le_eq_less_or_eq
              less_numeral_extra(1) mem_Collect_eq nth_Cons_0)
        thus "f  (λx. MkArr False True [x]) ` Arr"
          using 1 by auto
      qed
      thus "f = MkIde False  f = MkIde True  f  (λx. MkArr False True [x]) ` Arr"
        by auto
    qed

    lemma arr_char:
    shows "arr f  f = Zero  f = One  f  fromArr ` Arr"
      using arr_char' Zero_def One_def fromArr_def by simp

    lemma dom_char:
    shows "dom f = (if arr f then
                      if f = One then One else Zero
                    else null)"
    proof -
      have "¬ arr f  ?thesis"
        using dom_char by simp
      moreover have "arr f  ?thesis"
      proof -
        assume f: "arr f"
        have 1: "dom f = MkIde (Dom f)"
          using f dom_char by simp
        have "f = One  ?thesis"
          using f 1 One_def by (metis (full_types) Dom.simps(1))
        moreover have "f = Zero  ?thesis"
          using f 1 Zero_def by (metis (full_types) Dom.simps(1))
        moreover have "f  fromArr ` Arr  ?thesis"
          using f fromArr_def G.path_def Zero_def calculation(1) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma cod_char:
    shows "cod f = (if arr f then
                      if f = Zero then Zero else One
                    else null)"
    proof -
      have "¬ arr f  ?thesis"
        using cod_char by simp
      moreover have "arr f  ?thesis"
      proof -
        assume f: "arr f"
        have 1: "cod f = MkIde (Cod f)"
          using f cod_char by simp
        have "f = One  ?thesis"
          using f 1 One_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f = Zero  ?thesis"
          using f 1 Zero_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f  fromArr ` Arr  ?thesis"
          using f fromArr_def G.path_def One_def calculation(2) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma seq_char:
    shows "seq g f  arr g  arr f  ((f = Zero  g  One)  (f  Zero  g = One))"
    proof
      assume gf: "arr g  arr f  ((f = Zero  g  One)  (f  Zero  g = One))"
      show "seq g f"
        using gf dom_char cod_char by auto
      next
      assume gf: "seq g f"
      hence 1: "arr f  arr g  dom g = cod f" by auto
      have "Cod f = False  f = Zero"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def cod_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "Cod f = True  g = One"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def dom_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "¬(f = MkIde False  g = MkIde True)"
        using 1 by auto
      ultimately show "arr g  arr f  ((f = Zero  g  One)  (f  Zero  g = One))"
        using gf arr_char One_def Zero_def by blast
    qed

    lemma not_ide_fromArr:
    shows "¬ ide (fromArr x)"
      using fromArr_def ide_char ide_def Zero_def One_def
      by (metis Cod.simps(1) Dom.simps(1))

    lemma in_hom_char:
    shows "«f : a  b»  (a = Zero  b = Zero  f = Zero) 
                            (a = One  b = One  f = One) 
                            (a = Zero  b = One  f  fromArr ` Arr)"
    proof -
      have "f = Zero  ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) Zero_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr imageE is_category not_ide_fromArr)
      moreover have "f = One  ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) One_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr image_iff is_category not_ide_fromArr)
      moreover have "f  fromArr ` Arr  ?thesis"
      proof -
        assume f: "f  fromArr ` Arr"
        have 1: "arr f" using f arr_char by simp
        moreover have "dom f = Zero  cod f = One"
          using f 1 arr_char dom_char cod_char fromArr_def
          by (metis (no_types, lifting) ide_char imageE not_ide_fromArr)
        ultimately have "in_hom f Zero One" by auto
        thus "in_hom f a b  (a = Zero  b = Zero  f = Zero 
                                           a = One  b = One  f = One 
                                           a = Zero  b = One  f  fromArr ` Arr)"
          using f ide_char by auto
      qed
      ultimately show ?thesis
        using arr_char [of f] by fast
    qed

    lemma Zero_not_eq_One [simp]:
    shows "Zero  One"
      by (simp add: One_def Zero_def)

    lemma Zero_not_eq_fromArr [simp]:
    shows "Zero  fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma One_not_eq_fromArr [simp]:
    shows "One  fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma comp_char:
    shows "g  f = (if seq g f then
                      if f = Zero then g else if g = One then f else null
                    else null)"
    proof -
      have "seq g f  f = Zero  g  f = g"
        using seq_char comp_char [of g f] Zero_def dom_char cod_char comp_arr_dom
        by auto
      moreover have "seq g f  g = One  g  f = f"
        using seq_char comp_char [of g f] One_def dom_char cod_char comp_cod_arr
        by simp
      moreover have "seq g f  f  Zero  g  One  g  f = null"
        using seq_char Zero_def One_def by simp
      moreover have "¬seq g f  g  f = null"
        using comp_char ext by fastforce
      ultimately show ?thesis by argo
    qed

    lemma comp_simp [simp]:
    assumes "seq g f"
    shows "f = Zero  g  f = g"
    and "g = One  g  f = f"
      using assms seq_char comp_char by metis+

    lemma arr_fromArr:
    assumes "x  Arr"
    shows "arr (fromArr x)"
      using assms fromArr_def arr_char image_eqI by simp

    lemma toArr_in_Arr:
    assumes "arr f" and "¬ide f"
    shows "toArr f  Arr"
    proof -
      have "a. a  Arr  Path (fromArr a) = [a]"
        using fromArr_def arr_char by simp
      hence "hd (Path f)  Arr"
        using assms arr_char ide_char by auto
      thus ?thesis
        by (simp add: toArr_def)
    qed

    lemma toArr_fromArr [simp]:
    assumes "x  Arr"
    shows "toArr (fromArr x) = x"
      using assms fromArr_def toArr_def
      by (simp add: toArr_def)

    lemma fromArr_toArr [simp]:
    assumes "arr f" and "¬ide f"
    shows "fromArr (toArr f) = f"
      using assms fromArr_def toArr_def arr_char ide_char toArr_fromArr by auto

  end

  section "Parallel Pairs"

  text‹
    A parallel pair is a quiver with two non-identity arrows.
    It is important in the definition of equalizers.
›

  locale parallel_pair =
    quiver "{False, True} :: bool set"
  begin

    typedef arr = "UNIV :: bool quiver.arr set" ..

    definition j0
    where "j0  fromArr False"

    definition j1
    where "j1  fromArr True"

    lemma arr_char:
    shows "arr f  f = Zero  f = One  f = j0  f = j1"
      using arr_char j0_def j1_def by simp

    lemma dom_char:
    shows "dom f = (if f = j0  f = j1 then Zero else if arr f then f else null)"
      using arr_char dom_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma cod_char:
    shows "cod f = (if f = j0  f = j1 then One else if arr f then f else null)"
      using arr_char cod_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma j0_not_eq_j1 [simp]:
    shows "j0  j1"
      using j0_def j1_def
      by (metis insert_iff toArr_fromArr)

    lemma Zero_not_eq_j0 [simp]:
    shows "Zero  j0"
      using Zero_def j0_def Zero_not_eq_fromArr by auto

    lemma Zero_not_eq_j1 [simp]:
    shows "Zero  j1"
      using Zero_def j1_def Zero_not_eq_fromArr by auto

    lemma One_not_eq_j0 [simp]:
    shows "One  j0"
      using One_def j0_def One_not_eq_fromArr by auto

    lemma One_not_eq_j1 [simp]:
    shows "One  j1"
      using One_def j1_def One_not_eq_fromArr by auto

    lemma dom_simp [simp]:
    shows "dom Zero = Zero"
    and "dom One = One"
    and "dom j0 = Zero"
    and "dom j1 = Zero"
      using dom_char arr_char by auto

    lemma cod_simp [simp]:
    shows "cod Zero = Zero"
    and "cod One = One"
    and "cod j0 = One"
    and "cod j1 = One"
      using cod_char arr_char by auto

  end

end