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
$ogf
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
$of
PF → PF → PF
idf
PC → PF
domc
PF → PC
codc
PF → PC
$∈f
PF → PC → BOOL
$f
PF → PF → PF
Sepc
PC → (PF → BOOL) → PF
Λf
PC → (PF → PF) → PF
Gc
PC → PC
Types
PF
PC
Fixity
Right Infix 240:
ogf
Right Infix 310:
of f f
Definitions
func
⊢ ∀ s
fill• 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
fill• doms f = dom (snd f)
fill∧ cods f = fst f
fill∧ graph f = snd f
idff
⊢ ∀ f• idff f = mk_func f (id f)
iddom
idcod
⊢ ∀ f
fill• 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
ogf
⊢ ∀ f g
fill• f ogf g = mk_func (cods f) (graph f og graph g)
ccat
⊢ ∀ s
fill• ccat s
fill⇔ (∀ t
fill• t ∈g s
fill⇒ func t
fill∧ iddom t ∈g s
fill∧ idcod t ∈g s
fill∧ (∀ u
fill• u ∈g s ∧ doms t = cods u
fill⇒ t ogf u ∈g s))
ccat_const
⊢ ∀ c• ccat_const c = Imagep doms c ∪g Imagep cods c
cfunc
⊢ ∀ f
fill• cfunc f
fill⇔ func f
fill∧ (∀ g• g ∈g fields f ⇒ func g)
fill∧ (∀ g h
fill• g ∈g doms f
fill∧ h ∈g doms f
fill∧ doms g = cods h
fill∧ g ogf h ∈g doms f
fill⇒ doms (appg f g) = cods (appg f h)
fill∧ appg f (g ogf h)
fill= appg f g ogf appg f h)
cfunc_const
⊢ ∀ f• cfunc_const f = doms f ∪g cods f
ccat_cfunc
⊢ ∀ f
fill• ccat_cfunc f
fill⇔ 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
fill• pf_hered p
fill⇔ (∀ f
fill• ccat_cfunc f ∧ (∀ g• g ∈g cfunc_const f ⇒ p g)
fill⇒ p f)
pc_hered
⊢ ∀ p
fill• pc_hered p
fill⇔ (∀ c
fill• cfunc_ccat c ∧ (∀ d• d ∈g ccat_const c ⇒ p d)
fill⇒ 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
fill∧ (∀ x• mk_pf (pf_rep x) = x)
fill∧ (∀ x• pure_functor x ⇔ (∃ y• x = pf_rep y))
pc_rep
mk_pc
⊢ OneOne pc_rep
fill∧ (∀ x• mk_pc (pc_rep x) = x)
fill∧ (∀ x• pure_category x ⇔ (∃ y• x = pc_rep y))
of
⊢ ∀ f g• f of g = mk_pf (pf_rep f ogf pf_rep g)
idf
⊢ ∀ c• idf c = mk_pf (idff (pc_rep c))
domc
⊢ ∀ f• domc f = mk_pc (doms (pf_rep f))
codc
⊢ ∀ f• codc 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))
Sepc
⊢ ∀ c p
fill• Sepc c p
fill= mk_pf
fill(Sep (pc_rep c) (λ s• ∃ f• s = pf_rep f ∧ p f))
Λf
⊢ ∀ pc pfpf
fill• Λf pc pfpf
fill= mk_pf
fill(mk_func
fill(Imagep
fill(pf_rep o pfpf o mk_pf)
fill(pc_rep pc))
fill(Imagep
fill(λ f• f ↦g pf_rep (pfpf (mk_pf f)))
fill(pc_rep pc)))
Gc
⊢ ∀ pc
fill• Gc pc = mk_pc (Sep (Gx (pc_rep pc)) pure_functor)
Theorems
func_thm
⊢ ∀ f
fill• func f ⇒ fun (graph f) ∧ ran (graph f) ⊆g cods f
appg_thm1
⊢ ∀ f x
fill• func f
fill⇒ (∃ y• x ↦g y ∈g graph f)
fill⇒ x ↦g appg f x ∈g graph f
appg_thm2
⊢ ∀ f x
fill• 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
ogf_associative_thm
⊢ ∀ f g h• (f ogf g) ogf h = f ogf g ogf h
pf_⇔_lem1
⊢ ∀ f
fill• pure_functor f
fill⇔ ccat_cfunc f
fill∧ (∀ g• g ∈g cfunc_const f ⇒ pure_functor g)
pc_⇔_lem1
⊢ ∀ c
fill• pure_category c
fill⇔ cfunc_ccat c
fill∧ (∀ d• d ∈g ccat_const c ⇒ pure_category d)
pf_⇔_lem2
⊢ ∀ f
fill• pure_functor f
fill⇔ cfunc f
fill∧ pure_category (doms f)
fill∧ pure_category (cods f)
pc_⇔_lem2
⊢ ∀ c
fill• pure_category c
fill⇔ 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 ogf y)
doms_cods_ogf_thm
⊢ ∀ f g
fill• doms (f ogf g) ⊆g doms g
fill∧ cods (f ogf g) ⊆g cods f
fields_⊆g_thm
⊢ ∀ f g• fields (f ogf g) ⊆g fields f ∪g fields g
appg_ogf_thm
⊢ ∀ x y g
fill• func x ∧ func y ∧ doms x = cods y ∧ g ∈g doms y
fill⇒ appg (x ogf y) g = appg x (appg y g)

up quick index

privacy policy

Created:

V