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