structure cat = struct val thy = the_context () end ; val _ = use_legacy_bindings cat.thy ; val tri1' = rewrite_rule [tri1_def] tri1 ; val nt_eta' = rewrite_rule [nt_eta_def] nt_eta ; val _ = bind_thm ("hash_star", fold_rule [star_def] tri1') ; val _ = bind_thms ("hash_star_invs", [refl] RL ([hash_star] RL iffDs)) ; val _ = bind_thm ("G_eps_eta", [tri1', mks eps_def] MRS iffD2) ; val _ = bind_thm ("hash_G_eta", [tri1', refl] MRS iffD1) ; val _ = bind_thm ("G_hash_eta", [tri1', refl] MRS iffD2) ; val nt_eta' = rewrite_rule [nt_eta_def] nt_eta ; val nt_eta'' = fold_rule [M_def] nt_eta' ; (* M is a functor *) val _ = qed_goalw "fidM" cat.thy [M_def] "M id = id" (fn _ => [ simp_tac (esimps [fidF, fidG]) 1 ]) ; Addsimps [fidF, fidG, fidM] ; val _ = qed_goalw "fcompM" cat.thy [M_def] "M (g o f) = M g o M f" (fn _ => [ simp_tac (esimps [fcompF, fcompG]) 1 ]) ; val _ = qed_goal_spec_mp "mut_inv_lem" cat.thy "(ALL g f. (phi f = g) = (psi g = f)) = \ \ ((ALL f. psi (phi f) = f) & (ALL g. phi (psi g) = g))" (fn _ => [ Safe_tac, (etac allE2 1), (dtac iffD1 1), (rtac refl 1), atac 1, (etac allE2 1), (dtac iffD2 1), (rtac refl 1), Auto_tac]) ; val [mut_inv1, mut_inv2] = Seq.list_of (EVERY [Clarify_tac 1, (rtac conjunct2 1), (resolve_tac [adjf1, adjf2] 1)] (mut_inv_lem RS iffD1)) ; (* lemma using first adjunction triangle - note, it is used twice, for different objects, so must appear as a premise twice, with different types - can't use ALL f g. tri1 f g; need type annotations because if just two premises as tri1 _ _, they get given different free types *) val _ = qed_goalw_spec_mp "hash_eps_tri1" cat.thy [tri1_def] "nt_eta f --> tri1 f (?g :: 'c :: catC F => 'd :: catD) --> \ \ tri1 id (?h :: 'd G F => 'd) --> hash id o F f = hash f" (fn _ => [ Clarify_tac 1, (dtac iffD1 1), etac sym 2, (asm_full_simp_tac (esimps [nt_eta_def, fcompG, o_assoc RS sym]) 1), (dtac iffD2 1), (rtac refl 1), (asm_simp_tac (esimps [o_assoc]) 1)]) ; (* easier to prove using tri1 and nt_eta as theorems *) val hash_eps = tacthm (ALLGOALS (resolve_tac [nt_eta, tri1])) hash_eps_tri1 ; val hash_eps = prove_goal cat.thy "hash id o F f = hash f" (fn _ => [ (rtac (adjf1 RS conjunct2 RS iffD1 RS sym) 1), (simp_tac (esimps [fcompG, o_assoc RS sym, nt_eta']) 1), (simp_tac (esimps [o_assoc, G_hash_eta]) 1) ]) ; (* set show_types ; reset show_types ; *) val _ = qed_goalw "eta_def" cat.thy [star_def] "eta == star id" fn_at ; val _ = bind_thm ("hash_def", fold_rule [eps_def] (mk_eq (hash_eps RS sym))) ; val adjf3 = rewrite_rule [hash_def, star_def] hash_star ; val adjf3_fid = read_instantiate [("f", "id")] adjf3 ; val G_eps_eta = simplify (esimps [fcompG]) (refl RS (adjf3_fid RS iffD2)) ; val adjf3_gid = read_instantiate [("g", "id")] adjf3 ; val eps_F_eta = simplify (esimps [fcompF]) (refl RS (adjf3_gid RS iffD1)) ; val [hash_eta, star_eps] = [eta_def, eps_def] RL [def_imp_eq RS sym] RL ([hash_star] RL iffDs) ; val _ = qed_goalw "star_o" cat.thy [star_def] "star (g o f) = G g o star f" (fn _ => [ (simp_tac (esimps [fcompG, o_assoc]) 1) ]) ; val _ = qed_goal "star_o_eps" cat.thy "star (g o eps) = G g" (fn _ => [ (simp_tac (esimps [star_o, star_eps]) 1) ]) ; val _ = qed_goalw_spec_mp "tri12_hash" cat.thy [tri1_def, tri2_def, star_def, eps_def] "tri1 f g --> ?P --> tri2 f g" (fn _ => [ (Clarsimp_tac 1), (rtac iffI 1), (eatac trans 1 2), (eatac (sym RS trans) 1 1) ]) ; (* alternative proofs of tri2 *) val tri2 = [tri1, hash_eps] MRS tri12_hash ; val tri2' = rewrite_rule [hash_def] hash_star RS sym ; val _ = bind_thm ("star_eps_F'", [tri2', refl] MRS iffD1) ; val _ = bind_thm ("eps_F_star'", [tri2', refl] MRS iffD2) ; val _ = bind_thm ("eps_F_eta'", [tri2', mks eta_def] MRS iffD2) ; val _ = qed_goalw "nt_eps" cat.thy [nt_eps_def] "nt_eps phi" (fn _ => [ (simp_tac (esimps [adjf3 RS sym, fcompG, o_assoc RS sym, G_eps_eta]) 1) ]) ; val nt_eps' = rewrite_rule [nt_eps_def] nt_eps ; val nt_eps'' = fold_rule [M_def] nt_eps' ; (* proof of tri1 and nt_eta using adjf3 and hash_def *) val tri1' = fold_rule [hash_def] adjf3 ; val _ = qed_goalw "adjf3_nt_eta" cat.thy [nt_eta_def] "nt_eta phi" (fn _ => [ (simp_tac (esimps [adjf3, fcompF, o_assoc, eps_F_eta]) 1) ]) ; (* proof of monad axioms *) val _ = qed_goalw "KRunit" cat.thy [ext_def] "ext f o eta = f" (fn _ => [ (simp_tac (esimps [tri1']) 1) ]) ; val _ = qed_goalw "KLunit" cat.thy [ext_def] "ext eta = id" (fn _ => [ (simp_tac (esimps [hash_eta]) 1) ]) ; val _ = qed_goalw "hash_o" cat.thy [hash_def] "hash (g o f) = hash g o F f" (fn _ => [ (simp_tac (esimps [fcompF, o_assoc]) 1) ]) ; val _ = qed_goal "hash_eta_o" cat.thy "hash (eta o f) = F f" (fn _ => [ (simp_tac (esimps [hash_o, hash_eta]) 1) ]) ; val _ = qed_goal "hash_ass" cat.thy "hash (G (hash g) o f) = hash g o hash f" (fn _ => [ (rtac (tri1' RS iffD1) 1), (simp_tac (esimps [fcompG, mk_oap G_hash_eta]) 1) ]) ; (* hash is a functor from Kleisli category to D *) val _ = qed_goalw "hash_fun" cat.thy [ext_def, kcomp_def] "hash (kcomp g f) = hash g o hash f" (fn _ => [ (rtac hash_ass 1) ]) ; val _ = qed_goalw "ext_ass" cat.thy [ext_def] "ext (ext g o f) = ext g o ext f" (fn _ => [ (simp_tac (esimps [hash_ass, fcompG]) 1) ]) ; val _ = qed_goalw "ax5" cat.thy [mu_def] "mu o eta = id" (fn _ => [ (rtac G_eps_eta 1) ]) ; val _ = qed_goalw "ax6" cat.thy [mu_def, M_def] "mu o M eta = id" (fn _ => [ (simp_tac (esimps [fcompG RS sym, eps_F_eta]) 1) ]) ; val _ = qed_goalw "ext_jm" cat.thy [mu_def, M_def, ext_def, hash_def] "ext f = mu o M f" (fn _ => [ (rtac fcompG 1) ]) ; val _ = qed_goal "mu_ext" cat.thy "mu = ext id" (fn _ => [ (simp_tac (esimps [ext_jm]) 1) ]) ; val _ = qed_goalw "map_ext" cat.thy [M_def, ext_def] "M f = ext (eta o f)" (fn _ => [ (simp_tac (esimps [hash_eta_o]) 1) ]) ; val _ = qed_goal "ax4" cat.thy "mu o M (M f) = M f o mu" (fn _ => [ (simp_tac (esimps [ext_jm RS sym]) 1), (simp_tac (esimps [mu_ext, map_ext, ext_ass RS sym]) 1) ]) ; val _ = qed_goal "ax7" cat.thy "mu o M mu = mu o mu" (fn _ => [ (simp_tac (esimps [ext_jm RS sym]) 1), (simp_tac (esimps [mu_ext, ext_ass RS sym]) 1) ]) ; (* proof about M using map_ext as a definition *) val _ = qed_goalw "map_id" cat.thy [mk_eq map_ext] "M id = id" (fn _ => [ (simp_tac (esimps [KLunit]) 1) ]); val _ = qed_goalw "map_fun" cat.thy [mk_eq map_ext] "M (g o f) = M g o M f" (fn _ => [ (simp_tac (esimps [ext_ass RS sym, o_assoc, KRunit]) 1) ]); val _ = qed_goalw "ax3" cat.thy [mk_eq map_ext] "M f o eta = eta o f" (fn _ => [ (simp_tac (esimps [KRunit]) 1) ]); (* naturality of hash and star *) val _ = qed_goalw "star_nat" cat.thy [star_def] "star (b o g o F a) = G b o star g o a" (fn _ => [ (simp_tac (esimps [fcompG, o_assoc, mk_oap nt_eta']) 1) ]) ; val _ = qed_goal "hash_nat" cat.thy "hash (G b o f o a) = b o hash f o F a" (fn _ => [ (simp_tac (esimps ([hash_star RS sym, star_nat] @ hash_star_invs)) 1) ]) ; (** Kleisli category, identity is eta, composition is kcomp **) val _ = qed_goalw "kcomp_eta_id" cat.thy [kcomp_def] "kcomp eta f = f & kcomp f eta = f" (fn _ => [ (simp_tac (esimps [KLunit, KRunit]) 1) ]) ; val _ = qed_goalw "kcomp_ass" cat.thy [kcomp_def] "kcomp h (kcomp g f) = kcomp (kcomp h g) f" (fn _ => [ (simp_tac (esimps [ext_ass, o_assoc]) 1) ]) ; (* ext is a functor from Kleisli category to C, KLunit and ext_fun *) val _ = qed_goalw "ext_fun" cat.thy [kcomp_def] "ext (kcomp g f) = ext g o ext f" (fn _ => [ (simp_tac (esimps [ext_ass]) 1) ]) ; val _ = qed_goalw "kcomp_id" cat.thy [kcomp_def] "kcomp id (eta o f) = f" (fn _ => [ (simp_tac (esimps [KRunit, o_assoc]) 1) ]) ; (* eta o _ is a functor to Kleisli category *) val _ = qed_goalw "unit_o_fun" cat.thy [kcomp_def] "eta o (g o f) = kcomp (eta o g) (eta o f)" (fn _ => [ (simp_tac (esimps [o_assoc, KRunit]) 1) ]) ; (* these two functors are adjoints *) val _ = qed_goal "Kl_adj" cat.thy "(ext g o eta = f) = (kcomp id (eta o f) = g)" (fn _ => [ (simp_tac (esimps [KRunit, kcomp_id]) 1), Fast_tac 1 ]) ; (** M-algebras, Eilenberg-Moore category **) (* G eps is of more general type than mu *) val _ = qed_goalw "M_alg_G_eps" cat.thy [M_alg_def, M_def, mu_def] "M_alg (G eps)" (fn _ => [ (simp_tac (esimps [fcompG RS sym, nt_eps', G_eps_eta]) 1) ]) ; val _ = qed_goalw "M_alg_morph_G_eps" cat.thy [M_alg_morph_def, M_def] "M_alg_morph (G eps) (G eps) (G f)" (fn _ => [ (simp_tac (esimps [fcompG RS sym, nt_eps']) 1) ]) ; (* functor into Eilenberg-Moore category, gives objects and arrows *) val _ = qed_goalw "M_into_EM_obj" cat.thy [mu_def] "M_alg mu" (fn _ => [ (rtac M_alg_G_eps 1) ]) ; val _ = qed_goalw "M_into_EM_morph" cat.thy [mu_def, M_def] "M_alg_morph mu mu (M f)" (fn _ => [ (rtac M_alg_morph_G_eps 1) ]) ; val _ = qed_goalw_spec_mp "EM_adj_lem" cat.thy [M_alg_def, M_alg_morph_def] "M_alg b --> M_alg_morph mu b (b o M f)" (fn _ => [ (clarsimp_tac (cesimps [fcompM, o_assoc, mk_oap ax4]) 1) ]) ; (* the eps of the EM adjunction is a M-algebra morphism *) val _ = qed_goalw_spec_mp "EM_eps_morph" cat.thy [M_alg_def, M_alg_morph_def] "M_alg b --> M_alg_morph mu b b" (fn _ => [ Clarify_tac 1 ]) ; val _ = qed_goal_spec_mp "EM_adjf" cat.thy "M_alg b --> (M_alg_morph mu b g & g o eta = f) = (b o M f = g)" (fn _ => [ Safe_tac, (etac EM_adj_lem 2), (rewrite_goals_tac [M_alg_def, M_alg_morph_def]), (asm_simp_tac (esimps [fcompM, o_assoc, mk_oap (rewrite_rule [mk_eq ext_jm] KLunit)]) 1), (asm_simp_tac (esimps [mk_oap nt_eta'']) 1) ]) ; (* Kleisli splitting of monad is initial, the relevant functor is hash, relevant theorems are hash_eta_o, ext_def *) (* how to show the equalities hash_eta_o, ext_def deetermine hash f uniquely (given that hash is a functor)? *) (* Eilenberg-Moore splitting of monad is terminal, the relevant functor is G, functor on arrows is determined, but on objects, which M-algebra? *)