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