1(* Title: HOL/Tools/BNF/bnf_lfp_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Andrei Popescu, TU Muenchen 4 Copyright 2012 5 6Tactics for the datatype construction. 7*) 8 9signature BNF_LFP_TACTICS = 10sig 11 val mk_alg_min_alg_tac: Proof.context -> int -> thm -> thm list -> thm -> thm -> thm list list -> 12 thm list -> thm list -> tactic 13 val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic 14 val mk_alg_select_tac: Proof.context -> thm -> tactic 15 val mk_alg_set_tac: Proof.context -> thm -> tactic 16 val mk_bd_card_order_tac: Proof.context -> thm list -> tactic 17 val mk_bd_limit_tac: Proof.context -> int -> thm -> tactic 18 val mk_card_of_min_alg_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> tactic 19 val mk_copy_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list list -> tactic 20 val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm -> 21 thm list -> thm list -> thm list -> tactic 22 val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm -> 23 thm list -> tactic 24 val mk_ctor_set_tac: Proof.context -> thm -> thm -> thm list -> tactic 25 val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> 26 thm list -> tactic 27 val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> 28 thm -> thm -> thm list -> thm list -> thm list list -> tactic 29 val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic 30 val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm -> 31 tactic 32 val mk_init_induct_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> tactic 33 val mk_init_unique_mor_tac: Proof.context -> cterm list -> int -> thm -> thm -> thm list -> 34 thm list -> thm list -> thm list -> thm list -> tactic 35 val mk_fold_unique_mor_tac: Proof.context -> thm list -> thm list -> thm list -> thm -> thm -> 36 thm -> tactic 37 val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic 38 val mk_least_min_alg_tac: Proof.context -> thm -> thm -> tactic 39 val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> 40 thm list -> tactic 41 val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> int -> tactic 42 val mk_map_id0_tac: Proof.context -> thm list -> thm -> tactic 43 val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> tactic 44 val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic 45 val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list -> 46 thm list -> tactic 47 val mk_min_algs_card_of_tac: Proof.context -> ctyp -> cterm -> int -> thm -> thm list -> 48 thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic 49 val mk_min_algs_least_tac: Proof.context -> ctyp -> cterm -> thm -> thm list -> thm list -> tactic 50 val mk_min_algs_mono_tac: Proof.context -> thm -> tactic 51 val mk_min_algs_tac: Proof.context -> thm -> thm list -> tactic 52 val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list -> 53 tactic 54 val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list -> 55 thm list list -> tactic 56 val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic 57 val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic 58 val mk_mor_elim_tac: Proof.context -> thm -> tactic 59 val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic 60 val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic 61 val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> 62 thm list list -> thm list -> tactic 63 val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic 64 val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list -> 65 thm list -> tactic 66 val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic 67 val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic 68 val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list -> 69 int -> tactic 70 val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list -> 71 cterm list -> thm list -> int -> tactic 72 val mk_set_map0_tac: Proof.context -> thm -> tactic 73 val mk_set_tac: Proof.context -> thm -> tactic 74 val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic 75end; 76 77structure BNF_LFP_Tactics : BNF_LFP_TACTICS = 78struct 79 80open BNF_Tactics 81open BNF_LFP_Util 82open BNF_Util 83 84val fst_snd_convs = @{thms fst_conv snd_conv}; 85val ord_eq_le_trans = @{thm ord_eq_le_trans}; 86val subset_trans = @{thm subset_trans}; 87val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; 88val rev_bspec = Drule.rotate_prems 1 bspec; 89val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]}; 90val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]}; 91 92fun mk_alg_set_tac ctxt alg_def = 93 EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI, 94 REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1; 95 96fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits = 97 (EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN' 98 REPEAT_DETERM o FIRST' 99 [EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits], 100 EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits], 101 EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt, 102 FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN' 103 etac ctxt @{thm emptyE}) 1; 104 105fun mk_mor_elim_tac ctxt mor_def = 106 (dtac ctxt (mor_def RS iffD1) THEN' 107 REPEAT o etac ctxt conjE THEN' 108 TRY o rtac ctxt @{thm image_subsetI} THEN' 109 etac ctxt bspec THEN' 110 assume_tac ctxt) 1; 111 112fun mk_mor_incl_tac ctxt mor_def map_ids = 113 (rtac ctxt (mor_def RS iffD2) THEN' 114 rtac ctxt conjI THEN' 115 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})])) 116 map_ids THEN' 117 CONJ_WRAP' (fn thm => 118 (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1; 119 120fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids = 121 let 122 val fbetw_tac = 123 EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), 124 etac ctxt bspec, etac ctxt bspec, assume_tac ctxt]; 125 fun mor_tac (set_map, map_comp_id) = 126 EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans, 127 rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong, 128 REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN' 129 CONJ_WRAP' (fn thm => 130 FIRST' [rtac ctxt subset_UNIV, 131 (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI}, 132 etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN' 133 rtac ctxt (map_comp_id RS arg_cong); 134 in 135 (dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN' 136 REPEAT o etac ctxt conjE THEN' 137 rtac ctxt conjI THEN' 138 CONJ_WRAP' (K fbetw_tac) set_maps THEN' 139 CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1 140 end; 141 142fun mk_mor_str_tac ctxt ks mor_def = 143 (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' 144 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN' 145 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1; 146 147fun mk_mor_UNIV_tac ctxt m morEs mor_def = 148 let 149 val n = length morEs; 150 fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, 151 rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n), 152 rtac ctxt sym, rtac ctxt o_apply]; 153 in 154 EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs, 155 rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs, 156 REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1), 157 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans, 158 etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1 159 end; 160 161fun mk_copy_tac ctxt m alg_def mor_def alg_sets set_mapss = 162 let 163 val n = length alg_sets; 164 fun set_tac thm = 165 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono}, 166 rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}]; 167 val alg_tac = 168 CONJ_WRAP' (fn (set_maps, alg_set) => 169 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp, 170 rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]}, 171 rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))]) 172 (set_mapss ~~ alg_sets); 173 174 val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN' 175 CONJ_WRAP' (fn (set_maps, alg_set) => 176 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 177 etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set, 178 EVERY' (map set_tac (drop m set_maps))]) 179 (set_mapss ~~ alg_sets); 180 in 181 (REPEAT_DETERM_N n o rtac ctxt exI THEN' rtac ctxt conjI THEN' 182 rtac ctxt (alg_def RS iffD2) THEN' alg_tac THEN' rtac ctxt (mor_def RS iffD2) THEN' mor_tac) 1 183 end; 184 185fun mk_bd_limit_tac ctxt n bd_Cinfinite = 186 EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite}, 187 REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI}, 188 REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI}, 189 rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI, 190 CONJ_WRAP' (fn i => 191 EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}]) 192 (0 upto n - 1), 193 assume_tac ctxt] 1; 194 195fun mk_min_algs_tac ctxt worel in_congs = 196 let 197 val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec, 198 assume_tac ctxt, etac ctxt arg_cong]; 199 fun minH_tac thm = 200 EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm, 201 REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl]; 202 in 203 (rtac ctxt (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ctxt iffD2 THEN' 204 rtac ctxt meta_eq_to_obj_eq THEN' rtac ctxt (worel RS @{thm wo_rel.adm_wo_def}) THEN' 205 REPEAT_DETERM_N 3 o rtac ctxt allI THEN' rtac ctxt impI THEN' 206 CONJ_WRAP_GEN' (EVERY' [rtac ctxt prod_injectI, rtac ctxt conjI]) minH_tac in_congs) 1 207 end; 208 209fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 210 rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI, 211 rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt, 212 assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD}, 213 hyp_subst_tac ctxt, rtac ctxt refl] 1; 214 215fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero 216 suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite = 217 let 218 val induct = worel RS 219 Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; 220 val src = 1 upto m + 1; 221 val dest = (m + 1) :: (1 upto m); 222 val absorbAs_tac = if m = 0 then K (all_tac) 223 else EVERY' [rtac ctxt @{thm ordIso_transitive}, rtac ctxt @{thm csum_cong1}, 224 rtac ctxt @{thm ordIso_transitive}, 225 BNF_Tactics.mk_rotate_eq_tac ctxt (rtac ctxt @{thm ordIso_refl} THEN' 226 FIRST' [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, 227 rtac ctxt @{thm Card_order_cexp}]) 228 @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} 229 src dest, 230 rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt ctrans, rtac ctxt @{thm ordLeq_csum1}, 231 FIRST' [rtac ctxt @{thm Card_order_csum}, rtac ctxt @{thm card_of_Card_order}], 232 rtac ctxt @{thm ordLeq_cexp1}, rtac ctxt suc_Cnotzero, rtac ctxt @{thm Card_order_csum}]; 233 234 val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq}, 235 rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order, 236 assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE, 237 dtac ctxt mp, etac ctxt @{thm underS_E}, 238 dtac ctxt mp, etac ctxt @{thm underS_Field}, 239 REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 240 241 fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, 242 rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound}, 243 minG_tac, rtac ctxt ctrans, rtac ctxt @{thm card_of_image}, rtac ctxt ctrans, rtac ctxt in_bd, rtac ctxt ctrans, 244 rtac ctxt @{thm cexp_mono1}, rtac ctxt @{thm csum_mono1}, 245 REPEAT_DETERM_N m o rtac ctxt @{thm csum_mono2}, 246 CONJ_WRAP_GEN' (rtac ctxt @{thm csum_cinfinite_bound}) (K minG_tac) min_algs, 247 REPEAT_DETERM o FIRST' 248 [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum}, 249 rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order], 250 rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, absorbAs_tac, 251 rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite}, 252 rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order, 253 rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq}, 254 resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite, 255 rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite]; 256 in 257 (rtac ctxt induct THEN' 258 rtac ctxt impI THEN' 259 CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1 260 end; 261 262fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets = 263 let 264 val induct = worel RS 265 Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp}; 266 267 val minG_tac = 268 EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E}, 269 dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]; 270 271 fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg, 272 rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI}, 273 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set, 274 REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)]; 275 in 276 (rtac ctxt induct THEN' 277 rtac ctxt impI THEN' 278 CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1 279 end; 280 281fun mk_alg_min_alg_tac ctxt m alg_def min_alg_defs bd_limit bd_Cinfinite 282 set_bdss min_algs min_alg_monos = 283 let 284 val n = length min_algs; 285 fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY' 286 [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono, 287 etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds]; 288 fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) = 289 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 290 EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE, 291 rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt, 292 rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}), 293 rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl, 294 assume_tac ctxt, rtac ctxt set_mp, 295 rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2, 296 rtac ctxt @{thm image_eqI}, rtac ctxt refl, 297 rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl, 298 REPEAT_DETERM o etac ctxt conjE, 299 CONJ_WRAP' (K (FIRST' [assume_tac ctxt, 300 EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I}, 301 etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]])) 302 set_bds]; 303 in 304 (rtac ctxt (alg_def RS iffD2) THEN' 305 CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1 306 end; 307 308fun mk_card_of_min_alg_tac ctxt min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite = 309 EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}), 310 rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans}, 311 rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq}, 312 rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of, 313 REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1; 314 315fun mk_least_min_alg_tac ctxt min_alg_def least = 316 EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least}, 317 dtac ctxt least, dtac ctxt mp, assume_tac ctxt, 318 REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1; 319 320fun mk_alg_select_tac ctxt Abs_inverse = 321 EVERY' [rtac ctxt ballI, 322 REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN 323 unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1; 324 325fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets 326 set_maps str_init_defs = 327 let 328 val n = length alg_sets; 329 val fbetw_tac = 330 CONJ_WRAP' 331 (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec, 332 etac ctxt CollectE, assume_tac ctxt])) alg_sets; 333 val mor_tac = 334 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs; 335 fun alg_epi_tac ((alg_set, str_init_def), set_map) = 336 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI, 337 rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec], 338 rtac ctxt (str_init_def RS @{thm ssubst_mem}), 339 etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map, 340 rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec, 341 assume_tac ctxt]]; 342 in 343 EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}), 344 rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp), 345 rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, fbetw_tac, mor_tac, rtac ctxt mor_incl_min_alg, 346 rtac ctxt (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1 347 end; 348 349fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl = 350 let 351 val n = length card_of_min_algs; 352 in 353 EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs), 354 REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, 355 rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt, 356 rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI, 357 rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, 358 rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt, 359 SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)), 360 etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1 361 end; 362 363fun mk_init_unique_mor_tac ctxt cts m 364 alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s = 365 let 366 val n = length least_min_algs; 367 val ks = (1 upto n); 368 369 fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono, 370 REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI, 371 REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)]; 372 fun cong_tac ct map_cong0 = EVERY' 373 [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong), 374 REPEAT_DETERM_N m o rtac ctxt refl, 375 REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)]; 376 377 fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) = 378 EVERY' [rtac ctxt ballI, rtac ctxt CollectI, 379 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), 380 REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), 381 rtac ctxt trans, mor_tac morE in_mono, 382 rtac ctxt trans, cong_tac ct map_cong0, 383 rtac ctxt sym, mor_tac morE in_mono]; 384 385 fun mk_unique_tac (k, least_min_alg) = 386 select_prem_tac ctxt n (etac ctxt @{thm prop_restrict}) k THEN' rtac ctxt least_min_alg THEN' 387 rtac ctxt (alg_def RS iffD2) THEN' 388 CONJ_WRAP' mk_alg_tac (cts ~~ (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)))); 389 in 390 CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1 391 end; 392 393fun mk_init_induct_tac ctxt m alg_def alg_min_alg least_min_algs alg_sets = 394 let 395 val n = length least_min_algs; 396 397 fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI, 398 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set), 399 REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}), 400 rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI, 401 REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt), 402 CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets, 403 CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)) 404 alg_sets]; 405 406 fun mk_induct_tac least_min_alg = 407 rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN' 408 rtac ctxt (alg_def RS iffD2) THEN' 409 CONJ_WRAP' mk_alg_tac alg_sets; 410 in 411 CONJ_WRAP' mk_induct_tac least_min_algs 1 412 end; 413 414fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss = 415 unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN 416 EVERY' [rtac ctxt conjI, 417 CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps, 418 CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) => 419 EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set), 420 EVERY' (map2 (fn Rep => fn set_map => 421 EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep]) 422 Reps (drop m set_maps))]) 423 (Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1; 424 425fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs = 426 unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN 427 EVERY' [rtac ctxt conjI, 428 CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses, 429 CONJ_WRAP' (fn (ct, thm) => 430 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 431 rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym), 432 EVERY' (map (fn Abs_inverse => 433 EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse), 434 assume_tac ctxt]) 435 Abs_inverses)]) 436 (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1; 437 438fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor = 439 (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN' 440 REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN' 441 rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1; 442 443fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold = 444 let 445 fun mk_unique type_def = 446 EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}), 447 rtac ctxt ballI, resolve_tac ctxt init_unique_mors, 448 EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps), 449 rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt, 450 rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold]; 451 in 452 CONJ_WRAP' mk_unique type_defs 1 453 end; 454 455fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds = 456 EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans), 457 rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L, 458 EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) 459 ctor_o_folds), 460 rtac ctxt sym, rtac ctxt id_apply] 1; 461 462fun mk_rec_tac ctxt rec_defs foldx fst_recs = 463 unfold_thms_tac ctxt 464 (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN 465 EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt (foldx RS @{thm arg_cong[of _ _ snd]}), 466 rtac ctxt @{thm snd_convol'}] 1; 467 468fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor = 469 unfold_thms_tac ctxt 470 (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN 471 etac ctxt fold_unique_mor 1; 472 473fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = 474 let 475 val n = length set_mapss; 476 val ks = 1 upto n; 477 478 fun mk_IH_tac Rep_inv Abs_inv set_map = 479 DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec, 480 dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE, 481 hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp, 482 assume_tac ctxt, assume_tac ctxt]; 483 484 fun mk_closed_tac (k, (morE, set_maps)) = 485 EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI, 486 rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt, 487 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec}, 488 EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt]; 489 490 fun mk_induct_tac (Rep, Rep_inv) = 491 EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))]; 492 in 493 (rtac ctxt mp THEN' rtac ctxt impI THEN' 494 DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' 495 rtac ctxt init_induct THEN' 496 DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1 497 end; 498 499fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts = 500 let 501 val n = length weak_ctor_inducts; 502 val ks = 1 upto n; 503 fun mk_inner_induct_tac induct i = 504 EVERY' [rtac ctxt allI, fo_rtac ctxt induct, 505 select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i, 506 REPEAT_DETERM_N n o 507 EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt, 508 REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp), 509 assume_tac ctxt], 510 assume_tac ctxt]; 511 in 512 EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct), 513 EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI, 514 REPEAT_DETERM o eresolve_tac ctxt [conjE, allE], 515 CONJ_WRAP' (K (assume_tac ctxt)) ks] 1 516 end; 517 518fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 = 519 EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, 520 rtac ctxt o_apply, 521 rtac ctxt trans, rtac ctxt (map_comp_id RS arg_cong), rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong), 522 REPEAT_DETERM_N m o rtac ctxt refl, 523 REPEAT_DETERM_N n o (EVERY' (map (rtac ctxt) [trans, o_apply, id_apply])), 524 rtac ctxt sym, rtac ctxt o_apply] 1; 525 526fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps = 527 rtac ctxt fold_unique 1 THEN 528 unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN 529 ALLGOALS (assume_tac ctxt); 530 531fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, 532 rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1; 533 534fun mk_ctor_set_tac ctxt set set_map set_maps = 535 let 536 val n = length set_maps; 537 fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) 538 THEN' rtac ctxt @{thm refl}; 539 in 540 EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong, 541 rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]), 542 REPEAT_DETERM_N (n - 1) o rtac ctxt Un_cong, 543 EVERY' (map mk_UN set_maps)] 1 544 end; 545 546fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i = 547 let 548 val n = length ctor_maps; 549 550 fun useIH set_nat = EVERY' [rtac ctxt trans, rtac ctxt @{thm image_UN}, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, 551 rtac ctxt refl, Goal.assume_rule_tac ctxt, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm SUP_cong}, 552 rtac ctxt set_nat, rtac ctxt refl, rtac ctxt @{thm UN_simps(10)}]; 553 554 fun mk_set_nat cset ctor_map ctor_set set_nats = 555 EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym, 556 rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong, 557 ctor_set RS trans]), 558 rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]), 559 rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)), 560 REPEAT_DETERM_N (n - 1) o EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]), 561 EVERY' (map useIH (drop m set_nats))]; 562 in 563 (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 564 end; 565 566fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = 567 let 568 val n = length ctor_sets; 569 570 fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI, 571 Goal.assume_rule_tac ctxt, rtac ctxt bd_Cinfinite]; 572 573 fun mk_set_nat ctor_set set_bds = 574 EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set, 575 rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i - 1)), 576 REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), 577 EVERY' (map useIH (drop m set_bds))]; 578 in 579 (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1 580 end; 581 582fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps = 583 let 584 fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm]; 585 586 fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt, 587 CONJ_WRAP' (fn thm => 588 EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets]; 589 590 fun mk_map_cong0 ctor_map map_cong0 set_setss = 591 EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE, 592 rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong), 593 EVERY' (map use_asm (map hd set_setss)), 594 EVERY' (map useIH (transpose (map tl set_setss))), 595 rtac ctxt sym, rtac ctxt ctor_map]; 596 in 597 (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 598 end; 599 600fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = 601 EVERY' (rtac ctxt induct :: 602 @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => 603 EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}), 604 REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2), 605 rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}), 606 rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt, 607 REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt], 608 REPEAT_DETERM_N (length le_rel_OOs) o 609 EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]]) 610 ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1; 611 612(* BNF tactics *) 613 614fun mk_map_id0_tac ctxt map_id0s unique = 615 (rtac ctxt sym THEN' rtac ctxt unique THEN' 616 EVERY' (map (fn thm => 617 EVERY' [rtac ctxt trans, rtac ctxt @{thm id_comp}, rtac ctxt trans, rtac ctxt sym, rtac ctxt @{thm comp_id}, 618 rtac ctxt (thm RS sym RS arg_cong)]) map_id0s)) 1; 619 620fun mk_map_comp0_tac ctxt map_comp0s ctor_maps unique iplus1 = 621 let 622 val i = iplus1 - 1; 623 val unique' = Thm.permute_prems 0 i unique; 624 val map_comp0s' = drop i map_comp0s @ take i map_comp0s; 625 val ctor_maps' = drop i ctor_maps @ take i ctor_maps; 626 fun mk_comp comp simp = 627 EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt o_apply, 628 rtac ctxt trans, rtac ctxt (simp RS arg_cong), rtac ctxt trans, rtac ctxt simp, 629 rtac ctxt trans, rtac ctxt (comp RS arg_cong), rtac ctxt sym, rtac ctxt o_apply]; 630 in 631 (rtac ctxt sym THEN' rtac ctxt unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 632 end; 633 634fun mk_set_map0_tac ctxt set_nat = 635 EVERY' (map (rtac ctxt) [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1; 636 637fun mk_bd_card_order_tac ctxt bd_card_orders = 638 CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1; 639 640fun mk_wit_tac ctxt n ctor_set wit = 641 REPEAT_DETERM (assume_tac ctxt 1 ORELSE 642 EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set, 643 REPEAT_DETERM o 644 (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN' 645 (eresolve_tac ctxt wit ORELSE' 646 (dresolve_tac ctxt wit THEN' 647 (etac ctxt FalseE ORELSE' 648 EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set, 649 REPEAT_DETERM_N n o etac ctxt UnE]))))] 1); 650 651fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject 652 ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss = 653 let 654 val m = length ctor_set_incls; 655 val n = length ctor_set_set_inclss; 656 657 val (passive_set_map0s, active_set_map0s) = chop m set_map0s; 658 val in_Irel = nth in_Irels (i - 1); 659 val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; 660 val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; 661 val if_tac = 662 EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 663 rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 664 EVERY' (map2 (fn set_map0 => fn ctor_set_incl => 665 EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, 666 rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply, 667 rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor]) 668 passive_set_map0s ctor_set_incls), 669 CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) => 670 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, 671 rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 672 CONJ_WRAP' (fn thm => 673 EVERY' (map (etac ctxt) [thm RS subset_trans, le_arg_cong_ctor_dtor])) 674 ctor_set_set_incls, 675 rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) 676 (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)), 677 CONJ_WRAP' (fn conv => 678 EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 679 REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 680 REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]), 681 rtac ctxt (ctor_inject RS iffD1), rtac ctxt trans, rtac ctxt sym, rtac ctxt ctor_map, 682 etac ctxt eq_arg_cong_ctor_dtor]) 683 fst_snd_convs]; 684 val only_if_tac = 685 EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 686 rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 687 CONJ_WRAP' (fn (ctor_set, passive_set_map0) => 688 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least}, 689 rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]}, 690 rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt, 691 CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) 692 (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans, 693 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least}, 694 dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE, 695 dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 696 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 697 @{thms case_prodE iffD1[OF prod.inject, elim_format]}), 698 hyp_subst_tac ctxt, 699 dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, 700 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt]) 701 (rev (active_set_map0s ~~ in_Irels))]) 702 (ctor_sets ~~ passive_set_map0s), 703 rtac ctxt conjI, 704 REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2), 705 rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 706 REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 707 EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, 708 dtac ctxt set_rev_mp, assume_tac ctxt, 709 dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 710 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 711 @{thms case_prodE iffD1[OF prod.inject, elim_format]}), 712 hyp_subst_tac ctxt, 713 dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, 714 REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) 715 in_Irels), 716 assume_tac ctxt]] 717 in 718 EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1 719 end; 720 721fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers 722 ctor_rels = 723 CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) => 724 REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 725 unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN 726 HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN' 727 etac ctxt (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN' 728 EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel => 729 etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN' 730 rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN' 731 rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' 732 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' 733 REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN' 734 rtac ctxt rel_funI THEN' 735 etac ctxt (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels))) 736 (ctor_rec_defs ~~ ctor_fold_transfers); 737 738fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = 739 let val n = length ks; 740 in 741 unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN 742 EVERY' [REPEAT_DETERM o rtac ctxt allI, rtac ctxt ctor_induct2, 743 EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 => 744 EVERY' [rtac ctxt impI, dtac ctxt (ctor_rel RS iffD1), rtac ctxt (IH RS @{thm spec2} RS mp), 745 etac ctxt rel_mono_strong0, 746 REPEAT_DETERM_N m o rtac ctxt @{thm ballI[OF ballI[OF imp_refl]]}, 747 EVERY' (map (fn j => 748 EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) j, rtac ctxt @{thm ballI[OF ballI]}, 749 Goal.assume_rule_tac ctxt]) ks)]) 750 IHs ctor_rels rel_mono_strong0s)] 1 751 end; 752 753fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds = 754 let 755 val n = length map_transfers; 756 in 757 unfold_thms_tac ctxt 758 @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN 759 unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN 760 HEADGOAL (EVERY' 761 [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_induct, 762 EVERY' (map (fn map_transfer => EVERY' 763 [REPEAT_DETERM o resolve_tac ctxt [allI, impI, @{thm vimage2pI}], 764 SELECT_GOAL (unfold_thms_tac ctxt folds), 765 etac ctxt @{thm predicate2D_vimage2p}, 766 rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer), 767 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer}, 768 REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun}, 769 assume_tac ctxt]) 770 map_transfers)]) 771 end; 772 773end; 774