(*  Title:      HOL/Codatatype/Tools/bnf_gfp_tactics.ML

    Author:     Dmitriy Traytel, TU Muenchen

    Author:     Andrei Popescu, TU Muenchen

    Author:     Jasmin Blanchette, TU Muenchen

    Copyright   2012

Tactics for the codatatype construction.

*)

signature BNF_GFP_TACTICS =

sig

  val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic

  val mk_bd_card_order_tac: thm -> tactic

  val mk_bd_cinfinite_tac: thm -> tactic

  val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic

  val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic

  val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic

  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic

  val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic

  val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->

    tactic

  val mk_coalg_set_tac: thm -> tactic

  val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->

    thm list list -> tactic

  val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic

  val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic

  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->

    thm -> thm -> tactic

  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic

  val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic

  val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->

    thm -> thm -> thm -> tactic

  val mk_incl_lsbis_tac: int -> int -> thm -> tactic

  val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic

  val mk_length_Lev'_tac: thm -> tactic

  val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic

  val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic

  val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->

    thm list list -> thm list list list -> tactic

  val mk_map_id_tac: thm list -> thm -> thm -> tactic

  val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic

  val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic

  val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic

  val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->

    thm list -> {prems: 'a, context: Proof.context} -> tactic

  val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic

  val mk_mor_UNIV_tac: thm list -> thm -> tactic

  val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->

    thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->

    thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->

    thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic

  val mk_mor_elim_tac: thm -> tactic

  val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->

    thm list -> thm list list -> thm list list -> tactic

  val mk_mor_hset_tac: thm -> thm -> tactic

  val mk_mor_incl_tac: thm -> thm list -> tactic

  val mk_mor_str_tac: 'a list -> thm -> tactic

  val mk_mor_sum_case_tac: 'a list -> thm -> tactic

  val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->

    {prems: thm list, context: Proof.context} -> tactic

  val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->

    {prems: thm list, context: Proof.context} -> tactic

  val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->

    thm list -> tactic

  val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic

  val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)

  val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->

    thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->

    tactic

  val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->

    thm list -> thm list -> thm -> thm list -> tactic

  val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic

  val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic

  val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->

    thm list list -> tactic

  val mk_set_bd_tac: thm -> thm -> thm -> tactic

  val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic

  val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->

    thm list list -> thm list list -> tactic

  val mk_set_incl_hin_tac: thm list -> tactic

  val mk_set_incl_hset_tac: thm -> thm -> tactic

  val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic

  val mk_set_natural_tac: thm -> thm -> tactic

  val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->

    thm list list -> thm list list -> tactic

  val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic

  val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic

  val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->

    thm list -> thm list -> tactic

  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->

    thm list -> thm list -> thm list list -> tactic

  val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->

    cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->

    thm list list -> thm list list -> thm -> thm list list -> tactic

  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic

  val mk_unique_mor_tac: thm list -> thm -> tactic

  val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->

    {prems: 'a, context: Proof.context} -> tactic

  val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic

end;

structure BNF_GFP_Tactics : BNF_GFP_TACTICS =

struct

open BNF_Tactics

open BNF_Util

open BNF_FP

open BNF_GFP_Util

val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;

val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};

val nat_induct = @{thm nat_induct};

val o_apply_trans_sym = o_apply RS trans RS sym;

val ord_eq_le_trans = @{thm ord_eq_le_trans};

val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =

  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};

val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};

val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;

val sum_case_weak_cong = @{thm sum_case_weak_cong};

val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};

fun mk_coalg_set_tac coalg_def =

  dtac (coalg_def RS iffD1) 1 THEN

  REPEAT_DETERM (etac conjE 1) THEN

  EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN

  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;

fun mk_mor_elim_tac mor_def =

  (dtac (subst OF [mor_def]) THEN'

  REPEAT o etac conjE THEN'

  TRY o rtac @{thm image_subsetI} THEN'

  etac bspec THEN'

  atac) 1;

fun mk_mor_incl_tac mor_def map_id's =

  (stac mor_def THEN'

  rtac conjI THEN'

  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))

    map_id's THEN'

  CONJ_WRAP' (fn thm =>

   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))

  map_id's) 1;

fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =

  let

    fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];

    fun mor_tac ((mor_image, morE), map_comp_id) =

      EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,

        etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];

  in

    (stac mor_def THEN' rtac conjI THEN'

    CONJ_WRAP' fbetw_tac mor_images THEN'

    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1

  end;

fun mk_mor_UNIV_tac morEs mor_def =

  let

    val n = length morEs;

    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,

      rtac UNIV_I, rtac sym, rtac o_apply];

  in

    EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,

    stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,

    CONJ_WRAP' (fn i =>

      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1

  end;

fun mk_mor_str_tac ks mor_UNIV =

  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;

fun mk_mor_sum_case_tac ks mor_UNIV =

  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1;

fun mk_set_incl_hset_tac def rec_Suc =

  EVERY' (stac def ::

    map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},

      sym, rec_Suc]) 1;

fun mk_set_hset_incl_hset_tac n defs rec_Suc i =

  EVERY' (map (TRY oo stac) defs @

    map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,

      mk_UnIN n i] @

    [etac @{thm UN_I}, atac]) 1;

fun mk_set_incl_hin_tac incls =

  if null incls then rtac subset_UNIV 1

  else EVERY' [rtac subsetI, rtac CollectI,

    CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;

fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =

  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

    REPEAT_DETERM o rtac allI,

    CONJ_WRAP' (fn thm => EVERY'

      [rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,

    REPEAT_DETERM o rtac allI,

    CONJ_WRAP' (fn rec_Suc => EVERY'

      [rtac ord_eq_le_trans, rtac rec_Suc,

        if m = 0 then K all_tac

        else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),

        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))

          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],

            rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])

      rec_Sucs] 1;

fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =

  (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,

    rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,

    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,

    REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1

fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =

  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

    REPEAT_DETERM o rtac allI,

    CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,

    REPEAT_DETERM o rtac allI,

    CONJ_WRAP'

      (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) =>

        EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),

          if m = 0 then K all_tac

          else EVERY' [rtac @{thm Un_cong}, rtac box_equals,

            rtac (nth passive_set_naturals (j - 1) RS sym),

            rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],

          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))

            (fn (i, (set_natural, coalg_set)) =>

              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),

                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,

                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),

                ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),

                REPEAT_DETERM o etac allE, atac, atac])

            (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])

      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;

fun mk_mor_hset_tac hset_def mor_hset_rec =

  EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,

    atac, atac, rtac (hset_def RS sym)] 1

fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =

  let

    val n = length srel_O_Grs;

    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);

    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =

      EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),

        etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,

        rtac (srel_O_Gr RS equalityD2 RS set_mp),

        rtac @{thm relcompI}, rtac @{thm converseI},

        EVERY' (map (fn thm =>

          EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],

            rtac CollectI,

            CONJ_WRAP' (fn (i, thm) =>

              if i <= m

              then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,

                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]

              else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,

                rtac trans_fun_cong_image_id_id_apply, atac])

            (1 upto (m + n) ~~ set_naturals),

            rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,

            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])

          @{thms fst_diag_id snd_diag_id})];

    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =

      EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,

        etac allE, etac allE, etac impE, atac,

        dtac (srel_O_Gr RS equalityD1 RS set_mp),

        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],

        REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],

        REPEAT_DETERM o dtac Pair_eqD,

        REPEAT_DETERM o etac conjE,

        hyp_subst_tac,

        REPEAT_DETERM o eresolve_tac [CollectE, conjE],

        rtac bexI, rtac conjI, rtac trans, rtac map_comp,

        REPEAT_DETERM_N m o stac @{thm id_o},

        REPEAT_DETERM_N n o stac @{thm o_id},

        etac sym, rtac trans, rtac map_comp,

        REPEAT_DETERM_N m o stac @{thm id_o},

        REPEAT_DETERM_N n o stac @{thm o_id},

        rtac trans, rtac map_cong,

        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],

        REPEAT_DETERM_N n o rtac refl,

        etac sym, rtac CollectI,

        CONJ_WRAP' (fn (i, thm) =>

          if i <= m

          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},

            rtac @{thm diag_fst}, etac set_mp, atac]

          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,

            rtac trans_fun_cong_image_id_id_apply, atac])

        (1 upto (m + n) ~~ set_naturals)];

  in

    EVERY' [rtac (bis_def RS trans),

      rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,

      etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1

  end;

fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =

  EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),

    REPEAT_DETERM o etac conjE, rtac conjI,

    CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,

      rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,

    CONJ_WRAP' (fn (srel_cong, srel_converse) =>

      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},

        rtac (srel_cong RS trans),

        REPEAT_DETERM_N m o rtac @{thm diag_converse},

        REPEAT_DETERM_N (length srel_congs) o rtac refl,

        rtac srel_converse,

        REPEAT_DETERM o etac allE,

        rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;

fun mk_bis_O_tac m bis_srel srel_congs srel_Os =

  EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),

    REPEAT_DETERM o etac conjE, rtac conjI,

    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,

    CONJ_WRAP' (fn (srel_cong, srel_O) =>

      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},

        rtac (srel_cong RS trans),

        REPEAT_DETERM_N m o rtac @{thm diag_Comp},

        REPEAT_DETERM_N (length srel_congs) o rtac refl,

        rtac srel_O,

        etac @{thm relcompE},

        REPEAT_DETERM o dtac Pair_eqD,

        etac conjE, hyp_subst_tac,

        REPEAT_DETERM o etac allE, rtac @{thm relcompI},

        etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;

fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins

  {context = ctxt, prems = _} =

  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN

  EVERY' [rtac conjI,

    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,

    CONJ_WRAP' (fn (coalg_in, morE) =>

      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,

        etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},

        etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1;

fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =

  let

    val n = length in_monos;

    val ks = 1 upto n;

  in

    unfold_thms_tac ctxt [bis_def] THEN

    EVERY' [rtac conjI,

      CONJ_WRAP' (fn i =>

        EVERY' [rtac @{thm UN_least}, dtac bspec, atac,

          dtac conjunct1, etac (mk_conjunctN n i)]) ks,

      CONJ_WRAP' (fn (i, in_mono) =>

        EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,

          dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,

          atac, etac bexE, rtac bexI, atac, rtac in_mono,

          REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},

          atac]) (ks ~~ in_monos)] 1

  end;

fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =

  let

    val n = length lsbis_defs;

  in

    EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),

      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],

      hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1

  end;

fun mk_incl_lsbis_tac n i lsbis_def =

  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,

    REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,

    rtac (mk_nth_conv n i)] 1;

fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =

  EVERY' [rtac (@{thm equiv_def} RS iffD2),

    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),

    rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,

    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},

    rtac conjI, rtac (@{thm sym_def} RS iffD2),

    rtac allI, rtac allI, rtac impI, rtac set_mp,

    rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},

    rtac (@{thm trans_def} RS iffD2),

    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,

    rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,

    etac @{thm relcompI}, atac] 1;

fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =

  let

    val n = length strT_defs;

    val ks = 1 upto n;

    fun coalg_tac (i, ((passive_sets, active_sets), def)) =

      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],

        hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),

        rtac (mk_sum_casesN n i), rtac CollectI,

        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),

          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])

          passive_sets),

        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),

          rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,

          rtac conjI,

          rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,

            etac equalityD1, etac CollectD,

          rtac conjI, etac @{thm Shift_clists},

          rtac conjI, etac @{thm Shift_prefCl},

          rtac conjI, rtac ballI,

            rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,

            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),

            etac bspec, etac @{thm ShiftD},

            CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},

              dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),

              dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},

              REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,

              rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),

              rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,

              REPEAT_DETERM_N m o (rtac conjI THEN' atac),

              CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},

                rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},

                rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,

          rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],

          etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,

          dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,

          etac @{thm set_mp[OF equalityD1]}, atac,

          REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,

          rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),

          etac (@{thm append_Nil} RS sym RS arg_cong RS trans),

          REPEAT_DETERM_N m o (rtac conjI THEN' atac),

          CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},

            rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},

            rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];

  in

    unfold_thms_tac ctxt defs THEN

    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1

  end;

