(* MonadMapC.ML *) fun umc _ = update_thy "MonadMapC" ; open Monad3C MonadJD MonadMapC ; structure Pext2 : PEXT2 = struct open Monad3C C ; val pextomap = FJR.pextomap ; val pext_ojoin = FJR.pext_ojoin ; open CompJ ; end ; (* structure Pext2 *) structure FP2 = fromPext2 (Pext2) ; structure PextMM : PEXTMM = struct val EC = C.EC ; (* monad morphism condition - enough to show J1 and J2 *) val mm2 = MonadMapC.mm2 ; open CompJ ; val thy = MonadMapC.thy ; end ; (* structure PextMM *) structure FPMM = fromPextMM (PextMM) ; structure Comp : CMONAD = struct val J1S = C.J1S ; val PE = C.PE ; val prod_pid = Monad3C.prod_pid ; open CompJ ; val thy = MonadMapC.thy ; end ; structure PA = PextAxioms (Comp) ; (* check that this gives all that is needed for our derivation using pext *) structure PAPext : MONAD3C = struct open Comp open PA val A5NM = NM.A5 ; val E4NM = NM.E4 ; end ; structure frPAP = from3C (PAPext) ; (** the lifted monad, seems to depend on J2 (DJK_alt) and J1 (dRunit, EC) **) val E2 = prove_goal MonadMapC.thy "extNL unitNL = id" (fn _ => [ (simp_tac (esimps [extNL_def, unitNL_def, M.ax3s RS sym]) 1), (simp_tac (esimps [symmetric UC, NM.E2]) 1) ]) ; val E3 = prove_goalw MonadMapC.thy [oNL_def, extNL_def] "extNL (g oNL f) = extNL g o extNL f" (fn _ => [ (simp_tac (esimps [o_assoc RS sym, NM.E3']) 1) ]) ; val E1_cond = prove_goal MonadMapC.thy "extNL (extM f) o unitNL = extM f" (fn _ => [(simp_tac (esimps [extNL_def, unitNL_def, M.E1, dRunit]) 1)]) ; val E4 = prove_goalw MonadMapC.thy [joinNL_def, extNL_def] "joinNL == extNL id" (fn _ => [ (simp_tac (esimps [DJK_alt]) 1) ]) ; val unitNL_comp = prove_goal MonadMapC.thy "unitNL o unitM = unitNM" (fn _ => [ (rtac ext 1), (simp_tac (esimps [unitNL_def, UC, M.ax3s]) 1) ]) ; val extNL_comp = prove_goal MonadMapC.thy "extNL o extM = extNM" (fn _ => [ (rtac ext 1), (simp_tac (esimps [unitNL_def, extNL_def, M.E1]) 1) ]) ; val mapNL_comp = prove_goal MonadMapC.thy "mapNL o mapM = mapNM" (fn _ => [ (rtac ext 1), (simp_tac (esimps [mapNL_def, NM.E5, unitNL_def, extNL_def]) 1), (simp_tac (esimps [M.ax2s, M.ax3s RS sym, UC, o_assoc]) 1) ]) ; val ax8 = prove_goalw MonadMapC.thy [E4, mapNL_def] "extNL f == joinNL o mapNL f" (fn _ => [ (simp_tac (esimps [E3 RS sym, oNL_def, o_assoc]) 1), (simp_tac (esimps [M.E2 RS sym, E1_cond]) 1), (simp_tac (esimps [M.E2]) 1) ]) ; (* regarding 'a N M as 'a M NL, derive the pext rules and J1/2 *) val E2K = prove_goalw MonadMapC.thy [UC, unitNL_def] "extM unitNM = unitNL" (fn _ => [ (simp_tac (esimps [M.extomap RS sym, M.E2]) 1) ]) ; (* E1K' is exactly E1 *) val pext_o_fun = prove_goalw MonadMapC.thy [oNL_def, NM.E6] "extM (g oNM f) = extM g oNL extM f" (fn _ => [(simp_tac (esimps [mk_ap extNL_comp, EC, M.E3']) 1)]) ; val J1e = prove_goalw MonadMapC.thy [E4, extNL_def, NM.E4] "extNL joinNM = joinNM o joinNL" (fn _ => [ (rtac trans 1), (rtac NM.E3' 2), Simp_tac 1 ]) ; val J2e = prove_goalw MonadMapC.thy [E4, extNL_def] "extNM joinNL = joinNL o joinNM" (fn _ => [ (rtac NM.ext_ext 1) ]) ;