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