Menu
▾
▴
[Hol-checkins] SF.net SVN: hol:[7589] branches/HOL-Omega/examples/HolOmega/interim
|
From: <jer...@us...> - 2009-12-24 06:02:24
|
Revision: 7589
http://hol.svn.sourceforge.net/hol/?rev=7589&view=rev
Author: jeremydawson
Date: 2009-12-24 06:02:12 +0000 (Thu, 24 Dec 2009)
Log Message:
-----------
bug flagged in my previous log message was not, just my typo
Modified Paths:
--------------
branches/HOL-Omega/examples/HolOmega/interim/KmonadScript.sml
branches/HOL-Omega/examples/HolOmega/interim/auxLib.sml
Added Paths:
-----------
branches/HOL-Omega/examples/HolOmega/interim/dist_monadsScript.sml
Modified: branches/HOL-Omega/examples/HolOmega/interim/KmonadScript.sml
===================================================================
--- branches/HOL-Omega/examples/HolOmega/interim/KmonadScript.sml 2009-12-23 02:11:42 UTC (rev 7588)
+++ branches/HOL-Omega/examples/HolOmega/interim/KmonadScript.sml 2009-12-24 06:02:12 UTC (rev 7589)
@@ -22,16 +22,21 @@
val _ = new_theory "Kmonad";
-(* abbreviate a much used tactic *)
+(* now in auxLib
+(* abbreviate much used tactics *)
fun farwmmp con = (FIRST_ASSUM (fn th =>
CHANGED_TAC (REWRITE_TAC [MATCH_MP con th]))) ;
+fun frrc_rewr impth =
+ FIRST_REP_RES (fn th => CHANGED_TAC (REWRITE_TAC [th])) impth ;
+
(* given f = \x. ..., put into more usual form *)
fun fix_abs_eq rewrs th =
let val th0 = REWRITE_RULE ([TY_FUN_EQ_THM, FUN_EQ_THM] @ rewrs) th ;
val th1 = CONV_RULE (DEPTH_CONV TY_BETA_CONV) th0 ;
val th2 = CONV_RULE (DEPTH_CONV BETA_CONV) th1 ;
in th2 end ;
+*)
(* Kleisli arrow, 'A = arrow type in original category, 'M = monad type *)
val _ = type_abbrev ("Kleisli", Type `: \'A 'M 'a 'b. ('a, 'b 'M) 'A`) ;
@@ -44,6 +49,8 @@
\ (h : ('A,'M,'b,'c) Kleisli) (k : ('A,'M,'a,'b) Kleisli).
comp (ext h) k : ('A,'M,'a,'c) Kleisli`) ;
+val Kcomp_thm = save_thm ("Kcomp_thm", fix_abs_eq [] Kcomp_def) ;
+
val Kmonad_def = new_definition("Kmonad_def", Term
`Kmonad = \:'A 'M. \ ((id, comp) : 'A category)
(unit: (!'a. ('a, 'a 'M) 'A), ext: 'M ('A ext)).
@@ -120,9 +127,13 @@
(farwmmp KmonDAss), (farwmmp catDAss),
(farwmmp KmonDRU), (farwmmp catDLU) ]) ;
-val KdmonadD_EXT_SYM = GSYM (fix_abs_eq [EXT_def] KdmonadD_EXT) ;
-val KdmonadD_JOIN_SYM = GSYM (fix_abs_eq [JOINE_def] KdmonadD_JOIN) ;
-val KdmonadD_MAP_SYM = GSYM (fix_abs_eq [MAPE_def] KdmonadD_MAP) ;
+val KdmonadD_EXTe = fix_abs_eq [] (REWRITE_RULE [EXT_def] KdmonadD_EXT) ;
+val KdmonadD_EXTe = (fix_abs_eq [EXT_def] KdmonadD_EXT) ;
+val KdmonadD_JOINe = (fix_abs_eq [JOINE_def] KdmonadD_JOIN) ;
+val KdmonadD_MAPe = (fix_abs_eq [MAPE_def] KdmonadD_MAP) ;
+val KdmonadD_EXT_SYM = GSYM KdmonadD_EXTe ;
+val KdmonadD_JOIN_SYM = GSYM KdmonadD_JOINe ;
+val KdmonadD_MAP_SYM = GSYM KdmonadD_MAPe ;
(* Kleisli category is a category iff 'M is a monad *)
@@ -278,9 +289,11 @@
val Kmonad_extomap = save_thm ("Kmonad_extomap",
(DISCH_ALL o TY_GEN_ALL o GEN_ALL o UNDISCH_ALL) Kmonad_extomap') ;
+(*
val Kdmonad_extomap = DISCH_ALL
(MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] Kmonad_extomap)
(UNDISCH KdmonadDK)) ;
+*)
val Kdmonad_extomap = store_thm ("Kdmonad_extomap",
``Kdmonad [:'A,'M:] (id,comp) (unit,ext,map,join) /\
@@ -297,6 +310,8 @@
EVERY [ REPEAT STRIP_TAC, (ASM_REWRITE_TAC []),
(farwmmp KmonDAss), (farwmmp catDRU) ]) ;
+val Kmonad_umj47 = save_thm ("Kmonad_umj47", inst_eqs Kmonad_t2a) ;
+
val tmsgx = ``Kmonad [:'A, 'M:] (id,comp) (unit,ext) /\ category (id, comp) ==>
(ext [:'a, 'b:] (comp f unit) =
comp (ext f) (ext [:'a, 'a 'M:] (comp unit unit)))`` ;
@@ -312,10 +327,60 @@
val Kmonad_t2b' = DISCH_ALL (GSYM (UNDISCH_ALL Kmonad_t2b)) ;
+val Kdmonad_t2a = save_thm ("Kdmonad_t2a", DISCH_ALL
+ (MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] Kmonad_t2a)
+ (UNDISCH KdmonadDK))) ;
+
val Kdmonad_t2b = save_thm ("Kdmonad_t2b", DISCH_ALL
(MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] Kmonad_t2b)
(UNDISCH KdmonadDK))) ;
+(* get the 7 axioms for unit, map, join *)
+val Kdmonad_umj2 = store_thm ("Kdmonad_umj2",
+ ``category (id,comp) ==> Kdmonad [:'A, 'M:] (id,comp) (unit,ext,map,join) ==>
+ !f g. map (comp g f) = comp (map g) (map f)``,
+ EVERY [ (REWRITE_TAC [Kdmonad_thm, MAPE_def]), (REPEAT STRIP_TAC),
+ (ASM_REWRITE_TAC []), TY_BETA_TAC, BETA_TAC,
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KmonDAss), (farwmmp catDAss),
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KmonDRU) ]) ;
+
+val Kdmonad_umj3 = store_thm ("Kdmonad_umj3",
+ ``category (id,comp) ==> Kdmonad [:'A, 'M:] (id,comp) (unit,ext,map,join) ==>
+ !f. comp (map f) unit = comp unit f``,
+ EVERY [ (REWRITE_TAC [Kdmonad_thm, MAPE_def]), (REPEAT STRIP_TAC),
+ (ASM_REWRITE_TAC []), TY_BETA_TAC, BETA_TAC,
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KmonDRU) ]) ;
+
+val Kdmonad_umj1 = store_thm ("Kdmonad_umj1",
+ ``category (id,comp) ==> Kdmonad [:'A, 'M:] (id,comp) (unit,ext,map,join) ==>
+ (map id = id)``,
+ EVERY [ (REWRITE_TAC [Kdmonad_thm, MAPE_def]), (REPEAT STRIP_TAC),
+ (ASM_REWRITE_TAC []), TY_BETA_TAC, BETA_TAC, (farwmmp catDRU),
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KmonDLU) ]) ;
+
+val Kdmonad_umj5 = store_thm ("Kdmonad_umj5",
+ ``category (id,comp) ==> Kdmonad [:'A, 'M:] (id,comp) (unit,ext,map,join) ==>
+ (comp join unit = id)``,
+ EVERY [ (REWRITE_TAC [Kdmonad_thm, JOINE_def]), (REPEAT STRIP_TAC),
+ (ASM_REWRITE_TAC []), TY_BETA_TAC,
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KmonDRU) ]) ;
+
+val Kdmonad_umj6 = store_thm ("Kdmonad_umj6",
+ ``category (id,comp) ==> Kdmonad [:'A, 'M:] (id,comp) (unit,ext,map,join) ==>
+ (comp join (map unit) = id)``,
+ EVERY [ (REPEAT STRIP_TAC),
+ (USE_LIM_RES_TAC (fn th => REWRITE_TAC [th]) KdmonadD_EXT_SYM),
+ (FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP KdmonadDK)),
+ (USE_LIM_RES_TAC MATCH_ACCEPT_TAC KmonDLU) ]) ;
+
+(*
+show_types := true ;
+show_types := false ;
+handle e => Raise e ;
+set_goal ([], it) ;
+val (sgs, goal) = top_goal () ;
+*)
+
(* approach to distributive law for monads;
a monad in the Kleisli category of another monad *)
(* first note this type equality *)
@@ -497,7 +562,8 @@
(C3) is a special case of E1D, (C4) is a special case of J1S
but (C3) implies E1D and (C4) implies J1S
*)
-val tm_C3_J1S = ``category (id, comp) /\
+(* note - the extra condition here is implied by mapNM f = mapm (mapN f) *)
+val tm_C4_J1S = ``category (id, comp) /\
Kdmonad [:'A, 'M:] (id, comp) (unitM, extM, mapM, joinM) /\
Kdmonad [:'A, 'N o 'M:] (id, comp) (unitNM, extNM, mapNM, joinNM) /\
(!: 'a 'b. !f. extM (mapNM [:'a,'b:] f) = comp (mapNM [:'a,'b:] f) joinM) ==>
@@ -507,7 +573,7 @@
fun ttac th = FIRST_X_ASSUM (fn ass =>
REWRITE_TAC [EXT_def, test_lhs_head_var "extNM" (MATCH_MP th ass)]) ;
-val C3_IFF_J1S = store_thm ("C3_IFF_J1S", tm_C3_J1S,
+val C4_IFF_J1S = store_thm ("C4_IFF_J1S", tm_C4_J1S,
EVERY [ STRIP_TAC, (REWRITE_TAC [J1S_def]), EQ_TAC]
THENL [
EVERY [
@@ -525,9 +591,25 @@
(REWRITE_TAC [JOINE_def, MATCH_MP KdmonadD_JOIN th])))),
TY_BETA_TAC, (ASM_REWRITE_TAC []) ]]) ;
-
+val tm_C3_iff_E1D = ``category (id, comp) /\
+ Kdmonad [:'A, 'M:] (id, comp) (unitM, extM, mapM, joinM) /\
+ Kdmonad [:'A, 'N:] (id, comp) (unitN, extN, mapN, joinN) /\
+ Kdmonad [:'A, 'N o 'M:] (id, comp) (unitNM, extNM, mapNM, joinNM) /\
+ (mapNM = \:'a 'b. \f. mapM (mapN f)) ==>
+ ((!: 'a. comp joinNM (mapM unitN) = joinM [:'a 'N:]) =
+ (!: 'a 'b. !f. comp (extNM [:'a, 'b:] f) (mapM unitN) = extM f))``;
-
+val C3_IFF_E1D = store_thm ("C3_IFF_E1D", tm_C3_iff_E1D,
+ (EVERY [STRIP_TAC, EQ_TAC, REPEAT STRIP_TAC])
+ THENL [
+ (EVERY [ frrc_rewr KdmonadD_EXTe, frrc_rewr KdmonadD_EXTe,
+ (ASM_REWRITE_TAC []), TY_BETA_TAC, BETA_TAC,
+ (farwmmp catDRAss), frrc_rewr (GSYM Kdmonad_umj2),
+ frrc_rewr Kdmonad_umj3, frrc_rewr Kdmonad_umj2,
+ (farwmmp catDAss), (ASM_REWRITE_TAC []) ]),
+ (EVERY [ frrc_rewr KdmonadD_JOINe , frrc_rewr KdmonadD_JOINe,
+ (ASM_REWRITE_TAC []) ]) ]) ;
+
(*
show_types := true ;
show_types := false ;
@@ -536,7 +618,7 @@
val (sgs, goal) = top_goal () ;
*)
(* Barr & Wells, conditions (C2) and (C5) for compatible monads,
- we show these are equivalent *)
+ we show these are equivalent; note, (C5) is (J2) of Jones & Duponcheeel *)
val tmBWC25x =
``Gmonad (id,comp) [:'N, 'M:] (dunit,dmap,djoin)
@@ -572,6 +654,26 @@
(farwmmp KmonDRU), (farwmmp catDRAss),
(farwmmp KmonDRU), (farwmmp catDRU) ]) ;
+(* J1 and J2, ie, C4 and C5, both imply a certain equality *)
+val E1D_J12 = store_thm ("E1D_J12",
+ ``Kmonad [:'A, 'M:] (id,comp) (unitM,extM) ==>
+ (!: 'a 'b. !f. comp (extNM f) (mapM unitN) = extM f) ==>
+ (comp (extNM unitM) (mapM unitN) = id)``,
+ EVERY [ (REPEAT STRIP_TAC), (ASM_REWRITE_TAC []), (farwmmp KmonDLU) ]) ;
+
+val C2_J12 = store_thm ("C2_J12",
+ ``category [:'A:] (id,comp) ==>
+ Kdmonad [:'A, 'N:] (id,comp) (unitN,extN,mapN,joinN) ==>
+ Kdmonad [:'A, 'M:] (id,comp) (unitM,extM,mapM,joinM) ==>
+ (extNM unitM = mapM joinN) ==> (comp (extNM unitM) (mapM unitN) = id)``,
+ EVERY [ (REPEAT STRIP_TAC), (ASM_REWRITE_TAC []),
+ (frrc_rewr (GSYM Kdmonad_umj2)),
+ (frrc_rewr Kdmonad_umj5), (frrc_rewr Kdmonad_umj1) ]) ;
+
+(* and if dunit = mapM unitN, then from J12,
+ ie, (comp (extNM unitM) (mapM unitN) = id),
+ we can satisfy the conditions of Kmonad_IMP_Gmonad *)
+
(*
show_types := true ;
show_types := false ;
Modified: branches/HOL-Omega/examples/HolOmega/interim/auxLib.sml
===================================================================
--- branches/HOL-Omega/examples/HolOmega/interim/auxLib.sml 2009-12-23 02:11:42 UTC (rev 7588)
+++ branches/HOL-Omega/examples/HolOmega/interim/auxLib.sml 2009-12-24 06:02:12 UTC (rev 7589)
@@ -105,7 +105,10 @@
fun USE_LIM_RES_TAC ttac imp_thm =
ASSUM_LIST (ttac o thm_from_ass imp_thm) ;
-(* FIRST_REP_RES : thm_tactic -> thm_tactic *)
+(* FIRST_REP_RES : thm_tactic -> thm_tactic
+ resolves implication theorem against assumptions as much as possible
+ and applies ttac to result - backtracking in regard to choice of assumption
+ and whether to fully resolve implication theorem *)
fun FIRST_REP_RES ttac impth =
FIRST_ASSUM (fn ass => FIRST_REP_RES ttac (MATCH_MP impth ass))
(* following delayed evaluation since ttac impth can cause an
@@ -150,6 +153,25 @@
val iffD1 =
(DISCH_ALL o CONJUNCT1 o UNDISCH o fst o EQ_IMP_RULE o SPEC_ALL) EQ_IMP_THM ;
+(* abbreviate much used tactics *)
+(* farwmmp, frrc_rewr : thm -> tactic,
+ for resolving an implicative theorem against the assumptions,
+ in a way which will rewrite, and change, the goal;
+ farwmmp resolves implication exactly once, frrc_rewr any number of times *)
+fun farwmmp con = (FIRST_ASSUM (fn th =>
+ CHANGED_TAC (REWRITE_TAC [MATCH_MP con th]))) ;
+
+fun frrc_rewr impth =
+ FIRST_REP_RES (fn th => CHANGED_TAC (REWRITE_TAC [th])) impth ;
+
+(* given f = \x. ..., put into more usual form *)
+fun fix_abs_eq rewrs th =
+ let val th0 = REWRITE_RULE ([TY_FUN_EQ_THM, FUN_EQ_THM] @ rewrs) th ;
+ val th1 = CONV_RULE (DEPTH_CONV TY_BETA_CONV) th0 ;
+ val th2 = CONV_RULE (DEPTH_CONV BETA_CONV) th1 ;
+ in th2 end ;
+
+
end ; (* local open HolKernel bossLib *)
end ; (* structure auxLib *)
Added: branches/HOL-Omega/examples/HolOmega/interim/dist_monadsScript.sml
===================================================================
--- branches/HOL-Omega/examples/HolOmega/interim/dist_monadsScript.sml (rev 0)
+++ branches/HOL-Omega/examples/HolOmega/interim/dist_monadsScript.sml 2009-12-24 06:02:12 UTC (rev 7589)
@@ -0,0 +1,75 @@
+
+(* proof of various results in Barr & Wells about distributive law for monads,
+ and in Jones & Duponcheel re prod, dorp, swap constructions *)
+
+structure dist_monadsScript =
+struct
+
+open HolKernel Parse boolLib
+ bossLib
+
+open categoryTheory KmonadTheory ;
+open auxLib ;
+(*
+load "auxLib" ;
+load "dist_monadsTheory" ; open dist_monadsTheory ;
+fun sge tm = set_goal ([], tm) ;
+fun eev tacs = e (EVERY tacs) ;
+fun eall [] = ()
+ | eall (t :: ts) = (e t ; eall ts) ;
+*)
+
+val _ = set_trace "Unicode" 1;
+val _ = set_trace "kinds" 0;
+
+val _ = new_theory "dist_monads";
+
+(* given monad N in the Kleisli category of monad M,
+ prove Jones & Duponcheel results about prod, where prod = pext id *)
+
+val tm_Kcm_P2 = ``category (id, comp) /\
+ Kmonad [:'A:] (id,comp) (unitM, extM : ('A, 'M) ext) ==>
+ Kmonad [: ('A, 'M) Kleisli, 'N :]
+ (unitM, Kcomp (id,comp) extM) (unitNM, pext) ==>
+ (unitNM = \:'a. comp (unitM [:'a 'N:]) (unitN [:'a:])) ==>
+ (comp (pext id) unitN = id)`` ;
+
+val Kcm_P2 = store_thm ("Kcm_P2", tm_Kcm_P2,
+ EVERY [ (REWRITE_TAC [Kcomp_def]), (REPEAT STRIP_TAC),
+ (FIRST_ASSUM (MP_TAC o MATCH_MP KmonDRU)),
+ (ASM_REWRITE_TAC []), TY_BETA_TAC, BETA_TAC,
+ (farwmmp catDAss), (frrc_rewr KmonDRU),
+ STRIP_TAC, (FIRST_ASSUM MATCH_ACCEPT_TAC)]) ;
+
+val Kcm_P3 = store_thm ("Kcm_P3",
+ ``Kmonad [: ('A, 'M) Kleisli, 'N :]
+ (unitM, Kcomp (id,comp) extM) (unitNM, pext) ==>
+ (pext (unitNM [:'a:]) = unitM [:'a 'N:])``,
+ EVERY [ (REWRITE_TAC [Kcomp_def]), STRIP_TAC,
+ (FIRST_ASSUM (ASSUME_TAC o GSYM o MATCH_MP KmonDLU)),
+ (ASM_REWRITE_TAC []) ]) ;
+
+(*
+show_types := true ;
+show_types := false ;
+handle e => Raise e ;
+set_goal ([], it) ;
+val (sgs, goal) = top_goal () ;
+*)
+
+(*
+show_types := true ;
+show_types := false ;
+handle e => Raise e ;
+set_goal ([], it) ;
+val (sgs, goal) = top_goal () ;
+*)
+
+val _ = set_trace "types" 1;
+val _ = set_trace "kinds" 0;
+val _ = html_theory "dist_monads";
+
+val _ = export_theory();
+
+end; (* structure dist_monadsScript *)
+
Property changes on: branches/HOL-Omega/examples/HolOmega/interim/dist_monadsScript.sml
___________________________________________________________________
Added: svn:mime-type
+ text/plain
Added: svn:eol-style
+ native
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|