(* Monad3.ML - monads based on 3 axioms re unit and ext *) open Monad3 ; structure ME : MONAD3 = struct open Monad3 ; structure Cs = Cso ; fun sub str = str ; end ; structure M = from3 (ME) ; (* tests of functors without join and map *) structure MA1245 : MONADA1245 = fromE126 (M) ; structure ME126 : MONADE126 = fromA1245 (MA1245) ; structure ME123 : MONADE123 = fromA (M) ; structure MA : MONADA = fromE123 (ME) ; structure MonadM = M ; structure M7 : MONAD7 = struct open MonadM ; structure Cs = Cso ; fun sub str = str ; val thy = Monad3.thy ; end ; structure F7G = from7G (M7) ; structure F7 : MONAD3 = F7G ; (* alternatively, starting from ext_inj, E3' and E2, can prove E1, thence _define_ oM by E6, so have E3, thence Monad3 and MonadM *) val E1_alt = prove_goal Monad3.thy "extM f o unitM = f" (fn _ => [rtac MonadM.ext_inj 1, rtac (MonadM.E3' RS trans) 1, (simp_tac (esimps [E2]) 1)]) ; (* try to prove unit_cong thus Goal : unit a = unit b --> a = b Proof : unit a = unit b --> ext id (unit a) = ext id (unit b) ie a = b Goal "unitM a = unitM b ==> a = b" ; by (dres_inst_tac [("f", "extM id")] arg_cong 1) ; *) (** algebras, the Eilenberg-Moore category of a functor **) (* note - ([M.ax5, M.ax7] MRS conjI) is more type-general *) val join_alg = prove_goalw Monad3.thy [isalg_def] "isalg joinM" (fn _ => [ (rtac ([M.ax5, M.ax7] MRS conjI) 1) ]) ; (* mapM f is an algebra morphism between two join algebras, isalgmorph joinM joinM (mapM f)" *) val jm_am = fold_rule [isalgmorph_def] M.ax4 ; val id_am = prove_goalw Monad3.thy [isalgmorph_def] "isalgmorph (a, id, a)" (fn _ => [ (simp_tac (esimps [M.ax1]) 1) ]) ; val comp_am = prove_goalw Monad3.thy [isalgmorph_def] "isalgmorph (a, f, b) --> isalgmorph (b, g, c) --> isalgmorph (a, g o f, c)" (fn _ => [ (clarsimp_tac (cesimps [M.ax2, o_assoc]) 1), (clarsimp_tac (cesimps [o_assoc RS sym]) 1) ]) RS mp RS mp ; (* "isalg a --> isalgmorph joinM a a" *) val counit_am = isalg_def RS defD1 RS conjunct2 RS (isalgmorph_def RS iffD2) ; (* unit triangle for adjoint functors, a unique solution for hf = hash f which is an algebra morphism and makes the triangle commute *) val adjf1_em = prove_goalw Monad3.thy [isalg_def] "isalg a --> (isalgmorph (joinM, hf, a) & hf o unitM = f) = \ \ (a o mapM f = hf)" (fn _ => [ Safe_tac, (asm_full_simp_tac (esimps [M.ax2, o_assoc, mk_oap M.ax6]) 1), (asm_simp_tac (esimps [M.ax2, o_assoc, mk_oap M.ax4]) 1), (asm_simp_tac (esimps [mk_oap M.ax3]) 1) ]) RS mp ; (* note - the counit a is an algebra morphism (above), and for f : (A, a) -> (B, b) in the E-M category, the commuting square for the counit eps to be a nt is exactly that f is an algebra morphism *) (* counit triangle for adjoint functors, given g an algebra morphism, a unique solution for sg = star g which makes the triangle commute *) val adjf2_em = prove_goalw Monad3.thy [isalg_def] "isalg a --> isalgmorph (joinM, g, a) --> \ \ (a o mapM sg = g) = (g o unitM = sg)" (fn _ => [ Safe_tac, (clarsimp_tac (cesimps [mk_oap M.ax3]) 1), (clarsimp_tac (cesimps [M.ax2, o_assoc, mk_oap M.ax6]) 1) ]) RS mp RS mp ;