fun mk_card_of_carT_tac m isNode_defs sbd_sbd

  sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =

  let

    val n = length isNode_defs;

  in

    EVERY' [rtac (Thm.permute_prems 0 1 ctrans),

      rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp},

      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},

      rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},

      rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,

      rtac ctrans, rtac @{thm card_of_diff},

      rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},

      rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,

      rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},

      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},

      rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists},

      rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,

      rtac @{thm clists_Cinfinite},

      if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),

      rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},

      rtac sbd_Cinfinite,

      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},

      rtac @{thm Cnotzero_clists},

      rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc},

      rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},

      rtac ctrans, rtac @{thm cexp_mono},

      rtac @{thm ordLeq_ordIso_trans},

      CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1

          (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}

        RSN (3, @{thm Un_Cinfinite_bound}))))

        (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),

      rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1},

      REPEAT_DETERM_N m o rtac @{thm csum_cong2},

      CONJ_WRAP_GEN' (rtac @{thm csum_cong})

        (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,

      rtac sbd_Card_order,

      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},

      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},

      rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},

      rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,

      rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp},

      rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2},

      rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac,

      rtac @{thm card_of_Card_order},

      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},

      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},

      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2_Cnotzero},

      rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,

      rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,

      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod},

      rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},

      rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},

      rtac @{thm ordIso_transitive},

      REPEAT_DETERM_N m o rtac @{thm csum_cong2},

      rtac sbd_sbd,

      BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'

        FIRST' [rtac @{thm card_of_Card_order},

          rtac @{thm Card_order_csum}, rtac sbd_Card_order])

        @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}

        (1 upto m + 1) (m + 1 :: (1 upto m)),

      if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}],

      rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,

      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},

      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},

      rtac @{thm Card_order_ctwo},

      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order,

      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},

      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},

      rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,

      rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},

      rtac sbd_Cinfinite,

      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},

      rtac sbd_Cnotzero,

      rtac @{thm card_of_mono1}, rtac subsetI,

      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,

      rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,

      rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),

      rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},

      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),

      rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,

      CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'

        [rtac (mk_UnIN n i), dtac (def RS iffD1),

        REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,

        REPEAT_DETERM_N m o (rtac conjI THEN' atac),

        CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,

          rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},

          rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),

      atac] 1

  end;

fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=

  EVERY' [dtac (carT_def RS equalityD1 RS set_mp),

    REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],

    dtac Pair_eqD,

    etac conjE, hyp_subst_tac,

    dtac (isNode_def RS iffD1),

    REPEAT_DETERM o eresolve_tac [exE, conjE],

    rtac (equalityD2 RS set_mp),

    rtac (strT_def RS arg_cong RS trans),

    etac (arg_cong RS trans),

    fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,

    rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,

    etac @{thm prefCl_Succ}, atac] 1;

fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs

  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss =

  let

    val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss;

    val ks = 1 upto n;

    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) =

      CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'

        (if i = i'

        then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,

          rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),

          rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),

          rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),

          rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]

        else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),

          REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,

          dtac conjunct2, dtac Pair_eqD, etac conjE,

          hyp_subst_tac, dtac (isNode_def RS iffD1),

          REPEAT_DETERM o eresolve_tac [exE, conjE],

          rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))

      (ks ~~ (carT_defs ~~ isNode_defs));

    fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =

      dtac (mk_conjunctN n i) THEN'

      CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>

        EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,

          rtac (coalgT RS coalg_set RS set_mp), atac, etac carT_set, atac, atac,

          etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,

          rtac set_hset_incl_hset, etac carT_set, atac, atac])

      (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));

  in

    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),

      REPEAT_DETERM o rtac allI, rtac impI,

      CONJ_WRAP' base_tac

        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))),

      REPEAT_DETERM o rtac allI, rtac impI,

      REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},

      CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'

        CONJ_WRAP_GEN' (K all_tac) step_tac

          (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1

  end;

fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} =

  let

    val m = length strT_hsets;

  in

    if m = 0 then atac 1

    else (unfold_thms_tac ctxt [isNode_def] THEN

      EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],

        rtac exI, rtac conjI, atac,

        CONJ_WRAP' (fn (thm, i) =>  if i > m then atac

          else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac])

        (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)

  end;

fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =

  let

    val n = length Lev_0s;

    val ks = 1 upto n;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn Lev_0 =>

        EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>

        EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,

          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))

            (fn (i, to_sbd) => EVERY' [rtac subsetI,

              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,

              rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,

              etac set_rev_mp, REPEAT_DETERM o etac allE,

              etac (mk_conjunctN n i)])

          (rev (ks ~~ to_sbds))])

      (Lev_Sucs ~~ to_sbdss)] 1

  end;

fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =

  let

    val n = length Lev_0s;

    val ks = n downto 1;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn Lev_0 =>

        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),

          etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn Lev_Suc =>

        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),

          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,

              rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},

              REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])

      Lev_Sucs] 1

  end;

fun mk_length_Lev'_tac length_Lev =

  EVERY' [ftac length_Lev, etac ssubst, atac] 1;

fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =

  let

    val n = length Lev_0s;

    val ks = n downto 1;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn Lev_0 =>

        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),

          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},

          hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},

          rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>

        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),

          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,

              dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,

              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},

              rtac Lev_0, rtac @{thm singletonI},

              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,

              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},

              rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,

              rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),

              etac mp, etac conjI, atac]) ks])

      (Lev_0s ~~ Lev_Sucs)] 1

  end;

fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =

  let

    val n = length rv_Nils;

    val ks = 1 upto n;

  in

    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn rv_Cons =>

        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,

          rtac (@{thm append_Nil} RS arg_cong RS trans),

          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))

        (ks ~~ rv_Nils))

      rv_Conss,

      REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),

      EVERY' (map (fn i =>

        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),

          CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,

            rtac (@{thm append_Cons} RS arg_cong RS trans),

            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),

            rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])

          ks])

        rv_Conss)

      ks)] 1

  end;

fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =

  let

    val n = length Lev_0s;

    val ks = 1 upto n;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>

        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,

          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,

          rtac (rv_Nil RS arg_cong RS iffD2),

          rtac (mk_sum_casesN n i RS iffD2),

          CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])

      (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>

        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),

          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

            (fn (i, (from_to_sbd, coalg_set)) =>

              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,

              rtac (rv_Cons RS arg_cong RS iffD2),

              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),

              etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,

              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,

              etac coalg_set, atac])

          (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])

      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1

  end;

fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =

  let

    val n = length Lev_0s;

    val ks = 1 upto n;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>

        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),

          etac @{thm singletonE}, hyp_subst_tac,

          CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'

            (if i = i'

            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,

              CONJ_WRAP' (fn (i'', Lev_0'') =>

                EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},

                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),

                  rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,

                  etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),

                  rtac @{thm singletonI}])

              (ks ~~ Lev_0s)]

            else etac (mk_InN_not_InM i' i RS notE)))

          ks])

      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>

        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),

          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

            (fn (i, from_to_sbd) =>

              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,

                CONJ_WRAP' (fn i' => rtac impI THEN'

                  CONJ_WRAP' (fn i'' =>

                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),

                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),

                      rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,

                      rtac conjI, atac, dtac (sym RS trans RS sym),

                      rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),

                      etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,

                      dtac (mk_conjunctN n i), dtac mp, atac,

                      dtac (mk_conjunctN n i'), dtac mp, atac,

                      dtac (mk_conjunctN n i''), etac mp, atac])

                  ks)

                ks])

          (rev (ks ~~ from_to_sbds))])

      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1

  end;

fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =

  let

    val n = length Lev_0s;

    val ks = 1 upto n;

  in

    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>

        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),

          etac @{thm singletonE}, hyp_subst_tac,

          CONJ_WRAP' (fn i' => rtac impI THEN'

            CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'

              (if i = i''

              then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},

                dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),

                hyp_subst_tac,

                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

                  (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'

                    dtac list_inject_iffD1 THEN' etac conjE THEN'

                    (if k = i'

                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]

                    else etac (mk_InN_not_InM i' k RS notE)))

                (rev ks)]

              else etac (mk_InN_not_InM i'' i RS notE)))

            ks)

          ks])

      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),

      REPEAT_DETERM o rtac allI,

      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>

        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),

          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))

            (fn (i, (from_to_sbd, to_sbd_inj)) =>

              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'

              CONJ_WRAP' (fn i' => rtac impI THEN'

                dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'

                dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'

                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>

                  REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'

                  dtac list_inject_iffD1 THEN' etac conjE THEN'

                  (if k = i

                  then EVERY' [dtac (mk_InN_inject n i),

                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),

                    atac, atac, hyp_subst_tac] THEN'

                    CONJ_WRAP' (fn i'' =>

                      EVERY' [rtac impI, dtac (sym RS trans),

                        rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),

                        etac (from_to_sbd RS arg_cong),

                        REPEAT_DETERM o etac allE,

                        dtac (mk_conjunctN n i), dtac mp, atac,

                        dtac (mk_conjunctN n i'), dtac mp, atac,

                        dtac (mk_conjunctN n i''), etac mp, etac sym])

                    ks

                  else etac (mk_InN_not_InM i k RS notE)))

                (rev ks))

              ks)

          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])

      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1

  end;

fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs

  to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's

  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss

  map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =

  let

    val n = length beh_defs;

    val ks = 1 upto n;

    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,

      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,

        (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =

      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),

        rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,

        rtac conjI,

          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),

          rtac @{thm singletonI},

        rtac conjI,

          rtac @{thm UN_least}, rtac Lev_sbd,

        rtac conjI,

          rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,

          rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},

          etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,

        rtac conjI,

          rtac ballI, etac @{thm UN_E}, rtac conjI,

          if n = 1 then K all_tac else rtac (mk_sumEN n),

          EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>

            fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>

            EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),

              rtac exI, rtac conjI,

              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'

              else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'

                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),

              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>

                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),

                  rtac trans_fun_cong_image_id_id_apply,

                  etac set_rv_Lev, TRY o atac, etac conjI, atac])

              (take m set_naturals) set_rv_Levs),

              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>

                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},

                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,

                  if n = 1 then rtac refl else atac, atac, rtac subsetI,

                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],

                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',

                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},

                  if n = 1 then rtac refl else atac])

              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])

          ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss),

          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals,

            (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>

            EVERY' [rtac ballI,

              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],

              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),

              rtac exI, rtac conjI,

              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'

              else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'

                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),

              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>

                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),

                  rtac trans_fun_cong_image_id_id_apply,

                  etac set_rv_Lev, TRY o atac, etac conjI, atac])

              (take m set_naturals) set_rv_Levs),

              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>

                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},

                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,

                  if n = 1 then rtac refl else atac, atac, rtac subsetI,

                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],

                  REPEAT_DETERM_N 4 o etac thin_rl,

                  rtac set_image_Lev,

                  atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',

                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},

                  if n = 1 then rtac refl else atac])

              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])

          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~

            (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),

        (**)

          rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,

          etac notE, etac @{thm UN_I[OF UNIV_I]},

        (*root isNode*)

          rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),

          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},

          CONVERSION (Conv.top_conv

            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),

          if n = 1 then rtac refl else rtac (mk_sum_casesN n i),

          EVERY' (map2 (fn set_natural => fn coalg_set =>

            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),

              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])

            (take m set_naturals) (take m coalg_sets)),

          CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>

            EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},

              rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,

              rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,

              atac, rtac subsetI,

              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],

              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),

              rtac @{thm singletonI}, dtac length_Lev',

              etac @{thm set_mp[OF equalityD1[OF arg_cong[OF

                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},

              rtac rv_Nil])

          (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];

    fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),

      ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =

      EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,

        rtac (@{thm if_P} RS

          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),

        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),

        rtac Lev_0, rtac @{thm singletonI},

        CONVERSION (Conv.top_conv

          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),

        if n = 1 then K all_tac

        else (rtac (sum_case_weak_cong RS trans) THEN'

          rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),

        rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),

        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>

          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,

            rtac trans, rtac @{thm Shift_def},

            rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,

            REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,

            etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},

            rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,

            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>

              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],

                dtac list_inject_iffD1, etac conjE,

                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),

                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),

                  atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]

                else etac (mk_InN_not_InM i' i'' RS notE)])

            (rev ks),

            rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},

            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,

            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,

            rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,

            rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,

            dtac asm_rl, dtac asm_rl, dtac asm_rl,

            dtac (Lev_Suc RS equalityD1 RS set_mp),

            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>

              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],

                dtac list_inject_iffD1, etac conjE,

                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),

                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),

                  atac, atac, hyp_subst_tac, atac]

                else etac (mk_InN_not_InM i' i'' RS notE)])

            (rev ks),

            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,

            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,

            CONVERSION (Conv.top_conv

              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),

            if n = 1 then K all_tac

            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),

            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,

            rtac refl])

        ks to_sbd_injs from_to_sbds)];

  in

    (rtac mor_cong THEN'