The Theory pcf-defs

Parents

gst

Constants

func	GS → BOOL
mk_func	GS → GS → GS
graph	GS → GS
cods	GS → GS
doms	GS → GS
idff	GS → GS
idcod	GS → GS
iddom	GS → GS
fields	GS → GS
appg	GS → GS → GS
$og_f	GS → GS → GS
ccat	GS → BOOL
ccat_const	GS → GS
cfunc	GS → BOOL
cfunc_const	GS → GS
ccat_cfunc	GS → BOOL
cfunc_ccat	GS → BOOL
pf_hered	(GS → BOOL) → BOOL
pc_hered	(GS → BOOL) → BOOL
pure_functor	GS → BOOL
pure_category	GS → BOOL
mk_pf	GS → PF
pf_rep	PF → GS
mk_pc	GS → PC
pc_rep	PC → GS
$o_f	PF → PF → PF
id_f	PC → PF
dom_c	PF → PC
cod_c	PF → PC
$∈_f	PF → PC → BOOL
$_f	PF → PF → PF
Sep_c	PC → (PF → BOOL) → PF
Λ_f	PC → (PF → PF) → PF
G_c	PC → PC

Types

Fixity

Right Infix 240:

og_f

Right Infix 310:

o_f

∈_f

Definitions

func	⊢ ∀ s • func s ⇔ (∃ c g• s = c ↦_g g ∧ fun g ∧ ran g ⊆_g c)
mk_func	⊢ ∀ c g• mk_func c g = c ↦_g g
doms cods graph	⊢ ∀ f • doms f = dom (snd f) ∧ cods f = fst f ∧ graph f = snd f
idff	⊢ ∀ f• idff f = mk_func f (id f)
iddom idcod	⊢ ∀ f • iddom f = idff (doms f) ∧ idcod f = idff (cods f)
fields	⊢ ∀ f• fields f = doms f ∪_g cods f
appg	⊢ ∀ f g• appg f g = graph f _g g
og_f	⊢ ∀ f g • f og_f g = mk_func (cods f) (graph f o_g graph g)
ccat	⊢ ∀ s • ccat s ⇔ (∀ t • t ∈_g s ⇒ func t ∧ iddom t ∈_g s ∧ idcod t ∈_g s ∧ (∀ u • u ∈_g s ∧ doms t = cods u ⇒ t og_f u ∈_g s))
ccat_const	⊢ ∀ c• ccat_const c = Imagep doms c ∪_g Imagep cods c
cfunc	⊢ ∀ f • cfunc f ⇔ func f ∧ (∀ g• g ∈_g fields f ⇒ func g) ∧ (∀ g h • g ∈_g doms f ∧ h ∈_g doms f ∧ doms g = cods h ∧ g og_f h ∈_g doms f ⇒ doms (appg f g) = cods (appg f h) ∧ appg f (g og_f h) = appg f g og_f appg f h)
cfunc_const	⊢ ∀ f• cfunc_const f = doms f ∪_g cods f
ccat_cfunc	⊢ ∀ f • ccat_cfunc f ⇔ cfunc f ∧ ccat (doms f) ∧ ccat (cods f)
cfunc_ccat	⊢ ∀ c• cfunc_ccat c ⇔ ccat c ∧ (∀ f• f ∈_g c ⇒ cfunc f)
pf_hered	⊢ ∀ p • pf_hered p ⇔ (∀ f • ccat_cfunc f ∧ (∀ g• g ∈_g cfunc_const f ⇒ p g) ⇒ p f)
pc_hered	⊢ ∀ p • pc_hered p ⇔ (∀ c • cfunc_ccat c ∧ (∀ d• d ∈_g ccat_const c ⇒ p d) ⇒ p c)
pure_functor	⊢ ∀ s• pure_functor s ⇔ (∀ p• pf_hered p ⇒ p s)
PF	⊢ ∃ f• TypeDefn pure_functor f
pure_category	⊢ ∀ c• pure_category c ⇔ (∀ p• pc_hered p ⇒ p c)
PC	⊢ ∃ f• TypeDefn pure_category f
pf_rep mk_pf	⊢ OneOne pf_rep ∧ (∀ x• mk_pf (pf_rep x) = x) ∧ (∀ x• pure_functor x ⇔ (∃ y• x = pf_rep y))
pc_rep mk_pc	⊢ OneOne pc_rep ∧ (∀ x• mk_pc (pc_rep x) = x) ∧ (∀ x• pure_category x ⇔ (∃ y• x = pc_rep y))
o_f	⊢ ∀ f g• f o_f g = mk_pf (pf_rep f og_f pf_rep g)
id_f	⊢ ∀ c• id_f c = mk_pf (idff (pc_rep c))
dom_c	⊢ ∀ f• dom_c f = mk_pc (doms (pf_rep f))
cod_c	⊢ ∀ f• cod_c f = mk_pc (cods (pf_rep f))
∈_f	⊢ ∀ f c• f ∈_f c ⇔ pf_rep f ∈_g pc_rep c
_f	⊢ ∀ f g• f _f g = mk_pf (appg (pf_rep f) (pf_rep g))
Sep_c	⊢ ∀ c p • Sep_c c p = mk_pf (Sep (pc_rep c) (λ s• ∃ f• s = pf_rep f ∧ p f))
Λ_f	⊢ ∀ pc pfpf • Λ_f pc pfpf = mk_pf (mk_func (Imagep (pf_rep o pfpf o mk_pf) (pc_rep pc)) (Imagep (λ f• f ↦_g pf_rep (pfpf (mk_pf f))) (pc_rep pc)))
G_c	⊢ ∀ pc • G_c pc = mk_pc (Sep (Gx (pc_rep pc)) pure_functor)

