1(* Title: HOL/Tools/BNF/bnf_gfp_tactics.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Andrei Popescu, TU Muenchen 4 Author: Jasmin Blanchette, TU Muenchen 5 Copyright 2012 6 7Tactics for the codatatype construction. 8*) 9 10signature BNF_GFP_TACTICS = 11sig 12 val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic 13 val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic 14 val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic 15 val mk_bis_converse_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic 16 val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> 17 thm list list -> tactic 18 val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic 19 val mk_coalg_final_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list list -> 20 thm list list -> tactic 21 val mk_coalg_set_tac: Proof.context -> thm -> tactic 22 val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic 23 val mk_col_bd_tac: Proof.context -> int -> int -> cterm option list -> thm list -> thm list -> 24 thm -> thm -> thm list list -> tactic 25 val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> 26 thm list list -> tactic 27 val mk_congruent_str_final_tac: Proof.context -> int -> thm -> thm -> thm -> thm list -> tactic 28 val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic 29 val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic 30 val mk_dtor_coinduct_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic 31 val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> 32 thm list -> tactic 33 val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> 34 thm -> thm -> thm list -> thm list -> thm list list -> tactic 35 val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic 36 val mk_equiv_lsbis_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic 37 val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic 38 val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> 39 tactic 40 val mk_incl_lsbis_tac: Proof.context -> int -> int -> thm -> tactic 41 val mk_length_Lev'_tac: Proof.context -> thm -> tactic 42 val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic 43 val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> tactic 44 val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> 45 thm list list -> thm list list -> thm list list list -> thm list -> tactic 46 val mk_map_id0_tac: Proof.context -> thm list -> thm -> thm -> tactic 47 val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> thm -> tactic 48 val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic 49 val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic 50 val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> 51 thm list -> thm list -> tactic 52 val mk_mor_T_final_tac: Proof.context -> thm -> thm list -> thm list -> tactic 53 val mk_mor_UNIV_tac: Proof.context -> thm list -> thm -> tactic 54 val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list -> 55 thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> 56 thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> 57 thm list list -> thm list -> thm list -> tactic 58 val mk_mor_comp_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic 59 val mk_mor_elim_tac: Proof.context -> thm -> tactic 60 val mk_mor_col_tac: Proof.context -> int -> int -> cterm option list -> int -> thm list -> 61 thm list -> thm list -> thm list list -> thm list list -> tactic 62 val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic 63 val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic 64 val mk_mor_unfold_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> 65 thm list -> thm list -> thm list -> tactic 66 val mk_raw_coind_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> 67 thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic 68 val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> 69 thm list -> thm list -> tactic 70 val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list -> 71 thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic 72 val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list -> 73 int -> thm -> tactic 74 val mk_rv_last_tac: Proof.context -> ctyp option list -> cterm option list -> thm list -> 75 thm list -> tactic 76 val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic 77 val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> 78 thm list -> thm list list -> tactic 79 val mk_set_bd_tac: Proof.context -> thm -> thm -> tactic 80 val mk_set_Jset_incl_Jset_tac: Proof.context -> int -> thm -> int -> tactic 81 val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> 82 thm list -> thm list -> thm list list -> thm list list -> tactic 83 val mk_set_incl_Jset_tac: Proof.context -> thm -> tactic 84 val mk_set_ge_tac: Proof.context -> int -> thm -> thm list -> tactic 85 val mk_set_le_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic 86 val mk_set_map0_tac: Proof.context -> thm -> tactic 87 val mk_unfold_unique_mor_tac: Proof.context -> thm list -> thm -> thm -> thm list -> tactic 88 val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic 89 val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic 90 val mk_le_rel_OO_tac: Proof.context -> thm -> thm list -> thm list -> tactic 91end; 92 93structure BNF_GFP_Tactics : BNF_GFP_TACTICS = 94struct 95 96open BNF_Tactics 97open BNF_Util 98open BNF_FP_Util 99open BNF_GFP_Util 100 101val fst_convol_fun_cong_sym = @{thm fst_convol[simplified convol_def]} RS fun_cong RS sym; 102val list_inject_iffD1 = @{thm list.inject[THEN iffD1]}; 103val nat_induct = @{thm nat_induct}; 104val o_apply_trans_sym = o_apply RS trans RS sym; 105val ord_eq_le_trans = @{thm ord_eq_le_trans}; 106val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans}; 107val snd_convol_fun_cong_sym = @{thm snd_convol[simplified convol_def]} RS fun_cong RS sym; 108val sum_case_cong_weak = @{thm sum.case_cong_weak}; 109val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; 110val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]}; 111val rev_bspec = Drule.rotate_prems 1 bspec; 112val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]}; 113val converse_shift = @{thm converse_subset_swap} RS iffD1; 114 115fun mk_coalg_set_tac ctxt coalg_def = 116 dtac ctxt (coalg_def RS iffD1) 1 THEN 117 REPEAT_DETERM (etac ctxt conjE 1) THEN 118 EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN 119 REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1; 120 121fun mk_mor_elim_tac ctxt mor_def = 122 (dtac ctxt (mor_def RS iffD1) THEN' 123 REPEAT o etac ctxt conjE THEN' 124 TRY o rtac ctxt @{thm image_subsetI} THEN' 125 etac ctxt bspec THEN' 126 assume_tac ctxt) 1; 127 128fun mk_mor_incl_tac ctxt mor_def map_ids = 129 (rtac ctxt (mor_def RS iffD2) THEN' 130 rtac ctxt conjI THEN' 131 CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})])) 132 map_ids THEN' 133 CONJ_WRAP' (fn thm => 134 (EVERY' [rtac ctxt ballI, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1; 135 136fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids = 137 let 138 fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image, 139 etac ctxt image, assume_tac ctxt]; 140 fun mor_tac ((mor_image, morE), map_comp_id) = 141 EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans, 142 etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE, 143 etac ctxt mor_image, assume_tac ctxt]; 144 in 145 (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' 146 CONJ_WRAP' fbetw_tac mor_images THEN' 147 CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1 148 end; 149 150fun mk_mor_UNIV_tac ctxt morEs mor_def = 151 let 152 val n = length morEs; 153 fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE, 154 rtac ctxt UNIV_I, rtac ctxt sym, rtac ctxt o_apply]; 155 in 156 EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs, 157 rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs, 158 CONJ_WRAP' (fn i => 159 EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt ballI, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1 160 end; 161 162fun mk_mor_str_tac ctxt ks mor_UNIV = 163 (rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac ctxt refl)) ks) 1; 164 165fun mk_set_incl_Jset_tac ctxt rec_Suc = 166 EVERY' (map (rtac ctxt) [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym, 167 rec_Suc]) 1; 168 169fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i = 170 EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, 171 rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1; 172 173fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs = 174 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 175 REPEAT_DETERM o rtac ctxt allI, 176 CONJ_WRAP' (fn thm => EVERY' 177 [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s, 178 REPEAT_DETERM o rtac ctxt allI, 179 CONJ_WRAP' (fn rec_Suc => EVERY' 180 [rtac ctxt ord_eq_le_trans, rtac ctxt rec_Suc, 181 if m = 0 then K all_tac 182 else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt), 183 CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) 184 (K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], 185 rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s]) 186 rec_Sucs] 1; 187 188fun mk_Jset_minimal_tac ctxt n col_minimal = 189 (CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal, 190 EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI, 191 REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1 192 193fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss = 194 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 195 REPEAT_DETERM o rtac ctxt allI, 196 CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s, 197 REPEAT_DETERM o rtac ctxt allI, 198 CONJ_WRAP' 199 (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) => 200 EVERY' [rtac ctxt impI, rtac ctxt (rec_Suc RS trans), rtac ctxt (rec_Suc RS trans RS sym), 201 if m = 0 then K all_tac 202 else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals}, 203 rtac ctxt (nth passive_set_map0s (j - 1) RS sym), 204 rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong), 205 assume_tac ctxt], 206 CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong)) 207 (fn (i, (set_map0, coalg_set)) => 208 EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})), 209 etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0, 210 rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}), 211 forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt, 212 rtac ctxt mp, rtac ctxt (mk_conjunctN n i), 213 REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt]) 214 (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))]) 215 (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1; 216 217fun mk_bis_rel_tac ctxt m bis_def in_rels map_comp0s map_cong0s set_map0ss = 218 let 219 val n = length in_rels; 220 val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels); 221 222 fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = 223 EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i), 224 etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE, 225 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], 226 rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), 227 CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0, 228 REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), 229 assume_tac ctxt]) 230 @{thms fst_diag_id snd_diag_id}, 231 rtac ctxt CollectI, 232 CONJ_WRAP' (fn (i, thm) => 233 if i <= m 234 then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, 235 etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, 236 rtac ctxt @{thm case_prodI}, rtac ctxt refl] 237 else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm, 238 rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}]) 239 (1 upto (m + n) ~~ set_map0s)]; 240 241 fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = 242 EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 243 etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, 244 dtac ctxt (in_rel RS @{thm iffD1}), 245 REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @ 246 @{thms CollectE Collect_case_prod_in_rel_leE}), 247 rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 248 REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), 249 REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), 250 assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 251 REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), 252 REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), 253 rtac ctxt trans, rtac ctxt map_cong0, 254 REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt], 255 REPEAT_DETERM_N n o rtac ctxt refl, 256 assume_tac ctxt, rtac ctxt CollectI, 257 CONJ_WRAP' (fn (i, thm) => 258 if i <= m then rtac ctxt subset_UNIV 259 else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm, 260 rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt]) 261 (1 upto (m + n) ~~ set_map0s)]; 262 in 263 EVERY' [rtac ctxt (bis_def RS trans), 264 rtac ctxt iffI, etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_if_tac thms, 265 etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_only_if_tac thms] 1 266 end; 267 268fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps = 269 EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1), 270 REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI, 271 CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt subset_trans, 272 rtac ctxt equalityD2, rtac ctxt @{thm converse_Times}])) rel_congs, 273 CONJ_WRAP' (fn (rel_cong, rel_conversep) => 274 EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 275 rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), 276 REPEAT_DETERM_N m o rtac ctxt @{thm conversep_eq}, 277 REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm conversep_in_rel}, 278 rtac ctxt (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}), 279 REPEAT_DETERM o etac ctxt allE, 280 rtac ctxt @{thm conversepI}, etac ctxt mp, etac ctxt @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1; 281 282fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs = 283 EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1), 284 REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI, 285 CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs, 286 CONJ_WRAP' (fn (rel_cong, le_rel_OO) => 287 EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 288 rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), 289 REPEAT_DETERM_N m o rtac ctxt @{thm eq_OO}, 290 REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm relcompp_in_rel}, 291 rtac ctxt (le_rel_OO RS @{thm predicate2D}), 292 etac ctxt @{thm relcompE}, 293 REPEAT_DETERM o dtac ctxt prod_injectD, 294 etac ctxt conjE, hyp_subst_tac ctxt, 295 REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI}, 296 etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1; 297 298fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins = 299 unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN 300 EVERY' [rtac ctxt conjI, 301 CONJ_WRAP' (fn thm => rtac ctxt (@{thm Gr_incl} RS iffD2) THEN' etac ctxt thm) mor_images, 302 CONJ_WRAP' (fn (coalg_in, morE) => 303 EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt @{thm GrpI}, etac ctxt (morE RS trans), 304 etac ctxt @{thm GrD1}, etac ctxt (@{thm GrD2} RS arg_cong), etac ctxt coalg_in, etac ctxt @{thm GrD1}]) 305 (coalg_ins ~~ morEs)] 1; 306 307fun mk_bis_Union_tac ctxt bis_def in_monos = 308 let 309 val n = length in_monos; 310 val ks = 1 upto n; 311 in 312 unfold_thms_tac ctxt [bis_def] THEN 313 EVERY' [rtac ctxt conjI, 314 CONJ_WRAP' (fn i => 315 EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt, 316 dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks, 317 CONJ_WRAP' (fn (i, in_mono) => 318 EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E}, 319 dtac ctxt bspec, assume_tac ctxt, 320 dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp, 321 assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono, 322 REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]}, 323 assume_tac ctxt]) (ks ~~ in_monos)] 1 324 end; 325 326fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong = 327 let 328 val n = length lsbis_defs; 329 in 330 EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs), 331 rtac ctxt bis_Union, rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE], 332 hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1 333 end; 334 335fun mk_incl_lsbis_tac ctxt n i lsbis_def = 336 EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI, 337 REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt, 338 rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1; 339 340fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O = 341 EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2), 342 343 rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2), 344 rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp, 345 rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI}, 346 347 rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2), 348 rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp, 349 rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI}, 350 351 rtac ctxt (@{thm trans_def} RS iffD2), 352 rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp, 353 rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis, 354 etac ctxt @{thm relcompI}, assume_tac ctxt] 1; 355 356fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss = 357 let 358 val n = length strT_defs; 359 val ks = 1 upto n; 360 fun coalg_tac (i, (active_sets, def)) = 361 EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], 362 hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans), 363 rtac ctxt (mk_sum_caseN n i), rtac ctxt CollectI, 364 REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV], 365 CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans), 366 rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, 367 rtac ctxt conjI, 368 rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp, 369 etac ctxt equalityD1, etac ctxt CollectD, 370 rtac ctxt ballI, 371 CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD}, 372 dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), 373 dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]}, 374 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI, 375 rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans), 376 rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt, 377 CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong}, 378 rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift}, 379 rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks, 380 dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec, 381 etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt, 382 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI, 383 rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans), 384 etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans), 385 REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt), 386 CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong}, 387 rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift}, 388 rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; 389 in 390 unfold_thms_tac ctxt defs THEN 391 CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1 392 end; 393 394fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs = 395 let 396 val n = length Lev_0s; 397 val ks = n downto 1; 398 in 399 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 400 REPEAT_DETERM o rtac ctxt allI, 401 CONJ_WRAP' (fn Lev_0 => 402 EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), 403 etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s, 404 REPEAT_DETERM o rtac ctxt allI, 405 CONJ_WRAP' (fn Lev_Suc => 406 EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), 407 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) 408 (fn i => 409 EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt, 410 rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]}, 411 REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), 412 etac ctxt mp, assume_tac ctxt]) ks]) 413 Lev_Sucs] 1 414 end; 415 416fun mk_length_Lev'_tac ctxt length_Lev = 417 EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1; 418 419fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss = 420 let 421 val n = length rv_Nils; 422 val ks = 1 upto n; 423 in 424 EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}), 425 REPEAT_DETERM o rtac ctxt allI, 426 CONJ_WRAP' (fn rv_Cons => 427 CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI, 428 rtac ctxt (@{thm append_Nil} RS arg_cong RS trans), 429 rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), rtac ctxt rv_Nil])) 430 (ks ~~ rv_Nils)) 431 rv_Conss, 432 REPEAT_DETERM o rtac ctxt allI, rtac ctxt (mk_sumEN n), 433 EVERY' (map (fn i => 434 CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i), 435 CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI, 436 rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans), 437 if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans), 438 rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt]) 439 ks]) 440 rv_Conss) 441 ks)] 1 442 end; 443 444fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss = 445 let 446 val n = length Lev_0s; 447 val ks = 1 upto n; 448 in 449 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 450 REPEAT_DETERM o rtac ctxt allI, 451 CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => 452 EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), 453 etac ctxt @{thm singletonE}, hyp_subst_tac ctxt, 454 CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN' 455 (if i = i' 456 then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt, 457 CONJ_WRAP' (fn (i'', Lev_0'') => 458 EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]}, 459 rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i''), 460 rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, 461 etac ctxt conjI, rtac ctxt (Lev_0'' RS equalityD2 RS set_mp), 462 rtac ctxt @{thm singletonI}]) 463 (ks ~~ Lev_0s)] 464 else etac ctxt (mk_InN_not_InM i' i RS notE))) 465 ks]) 466 ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), 467 REPEAT_DETERM o rtac ctxt allI, 468 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) => 469 EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), 470 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) 471 (fn (i, from_to_sbd) => 472 EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt, 473 CONJ_WRAP' (fn i' => rtac ctxt impI THEN' 474 CONJ_WRAP' (fn i'' => 475 EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), 476 rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i), 477 rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, 478 rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym), 479 rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), 480 etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE, 481 dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt, 482 dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt, 483 dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt]) 484 ks) 485 ks]) 486 (rev (ks ~~ from_to_sbds))]) 487 ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1 488 end; 489 490fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss = 491 let 492 val n = length Lev_0s; 493 val ks = 1 upto n; 494 in 495 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 496 REPEAT_DETERM o rtac ctxt allI, 497 CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => 498 EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp), 499 etac ctxt @{thm singletonE}, hyp_subst_tac ctxt, 500 CONJ_WRAP' (fn i' => rtac ctxt impI THEN' 501 CONJ_WRAP' (fn i'' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN' 502 (if i = i'' 503 then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]}, 504 dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), dtac ctxt (mk_InN_inject n i), 505 hyp_subst_tac ctxt, 506 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) 507 (fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' 508 dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN' 509 (if k = i' 510 then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt imageI] 511 else etac ctxt (mk_InN_not_InM i' k RS notE))) 512 (rev ks)] 513 else etac ctxt (mk_InN_not_InM i'' i RS notE))) 514 ks) 515 ks]) 516 ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), 517 REPEAT_DETERM o rtac ctxt allI, 518 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) => 519 EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), 520 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) 521 (fn (i, (from_to_sbd, to_sbd_inj)) => 522 REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN' 523 CONJ_WRAP' (fn i' => rtac ctxt impI THEN' 524 dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN' 525 dtac ctxt (Lev_Suc RS equalityD1 RS set_mp) THEN' 526 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn k => 527 REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' 528 dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN' 529 (if k = i 530 then EVERY' [dtac ctxt (mk_InN_inject n i), 531 dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), 532 assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN' 533 CONJ_WRAP' (fn i'' => 534 EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans), 535 rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans), 536 etac ctxt (from_to_sbd RS arg_cong), 537 REPEAT_DETERM o etac ctxt allE, 538 dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt, 539 dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt, 540 dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym]) 541 ks 542 else etac ctxt (mk_InN_not_InM i k RS notE))) 543 (rev ks)) 544 ks) 545 (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))]) 546 ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1 547 end; 548 549fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss 550 from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss 551 set_image_Levsss set_map0ss map_comp_ids map_cong0s = 552 let 553 val n = length beh_defs; 554 val ks = 1 upto n; 555 556 fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'), 557 (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) = 558 EVERY' [rtac ctxt ballI, rtac ctxt (carT_def RS equalityD2 RS set_mp), 559 rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI, 560 rtac ctxt conjI, 561 rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt (Lev_0 RS equalityD2 RS set_mp), 562 rtac ctxt @{thm singletonI}, 563 (**) 564 rtac ctxt ballI, etac ctxt @{thm UN_E}, 565 CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s, 566 (set_Levs, set_image_Levs))))) => 567 EVERY' [rtac ctxt ballI, 568 REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], 569 rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2), 570 rtac ctxt exI, rtac ctxt conjI, 571 if n = 1 then rtac ctxt refl 572 else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i), 573 CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => 574 EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI}, 575 rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev, 576 if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI, 577 REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], 578 REPEAT_DETERM_N 4 o etac ctxt thin_rl, 579 rtac ctxt set_image_Lev, 580 assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev', 581 etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, 582 if n = 1 then rtac ctxt refl else assume_tac ctxt]) 583 (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) 584 (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ 585 (set_Levss ~~ set_image_Levss))))), 586 (*root isNode*) 587 rtac ctxt (isNode_def RS iffD2), rtac ctxt exI, rtac ctxt conjI, 588 CONVERSION (Conv.top_conv 589 (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), 590 if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i), 591 CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => 592 EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI}, 593 rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev, 594 rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil, 595 assume_tac ctxt, rtac ctxt subsetI, 596 REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}], 597 rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp), 598 rtac ctxt @{thm singletonI}, dtac ctxt length_Lev', 599 etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF 600 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]}, 601 rtac ctxt rv_Nil]) 602 (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; 603 604 fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)), 605 ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = 606 EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def, 607 CONVERSION (Conv.top_conv 608 (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), 609 if n = 1 then K all_tac 610 else (rtac ctxt (sum_case_cong_weak RS trans) THEN' 611 rtac ctxt (mk_sum_caseN n i) THEN' rtac ctxt (mk_sum_caseN n i RS trans)), 612 rtac ctxt (map_comp_id RS trans), rtac ctxt (map_cong0 OF replicate m refl), 613 EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd => 614 DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI, 615 rtac ctxt trans, rtac ctxt @{thm Shift_def}, 616 rtac ctxt equalityI, rtac ctxt subsetI, etac ctxt thin_rl, 617 REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac ctxt length_Lev', dtac ctxt asm_rl, 618 etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]}, 619 rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc, 620 CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn i'' => 621 EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], 622 dtac ctxt list_inject_iffD1, etac ctxt conjE, 623 if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'), 624 dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), 625 assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}] 626 else etac ctxt (mk_InN_not_InM i' i'' RS notE)]) 627 (rev ks), 628 rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]}, 629 rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI, 630 REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt, 631 rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI, 632 CONVERSION (Conv.top_conv 633 (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), 634 if n = 1 then K all_tac 635 else rtac ctxt sum_case_cong_weak THEN' rtac ctxt (mk_sum_caseN n i' RS trans), 636 SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac ctxt refl]) 637 ks to_sbd_injs from_to_sbds)]; 638 in 639 (rtac ctxt mor_cong THEN' 640 EVERY' (map (fn thm => rtac ctxt (thm RS @{thm ext})) beh_defs) THEN' 641 rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN' 642 CONJ_WRAP' fbetw_tac 643 (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~ 644 (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN' 645 CONJ_WRAP' mor_tac 646 (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~ 647 ((map_comp_ids ~~ map_cong0s) ~~ 648 (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1 649 end; 650 651fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs = 652 EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE, 653 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans), 654 etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans), 655 rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl, 656 EVERY' (map (fn equiv_LSBIS => 657 EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt]) 658 equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans), 659 etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1; 660 661fun mk_coalg_final_tac ctxt m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss = 662 EVERY' [rtac ctxt (coalg_def RS iffD2), 663 CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => 664 EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final, 665 rtac ctxt ballI, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt CollectI, 666 REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV], 667 CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) => 668 EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans), 669 rtac ctxt @{thm image_subsetI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, 670 rtac ctxt equiv_LSBIS, etac ctxt set_rev_mp, etac ctxt coalgT_set]) 671 (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))]) 672 ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; 673 674fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs = 675 EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, 676 CONJ_WRAP' (fn equiv_LSBIS => 677 EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff}, 678 rtac ctxt equiv_LSBIS, assume_tac ctxt]) 679 equiv_LSBISs, 680 CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) => 681 EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS, 682 rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply]) 683 (equiv_LSBISs ~~ congruent_str_finals)] 1; 684 685fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls = 686 unfold_thms_tac ctxt defs THEN 687 EVERY' [rtac ctxt conjI, 688 CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps, 689 CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) => 690 EVERY' [rtac ctxt ballI, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L, 691 EVERY' (map2 (fn Abs_inverse => fn coalg_final_set => 692 EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse, 693 etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep]) 694 Abs_inverses coalg_final_sets)]) 695 (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1; 696 697fun mk_mor_Abs_tac ctxt defs Abs_inverses = 698 unfold_thms_tac ctxt defs THEN 699 EVERY' [rtac ctxt conjI, 700 CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses, 701 CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1; 702 703fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s = 704 EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV, 705 CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) => 706 EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (dtor_def RS trans), 707 rtac ctxt (unfold_def RS arg_cong RS trans), rtac ctxt (Abs_inverse RS arg_cong RS trans), 708 rtac ctxt (morE RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans), 709 rtac ctxt (o_apply RS trans RS sym), rtac ctxt map_cong0, 710 REPEAT_DETERM_N m o rtac ctxt refl, 711 EVERY' (map (fn thm => rtac ctxt (thm RS trans) THEN' rtac ctxt (o_apply RS sym)) unfold_defs)]) 712 ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1; 713 714fun mk_raw_coind_tac ctxt bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final 715 sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = 716 let 717 val n = length Rep_injects; 718 in 719 EVERY' [rtac ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1], 720 REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse, 721 rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt, 722 rtac ctxt bis_Gr, rtac ctxt tcoalg, 723 rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr}, 724 rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT, 725 rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT, 726 rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls), 727 rtac ctxt impI, 728 CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) => 729 EVERY' [rtac ctxt subset_trans, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt subset_trans, 730 rtac ctxt @{thm relInvImage_mono}, rtac ctxt subset_trans, etac ctxt incl_lsbis, 731 rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]}, 732 rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong}, 733 rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl, 734 rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt, 735 rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on}, 736 rtac ctxt Rep_inject]) 737 (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 738 end; 739 740fun mk_unfold_unique_mor_tac ctxt raw_coinds bis mor unfold_defs = 741 CONJ_WRAP' (fn (raw_coind, unfold_def) => 742 EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor, 743 rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans), 744 rtac ctxt (o_apply RS sym), rtac ctxt UNIV_I]) (raw_coinds ~~ unfold_defs) 1; 745 746fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors = 747 unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, 748 rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L, 749 EVERY' (map (fn thm => 750 rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors), 751 rtac ctxt sym, rtac ctxt id_apply] 1; 752 753fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls = 754 unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac ctxt trans, rtac ctxt (o_apply RS arg_cong), 755 rtac ctxt trans, rtac ctxt unfold, fo_rtac ctxt (@{thm sum.case(2)} RS arg_cong RS trans), 756 rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt refl, 757 EVERY' (map (fn thm => rtac ctxt @{thm case_sum_expand_Inr} THEN' rtac ctxt thm) corec_Inls)] 1; 758 759fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor = 760 unfold_thms_tac ctxt 761 (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN 762 etac ctxt unfold_unique_mor 1; 763 764fun mk_dtor_coinduct_tac ctxt m raw_coind bis_rel rel_congs = 765 EVERY' [rtac ctxt rev_mp, rtac ctxt raw_coind, rtac ctxt iffD2, rtac ctxt bis_rel, rtac ctxt conjI, 766 CONJ_WRAP' (K (rtac ctxt @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) 767 rel_congs, 768 CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, 769 REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), 770 REPEAT_DETERM_N m o rtac ctxt refl, 771 REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]}, 772 etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}]) 773 rel_congs, 774 rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE, 775 CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp, 776 rtac ctxt CollectI, etac ctxt @{thm case_prodI}])) rel_congs] 1; 777 778fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 = 779 EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym), 780 rtac ctxt (unfold RS trans), rtac ctxt (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})), 781 rtac ctxt map_cong0, 782 REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong), 783 REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong), 784 rtac ctxt map_arg_cong, rtac ctxt (o_apply RS sym)] 1; 785 786fun mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss = 787 EVERY' [rtac ctxt Jset_minimal, 788 REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1}, 789 REPEAT_DETERM_N n o 790 EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets => 791 EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I}, 792 etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE, 793 EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)]) 794 (1 upto n) set_Jsets set_Jset_Jsetss)] 1; 795 796fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets = 797 EVERY' [rtac ctxt @{thm Un_least}, rtac ctxt set_incl_Jset, 798 REPEAT_DETERM_N (n - 1) o rtac ctxt @{thm Un_least}, 799 EVERY' (map (fn thm => rtac ctxt @{thm UN_least} THEN' etac ctxt thm) set_Jset_incl_Jsets)] 1; 800 801fun mk_map_id0_tac ctxt maps unfold_unique unfold_dtor = 802 EVERY' [rtac ctxt (unfold_unique RS trans), EVERY' (map (rtac ctxt o mk_sym) maps), 803 rtac ctxt unfold_dtor] 1; 804 805fun mk_map_comp0_tac ctxt maps map_comp0s map_unique = 806 EVERY' [rtac ctxt map_unique, 807 EVERY' (map2 (fn map_thm => fn map_comp0 => 808 EVERY' (map (rtac ctxt) 809 [@{thm comp_assoc[symmetric]} RS trans, 810 @{thm arg_cong2[of _ _ _ _ "(\<circ>)"]} OF [map_thm, refl] RS trans, 811 @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans, 812 @{thm comp_assoc[symmetric]} RS trans, 813 @{thm arg_cong2[of _ _ _ _ "(\<circ>)"]} OF [map_comp0 RS sym, refl]])) 814 maps map_comp0s)] 1; 815 816fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss 817 set_Jset_Jsetsss in_rels = 818 let 819 val n = length map_comps; 820 val ks = 1 upto n; 821 in 822 EVERY' ([rtac ctxt rev_mp, coinduct_tac] @ 823 maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets), 824 set_Jset_Jsetss), in_rel) => 825 [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2], 826 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], hyp_subst_tac ctxt, rtac ctxt exI, 827 rtac ctxt (Drule.rotate_prems 1 conjI), 828 rtac ctxt conjI, rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0, 829 REPEAT_DETERM_N m o (rtac ctxt o_apply_trans_sym THEN' rtac ctxt @{thm fst_conv}), 830 REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym, 831 rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0, 832 EVERY' (maps (fn set_Jset => 833 [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt CollectE, 834 REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, etac ctxt set_Jset]) set_Jsets), 835 REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym, 836 rtac ctxt CollectI, 837 EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, 838 rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt refl]) 839 (take m set_map0s)), 840 CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) => 841 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, 842 rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI, 843 rtac ctxt CollectI, etac ctxt CollectE, 844 REPEAT_DETERM o etac ctxt conjE, 845 CONJ_WRAP' (fn set_Jset_Jset => 846 EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets, 847 rtac ctxt (conjI OF [refl, refl])]) 848 (drop m set_map0s ~~ set_Jset_Jsetss)]) 849 (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ 850 map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @ 851 [rtac ctxt impI, 852 CONJ_WRAP' (fn k => 853 EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt CollectI, 854 rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) ks]) 1 855 end 856 857fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps = 858 rtac ctxt unfold_unique 1 THEN 859 unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN 860 ALLGOALS (etac ctxt sym); 861 862fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss = 863 let 864 val n = length dtor_maps; 865 in 866 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 867 REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s), 868 CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s, 869 REPEAT_DETERM o rtac ctxt allI, 870 CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY' 871 [SELECT_GOAL (unfold_thms_tac ctxt 872 (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), 873 rtac ctxt Un_cong, rtac ctxt refl, 874 CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong)) 875 (fn i => EVERY' [rtac ctxt @{thm SUP_cong[OF refl]}, 876 REPEAT_DETERM o etac ctxt allE, etac ctxt (mk_conjunctN n i)]) (n downto 1)]) 877 (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1 878 end; 879 880fun mk_set_map0_tac ctxt col_natural = 881 EVERY' (map (rtac ctxt) [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, 882 @{thm image_UN} RS trans, refl RS @{thm SUP_cong}, col_natural]) 1; 883 884fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss = 885 let 886 val n = length rec_0s; 887 in 888 EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), 889 REPEAT_DETERM o rtac ctxt allI, 890 CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans, 891 @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s, 892 REPEAT_DETERM o rtac ctxt allI, 893 CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY' 894 [rtac ctxt ordIso_ordLeq_trans, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt rec_Suc, 895 rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_sbds (j - 1)), 896 REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), 897 EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, 898 rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, 899 etac ctxt (mk_conjunctN n i), rtac ctxt sbd_Cinfinite]) (1 upto n) (drop m set_sbds))]) 900 (rec_Sucs ~~ set_sbdss)] 1 901 end; 902 903fun mk_set_bd_tac ctxt sbd_Cinfinite col_bd = 904 EVERY' (map (rtac ctxt) [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, 905 @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1; 906 907fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs = 908 EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO => 909 let val Jrel_imp_rel = rel_Jrel RS iffD1; 910 in 911 EVERY' [rtac ctxt (le_rel_OO RS @{thm predicate2D}), etac ctxt @{thm relcomppE}, 912 rtac ctxt @{thm relcomppI}, etac ctxt Jrel_imp_rel, etac ctxt Jrel_imp_rel] 913 end) 914 rel_Jrels le_rel_OOs) 1; 915 916fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits = 917 ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN 918 REPEAT_DETERM (assume_tac ctxt 1 ORELSE 919 EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set, 920 K (unfold_thms_tac ctxt dtor_ctors), 921 REPEAT_DETERM_N n o etac ctxt UnE, 922 REPEAT_DETERM o 923 (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN' 924 (eresolve_tac ctxt wit ORELSE' 925 (dresolve_tac ctxt wit THEN' 926 (etac ctxt FalseE ORELSE' 927 EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set, 928 K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt UnE]))))] 1); 929 930fun mk_coind_wit_tac ctxt induct unfolds set_nats wits = 931 rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN 932 unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN 933 ALLGOALS (REPEAT_DETERM o etac ctxt imageE THEN' TRY o hyp_subst_tac ctxt) THEN 934 ALLGOALS (TRY o 935 FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]); 936 937fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers 938 dtor_rels = 939 CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) => 940 REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 941 unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN 942 HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN' 943 EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel => 944 etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN' 945 rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN' 946 rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' 947 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' 948 REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN' 949 rtac ctxt rel_funI THEN' 950 etac ctxt (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN' 951 etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer}))) 952 (dtor_corec_defs ~~ dtor_unfold_transfer); 953 954fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject 955 dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss = 956 let 957 val m = length dtor_set_incls; 958 val n = length dtor_set_set_inclss; 959 val (passive_set_map0s, active_set_map0s) = chop m set_map0s; 960 val in_Jrel = nth in_Jrels (i - 1); 961 val if_tac = 962 EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 963 rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 964 EVERY' (map2 (fn set_map0 => fn set_incl => 965 EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, 966 rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply, 967 etac ctxt (set_incl RS @{thm subset_trans})]) 968 passive_set_map0s dtor_set_incls), 969 CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) => 970 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, 971 rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 972 CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls, 973 rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) 974 (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)), 975 CONJ_WRAP' (fn conv => 976 EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0, 977 REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 978 REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]), 979 rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt]) 980 @{thms fst_conv snd_conv}]; 981 val only_if_tac = 982 EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], 983 rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI, 984 CONJ_WRAP' (fn (dtor_set, passive_set_map0) => 985 EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least}, 986 rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0, 987 rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt, 988 CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least})) 989 (fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans, 990 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]}, 991 rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least}, 992 dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE, 993 dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 994 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 995 @{thms case_prodE iffD1[OF prod.inject, elim_format]}), 996 hyp_subst_tac ctxt, 997 dtac ctxt (in_Jrel RS iffD1), 998 dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, 999 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt]) 1000 (rev (active_set_map0s ~~ in_Jrels))]) 1001 (dtor_sets ~~ passive_set_map0s), 1002 rtac ctxt conjI, 1003 REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map, 1004 rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans, 1005 rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]}, 1006 EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt, 1007 dtac ctxt @{thm ssubst_mem[OF prod.collapse]}, 1008 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE :: 1009 @{thms case_prodE iffD1[OF prod.inject, elim_format]}), 1010 hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1), 1011 dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels), 1012 assume_tac ctxt]] 1013 in 1014 EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1 1015 end; 1016 1017fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 1018 dtor_unfolds dtor_maps in_rels = 1019 let 1020 val n = length ks; 1021 val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd}; 1022 val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd}; 1023 in 1024 EVERY' [rtac ctxt coinduct, 1025 EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => 1026 fn dtor_unfold => fn dtor_map => fn in_rel => 1027 EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2], 1028 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], 1029 select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, 1030 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt, 1031 rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI, 1032 rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym), 1033 rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]), 1034 REPEAT_DETERM_N m o rtac ctxt (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}), 1035 REPEAT_DETERM_N n o (rtac ctxt @{thm sym[OF trans[OF o_apply]]} THEN' rtac ctxt @{thm fst_conv}), 1036 rtac ctxt (map_comp0 RS trans), rtac ctxt (map_cong RS trans), 1037 REPEAT_DETERM_N m o rtac ctxt (snd_diag_nth RS fun_cong), 1038 REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}), 1039 etac ctxt (@{thm prod.case} RS map_arg_cong RS trans), 1040 SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}), 1041 rtac ctxt CollectI, 1042 CONJ_WRAP' (fn set_map0 => 1043 EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans), 1044 rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, 1045 FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, 1046 assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]]) 1047 set_map0s]) 1048 ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1 1049 end; 1050 1051val split_id_unfolds = @{thms prod.case image_id id_apply}; 1052 1053fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct = 1054 let val n = length ks; 1055 in 1056 rtac ctxt set_induct 1 THEN 1057 EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => 1058 EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE, 1059 select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, 1060 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp], 1061 hyp_subst_tac ctxt, 1062 SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)), 1063 rtac ctxt subset_refl]) 1064 unfolds set_map0ss ks) 1 THEN 1065 EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i => 1066 EVERY' (map (fn set_map0 => 1067 EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE, 1068 select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt, 1069 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt, 1070 SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)), 1071 etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp], 1072 rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt, 1073 rtac ctxt (@{thm surjective_pairing} RS arg_cong)]) 1074 (drop m set_map0s))) 1075 unfolds set_map0ss ks) 1 1076 end; 1077 1078fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s = 1079 let val n = length in_rels; 1080 in 1081 Method.insert_tac ctxt CIHs 1 THEN 1082 unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN 1083 REPEAT_DETERM (etac ctxt exE 1) THEN 1084 CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) => 1085 EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, 1086 if null helper_inds then rtac ctxt UNIV_I 1087 else rtac ctxt CollectI THEN' 1088 CONJ_WRAP' (fn helper_ind => 1089 EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, 1090 REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI, 1091 REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}], 1092 dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE], 1093 etac ctxt (refl RSN (2, conjI))]) 1094 helper_inds, 1095 rtac ctxt conjI, 1096 rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, 1097 REPEAT_DETERM_N n o etac ctxt thin_rl, 1098 rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)), 1099 rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt, 1100 REPEAT_DETERM_N n o etac ctxt thin_rl, 1101 rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))]) 1102 (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1 1103 end; 1104 1105fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds = 1106 let 1107 val n = length map_transfers; 1108 in 1109 unfold_thms_tac ctxt 1110 @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN 1111 unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN 1112 HEADGOAL (EVERY' 1113 [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_coinduct, 1114 EVERY' (map (fn map_transfer => EVERY' 1115 [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt @{thm image2pE}, hyp_subst_tac ctxt, 1116 SELECT_GOAL (unfold_thms_tac ctxt unfolds), 1117 rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer), 1118 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer}, 1119 REPEAT_DETERM_N n o rtac ctxt @{thm rel_fun_image2p}, 1120 etac ctxt @{thm predicate2D}, etac ctxt @{thm image2pI}]) 1121 map_transfers)]) 1122 end; 1123 1124end; 1125