src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49227 2652319c394e
child 49306 c13fff97a8df
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/Tools/bnf_lfp_tactics.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Copyright   2012
     5 
     6 Tactics for the datatype construction.
     7 *)
     8 
     9 signature BNF_LFP_TACTICS =
    10 sig
    11   val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
    12     thm list -> tactic
    13   val mk_alg_not_empty_tac: thm -> thm list -> thm list -> tactic
    14   val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
    15   val mk_alg_set_tac: thm -> tactic
    16   val mk_bd_card_order_tac: thm list -> tactic
    17   val mk_bd_limit_tac: int -> thm -> tactic
    18   val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
    19   val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic
    20   val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
    21   val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
    22   val mk_fld_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
    23     {prems: 'a, context: Proof.context} -> tactic
    24   val mk_fld_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list ->
    25     thm list -> tactic
    26   val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
    27   val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
    28     {prems: 'a, context: Proof.context} -> tactic
    29   val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    30     {prems: 'a, context: Proof.context} -> tactic
    31   val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
    32   val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    33     thm list -> tactic
    34   val mk_iso_alt_tac: thm list -> thm -> tactic
    35   val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    36   val mk_least_min_alg_tac: thm -> thm -> tactic
    37   val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
    38     thm list list list -> thm list -> tactic
    39   val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
    40   val mk_map_id_tac: thm list -> thm -> tactic
    41   val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
    42   val mk_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
    43   val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
    44     {prems: 'a, context: Proof.context} -> tactic
    45   val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
    46     thm -> thm -> thm -> thm -> thm -> thm -> tactic
    47   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
    48   val mk_min_algs_mono_tac: thm -> tactic
    49   val mk_min_algs_tac: thm -> thm list -> tactic
    50   val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
    51   val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
    52     {prems: 'a, context: Proof.context} -> tactic
    53   val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
    54   val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
    55   val mk_mor_convol_tac: 'a list -> thm -> tactic
    56   val mk_mor_elim_tac: thm -> tactic
    57   val mk_mor_incl_tac: thm -> thm list -> tactic
    58   val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
    59   val mk_mor_iter_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
    60   val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
    61     thm list -> tactic
    62   val mk_mor_str_tac: 'a list -> thm -> tactic
    63   val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    64   val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
    65     thm -> thm list -> thm list -> thm list list -> tactic
    66   val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
    67     {prems: 'a, context: Proof.context} -> tactic
    68   val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
    69     thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
    70   val mk_set_natural_tac: thm -> tactic
    71   val mk_set_simp_tac: thm -> thm -> thm list -> tactic
    72   val mk_set_tac: thm -> tactic
    73   val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    74   val mk_wit_tac: int -> thm list -> thm list -> tactic
    75   val mk_wpull_tac: thm -> tactic
    76 end;
    77 
    78 structure BNF_LFP_Tactics : BNF_LFP_TACTICS =
    79 struct
    80 
    81 open BNF_Tactics
    82 open BNF_LFP_Util
    83 open BNF_Util
    84 
    85 fun mk_alg_set_tac alg_def =
    86   dtac (alg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) 1 THEN
    87   REPEAT_DETERM (etac conjE 1) THEN
    88   EVERY' [etac bspec, rtac CollectI] 1 THEN
    89   REPEAT_DETERM (etac conjI 1) THEN atac 1;
    90 
    91 fun mk_alg_not_empty_tac alg_set alg_sets wits =
    92   (EVERY' [rtac notI, hyp_subst_tac, ftac alg_set] THEN'
    93   REPEAT_DETERM o FIRST'
    94     [rtac @{thm subset_UNIV},
    95     EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
    96     EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
    97     EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac,
    98       FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
    99   etac @{thm emptyE}) 1;
   100 
   101 fun mk_mor_elim_tac mor_def =
   102   (dtac (subst OF [mor_def]) THEN'
   103   REPEAT o etac conjE THEN'
   104   TRY o rtac @{thm image_subsetI} THEN'
   105   etac bspec THEN'
   106   atac) 1;
   107 
   108 fun mk_mor_incl_tac mor_def map_id's =
   109   (stac mor_def THEN'
   110   rtac conjI THEN'
   111   CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm set_mp}, stac @{thm id_apply}, atac]))
   112     map_id's THEN'
   113   CONJ_WRAP' (fn thm =>
   114    (EVERY' [rtac ballI, rtac trans, rtac @{thm id_apply}, stac thm, rtac refl])) map_id's) 1;
   115 
   116 fun mk_mor_comp_tac mor_def set_natural's map_comp_ids =
   117   let
   118     val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
   119     fun mor_tac (set_natural', map_comp_id) =
   120       EVERY' [rtac ballI, stac o_apply, rtac trans,
   121         rtac trans, dtac @{thm rev_bspec}, atac, etac arg_cong,
   122          REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
   123       CONJ_WRAP' (fn thm =>
   124         FIRST' [rtac @{thm subset_UNIV},
   125           (EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
   126             etac bspec, etac @{thm set_mp}, atac])]) set_natural' THEN'
   127       rtac (map_comp_id RS arg_cong);
   128   in
   129     (dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN'
   130     REPEAT o etac conjE THEN'
   131     rtac conjI THEN'
   132     CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
   133     CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1
   134   end;
   135 
   136 fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_congLs =
   137   let
   138     val fbetw_tac = EVERY' [rtac ballI, etac @{thm set_mp}, etac imageI];
   139     fun Collect_tac set_natural' =
   140       CONJ_WRAP' (fn thm =>
   141         FIRST' [rtac @{thm subset_UNIV},
   142           (EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac subset_trans,
   143             etac @{thm image_mono}, atac])]) set_natural';
   144     fun mor_tac (set_natural', ((morE, map_comp_id), map_congL)) =
   145       EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
   146          REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
   147          etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_natural',
   148          rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural',
   149          rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_congL RS arg_cong),
   150          REPEAT_DETERM_N (length morEs) o
   151            (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
   152   in
   153     (stac mor_def THEN'
   154     dtac (alg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) THEN'
   155     dtac (alg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) THEN'
   156     REPEAT o etac conjE THEN'
   157     rtac conjI THEN'
   158     CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
   159     CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_congLs))) 1
   160   end;
   161 
   162 fun mk_mor_str_tac ks mor_def =
   163   (stac mor_def THEN' rtac conjI THEN'
   164   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
   165   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac refl])) ks) 1;
   166 
   167 fun mk_mor_convol_tac ks mor_def =
   168   (stac mor_def THEN' rtac conjI THEN'
   169   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
   170   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1;
   171 
   172 fun mk_mor_UNIV_tac m morEs mor_def =
   173   let
   174     val n = length morEs;
   175     fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
   176       rtac CollectI, CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n),
   177       rtac sym, rtac o_apply];
   178   in
   179     EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
   180     stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
   181     REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS subst),
   182     CONJ_WRAP' (K (EVERY' [rtac ballI, REPEAT_DETERM o etac allE, rtac trans,
   183       etac (o_apply RS subst), rtac o_apply])) morEs] 1
   184   end;
   185 
   186 fun mk_iso_alt_tac mor_images mor_inv =
   187   let
   188     val n = length mor_images;
   189     fun if_wrap_tac thm =
   190       EVERY' [rtac ssubst, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI,
   191         rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac]
   192     val if_tac =
   193       EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE],
   194         rtac conjI, atac, CONJ_WRAP' if_wrap_tac mor_images];
   195     val only_if_tac =
   196       EVERY' [rtac conjI, etac conjunct1, EVERY' (map (fn thm =>
   197         EVERY' [rtac exE, rtac @{thm bij_betw_ex_weakE}, etac (conjunct2 RS thm)])
   198         (map (mk_conjunctN n) (1 upto n))), REPEAT o rtac exI, rtac conjI, rtac mor_inv,
   199         etac conjunct1, atac, atac, REPEAT_DETERM_N n o atac,
   200         CONJ_WRAP' (K (etac conjunct2)) mor_images];
   201   in
   202     (rtac iffI THEN' if_tac THEN' only_if_tac) 1
   203   end;
   204 
   205 fun mk_copy_str_tac set_natural's alg_def alg_sets =
   206   let
   207     val n = length alg_sets;
   208     val bij_betw_inv_tac =
   209       EVERY' [etac thin_rl, REPEAT_DETERM_N n o EVERY' [dtac @{thm bij_betwI}, atac, atac],
   210         REPEAT_DETERM_N (2 * n) o etac thin_rl, REPEAT_DETERM_N (n - 1) o etac conjI, atac];
   211     fun set_tac thms =
   212       EVERY' [rtac @{thm ord_eq_le_trans}, resolve_tac thms, rtac subset_trans,
   213           etac @{thm image_mono}, rtac equalityD1, etac @{thm bij_betw_imageE}];
   214     val copy_str_tac =
   215       CONJ_WRAP' (fn (thms, thm) =>
   216         EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac @{thm set_mp},
   217           rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
   218           REPEAT_DETERM o rtac @{thm subset_UNIV}, REPEAT_DETERM_N n o (set_tac thms)])
   219       (set_natural's ~~ alg_sets);
   220   in
   221     (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
   222     stac alg_def THEN' copy_str_tac) 1
   223   end;
   224 
   225 fun mk_copy_alg_tac set_natural's alg_sets mor_def iso_alt copy_str =
   226   let
   227     val n = length alg_sets;
   228     val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
   229     fun set_tac thms =
   230       EVERY' [rtac @{thm ord_eq_le_trans}, resolve_tac thms, rtac subset_trans,
   231         REPEAT_DETERM o etac conjE, etac @{thm image_mono},
   232         rtac equalityD1, etac @{thm bij_betw_imageE}];
   233     val mor_tac =
   234       CONJ_WRAP' (fn (thms, thm) =>
   235         EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
   236           REPEAT_DETERM o rtac @{thm subset_UNIV}, REPEAT_DETERM_N n o (set_tac thms)])
   237       (set_natural's ~~ alg_sets);
   238   in
   239     (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
   240     etac copy_str THEN' REPEAT_DETERM o atac THEN'
   241     rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
   242     CONJ_WRAP' (K atac) alg_sets) 1
   243   end;
   244 
   245 fun mk_ex_copy_alg_tac n copy_str copy_alg =
   246   EVERY' [REPEAT_DETERM_N n o rtac exI, rtac conjI, etac copy_str,
   247     REPEAT_DETERM_N n o atac,
   248     REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
   249     REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}, etac copy_alg,
   250     REPEAT_DETERM_N n o atac,
   251     REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
   252     REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}] 1;
   253 
   254 fun mk_bd_limit_tac n bd_Cinfinite =
   255   EVERY' [REPEAT_DETERM o etac conjE, rtac rev_mp, rtac @{thm Cinfinite_limit_finite},
   256     REPEAT_DETERM_N n o rtac @{thm finite.insertI}, rtac @{thm finite.emptyI},
   257     REPEAT_DETERM_N n o etac @{thm insert_subsetI}, rtac @{thm empty_subsetI},
   258     rtac bd_Cinfinite, rtac impI, etac bexE, rtac bexI,
   259     CONJ_WRAP' (fn i =>
   260       EVERY' [etac bspec, REPEAT_DETERM_N i o rtac @{thm insertI2}, rtac @{thm insertI1}])
   261       (0 upto n - 1),
   262     atac] 1;
   263 
   264 fun mk_min_algs_tac worel in_congs =
   265   let
   266     val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
   267     fun minH_tac thm =
   268       EVERY' [rtac @{thm Un_cong}, minG_tac, rtac @{thm image_cong}, rtac thm,
   269         REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
   270   in
   271     (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
   272     rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
   273     REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
   274     CONJ_WRAP_GEN' (EVERY' [rtac ssubst, rtac @{thm Pair_eq}, rtac conjI]) minH_tac in_congs) 1
   275   end;
   276 
   277 fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
   278   rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2},
   279   rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac,
   280   rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac, rtac refl] 1;
   281 
   282 fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   283   suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
   284   let
   285     val induct = worel RS
   286       Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   287     val src = 1 upto m + 1;
   288     val dest = (m + 1) :: (1 upto m);
   289     val absorbAs_tac = if m = 0 then K (all_tac)
   290       else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
   291         rtac @{thm ordIso_transitive},
   292         BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
   293           FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum},
   294             rtac @{thm Card_order_cexp}])
   295         @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
   296         src dest,
   297         rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac ctrans, rtac @{thm ordLeq_csum1},
   298         FIRST' [rtac @{thm Card_order_csum}, rtac @{thm card_of_Card_order}],
   299         rtac @{thm ordLeq_cexp1}, rtac suc_Cnotzero, rtac @{thm Card_order_csum}];
   300 
   301     val minG_tac = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordLess_imp_ordLeq},
   302       rtac @{thm ordLess_transitive}, rtac @{thm card_of_underS}, rtac suc_Card_order,
   303       atac, rtac suc_Asuc, rtac ballI, etac allE, dtac mp, etac @{thm underS_E},
   304       dtac mp, etac @{thm underS_Field}, REPEAT o etac conjE, atac, rtac Asuc_Cinfinite]
   305 
   306     fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans},
   307       rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound},
   308       minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans,
   309       rtac @{thm cexp_mono1_Cnotzero}, rtac @{thm csum_mono1},
   310       REPEAT_DETERM_N m o rtac @{thm csum_mono2},
   311       CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
   312       REPEAT_DETERM o FIRST'
   313         [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, rtac Asuc_Cinfinite],
   314       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac bd_Card_order,
   315       rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1_Cnotzero}, absorbAs_tac,
   316       rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite},
   317       rtac Asuc_Cinfinite, rtac bd_Card_order,
   318       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac Asuc_Cnotzero,
   319       rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq},
   320       TRY o rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac suc_Cinfinite,
   321       rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite];
   322   in
   323     (rtac induct THEN'
   324     rtac impI THEN'
   325     CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1
   326   end;
   327 
   328 fun mk_min_algs_least_tac cT ct worel min_algs alg_sets =
   329   let
   330     val induct = worel RS
   331       Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   332 
   333     val minG_tac = EVERY' [rtac @{thm UN_least}, etac allE, dtac mp, etac @{thm underS_E},
   334       dtac mp, etac @{thm underS_Field}, REPEAT_DETERM o etac conjE, atac];
   335 
   336     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac @{thm ord_eq_le_trans}, etac min_alg,
   337       rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI},
   338       REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set,
   339       REPEAT_DETERM o FIRST' [atac, etac subset_trans THEN' minG_tac]];
   340   in
   341     (rtac induct THEN'
   342     rtac impI THEN'
   343     CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1
   344   end;
   345 
   346 fun mk_alg_min_alg_tac m alg_def min_alg_defs bd_limit bd_Cinfinite
   347     set_bdss min_algs min_alg_monos =
   348   let
   349     val n = length min_algs;
   350     fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
   351       [rtac bexE, rtac @{thm cardSuc_UNION_Cinfinite}, rtac bd_Cinfinite, rtac mono,
   352        etac (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac set_bds];
   353     fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
   354       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   355         EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac bexE,
   356         rtac bd_limit, REPEAT_DETERM_N (n - 1) o etac conjI, atac,
   357         rtac (min_alg_def RS @{thm set_mp[OF equalityD2]}),
   358         rtac @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac thin_rl, atac, rtac @{thm set_mp},
   359         rtac equalityD2, rtac min_alg, atac, rtac UnI2, rtac @{thm image_eqI}, rtac refl,
   360         rtac CollectI, REPEAT_DETERM_N m o dtac asm_rl, REPEAT_DETERM_N n o etac thin_rl,
   361         REPEAT_DETERM o etac conjE,
   362         CONJ_WRAP' (K (FIRST' [atac,
   363           EVERY' [etac subset_trans, rtac subsetI, rtac @{thm UN_I},
   364             etac @{thm underS_I}, atac, atac]]))
   365           set_bds];
   366   in
   367     (rtac (alg_def RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
   368     CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1
   369   end;
   370 
   371 fun mk_card_of_min_alg_tac min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite =
   372   EVERY' [stac min_alg_def, rtac @{thm UNION_Cinfinite_bound},
   373     rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order,
   374     rtac @{thm ordLess_imp_ordLeq}, rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of,
   375     REPEAT_DETERM o etac conjE, atac, rtac Asuc_Cinfinite] 1;
   376 
   377 fun mk_least_min_alg_tac min_alg_def least =
   378   EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
   379     REPEAT_DETERM o etac conjE, atac] 1;
   380 
   381 fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
   382   EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
   383   Local_Defs.unfold_tac ctxt (Abs_inverse :: @{thms fst_conv snd_conv}) THEN atac 1;
   384 
   385 fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
   386     alg_sets set_natural's str_init_defs =
   387   let
   388     val n = length alg_sets;
   389     val fbetw_tac =
   390       CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm rev_bspec}, etac CollectE, atac])) alg_sets;
   391     val mor_tac =
   392       CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
   393     fun alg_epi_tac ((alg_set, str_init_def), set_natural') =
   394       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
   395         rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
   396         REPEAT_DETERM o FIRST' [rtac @{thm subset_UNIV},
   397           EVERY' [rtac @{thm ord_eq_le_trans}, resolve_tac set_natural', rtac @{thm subset_trans},
   398             etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
   399   in
   400     (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN'
   401     rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
   402     stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
   403     stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_natural's)) 1
   404   end;
   405 
   406 fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
   407     mor_comp mor_select mor_incl_min_alg {context = ctxt, prems = _} =
   408   let
   409     val n = length card_of_min_algs;
   410     val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso},
   411       rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac];
   412     fun internalize_tac card_of = EVERY' [rtac subst, rtac @{thm internalize_card_of_ordLeq2},
   413       rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac subst,
   414       rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}];
   415   in
   416     (rtac rev_mp THEN'
   417     REPEAT_DETERM_N (2 * n) o (rtac mp THEN' rtac @{thm ex_mono} THEN' rtac impI) THEN'
   418     REPEAT_DETERM_N (n + 1) o etac thin_rl THEN' rtac (alg_min_alg RS copy_alg_ex) THEN'
   419     REPEAT_DETERM_N n o atac THEN'
   420     REPEAT_DETERM_N n o card_of_ordIso_tac THEN'
   421     EVERY' (map internalize_tac card_of_min_algs) THEN'
   422     rtac impI THEN'
   423     REPEAT_DETERM o eresolve_tac [exE, conjE] THEN'
   424     REPEAT_DETERM o rtac exI THEN'
   425     rtac mor_select THEN' atac THEN' rtac CollectI THEN'
   426     REPEAT_DETERM o rtac exI THEN'
   427     rtac conjI THEN' rtac refl THEN' atac THEN'
   428     K (Local_Defs.unfold_tac ctxt (Abs_inverse :: @{thms fst_conv snd_conv})) THEN'
   429     etac mor_comp THEN' etac mor_incl_min_alg) 1
   430   end;
   431 
   432 fun mk_init_unique_mor_tac m
   433     alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_congs =
   434   let
   435     val n = length least_min_algs;
   436     val ks = (1 upto n);
   437 
   438     fun mor_tac morE in_mono = EVERY' [etac morE, rtac @{thm set_mp}, rtac in_mono,
   439       REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
   440       REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
   441     fun cong_tac map_cong = EVERY' [rtac (map_cong RS arg_cong),
   442       REPEAT_DETERM_N m o rtac refl,
   443       REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
   444 
   445     fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong))) = EVERY' [rtac ballI, rtac CollectI,
   446       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
   447       REPEAT_DETERM_N m o rtac @{thm subset_UNIV},
   448       REPEAT_DETERM_N n o (etac @{thm subset_trans} THEN' rtac @{thm Collect_restrict}),
   449       rtac trans, mor_tac morE in_mono,
   450       rtac trans, cong_tac map_cong,
   451       rtac sym, mor_tac morE in_mono];
   452 
   453     fun mk_unique_tac (k, least_min_alg) =
   454       select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
   455       stac alg_def THEN'
   456       CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_congs)));
   457   in
   458     CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
   459   end;
   460 
   461 fun mk_init_induct_tac m alg_def alg_min_alg least_min_algs alg_sets =
   462   let
   463     val n = length least_min_algs;
   464 
   465     fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI,
   466       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
   467       REPEAT_DETERM_N m o rtac @{thm subset_UNIV},
   468       REPEAT_DETERM_N n o (etac @{thm subset_trans} THEN' rtac @{thm Collect_restrict}),
   469       rtac mp, etac bspec, rtac CollectI,
   470       REPEAT_DETERM_N m o (rtac conjI THEN' atac),
   471       CONJ_WRAP' (K (etac @{thm subset_trans} THEN' rtac @{thm Collect_restrict})) alg_sets,
   472       CONJ_WRAP' (K (rtac ballI THEN' etac @{thm prop_restrict} THEN' atac)) alg_sets];
   473 
   474     fun mk_induct_tac least_min_alg =
   475       rtac ballI THEN' etac @{thm prop_restrict} THEN' rtac least_min_alg THEN'
   476       stac alg_def THEN'
   477       CONJ_WRAP' mk_alg_tac alg_sets;
   478   in
   479     CONJ_WRAP' mk_induct_tac least_min_algs 1
   480   end;
   481 
   482 fun mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
   483   (K (Local_Defs.unfold_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   484   EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   485   EVERY' (map rtac inver_Abss) THEN'
   486   EVERY' (map rtac inver_Reps)) 1;
   487 
   488 fun mk_mor_Abs_tac inv inver_Abss inver_Reps =
   489   (rtac inv THEN'
   490   EVERY' (map2 (fn inver_Abs => fn inver_Rep =>
   491     EVERY' [rtac conjI, rtac @{thm subset_UNIV}, rtac conjI, rtac inver_Rep, rtac inver_Abs])
   492     inver_Abss inver_Reps)) 1;
   493 
   494 fun mk_mor_iter_tac cT ct iter_defs ex_mor mor =
   495   (EVERY' (map stac iter_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
   496   REPEAT_DETERM_N (length iter_defs) o etac exE THEN'
   497   rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
   498 
   499 fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter =
   500   let
   501     fun mk_unique type_def =
   502       EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
   503         rtac ballI, resolve_tac init_unique_mors,
   504         EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
   505         rtac mor_comp, rtac mor_Abs, atac,
   506         rtac mor_comp, rtac mor_Abs, rtac mor_iter];
   507   in
   508     CONJ_WRAP' mk_unique type_defs 1
   509   end;
   510 
   511 fun mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iters =
   512   EVERY' [stac unf_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter,
   513     rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   514     EVERY' (map (fn thm =>
   515       rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) fld_o_iters),
   516     rtac sym, rtac @{thm id_apply}] 1;
   517 
   518 fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}=
   519   Local_Defs.unfold_tac ctxt
   520     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   521   EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}),
   522     rtac @{thm snd_convol'}] 1;
   523 
   524 fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   525   let
   526     val n = length set_natural'ss;
   527     val ks = 1 upto n;
   528 
   529     fun mk_IH_tac Rep_inv Abs_inv set_natural' =
   530       DETERM o EVERY' [dtac @{thm meta_mp}, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
   531         dtac @{thm set_rev_mp}, rtac equalityD1, rtac set_natural', etac imageE,
   532         hyp_subst_tac, rtac (Abs_inv RS ssubst), etac @{thm set_mp},
   533         atac, atac];
   534 
   535     fun mk_closed_tac (k, (morE, set_natural's)) =
   536       EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
   537         rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac,
   538         REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
   539         EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's)), atac];
   540 
   541     fun mk_induct_tac (Rep, Rep_inv) =
   542       EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))];
   543   in
   544     (rtac mp THEN' rtac impI THEN'
   545     DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
   546     rtac init_induct THEN'
   547     DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_natural'ss))) 1
   548   end;
   549 
   550 fun mk_fld_induct2_tac cTs cts fld_induct weak_fld_inducts {context = ctxt, prems = _} =
   551   let
   552     val n = length weak_fld_inducts;
   553     val ks = 1 upto n;
   554     fun mk_inner_induct_tac induct i =
   555       EVERY' [rtac allI, fo_rtac induct ctxt,
   556         select_prem_tac n (dtac @{thm meta_spec2}) i,
   557         REPEAT_DETERM_N n o
   558           EVERY' [dtac @{thm meta_mp} THEN_ALL_NEW Goal.norm_hhf_tac,
   559             REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS @{thm meta_mp}), atac],
   560         atac];
   561   in
   562     EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts fld_induct),
   563       EVERY' (map2 mk_inner_induct_tac weak_fld_inducts ks), rtac impI,
   564       REPEAT_DETERM o eresolve_tac [conjE, allE],
   565       CONJ_WRAP' (K atac) ks] 1
   566   end;
   567 
   568 fun mk_map_tac m n iter map_comp_id map_cong =
   569   EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, rtac trans, rtac o_apply,
   570     rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
   571     REPEAT_DETERM_N m o rtac refl,
   572     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, @{thm id_apply}])),
   573     rtac sym, rtac o_apply] 1;
   574 
   575 fun mk_map_unique_tac m mor_def iter_unique_mor map_comp_ids map_congs =
   576   let
   577     val n = length map_congs;
   578     fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
   579       rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
   580       rtac (cong RS arg_cong),
   581       REPEAT_DETERM_N m o rtac refl,
   582       REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, @{thm id_apply}]))];
   583   in
   584     EVERY' [rtac iter_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
   585       CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
   586       CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
   587   end;
   588 
   589 fun mk_set_tac iter = EVERY' [rtac ext, rtac trans, rtac o_apply,
   590   rtac trans, rtac iter, rtac sym, rtac o_apply] 1;
   591 
   592 fun mk_set_simp_tac set set_natural' set_natural's =
   593   let
   594     val n = length set_natural's;
   595     fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
   596       rtac @{thm Union_image_eq};
   597   in
   598     EVERY' [rtac (set RS @{thm pointfreeE} RS trans), rtac @{thm Un_cong},
   599       rtac (trans OF [set_natural', @{thm trans[OF fun_cong[OF image_id] id_apply]}]),
   600       REPEAT_DETERM_N (n - 1) o rtac @{thm Un_cong},
   601       EVERY' (map mk_UN set_natural's)] 1
   602   end;
   603 
   604 fun mk_set_nat_tac m induct_tac set_natural'ss
   605     map_simps csets set_simps i {context = ctxt, prems = _} =
   606   let
   607     val n = length map_simps;
   608 
   609     fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
   610       rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
   611       rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
   612 
   613     fun mk_set_nat cset map_simp set_simp set_nats =
   614       EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl,
   615         rtac sym, rtac (trans OF [map_simp RS HOL_arg_cong cset, set_simp RS trans]),
   616         rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
   617         rtac sym, rtac (nth set_nats (i - 1)),
   618         REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
   619         EVERY' (map useIH (drop m set_nats))];
   620   in
   621     (induct_tac THEN' EVERY' (map4 mk_set_nat csets map_simps set_simps set_natural'ss)) 1
   622   end;
   623 
   624 fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} =
   625   let
   626     val n = length set_simps;
   627 
   628     fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI,
   629       Goal.assume_rule_tac ctxt, rtac bd_Cinfinite];
   630 
   631     fun mk_set_nat set_simp set_bds =
   632       EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac set_simp,
   633         rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_bds (i - 1)),
   634         REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
   635         EVERY' (map useIH (drop m set_bds))];
   636   in
   637     (induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1
   638   end;
   639 
   640 fun mk_mcong_tac induct_tac set_setsss map_congs map_simps {context = ctxt, prems = _} =
   641   let
   642     fun use_asm thm = EVERY' [etac bspec, etac @{thm set_rev_mp}, rtac thm];
   643 
   644     fun useIH set_sets = EVERY' [rtac mp, Goal.assume_rule_tac ctxt,
   645       CONJ_WRAP' (fn thm =>
   646         EVERY' [rtac ballI, etac bspec, etac @{thm set_rev_mp}, etac thm]) set_sets];
   647 
   648     fun mk_map_cong map_simp map_cong set_setss =
   649       EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
   650         rtac trans, rtac map_simp, rtac trans, rtac (map_cong RS arg_cong),
   651         EVERY' (map use_asm (map hd set_setss)),
   652         EVERY' (map useIH (transpose (map tl set_setss))),
   653         rtac sym, rtac map_simp];
   654   in
   655     (induct_tac THEN' EVERY' (map3 mk_map_cong map_simps map_congs set_setsss)) 1
   656   end;
   657 
   658 fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
   659   let
   660     fun use_asm thm = etac (thm RS subset_trans);
   661 
   662     fun useIH set_sets = EVERY' [rtac subsetI, rtac mp, Goal.assume_rule_tac ctxt,
   663       rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [etac (thm RS subset_trans), atac]) set_sets];
   664 
   665     fun mk_incl alg_set set_setss =
   666       EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   667         rtac (alg_min_alg RS alg_set),
   668         EVERY' (map use_asm (map hd set_setss)),
   669         EVERY' (map useIH (transpose (map tl set_setss)))];
   670   in
   671     (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
   672   end;
   673 
   674 fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss fld_injects =
   675   let
   676     val n = length wpulls;
   677     val ks = 1 upto n;
   678     val ls = 1 upto m;
   679 
   680     fun use_pass_asm thm = rtac conjI THEN' etac (thm RS subset_trans);
   681     fun use_act_asm thm = etac (thm RS subset_trans) THEN' atac;
   682 
   683     fun useIH set_sets i = EVERY' [rtac ssubst, rtac @{thm wpull_def},
   684        REPEAT_DETERM_N m o etac thin_rl, select_prem_tac n (dtac asm_rl) i,
   685        rtac allI, rtac allI, rtac impI, REPEAT_DETERM o etac conjE,
   686        REPEAT_DETERM o dtac @{thm meta_spec},
   687        dtac @{thm meta_mp}, atac,
   688        dtac @{thm meta_mp}, atac, etac mp,
   689        rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets,
   690        rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets,
   691        atac];
   692 
   693     fun mk_subset thm = EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm Un_least}, atac,
   694       REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
   695       REPEAT_DETERM_N n o
   696         EVERY' [rtac @{thm UN_least}, rtac CollectE, etac @{thm set_rev_mp}, atac,
   697           REPEAT_DETERM o etac conjE, atac]];
   698 
   699     fun mk_wpull wpull map_simp set_simps set_setss fld_inject =
   700       EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   701         rtac rev_mp, rtac wpull,
   702         EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls),
   703         EVERY' (map2 useIH (transpose (map tl set_setss)) ks),
   704         rtac impI, REPEAT_DETERM_N (m + n) o etac thin_rl,
   705         dtac @{thm subst[OF wpull_def, of "%x. x"]}, etac allE, etac allE, etac impE,
   706         rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
   707           CONJ_WRAP' (K (rtac subset_refl)) ks,
   708         rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
   709           CONJ_WRAP' (K (rtac subset_refl)) ks,
   710         rtac subst, rtac fld_inject, rtac trans, rtac sym, rtac map_simp,
   711         rtac trans, atac, rtac map_simp, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
   712         hyp_subst_tac, rtac bexI, rtac conjI, rtac map_simp, rtac map_simp, rtac CollectI,
   713         CONJ_WRAP' mk_subset set_simps];
   714   in
   715     (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss fld_injects)) 1
   716   end;
   717 
   718 (* BNF tactics *)
   719 
   720 fun mk_map_id_tac map_ids unique =
   721   (rtac sym THEN' rtac unique THEN'
   722   EVERY' (map (fn thm =>
   723     EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
   724       rtac (thm RS sym RS arg_cong)]) map_ids)) 1;
   725 
   726 fun mk_map_comp_tac map_comps map_simps unique iplus1 =
   727   let
   728     val i = iplus1 - 1;
   729     val unique' = Thm.permute_prems 0 i unique;
   730     val map_comps' = drop i map_comps @ take i map_comps;
   731     val map_simps' = drop i map_simps @ take i map_simps;
   732     fun mk_comp comp simp =
   733       EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
   734         rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
   735         rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
   736   in
   737     (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' map_simps')) 1
   738   end;
   739 
   740 fun mk_set_natural_tac set_nat =
   741   EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
   742 
   743 fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg =
   744   EVERY' [rtac ctrans, rtac @{thm card_of_mono1}, rtac subsetI, etac rev_mp,
   745     rtac incl, rtac ctrans, rtac card_of_min_alg, rtac @{thm cexp_mono2_Cnotzero},
   746     rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm csum_Cnotzero2},
   747     rtac @{thm ctwo_Cnotzero}, rtac sucbd_Cnotzero] 1;
   748 
   749 fun mk_bd_card_order_tac bd_card_orders =
   750   (rtac @{thm card_order_cpow} THEN'
   751     CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders) 1;
   752 
   753 fun mk_wpull_tac wpull =
   754   EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
   755     rtac wpull, REPEAT_DETERM o atac] 1;
   756 
   757 fun mk_wit_tac n set_simp wit =
   758   REPEAT_DETERM (atac 1 ORELSE
   759     EVERY' [dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
   760     REPEAT_DETERM o
   761       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
   762         (eresolve_tac wit ORELSE'
   763         (dresolve_tac wit THEN'
   764           (etac FalseE ORELSE'
   765           EVERY' [hyp_subst_tac, dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
   766             REPEAT_DETERM_N n o etac UnE]))))] 1);
   767 
   768 fun mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject
   769   fld_unf set_naturals set_incls set_set_inclss =
   770   let
   771     val m = length set_incls;
   772     val n = length set_set_inclss;
   773 
   774     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
   775     val in_Irel = nth in_Irels (i - 1);
   776     val le_arg_cong_fld_unf = fld_unf RS arg_cong RS @{thm ord_eq_le_trans};
   777     val eq_arg_cong_fld_unf = fld_unf RS arg_cong RS trans;
   778     val if_tac =
   779       EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   780         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   781         EVERY' (map2 (fn set_natural => fn set_incl =>
   782           EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac set_natural,
   783             rtac @{thm ord_eq_le_trans}, rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
   784             rtac (set_incl RS @{thm subset_trans}), etac le_arg_cong_fld_unf])
   785         passive_set_naturals set_incls),
   786         CONJ_WRAP' (fn (in_Irel, (set_natural, set_set_incls)) =>
   787           EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_natural, rtac @{thm image_subsetI},
   788             rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   789             CONJ_WRAP' (fn thm =>
   790               EVERY' (map etac [thm RS @{thm subset_trans}, le_arg_cong_fld_unf]))
   791             set_set_incls,
   792             rtac conjI, rtac refl, rtac refl])
   793         (in_Irels ~~ (active_set_naturals ~~ set_set_inclss)),
   794         CONJ_WRAP' (fn conv =>
   795           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   796           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   797           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
   798           rtac (fld_inject RS iffD1), rtac trans, rtac sym, rtac map_simp,
   799           etac eq_arg_cong_fld_unf])
   800         @{thms fst_conv snd_conv}];
   801     val only_if_tac =
   802       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   803         rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   804         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
   805           EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_simp, rtac @{thm Un_least},
   806             rtac @{thm ord_eq_le_trans}, rtac @{thm box_equals[OF _ refl]},
   807             rtac passive_set_natural, rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
   808             atac,
   809             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   810               (fn (active_set_natural, in_Irel) => EVERY' [rtac @{thm ord_eq_le_trans},
   811                 rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
   812                 dtac @{thm set_rev_mp}, etac @{thm image_mono}, etac imageE,
   813                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1),
   814                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   815                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
   816                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   817             (rev (active_set_naturals ~~ in_Irels))])
   818         (set_simps ~~ passive_set_naturals),
   819         rtac conjI,
   820         REPEAT_DETERM_N 2 o EVERY'[rtac trans, rtac map_simp, rtac (fld_inject RS iffD2),
   821           rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   822           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   823           EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac @{thm set_rev_mp}, atac,
   824             dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1), dtac @{thm someI_ex},
   825             REPEAT_DETERM o etac conjE, atac]) in_Irels),
   826           atac]]
   827   in
   828     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   829   end;
   830 
   831 end;