src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49510 ba50d204095e
parent 49509 163914705f8d
child 49516 d4859efc1096
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Fri Sep 21 16:45:06 2012 +0200
     1.3 @@ -0,0 +1,1554 @@
     1.4 +(*  Title:      HOL/BNF/Tools/bnf_gfp_tactics.ML
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +    Copyright   2012
     1.9 +
    1.10 +Tactics for the codatatype construction.
    1.11 +*)
    1.12 +
    1.13 +signature BNF_GFP_TACTICS =
    1.14 +sig
    1.15 +  val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic
    1.16 +  val mk_bd_card_order_tac: thm -> tactic
    1.17 +  val mk_bd_cinfinite_tac: thm -> tactic
    1.18 +  val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
    1.19 +    {prems: 'a, context: Proof.context} -> tactic
    1.20 +  val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
    1.21 +  val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.22 +  val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
    1.23 +  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    1.24 +  val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
    1.25 +    {prems: 'a, context: Proof.context} -> tactic
    1.26 +  val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
    1.27 +  val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
    1.28 +    {prems: 'a, context: Proof.context} -> tactic
    1.29 +  val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
    1.30 +    tactic
    1.31 +  val mk_coalg_set_tac: thm -> tactic
    1.32 +  val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->
    1.33 +    {prems: 'a, context: Proof.context} -> tactic
    1.34 +  val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
    1.35 +    {prems: 'a, context: Proof.context} -> tactic
    1.36 +  val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
    1.37 +    thm list list -> tactic
    1.38 +  val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
    1.39 +    {prems: 'a, context: Proof.context} -> tactic
    1.40 +  val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
    1.41 +  val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
    1.42 +    {prems: 'a, context: Proof.context} -> tactic
    1.43 +  val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
    1.44 +  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.45 +    thm -> thm -> tactic
    1.46 +  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    1.47 +    {prems: 'a, context: Proof.context} -> tactic
    1.48 +  val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
    1.49 +  val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    1.50 +  val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
    1.51 +    {prems: 'a, context: Proof.context} -> tactic
    1.52 +  val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    1.53 +    thm -> thm -> thm -> tactic
    1.54 +  val mk_incl_lsbis_tac: int -> int -> thm -> tactic
    1.55 +  val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.56 +  val mk_length_Lev'_tac: thm -> tactic
    1.57 +  val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    1.58 +  val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
    1.59 +  val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
    1.60 +    thm list list -> thm list list list -> tactic
    1.61 +  val mk_map_id_tac: thm list -> thm -> thm -> tactic
    1.62 +  val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
    1.63 +  val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.64 +  val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.65 +  val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
    1.66 +    thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.67 +  val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
    1.68 +  val mk_mor_UNIV_tac: thm list -> thm -> tactic
    1.69 +  val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    1.70 +    thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
    1.71 +    thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    1.72 +    thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    1.73 +    {prems: 'a, context: Proof.context} -> tactic
    1.74 +  val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    1.75 +  val mk_mor_elim_tac: thm -> tactic
    1.76 +  val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
    1.77 +    thm list -> thm list list -> thm list list -> tactic
    1.78 +  val mk_mor_hset_tac: thm -> thm -> tactic
    1.79 +  val mk_mor_incl_tac: thm -> thm list -> tactic
    1.80 +  val mk_mor_str_tac: 'a list -> thm -> tactic
    1.81 +  val mk_mor_sum_case_tac: 'a list -> thm -> tactic
    1.82 +  val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
    1.83 +    {prems: thm list, context: Proof.context} -> tactic
    1.84 +  val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
    1.85 +    {prems: thm list, context: Proof.context} -> tactic
    1.86 +  val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
    1.87 +    {prems: 'a, context: Proof.context} -> tactic
    1.88 +  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    1.89 +    thm list -> tactic
    1.90 +  val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    1.91 +  val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
    1.92 +  val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
    1.93 +    thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
    1.94 +    tactic
    1.95 +  val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    1.96 +    thm list -> thm list -> thm -> thm list -> tactic
    1.97 +  val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
    1.98 +  val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
    1.99 +  val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
   1.100 +    thm list list -> tactic
   1.101 +  val mk_set_bd_tac: thm -> thm -> thm -> tactic
   1.102 +  val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
   1.103 +  val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
   1.104 +    thm list list -> thm list list -> tactic
   1.105 +  val mk_set_incl_hin_tac: thm list -> tactic
   1.106 +  val mk_set_incl_hset_tac: thm -> thm -> tactic
   1.107 +  val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   1.108 +  val mk_set_natural_tac: thm -> thm -> tactic
   1.109 +  val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
   1.110 +    thm list list -> thm list list -> tactic
   1.111 +  val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
   1.112 +  val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   1.113 +  val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
   1.114 +    thm list -> thm list -> tactic
   1.115 +  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
   1.116 +    thm list -> thm list -> thm list list -> tactic
   1.117 +  val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
   1.118 +    cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
   1.119 +    thm list list -> thm list list -> thm -> thm list list -> tactic
   1.120 +  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   1.121 +  val mk_unique_mor_tac: thm list -> thm -> tactic
   1.122 +  val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
   1.123 +    {prems: 'a, context: Proof.context} -> tactic
   1.124 +  val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic
   1.125 +end;
   1.126 +
   1.127 +structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
   1.128 +struct
   1.129 +
   1.130 +open BNF_Tactics
   1.131 +open BNF_Util
   1.132 +open BNF_FP
   1.133 +open BNF_GFP_Util
   1.134 +
   1.135 +val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
   1.136 +val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
   1.137 +val nat_induct = @{thm nat_induct};
   1.138 +val o_apply_trans_sym = o_apply RS trans RS sym;
   1.139 +val ord_eq_le_trans = @{thm ord_eq_le_trans};
   1.140 +val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
   1.141 +  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
   1.142 +val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
   1.143 +val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
   1.144 +val sum_case_weak_cong = @{thm sum_case_weak_cong};
   1.145 +val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
   1.146 +
   1.147 +fun mk_coalg_set_tac coalg_def =
   1.148 +  dtac (coalg_def RS iffD1) 1 THEN
   1.149 +  REPEAT_DETERM (etac conjE 1) THEN
   1.150 +  EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   1.151 +  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
   1.152 +
   1.153 +fun mk_mor_elim_tac mor_def =
   1.154 +  (dtac (subst OF [mor_def]) THEN'
   1.155 +  REPEAT o etac conjE THEN'
   1.156 +  TRY o rtac @{thm image_subsetI} THEN'
   1.157 +  etac bspec THEN'
   1.158 +  atac) 1;
   1.159 +
   1.160 +fun mk_mor_incl_tac mor_def map_id's =
   1.161 +  (stac mor_def THEN'
   1.162 +  rtac conjI THEN'
   1.163 +  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))
   1.164 +    map_id's THEN'
   1.165 +  CONJ_WRAP' (fn thm =>
   1.166 +   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
   1.167 +  map_id's) 1;
   1.168 +
   1.169 +fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   1.170 +  let
   1.171 +    fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
   1.172 +    fun mor_tac ((mor_image, morE), map_comp_id) =
   1.173 +      EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
   1.174 +        etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
   1.175 +  in
   1.176 +    (stac mor_def THEN' rtac conjI THEN'
   1.177 +    CONJ_WRAP' fbetw_tac mor_images THEN'
   1.178 +    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
   1.179 +  end;
   1.180 +
   1.181 +fun mk_mor_UNIV_tac morEs mor_def =
   1.182 +  let
   1.183 +    val n = length morEs;
   1.184 +    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
   1.185 +      rtac UNIV_I, rtac sym, rtac o_apply];
   1.186 +  in
   1.187 +    EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
   1.188 +    stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
   1.189 +    CONJ_WRAP' (fn i =>
   1.190 +      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1
   1.191 +  end;
   1.192 +
   1.193 +fun mk_mor_str_tac ks mor_UNIV =
   1.194 +  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
   1.195 +
   1.196 +fun mk_mor_sum_case_tac ks mor_UNIV =
   1.197 +  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1;
   1.198 +
   1.199 +fun mk_set_incl_hset_tac def rec_Suc =
   1.200 +  EVERY' (stac def ::
   1.201 +    map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
   1.202 +      sym, rec_Suc]) 1;
   1.203 +
   1.204 +fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
   1.205 +  EVERY' (map (TRY oo stac) defs @
   1.206 +    map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
   1.207 +      mk_UnIN n i] @
   1.208 +    [etac @{thm UN_I}, atac]) 1;
   1.209 +
   1.210 +fun mk_set_incl_hin_tac incls =
   1.211 +  if null incls then rtac subset_UNIV 1
   1.212 +  else EVERY' [rtac subsetI, rtac CollectI,
   1.213 +    CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
   1.214 +
   1.215 +fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
   1.216 +  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.217 +    REPEAT_DETERM o rtac allI,
   1.218 +    CONJ_WRAP' (fn thm => EVERY'
   1.219 +      [rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
   1.220 +    REPEAT_DETERM o rtac allI,
   1.221 +    CONJ_WRAP' (fn rec_Suc => EVERY'
   1.222 +      [rtac ord_eq_le_trans, rtac rec_Suc,
   1.223 +        if m = 0 then K all_tac
   1.224 +        else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
   1.225 +        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   1.226 +          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
   1.227 +            rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
   1.228 +      rec_Sucs] 1;
   1.229 +
   1.230 +fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
   1.231 +  (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
   1.232 +    rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
   1.233 +    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
   1.234 +    REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
   1.235 +
   1.236 +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =
   1.237 +  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.238 +    REPEAT_DETERM o rtac allI,
   1.239 +    CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
   1.240 +    REPEAT_DETERM o rtac allI,
   1.241 +    CONJ_WRAP'
   1.242 +      (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) =>
   1.243 +        EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
   1.244 +          if m = 0 then K all_tac
   1.245 +          else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
   1.246 +            rtac (nth passive_set_naturals (j - 1) RS sym),
   1.247 +            rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
   1.248 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   1.249 +            (fn (i, (set_natural, coalg_set)) =>
   1.250 +              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
   1.251 +                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,
   1.252 +                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
   1.253 +                ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
   1.254 +                REPEAT_DETERM o etac allE, atac, atac])
   1.255 +            (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])
   1.256 +      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;
   1.257 +
   1.258 +fun mk_mor_hset_tac hset_def mor_hset_rec =
   1.259 +  EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
   1.260 +    atac, atac, rtac (hset_def RS sym)] 1
   1.261 +
   1.262 +fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
   1.263 +  let
   1.264 +    val n = length srel_O_Grs;
   1.265 +    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
   1.266 +
   1.267 +    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
   1.268 +      EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
   1.269 +        etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
   1.270 +        rtac (srel_O_Gr RS equalityD2 RS set_mp),
   1.271 +        rtac @{thm relcompI}, rtac @{thm converseI},
   1.272 +        EVERY' (map (fn thm =>
   1.273 +          EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.274 +            rtac CollectI,
   1.275 +            CONJ_WRAP' (fn (i, thm) =>
   1.276 +              if i <= m
   1.277 +              then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
   1.278 +                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
   1.279 +              else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
   1.280 +                rtac trans_fun_cong_image_id_id_apply, atac])
   1.281 +            (1 upto (m + n) ~~ set_naturals),
   1.282 +            rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
   1.283 +            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
   1.284 +          @{thms fst_diag_id snd_diag_id})];
   1.285 +
   1.286 +    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
   1.287 +      EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
   1.288 +        etac allE, etac allE, etac impE, atac,
   1.289 +        dtac (srel_O_Gr RS equalityD1 RS set_mp),
   1.290 +        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
   1.291 +        REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
   1.292 +        REPEAT_DETERM o dtac Pair_eqD,
   1.293 +        REPEAT_DETERM o etac conjE,
   1.294 +        hyp_subst_tac,
   1.295 +        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.296 +        rtac bexI, rtac conjI, rtac trans, rtac map_comp,
   1.297 +        REPEAT_DETERM_N m o stac @{thm id_o},
   1.298 +        REPEAT_DETERM_N n o stac @{thm o_id},
   1.299 +        etac sym, rtac trans, rtac map_comp,
   1.300 +        REPEAT_DETERM_N m o stac @{thm id_o},
   1.301 +        REPEAT_DETERM_N n o stac @{thm o_id},
   1.302 +        rtac trans, rtac map_cong,
   1.303 +        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
   1.304 +        REPEAT_DETERM_N n o rtac refl,
   1.305 +        etac sym, rtac CollectI,
   1.306 +        CONJ_WRAP' (fn (i, thm) =>
   1.307 +          if i <= m
   1.308 +          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
   1.309 +            rtac @{thm diag_fst}, etac set_mp, atac]
   1.310 +          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
   1.311 +            rtac trans_fun_cong_image_id_id_apply, atac])
   1.312 +        (1 upto (m + n) ~~ set_naturals)];
   1.313 +  in
   1.314 +    EVERY' [rtac (bis_def RS trans),
   1.315 +      rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
   1.316 +      etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
   1.317 +  end;
   1.318 +
   1.319 +fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =
   1.320 +  EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),
   1.321 +    REPEAT_DETERM o etac conjE, rtac conjI,
   1.322 +    CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
   1.323 +      rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
   1.324 +    CONJ_WRAP' (fn (srel_cong, srel_converse) =>
   1.325 +      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
   1.326 +        rtac (srel_cong RS trans),
   1.327 +        REPEAT_DETERM_N m o rtac @{thm diag_converse},
   1.328 +        REPEAT_DETERM_N (length srel_congs) o rtac refl,
   1.329 +        rtac srel_converse,
   1.330 +        REPEAT_DETERM o etac allE,
   1.331 +        rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
   1.332 +
   1.333 +fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
   1.334 +  EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
   1.335 +    REPEAT_DETERM o etac conjE, rtac conjI,
   1.336 +    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
   1.337 +    CONJ_WRAP' (fn (srel_cong, srel_O) =>
   1.338 +      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
   1.339 +        rtac (srel_cong RS trans),
   1.340 +        REPEAT_DETERM_N m o rtac @{thm diag_Comp},
   1.341 +        REPEAT_DETERM_N (length srel_congs) o rtac refl,
   1.342 +        rtac srel_O,
   1.343 +        etac @{thm relcompE},
   1.344 +        REPEAT_DETERM o dtac Pair_eqD,
   1.345 +        etac conjE, hyp_subst_tac,
   1.346 +        REPEAT_DETERM o etac allE, rtac @{thm relcompI},
   1.347 +        etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
   1.348 +
   1.349 +fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
   1.350 +  {context = ctxt, prems = _} =
   1.351 +  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
   1.352 +  EVERY' [rtac conjI,
   1.353 +    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
   1.354 +    CONJ_WRAP' (fn (coalg_in, morE) =>
   1.355 +      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,
   1.356 +        etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},
   1.357 +        etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1;
   1.358 +
   1.359 +fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
   1.360 +  let
   1.361 +    val n = length in_monos;
   1.362 +    val ks = 1 upto n;
   1.363 +  in
   1.364 +    unfold_thms_tac ctxt [bis_def] THEN
   1.365 +    EVERY' [rtac conjI,
   1.366 +      CONJ_WRAP' (fn i =>
   1.367 +        EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
   1.368 +          dtac conjunct1, etac (mk_conjunctN n i)]) ks,
   1.369 +      CONJ_WRAP' (fn (i, in_mono) =>
   1.370 +        EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
   1.371 +          dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
   1.372 +          atac, etac bexE, rtac bexI, atac, rtac in_mono,
   1.373 +          REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},
   1.374 +          atac]) (ks ~~ in_monos)] 1
   1.375 +  end;
   1.376 +
   1.377 +fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
   1.378 +  let
   1.379 +    val n = length lsbis_defs;
   1.380 +  in
   1.381 +    EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
   1.382 +      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
   1.383 +      hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   1.384 +  end;
   1.385 +
   1.386 +fun mk_incl_lsbis_tac n i lsbis_def =
   1.387 +  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
   1.388 +    REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
   1.389 +    rtac (mk_nth_conv n i)] 1;
   1.390 +
   1.391 +fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
   1.392 +  EVERY' [rtac (@{thm equiv_def} RS iffD2),
   1.393 +
   1.394 +    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
   1.395 +    rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
   1.396 +    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
   1.397 +
   1.398 +    rtac conjI, rtac (@{thm sym_def} RS iffD2),
   1.399 +    rtac allI, rtac allI, rtac impI, rtac set_mp,
   1.400 +    rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
   1.401 +
   1.402 +    rtac (@{thm trans_def} RS iffD2),
   1.403 +    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
   1.404 +    rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
   1.405 +    etac @{thm relcompI}, atac] 1;
   1.406 +
   1.407 +fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =
   1.408 +  let
   1.409 +    val n = length strT_defs;
   1.410 +    val ks = 1 upto n;
   1.411 +    fun coalg_tac (i, ((passive_sets, active_sets), def)) =
   1.412 +      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.413 +        hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
   1.414 +        rtac (mk_sum_casesN n i), rtac CollectI,
   1.415 +        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
   1.416 +          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])
   1.417 +          passive_sets),
   1.418 +        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
   1.419 +          rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
   1.420 +          rtac conjI,
   1.421 +          rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
   1.422 +            etac equalityD1, etac CollectD,
   1.423 +          rtac conjI, etac @{thm Shift_clists},
   1.424 +          rtac conjI, etac @{thm Shift_prefCl},
   1.425 +          rtac conjI, rtac ballI,
   1.426 +            rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
   1.427 +            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
   1.428 +            etac bspec, etac @{thm ShiftD},
   1.429 +            CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
   1.430 +              dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
   1.431 +              dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
   1.432 +              REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
   1.433 +              rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
   1.434 +              rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
   1.435 +              REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   1.436 +              CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
   1.437 +                rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
   1.438 +                rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
   1.439 +          rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],
   1.440 +          etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,
   1.441 +          dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,
   1.442 +          etac @{thm set_mp[OF equalityD1]}, atac,
   1.443 +          REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
   1.444 +          rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
   1.445 +          etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
   1.446 +          REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   1.447 +          CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
   1.448 +            rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
   1.449 +            rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   1.450 +  in
   1.451 +    unfold_thms_tac ctxt defs THEN
   1.452 +    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
   1.453 +  end;
   1.454 +
   1.455 +fun mk_card_of_carT_tac m isNode_defs sbd_sbd
   1.456 +  sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
   1.457 +  let
   1.458 +    val n = length isNode_defs;
   1.459 +  in
   1.460 +    EVERY' [rtac (Thm.permute_prems 0 1 ctrans),
   1.461 +      rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp},
   1.462 +      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   1.463 +      rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},
   1.464 +      rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,
   1.465 +      rtac ctrans, rtac @{thm card_of_diff},
   1.466 +      rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},
   1.467 +      rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,
   1.468 +      rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
   1.469 +      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   1.470 +      rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists},
   1.471 +      rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,
   1.472 +      rtac @{thm clists_Cinfinite},
   1.473 +      if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
   1.474 +      rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
   1.475 +      rtac sbd_Cinfinite,
   1.476 +      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   1.477 +      rtac @{thm Cnotzero_clists},
   1.478 +      rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc},
   1.479 +      rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},
   1.480 +      rtac ctrans, rtac @{thm cexp_mono},
   1.481 +      rtac @{thm ordLeq_ordIso_trans},
   1.482 +      CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1
   1.483 +          (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}
   1.484 +        RSN (3, @{thm Un_Cinfinite_bound}))))
   1.485 +        (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),
   1.486 +      rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1},
   1.487 +      REPEAT_DETERM_N m o rtac @{thm csum_cong2},
   1.488 +      CONJ_WRAP_GEN' (rtac @{thm csum_cong})
   1.489 +        (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,
   1.490 +      rtac sbd_Card_order,
   1.491 +      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   1.492 +      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   1.493 +      rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},
   1.494 +      rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,
   1.495 +      rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp},
   1.496 +      rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2},
   1.497 +      rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac,
   1.498 +      rtac @{thm card_of_Card_order},
   1.499 +      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},
   1.500 +      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
   1.501 +      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2_Cnotzero},
   1.502 +      rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
   1.503 +      rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
   1.504 +      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod},
   1.505 +      rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
   1.506 +      rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
   1.507 +      rtac @{thm ordIso_transitive},
   1.508 +      REPEAT_DETERM_N m o rtac @{thm csum_cong2},
   1.509 +      rtac sbd_sbd,
   1.510 +      BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
   1.511 +        FIRST' [rtac @{thm card_of_Card_order},
   1.512 +          rtac @{thm Card_order_csum}, rtac sbd_Card_order])
   1.513 +        @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
   1.514 +        (1 upto m + 1) (m + 1 :: (1 upto m)),
   1.515 +      if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}],
   1.516 +      rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,
   1.517 +      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
   1.518 +      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
   1.519 +      rtac @{thm Card_order_ctwo},
   1.520 +      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order,
   1.521 +      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},
   1.522 +      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   1.523 +      rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
   1.524 +      rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
   1.525 +      rtac sbd_Cinfinite,
   1.526 +      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
   1.527 +      rtac sbd_Cnotzero,
   1.528 +      rtac @{thm card_of_mono1}, rtac subsetI,
   1.529 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
   1.530 +      rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
   1.531 +      rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
   1.532 +      rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
   1.533 +      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
   1.534 +      rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
   1.535 +      CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
   1.536 +        [rtac (mk_UnIN n i), dtac (def RS iffD1),
   1.537 +        REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
   1.538 +        REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   1.539 +        CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
   1.540 +          rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},
   1.541 +          rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
   1.542 +      atac] 1
   1.543 +  end;
   1.544 +
   1.545 +fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
   1.546 +  EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.547 +    REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.548 +    dtac Pair_eqD,
   1.549 +    etac conjE, hyp_subst_tac,
   1.550 +    dtac (isNode_def RS iffD1),
   1.551 +    REPEAT_DETERM o eresolve_tac [exE, conjE],
   1.552 +    rtac (equalityD2 RS set_mp),
   1.553 +    rtac (strT_def RS arg_cong RS trans),
   1.554 +    etac (arg_cong RS trans),
   1.555 +    fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
   1.556 +    rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
   1.557 +    etac @{thm prefCl_Succ}, atac] 1;
   1.558 +
   1.559 +fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   1.560 +  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss =
   1.561 +  let
   1.562 +    val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss;
   1.563 +    val ks = 1 upto n;
   1.564 +    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) =
   1.565 +      CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
   1.566 +        (if i = i'
   1.567 +        then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
   1.568 +          rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
   1.569 +          rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
   1.570 +          rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
   1.571 +          rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
   1.572 +        else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.573 +          REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
   1.574 +          dtac conjunct2, dtac Pair_eqD, etac conjE,
   1.575 +          hyp_subst_tac, dtac (isNode_def RS iffD1),
   1.576 +          REPEAT_DETERM o eresolve_tac [exE, conjE],
   1.577 +          rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
   1.578 +      (ks ~~ (carT_defs ~~ isNode_defs));
   1.579 +    fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =
   1.580 +      dtac (mk_conjunctN n i) THEN'
   1.581 +      CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>
   1.582 +        EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,
   1.583 +          rtac (coalgT RS coalg_set RS set_mp), atac, etac carT_set, atac, atac,
   1.584 +          etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,
   1.585 +          rtac set_hset_incl_hset, etac carT_set, atac, atac])
   1.586 +      (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));
   1.587 +  in
   1.588 +    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
   1.589 +      REPEAT_DETERM o rtac allI, rtac impI,
   1.590 +      CONJ_WRAP' base_tac
   1.591 +        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))),
   1.592 +      REPEAT_DETERM o rtac allI, rtac impI,
   1.593 +      REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
   1.594 +      CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
   1.595 +        CONJ_WRAP_GEN' (K all_tac) step_tac
   1.596 +          (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1
   1.597 +  end;
   1.598 +
   1.599 +fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} =
   1.600 +  let
   1.601 +    val m = length strT_hsets;
   1.602 +  in
   1.603 +    if m = 0 then atac 1
   1.604 +    else (unfold_thms_tac ctxt [isNode_def] THEN
   1.605 +      EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.606 +        rtac exI, rtac conjI, atac,
   1.607 +        CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
   1.608 +          else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac])
   1.609 +        (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
   1.610 +  end;
   1.611 +
   1.612 +fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
   1.613 +  let
   1.614 +    val n = length Lev_0s;
   1.615 +    val ks = 1 upto n;
   1.616 +  in
   1.617 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.618 +      REPEAT_DETERM o rtac allI,
   1.619 +      CONJ_WRAP' (fn Lev_0 =>
   1.620 +        EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,
   1.621 +      REPEAT_DETERM o rtac allI,
   1.622 +      CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
   1.623 +        EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
   1.624 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   1.625 +            (fn (i, to_sbd) => EVERY' [rtac subsetI,
   1.626 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.627 +              rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
   1.628 +              etac set_rev_mp, REPEAT_DETERM o etac allE,
   1.629 +              etac (mk_conjunctN n i)])
   1.630 +          (rev (ks ~~ to_sbds))])
   1.631 +      (Lev_Sucs ~~ to_sbdss)] 1
   1.632 +  end;
   1.633 +
   1.634 +fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
   1.635 +  let
   1.636 +    val n = length Lev_0s;
   1.637 +    val ks = n downto 1;
   1.638 +  in
   1.639 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.640 +      REPEAT_DETERM o rtac allI,
   1.641 +      CONJ_WRAP' (fn Lev_0 =>
   1.642 +        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.643 +          etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
   1.644 +      REPEAT_DETERM o rtac allI,
   1.645 +      CONJ_WRAP' (fn Lev_Suc =>
   1.646 +        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.647 +          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.648 +            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.649 +              rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
   1.650 +              REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
   1.651 +      Lev_Sucs] 1
   1.652 +  end;
   1.653 +
   1.654 +fun mk_length_Lev'_tac length_Lev =
   1.655 +  EVERY' [ftac length_Lev, etac ssubst, atac] 1;
   1.656 +
   1.657 +fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
   1.658 +  let
   1.659 +    val n = length Lev_0s;
   1.660 +    val ks = n downto 1;
   1.661 +  in
   1.662 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.663 +      REPEAT_DETERM o rtac allI,
   1.664 +      CONJ_WRAP' (fn Lev_0 =>
   1.665 +        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.666 +          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
   1.667 +          hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   1.668 +          rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
   1.669 +      REPEAT_DETERM o rtac allI,
   1.670 +      CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
   1.671 +        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.672 +          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.673 +            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.674 +              dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
   1.675 +              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   1.676 +              rtac Lev_0, rtac @{thm singletonI},
   1.677 +              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
   1.678 +              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
   1.679 +              rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
   1.680 +              rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   1.681 +              etac mp, etac conjI, atac]) ks])
   1.682 +      (Lev_0s ~~ Lev_Sucs)] 1
   1.683 +  end;
   1.684 +
   1.685 +fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
   1.686 +  let
   1.687 +    val n = length rv_Nils;
   1.688 +    val ks = 1 upto n;
   1.689 +  in
   1.690 +    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
   1.691 +      REPEAT_DETERM o rtac allI,
   1.692 +      CONJ_WRAP' (fn rv_Cons =>
   1.693 +        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
   1.694 +          rtac (@{thm append_Nil} RS arg_cong RS trans),
   1.695 +          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
   1.696 +        (ks ~~ rv_Nils))
   1.697 +      rv_Conss,
   1.698 +      REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
   1.699 +      EVERY' (map (fn i =>
   1.700 +        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   1.701 +          CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
   1.702 +            rtac (@{thm append_Cons} RS arg_cong RS trans),
   1.703 +            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
   1.704 +            rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
   1.705 +          ks])
   1.706 +        rv_Conss)
   1.707 +      ks)] 1
   1.708 +  end;
   1.709 +
   1.710 +fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
   1.711 +  let
   1.712 +    val n = length Lev_0s;
   1.713 +    val ks = 1 upto n;
   1.714 +  in
   1.715 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.716 +      REPEAT_DETERM o rtac allI,
   1.717 +      CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
   1.718 +        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
   1.719 +          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
   1.720 +          rtac (rv_Nil RS arg_cong RS iffD2),
   1.721 +          rtac (mk_sum_casesN n i RS iffD2),
   1.722 +          CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
   1.723 +      (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
   1.724 +      REPEAT_DETERM o rtac allI,
   1.725 +      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
   1.726 +        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.727 +          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.728 +            (fn (i, (from_to_sbd, coalg_set)) =>
   1.729 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.730 +              rtac (rv_Cons RS arg_cong RS iffD2),
   1.731 +              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
   1.732 +              etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   1.733 +              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
   1.734 +              etac coalg_set, atac])
   1.735 +          (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
   1.736 +      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
   1.737 +  end;
   1.738 +
   1.739 +fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   1.740 +  let
   1.741 +    val n = length Lev_0s;
   1.742 +    val ks = 1 upto n;
   1.743 +  in
   1.744 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.745 +      REPEAT_DETERM o rtac allI,
   1.746 +      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   1.747 +        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.748 +          etac @{thm singletonE}, hyp_subst_tac,
   1.749 +          CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   1.750 +            (if i = i'
   1.751 +            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
   1.752 +              CONJ_WRAP' (fn (i'', Lev_0'') =>
   1.753 +                EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
   1.754 +                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
   1.755 +                  rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
   1.756 +                  etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
   1.757 +                  rtac @{thm singletonI}])
   1.758 +              (ks ~~ Lev_0s)]
   1.759 +            else etac (mk_InN_not_InM i' i RS notE)))
   1.760 +          ks])
   1.761 +      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
   1.762 +      REPEAT_DETERM o rtac allI,
   1.763 +      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
   1.764 +        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.765 +          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.766 +            (fn (i, from_to_sbd) =>
   1.767 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.768 +                CONJ_WRAP' (fn i' => rtac impI THEN'
   1.769 +                  CONJ_WRAP' (fn i'' =>
   1.770 +                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
   1.771 +                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
   1.772 +                      rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
   1.773 +                      rtac conjI, atac, dtac (sym RS trans RS sym),
   1.774 +                      rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
   1.775 +                      etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   1.776 +                      dtac (mk_conjunctN n i), dtac mp, atac,
   1.777 +                      dtac (mk_conjunctN n i'), dtac mp, atac,
   1.778 +                      dtac (mk_conjunctN n i''), etac mp, atac])
   1.779 +                  ks)
   1.780 +                ks])
   1.781 +          (rev (ks ~~ from_to_sbds))])
   1.782 +      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
   1.783 +  end;
   1.784 +
   1.785 +fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
   1.786 +  let
   1.787 +    val n = length Lev_0s;
   1.788 +    val ks = 1 upto n;
   1.789 +  in
   1.790 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.791 +      REPEAT_DETERM o rtac allI,
   1.792 +      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   1.793 +        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.794 +          etac @{thm singletonE}, hyp_subst_tac,
   1.795 +          CONJ_WRAP' (fn i' => rtac impI THEN'
   1.796 +            CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   1.797 +              (if i = i''
   1.798 +              then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
   1.799 +                dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
   1.800 +                hyp_subst_tac,
   1.801 +                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.802 +                  (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
   1.803 +                    dtac list_inject_iffD1 THEN' etac conjE THEN'
   1.804 +                    (if k = i'
   1.805 +                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
   1.806 +                    else etac (mk_InN_not_InM i' k RS notE)))
   1.807 +                (rev ks)]
   1.808 +              else etac (mk_InN_not_InM i'' i RS notE)))
   1.809 +            ks)
   1.810 +          ks])
   1.811 +      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
   1.812 +      REPEAT_DETERM o rtac allI,
   1.813 +      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
   1.814 +        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.815 +          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.816 +            (fn (i, (from_to_sbd, to_sbd_inj)) =>
   1.817 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
   1.818 +              CONJ_WRAP' (fn i' => rtac impI THEN'
   1.819 +                dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
   1.820 +                dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
   1.821 +                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
   1.822 +                  REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
   1.823 +                  dtac list_inject_iffD1 THEN' etac conjE THEN'
   1.824 +                  (if k = i
   1.825 +                  then EVERY' [dtac (mk_InN_inject n i),
   1.826 +                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.827 +                    atac, atac, hyp_subst_tac] THEN'
   1.828 +                    CONJ_WRAP' (fn i'' =>
   1.829 +                      EVERY' [rtac impI, dtac (sym RS trans),
   1.830 +                        rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
   1.831 +                        etac (from_to_sbd RS arg_cong),
   1.832 +                        REPEAT_DETERM o etac allE,
   1.833 +                        dtac (mk_conjunctN n i), dtac mp, atac,
   1.834 +                        dtac (mk_conjunctN n i'), dtac mp, atac,
   1.835 +                        dtac (mk_conjunctN n i''), etac mp, etac sym])
   1.836 +                    ks
   1.837 +                  else etac (mk_InN_not_InM i k RS notE)))
   1.838 +                (rev ks))
   1.839 +              ks)
   1.840 +          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
   1.841 +      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
   1.842 +  end;
   1.843 +
   1.844 +fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   1.845 +  to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   1.846 +  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
   1.847 +  map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =
   1.848 +  let
   1.849 +    val n = length beh_defs;
   1.850 +    val ks = 1 upto n;
   1.851 +
   1.852 +    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
   1.853 +      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,
   1.854 +        (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
   1.855 +      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
   1.856 +        rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
   1.857 +        rtac conjI,
   1.858 +          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
   1.859 +          rtac @{thm singletonI},
   1.860 +        rtac conjI,
   1.861 +          rtac @{thm UN_least}, rtac Lev_sbd,
   1.862 +        rtac conjI,
   1.863 +          rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
   1.864 +          rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
   1.865 +          etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
   1.866 +        rtac conjI,
   1.867 +          rtac ballI, etac @{thm UN_E}, rtac conjI,
   1.868 +          if n = 1 then K all_tac else rtac (mk_sumEN n),
   1.869 +          EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
   1.870 +            fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
   1.871 +            EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
   1.872 +              rtac exI, rtac conjI,
   1.873 +              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   1.874 +              else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
   1.875 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
   1.876 +              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   1.877 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.878 +                  rtac trans_fun_cong_image_id_id_apply,
   1.879 +                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
   1.880 +              (take m set_naturals) set_rv_Levs),
   1.881 +              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.882 +                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.883 +                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   1.884 +                  if n = 1 then rtac refl else atac, atac, rtac subsetI,
   1.885 +                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.886 +                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.887 +                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.888 +                  if n = 1 then rtac refl else atac])
   1.889 +              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   1.890 +          ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss),
   1.891 +          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals,
   1.892 +            (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
   1.893 +            EVERY' [rtac ballI,
   1.894 +              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.895 +              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
   1.896 +              rtac exI, rtac conjI,
   1.897 +              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   1.898 +              else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
   1.899 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
   1.900 +              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   1.901 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.902 +                  rtac trans_fun_cong_image_id_id_apply,
   1.903 +                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
   1.904 +              (take m set_naturals) set_rv_Levs),
   1.905 +              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.906 +                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.907 +                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   1.908 +                  if n = 1 then rtac refl else atac, atac, rtac subsetI,
   1.909 +                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.910 +                  REPEAT_DETERM_N 4 o etac thin_rl,
   1.911 +                  rtac set_image_Lev,
   1.912 +                  atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.913 +                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.914 +                  if n = 1 then rtac refl else atac])
   1.915 +              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   1.916 +          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~
   1.917 +            (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
   1.918 +        (**)
   1.919 +          rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
   1.920 +          etac notE, etac @{thm UN_I[OF UNIV_I]},
   1.921 +        (*root isNode*)
   1.922 +          rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
   1.923 +          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
   1.924 +          CONVERSION (Conv.top_conv
   1.925 +            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   1.926 +          if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
   1.927 +          EVERY' (map2 (fn set_natural => fn coalg_set =>
   1.928 +            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.929 +              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
   1.930 +            (take m set_naturals) (take m coalg_sets)),
   1.931 +          CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.932 +            EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.933 +              rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
   1.934 +              rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
   1.935 +              atac, rtac subsetI,
   1.936 +              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.937 +              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
   1.938 +              rtac @{thm singletonI}, dtac length_Lev',
   1.939 +              etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
   1.940 +                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
   1.941 +              rtac rv_Nil])
   1.942 +          (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
   1.943 +
   1.944 +    fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
   1.945 +      ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
   1.946 +      EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
   1.947 +        rtac (@{thm if_P} RS
   1.948 +          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
   1.949 +        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
   1.950 +        rtac Lev_0, rtac @{thm singletonI},
   1.951 +        CONVERSION (Conv.top_conv
   1.952 +          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   1.953 +        if n = 1 then K all_tac
   1.954 +        else (rtac (sum_case_weak_cong RS trans) THEN'
   1.955 +          rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
   1.956 +        rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
   1.957 +        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
   1.958 +          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
   1.959 +            rtac trans, rtac @{thm Shift_def},
   1.960 +            rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
   1.961 +            REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
   1.962 +            etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
   1.963 +            rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
   1.964 +            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
   1.965 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.966 +                dtac list_inject_iffD1, etac conjE,
   1.967 +                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   1.968 +                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.969 +                  atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
   1.970 +                else etac (mk_InN_not_InM i' i'' RS notE)])
   1.971 +            (rev ks),
   1.972 +            rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
   1.973 +            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
   1.974 +            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
   1.975 +            rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
   1.976 +            rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
   1.977 +            dtac asm_rl, dtac asm_rl, dtac asm_rl,
   1.978 +            dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.979 +            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
   1.980 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.981 +                dtac list_inject_iffD1, etac conjE,
   1.982 +                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   1.983 +                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.984 +                  atac, atac, hyp_subst_tac, atac]
   1.985 +                else etac (mk_InN_not_InM i' i'' RS notE)])
   1.986 +            (rev ks),
   1.987 +            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
   1.988 +            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
   1.989 +            CONVERSION (Conv.top_conv
   1.990 +              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
   1.991 +            if n = 1 then K all_tac
   1.992 +            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
   1.993 +            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
   1.994 +            rtac refl])
   1.995 +        ks to_sbd_injs from_to_sbds)];
   1.996 +  in
   1.997 +    (rtac mor_cong THEN'
   1.998 +    EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
   1.999 +    stac mor_def THEN' rtac conjI THEN'
  1.1000 +    CONJ_WRAP' fbetw_tac
  1.1001 +      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
  1.1002 +        ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
  1.1003 +          (set_naturalss ~~ (coalg_setss ~~
  1.1004 +            (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
  1.1005 +    CONJ_WRAP' mor_tac
  1.1006 +      (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
  1.1007 +        ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~
  1.1008 +          (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
  1.1009 +  end;
  1.1010 +
  1.1011 +fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs =
  1.1012 +  EVERY' [rtac @{thm congruentI}, dtac lsbisE,
  1.1013 +    REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
  1.1014 +    etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
  1.1015 +    rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
  1.1016 +    EVERY' (map (fn equiv_LSBIS =>
  1.1017 +      EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
  1.1018 +    equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
  1.1019 +    etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
  1.1020 +
  1.1021 +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss =
  1.1022 +  EVERY' [stac coalg_def,
  1.1023 +    CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
  1.1024 +      EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
  1.1025 +        rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
  1.1026 +        EVERY' (map2 (fn set_natural => fn coalgT_set =>
  1.1027 +          EVERY' [rtac conjI, rtac (set_natural RS ord_eq_le_trans),
  1.1028 +            rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
  1.1029 +            etac coalgT_set])
  1.1030 +        (take m set_naturals) (take m coalgT_sets)),
  1.1031 +        CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) =>
  1.1032 +          EVERY' [rtac (set_natural RS ord_eq_le_trans),
  1.1033 +            rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
  1.1034 +            rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
  1.1035 +        (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))])
  1.1036 +    ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
  1.1037 +
  1.1038 +fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
  1.1039 +  EVERY' [stac mor_def, rtac conjI,
  1.1040 +    CONJ_WRAP' (fn equiv_LSBIS =>
  1.1041 +      EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
  1.1042 +    equiv_LSBISs,
  1.1043 +    CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
  1.1044 +      EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
  1.1045 +        rtac congruent_str_final, atac, rtac o_apply])
  1.1046 +    (equiv_LSBISs ~~ congruent_str_finals)] 1;
  1.1047 +
  1.1048 +fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
  1.1049 +  {context = ctxt, prems = _} =
  1.1050 +  unfold_thms_tac ctxt defs THEN
  1.1051 +  EVERY' [rtac conjI,
  1.1052 +    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
  1.1053 +    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
  1.1054 +      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
  1.1055 +        EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
  1.1056 +          EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
  1.1057 +            etac set_rev_mp, rtac coalg_final_set, rtac Rep])
  1.1058 +        Abs_inverses (drop m coalg_final_sets))])
  1.1059 +    (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
  1.1060 +
  1.1061 +fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
  1.1062 +  unfold_thms_tac ctxt defs THEN
  1.1063 +  EVERY' [rtac conjI,
  1.1064 +    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
  1.1065 +    CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
  1.1066 +
  1.1067 +fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
  1.1068 +  EVERY' [rtac iffD2, rtac mor_UNIV,
  1.1069 +    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
  1.1070 +      EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
  1.1071 +        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
  1.1072 +        rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
  1.1073 +        rtac (o_apply RS trans RS sym), rtac map_cong,
  1.1074 +        REPEAT_DETERM_N m o rtac refl,
  1.1075 +        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
  1.1076 +    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
  1.1077 +
  1.1078 +fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
  1.1079 +  sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
  1.1080 +  let
  1.1081 +    val n = length Rep_injects;
  1.1082 +  in
  1.1083 +    EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
  1.1084 +      REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
  1.1085 +      rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
  1.1086 +      rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
  1.1087 +      rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
  1.1088 +      rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,
  1.1089 +      rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls),
  1.1090 +      rtac impI,
  1.1091 +      CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
  1.1092 +        EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
  1.1093 +          rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
  1.1094 +          rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
  1.1095 +          rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
  1.1096 +          rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
  1.1097 +          rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
  1.1098 +          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
  1.1099 +          rtac Rep_inject])
  1.1100 +      (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
  1.1101 +  end;
  1.1102 +
  1.1103 +fun mk_unique_mor_tac raw_coinds bis =
  1.1104 +  CONJ_WRAP' (fn raw_coind =>
  1.1105 +    EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac,
  1.1106 +      etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
  1.1107 +  raw_coinds 1;
  1.1108 +
  1.1109 +fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
  1.1110 +  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
  1.1111 +    EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
  1.1112 +      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
  1.1113 +      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
  1.1114 +
  1.1115 +fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
  1.1116 +  {context = ctxt, prems = _} =
  1.1117 +  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
  1.1118 +    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
  1.1119 +    EVERY' (map (fn thm =>
  1.1120 +      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
  1.1121 +    rtac sym, rtac @{thm id_apply}] 1;
  1.1122 +
  1.1123 +fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
  1.1124 +  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
  1.1125 +    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
  1.1126 +    REPEAT_DETERM_N m o rtac refl,
  1.1127 +    EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
  1.1128 +
  1.1129 +fun mk_srel_coinduct_tac ks raw_coind bis_srel =
  1.1130 +  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
  1.1131 +    CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
  1.1132 +    CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
  1.1133 +      REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
  1.1134 +    rtac impI, REPEAT_DETERM o etac conjE,
  1.1135 +    CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
  1.1136 +      rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
  1.1137 +
  1.1138 +fun mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids =
  1.1139 +  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts srel_coinduct),
  1.1140 +    EVERY' (map2 (fn srel_mono => fn srel_Id =>
  1.1141 +      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
  1.1142 +        etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
  1.1143 +        REPEAT_DETERM_N m o rtac @{thm subset_refl},
  1.1144 +        REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
  1.1145 +        rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
  1.1146 +    srel_monos srel_Ids),
  1.1147 +    rtac impI, REPEAT_DETERM o etac conjE,
  1.1148 +    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
  1.1149 +
  1.1150 +fun mk_dtor_coinduct_tac m ks raw_coind bis_def =
  1.1151 +  let
  1.1152 +    val n = length ks;
  1.1153 +  in
  1.1154 +    EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI,
  1.1155 +      CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
  1.1156 +      CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI,
  1.1157 +        rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
  1.1158 +        atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
  1.1159 +        etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
  1.1160 +        rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
  1.1161 +        CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
  1.1162 +          REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
  1.1163 +        ks])
  1.1164 +      ks,
  1.1165 +      rtac impI,
  1.1166 +      CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
  1.1167 +        rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp,
  1.1168 +        rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
  1.1169 +  end;
  1.1170 +
  1.1171 +fun mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def bis_diag =
  1.1172 +  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
  1.1173 +    EVERY' (map (fn i =>
  1.1174 +      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
  1.1175 +        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
  1.1176 +        rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
  1.1177 +        etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
  1.1178 +        rtac exI, rtac conjI, etac conjI, atac,
  1.1179 +        CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
  1.1180 +          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
  1.1181 +    ks),
  1.1182 +    rtac impI, REPEAT_DETERM o etac conjE,
  1.1183 +    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
  1.1184 +
  1.1185 +fun mk_map_tac m n cT unfold map_comp' map_cong =
  1.1186 +  EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
  1.1187 +    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
  1.1188 +    REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
  1.1189 +    REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
  1.1190 +    rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
  1.1191 +
  1.1192 +fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
  1.1193 +  EVERY' [rtac hset_minimal,
  1.1194 +    REPEAT_DETERM_N n o rtac @{thm Un_upper1},
  1.1195 +    REPEAT_DETERM_N n o
  1.1196 +      EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
  1.1197 +        EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
  1.1198 +          etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
  1.1199 +          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
  1.1200 +      (1 upto n) set_hsets set_hset_hsetss)] 1;
  1.1201 +
  1.1202 +fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets =
  1.1203 +  EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
  1.1204 +    REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
  1.1205 +    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
  1.1206 +
  1.1207 +fun mk_map_id_tac maps unfold_unique unfold_dtor =
  1.1208 +  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
  1.1209 +    rtac unfold_dtor] 1;
  1.1210 +
  1.1211 +fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
  1.1212 +  EVERY' [rtac unfold_unique,
  1.1213 +    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
  1.1214 +      EVERY' (map rtac
  1.1215 +        ([@{thm o_assoc} RS trans,
  1.1216 +        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
  1.1217 +        @{thm o_assoc} RS trans RS sym,
  1.1218 +        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
  1.1219 +        @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
  1.1220 +        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
  1.1221 +        ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong] @
  1.1222 +        replicate m (@{thm id_o} RS fun_cong) @
  1.1223 +        replicate n (@{thm o_id} RS fun_cong))))
  1.1224 +    maps map_comps map_congs)] 1;
  1.1225 +
  1.1226 +fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
  1.1227 +  set_hset_hsetsss =
  1.1228 +  let
  1.1229 +    val n = length map_comp's;
  1.1230 +    val ks = 1 upto n;
  1.1231 +  in
  1.1232 +    EVERY' ([rtac rev_mp,
  1.1233 +      coinduct_tac] @
  1.1234 +      maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets),
  1.1235 +        set_hset_hsetss) =>
  1.1236 +        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
  1.1237 +         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
  1.1238 +         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
  1.1239 +         REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
  1.1240 +         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
  1.1241 +         EVERY' (maps (fn set_hset =>
  1.1242 +           [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
  1.1243 +           REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
  1.1244 +         REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
  1.1245 +         CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
  1.1246 +           EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
  1.1247 +             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural,
  1.1248 +             rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
  1.1249 +             REPEAT_DETERM o etac conjE,
  1.1250 +             CONJ_WRAP' (fn set_hset_hset =>
  1.1251 +               EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
  1.1252 +           (drop m set_naturals ~~ set_hset_hsetss)])
  1.1253 +        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~
  1.1254 +          map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
  1.1255 +      [rtac impI,
  1.1256 +       CONJ_WRAP' (fn k =>
  1.1257 +         EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
  1.1258 +           rtac conjI, rtac refl, rtac refl]) ks]) 1
  1.1259 +  end
  1.1260 +
  1.1261 +fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
  1.1262 +  rtac unfold_unique 1 THEN
  1.1263 +  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
  1.1264 +  ALLGOALS (etac sym);
  1.1265 +
  1.1266 +fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
  1.1267 +  {context = ctxt, prems = _} =
  1.1268 +  let
  1.1269 +    val n = length map_simps;
  1.1270 +  in
  1.1271 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
  1.1272 +      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
  1.1273 +      CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
  1.1274 +      REPEAT_DETERM o rtac allI,
  1.1275 +      CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
  1.1276 +        [SELECT_GOAL (unfold_thms_tac ctxt
  1.1277 +          (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
  1.1278 +        rtac @{thm Un_cong}, rtac refl,
  1.1279 +        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
  1.1280 +          (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
  1.1281 +            REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
  1.1282 +      (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1
  1.1283 +  end;
  1.1284 +
  1.1285 +fun mk_set_natural_tac hset_def col_natural =
  1.1286 +  EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
  1.1287 +    (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
  1.1288 +    (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
  1.1289 +
  1.1290 +fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
  1.1291 +  let
  1.1292 +    val n = length rec_0s;
  1.1293 +  in
  1.1294 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
  1.1295 +      REPEAT_DETERM o rtac allI,
  1.1296 +      CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [ordIso_ordLeq_trans,
  1.1297 +        @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
  1.1298 +      REPEAT_DETERM o rtac allI,
  1.1299 +      CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
  1.1300 +        [rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
  1.1301 +        rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
  1.1302 +        REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
  1.1303 +        EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
  1.1304 +          rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE,
  1.1305 +          etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
  1.1306 +      (rec_Sucs ~~ set_sbdss)] 1
  1.1307 +  end;
  1.1308 +
  1.1309 +fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
  1.1310 +  EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def,
  1.1311 +    ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
  1.1312 +    @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
  1.1313 +    ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
  1.1314 +
  1.1315 +fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
  1.1316 +  sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
  1.1317 +  let
  1.1318 +    val n = length isNode_hsets;
  1.1319 +    val in_hin_tac = rtac CollectI THEN'
  1.1320 +      CONJ_WRAP' (fn mor_hset => EVERY' (map etac
  1.1321 +        [mor_hset OF [coalgT, mor_T_final] RS sym RS ord_eq_le_trans,
  1.1322 +        arg_cong RS sym RS ord_eq_le_trans,
  1.1323 +        mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS ord_eq_le_trans])) mor_hsets;
  1.1324 +  in
  1.1325 +    EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans,
  1.1326 +      rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans,
  1.1327 +      rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
  1.1328 +      rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero},
  1.1329 +      rtac @{thm cexp_ordLeq_ccexp},  rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
  1.1330 +      rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order,
  1.1331 +      rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
  1.1332 +      rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1.1333 +      rtac set_mp, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
  1.1334 +      rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
  1.1335 +      rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
  1.1336 +      ftac (carT_def RS equalityD1 RS set_mp),
  1.1337 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  1.1338 +      rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
  1.1339 +      rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
  1.1340 +      rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
  1.1341 +      CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) =>
  1.1342 +        EVERY' [rtac (mk_disjIN n i), rtac isNode_hset, atac, atac, atac, in_hin_tac])
  1.1343 +      (1 upto n ~~ isNode_hsets),
  1.1344 +      CONJ_WRAP' (fn isNode_hset =>
  1.1345 +        EVERY' [rtac ballI, rtac isNode_hset, atac, ftac CollectD, etac @{thm SuccD},
  1.1346 +          etac bspec, atac, in_hin_tac])
  1.1347 +      isNode_hsets,
  1.1348 +      atac, rtac isNode_hset, atac, atac, atac, in_hin_tac] 1
  1.1349 +  end;
  1.1350 +
  1.1351 +fun mk_bd_card_order_tac sbd_card_order =
  1.1352 +  EVERY' (map rtac [@{thm card_order_ccexp}, sbd_card_order, sbd_card_order]) 1;
  1.1353 +
  1.1354 +fun mk_bd_cinfinite_tac sbd_Cinfinite =
  1.1355 +  EVERY' (map rtac [@{thm cinfinite_ccexp}, @{thm ctwo_ordLeq_Cinfinite},
  1.1356 +    sbd_Cinfinite, sbd_Cinfinite]) 1;
  1.1357 +
  1.1358 +fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
  1.1359 +  let
  1.1360 +    val m = length set_incl_hsets;
  1.1361 +  in
  1.1362 +    EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
  1.1363 +      EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
  1.1364 +      CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
  1.1365 +      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
  1.1366 +      EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
  1.1367 +      CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
  1.1368 +      REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
  1.1369 +  end;
  1.1370 +
  1.1371 +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
  1.1372 +  {context = ctxt, prems = _} =
  1.1373 +  unfold_thms_tac ctxt [coalg_def] THEN
  1.1374 +  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
  1.1375 +    EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1.1376 +      REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  1.1377 +      hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  1.1378 +      EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  1.1379 +      pickWP_assms_tac,
  1.1380 +      SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
  1.1381 +      REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1.1382 +      rtac CollectI,
  1.1383 +      REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
  1.1384 +      CONJ_WRAP' (fn set_natural =>
  1.1385 +        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
  1.1386 +          rtac trans_fun_cong_image_id_id_apply, atac])
  1.1387 +      (drop m set_naturals)])
  1.1388 +  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
  1.1389 +
  1.1390 +fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
  1.1391 +  {context = ctxt, prems = _} =
  1.1392 +  let
  1.1393 +    val n = length map_comps;
  1.1394 +  in
  1.1395 +    unfold_thms_tac ctxt [mor_def] THEN
  1.1396 +    EVERY' [rtac conjI,
  1.1397 +      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
  1.1398 +      CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
  1.1399 +        EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1.1400 +          REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  1.1401 +          hyp_subst_tac,
  1.1402 +          SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
  1.1403 +          rtac (map_comp RS trans),
  1.1404 +          SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
  1.1405 +          rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
  1.1406 +          pickWP_assms_tac])
  1.1407 +      (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
  1.1408 +  end;
  1.1409 +
  1.1410 +val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
  1.1411 +val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
  1.1412 +
  1.1413 +fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
  1.1414 +  unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
  1.1415 +  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
  1.1416 +  CONJ_WRAP' (fn (unfold, map_comp) =>
  1.1417 +    EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  1.1418 +      hyp_subst_tac,
  1.1419 +      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
  1.1420 +      rtac refl])
  1.1421 +  (unfolds ~~ map_comps) 1;
  1.1422 +
  1.1423 +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
  1.1424 +  {context = ctxt, prems = _} =
  1.1425 +  let
  1.1426 +    val n = length rec_0s;
  1.1427 +    val ks = n downto 1;
  1.1428 +  in
  1.1429 +    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
  1.1430 +      REPEAT_DETERM o rtac allI,
  1.1431 +      CONJ_WRAP' (fn thm => EVERY'
  1.1432 +        [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
  1.1433 +      REPEAT_DETERM o rtac allI,
  1.1434 +      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
  1.1435 +        EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  1.1436 +          REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  1.1437 +          hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  1.1438 +          EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  1.1439 +          pickWP_assms_tac,
  1.1440 +          rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  1.1441 +          rtac ord_eq_le_trans, rtac rec_Suc,
  1.1442 +          rtac @{thm Un_least},
  1.1443 +          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
  1.1444 +            @{thm prod.cases}]),
  1.1445 +          etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
  1.1446 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
  1.1447 +            EVERY' [rtac @{thm UN_least},
  1.1448 +              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
  1.1449 +              etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
  1.1450 +              dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
  1.1451 +          (ks ~~ rev (drop m set_naturals))])
  1.1452 +      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
  1.1453 +  end;
  1.1454 +
  1.1455 +fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
  1.1456 +  mor_unique pick_cols hset_defs =
  1.1457 +  EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
  1.1458 +    REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
  1.1459 +    rtac box_equals, rtac mor_unique,
  1.1460 +    rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1461 +    rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1462 +    rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1463 +    rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1.1464 +    rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv},
  1.1465 +    rtac box_equals, rtac mor_unique,
  1.1466 +    rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1467 +    rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1468 +    rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1469 +    rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1.1470 +    rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
  1.1471 +    rtac CollectI,
  1.1472 +    CONJ_WRAP' (fn (pick, def) =>
  1.1473 +      EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least},
  1.1474 +        rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
  1.1475 +        rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
  1.1476 +        rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
  1.1477 +    (pick_cols ~~ hset_defs)] 1;
  1.1478 +
  1.1479 +fun mk_wit_tac n dtor_ctors set_simp wit coind_wits {context = ctxt, prems = _} =
  1.1480 +  ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
  1.1481 +  REPEAT_DETERM (atac 1 ORELSE
  1.1482 +    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
  1.1483 +    K (unfold_thms_tac ctxt dtor_ctors),
  1.1484 +    REPEAT_DETERM_N n o etac UnE,
  1.1485 +    REPEAT_DETERM o
  1.1486 +      (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
  1.1487 +        (eresolve_tac wit ORELSE'
  1.1488 +        (dresolve_tac wit THEN'
  1.1489 +          (etac FalseE ORELSE'
  1.1490 +          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
  1.1491 +            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
  1.1492 +
  1.1493 +fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
  1.1494 +  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
  1.1495 +  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
  1.1496 +  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
  1.1497 +  ALLGOALS (TRY o
  1.1498 +    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
  1.1499 +
  1.1500 +fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
  1.1501 +  set_naturals set_incls set_set_inclss =
  1.1502 +  let
  1.1503 +    val m = length set_incls;
  1.1504 +    val n = length set_set_inclss;
  1.1505 +    val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
  1.1506 +    val in_Jsrel = nth in_Jsrels (i - 1);
  1.1507 +    val if_tac =
  1.1508 +      EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  1.1509 +        rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1.1510 +        EVERY' (map2 (fn set_natural => fn set_incl =>
  1.1511 +          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
  1.1512 +            rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
  1.1513 +            etac (set_incl RS @{thm subset_trans})])
  1.1514 +        passive_set_naturals set_incls),
  1.1515 +        CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
  1.1516 +          EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
  1.1517 +            rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1.1518 +            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
  1.1519 +            rtac conjI, rtac refl, rtac refl])
  1.1520 +        (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
  1.1521 +        CONJ_WRAP' (fn conv =>
  1.1522 +          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
  1.1523 +          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  1.1524 +          REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
  1.1525 +          rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac])
  1.1526 +        @{thms fst_conv snd_conv}];
  1.1527 +    val only_if_tac =
  1.1528 +      EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  1.1529 +        rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  1.1530 +        CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
  1.1531 +          EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
  1.1532 +            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
  1.1533 +            rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
  1.1534 +            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  1.1535 +              (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
  1.1536 +                rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
  1.1537 +                rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
  1.1538 +                dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
  1.1539 +                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  1.1540 +                dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  1.1541 +                dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  1.1542 +                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  1.1543 +            (rev (active_set_naturals ~~ in_Jsrels))])
  1.1544 +        (set_simps ~~ passive_set_naturals),
  1.1545 +        rtac conjI,
  1.1546 +        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
  1.1547 +          rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
  1.1548 +          rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  1.1549 +          EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
  1.1550 +            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  1.1551 +            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
  1.1552 +          atac]]
  1.1553 +  in
  1.1554 +    EVERY' [rtac iffI, if_tac, only_if_tac] 1
  1.1555 +  end;
  1.1556 +
  1.1557 +end;