1(* Title: HOL/Tools/BNF/bnf_def_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Author: Martin Desharnais, TU Muenchen 5 Author: Ondrej Kuncar, TU Muenchen 6 Copyright 2012, 2013, 2014, 2015 7 8Tactics for definition of bounded natural functors. 9*) 10 11signature BNF_DEF_TACTICS = 12sig 13 val mk_collect_set_map_tac: Proof.context -> thm list -> tactic 14 val mk_in_mono_tac: Proof.context -> int -> tactic 15 val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic 16 val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic 17 val mk_map_id: thm -> thm 18 val mk_map_ident: Proof.context -> thm -> thm 19 val mk_map_comp: thm -> thm 20 val mk_map_cong_tac: Proof.context -> thm -> tactic 21 val mk_set_map: thm -> thm 22 23 val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic 24 val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic 25 val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic 26 val mk_rel_conversep_tac: Proof.context -> thm -> thm -> tactic 27 val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic 28 val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic 29 val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic 30 val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic 31 val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic 32 val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic 33 val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic 34 val mk_pred_mono_tac: Proof.context -> thm -> thm -> tactic 35 36 val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic 37 val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic 38 val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic 39 val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic 40 41 val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list -> 42 thm -> thm -> thm -> thm -> tactic 43 44 val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic 45end; 46 47structure BNF_Def_Tactics : BNF_DEF_TACTICS = 48struct 49 50open BNF_Util 51open BNF_Tactics 52 53val ord_eq_le_trans = @{thm ord_eq_le_trans}; 54val ord_le_eq_trans = @{thm ord_le_eq_trans}; 55val conversep_shift = @{thm conversep_le_swap} RS iffD1; 56 57fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; 58fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def}; 59fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; 60fun mk_map_cong_tac ctxt cong0 = 61 (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN' 62 REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1; 63fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; 64 65fun mk_in_mono_tac ctxt n = 66 if n = 0 then rtac ctxt subset_UNIV 1 67 else 68 (rtac ctxt @{thm subsetI} THEN' rtac ctxt @{thm CollectI}) 1 THEN 69 REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN 70 REPEAT_DETERM_N (n - 1) 71 ((rtac ctxt conjI THEN' etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1) THEN 72 (etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1; 73 74fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong = 75 let 76 val map_cong' = map_cong OF (asm_rl :: replicate n refl); 77 val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id}); 78 in 79 HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN' 80 REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN' 81 REPEAT_DETERM_N n o assume_tac ctxt)) 82 end; 83 84fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong = 85 let 86 val rel_eq' = rel_eq RS @{thm predicate2_eqD}; 87 val rel_maps' = map (fn thm => thm RS iffD1) rel_maps; 88 in 89 HEADGOAL (dtac ctxt (rel_eq' RS iffD2) THEN' rtac ctxt (rel_eq' RS iffD1)) THEN 90 EVERY (map (HEADGOAL o dtac ctxt) rel_maps') THEN 91 HEADGOAL (etac ctxt rel_mono_strong) THEN 92 TRYALL (Goal.assume_rule_tac ctxt) 93 end; 94 95fun mk_collect_set_map_tac ctxt set_map0s = 96 (rtac ctxt (@{thm collect_comp} RS trans) THEN' rtac ctxt @{thm arg_cong[of _ _ collect]} THEN' 97 EVERY' (map (fn set_map0 => 98 rtac ctxt (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' 99 rtac ctxt set_map0) set_map0s) THEN' 100 rtac ctxt @{thm image_empty}) 1; 101 102fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps = 103 let 104 val n = length set_maps; 105 val rel_OO_Grps_tac = 106 if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans); 107 in 108 if null set_maps then 109 unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN 110 resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1 111 else 112 EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I}, 113 REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE}, 114 hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, 115 rtac ctxt map_cong0, 116 REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, 117 etac ctxt @{thm set_mp}, assume_tac ctxt], 118 rtac ctxt @{thm CollectI}, 119 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), 120 rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in}, 121 etac ctxt @{thm set_mp}, assume_tac ctxt]) 122 set_maps, 123 rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE], 124 hyp_subst_tac ctxt, 125 rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, 126 EVERY' (map2 (fn convol => fn map_id0 => 127 EVERY' [rtac ctxt @{thm GrpI}, 128 rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]), 129 REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong), 130 REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, 131 rtac ctxt @{thm CollectI}, 132 CONJ_WRAP' (fn thm => 133 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI}, 134 rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt]) 135 set_maps]) 136 @{thms fst_convol snd_convol} [map_id, refl])] 1 137 end; 138 139fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 = 140 (EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN' 141 rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN' 142 (if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl 143 else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]}, 144 rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, 145 rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI}, 146 CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1; 147 148fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id = 149 if live = 0 then 150 HEADGOAL (Goal.conjunction_tac) THEN 151 unfold_thms_tac ctxt @{thms id_apply} THEN 152 ALLGOALS (rtac ctxt refl) 153 else 154 let 155 val ks = 1 upto live; 156 in 157 Goal.conjunction_tac 1 THEN 158 unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN 159 TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI}, 160 resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI}, 161 CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, 162 assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, 163 resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI}, 164 CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, 165 REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE}, 166 dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt]) 167 end; 168 169fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono = 170 let 171 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac 172 else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' 173 rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans)); 174 in 175 EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]}, 176 rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}, 177 rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1 178 end; 179 180fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = 181 let 182 val n = length set_maps; 183 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac 184 else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' 185 rtac ctxt (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); 186 in 187 if null set_maps then rtac ctxt (rel_eq RS @{thm leq_conversepI}) 1 188 else 189 EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I}, 190 REPEAT_DETERM o 191 eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE}, 192 hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, 193 EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans, 194 rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm, 195 rtac ctxt (map_comp RS sym), rtac ctxt @{thm CollectI}, 196 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), 197 etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 198 end; 199 200fun mk_rel_conversep_tac ctxt le_conversep rel_mono = 201 EVERY' [rtac ctxt @{thm antisym}, rtac ctxt le_conversep, rtac ctxt @{thm xt1(6)}, rtac ctxt conversep_shift, 202 rtac ctxt le_conversep, rtac ctxt @{thm iffD2[OF conversep_mono]}, rtac ctxt rel_mono, 203 REPEAT_DETERM o rtac ctxt @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; 204 205fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps = 206 let 207 val n = length set_maps; 208 fun in_tac nthO_in = rtac ctxt @{thm CollectI} THEN' 209 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), 210 rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps; 211 val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac 212 else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN' 213 rtac ctxt (@{thm arg_cong2[of _ _ _ _ "(OO)"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN 214 (2, ord_le_eq_trans)); 215 in 216 if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1 217 else 218 EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I}, 219 REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE}, 220 hyp_subst_tac ctxt, 221 rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, 222 rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0, 223 REPEAT_DETERM_N n o rtac ctxt @{thm fst_fstOp}, 224 in_tac @{thm fstOp_in}, 225 rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0, 226 REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply, 227 rtac ctxt @{thm ballE}, rtac ctxt subst, 228 rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt, 229 etac ctxt notE, etac ctxt set_mp, assume_tac ctxt], 230 in_tac @{thm fstOp_in}, 231 rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, 232 rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0, 233 REPEAT_DETERM_N n o rtac ctxt o_apply, 234 in_tac @{thm sndOp_in}, 235 rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0, 236 REPEAT_DETERM_N n o rtac ctxt @{thm snd_sndOp}, 237 in_tac @{thm sndOp_in}] 1 238 end; 239 240fun mk_rel_mono_strong0_tac ctxt in_rel set_maps = 241 if null set_maps then assume_tac ctxt 1 242 else 243 unfold_tac ctxt [in_rel] THEN 244 REPEAT_DETERM (eresolve_tac ctxt @{thms exE CollectE conjE} 1) THEN 245 hyp_subst_tac ctxt 1 THEN 246 EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]}, 247 CONJ_WRAP' (fn thm => 248 (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt)) 249 set_maps] 1; 250 251fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong = 252 let 253 fun last_tac iffD = 254 HEADGOAL (etac ctxt rel_mono_strong) THEN 255 REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN' 256 REPEAT_DETERM o assume_tac ctxt)); 257 in 258 REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 259 (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE 260 REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) :: 261 @{thms exE conjE CollectE}))) THEN 262 HEADGOAL (hyp_subst_tac ctxt) THEN 263 REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm => 264 [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN 265 HEADGOAL (rtac ctxt iffI) THEN 266 last_tac iffD1 THEN last_tac iffD2) 267 end; 268 269fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp = 270 let 271 val n = length set_maps; 272 val in_tac = 273 if n = 0 then rtac ctxt @{thm UNIV_I} 274 else 275 rtac ctxt @{thm CollectI} THEN' CONJ_WRAP' (fn thm => 276 etac ctxt (thm RS 277 @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) 278 set_maps; 279 in 280 REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN 281 unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN 282 HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono, 283 REPEAT_DETERM_N n o assume_tac ctxt, 284 rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1), 285 REPEAT_DETERM o eresolve_tac ctxt @{thms exE CollectE conjE}, hyp_subst_tac ctxt, 286 rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac, 287 rtac ctxt conjI, 288 EVERY' (map (fn convol => 289 rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN' 290 REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong)) @{thms fst_convol snd_convol})]) 291 end; 292 293fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds 294 bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero = 295 if live = 0 then 296 rtac ctxt @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order] 297 ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1 298 else 299 let 300 val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1}; 301 val inserts = 302 map (fn set_bd => 303 iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF 304 [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]]) 305 set_bds; 306 in 307 EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt @{thm cprod_cinfinite_bound}, 308 rtac ctxt (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac ctxt @{thm card_of_Card_order}, 309 rtac ctxt @{thm ordLeq_csum2}, rtac ctxt @{thm Card_order_ctwo}, rtac ctxt @{thm Card_order_csum}, 310 rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, 311 if live = 1 then rtac ctxt @{thm ordIso_refl[OF Card_order_csum]} 312 else 313 REPEAT_DETERM_N (live - 2) o rtac ctxt @{thm ordIso_transitive[OF csum_cong2]} THEN' 314 REPEAT_DETERM_N (live - 1) o rtac ctxt @{thm csum_csum}, 315 rtac ctxt bd_Card_order, rtac ctxt (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac ctxt @{thm ordLeq_csum1}, 316 rtac ctxt bd_Card_order, rtac ctxt @{thm Card_order_csum}, rtac ctxt bd_Cnotzero, 317 rtac ctxt @{thm csum_Cfinite_cexp_Cinfinite}, 318 rtac ctxt (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}), 319 CONJ_WRAP_GEN' (rtac ctxt @{thm Cfinite_csum}) (K (rtac ctxt @{thm Cfinite_cone})) set_maps, 320 rtac ctxt bd'_Cinfinite, rtac ctxt @{thm card_of_Card_order}, 321 rtac ctxt @{thm Card_order_cexp}, rtac ctxt @{thm Cinfinite_cexp}, rtac ctxt @{thm ordLeq_csum2}, 322 rtac ctxt @{thm Card_order_ctwo}, rtac ctxt bd'_Cinfinite, 323 rtac ctxt (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))), 324 REPEAT_DETERM_N (live - 1) o 325 (rtac ctxt (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN' 326 rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}), 327 rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN 328 unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN 329 unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN 330 EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, 331 rtac ctxt @{thm subsetI}, 332 Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec, 333 REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], 334 etac ctxt @{thm CollectE}, 335 if live = 1 then K all_tac 336 else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE, 337 rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I}, 338 CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI}) 339 (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps, 340 rtac ctxt sym, 341 rtac ctxt (Drule.rotate_prems 1 342 ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f}, 343 map_comp RS sym, map_id]) RSN (2, trans))), 344 REPEAT_DETERM_N (2 * live) o assume_tac ctxt, 345 REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans), 346 rtac ctxt refl, 347 rtac ctxt @{thm surj_imp_ordLeq}, 348 rtac ctxt @{thm subsetI}, 349 rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), 350 REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI}, 351 CONJ_WRAP' (fn thm => 352 rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]}) 353 set_maps, 354 rtac ctxt sym, 355 rtac ctxt (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]}, 356 map_comp RS sym, map_id])] 1 357 end; 358 359fun mk_trivial_wit_tac ctxt wit_defs set_maps = 360 unfold_thms_tac ctxt wit_defs THEN 361 HEADGOAL (EVERY' (map (fn thm => 362 dtac ctxt (thm RS @{thm equalityD1} RS set_mp) THEN' 363 etac ctxt @{thm imageE} THEN' assume_tac ctxt) set_maps)) THEN 364 ALLGOALS (assume_tac ctxt); 365 366fun mk_set_transfer_tac ctxt in_rel set_maps = 367 Goal.conjunction_tac 1 THEN 368 EVERY (map (fn set_map => HEADGOAL (rtac ctxt rel_funI) THEN 369 REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) :: 370 @{thms exE conjE CollectE}))) THEN 371 HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN' 372 rtac ctxt @{thm rel_setI}) THEN 373 REPEAT (HEADGOAL (etac ctxt @{thm imageE} THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN' 374 REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN' 375 rtac ctxt @{thm bexI} THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt @{thm imageI}))) 376 set_maps); 377 378fun mk_rel_cong_tac ctxt (eqs, prems) mono = 379 let 380 fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt; 381 fun mk_tacs iffD = etac ctxt mono :: 382 map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD) 383 |> Drule.rotate_prems ~1 |> mk_tac) prems; 384 in 385 unfold_thms_tac ctxt eqs THEN 386 HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2)) 387 end; 388 389fun subst_conv ctxt thm = 390 Conv.arg_conv (Conv.arg_conv 391 (Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) ctxt)); 392 393fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp = 394 HEADGOAL (EVERY' 395 [SELECT_GOAL (unfold_thms_tac ctxt (pred_def :: @{thms UNIV_def eq_onp_Grp Ball_Collect})), 396 CONVERSION (subst_conv ctxt (map_id0 RS sym)), 397 rtac ctxt (unfold_thms ctxt @{thms UNIV_def} rel_Grp)]); 398 399fun mk_pred_mono_strong0_tac ctxt pred_rel rel_mono_strong0 = 400 unfold_thms_tac ctxt [pred_rel] THEN 401 HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0}); 402 403fun mk_pred_mono_tac ctxt rel_eq_onp rel_mono = 404 unfold_thms_tac ctxt (map mk_sym [@{thm eq_onp_mono_iff}, rel_eq_onp]) THEN 405 HEADGOAL (rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt); 406 407fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong = 408 HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1), 409 REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt, 410 rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]), 411 rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o 412 (etac ctxt @{thm rel_fun_Collect_case_prodD[where B="(=)"]} THEN_ALL_NEW assume_tac ctxt)]); 413 414end; 415