(* MonadE - compound error monad note similarity of proofs to those in MonadW *) open MonadE ; open MonadM ; val E1_ap = rewrite_rule [o_def] (E1 RS fun_cong) ; val pextEM_unitEM as E2K = prove_goal MonadE.thy "pextEM unitEM = unitM" (fn _ => [rtac ext 1, (case_tac "x" 1), (ALLGOALS (asm_simp_tac (esimps [unitEM_def]) )) ]) ; val E1K' = prove_goal MonadE.thy "pextEM f o unitE = f" (fn _ => [(rtac ext 1), (simp_tac (esimps [unitE_def]) 1)]) ; val pext_oEM_fun = prove_goal MonadE.thy "pextEM (g oEM f) = pextEM g oM pextEM f" (fn _ => [rtac ext 1, (case_tac "x" 1), (asm_simp_tac (esimps [oEM_def]) 1), (rewtac (mk_eq E6)), (Asm_simp_tac 1), (simp_tac (esimps [E1_ap]) 1) ]) ; structure EM : MONAD3C = struct structure M = MonadM ; val thy = MonadE.thy ; val A5NM = MonadE.extEM_def ; val E4NM = MonadE.joinEM_def ; val prod_pid = MonadE.prod_pid ; val E1K' = E1K' ; val E2K = E2K ; val E3K = pext_oEM_fun ; fun tr #"N" = "E" | tr ch = BasisLibrary.String.str ch ; fun sub str = BasisLibrary.String.translate tr str ; end ; structure FEM = from3C (EM) ; structure EM3 : MONAD3 = struct val E2 = FEM.E2NM ; val E1 = FEM.E1NM ; val E3 = FEM.E3NM ; val E4 = MonadE.joinEM_def ; val E5 = MonadE.mapEM_def ; fun tr #"M" = "EM" | tr ch = BasisLibrary.String.str ch ; fun sub str = BasisLibrary.String.translate tr str ; val thy = MonadE.thy ; end ; structure FEM3 = from3 (EM3) ; (* prove three monad axioms for E *) val E2E = prove_goal MonadE.thy "extE unitE = id" (fn _ => [ (rtac ext 1), (case_tac "x" 1), (ALLGOALS (asm_simp_tac (esimps [unitE_def]) ))]) ; val E1E = prove_goal MonadE.thy "extE f o unitE = f" (fn _ => [ (rtac ext 1), (simp_tac (esimps [unitE_def]) 1)]) ; val ext_oE_fun = prove_goal MonadE.thy "extE (g oE f) = extE g o extE f" (fn _ => [ (rtac ext 1), (case_tac "x" 1), (ALLGOALS (asm_simp_tac (esimps [oE_ext]) ))]) ; structure E3 : MONAD3 = struct val E2 = E2E ; val E1 = E1E ; val E3 = ext_oE_fun ; val E4 = joinE_def ; val E5 = mapE_def ; fun tr #"M" = #"E" | tr ch = ch ; fun sub str = CharVector.map tr str ; val thy = MonadE.thy ; end ; structure E = from3 (E3) ; (* mapEM = mapM o mapE *) val mapEM_comp = prove_goal MonadE.thy "mapEM = mapM o mapE" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [mapEM_def, MonadM.E5, FEM.EC, FEM.UC]) 1), (cong_tac 1), (rtac ext 1), (case_tac "xb" 1), (ALLGOALS (asm_simp_tac (esimps [mapE_def]) ))]) ; (* simple proof of pext_po *) val pext_po = prove_goal MonadE.thy "pextEM (pextEM f o g) = pextEM f o extE g" (fn _ => [ (rtac ext 1), (case_tac "x" 1), (ALLGOALS Asm_simp_tac)]) ; structure PextE : PEXT = struct structure N = E ; structure M = MonadM ; structure NM = FEM3 ; open EM FEM ; val pext_po = pext_po ; val E5 = mapEM_def ; val E4 = joinEM_def ; val MC = mapEM_comp ; val prod_pid = MonadE.prod_pid ; fun tr #"N" = #"E" | tr ch = ch ; fun sub str = CharVector.map tr str ; val thy = MonadE.thy ; end ; structure FPE = fromPext (PextE) ; val J2E = prove_goal MonadE.thy "joinEM o mapEM (mapM joinE) = (mapM joinE) o joinEM" (fn _ => [ (simp_tac (esimps [FEM3.ax8' RS sym, FEM3.ext_ojoin_iff]) 1), (simp_tac (esimps [FEM.EC, MonadM.E5]) 1), (cong_tac 1), (rtac ext 1), (case_tac "x" 1), (ALLGOALS (asm_simp_tac (esimps [FEM.UC, E.E4]) )), (simp_tac (esimps [mk_ap MonadM.E1, unitE_def]) 1)]) ; structure Pext2E : PEXT2 = struct open PextE FPE ; val J2 = J2E ; structure N = E ; structure M = MonadM ; structure NM = FEM3 ; end ; structure FP2E = fromPext2 (Pext2E) ;