(* funM.ML - functors and other generally useful stuff; functors to do with various axiom systems for a single monad *) (* have converted some meta-equalities to object equalities *) val rewrite_tac = Tactic.rewrite_tac o map mk_eq ; val fold_tac = Tactic.fold_tac o map mk_eq ; val rewrite_goals_tac = Tactic.rewrite_goals_tac o map mk_eq ; val fold_goals_tac = Tactic.fold_goals_tac o map mk_eq ; val rewtac = Tactic.rewtac o mk_eq ; val rewrite_rule = Tactic.rewrite_rule o map mk_eq ; val fold_rule = Tactic.fold_rule o map mk_eq ; fun mks th = symmetric th RS def_imp_eq handle _ => th RS sym ; fun mkoe th = th RS def_imp_eq handle _ => th ; fun mk_hd_cong th = let open HOLogic ; val (l, r) = dest_eq (dest_Trueprop (prop_of th)) ; val h = head_of l ; val thy = theory_of_thm th ; val hstr = Sign.string_of_term thy h ; in read_instantiate_sg thy [("f", hstr)] arg_cong end ; (* mk_hd_cong M.ax1 ; mk_hd_cong M.E2 ; *) fun mk_congLR thy str = let val ac = read_instantiate_sg thy [("f", str)] arg_cong ; val LR = ac RS cong ; val L = ac RS fun_cong ; val R = refl RS LR ; in (LR, L, R) end ; val str = "comp" ; signature CS = sig val congs : thm * thm * thm ; val simps : thm * thm * thm * thm ; val congLR : thm ; val congL : thm ; val congR : thm ; val id_c : thm ; val c_id : thm ; val assoc : thm ; val assoc_sym : thm ; val LaR : thm ; val idstr : string ; val ostr : string ; end ; fun rep_trans' [] = refl | rep_trans' (th :: ths) = let val th1 = rep_trans' ths RSN (2, trans) in th RS th1 handle _ => th RS def_imp_eq RS th1 end ; fun rep_trans ths = zero_var_indexes (rep_trans' ths) ; structure Cso : CS = struct val congs as (congLR, congL, congR) = mk_congLR Main.thy "comp" ; val simps as (id_c, c_id, assoc, assoc_sym) = (id_o, o_id, o_assoc, o_assoc RS sym) ; val LaR = rep_trans [congL, assoc_sym, congR] ; val idstr = "id" ; val ostr = "comp" ; end ; fun etsimps thy rules = simpset_of thy addsimps rules ; fun prove_sub_goal sub thy str = prove_goal thy (sub str) ; fun prove_sub_goalw sub thy rewrs str = prove_goalw thy (map mk_eq rewrs) (sub str) ; fun sub_goal sub thy str = goal thy (sub str) ; fun sub_goalw sub thy rewrs str = goalw thy (map mk_eq rewrs) (sub str) ; signature THYSUB = sig val thy : theory ; val sub : string -> string ; end ; (* signature THYSUB = sig end ; (* temporary *) *) signature TCS = sig include THYSUB structure Cs : CS end ; signature PREMONAD = sig include THYSUB ; val ax1 : thm (* "mapM id = id" *) val ax2s : thm (* "mapM f o mapM g = mapM (f o g)" *) val ax3s : thm (* "unitM o f = mapM f o unitM" *) val ax2 : thm ; (* "mapM (f o g) = mapM f o mapM g" *) val ax3 : thm ; (* "mapM f o unitM = unitM o f" *) end ; (* MONAD7, from7 - monads based on 7 axioms re unit, map and join, and definitions of ext and oM from these ax1 "mapM id = id" ax2s "mapM f o mapM g = mapM (f o g)" ax3s "unitM o f = mapM f o unitM" ax4 "joinM o mapM (mapM f) = mapM f o joinM" ax5 "joinM o unitM = id" ax6 "joinM o mapM unitM = id" ax7 "joinM o mapM joinM = joinM o joinM" E6 "h oM f == extM h o f" ax8 "extM f == joinM o mapM f" all the following use ax8, and the last uses E6, otherwise -- "mapM f = extM (unitM o f)" -- uses ax2s, ax6 "joinM = extM id" -- uses ax1 "extM unitM = id" -- uses ax6 "extM f o unitM = f" -- ax3s, ax5 "extM (g oM f) = extM g o extM f" -- uses ax2s, ax4, ax7 *) (* MONAD3, from3 - monads based on 3 axioms re unit, oM and ext, and definitions of map and join from these *) signature E45 = sig val E4 : thm ; (* "join == ext id" *) val E5 : thm ; (* "map f == ext (unit o f)" *) end ; signature E12 = sig val E1 : thm ; (* "ext f o unit = f" *) val E2 : thm ; (* "ext unit = id" *) end ; signature E123 = sig include E12 val E3 : thm ;(* "extM (g oM f) = extM g o extM f" *) end ; signature E126 = sig include E12 val E6 : thm ; (* "g oM y == extM g o y" *) end ; signature MONADE126 = sig include E126 TCS end ; signature MONADE12456 = sig include E126 E45 TCS end ; signature MONADE123 = sig include E123 TCS end ; signature MONAD3 = sig include MONADE123 E45 end ; signature AX7 = sig val ax1 : thm (* "mapM id = id" *) val ax2s : thm (* "mapM f o mapM g = mapM (f o g)" *) val ax3s : thm (* "unitM o f = mapM f o unitM" *) val ax4 : thm (* "joinM o mapM (mapM f) = mapM f o joinM" *) val ax5 : thm (* "joinM o unitM = id" *) val ax6 : thm (* "joinM o mapM unitM = id" *) val ax7 : thm (* "joinM o mapM joinM = joinM o joinM" *) end ; signature MONAD7 = sig include AX7 TCS val E6 : thm (* "h oM f == extM h o f" *) val ax8 : thm (* "extM f == joinM o mapM f" *) end ; signature MONADo = sig include E123 TCS val A2 : thm val A1 : thm val KR_imp : thm val KR_imp_eq : thm val ext_inj : thm val ext_cong : thm val E3' : thm val A3 : thm val A4 : thm val A4' : thm val A6 : thm val E3'_oM : thm (* "extM (h oM f) = h oM extM f" *) val A5 : thm val A5' : thm val E6 : thm val E6' : thm val is_ext : thm val is_ext' : thm val is_ext_ojo : thm (* "?y = extM ?g ==> extM (?y o ?f) = ?y o extM ?f" *) val mk_oMap : thm -> thm ; val unit_fun : thm ; structure Cs_oM : CS ; end ; signature MONAD = sig include AX7 E45 MONADo val ax8 : thm (* "ext f == join o map f" *) val ax8' : thm val ax9 : thm val ax9s : thm val ax2 : thm ; (* "map (f o g) = map f o map g" *) val ax3 : thm ; (* "map f o unit = unit o f" *) val ax4e : thm ; (* "ext (map f) = map f o join" *) val ax7e : thm ; (* "ext join = join o join" *) val ax4eo : thm ; val ax7eo : thm ; val ext_ext : thm (* "ext (ext g) = ext g o join" *) val is_ext_oj : thm (* "y = ext g ==> ext y = y o join" *) val ext_ojoin : thm (* "ext g = g o join ==> g = ext (g o unit)" *) val ext_ojoin_iff : thm (* "(ext g = g o join) = (g = ext (g o unit))" *) val extomap : thm val mapoext : thm val map_cong : thm end ; (* MONADA, fromA - monads based on four A axioms re unit and oM, and definitions of ext, map and join from these *) signature A1245 = sig val A5 : thm ; (* "extM f == f oM id" *) val A1 : thm ; (* "f oM unitM = f" *) val A2 : thm ; (* "unitM oM f = f" *) val A4 : thm ; (* "h oM f = h oM id o f" *) end ; signature MONADA1245 = sig include TCS A1245 end ; signature MONADA = sig include TCS A1245 val A3 : thm ; (* "h oM (g oM f) = h oM g oM f" *) end ; (* to show MONADA included in MONAD *) functor M2A (M : MONAD) : MONADA = struct open M end ; functor from7G (M7 : MONAD7) = struct open M7 ; local open Cs in val ax8' = ax8 RS def_imp_eq ; val [E2, ax4e, ax7e] = [ax6, ax4, ax7] RL [ax8' RS trans] ; val ax9s = rep_trans [ax8' RS congL, assoc_sym, ax2s RS congR, ax8' RS sym] ; val [ax1s, ax2, ax3, ax9] = [ax1, ax2s, ax3s, ax9s] RL [sym] ; val E1 = (rep_trans [ax8' RS congL, assoc_sym, ax3 RS congR, assoc, ax5 RS congL, id_c]) ; val G11 = rep_trans [ax3s, ax1 RS congL, id_c] RS sym ; val G12 = rep_trans [ax2, ax1 RS congL, id_c] RS sym ; val G9 = mk_eq (rep_trans [ax8', ax1 RS congR, c_id] RS sym) ; val E5 = mk_eq (rep_trans [ax9, E2 RS congL, id_c] RS sym) ; (* G9,G10 same as E4,E5 except in case of D structure *) val E4 = rewrite_rule [ax1] (mk_eq (rep_trans [ax4e, ax1 RS congL, id_c] RS sym)) ; val ax8NM' = rewrite_rule [id_c] (rep_trans [ax9, E4 RS def_imp_eq RS sym RS congL]) ; val mkeo = rep_trans [ax9, congL, assoc_sym, ax8NM' RS sym RS congR] ; val [ax4eo, ax7eo] = [ax4e, ax7e] RL [mkeo] ; val G10 = rewrite_rule [ax3] (mk_eq (rep_trans [ax4eo, E2 RS congR, c_id] RS sym)) ; val E3' = rewrite_rule [assoc, symmetric ax8] (rep_trans [ax7eo, ax4eo RS congR]) ; val E3 = refl RS simplify (HOL_ss addsimps [symmetric E6]) (E3' RS trans) ; end ; (* local *) end ; (* functor from7G *) functor from7 (M7 : MONAD7) : MONAD3 = from7G (M7) ; functor fromE126 (M : MONADE126) = struct open M ; local open Cs in val KR_imp as is_ext' = [congL, E1] MRS trans RS sym ; val KR_imp_eq = mk_eq (def_imp_eq RS KR_imp) ; val [E6'] = [E6] RL [def_imp_eq] ; val A1 = rep_trans [E6', E1] ; val A2 = rep_trans [E6', E2 RS congL, id_c] ; val A5' = zero_var_indexes ([E6', c_id] MRS trans RS sym) ; val [A5] = map mk_eq [A5'] ; val A4 = rewrite_rule [A5] E6' ; val A6 = rep_trans [E6', assoc, E6' RS sym RS congL] ; val A4' = rep_trans [A6, A1 RS congL] ; val ext_inj = [congL, E1, E1] MRS box_equals ; val ext_cong = mk_hd_cong E2 ; val th = rep_trans [E2 RS sym RS congL, E1] ; val unit_refl = [th RS sym, th] MRS trans ; (* unit o _ is a functor *) val unit_fun = rep_trans [A4', assoc_sym, unit_refl RS congL] RS sym ; end ; (* local *) end ; (* functor fromE126 *) functor fromE123 (ME : MONADE123) = struct open ME ; local open Cs in val E6' = rep_trans [E1 RS sym, E3 RS congL, assoc_sym, E1 RS congR] ; val [E6] = map mk_eq [E6'] ; local structure ME126 : MONADE126 = struct open ME val E6 = E6 end ; structure FME126 = fromE126 (ME126) ; in open FME126 ; end ; val E3' = rewrite_rule [E6] E3 ; val E3'_oM = [E3, E6' RS sym] MRS trans ; (* note, E3' and E3 involve moving the occurrence of extM in an expression *) (* now prove the rules used in MonadA, alternative proofs of A1, A2 *) val ext_A3 = rep_trans [E3, E3 RS congR, assoc, E3 RS sym RS congL, E3 RS sym]; val ext_A1 = rep_trans [E3, E2 RS congR, c_id] ; val ext_A2 = rep_trans [E3, E2 RS congL, id_c] ; val [A1, A2, A3] = ([ext_A1, ext_A2, ext_A3] RL [ext_inj]) ; (* gives a necessary (and obviously sufficient) condition for g to be of the form extM f *) val is_ext_ojo = sym RS (standard o asm_simplify HOL_ss o fst o freeze_thaw) (rep_trans [E3', congL]) ; val ie1 = tacsthm [etac KR_imp 1, atac 1] (conjI RS cut_rl) ; val is_ext = standard (tacsthm [(freeze_tac (hyp_subst_tac 2)), atac 2] (ie1 RS conjE)) ; val E6's = E6' RS sym ; val ofc = [congR, E6's, E6's] MRS box_equals ; fun mk_oMap th = simplify (etsimps thy [A3]) (th RS ofc handle THM _ => th RS def_imp_eq RS ofc) ; structure Cs_oM : CS = struct val (oM_tm $ unitM_tm $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of A2)) ; val ostr = Sign.string_of_term thy oM_tm ; val idstr = Sign.string_of_term thy unitM_tm ; val congs as (congLR, congL, congR) = mk_congLR thy ostr ; val simps as (id_c, c_id, assoc, assoc_sym) = (A2, A1, A3, A3 RS sym) ; val LaR = rep_trans [congL, assoc_sym, congR] ; end ; end ; (* local *) end ; (* functor fromE123 *) functor T3otoA (ME : MONADE123) : MONADA = struct structure S = fromE123 (ME) ; open S end ; functor fromE12456 (ME : MONADE12456) = struct open ME ; local structure ME126 = fromE126 (ME) ; open Cs in open ME126 ; val [E4', E5', E6'] = map mkoe [E4, E5, E6] ; val ax3s = E5' RS is_ext' ; val ax3 = ax3s RS sym ; val ax5 = E4' RS is_ext' RS sym ; val ax1 = rep_trans [E5', c_id RS ext_cong, E2] ; val E5's = E5' RS sym ; val map_cong = mk_hd_cong ax1 ; end ; (* local *) end ; (* functor fromE12456 *) functor from3G (ME : MONAD3) = struct open ME ; local structure FE123 = fromE123 (ME) ; structure ME12456 = struct open FE123 ME end ; structure FE12456 = fromE12456 (ME12456) ; open Cs in open FE12456 FE123 ; val extomap as ax9s = simplify (HOL_ss addsimps [assoc, E1]) (rep_trans [E5' RS congR, E3' RS sym]) ; val ax9 = ax9s RS sym ; val ax8' = rewrite_rule [id_c] (rep_trans [ax9, E4' RS sym RS congL]) ; val ax8 = mk_eq ax8' ; val ax6 = rewrite_rule [ax8] E2 ; (* note - this version of ext_ojoin allows distinct variables *) val ext_ojoin = rep_trans [ax9, congL, assoc_sym, ax6 RS congR, c_id] RS sym ; val ext_ext = rewrite_rule [c_id] (rep_trans [E3', E4' RS sym RS congR]); val is_ext_oj = sym RS (standard o asm_simplify HOL_ss o fst o freeze_thaw) (rep_trans [ext_ext, congL]) ; (* by remark above is_ext, this says that (extM g = g o joinM) holds iff g is of the form extM f *) val ext_ojoin_iff = tacsthm [etac is_ext_oj 2, etac ext_ojoin 1] iffI ; (* note - converses to E3' : suppose "extM (h o g) = h o extM g" holds for all g; in fact, if it holds for g = id, then ext_ojoin says h = extM (h o unitM); if it holds for g = unitM, then that gives directly extM (h o unitM) = h; ie, in either case, equivalently (by is_ext') h is for the form extM f *) (* two proofs of ax2, first based on composition of functors *) val ax2 = fold_rule [E5] (rep_trans [unit_fun RS ext_cong, E3]) ; val ax2 = rep_trans [E5', assoc RS ext_cong, ax9, E5' RS sym RS congL] ; val ax2s = ax2 RS sym ; val [ax4e, ax7e, ax4eo, ax7eo] = [E5', E4'] RL [is_ext_oj, is_ext_ojo] ; val [ax4, ax7] = map (rewrite_rule [ax8]) [ax4e, ax7e] ; val mapoext = ax4eo RS sym ; end ; (* local *) end ; (* functor from3G *) functor from3 (ME : MONAD3) : MONAD = from3G (ME) ; (* structure M = from3G (ME) ; structure SA : MONADA = M ; structure FSA = fromA (SA) ; structure Mo' = fromE123 (FSA) ; *) functor fromA1245 (MA : MONADA1245) = struct open MA ; local open Cs in val E6' = fold_rule [A5] A4 ; val E6 = mk_eq E6' ; val [A5'] = [A5] RL [def_imp_eq] ; val E1 = rewrite_rule [E6] A1 ; val E2 = rep_trans [A5', A2] ; (* A6 is apparently stronger version of A4, but can be proved directly from A4 *) val A6 = rep_trans [A4, assoc, A4 RS sym RS congL] ; end ; (* local *) end ; (* functor fromA *) functor fromAG (MA : MONADA) = struct open MA ; local open Cs structure FMA1245 = fromA1245 (MA) ; in open FMA1245 ; val E3 = rep_trans [A5' RS congR, mks E6, A3, E6, c_id] RS sym ; end ; (* local *) end ; (* functor fromAG *) functor fromA (MA : MONADA) : MONADE123 = fromAG (MA) ;