Structure simpleSetCatTheory

signature simpleSetCatTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Delta_def : thm
    val Gr_def : thm
    val RIMAGE_def : thm
    val RINV_IMAGE_def : thm
    val SPO_def : thm
    val SPO_pimg_def : thm
    val SPOr_def : thm
    val cardgt_def : thm
    val eps_def : thm
    val kernel_def : thm
    val restr_def : thm
    val shom_def : thm
    val span_def : thm
  
  (*  Theorems  *)
    val Delta_IMAGE : thm
    val Delta_INTER : thm
    val Gr_Id : thm
    val Gr_restr : thm
    val IN_UNCURRY : thm
    val RIMAGE_Gr : thm
    val RINV_IMAGE_Gr : thm
    val SPOr_REFL : thm
    val SPOr_lemma : thm
    val Spushout_def : thm
    val Spushout_ind : thm
    val Spushout_quotient : thm
    val Spushout_sym : thm
    val Spushout_transfer : thm
    val Spushouts_iso : thm
    val cardgt0 : thm
    val cardgt1_INJ_bool : thm
    val eps_partition : thm
    val kernel_graph : thm
    val oID : thm
    val restr_EMPTY : thm
    val restr_applies : thm
    val restr_cases : thm
    val restr_restr_o : thm
    val shom_into_EMPTY : thm
    val shom_outof_EMPTY : thm
    val shoms_exist : thm
    val symmetric_SPOr : thm
    val transitive_SPOr : thm
    val unit_pushout : thm
  
  val simpleSetCat_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [cardinal] Parent theory of "simpleSetCat"
   
   [Delta_def]  Definition
      
      ⊢ ∀V a b. Δ V a b ⇔ a = b ∧ a ∈ V
   
   [Gr_def]  Definition
      
      ⊢ ∀h A a b. Gr h A a b ⇔ a ∈ A ∧ b = h a
   
   [RIMAGE_def]  Definition
      
      ⊢ ∀f A R x y.
          RIMAGE f A R x y ⇔
          ∃x0 y0. x = f x0 ∧ y = f y0 ∧ R x0 y0 ∧ x0 ∈ A ∧ y0 ∈ A
   
   [RINV_IMAGE_def]  Definition
      
      ⊢ ∀f A R x y. RINV_IMAGE f A R x y ⇔ x ∈ A ∧ y ∈ A ∧ R (f x) (f y)
   
   [SPO_def]  Definition
      
      ⊢ ∀A B C f g.
          SPO A B C f g =
          (partition (SPOr A f g) (B ⊔ C),
           restr (λb. {a | a ∈ B ⊔ C ∧ SPOr A f g (INL b) a}) B,
           restr (λc. {a | a ∈ B ⊔ C ∧ SPOr A f g (INR c) a}) C)
   
   [SPO_pimg_def]  Definition
      
      ⊢ (∀A f g x. SPO_pimg A f g (INL x) = PREIMAGE f {x} ∩ A) ∧
        ∀A f g y. SPO_pimg A f g (INR y) = PREIMAGE g {y} ∩ A
   
   [SPOr_def]  Definition
      
      ⊢ ∀A f g.
          SPOr A f g =
          (λx y. (∃a. a ∈ A ∧ x = INL (f a) ∧ y = INR (g a)) ∨ x = y)^=
   
   [cardgt_def]  Definition
      
      ⊢ ∀n. cardgt (:α) n ⇔ FINITE 𝕌(:α) ⇒ n < CARD 𝕌(:α)
   
   [eps_def]  Definition
      
      ⊢ ∀R A a. eps R A a = if a ∈ A then {b | R a b ∧ b ∈ A} else ARB
   
   [kernel_def]  Definition
      
      ⊢ ∀A f x y. kernel A f x y ⇔ x ∈ A ∧ y ∈ A ∧ f x = f y
   
   [restr_def]  Definition
      
      ⊢ ∀f s. restr f s = (λx. if x ∈ s then f x else ARB)
   
   [shom_def]  Definition
      
      ⊢ ∀f A B. shom f A B ⇔ (∀a. a ∈ A ⇒ f a ∈ B) ∧ ∀a. a ∉ A ⇒ f a = ARB
   
   [span_def]  Definition
      
      ⊢ ∀A f g b d. span A f g b d ⇔ ∃a. a ∈ A ∧ b = f a ∧ d = g a
   
   [Delta_IMAGE]  Theorem
      
      ⊢ Δ (IMAGE f A) = RIMAGE f A (Δ A)
   
   [Delta_INTER]  Theorem
      
      ⊢ Δ (s ∩ t) = Δ s ∩ᵣ Δ t
   
   [Gr_Id]  Theorem
      
      ⊢ Gr (λx. x) A = Δ A
   
   [Gr_restr]  Theorem
      
      ⊢ Gr (restr f A) A = Gr f A
   
   [IN_UNCURRY]  Theorem
      
      ⊢ (a,b) ∈ UNCURRY R ⇔ R a b
   
   [RIMAGE_Gr]  Theorem
      
      ⊢ RIMAGE f A R = Gr f A ∘ᵣ R ∘ᵣ (Gr f A)ᵀ
   
   [RINV_IMAGE_Gr]  Theorem
      
      ⊢ RINV_IMAGE f A R = (Gr f A)ᵀ ∘ᵣ R ∘ᵣ Gr f A
   
   [SPOr_REFL]  Theorem
      
      ⊢ SPOr A f g x x
   
   [SPOr_lemma]  Theorem
      
      ⊢ restr (j1 ∘ f) A = restr (j2 ∘ g) A ⇒
        (∀b1 b2. SPOr A f g (INL b1) (INL b2) ⇒ j1 b1 = j1 b2) ∧
        (∀b c. SPOr A f g (INL b) (INR c) ⇒ j1 b = j2 c) ∧
        (∀b' c'. SPOr A f g (INR c') (INL b') ⇒ j1 b' = j2 c') ∧
        ∀c1 c2. SPOr A f g (INR c1) (INR c2) ⇒ j2 c1 = j2 c2
   
   [Spushout_def]  Theorem
      
      ⊢ Spushout A B C' f g (P,i1,i2) (:δ) ⇔
        shom f A B ∧ shom g A C' ∧ shom i1 B P ∧ shom i2 C' P ∧
        restr (i1 ∘ f) A = restr (i2 ∘ g) A ∧
        ∀Q j1 j2.
          shom j1 B Q ∧ shom j2 C' Q ∧ restr (j1 ∘ f) A = restr (j2 ∘ g) A ⇒
          ∃!u. shom u P Q ∧ restr (u ∘ i1) B = j1 ∧ restr (u ∘ i2) C' = j2
   
   [Spushout_ind]  Theorem
      
      ⊢ ∀P'.
          (∀A B C f g P i1 i2. P' A B C f g (P,i1,i2) (:δ)) ⇒
          ∀v v1 v2 v3 v4 v5 v6 v7 v8. P' v v1 v2 v3 v4 (v5,v6,v7) v8
   
   [Spushout_quotient]  Theorem
      
      ⊢ shom f A B ∧ shom g A C ⇒ Spushout A B C f g (SPO A B C f g) (:δ)
   
   [Spushout_sym]  Theorem
      
      ⊢ Spushout A B C f g (P,p1,p2) (:δ) ⇒
        Spushout A C B g f (P,p2,p1) (:δ)
   
   [Spushout_transfer]  Theorem
      
      ⊢ Spushout A B C f g (P,i1,i2) (:δ) ∧ INJ h 𝕌(:ε) 𝕌(:δ) ⇒
        Spushout A B C f g (P,i1,i2) (:ε)
   
   [Spushouts_iso]  Theorem
      
      ⊢ Spushout A B C f g (P,i1,i2) (:ε) ∧
        Spushout A B C f g (Q,j1,j2) (:δ) ∧ cardgt (:δ) 1 ∧ cardgt (:ε) 1 ⇒
        ∃H. BIJ H P Q ∧ restr (H ∘ i1) B = j1 ∧ restr (H ∘ i2) C = j2
   
   [cardgt0]  Theorem
      
      ⊢ cardgt (:α) 0
   
   [cardgt1_INJ_bool]  Theorem
      
      ⊢ cardgt (:α) 1 ⇔ ∃bf. INJ bf {T; F} 𝕌(:α)
   
   [eps_partition]  Theorem
      
      ⊢ a ∈ A ⇒ eps R A a ∈ partition R A
   
   [kernel_graph]  Theorem
      
      ⊢ kernel A f = (Gr f A)ᵀ ∘ᵣ Gr f A
   
   [oID]  Theorem
      
      ⊢ f ∘ (λx. x) = f ∧ (λx. x) ∘ f = f
   
   [restr_EMPTY]  Theorem
      
      ⊢ restr f ∅ = K ARB
   
   [restr_applies]  Theorem
      
      ⊢ x ∈ A ⇒ restr f A x = f x
   
   [restr_cases]  Theorem
      
      ⊢ restr f A x = g x ⇔ x ∈ A ∧ f x = g x ∨ x ∉ A ∧ g x = ARB
   
   [restr_restr_o]  Theorem
      
      ⊢ restr (f ∘ restr g A) A = restr (f ∘ g) A
   
   [shom_into_EMPTY]  Theorem
      
      ⊢ shom f A ∅ ⇔ A = ∅ ∧ f = K ARB
   
   [shom_outof_EMPTY]  Theorem
      
      ⊢ shom f ∅ A ⇔ f = K ARB
   
   [shoms_exist]  Theorem
      
      ⊢ ∀A B. B ≠ ∅ ⇒ ∃h. shom h A B
   
   [symmetric_SPOr]  Theorem
      
      ⊢ symmetric (SPOr A f g)
   
   [transitive_SPOr]  Theorem
      
      ⊢ transitive (SPOr A f g)
   
   [unit_pushout]  Theorem
      
      ⊢ shom f A B ∧ shom g A C ∧ A ≠ ∅ ⇒
        Spushout A B C f g ({()},restr (K ()) B,restr (K ()) C) (:unit)
   
   
*)
end

HOL 4, Kananaskis-14