src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49104 6defdacd595a
child 49305 8241f21d104b
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/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: cterm option list -> thm list -> thm list -> thm list list -> tactic
    13   val mk_bd_card_order_tac: thm -> tactic
    14   val mk_bd_cinfinite_tac: thm -> tactic
    15   val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
    16     {prems: 'a, context: Proof.context} -> tactic
    17   val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
    18   val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    19   val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
    20   val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    21   val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
    22     {prems: 'a, context: Proof.context} -> tactic
    23   val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
    24   val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
    25     {prems: 'a, context: Proof.context} -> tactic
    26   val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
    27     tactic
    28   val mk_coalg_set_tac: thm -> tactic
    29   val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->
    30     {prems: 'a, context: Proof.context} -> tactic
    31   val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
    32     {prems: 'a, context: Proof.context} -> tactic
    33   val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
    34   val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
    35     thm list list -> tactic
    36   val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
    37     {prems: 'a, context: Proof.context} -> tactic
    38   val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
    39   val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
    40     {prems: 'a, context: Proof.context} -> tactic
    41   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
    42   val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    43   val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
    44     {prems: 'a, context: Proof.context} -> tactic
    45   val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    46     thm -> thm -> thm -> tactic
    47   val mk_incl_lsbis_tac: int -> int -> thm -> tactic
    48   val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    49   val mk_length_Lev'_tac: thm -> tactic
    50   val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    51   val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
    52   val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
    53     thm list list -> thm list list list -> tactic
    54   val mk_map_id_tac: thm list -> thm -> thm -> tactic
    55   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
    56   val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    57   val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    58   val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
    59     thm list -> {prems: 'a, context: Proof.context} -> tactic
    60   val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
    61   val mk_mor_UNIV_tac: thm list -> thm -> tactic
    62   val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    63     thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
    64     thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    65     thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    66     {prems: 'a, context: Proof.context} -> tactic
    67   val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    68     thm list -> tactic
    69   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    70   val mk_mor_elim_tac: thm -> tactic
    71   val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
    72     thm list -> thm list list -> thm list list -> tactic
    73   val mk_mor_hset_tac: thm -> thm -> tactic
    74   val mk_mor_incl_tac: thm -> thm list -> tactic
    75   val mk_mor_str_tac: 'a list -> thm -> tactic
    76   val mk_mor_sum_case_tac: 'a list -> thm -> tactic
    77   val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
    78     {prems: thm list, context: Proof.context} -> tactic
    79   val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
    80     {prems: thm list, context: Proof.context} -> tactic
    81   val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
    82     {prems: 'a, context: Proof.context} -> tactic
    83   val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    84   val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
    85   val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
    86     thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
    87     tactic
    88   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    89     thm list -> thm list -> thm -> thm list -> tactic
    90   val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic
    91   val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
    92     thm list -> tactic
    93   val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    94     thm list -> thm list -> thm list list -> tactic
    95   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
    96   val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
    97   val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
    98     thm list list -> tactic
    99   val mk_set_bd_tac: thm -> thm -> thm -> tactic
   100   val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
   101   val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
   102     thm list list -> thm list list -> tactic
   103   val mk_set_incl_hin_tac: thm list -> tactic
   104   val mk_set_incl_hset_tac: thm -> thm -> tactic
   105   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   106   val mk_set_natural_tac: thm -> thm -> tactic
   107   val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
   108     thm list list -> thm list list -> tactic
   109   val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
   110   val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
   111     cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
   112     thm list list -> thm list list -> thm -> thm list list -> tactic
   113   val mk_unf_coinduct_tac: int -> int list -> thm -> thm -> tactic
   114   val mk_unf_coinduct_upto_tac: int list -> ctyp option list -> cterm option list -> thm -> thm ->
   115     thm -> tactic
   116   val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list ->
   117     {prems: 'a, context: Proof.context} -> tactic
   118   val mk_unique_mor_tac: thm list -> thm -> tactic
   119   val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
   120     {prems: 'a, context: Proof.context} -> tactic
   121   val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic
   122 end;
   123 
   124 structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
   125 struct
   126 
   127 open BNF_Tactics
   128 open BNF_Util
   129 open BNF_FP_Util
   130 open BNF_GFP_Util
   131 
   132 fun mk_coalg_set_tac coalg_def =
   133   dtac (coalg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) 1 THEN
   134   REPEAT_DETERM (etac conjE 1) THEN
   135   EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   136   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
   137 
   138 fun mk_mor_elim_tac mor_def =
   139   (dtac (subst OF [mor_def]) THEN'
   140   REPEAT o etac conjE THEN'
   141   TRY o rtac @{thm image_subsetI} THEN'
   142   etac bspec THEN'
   143   atac) 1;
   144 
   145 fun mk_mor_incl_tac mor_def map_id's =
   146   (stac mor_def THEN'
   147   rtac conjI THEN'
   148   CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm set_mp}, stac @{thm id_apply}, atac]))
   149     map_id's THEN'
   150   CONJ_WRAP' (fn thm =>
   151    (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
   152   map_id's) 1;
   153 
   154 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   155   let
   156     fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
   157     fun mor_tac ((mor_image, morE), map_comp_id) =
   158       EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
   159         etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
   160   in
   161     (stac mor_def THEN' rtac conjI THEN'
   162     CONJ_WRAP' fbetw_tac mor_images THEN'
   163     CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
   164   end;
   165 
   166 fun mk_mor_UNIV_tac morEs mor_def =
   167   let
   168     val n = length morEs;
   169     fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
   170       rtac UNIV_I, rtac sym, rtac o_apply];
   171   in
   172     EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
   173     stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
   174     CONJ_WRAP' (fn i =>
   175       EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1
   176   end;
   177 
   178 fun mk_mor_str_tac ks mor_UNIV =
   179   (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
   180 
   181 fun mk_mor_sum_case_tac ks mor_UNIV =
   182   (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1;
   183 
   184 fun mk_set_incl_hset_tac def rec_Suc =
   185   EVERY' (stac def ::
   186     map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
   187       sym, rec_Suc]) 1;
   188 
   189 fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
   190   EVERY' (map (TRY oo stac) defs @
   191     map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, @{thm set_mp}, equalityD2, rec_Suc,
   192       UnI2, mk_UnN n i] @
   193     [etac @{thm UN_I}, atac]) 1;
   194 
   195 fun mk_set_incl_hin_tac incls =
   196   if null incls then rtac @{thm subset_UNIV} 1
   197   else EVERY' [rtac subsetI, rtac CollectI,
   198     CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
   199 
   200 fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
   201   EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   202     REPEAT_DETERM o rtac allI,
   203     CONJ_WRAP' (fn thm => EVERY'
   204       [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
   205     REPEAT_DETERM o rtac allI,
   206     CONJ_WRAP' (fn rec_Suc => EVERY'
   207       [rtac @{thm ord_eq_le_trans}, rtac rec_Suc,
   208         if m = 0 then K all_tac
   209         else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
   210         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   211           (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
   212             rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
   213       rec_Sucs] 1;
   214 
   215 fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
   216   (CONJ_WRAP' (fn def => (EVERY' [rtac @{thm ord_eq_le_trans}, rtac def,
   217     rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
   218     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
   219     REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
   220 
   221 fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =
   222   EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   223     REPEAT_DETERM o rtac allI,
   224     CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
   225     REPEAT_DETERM o rtac allI,
   226     CONJ_WRAP'
   227       (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) =>
   228         EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
   229           if m = 0 then K all_tac
   230           else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
   231             rtac (nth passive_set_naturals (j - 1) RS sym),
   232             rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac (morE RS arg_cong), atac],
   233           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   234             (fn (i, (set_natural, coalg_set)) =>
   235               EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
   236                 etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,
   237                 rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
   238                 ftac coalg_set, atac, dtac @{thm set_mp}, atac, rtac mp, rtac (mk_conjunctN n i),
   239                 REPEAT_DETERM o etac allE, atac, atac])
   240             (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])
   241       (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;
   242 
   243 fun mk_mor_hset_tac hset_def mor_hset_rec =
   244   EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
   245     atac, atac, rtac (hset_def RS sym)] 1
   246 
   247 fun mk_bis_rel_tac m bis_def rel_defs map_comps map_congs set_naturalss =
   248   let
   249     val n = length rel_defs;
   250     val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_defs);
   251 
   252     fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
   253       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
   254         etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
   255         rtac (rel_def RS equalityD2 RS @{thm set_mp}),
   256         rtac @{thm relcompI}, rtac @{thm converseI},
   257         EVERY' (map (fn thm =>
   258           EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   259             rtac CollectI,
   260             CONJ_WRAP' (fn (i, thm) =>
   261               if i <= m
   262               then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac subset_trans,
   263                 etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
   264               else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm,
   265                 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
   266             (1 upto (m + n) ~~ set_naturals),
   267             rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
   268             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
   269           @{thms fst_diag_id snd_diag_id})];
   270 
   271     fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
   272       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
   273         etac allE, etac allE, etac impE, atac,
   274         dtac (rel_def RS equalityD1 RS @{thm set_mp}),
   275         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
   276         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
   277         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   278         REPEAT_DETERM o etac conjE,
   279         hyp_subst_tac,
   280         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   281         rtac bexI, rtac conjI, rtac trans, rtac map_comp,
   282         REPEAT_DETERM_N m o stac @{thm id_o},
   283         REPEAT_DETERM_N n o stac @{thm o_id},
   284         etac sym, rtac trans, rtac map_comp,
   285         REPEAT_DETERM_N m o stac @{thm id_o},
   286         REPEAT_DETERM_N n o stac @{thm o_id},
   287         rtac trans, rtac map_cong,
   288         REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac @{thm set_mp}, atac],
   289         REPEAT_DETERM_N n o rtac refl,
   290         etac sym, rtac CollectI,
   291         CONJ_WRAP' (fn (i, thm) =>
   292           if i <= m
   293           then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
   294             rtac @{thm diag_fst}, etac @{thm set_mp}, atac]
   295           else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm,
   296             rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
   297         (1 upto (m + n) ~~ set_naturals)];
   298   in
   299     EVERY' [rtac (bis_def RS trans),
   300       rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
   301       etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
   302   end;
   303 
   304 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
   305   EVERY' [stac bis_rel, dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}),
   306     REPEAT_DETERM o etac conjE, rtac conjI,
   307     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
   308       rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
   309     CONJ_WRAP' (fn (rel_cong, rel_converse) =>
   310       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
   311         rtac (rel_cong RS trans),
   312         REPEAT_DETERM_N m o rtac @{thm diag_converse},
   313         REPEAT_DETERM_N (length rel_congs) o rtac refl,
   314         rtac rel_converse,
   315         REPEAT_DETERM o etac allE,
   316         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
   317 
   318 fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
   319   EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}),
   320     REPEAT_DETERM o etac conjE, rtac conjI,
   321     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
   322     CONJ_WRAP' (fn (rel_cong, rel_O) =>
   323       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
   324         rtac (rel_cong RS trans),
   325         REPEAT_DETERM_N m o rtac @{thm diag_Comp},
   326         REPEAT_DETERM_N (length rel_congs) o rtac refl,
   327         rtac rel_O,
   328         etac @{thm relcompE},
   329         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   330         etac conjE, hyp_subst_tac,
   331         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
   332         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
   333 
   334 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
   335   {context = ctxt, prems = _} =
   336   Local_Defs.unfold_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
   337   EVERY' [rtac conjI,
   338     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
   339     CONJ_WRAP' (fn (coalg_in, morE) =>
   340       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,
   341         etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},
   342         etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1;
   343 
   344 fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
   345   let
   346     val n = length in_monos;
   347     val ks = 1 upto n;
   348   in
   349     Local_Defs.unfold_tac ctxt [bis_def] THEN
   350     EVERY' [rtac conjI,
   351       CONJ_WRAP' (fn i =>
   352         EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
   353           dtac conjunct1, etac (mk_conjunctN n i)]) ks,
   354       CONJ_WRAP' (fn (i, in_mono) =>
   355         EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
   356           dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
   357           atac, etac bexE, rtac bexI, atac, rtac in_mono,
   358           REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},
   359           atac]) (ks ~~ in_monos)] 1
   360   end;
   361 
   362 fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
   363   let
   364     val n = length lsbis_defs;
   365   in
   366     EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
   367       rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
   368       hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   369   end;
   370 
   371 fun mk_incl_lsbis_tac n i lsbis_def =
   372   EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
   373     REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
   374     rtac (mk_nth_conv n i)] 1;
   375 
   376 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
   377   EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF equiv_def]},
   378 
   379     rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF refl_on_def]},
   380     rtac conjI, rtac lsbis_incl, rtac ballI, rtac @{thm set_mp},
   381     rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
   382 
   383     rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF sym_def]},
   384     rtac allI, rtac allI, rtac impI, rtac @{thm set_mp},
   385     rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
   386 
   387     rtac @{thm ssubst[of _ _ "%x. x", OF trans_def]},
   388     rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac @{thm set_mp},
   389     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
   390     etac @{thm relcompI}, atac] 1;
   391 
   392 fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =
   393   let
   394     val n = length strT_defs;
   395     val ks = 1 upto n;
   396     fun coalg_tac (i, ((passive_sets, active_sets), def)) =
   397       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   398         hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
   399         rtac (mk_sum_casesN n i), rtac CollectI,
   400         EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS @{thm ord_eq_le_trans}),
   401           etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS
   402             @{thm ord_eq_le_trans})]) passive_sets),
   403         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   404           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
   405           rtac conjI,
   406           rtac conjI, etac @{thm empty_Shift}, dtac @{thm set_rev_mp},
   407             etac equalityD1, etac CollectD,
   408           rtac conjI, etac @{thm Shift_clists},
   409           rtac conjI, etac @{thm Shift_prefCl},
   410           rtac conjI, rtac ballI,
   411             rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
   412             SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Succ_Shift shift_def}),
   413             etac bspec, etac @{thm ShiftD},
   414             CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
   415               dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
   416               dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
   417               REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
   418               rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
   419               rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
   420               REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   421               CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
   422                 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
   423                 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
   424           rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],
   425           etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,
   426           dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,
   427           etac @{thm set_mp[OF equalityD1]}, atac,
   428           REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
   429           rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
   430           etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
   431           REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   432           CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
   433             rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
   434             rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   435   in
   436     Local_Defs.unfold_tac ctxt defs THEN
   437     CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
   438   end;
   439 
   440 fun mk_card_of_carT_tac m isNode_defs sbd_sbd
   441   sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
   442   let
   443     val n = length isNode_defs;
   444   in
   445     EVERY' [rtac (Thm.permute_prems 0 1 ctrans),
   446       rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp},
   447       if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   448       rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},
   449       rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,
   450       rtac ctrans, rtac @{thm card_of_diff},
   451       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso},
   452       rtac @{thm Card_order_cpow}, rtac @{thm ordIso_ordLeq_trans},
   453       rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
   454       if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   455       rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists},
   456       rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm ordIso_ordLeq_trans},
   457       rtac @{thm clists_Cinfinite},
   458       if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
   459       rtac @{thm ordIso_ordLeq_trans}, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
   460       rtac sbd_Cinfinite,
   461       if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   462       rtac @{thm Cnotzero_clists},
   463       rtac ballI, rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Func_Ffunc},
   464       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm Func_cexp},
   465       rtac ctrans, rtac @{thm cexp_mono},
   466       rtac @{thm ordLeq_ordIso_trans},
   467       CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1
   468           (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}
   469         RSN (3, @{thm Un_Cinfinite_bound}))))
   470         (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),
   471       rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1},
   472       REPEAT_DETERM_N m o rtac @{thm csum_cong2},
   473       CONJ_WRAP_GEN' (rtac @{thm csum_cong})
   474         (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,
   475       rtac sbd_Card_order,
   476       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   477       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   478       rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},
   479       rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,
   480       rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp},
   481       rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2},
   482       rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac,
   483       rtac @{thm card_of_Card_order},
   484       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod},
   485       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   486       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong2_Cnotzero},
   487       rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
   488       rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
   489       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod},
   490       rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
   491       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
   492       rtac @{thm ordIso_transitive},
   493       REPEAT_DETERM_N m o rtac @{thm csum_cong2},
   494       rtac sbd_sbd,
   495       BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
   496         FIRST' [rtac @{thm card_of_Card_order},
   497           rtac @{thm Card_order_csum}, rtac sbd_Card_order])
   498         @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
   499         (1 upto m + 1) (m + 1 :: (1 upto m)),
   500       if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}],
   501       rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,
   502       if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
   503       if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   504       rtac @{thm Card_order_ctwo},
   505       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order,
   506       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod_ordLeq},
   507       if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   508       rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
   509       rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
   510       rtac sbd_Cinfinite,
   511       if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   512       rtac sbd_Cnotzero,
   513       rtac @{thm card_of_mono1}, rtac subsetI,
   514       REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
   515       rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac @{thm set_mp}, rtac equalityD2,
   516       rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
   517       rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
   518       hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS @{thm set_mp}),
   519       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
   520       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
   521         [rtac (mk_UnN n i), dtac (def RS @{thm subst[of _ _ "%x. x"]}),
   522         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
   523         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   524         CONJ_WRAP' (K (EVERY' [etac @{thm ord_eq_le_trans}, rtac subset_trans,
   525           rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order},
   526           rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
   527       atac] 1
   528   end;
   529 
   530 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
   531   EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}),
   532     REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   533     dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   534     etac conjE, hyp_subst_tac,
   535     dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}),
   536     REPEAT_DETERM o eresolve_tac [exE, conjE],
   537     rtac (equalityD2 RS @{thm set_mp}),
   538     rtac (strT_def RS arg_cong RS trans),
   539     etac (arg_cong RS trans),
   540     fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
   541     rtac set_natural, rtac imageI, etac (equalityD2 RS @{thm set_mp}), rtac CollectI,
   542     etac @{thm prefCl_Succ}, atac] 1;
   543 
   544 fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   545   set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss =
   546   let
   547     val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss;
   548     val ks = 1 upto n;
   549     fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) =
   550       CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
   551         (if i = i'
   552         then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
   553           rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
   554           rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
   555           rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
   556           rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
   557         else EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}),
   558           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
   559           dtac conjunct2, dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, etac conjE,
   560           hyp_subst_tac, dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}),
   561           REPEAT_DETERM o eresolve_tac [exE, conjE],
   562           rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
   563       (ks ~~ (carT_defs ~~ isNode_defs));
   564     fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =
   565       dtac (mk_conjunctN n i) THEN'
   566       CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>
   567         EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,
   568           rtac (coalgT RS coalg_set RS @{thm set_mp}), atac, etac carT_set, atac, atac,
   569           etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,
   570           rtac set_hset_incl_hset, etac carT_set, atac, atac])
   571       (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));
   572   in
   573     EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
   574       REPEAT_DETERM o rtac allI, rtac impI,
   575       CONJ_WRAP' base_tac
   576         (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))),
   577       REPEAT_DETERM o rtac allI, rtac impI,
   578       REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
   579       CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
   580         CONJ_WRAP_GEN' (K all_tac) step_tac
   581           (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1
   582   end;
   583 
   584 fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} =
   585   let
   586     val m = length strT_hsets;
   587   in
   588     if m = 0 then atac 1
   589     else (Local_Defs.unfold_tac ctxt [isNode_def] THEN
   590       EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   591         rtac exI, rtac conjI, atac,
   592         CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
   593           else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac])
   594         (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
   595   end;
   596 
   597 fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
   598   let
   599     val n = length Lev_0s;
   600     val ks = 1 upto n;
   601   in
   602     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   603       REPEAT_DETERM o rtac allI,
   604       CONJ_WRAP' (fn Lev_0 =>
   605         EVERY' (map rtac [@{thm ord_eq_le_trans}, Lev_0, @{thm Nil_clists}])) Lev_0s,
   606       REPEAT_DETERM o rtac allI,
   607       CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
   608         EVERY' [rtac @{thm ord_eq_le_trans}, rtac Lev_Suc,
   609           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   610             (fn (i, to_sbd) => EVERY' [rtac subsetI,
   611               REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   612               rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
   613               etac @{thm set_rev_mp}, REPEAT_DETERM o etac allE,
   614               etac (mk_conjunctN n i)])
   615           (rev (ks ~~ to_sbds))])
   616       (Lev_Sucs ~~ to_sbdss)] 1
   617   end;
   618 
   619 fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
   620   let
   621     val n = length Lev_0s;
   622     val ks = n downto 1;
   623   in
   624     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   625       REPEAT_DETERM o rtac allI,
   626       CONJ_WRAP' (fn Lev_0 =>
   627         EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
   628           etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
   629       REPEAT_DETERM o rtac allI,
   630       CONJ_WRAP' (fn Lev_Suc =>
   631         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   632           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   633             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   634               rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
   635               REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
   636       Lev_Sucs] 1
   637   end;
   638 
   639 fun mk_length_Lev'_tac length_Lev =
   640   EVERY' [ftac length_Lev, etac ssubst, atac] 1;
   641 
   642 fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
   643   let
   644     val n = length Lev_0s;
   645     val ks = n downto 1;
   646   in
   647     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   648       REPEAT_DETERM o rtac allI,
   649       CONJ_WRAP' (fn Lev_0 =>
   650         EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
   651           etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
   652           hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   653           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
   654       REPEAT_DETERM o rtac allI,
   655       CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
   656         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   657           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   658             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   659               dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
   660               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   661               rtac Lev_0, rtac @{thm singletonI},
   662               REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
   663               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
   664               rtac Lev_Suc, rtac (mk_UnN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
   665               rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   666               etac mp, etac conjI, atac]) ks])
   667       (Lev_0s ~~ Lev_Sucs)] 1
   668   end;
   669 
   670 fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
   671   let
   672     val n = length rv_Nils;
   673     val ks = 1 upto n;
   674   in
   675     EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
   676       REPEAT_DETERM o rtac allI,
   677       CONJ_WRAP' (fn rv_Cons =>
   678         CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
   679           rtac (@{thm append_Nil} RS arg_cong RS trans),
   680           rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
   681         (ks ~~ rv_Nils))
   682       rv_Conss,
   683       REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
   684       EVERY' (map (fn i =>
   685         CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   686           CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
   687             rtac (@{thm append_Cons} RS arg_cong RS trans),
   688             rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans),
   689             rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
   690           ks])
   691         rv_Conss)
   692       ks)] 1
   693   end;
   694 
   695 fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
   696   let
   697     val n = length Lev_0s;
   698     val ks = 1 upto n;
   699   in
   700     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   701       REPEAT_DETERM o rtac allI,
   702       CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
   703         EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
   704           dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), etac @{thm singletonE}, etac ssubst,
   705           rtac (rv_Nil RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}),
   706           rtac (mk_sum_casesN n i RS @{thm ssubst[of _ _ "%x. x"]}),
   707           CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
   708       (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
   709       REPEAT_DETERM o rtac allI,
   710       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
   711         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   712           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   713             (fn (i, (from_to_sbd, coalg_set)) =>
   714               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   715               rtac (rv_Cons RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}),
   716               rtac (mk_sum_casesN n i RS arg_cong RS trans RS @{thm ssubst[of _ _ "%x. x"]}),
   717               etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   718               dtac (mk_conjunctN n i), etac mp, etac conjI, etac @{thm set_rev_mp},
   719               etac coalg_set, atac])
   720           (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
   721       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
   722   end;
   723 
   724 fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   725   let
   726     val n = length Lev_0s;
   727     val ks = 1 upto n;
   728   in
   729     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   730       REPEAT_DETERM o rtac allI,
   731       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   732         EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
   733           etac @{thm singletonE}, hyp_subst_tac,
   734           CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   735             (if i = i'
   736             then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
   737               CONJ_WRAP' (fn (i'', Lev_0'') =>
   738                 EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
   739                   rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i''),
   740                   rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
   741                   etac conjI, rtac (Lev_0'' RS equalityD2 RS @{thm set_mp}),
   742                   rtac @{thm singletonI}])
   743               (ks ~~ Lev_0s)]
   744             else etac (mk_InN_not_InM i' i RS notE)))
   745           ks])
   746       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
   747       REPEAT_DETERM o rtac allI,
   748       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
   749         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   750           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   751             (fn (i, from_to_sbd) =>
   752               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   753                 CONJ_WRAP' (fn i' => rtac impI THEN'
   754                   CONJ_WRAP' (fn i'' =>
   755                     EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}),
   756                       rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i),
   757                       rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
   758                       rtac conjI, atac, dtac (sym RS trans RS sym),
   759                       rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
   760                       etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   761                       dtac (mk_conjunctN n i), dtac mp, atac,
   762                       dtac (mk_conjunctN n i'), dtac mp, atac,
   763                       dtac (mk_conjunctN n i''), etac mp, atac])
   764                   ks)
   765                 ks])
   766           (rev (ks ~~ from_to_sbds))])
   767       ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
   768   end;
   769 
   770 fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
   771   let
   772     val n = length Lev_0s;
   773     val ks = 1 upto n;
   774   in
   775     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
   776       REPEAT_DETERM o rtac allI,
   777       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   778         EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
   779           etac @{thm singletonE}, hyp_subst_tac,
   780           CONJ_WRAP' (fn i' => rtac impI THEN'
   781             CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   782               (if i = i''
   783               then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
   784                 dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), dtac (mk_InN_inject n i),
   785                 hyp_subst_tac,
   786                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   787                   (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
   788                     dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN'
   789                     (if k = i'
   790                     then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
   791                     else etac (mk_InN_not_InM i' k RS notE)))
   792                 (rev ks)]
   793               else etac (mk_InN_not_InM i'' i RS notE)))
   794             ks)
   795           ks])
   796       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
   797       REPEAT_DETERM o rtac allI,
   798       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
   799         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   800           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   801             (fn (i, (from_to_sbd, to_sbd_inj)) =>
   802               REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
   803               CONJ_WRAP' (fn i' => rtac impI THEN'
   804                 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
   805                 dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}) THEN'
   806                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
   807                   REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
   808                   dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN'
   809                   (if k = i
   810                   then EVERY' [dtac (mk_InN_inject n i),
   811                     dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
   812                     atac, atac, hyp_subst_tac] THEN'
   813                     CONJ_WRAP' (fn i'' =>
   814                       EVERY' [rtac impI, dtac (sym RS trans),
   815                         rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
   816                         etac (from_to_sbd RS arg_cong),
   817                         REPEAT_DETERM o etac allE,
   818                         dtac (mk_conjunctN n i), dtac mp, atac,
   819                         dtac (mk_conjunctN n i'), dtac mp, atac,
   820                         dtac (mk_conjunctN n i''), etac mp, etac sym])
   821                     ks
   822                   else etac (mk_InN_not_InM i k RS notE)))
   823                 (rev ks))
   824               ks)
   825           (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
   826       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
   827   end;
   828 
   829 fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   830   to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   831   prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
   832   map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =
   833   let
   834     val n = length beh_defs;
   835     val ks = 1 upto n;
   836 
   837     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
   838       ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,
   839         (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
   840       EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS @{thm set_mp}),
   841         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
   842         rtac conjI,
   843           rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}),
   844           rtac @{thm singletonI},
   845         rtac conjI,
   846           rtac @{thm UN_least}, rtac Lev_sbd,
   847         rtac conjI,
   848           rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
   849           rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
   850           etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
   851         rtac conjI,
   852           rtac ballI, etac @{thm UN_E}, rtac conjI,
   853           if n = 1 then K all_tac else rtac (mk_sumEN n),
   854           EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
   855             fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
   856             EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
   857               rtac exI, rtac conjI,
   858               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   859               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
   860                 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
   861               EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   862                 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
   863                   rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
   864                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
   865               (take m set_naturals) set_rv_Levs),
   866               CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   867                 EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   868                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   869                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
   870                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   871                   rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   872                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   873                   if n = 1 then rtac refl else atac])
   874               (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   875           ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss),
   876           CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals,
   877             (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
   878             EVERY' [rtac ballI,
   879               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   880               rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
   881               rtac exI, rtac conjI,
   882               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   883               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
   884                 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
   885               EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   886                 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
   887                   rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
   888                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
   889               (take m set_naturals) set_rv_Levs),
   890               CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   891                 EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   892                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   893                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
   894                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   895                   REPEAT_DETERM_N 4 o etac thin_rl,
   896                   rtac set_image_Lev,
   897                   atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   898                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   899                   if n = 1 then rtac refl else atac])
   900               (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   901           (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~
   902             (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
   903         (**)
   904           rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
   905           etac notE, etac @{thm UN_I[OF UNIV_I]},
   906         (*root isNode*)
   907           rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
   908           rtac length_Lev', rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI},
   909           CONVERSION (Conv.top_conv
   910             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   911           if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
   912           EVERY' (map2 (fn set_natural => fn coalg_set =>
   913             EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
   914               rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac coalg_set, atac])
   915             (take m set_naturals) (take m coalg_sets)),
   916           CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   917             EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   918               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
   919               rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI}, rtac rv_Nil,
   920               atac, rtac subsetI,
   921               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   922               rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}),
   923               rtac @{thm singletonI}, dtac length_Lev',
   924               etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
   925                 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
   926               rtac rv_Nil])
   927           (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
   928 
   929     fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
   930       ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
   931       EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
   932         rtac (@{thm if_P} RS
   933           (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans),
   934         rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS @{thm set_mp}),
   935         rtac Lev_0, rtac @{thm singletonI},
   936         CONVERSION (Conv.top_conv
   937           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   938         if n = 1 then K all_tac
   939         else (rtac (@{thm sum_case_cong} RS trans) THEN'
   940           rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
   941         rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
   942         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
   943           DETERM o EVERY' [rtac trans, rtac o_apply, rtac ssubst, rtac @{thm Pair_eq}, rtac conjI,
   944             rtac trans, rtac @{thm Shift_def},
   945             rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
   946             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
   947             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
   948             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
   949             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
   950               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   951                 dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE,
   952                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   953                   dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
   954                   atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
   955                 else etac (mk_InN_not_InM i' i'' RS notE)])
   956             (rev ks),
   957             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
   958             rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI,
   959             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
   960             rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
   961             rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
   962             dtac asm_rl, dtac asm_rl, dtac asm_rl,
   963             dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
   964             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
   965               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   966                 dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE,
   967                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   968                   dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
   969                   atac, atac, hyp_subst_tac, atac]
   970                 else etac (mk_InN_not_InM i' i'' RS notE)])
   971             (rev ks),
   972             rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI,
   973             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
   974             CONVERSION (Conv.top_conv
   975               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
   976             if n = 1 then K all_tac
   977             else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans),
   978             SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl,
   979             rtac refl])
   980         ks to_sbd_injs from_to_sbds)];
   981   in
   982     (rtac mor_cong THEN'
   983     EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
   984     stac mor_def THEN' rtac conjI THEN'
   985     CONJ_WRAP' fbetw_tac
   986       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
   987         ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
   988           (set_naturalss ~~ (coalg_setss ~~
   989             (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
   990     CONJ_WRAP' mor_tac
   991       (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
   992         ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~
   993           (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
   994   end;
   995 
   996 fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs =
   997   EVERY' [rtac @{thm congruentI}, dtac lsbisE,
   998     REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
   999     etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
  1000     rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
  1001     EVERY' (map (fn equiv_LSBIS =>
  1002       EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac @{thm set_mp}, atac])
  1003     equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
  1004     etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
  1005 
  1006 fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss =
  1007   EVERY' [stac coalg_def,
  1008     CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
  1009       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
  1010         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
  1011         EVERY' (map2 (fn set_natural => fn coalgT_set =>
  1012           EVERY' [rtac conjI, rtac (set_natural RS @{thm ord_eq_le_trans}),
  1013             rtac @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]},
  1014             etac coalgT_set])
  1015         (take m set_naturals) (take m coalgT_sets)),
  1016         CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) =>
  1017           EVERY' [rtac (set_natural RS @{thm ord_eq_le_trans}),
  1018             rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
  1019             rtac equiv_LSBIS, etac @{thm set_rev_mp}, etac coalgT_set])
  1020         (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))])
  1021     ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
  1022 
  1023 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
  1024   EVERY' [stac mor_def, rtac conjI,
  1025     CONJ_WRAP' (fn equiv_LSBIS =>
  1026       EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
  1027     equiv_LSBISs,
  1028     CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
  1029       EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
  1030         rtac congruent_str_final, atac, rtac o_apply])
  1031     (equiv_LSBISs ~~ congruent_str_finals)] 1;
  1032 
  1033 fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
  1034   {context = ctxt, prems = _} =
  1035   Local_Defs.unfold_tac ctxt defs THEN
  1036   EVERY' [rtac conjI,
  1037     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
  1038     CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
  1039       EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
  1040         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
  1041           EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
  1042             etac @{thm set_rev_mp}, rtac coalg_final_set, rtac Rep])
  1043         Abs_inverses (drop m coalg_final_sets))])
  1044     (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
  1045 
  1046 fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
  1047   Local_Defs.unfold_tac ctxt defs THEN
  1048   EVERY' [rtac conjI,
  1049     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
  1050     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
  1051 
  1052 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
  1053   EVERY' [rtac @{thm ssubst[of _ _ "%x. x"]}, rtac mor_UNIV,
  1054     CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
  1055       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
  1056         rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
  1057         rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
  1058         rtac (o_apply RS trans RS sym), rtac map_cong,
  1059         REPEAT_DETERM_N m o rtac refl,
  1060         EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)])
  1061     ((Abs_inverses ~~ morEs) ~~ ((unf_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
  1062 
  1063 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
  1064   sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
  1065   let
  1066     val n = length Rep_injects;
  1067   in
  1068     EVERY' [rtac rev_mp, ftac (bis_def RS @{thm subst[of _ _ "%x. x"]}),
  1069       REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
  1070       rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
  1071       rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
  1072       rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
  1073       rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,
  1074       rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls),
  1075       rtac impI,
  1076       CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
  1077         EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
  1078           rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
  1079           rtac @{thm ord_eq_le_trans}, rtac @{thm sym[OF relImage_relInvImage]},
  1080           rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
  1081           rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
  1082           rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
  1083           rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
  1084           rtac Rep_inject])
  1085       (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
  1086   end;
  1087 
  1088 fun mk_unique_mor_tac raw_coinds bis =
  1089   CONJ_WRAP' (fn raw_coind =>
  1090     EVERY' [rtac impI, rtac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), atac,
  1091       etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
  1092   raw_coinds 1;
  1093 
  1094 fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
  1095   CONJ_WRAP' (fn (raw_coind, coiter_def) =>
  1096     EVERY' [rtac ext, etac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), rtac mor,
  1097       rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
  1098       rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
  1099 
  1100 fun mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unfs
  1101   {context = ctxt, prems = _} =
  1102   Local_Defs.unfold_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
  1103     rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
  1104     EVERY' (map (fn thm =>
  1105       rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_unfs),
  1106     rtac sym, rtac @{thm id_apply}] 1;
  1107 
  1108 fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
  1109   Local_Defs.unfold_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
  1110     rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
  1111     REPEAT_DETERM_N m o rtac refl,
  1112     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
  1113 
  1114 fun mk_rel_coinduct_tac ks raw_coind bis_rel =
  1115   EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
  1116     CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
  1117     CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
  1118       REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
  1119     rtac impI, REPEAT_DETERM o etac conjE,
  1120     CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac @{thm set_mp},
  1121       rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
  1122 
  1123 fun mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids =
  1124   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct),
  1125     EVERY' (map2 (fn rel_mono => fn rel_Id =>
  1126       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
  1127         etac disjE, etac mp, atac, hyp_subst_tac, rtac (rel_mono RS @{thm set_mp}),
  1128         REPEAT_DETERM_N m o rtac @{thm subset_refl},
  1129         REPEAT_DETERM_N (length rel_monos) o rtac @{thm Id_subset},
  1130         rtac (rel_Id RS equalityD2 RS @{thm set_mp}), rtac @{thm IdI}])
  1131     rel_monos rel_Ids),
  1132     rtac impI, REPEAT_DETERM o etac conjE,
  1133     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1;
  1134 
  1135 fun mk_unf_coinduct_tac m ks raw_coind bis_def =
  1136   let
  1137     val n = length ks;
  1138   in
  1139     EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI,
  1140       CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
  1141       CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI,
  1142         rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
  1143         atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
  1144         etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
  1145         rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
  1146         CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
  1147           REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
  1148         ks])
  1149       ks,
  1150       rtac impI,
  1151       CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
  1152         rtac @{thm subst[OF pair_in_Id_conv]}, etac @{thm set_mp},
  1153         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
  1154   end;
  1155 
  1156 fun mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def bis_diag =
  1157   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts unf_coinduct),
  1158     EVERY' (map (fn i =>
  1159       EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
  1160         atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
  1161         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
  1162         etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
  1163         rtac exI, rtac conjI, etac conjI, atac,
  1164         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
  1165           rtac disjI2, rtac @{thm diagE}, etac @{thm set_mp}, atac])) ks])
  1166     ks),
  1167     rtac impI, REPEAT_DETERM o etac conjE,
  1168     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
  1169 
  1170 fun mk_map_tac m n cT coiter map_comp' map_cong =
  1171   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
  1172     rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
  1173     REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
  1174     REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
  1175     rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
  1176 
  1177 fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
  1178   EVERY' [rtac hset_minimal,
  1179     REPEAT_DETERM_N n o rtac @{thm Un_upper1},
  1180     REPEAT_DETERM_N n o
  1181       EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
  1182         EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnN n i), etac @{thm UN_I},
  1183           etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
  1184           EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
  1185       (1 upto n) set_hsets set_hset_hsetss)] 1;
  1186 
  1187 fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets =
  1188   EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
  1189     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
  1190     EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
  1191 
  1192 fun mk_map_id_tac maps coiter_unique coiter_unf =
  1193   EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
  1194     rtac coiter_unf] 1;
  1195 
  1196 fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique =
  1197   EVERY' [rtac coiter_unique,
  1198     EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
  1199       EVERY' (map rtac
  1200         ([@{thm o_assoc} RS trans,
  1201         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
  1202         @{thm o_assoc} RS trans RS sym,
  1203         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
  1204         @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
  1205         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
  1206         ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong] @
  1207         replicate m (@{thm id_o} RS fun_cong) @
  1208         replicate n (@{thm o_id} RS fun_cong))))
  1209     maps map_comps map_congs)] 1;
  1210 
  1211 val o_apply_trans_sym = o_apply RS trans RS sym;
  1212 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
  1213 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
  1214 
  1215 fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
  1216   set_hset_hsetsss =
  1217   let
  1218     val n = length map_comp's;
  1219     val ks = 1 upto n;
  1220   in
  1221     EVERY' ([rtac rev_mp,
  1222       coinduct_tac] @
  1223       maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets),
  1224         set_hset_hsetss) =>
  1225         [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
  1226          rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
  1227          REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
  1228          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
  1229          rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
  1230          EVERY' (maps (fn set_hset =>
  1231            [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
  1232            REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
  1233          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
  1234          CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
  1235            EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
  1236              etac @{thm set_rev_mp}, rtac @{thm ord_eq_le_trans}, rtac set_natural,
  1237              rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
  1238              REPEAT_DETERM o etac conjE,
  1239              CONJ_WRAP' (fn set_hset_hset =>
  1240                EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
  1241            (drop m set_naturals ~~ set_hset_hsetss)])
  1242         (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~
  1243           map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
  1244       [rtac impI,
  1245        CONJ_WRAP' (fn k =>
  1246          EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
  1247            rtac conjI, rtac refl, rtac refl]) ks]) 1
  1248   end
  1249 
  1250 fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
  1251   rtac coiter_unique 1 THEN
  1252   Local_Defs.unfold_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
  1253   ALLGOALS (etac sym);
  1254 
  1255 fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
  1256   {context = ctxt, prems = _} =
  1257   let
  1258     val n = length map_simps;
  1259   in
  1260     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
  1261       REPEAT_DETERM o rtac allI, SELECT_GOAL (Local_Defs.unfold_tac ctxt rec_0s),
  1262       CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
  1263       REPEAT_DETERM o rtac allI,
  1264       CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
  1265         [SELECT_GOAL (Local_Defs.unfold_tac ctxt
  1266           (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
  1267         rtac @{thm Un_cong}, rtac refl,
  1268         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
  1269           (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
  1270             REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
  1271       (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1
  1272   end;
  1273 
  1274 fun mk_set_natural_tac hset_def col_natural =
  1275   EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
  1276     (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
  1277     (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
  1278 
  1279 fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
  1280   let
  1281     val n = length rec_0s;
  1282   in
  1283     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
  1284       REPEAT_DETERM o rtac allI,
  1285       CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [@{thm ordIso_ordLeq_trans},
  1286         @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
  1287       REPEAT_DETERM o rtac allI,
  1288       CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
  1289         [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
  1290         rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
  1291         REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
  1292         EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
  1293           rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE,
  1294           etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
  1295       (rec_Sucs ~~ set_sbdss)] 1
  1296   end;
  1297 
  1298 fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
  1299   EVERY' (map rtac [@{thm ordIso_ordLeq_trans}, @{thm card_of_ordIso_subst}, hset_def,
  1300     ctrans, @{thm UNION_Cinfinite_bound}, @{thm ordIso_ordLeq_trans}, @{thm card_of_nat},
  1301     @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
  1302     ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
  1303 
  1304 fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
  1305   sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
  1306   let
  1307     val n = length isNode_hsets;
  1308     val in_hin_tac = rtac CollectI THEN'
  1309       CONJ_WRAP' (fn mor_hset => EVERY' (map etac
  1310         [mor_hset OF [coalgT, mor_T_final] RS sym RS @{thm ord_eq_le_trans},
  1311         arg_cong RS sym RS @{thm ord_eq_le_trans},
  1312         mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS @{thm ord_eq_le_trans}])) mor_hsets;
  1313   in
  1314     EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans,
  1315       rtac @{thm card_of_image}, rtac @{thm ordIso_ordLeq_trans},
  1316       rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
  1317       rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero},
  1318       rtac @{thm cexp_ordLeq_ccexp},  rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
  1319       rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order,
  1320       rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
  1321       rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1322       rtac @{thm set_mp}, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
  1323       rtac @{thm set_rev_mp}, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
  1324       rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
  1325       ftac (carT_def RS equalityD1 RS @{thm set_mp}),
  1326       REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  1327       rtac (carT_def RS equalityD2 RS @{thm set_mp}), rtac CollectI, REPEAT_DETERM o rtac exI,
  1328       rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
  1329       rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
  1330       CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) =>
  1331         EVERY' [rtac (mk_disjIN n i), rtac isNode_hset, atac, atac, atac, in_hin_tac])
  1332       (1 upto n ~~ isNode_hsets),
  1333       CONJ_WRAP' (fn isNode_hset =>
  1334         EVERY' [rtac ballI, rtac isNode_hset, atac, ftac CollectD, etac @{thm SuccD},
  1335           etac bspec, atac, in_hin_tac])
  1336       isNode_hsets,
  1337       atac, rtac isNode_hset, atac, atac, atac, in_hin_tac] 1
  1338   end;
  1339 
  1340 fun mk_bd_card_order_tac sbd_card_order =
  1341   EVERY' (map rtac [@{thm card_order_ccexp}, sbd_card_order, sbd_card_order]) 1;
  1342 
  1343 fun mk_bd_cinfinite_tac sbd_Cinfinite =
  1344   EVERY' (map rtac [@{thm cinfinite_ccexp}, @{thm ctwo_ordLeq_Cinfinite},
  1345     sbd_Cinfinite, sbd_Cinfinite]) 1;
  1346 
  1347 fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
  1348   let
  1349     val m = length set_incl_hsets;
  1350   in
  1351     EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
  1352       EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
  1353       CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
  1354       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
  1355       EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
  1356       CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
  1357       REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
  1358   end;
  1359 
  1360 fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
  1361   {context = ctxt, prems = _} =
  1362   Local_Defs.unfold_tac ctxt [coalg_def] THEN
  1363   CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
  1364     EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1365       REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  1366       hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  1367       EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  1368       pickWP_assms_tac,
  1369       SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), rtac impI,
  1370       REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1371       rtac CollectI,
  1372       REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
  1373       CONJ_WRAP' (fn set_natural =>
  1374         EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac set_natural,
  1375           rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
  1376       (drop m set_naturals)])
  1377   (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
  1378 
  1379 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
  1380   {context = ctxt, prems = _} =
  1381   let
  1382     val n = length map_comps;
  1383   in
  1384     Local_Defs.unfold_tac ctxt [mor_def] THEN
  1385     EVERY' [rtac conjI,
  1386       CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
  1387       CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
  1388         EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1389           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  1390           hyp_subst_tac,
  1391           SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}),
  1392           rtac (map_comp RS trans),
  1393           SELECT_GOAL (Local_Defs.unfold_tac ctxt (conv :: @{thms o_id id_o})),
  1394           rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
  1395           pickWP_assms_tac])
  1396       (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
  1397   end;
  1398 
  1399 val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
  1400 val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
  1401 
  1402 fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
  1403   Local_Defs.unfold_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
  1404   CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
  1405   CONJ_WRAP' (fn (coiter, map_comp) =>
  1406     EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  1407       hyp_subst_tac,
  1408       SELECT_GOAL (Local_Defs.unfold_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
  1409       rtac refl])
  1410   (coiters ~~ map_comps) 1;
  1411 
  1412 fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs
  1413   {context = ctxt, prems = _} =
  1414   let
  1415     val n = length rec_0s;
  1416     val ks = n downto 1;
  1417   in
  1418     EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
  1419       REPEAT_DETERM o rtac allI,
  1420       CONJ_WRAP' (fn thm => EVERY'
  1421         [rtac impI, rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
  1422       REPEAT_DETERM o rtac allI,
  1423       CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
  1424         EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1425           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  1426           hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  1427           EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  1428           pickWP_assms_tac,
  1429           rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1430           rtac @{thm ord_eq_le_trans}, rtac rec_Suc,
  1431           rtac @{thm Un_least},
  1432           SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, nth set_naturals (j - 1),
  1433             @{thm prod.cases}]),
  1434           etac @{thm ord_eq_le_trans[OF trans [OF fun_cong[OF image_id] id_apply]]},
  1435           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
  1436             EVERY' [rtac @{thm UN_least},
  1437               SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
  1438               etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
  1439               dtac (mk_conjunctN n i), etac mp, etac @{thm set_mp}, atac])
  1440           (ks ~~ rev (drop m set_naturals))])
  1441       (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
  1442   end;
  1443 
  1444 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
  1445   mor_unique pick_cols hset_defs =
  1446   EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF wpull_def]}, REPEAT_DETERM o rtac allI, rtac impI,
  1447     REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
  1448     rtac box_equals, rtac mor_unique,
  1449     rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1450     rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1451     rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1452     rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1453     rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv},
  1454     rtac box_equals, rtac mor_unique,
  1455     rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1456     rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1457     rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1458     rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1459     rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
  1460     rtac CollectI,
  1461     CONJ_WRAP' (fn (pick, def) =>
  1462       EVERY' [rtac (def RS @{thm ord_eq_le_trans}), rtac @{thm UN_least},
  1463         rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1464         rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1465         rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
  1466     (pick_cols ~~ hset_defs)] 1;
  1467 
  1468 fun mk_wit_tac n unf_flds set_simp wit coind_wits {context = ctxt, prems = _} =
  1469   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
  1470   REPEAT_DETERM (atac 1 ORELSE
  1471     EVERY' [dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
  1472     K (Local_Defs.unfold_tac ctxt unf_flds),
  1473     REPEAT_DETERM_N n o etac UnE,
  1474     REPEAT_DETERM o
  1475       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
  1476         (eresolve_tac wit ORELSE'
  1477         (dresolve_tac wit THEN'
  1478           (etac FalseE ORELSE'
  1479           EVERY' [hyp_subst_tac, dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
  1480             K (Local_Defs.unfold_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1);
  1481 
  1482 fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
  1483   rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
  1484   Local_Defs.unfold_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
  1485   ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
  1486   ALLGOALS (TRY o
  1487     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
  1488 
  1489 fun mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld
  1490   set_naturals set_incls set_set_inclss =
  1491   let
  1492     val m = length set_incls;
  1493     val n = length set_set_inclss;
  1494     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
  1495     val in_Jrel = nth in_Jrels (i - 1);
  1496     val if_tac =
  1497       EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  1498         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1499         EVERY' (map2 (fn set_natural => fn set_incl =>
  1500           EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac set_natural,
  1501             rtac @{thm ord_eq_le_trans}, rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
  1502             etac (set_incl RS @{thm subset_trans})])
  1503         passive_set_naturals set_incls),
  1504         CONJ_WRAP' (fn (in_Jrel, (set_natural, set_set_incls)) =>
  1505           EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_natural, rtac @{thm image_subsetI},
  1506             rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1507             CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
  1508             rtac conjI, rtac refl, rtac refl])
  1509         (in_Jrels ~~ (active_set_naturals ~~ set_set_inclss)),
  1510         CONJ_WRAP' (fn conv =>
  1511           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
  1512           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  1513           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
  1514           rtac trans, rtac sym, rtac map_simp, rtac (unf_inject RS iffD2), atac])
  1515         @{thms fst_conv snd_conv}];
  1516     val only_if_tac =
  1517       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  1518         rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1519         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
  1520           EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_simp, rtac @{thm Un_least},
  1521             rtac @{thm ord_eq_le_trans}, rtac box_equals, rtac passive_set_natural,
  1522             rtac (unf_fld RS sym RS arg_cong), rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
  1523             atac,
  1524             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  1525               (fn (active_set_natural, in_Jrel) => EVERY' [rtac @{thm ord_eq_le_trans},
  1526                 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
  1527                 rtac active_set_natural, rtac (unf_fld RS sym RS arg_cong), rtac @{thm UN_least},
  1528                 dtac @{thm set_rev_mp}, etac @{thm image_mono}, etac imageE,
  1529                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1),
  1530                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  1531                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  1532                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  1533             (rev (active_set_naturals ~~ in_Jrels))])
  1534         (set_simps ~~ passive_set_naturals),
  1535         rtac conjI,
  1536         REPEAT_DETERM_N 2 o EVERY'[rtac (unf_inject RS iffD1), rtac trans, rtac map_simp,
  1537           rtac box_equals, rtac map_comp, rtac (unf_fld RS sym RS arg_cong), rtac trans,
  1538           rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  1539           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac @{thm set_rev_mp}, atac,
  1540             dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex},
  1541             REPEAT_DETERM o etac conjE, atac]) in_Jrels),
  1542           atac]]
  1543   in
  1544     EVERY' [rtac iffI, if_tac, only_if_tac] 1
  1545   end;
  1546 
  1547 end;