Theory DiscreteCategory

(*  Title:       DiscreteCategory
    Author:      Eugene W. Stark <>, 2016
    Maintainer:  Eugene W. Stark <>

chapter DiscreteCategory

theory DiscreteCategory
imports Category

    The locale defined here permits us to construct a discrete category having
    a specified set of objects, assuming that the set does not exhaust the elements
    of its type.  In that case, we have the convenient situation that the arrows of
    the category can be directly identified with the elements of the given set,
    rather than having to pass between the two via tedious coercion maps.
    If it cannot be guaranteed that the given set is not the universal set at its type,
    then the more general discrete category construction defined (using coercions)
    in FreeCategory› can be used.

  locale discrete_category =
    fixes Obj :: "'a set"
    and Null :: 'a
    assumes Null_not_in_Obj: "Null  Obj"

    definition comp :: "'a comp"      (infixr "" 55)
    where "y  x  (if x  Obj  x = y then x else Null)"

    interpretation partial_composition comp
      apply unfold_locales
      using comp_def by metis

    lemma null_char:
    shows "null = Null"
      using comp_def null_def by auto

    lemma ide_char [iff]:
    shows "ide f  f  Obj"
      using comp_def null_char ide_def Null_not_in_Obj by auto

    lemma domains_char:
    shows "domains f = {x. x  Obj  x = f}"
      unfolding domains_def
      using ide_char ide_def comp_def null_char by metis

    theorem is_category:
    shows "category comp"
      using comp_def
      apply unfold_locales
      using arr_def null_char self_domain_iff_ide ide_char
           apply fastforce
      using null_char self_codomain_iff_ide domains_char codomains_def ide_char
          apply fastforce
         apply (metis not_arr_null null_char)
        apply (metis not_arr_null null_char)
      by auto


  sublocale discrete_category  category comp
    using is_category by auto

  context discrete_category

    lemma arr_char [iff]:
    shows "arr f  f  Obj"
      using comp_def comp_cod_arr
      by (metis empty_iff has_codomain_iff_arr not_arr_null null_char self_codomain_iff_ide ide_char)

    lemma dom_char [simp]:
    shows "dom f = (if f  Obj then f else null)"
      using arr_def dom_def arr_char ideD(2) by auto

    lemma cod_char [simp]:
    shows "cod f = (if f  Obj then f else null)"
      using arr_def in_homE cod_def ideD(3) by auto

    lemma comp_char [simp]:
    shows "comp g f = (if f  Obj  f = g then f else null)"
      using comp_def null_char by auto

    lemma is_discrete:
    shows "ide = arr"
      using arr_char ide_char by auto

    lemma seq_char [iff]:
    shows "seq f g  ide f  f = g"
      using is_discrete by (metis (full_types) ide_def seqE)