(* MonadW - compound writer monad *) open MonadM MonadW ; val () = qed_goal "p1_Nil" MonadW.thy "p1 [] = id" (fn _ => [rtac ext 1, (split_all_tac 1), Simp_tac 1]) ; val () = qed_goal "p1_App" MonadW.thy "p1 (r @ s) = p1 r o p1 s" (fn _ => [rtac ext 1, (split_all_tac 1), (simp_tac (HOL_ss addsimps [o_apply, p1_def]) 1), (simp_tac (HOL_ss addsimps [append_assoc]) 1) ]) ; val pextWM_unitWM as E2K = prove_goal MonadW.thy "pextWM unitWM = unitM" (fn _ => [rtac ext 1, (split_all_tac 1), (simp_tac (esimps [unitWM_def, mk_ap ax3s RS sym]) 1) ]) ; val lem1 = prove_goal MonadW.thy "mapM (p1 r) o pextWM g = pextWM g o p1 r" (fn _ => [rtac ext 1, (split_all_tac 1), (simp_tac (esimps [mk_ap ax2s, p1_App]) 1)]) ; val lem2 = prove_goal MonadW.thy "mapM (p1 r) o extM (pextWM g) = extM (pextWM g) o mapM (p1 r)" (fn _ => [ (simp_tac (esimps [mapoext, extomap]) 1), (cong_tac 1), rtac lem1 1 ]) ; val pextWM_Nil = prove_goal MonadW.thy "pextWM f (a, []) = f a" (fn _ => [(simp_tac (esimps [p1_Nil, ax1]) 1)]) ; val E1K' = prove_goal MonadW.thy "pextWM f o unitW = f" (fn _ => [(rtac ext 1), (simp_tac (esimps [unitW_def, p1_Nil, ax1]) 1)]) ; val pext_oWM_fun = prove_goal MonadW.thy "pextWM (g oWM f) = pextWM g oM pextWM f" (fn _ => [rtac ext 1, (split_all_tac 1), (simp_tac (esimps [oWM_def]) 1), (rewtac (mk_eq E6)), (simp_tac (HOL_ss addsimps [o_apply, pextWM_Nil]) 1), (Simp_tac 1), (rtac (mk_ap lem2) 1)]) ; structure WM : MONAD3C = struct structure M = MonadM ; val thy = MonadW.thy ; val A5NM = MonadW.extWM_def ; val E4NM = MonadW.joinWM_def ; val prod_pid = MonadW.prod_pid ; val E1K' = E1K' ; val E2K = E2K ; val E3K = pext_oWM_fun ; fun tr #"N" = #"W" | tr ch = ch ; fun sub str = CharVector.map tr str ; end ; structure FWM = from3C (WM) ; structure WM3 : MONAD3 = struct val E2 = FWM.E2NM ; val E1 = FWM.E1NM ; val E3 = FWM.E3NM ; val E4 = MonadW.joinWM_def ; val E5 = MonadW.mapWM_def ; fun tr #"M" = "WM" | tr ch = BasisLibrary.String.str ch ; fun sub str = BasisLibrary.String.translate tr str ; val thy = MonadW.thy ; end ; structure FWM3 = from3 (WM3) ; (* prove three monad axioms for W *) val E2W = prove_goal MonadW.thy "extW unitW = id" (fn _ => [ (rtac ext 1), (split_all_tac 1), (simp_tac (esimps [unitW_def]) 1)]) ; val E1W = prove_goal MonadW.thy "extW f o unitW = f" (fn _ => [ (rtac ext 1), (simp_tac (esimps [unitW_def, p1_Nil]) 1)]) ; val ext_oW_fun = prove_goal MonadW.thy "extW (g oW f) = extW g o extW f" (fn _ => [ (rtac ext 1), (split_all_tac 1), (case_tac "f a" 1), (asm_simp_tac (esimps [oW_ext, p1_App]) 1)]) ; structure W3 : MONAD3 = struct val E2 = E2W ; val E1 = E1W ; val E3 = ext_oW_fun ; val E4 = joinW_def ; val E5 = mapW_def ; fun tr #"M" = #"W" | tr ch = ch ; fun sub str = CharVector.map tr str ; val thy = MonadW.thy ; end ; structure W = from3 (W3) ; (* mapWM = mapM o mapW *) val mapWM_comp = prove_goal MonadW.thy "mapWM = mapM o mapW" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [mapWM_def, MonadM.E5, FWM.EC, FWM.UC]) 1), (cong_tac 1), (rtac ext 1), (split_all_tac 1), (simp_tac (esimps [mapW_def]) 1), (rtac (mk_ap MonadM.ax3s RS sym) 1)]) ; (* simple proof of pext_po *) val pext_po = prove_goal MonadW.thy "pextWM (pextWM f o g) = pextWM f o extW g" (fn _ => [ (rtac ext 1), (split_all_tac 1), Simp_tac 1, rtac (mk_ap lem1) 1]) ; structure PextW : PEXT = struct structure N = W ; structure M = MonadM ; structure NM = FWM3 ; open WM FWM ; val pext_po = pext_po ; val E5 = mapWM_def ; val E4 = joinWM_def ; val MC = mapWM_comp ; val prod_pid = MonadW.prod_pid ; fun tr #"N" = #"W" | tr ch = ch ; fun sub str = CharVector.map tr str ; val thy = MonadW.thy ; end ; structure FPW = fromPext (PextW) ; val J2W = prove_goal MonadW.thy "joinWM o mapWM (mapM joinW) = (mapM joinW) o joinWM" (fn _ => [ (simp_tac (esimps [FWM3.ax8' RS sym, FWM3.ext_ojoin_iff]) 1), (simp_tac (esimps [FWM.EC, MonadM.E5]) 1), (cong_tac 1), (rtac ext 1), (split_all_tac 1), (simp_tac (esimps [FWM.UC, W.E4]) 1), (simp_tac (esimps [mk_ap MonadM.E1, unitW_def]) 1), (simp_tac (esimps [mk_ap MonadM.ax3s RS sym]) 1)]) ; structure Pext2W : PEXT2 = struct open PextW FPW ; val J2 = J2W ; structure N = W ; structure M = MonadM ; structure NM = FWM3 ; end ; structure FP2W = fromPext2 (Pext2W) ;