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