Theorems

func_thm	⊢ ∀ f • func f ⇒ fun (graph f) ∧ ran (graph f) ⊆_g cods f
appg_thm1	⊢ ∀ f x • func f ⇒ (∃ y• x ↦_g y ∈_g graph f) ⇒ x ↦_g appg f x ∈_g graph f
appg_thm2	⊢ ∀ f x • func f ∧ x ∈_g doms f ⇒ x ↦_g appg f x ∈_g graph f
appg_thm3	⊢ ∀ f x y• func f ∧ x ↦_g y ∈_g graph f ⇒ appg f x = y
appg_thm4	⊢ ∀ f x• func f ∧ x ∈_g doms f ⇒ appg f x ∈_g cods f
og_f_associative_thm	⊢ ∀ f g h• (f og_f g) og_f h = f og_f g og_f h
pf_⇔_lem1	⊢ ∀ f • pure_functor f ⇔ ccat_cfunc f ∧ (∀ g• g ∈_g cfunc_const f ⇒ pure_functor g)
pc_⇔_lem1	⊢ ∀ c • pure_category c ⇔ cfunc_ccat c ∧ (∀ d• d ∈_g ccat_const c ⇒ pure_category d)
pf_⇔_lem2	⊢ ∀ f • pure_functor f ⇔ cfunc f ∧ pure_category (doms f) ∧ pure_category (cods f)
pc_⇔_lem2	⊢ ∀ c • pure_category c ⇔ ccat c ∧ (∀ g• g ∈_g c ⇒ pure_functor g)
pf_pf_rep_thm	⊢ ∀ f• pure_functor (pf_rep f)
pc_pc_rep_thm	⊢ ∀ c• pure_category (pc_rep c)
pf_inv_thm	⊢ ∀ x• pure_functor x ⇒ pf_rep (mk_pf x) = x
pc_inv_thm	⊢ ∀ x• pure_category x ⇒ pc_rep (mk_pc x) = x
idff_closure_lem	⊢ ∀ c• pure_category c ⇒ pure_functor (idff c)
func_comp_thm	⊢ ∀ x y• func x ∧ func y ⇒ func (x og_f y)
doms_cods_og_f_thm	⊢ ∀ f g • doms (f og_f g) ⊆_g doms g ∧ cods (f og_f g) ⊆_g cods f
fields_⊆_g_thm	⊢ ∀ f g• fields (f og_f g) ⊆_g fields f ∪_g fields g
appg_og_f_thm	⊢ ∀ x y g • func x ∧ func y ∧ doms x = cods y ∧ g ∈_g doms y ⇒ appg (x og_f y) g = appg x (appg y g)

Created: