structure kozen = struct val thy = the_context () end ; val _ = use_legacy_bindings kozen.thy ; Addsimps [arr_id] ; val oafc = read_instantiate_sg (sign_of kozen.thy) [("f", "%y. ?z oa y")] arg_cong; fun mk_oaap th = simplify (esimps [arr_assoc]) (th RS oafc handle THM _ => th RS def_imp_eq RS oafc) ; val _ = qed_goalw "arrstI" kozen.thy [arrst_def] "arrst cs carr ct" fn_at ; AddIffs [arrstI] ; val _ = qed_goal "arrstI_TY" kozen.thy "arrst TYPE (?'cs) carr TYPE (?'ct)" fn_at ; val _ = bind_thm ("ntGa", [arrstI, arrstI] MRS ntGa_ty) ; (* can't simplify using ntGa' because it has new variables on the rhs *) val _ = bind_thm ("ntGa_TY", [arrstI_TY, arrstI_TY] MRS ntGa_ty) ; val ic_defs = [compC_def, compD_def, compCD_def, compE_def, idC_def, idD_def, idCD_def, idE_def] ; (* composition of product category arrows obeys identity and associativity, same theorem as for the arrow category *) val prod_comp_id_ass = prove_goalw kozen.thy [prod_id_def] "(fs, ft) ox prod_id = (fs, ft) & \ \ prod_id ox (fs, ft) = (fs, ft) & \ \ ((hs, ht) ox (gs, gt)) ox (fs, ft) = \ \ (hs, ht) ox ((gs, gt) ox (fs, ft))" (fn _ => [ (simp_tac (esimps [arr_assoc]) 1) ]) ; (* for F : Fun [C x D, E], theta F : Fun [C, Fun [D, E]], so for c : C, theta F c should be an object in Fun [D, E], ie a functor *) val _ = qed_goalw_spec_mp "theta_F_obj_arr_TY_id'" kozen.thy (prod_id_def :: theta_F_obj_arr_TY_def :: ic_defs) "F idCD = idE --> theta_F_obj_arr_TY F c idD = idE" fn_at ; (* making Fi all F restricts types *) val _ = qed_goalw_spec_mp "theta_F_obj_arr_TY_comp'" kozen.thy (theta_F_obj_arr_TY_def :: ic_defs) "F1 ((idC, g) ocd (idC, f)) = F2 (idC, g) oe F3 (idC, f) --> \ \ theta_F_obj_arr_TY F1 c (g od f) = \ \ theta_F_obj_arr_TY F2 c g oe theta_F_obj_arr_TY F3 c f" (fn _ => [ (rtac impI 1), (rtac trans 1), atac 2, Simp_tac 1 ]) ; val _ = bind_thm ("theta_F_obj_arr_TY_id", tacthm (rtac idXE 1) theta_F_obj_arr_TY_id') ; val _ = bind_thm ("theta_F_obj_arr_TY_comp", tacthm (rtac compXE 1) theta_F_obj_arr_TY_comp') ; (* and for carr : C (cs, ct), theta F carr should be an arrow in Fun [D, E], ie a natural transformation *) val _ = qed_goalw_spec_mp "theta_F_arr_nt'" kozen.thy [theta_F_obj_arr_TY_def, theta_F_arr_TY_def, arrst_def] "arrst cs carr ct --> arrst ds darr dt --> \ \ theta_F_obj_arr_TY XE ct darr oe theta_F_arr_TY XE carr ds = \ \ theta_F_arr_TY XE carr dt oe theta_F_obj_arr_TY XE cs darr" (fn _ => [ Safe_tac, (rtac box_equals 1), (rtac compXE 2), (rtac compXE 2), (simp_tac (esimps (compCD_def :: ic_defs)) 1) ]) ; val _ = bind_thm ("theta_F_arr_nt", [arrstI, arrstI] MRS theta_F_arr_nt') ; (* to show etaG is a functor *) val _ = ListPair.app bind_thm (["idGo'", "idGa'", "compGo'", "compGa'", "ntGa'", "ntGa_TY'"], map (rewrite_rule ic_defs) [idGo, idGa, compGo, compGa, ntGa, ntGa_TY]) ; val _ = qed_goalw "etaG_fun_id" kozen.thy (prod_id_def :: ic_defs) "etaG idCD = idE" (fn _ => [ (simp_tac (esimps (idGo' :: idGa' :: ic_defs)) 1) ]) ; val _ = qed_goalw "etaG_fun_comp" kozen.thy (ic_defs) "etaG ((c2, d2) ocd (c1, d1)) = etaG (c2, d2) oe etaG (c1, d1)" (fn _ => [ (simp_tac (esimps (source_TY_def :: target_TY_def :: compGo' :: compGa' :: ic_defs)) 1), (simp_tac (esimps [arr_assoc, ntGa_TY', mk_oaap ntGa_TY']) 1) ]) ; (* note difficulty in the above at first, can't simplify using ntGa' because it has new variables on the rhs, alternative proofs from level 1 : (simp_tac (esimps [arr_assoc]) 1), (stac (mk_oaap ntGa' RS sym) 1), (rtac refl 1), or (simp_tac (esimps [arr_assoc]) 1), (cong_tac 1), (simp_tac (esimps [arr_assoc RS sym]) 1), (cong_tac 1), (rtac ntGa' 1) *) (* set show_types ; reset show_types ; set show_sorts ; reset show_sorts ; *)