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 • 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 ogf ⊢ ∀ f g • f ogf g = mk_func (cods f) (graph f og 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 ogf 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 ogf h ∈g doms f ⇒ doms (appg f g) = cods (appg f h) ∧ appg f (g ogf h) = appg f g ogf 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)) 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 • Sepc 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))) Gc ⊢ ∀ pc • Gc 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 ogf_associative_thm ⊢ ∀ f g h• (f ogf g) ogf h = f ogf g ogf 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 ogf y) doms_cods_ogf_thm ⊢ ∀ f g • doms (f ogf g) ⊆g doms g ∧ 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 • func x ∧ func y ∧ doms x = cods y ∧ g ∈g doms y ⇒ appg (x ogf y) g = appg x (appg y g)