Theory "coalgAxioms"

Signature

Axioms

mapID

⊢ mapF (λx. x) = (λa. a)

mapO

⊢ mapF f ∘ mapF g = mapF (f ∘ g)

map_CONG

⊢ ∀f g y. (∀x. x ∈ setF y ⇒ (f x = g x)) ⇒ (mapF f y = mapF g y)

relO

⊢ relF R ∘ᵣ relF S ⊆ᵣ relF (R ∘ᵣ S)

set_map

⊢ setF ∘ mapF f = IMAGE f ∘ setF

Definitions

Fset_def

⊢ ∀A. Fset A = {af | setF af ⊆ A}

bisim_def

⊢ ∀R A af B bf.
    bisim R (A,af) (B,bf) ⇔
    system (A,af) ∧ system (B,bf) ∧
    ∀a b. R a b ⇒ a ∈ A ∧ b ∈ B ∧ relF R (af a) (bf b)

bisimilar_def

⊢ ∀As Bs. bisimilar As Bs ⇔ ∃R. bisim R As Bs

bquot_def

⊢ ∀A af R.
    bquot (A,af) R =
    (partition R A,(λap. mapF (eps R A) (af (CHOICE ap)))⟨partition R A⟩)

gbisim_def

⊢ ∀A af x y. gbisim (A,af) x y ⇔ ∃R. bisim R (A,af) (A,af) ∧ R x y

genS_def

⊢ ∀As X. genS As X = BIGINTER {V | subsystem V As ∧ X ⊆ V}

hom_def

⊢ ∀h A af B bf.
    hom h (A,af) (B,bf) ⇔
    system (A,af) ∧ system (B,bf) ∧
    (∀a. a ∈ A ⇒ h a ∈ B ∧ (bf (h a) = mapF h (af a))) ∧
    ∀a. a ∉ A ⇒ (h a = ARB)

iso_def

⊢ ∀A af B bf.
    iso (A,af) (B,bf) ⇔
    ∃f g.
      hom f (A,af) (B,bf) ∧ hom g (B,bf) (A,af) ∧
      (∀a. a ∈ A ⇒ (g (f a) = a)) ∧ ∀b. b ∈ B ⇒ (f (g b) = b)

relF_def

⊢ ∀R x y. relF R x y ⇔ ∃z. setF z ⊆ Rᴾ ∧ (mapF FST z = x) ∧ (mapF SND z = y)

simple_def

⊢ ∀A. simple A ⇔ ∀R. bisim R A A ⇒ ∀x y. R x y ⇒ (x = y)

subsystem_def

⊢ ∀V A af.
    subsystem V (A,af) ⇔
    system (A,af) ∧ V ⊆ A ∧ ∃vf. hom (λx. x)⟨V⟩ (V,vf) (A,af)

system_def

⊢ ∀A af.
    system (A,af) ⇔ (∀a. a ∈ A ⇒ af a ∈ Fset A) ∧ ∀a. a ∉ A ⇒ (af a = ARB)

Theorems

BIJ_homs_iso

⊢ hom f (A,af) (B,bf) ∧ BIJ f A B ⇒ iso (A,af) (B,bf)

Fpushout_def

