fun upr _ = update_thy "MonadPR" ; fun etsimps thy rules = simpset_of thy addsimps rules ; fun mk_ap th = rewrite_rule [mk_eq o_apply] (th RS fun_cong handle THM _ => th RS def_imp_eq RS fun_cong) ; val ofc = read_instantiate_sg (sign_of Fun.thy) [("f", "%y. ?z o y")] arg_cong ; fun mk_oap th = simplify (esimps [o_assoc]) (th RS ofc handle THM _ => th RS def_imp_eq RS ofc) ; fun prove_sub_goal sub thy str = prove_goal thy (sub str) ; fun prove_sub_goalw sub thy rewrs str = prove_goalw thy rewrs (sub str) ; fun sub_goal sub thy str = goal thy (sub str) ; fun sub_goalw sub thy rewrs str = goalw thy rewrs (sub str) ; fun sub str = str ; val oQ_R = mk_eq (prove_sub_goal sub thy "g oQ f = R g o f" (fn _ => [(rtac trans 1), (rtac (RRunit RS sym) 1), (simp_tac (esimps [Rfun]) 1), (rtac trans 1), (rtac (o_assoc RS sym) 1), (simp_tac (esimps [RRunit]) 1)])) ; val oQoassoc = prove_sub_goalw sub thy [oQ_R] "h oQ (g o f) = h oQ g o f" (fn _ => [(rtac o_assoc 1)]) ; val oM_P = mk_eq (prove_sub_goal sub thy "h oM f = P h oQ f" (fn _ => [(rtac (PRunit RS sym RS trans) 1), (simp_tac (etsimps thy [Pfun]) 1), rtac (oQoassoc RS sym RS trans) 1, (simp_tac (etsimps thy [PRunit]) 1)])) ; (* typeing problems here *) val A6 = prove_sub_goalw sub thy [oM_P] "h oM (g o f) = h oM g o f" (fn _ => [(rtac (oQoassoc RS sym) 1)]) ;