1(* Title: HOL/Tools/BNF/bnf_comp_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Copyright 2012 5 6Tactics for composition of bounded natural functors. 7*) 8 9signature BNF_COMP_TACTICS = 10sig 11 val mk_comp_bd_card_order_tac: Proof.context -> thm list -> thm -> tactic 12 val mk_comp_bd_cinfinite_tac: Proof.context -> thm -> thm -> tactic 13 val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic 14 val mk_comp_map_comp0_tac: Proof.context -> thm -> thm -> thm list -> tactic 15 val mk_comp_map_cong0_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic 16 val mk_comp_map_id0_tac: Proof.context -> thm -> thm -> thm list -> tactic 17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic 18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm option -> thm -> thm list -> tactic 19 val mk_comp_set_map0_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic 20 val mk_comp_wit_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic 21 22 val kill_in_alt_tac: Proof.context -> tactic 23 val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic 24 25 val empty_natural_tac: Proof.context -> tactic 26 val lift_in_alt_tac: Proof.context -> tactic 27 val mk_lift_set_bd_tac: Proof.context -> thm -> tactic 28 29 val mk_permute_in_alt_tac: Proof.context -> ''a list -> ''a list -> tactic 30 31 val mk_le_rel_OO_tac: Proof.context -> thm -> thm -> thm list -> tactic 32 val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic 33 val mk_simple_pred_set_tac: Proof.context -> thm -> thm -> tactic 34 val mk_simple_wit_tac: Proof.context -> thm list -> tactic 35 val mk_simplified_set_tac: Proof.context -> thm -> tactic 36 val bd_ordIso_natLeq_tac: Proof.context -> tactic 37end; 38 39structure BNF_Comp_Tactics : BNF_COMP_TACTICS = 40struct 41 42open BNF_Util 43open BNF_Tactics 44 45val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; 46val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs}; 47val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; 48val trans_o_apply = @{thm trans[OF o_apply]}; 49 50 51(* Composition *) 52 53fun mk_comp_set_alt_tac ctxt collect_set_map = 54 unfold_thms_tac ctxt @{thms comp_assoc} THEN 55 unfold_thms_tac ctxt [collect_set_map RS sym] THEN 56 rtac ctxt refl 1; 57 58fun mk_comp_map_id0_tac ctxt Gmap_id0 Gmap_cong0 map_id0s = 59 EVERY' ([rtac ctxt @{thm ext}, rtac ctxt (Gmap_cong0 RS trans)] @ 60 map (fn thm => rtac ctxt (thm RS fun_cong)) map_id0s @ [rtac ctxt (Gmap_id0 RS fun_cong)]) 1; 61 62fun mk_comp_map_comp0_tac ctxt Gmap_comp0 Gmap_cong0 map_comp0s = 63 EVERY' ([rtac ctxt @{thm ext}, rtac ctxt sym, rtac ctxt trans_o_apply, 64 rtac ctxt (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac ctxt Gmap_cong0] @ 65 map (fn thm => rtac ctxt (thm RS sym RS fun_cong)) map_comp0s) 1; 66 67fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = 68 unfold_thms_tac ctxt [set'_eq_set] THEN 69 EVERY' ([rtac ctxt @{thm ext}] @ 70 replicate 3 (rtac ctxt trans_o_apply) @ 71 [rtac ctxt (arg_cong_Union RS trans), 72 rtac ctxt (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), 73 rtac ctxt (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), 74 rtac ctxt Gmap_cong0] @ 75 map (fn thm => rtac ctxt (thm RS fun_cong)) set_map0s @ 76 [rtac ctxt (Gset_map0 RS comp_eq_dest_lhs), rtac ctxt sym, rtac ctxt trans_o_apply, 77 rtac ctxt trans_image_cong_o_apply, rtac ctxt trans_image_cong_o_apply, 78 rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] 79 RS trans), 80 rtac ctxt @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac ctxt arg_cong_Union, 81 rtac ctxt @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]}, 82 rtac ctxt @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ 83 [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac ctxt @{thm trans[OF image_insert]}, 84 rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext}, 85 rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply, 86 rtac ctxt @{thm trans[OF image_image]}, rtac ctxt @{thm sym[OF trans[OF o_apply]]}, 87 rtac ctxt @{thm image_cong[OF refl o_apply]}], 88 rtac ctxt @{thm image_empty}]) 1; 89 90fun mk_comp_map_cong0_tac ctxt set'_eq_sets comp_set_alts map_cong0 map_cong0s = 91 let 92 val n = length comp_set_alts; 93 in 94 unfold_thms_tac ctxt set'_eq_sets THEN 95 (if n = 0 then rtac ctxt refl 1 96 else rtac ctxt map_cong0 1 THEN 97 EVERY' (map_index (fn (i, map_cong0) => 98 rtac ctxt map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) => 99 EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp, 100 rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans), 101 rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union), 102 rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, 103 REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}, 104 rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt]) 105 comp_set_alts)) 106 map_cong0s) 1) 107 end; 108 109fun mk_comp_bd_card_order_tac ctxt Fbd_card_orders Gbd_card_order = 110 rtac ctxt @{thm natLeq_card_order} 1 ORELSE 111 let 112 val (card_orders, last_card_order) = split_last Fbd_card_orders; 113 fun gen_before thm = rtac ctxt @{thm card_order_csum} THEN' rtac ctxt thm; 114 in 115 (rtac ctxt @{thm card_order_cprod} THEN' 116 WRAP' gen_before (K (K all_tac)) card_orders (rtac ctxt last_card_order) THEN' 117 rtac ctxt Gbd_card_order) 1 118 end; 119 120fun mk_comp_bd_cinfinite_tac ctxt Fbd_cinfinite Gbd_cinfinite = 121 (rtac ctxt @{thm natLeq_cinfinite} ORELSE' 122 rtac ctxt @{thm cinfinite_cprod} THEN' 123 ((K (TRY ((rtac ctxt @{thm cinfinite_csum} THEN' rtac ctxt disjI1) 1)) THEN' 124 ((rtac ctxt @{thm cinfinite_csum} THEN' rtac ctxt disjI1 THEN' rtac ctxt Fbd_cinfinite) ORELSE' 125 rtac ctxt Fbd_cinfinite)) ORELSE' 126 rtac ctxt Fbd_cinfinite) THEN' 127 rtac ctxt Gbd_cinfinite) 1; 128 129fun mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds = 130 let 131 val (bds, last_bd) = split_last Gset_Fset_bds; 132 fun gen_before bd = 133 rtac ctxt ctrans THEN' rtac ctxt @{thm Un_csum} THEN' 134 rtac ctxt ctrans THEN' rtac ctxt @{thm csum_mono} THEN' 135 rtac ctxt bd; 136 fun gen_after _ = rtac ctxt @{thm ordIso_imp_ordLeq} THEN' rtac ctxt @{thm cprod_csum_distrib1}; 137 in 138 (case bd_ordIso_natLeq_opt of 139 SOME thm => rtac ctxt (thm RSN (2, @{thm ordLeq_ordIso_trans})) 1 140 | NONE => all_tac) THEN 141 unfold_thms_tac ctxt [set'_eq_set, comp_set_alt] THEN 142 rtac ctxt @{thm comp_set_bd_Union_o_collect} 1 THEN 143 unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN 144 (rtac ctxt ctrans THEN' 145 WRAP' gen_before gen_after bds (rtac ctxt last_bd) THEN' 146 rtac ctxt @{thm ordIso_imp_ordLeq} THEN' 147 rtac ctxt @{thm cprod_com}) 1 148 end; 149 150val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert 151 UN_empty Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset 152 conj_assoc}; 153 154fun mk_comp_in_alt_tac ctxt comp_set_alts = 155 unfold_thms_tac ctxt comp_set_alts THEN 156 unfold_thms_tac ctxt comp_in_alt_thms THEN 157 unfold_thms_tac ctxt @{thms set_eq_subset} THEN 158 rtac ctxt conjI 1 THEN 159 REPEAT_DETERM ( 160 rtac ctxt @{thm subsetI} 1 THEN 161 unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN 162 (REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN 163 REPEAT_DETERM (CHANGED (( 164 (rtac ctxt conjI THEN' (assume_tac ctxt ORELSE' rtac ctxt subset_UNIV)) ORELSE' 165 assume_tac ctxt ORELSE' 166 (rtac ctxt subset_UNIV)) 1)) ORELSE rtac ctxt subset_UNIV 1)); 167 168val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right 169 Union_image_insert Union_image_empty}; 170 171fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms = 172 unfold_thms_tac ctxt set'_eq_sets THEN 173 ALLGOALS (dtac ctxt @{thm in_Union_o_assoc}) THEN 174 unfold_thms_tac ctxt [collect_set_map] THEN 175 unfold_thms_tac ctxt comp_wit_thms THEN 176 REPEAT_DETERM ((assume_tac ctxt ORELSE' 177 REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN' 178 etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN' 179 (etac ctxt FalseE ORELSE' 180 hyp_subst_tac ctxt THEN' 181 dresolve_tac ctxt Fwit_thms THEN' 182 (etac ctxt FalseE ORELSE' assume_tac ctxt))) 1); 183 184 185(* Kill operation *) 186 187fun mk_kill_map_cong0_tac ctxt n m map_cong0 = 188 (rtac ctxt map_cong0 THEN' EVERY' (replicate n (rtac ctxt refl)) THEN' 189 EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1; 190 191fun kill_in_alt_tac ctxt = 192 ((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN 193 REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN 194 REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' 195 rtac ctxt conjI THEN' rtac ctxt subset_UNIV) 1)) THEN 196 (rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN 197 REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN 198 REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE 199 ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN 200 REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1)); 201 202 203(* Lift operation *) 204 205fun empty_natural_tac ctxt = rtac ctxt @{thm empty_natural} 1; 206 207fun mk_lift_set_bd_tac ctxt bd_Card_order = 208 (rtac ctxt @{thm Card_order_empty} THEN' rtac ctxt bd_Card_order) 1; 209 210fun lift_in_alt_tac ctxt = 211 ((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN 212 REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN 213 REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1)) THEN 214 REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN 215 REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' 216 rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN 217 (rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE 218 ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN 219 REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1)); 220 221 222(* Permute operation *) 223 224fun mk_permute_in_alt_tac ctxt src dest = 225 (rtac ctxt @{thm Collect_cong} THEN' 226 mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute} 227 @{thm conj_cong} dest src) 1; 228 229 230(* Miscellaneous *) 231 232fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs = 233 HEADGOAL (EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: 234 inner_le_rel_OOs))); 235 236fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm = 237 HEADGOAL (rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym])); 238 239fun mk_simple_pred_set_tac ctxt pred_set in_alt_thm = 240 HEADGOAL (rtac ctxt (pred_set RS trans)) THEN 241 unfold_thms_tac ctxt @{thms Ball_Collect UNIV_def} THEN 242 HEADGOAL (rtac ctxt (unfold_thms ctxt @{thms UNIV_def} in_alt_thm RS @{thm Collect_inj} RS sym)); 243 244fun mk_simple_wit_tac ctxt wit_thms = 245 ALLGOALS (assume_tac ctxt ORELSE' eresolve_tac ctxt (@{thm emptyE} :: wit_thms)); 246 247val csum_thms = 248 @{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]}; 249val cprod_thms = 250 @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]}; 251 252val simplified_set_simps = 253 @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left 254 o_def Union_Un_distrib UN_empty2 UN_singleton id_bnf_def}; 255 256fun mk_simplified_set_tac ctxt collect_set_map = 257 unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN 258 unfold_thms_tac ctxt simplified_set_simps THEN rtac ctxt refl 1; 259 260fun bd_ordIso_natLeq_tac ctxt = 261 HEADGOAL (REPEAT_DETERM o resolve_tac ctxt 262 (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms)); 263 264end; 265