(* MonadSR.ML *) val () = qed_goal "phi_mm" MonadSR.thy "mmSR o f = phi f" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [phi_def, mmSR_def]) 1)]) ; val ax1' = simplify (simpset ()) (mk_ap ax1) ; val () = qed_goal "psi_phi" MonadSR.thy "psi (phi f) = f" (fn _ => [ (REPEAT (rtac ext 1)), (rewrite_goals_tac [psi_def, phi_def]), (simp_tac (esimps [mk_ap ax2s]) 1), rtac trans 1, rtac ax1' 2, cong_tac 1, rtac ext 1, Simp_tac 1]) ; val () = qed_goal "phi_psi_unit" MonadSR.thy "phi (psi unitSM) = unitSM" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [psi_def, phi_def, unitSM_def]) 1), (simp_tac (esimps [mk_ap ax3s RS sym]) 1)]) ; val () = qed_goal "ppp" MonadSR.thy "phi (psi (phi g oSM phi f)) = (phi g oSM phi f)" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [psi_def, phi_def, oSM_def]) 1), (simp_tac (esimps [E6, phi_def]) 1), (simp_tac (esimps [mk_ap extomap, mk_ap mapoext]) 1), cong_tac 1, rtac ext 1, (simp_tac (esimps [phi_def, mk_ap ax2s]) 1), cong_tac 1, rtac ext 1, Simp_tac 1]) ; (* note "phi (psi f) = f" does not hold *) structure SRMA : MONADA = struct val A2 = prove_goalw MonadSR.thy [unitSR_def, oSR_def] "unitSR oSR f = f" (fn _ => [ (simp_tac (esimps [phi_psi_unit, psi_phi, SMLid]) 1)]) ; val A1 = prove_goalw MonadSR.thy [unitSR_def, oSR_def] "f oSR unitSR = f" (fn _ => [ (simp_tac (esimps [phi_psi_unit, psi_phi, SMRid]) 1)]) ; val A3 = prove_goalw MonadSR.thy [oSR_def] "h oSR (g oSR f) = h oSR g oSR f" (fn _ => [ (simp_tac (esimps [ppp, oSMassoc]) 1)]) ; val A4 = prove_goalw MonadSR.thy [oSR_def] "h oSR f = h oSR id o f" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [psi_def, phi_def, oSM_def]) 1), (simp_tac (esimps [E6, phi_def]) 1)]) ; val (A5, E4, E5) = (extSR_def, joinSR_def, mapSR_def) ; fun tr #"M" = "SR" | tr ch = BasisLibrary.String.str ch ; fun sub str = BasisLibrary.String.translate tr str ; val thy = MonadSR.thy ; end ; structure SRM3 = fromA (SRMA) ; structure SRM = from3 (SRM3) ; (* now show definitions same as MR monad *) val sameunit = prove_goalw MonadSR.thy [unitSR_def] "unitSR = unitMR" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [psi_def, unitSM_def, mk_ap ax3s RS sym]) 1)]) ; val sameo = prove_goal MonadSR.thy "op oSR = op oMR" (fn _ => [ (REPEAT (rtac ext 1)), (simp_tac (esimps [oSR_def, oSM_def]) 1), (simp_tac (esimps [phi_def, psi_def, E6]) 1), (simp_tac (esimps [mk_ap extomap, mk_ap mapoext]) 1), cong_tac 1, rtac ext 1, (simp_tac (esimps [phi_def, mk_ap ax2s]) 1), (rtac trans 1), (rtac ax1' 2), cong_tac 1, rtac ext 1, Simp_tac 1]) ; (* mmSR is a monad morphism from MR to SM *) val mmSRunit = prove_goalw MonadSR.thy [unitSR_def] "unitSM = mmSR o unitSR" (fn _ => [ (simp_tac (esimps [phi_mm, phi_psi_unit]) 1)]) ; val mmSRo = prove_goalw MonadSR.thy [oSR_def] "mmSR o g oSM (mmSR o f) = mmSR o (g oSR f)" (fn _ => [ (simp_tac (esimps [phi_mm, ppp]) 1)]) ;