⊢ Fpushout (A,af) (B,bf) (C',cf) f g ((P,pf),i1,i2) (:δ) ⇔
  hom f (A,af) (B,bf) ∧ hom g (A,af) (C',cf) ∧ hom i1 (B,bf) (P,pf) ∧
  hom i2 (C',cf) (P,pf) ∧ ((i1 ∘ f)⟨A⟩ = (i2 ∘ g)⟨A⟩) ∧
  ∀Q qf j1 j2.
    hom j1 (B,bf) (Q,qf) ∧ hom j2 (C',cf) (Q,qf) ∧ ((j1 ∘ f)⟨A⟩ = (j2 ∘ g)⟨A⟩) ⇒
    ∃!u. hom u (P,pf) (Q,qf) ∧ ((u ∘ i1)⟨B⟩ = j1) ∧ ((u ∘ i2)⟨C'⟩ = j2)

Fpushout_ind

⊢ ∀P'.
    (∀A af B bf C cf f g P pf i1 i2.
       P' (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:δ)) ⇒
    ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12.
      P' (v,v1) (v2,v3) (v4,v5) v6 v7 ((v8,v9),v10,v11) v12

INJ_homs_mono

⊢ hom f (A,af) (B,bf) ∧ INJ f A B ⇒
  ∀C cf g h.
    hom g (C,cf) (A,af) ∧ hom h (C,cf) (A,af) ∧ (f ∘ g = f ∘ h) ⇒ (g = h)

SURJ_homs_epi

⊢ hom f (A,af) (B,bf) ∧ SURJ f A B ⇒ epi f (A,af) (B,bf) (:γ)

UNIV_system

⊢ system (𝕌(:α),af)

bisim_RUNION

⊢ bisim R1 As Bs ∧ bisim R2 As Bs ⇒ bisim (R1 ∪ᵣ R2) As Bs

bisim_gbisim

⊢ system (A,af) ⇒ bisim (gbisim (A,af)) (A,af) (A,af)

bisim_system

⊢ bisim R As Bs ⇒ system As ∧ system Bs

bisimilar_equivalence

⊢ bisimilar equiv_on system

bisimulations_compose

⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒ bisim (Q ∘ᵣ R) (A,af) (C,cf)

bounded_def

⊢ bounded (:α) (:β) ⇔
  ∀a A af. system (A,af) ∧ a ∈ A ⇒ ∃f V. INJ f (genS (A,af) {a}) V

bounded_ind

⊢ ∀P. P (:α) (:β) ⇒ ∀v v1. P v v1

bquot_coequalizer

⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  ∃Rf.
    coequalizer (Rᴾ,Rf) (A,af) FST⟨Rᴾ⟩ SND⟨Rᴾ⟩ (bquot (A,af) R,eps R A) (:δ)

bquot_correct

⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)

coequalizer_def

⊢ coequalizer (A,af) (B,bf) f1 f2 ((C',cf),g) (:δ) ⇔
  hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧ hom g (B,bf) (C',cf) ∧
  ((g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩) ∧
  ∀h D df.
    hom h (B,bf) (D,df) ∧ ((h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩) ⇒
    ∃!u. hom u (C',cf) (D,df) ∧ (h = (u ∘ g)⟨B⟩)

coequalizer_ind

⊢ ∀P. (∀A af B bf f1 f2 C cf g. P (A,af) (B,bf) f1 f2 ((C,cf),g) (:δ)) ⇒
      ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9. P (v,v1) (v2,v3) v4 v5 ((v6,v7),v8) v9

coequalizer_thm

⊢ coequalizer (A,af) (B,bf) f1 f2 (Cs,g) (:δ) ⇔
  hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧ hom g (B,bf) Cs ∧
  ((g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩) ∧
  ∀h D df.
    hom h (B,bf) (D,df) ∧ ((h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩) ⇒
    ∃!u. hom u Cs (D,df) ∧ (h = (u ∘ g)⟨B⟩)

epi_Fpushout

⊢ epi f (A,af) (B,bf) (:γ) ⇔
  Fpushout (A,af) (B,bf) (B,bf) f f ((B,bf),(λx. x)⟨B⟩,(λx. x)⟨B⟩) (:γ)

epi_def

⊢ epi f (A,af) (B,bf) (:γ) ⇔
  hom f (A,af) (B,bf) ∧
  ∀C cf g h.
    hom g (B,bf) (C,cf) ∧ hom h (B,bf) (C,cf) ∧ ((g ∘ f)⟨A⟩ = (h ∘ f)⟨A⟩) ⇒
    (g = h)

epi_ind

⊢ ∀P. (∀f A af B bf. P f (A,af) (B,bf) (:γ)) ⇒
      ∀v v1 v2 v3 v4 v5. P v (v1,v2) (v3,v4) v5

gbisim_equivalence

⊢ system (A,af) ⇒ gbisim (A,af) equiv_on A

genS_correct

⊢ system (A,af) ∧ X ⊆ A ⇒ subsystem (genS (A,af) X) (A,af)

hom_ID

⊢ system (A,af) ⇒ hom (λx. x)⟨A⟩ (A,af) (A,af)

hom_implies_restr

⊢ hom f (A,af) Bs ⇒ (f⟨A⟩ = f)

hom_shom

⊢ hom f (A,af) (B,bf) ⇒ shom f A B

homs_compose

⊢ hom f As Bs ∧ hom g Bs Cs ⇒ hom (g ∘ f)⟨FST As⟩ As Cs

iso_SYM

⊢ iso As Bs ⇔ iso Bs As

iso_inj_hom

⊢ iso (A,af) (B,bf) ∧ hom h (A,af) (C,cf) ∧ INJ h A C ⇒
  ∃j. hom j (B,bf) (C,cf) ∧ INJ j B C

lemma2_4_1

⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom g (A,af) (B,bf) ∧ SURJ g A B ∧
  (∀b. b ∉ B ⇒ (h b = ARB)) ⇒
  hom h (B,bf) (C,cf)

lemma2_4_2

⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom h (B,bf) (C,cf) ∧ (∀a. a ∈ A ⇒ g a ∈ B) ∧
  (∀a. a ∉ A ⇒ (g a = ARB)) ∧ INJ h B C ⇒
  hom g (A,af) (B,bf)

lemma5_3

⊢ hom f (A,af) (B,bf) ∧ hom g (A,af) (C,cf) ⇒ bisim (span A f g) (B,bf) (C,cf)

mapO'

⊢ ∀x. mapF f (mapF g x) = mapF (f ∘ g) x

map_preserves_INJ

⊢ INJ f A B ⇒ INJ (mapF f) (Fset A) (Fset B)

map_preserves_funs

⊢ (∀a. a ∈ A ⇒ f a ∈ B) ⇒ ∀af. af ∈ Fset A ⇒ mapF f af ∈ Fset B

prop5_1

⊢ system (A,af) ⇒ bisim (Δ A) (A,af) (A,af)

prop5_7

⊢ hom f (A,af) (B,bf) ⇒
  bisim (kernel A f) (A,af) (A,af) ∧ kernel A f equiv_on A

prop5_8

⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)

prop5_9_1

⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ⇒
  bisim (RIMAGE f A R) (B,bf) (B,bf)

prop5_9_2

⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim Q (B,bf) (B,bf) ⇒
  bisim (RINV_IMAGE f A Q) (A,af) (A,af)

prop6_1

⊢ V ⊆ A ∧ hom (λx. x)⟨V⟩ (V,kf) (A,af) ∧ hom (λx. x)⟨V⟩ (V,lf) (A,af) ⇒
  (kf = lf)

prop6_2

⊢ system (A,af) ⇒ (subsystem V (A,af) ⇔ V ⊆ A ∧ bisim (Δ V) (A,af) (A,af))

relEQ

⊢ relF $= = $=

relF_inv

⊢ relF Rᵀ x y ⇔ relF R y x

relO_EQ

⊢ relF R ∘ᵣ relF S = relF (R ∘ᵣ S)

rel_monotone

⊢ (∀a b. R a b ⇒ S a b) ⇒ ∀A B. relF R A B ⇒ relF S A B

sbisimulation_projns_homo

⊢ bisim R (A,af) (B,bf) ⇔
  ∃Rf. hom FST⟨Rᴾ⟩ (Rᴾ,Rf) (A,af) ∧ hom SND⟨Rᴾ⟩ (Rᴾ,Rf) (B,bf)

set_map'

⊢ ∀x x'. x' ∈ setF (mapF f x) ⇔ ∃x''. (x' = f x'') ∧ x'' ∈ setF x

simple_eq3

⊢ simple As ⇔ ∀R. bisim R As As ∧ R equiv_on FST As ⇒ (R = Δ (FST As))

simple_imp4

⊢ simple As ⇒ ∀Bs f g. hom f Bs As ∧ hom g Bs As ⇒ (f = g)

subsystem_ALT

⊢ subsystem V (A,af) ⇔ V ⊆ A ∧ system (A,af) ∧ hom (λx. x)⟨V⟩ (V,af⟨V⟩) (A,af)

subsystem_INTER

⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ∧ VS ≠ ∅ ⇒
  subsystem (BIGINTER VS) (A,af)

subsystem_INTER2

⊢ system (A,af) ∧ subsystem V1 (A,af) ∧ subsystem V2 (A,af) ⇒
  subsystem (V1 ∩ V2) (A,af)

subsystem_UNION

⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ⇒
  subsystem (BIGUNION VS) (A,af)

subsystem_refl

⊢ system (A,af) ⇒ subsystem A (A,af)

subsystem_system

⊢ subsystem V (A,af) ⇒ system (V,af⟨V⟩)

system_members

⊢ system (A,af) ⇒ ∀a b. a ∈ A ∧ b ∈ setF (af a) ⇒ b ∈ A

thm2_5

⊢ hom h (A,af) (B,bf) ⇔
  (∀a. a ∈ A ⇒ h a ∈ B) ∧ (∀a. a ∉ A ⇒ (h a = ARB)) ∧
  bisim (Gr h A) (A,af) (B,bf)

thm5_2

⊢ bisim Rᵀ Bs As ⇔ bisim R As Bs

thm5_4

⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒ bisim (Q ∘ᵣ R) (A,af) (C,cf)

thm5_5

⊢ (∀R. R ∈ Rs ⇒ bisim R As Bs) ∧ system As ∧ system Bs ⇒
  bisim (λa b. ∃R. R ∈ Rs ∧ R a b) As Bs

thm6_3_1

⊢ hom f (A,af) (B,bf) ∧ subsystem V (A,af) ⇒ subsystem (IMAGE f V) (B,bf)

thm6_3_2

⊢ hom f (A,af) (B,bf) ∧ subsystem W (B,bf) ⇒
  subsystem (PREIMAGE f W ∩ A) (A,af)

thm7_1

⊢ hom f (A,af) (B,bf) ⇒
  hom f (A,af) (IMAGE f A,bf⟨IMAGE f A⟩) ∧
  (∀g h C cf.
     hom g (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧
     hom h (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧ ((h ∘ f)⟨A⟩ = (g ∘ f)⟨A⟩) ⇒
     (h = g)) ∧ hom (eps (kernel A f) A) (A,af) (bquot (A,af) (kernel A f)) ∧
  hom (λx. x)⟨IMAGE f A⟩ (IMAGE f A,bf⟨IMAGE f A⟩) (B,bf) ∧
  iso (IMAGE f A,bf⟨IMAGE f A⟩) (bquot (A,af) (kernel A f)) ∧
  ∃mu.
    hom mu (bquot (A,af) (kernel A f)) (B,bf) ∧
    INJ mu (FST (bquot (A,af) (kernel A f))) B

thm7_2

⊢ hom f (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ∧ R ⊆ᵣ kernel A f ∧ R equiv_on A ⇒
  ∃!fbar. hom fbar (bquot (A,af) R) (B,bf) ∧ (f = (fbar ∘ eps R A)⟨A⟩)

thm7_3

⊢ system (A,af) ∧ subsystem B (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ∧
  Abbrev (TR = {a | a ∈ A ∧ ∃b. b ∈ B ∧ R a b}) ⇒
  subsystem TR (A,af) ∧
  (let
     Q = CURRY (Rᴾ ∩ (B × B))
   in
     bisim Q (B,af⟨B⟩) (B,af⟨B⟩) ∧ Q equiv_on B ∧
     iso (bquot (B,af⟨B⟩) Q) (bquot (TR,af⟨TR⟩) R))