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