src/HOL/Tools/BNF/bnf_lfp_tactics.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61334 8d40ddaa427f
child 61841 4d3527b94f2a
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     1 (*  Title:      HOL/Tools/BNF/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: Proof.context -> int -> thm -> thm list -> thm -> thm -> thm list list ->
    12     thm list -> thm list -> tactic
    13   val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
    14   val mk_alg_select_tac: Proof.context -> thm -> tactic
    15   val mk_alg_set_tac: Proof.context -> thm -> tactic
    16   val mk_bd_card_order_tac: Proof.context -> thm list -> tactic
    17   val mk_bd_limit_tac: Proof.context -> int -> thm -> tactic
    18   val mk_card_of_min_alg_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> tactic
    19   val mk_copy_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list list -> tactic
    20   val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
    21     thm list -> thm list -> thm list -> tactic
    22   val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
    23     thm list -> tactic
    24   val mk_ctor_set_tac: Proof.context -> thm -> thm -> thm list -> tactic
    25   val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
    26     thm list -> tactic
    27   val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    28     thm -> thm -> thm list -> thm list -> thm list list -> tactic
    29   val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
    30   val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
    31     tactic
    32   val mk_init_induct_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> tactic
    33   val mk_init_unique_mor_tac: Proof.context -> cterm list -> int -> thm -> thm -> thm list ->
    34     thm list -> thm list -> thm list -> thm list -> tactic
    35   val mk_fold_unique_mor_tac: Proof.context -> thm list -> thm list -> thm list -> thm -> thm ->
    36     thm -> tactic
    37   val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    38   val mk_least_min_alg_tac: Proof.context -> thm -> thm -> tactic
    39   val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    40     thm list -> tactic
    41   val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> int -> tactic
    42   val mk_map_id0_tac: Proof.context -> thm list -> thm -> tactic
    43   val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> tactic
    44   val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
    45   val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
    46     thm list -> tactic
    47   val mk_min_algs_card_of_tac: Proof.context -> ctyp -> cterm -> int -> thm -> thm list ->
    48     thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
    49   val mk_min_algs_least_tac: Proof.context -> ctyp -> cterm -> thm -> thm list -> thm list -> tactic
    50   val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
    51   val mk_min_algs_tac: Proof.context -> thm -> thm list -> tactic
    52   val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list ->
    53     tactic
    54   val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
    55     thm list list -> tactic
    56   val mk_mor_UNIV_tac: Proof.context -> int -> thm list -> thm -> tactic
    57   val mk_mor_comp_tac: Proof.context -> thm -> thm list list -> thm list -> tactic
    58   val mk_mor_convol_tac: Proof.context -> 'a list -> thm -> tactic
    59   val mk_mor_elim_tac: Proof.context -> thm -> tactic
    60   val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic
    61   val mk_mor_fold_tac: Proof.context -> ctyp -> cterm -> thm list -> thm -> thm -> tactic
    62   val mk_mor_select_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    63     thm list list -> thm list -> tactic
    64   val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic
    65   val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
    66     thm list -> tactic
    67   val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
    68   val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
    69   val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list ->
    70     int -> tactic
    71   val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
    72     cterm list -> thm list -> int -> tactic
    73   val mk_set_map0_tac: Proof.context -> thm -> tactic
    74   val mk_set_tac: Proof.context -> thm -> tactic
    75   val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> 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 val fst_snd_convs = @{thms fst_conv snd_conv};
    86 val ord_eq_le_trans = @{thm ord_eq_le_trans};
    87 val subset_trans = @{thm subset_trans};
    88 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    89 val rev_bspec = Drule.rotate_prems 1 bspec;
    90 val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
    91 val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
    92 
    93 fun mk_alg_set_tac ctxt alg_def =
    94   EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
    95    REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
    96 
    97 fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
    98   (EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
    99   REPEAT_DETERM o FIRST'
   100     [EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
   101     EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
   102     EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
   103       FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
   104   etac ctxt @{thm emptyE}) 1;
   105 
   106 fun mk_mor_elim_tac ctxt mor_def =
   107   (dtac ctxt (mor_def RS iffD1) THEN'
   108   REPEAT o etac ctxt conjE THEN'
   109   TRY o rtac ctxt @{thm image_subsetI} THEN'
   110   etac ctxt bspec THEN'
   111   assume_tac ctxt) 1;
   112 
   113 fun mk_mor_incl_tac ctxt mor_def map_ids =
   114   (rtac ctxt (mor_def RS iffD2) THEN'
   115   rtac ctxt conjI THEN'
   116   CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
   117     map_ids THEN'
   118   CONJ_WRAP' (fn thm =>
   119     (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
   120 
   121 fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids =
   122   let
   123     val fbetw_tac =
   124       EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
   125         etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
   126     fun mor_tac (set_map, map_comp_id) =
   127       EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
   128         rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
   129          REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
   130       CONJ_WRAP' (fn thm =>
   131         FIRST' [rtac ctxt subset_UNIV,
   132           (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
   133             etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
   134       rtac ctxt (map_comp_id RS arg_cong);
   135   in
   136     (dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
   137     REPEAT o etac ctxt conjE THEN'
   138     rtac ctxt conjI THEN'
   139     CONJ_WRAP' (K fbetw_tac) set_maps THEN'
   140     CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1
   141   end;
   142 
   143 fun mk_mor_str_tac ctxt ks mor_def =
   144   (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
   145   CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN'
   146   CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1;
   147 
   148 fun mk_mor_convol_tac ctxt ks mor_def =
   149   (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
   150   CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN'
   151   CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt @{thm fst_convol'}, rtac ctxt o_apply])) ks) 1;
   152 
   153 fun mk_mor_UNIV_tac ctxt m morEs mor_def =
   154   let
   155     val n = length morEs;
   156     fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
   157       rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
   158       rtac ctxt sym, rtac ctxt o_apply];
   159   in
   160     EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
   161     rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
   162     REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1),
   163     CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
   164       etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1
   165   end;
   166 
   167 fun mk_copy_tac ctxt m alg_def mor_def alg_sets set_mapss =
   168   let
   169     val n = length alg_sets;
   170     fun set_tac thm =
   171       EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
   172         rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
   173     val alg_tac =
   174       CONJ_WRAP' (fn (set_maps, alg_set) =>
   175         EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
   176           rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
   177           rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
   178       (set_mapss ~~ alg_sets);
   179 
   180     val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
   181       CONJ_WRAP' (fn (set_maps, alg_set) =>
   182         EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
   183           etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
   184           EVERY' (map set_tac (drop m set_maps))])
   185       (set_mapss ~~ alg_sets);
   186   in
   187     (REPEAT_DETERM_N n o rtac ctxt exI THEN' rtac ctxt conjI THEN'
   188     rtac ctxt (alg_def RS iffD2) THEN' alg_tac THEN' rtac ctxt (mor_def RS iffD2) THEN' mor_tac) 1
   189   end;
   190 
   191 fun mk_bd_limit_tac ctxt n bd_Cinfinite =
   192   EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite},
   193     REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI},
   194     REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI},
   195     rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI,
   196     CONJ_WRAP' (fn i =>
   197       EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
   198       (0 upto n - 1),
   199     assume_tac ctxt] 1;
   200 
   201 fun mk_min_algs_tac ctxt worel in_congs =
   202   let
   203     val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
   204       assume_tac ctxt, etac ctxt arg_cong];
   205     fun minH_tac thm =
   206       EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
   207         REPEAT_DETERM_N (length in_congs) o minG_tac, rtac ctxt refl];
   208   in
   209     (rtac ctxt (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ctxt iffD2 THEN'
   210     rtac ctxt meta_eq_to_obj_eq THEN' rtac ctxt (worel RS @{thm wo_rel.adm_wo_def}) THEN'
   211     REPEAT_DETERM_N 3 o rtac ctxt allI THEN' rtac ctxt impI THEN'
   212     CONJ_WRAP_GEN' (EVERY' [rtac ctxt prod_injectI, rtac ctxt conjI]) minH_tac in_congs) 1
   213   end;
   214 
   215 fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
   216   rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
   217   rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
   218   assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
   219   hyp_subst_tac ctxt, rtac ctxt refl] 1;
   220 
   221 fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   222   suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
   223   let
   224     val induct = worel RS
   225       Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   226     val src = 1 upto m + 1;
   227     val dest = (m + 1) :: (1 upto m);
   228     val absorbAs_tac = if m = 0 then K (all_tac)
   229       else EVERY' [rtac ctxt @{thm ordIso_transitive}, rtac ctxt @{thm csum_cong1},
   230         rtac ctxt @{thm ordIso_transitive},
   231         BNF_Tactics.mk_rotate_eq_tac ctxt (rtac ctxt @{thm ordIso_refl} THEN'
   232           FIRST' [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum},
   233             rtac ctxt @{thm Card_order_cexp}])
   234         @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
   235         src dest,
   236         rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt ctrans, rtac ctxt @{thm ordLeq_csum1},
   237         FIRST' [rtac ctxt @{thm Card_order_csum}, rtac ctxt @{thm card_of_Card_order}],
   238         rtac ctxt @{thm ordLeq_cexp1}, rtac ctxt suc_Cnotzero, rtac ctxt @{thm Card_order_csum}];
   239 
   240     val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
   241       rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
   242       assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
   243       dtac ctxt mp, etac ctxt @{thm underS_E},
   244       dtac ctxt mp, etac ctxt @{thm underS_Field},
   245       REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
   246 
   247     fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans},
   248       rtac ctxt @{thm card_of_ordIso_subst}, etac ctxt min_alg, rtac ctxt @{thm Un_Cinfinite_bound},
   249       minG_tac, rtac ctxt ctrans, rtac ctxt @{thm card_of_image}, rtac ctxt ctrans, rtac ctxt in_bd, rtac ctxt ctrans,
   250       rtac ctxt @{thm cexp_mono1}, rtac ctxt @{thm csum_mono1},
   251       REPEAT_DETERM_N m o rtac ctxt @{thm csum_mono2},
   252       CONJ_WRAP_GEN' (rtac ctxt @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
   253       REPEAT_DETERM o FIRST'
   254         [rtac ctxt @{thm card_of_Card_order}, rtac ctxt @{thm Card_order_csum},
   255         rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order],
   256       rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1}, absorbAs_tac,
   257       rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite},
   258       rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order,
   259       rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq},
   260       resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
   261       rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite];
   262   in
   263     (rtac ctxt induct THEN'
   264     rtac ctxt impI THEN'
   265     CONJ_WRAP' mk_minH_tac (min_algs ~~ in_bds)) 1
   266   end;
   267 
   268 fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets =
   269   let
   270     val induct = worel RS
   271       Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   272 
   273     val minG_tac =
   274       EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   275         dtac ctxt mp, etac ctxt @{thm underS_Field}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt];
   276 
   277     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
   278       rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
   279       REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
   280       REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)];
   281   in
   282     (rtac ctxt induct THEN'
   283     rtac ctxt impI THEN'
   284     CONJ_WRAP' mk_minH_tac (min_algs ~~ alg_sets)) 1
   285   end;
   286 
   287 fun mk_alg_min_alg_tac ctxt m alg_def min_alg_defs bd_limit bd_Cinfinite
   288     set_bdss min_algs min_alg_monos =
   289   let
   290     val n = length min_algs;
   291     fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
   292       [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
   293        etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
   294     fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
   295       EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
   296         EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
   297         rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
   298         rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
   299         rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
   300         assume_tac ctxt, rtac ctxt set_mp,
   301         rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
   302         rtac ctxt @{thm image_eqI}, rtac ctxt refl,
   303         rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
   304         REPEAT_DETERM o etac ctxt conjE,
   305         CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
   306           EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
   307             etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
   308           set_bds];
   309   in
   310     (rtac ctxt (alg_def RS iffD2) THEN'
   311     CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1
   312   end;
   313 
   314 fun mk_card_of_min_alg_tac ctxt min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite =
   315   EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
   316     rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
   317     rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
   318     rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
   319     REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
   320 
   321 fun mk_least_min_alg_tac ctxt min_alg_def least =
   322   EVERY' [rtac ctxt (min_alg_def RS ord_eq_le_trans), rtac ctxt @{thm UN_least},
   323     dtac ctxt least, dtac ctxt mp, assume_tac ctxt,
   324     REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
   325 
   326 fun mk_alg_select_tac ctxt Abs_inverse =
   327   EVERY' [rtac ctxt ballI,
   328     REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
   329   unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
   330 
   331 fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
   332     set_maps str_init_defs =
   333   let
   334     val n = length alg_sets;
   335     val fbetw_tac =
   336       CONJ_WRAP'
   337         (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
   338           etac ctxt CollectE, assume_tac ctxt])) alg_sets;
   339     val mor_tac =
   340       CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
   341     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
   342       EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
   343         rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
   344         rtac ctxt (str_init_def RS @{thm ssubst_mem}),
   345         etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
   346           rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
   347           assume_tac ctxt]];
   348   in
   349     EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
   350       rtac ctxt (Thm.permute_prems 0 1 mor_comp), etac ctxt (Thm.permute_prems 0 1 mor_comp),
   351       rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, fbetw_tac, mor_tac, rtac ctxt mor_incl_min_alg,
   352       rtac ctxt (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1
   353   end;
   354 
   355 fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl =
   356   let
   357     val n = length card_of_min_algs;
   358   in
   359     EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
   360       REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
   361       rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
   362       rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
   363       rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
   364       rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
   365       SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
   366       etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
   367   end;
   368 
   369 fun mk_init_unique_mor_tac ctxt cts m
   370     alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
   371   let
   372     val n = length least_min_algs;
   373     val ks = (1 upto n);
   374 
   375     fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
   376       REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
   377       REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
   378     fun cong_tac ct map_cong0 = EVERY'
   379       [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
   380       REPEAT_DETERM_N m o rtac ctxt refl,
   381       REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
   382 
   383     fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
   384       EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
   385         REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
   386         REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
   387         rtac ctxt trans, mor_tac morE in_mono,
   388         rtac ctxt trans, cong_tac ct map_cong0,
   389         rtac ctxt sym, mor_tac morE in_mono];
   390 
   391     fun mk_unique_tac (k, least_min_alg) =
   392       select_prem_tac ctxt n (etac ctxt @{thm prop_restrict}) k THEN' rtac ctxt least_min_alg THEN'
   393       rtac ctxt (alg_def RS iffD2) THEN'
   394       CONJ_WRAP' mk_alg_tac (cts ~~ (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s))));
   395   in
   396     CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
   397   end;
   398 
   399 fun mk_init_induct_tac ctxt m alg_def alg_min_alg least_min_algs alg_sets =
   400   let
   401     val n = length least_min_algs;
   402 
   403     fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
   404       REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
   405       REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
   406       rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
   407       REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
   408       CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
   409       CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
   410         alg_sets];
   411 
   412     fun mk_induct_tac least_min_alg =
   413       rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
   414       rtac ctxt (alg_def RS iffD2) THEN'
   415       CONJ_WRAP' mk_alg_tac alg_sets;
   416   in
   417     CONJ_WRAP' mk_induct_tac least_min_algs 1
   418   end;
   419 
   420 fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
   421   unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   422   EVERY' [rtac ctxt conjI,
   423     CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
   424     CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
   425       EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
   426         EVERY' (map2 (fn Rep => fn set_map =>
   427           EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep])
   428         Reps (drop m set_maps))])
   429     (Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1;
   430 
   431 fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
   432   unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   433   EVERY' [rtac ctxt conjI,
   434     CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
   435     CONJ_WRAP' (fn (ct, thm) =>
   436       EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
   437         rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
   438         EVERY' (map (fn Abs_inverse =>
   439           EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
   440             assume_tac ctxt])
   441         Abs_inverses)])
   442     (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
   443 
   444 fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
   445   (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
   446   REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
   447   rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   448 
   449 fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
   450   let
   451     fun mk_unique type_def =
   452       EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
   453         rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
   454         EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
   455         rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
   456         rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
   457   in
   458     CONJ_WRAP' mk_unique type_defs 1
   459   end;
   460 
   461 fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
   462   EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans),
   463     rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
   464     EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
   465       ctor_o_folds),
   466     rtac ctxt sym, rtac ctxt id_apply] 1;
   467 
   468 fun mk_rec_tac ctxt rec_defs foldx fst_recs =
   469   unfold_thms_tac ctxt
   470     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   471   EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt (foldx RS @{thm arg_cong[of _ _ snd]}),
   472     rtac ctxt @{thm snd_convol'}] 1;
   473 
   474 fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor =
   475   unfold_thms_tac ctxt
   476     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
   477   etac ctxt fold_unique_mor 1;
   478 
   479 fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   480   let
   481     val n = length set_mapss;
   482     val ks = 1 upto n;
   483 
   484     fun mk_IH_tac Rep_inv Abs_inv set_map =
   485       DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
   486         dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
   487         hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
   488         assume_tac ctxt, assume_tac ctxt];
   489 
   490     fun mk_closed_tac (k, (morE, set_maps)) =
   491       EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
   492         rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
   493         REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
   494         EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
   495 
   496     fun mk_induct_tac (Rep, Rep_inv) =
   497       EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
   498   in
   499     (rtac ctxt mp THEN' rtac ctxt impI THEN'
   500     DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
   501     rtac ctxt init_induct THEN'
   502     DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
   503   end;
   504 
   505 fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts =
   506   let
   507     val n = length weak_ctor_inducts;
   508     val ks = 1 upto n;
   509     fun mk_inner_induct_tac induct i =
   510       EVERY' [rtac ctxt allI, fo_rtac ctxt induct,
   511         select_prem_tac ctxt n (dtac ctxt @{thm meta_spec2}) i,
   512         REPEAT_DETERM_N n o
   513           EVERY' [dtac ctxt meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
   514             REPEAT_DETERM o dtac ctxt @{thm meta_spec}, etac ctxt (spec RS meta_mp),
   515             assume_tac ctxt],
   516         assume_tac ctxt];
   517   in
   518     EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct),
   519       EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
   520       REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
   521       CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
   522   end;
   523 
   524 fun mk_map_tac ctxt m n foldx map_comp_id map_cong0 =
   525   EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans,
   526     rtac ctxt o_apply,
   527     rtac ctxt trans, rtac ctxt (map_comp_id RS arg_cong), rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong),
   528     REPEAT_DETERM_N m o rtac ctxt refl,
   529     REPEAT_DETERM_N n o (EVERY' (map (rtac ctxt) [trans, o_apply, id_apply])),
   530     rtac ctxt sym, rtac ctxt o_apply] 1;
   531 
   532 fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
   533   rtac ctxt fold_unique 1 THEN
   534   unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   535   ALLGOALS (assume_tac ctxt);
   536 
   537 fun mk_set_tac ctxt foldx = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
   538   rtac ctxt trans, rtac ctxt foldx, rtac ctxt sym, rtac ctxt o_apply] 1;
   539 
   540 fun mk_ctor_set_tac ctxt set set_map set_maps =
   541   let
   542     val n = length set_maps;
   543     fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
   544       rtac ctxt @{thm Union_image_eq};
   545   in
   546     EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong,
   547       rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
   548       REPEAT_DETERM_N (n - 1) o rtac ctxt Un_cong,
   549       EVERY' (map mk_UN set_maps)] 1
   550   end;
   551 
   552 fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i =
   553   let
   554     val n = length ctor_maps;
   555 
   556     fun useIH set_nat = EVERY' [rtac ctxt trans, rtac ctxt @{thm image_UN}, rtac ctxt trans, rtac ctxt @{thm SUP_cong},
   557       rtac ctxt refl, Goal.assume_rule_tac ctxt, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm SUP_cong},
   558       rtac ctxt set_nat, rtac ctxt refl, rtac ctxt @{thm UN_simps(10)}];
   559 
   560     fun mk_set_nat cset ctor_map ctor_set set_nats =
   561       EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym,
   562         rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong,
   563           ctor_set RS trans]),
   564         rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]),
   565         rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)),
   566         REPEAT_DETERM_N (n - 1) o EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]),
   567         EVERY' (map useIH (drop m set_nats))];
   568   in
   569     (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   570   end;
   571 
   572 fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
   573   let
   574     val n = length ctor_sets;
   575 
   576     fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI,
   577       Goal.assume_rule_tac ctxt, rtac ctxt bd_Cinfinite];
   578 
   579     fun mk_set_nat ctor_set set_bds =
   580       EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set,
   581         rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i - 1)),
   582         REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
   583         EVERY' (map useIH (drop m set_bds))];
   584   in
   585     (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   586   end;
   587 
   588 fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
   589   let
   590     fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm];
   591 
   592     fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt,
   593       CONJ_WRAP' (fn thm =>
   594         EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
   595 
   596     fun mk_map_cong0 ctor_map map_cong0 set_setss =
   597       EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
   598         rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt trans, rtac ctxt (map_cong0 RS arg_cong),
   599         EVERY' (map use_asm (map hd set_setss)),
   600         EVERY' (map useIH (transpose (map tl set_setss))),
   601         rtac ctxt sym, rtac ctxt ctor_map];
   602   in
   603     (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   604   end;
   605 
   606 fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
   607   EVERY' (rtac ctxt induct ::
   608   @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
   609     EVERY' [rtac ctxt impI, etac ctxt (nchotomy RS @{thm nchotomy_relcomppE}),
   610       REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
   611       rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
   612       rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
   613       REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
   614       REPEAT_DETERM_N (length le_rel_OOs) o
   615         EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
   616   ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
   617 
   618 (* BNF tactics *)
   619 
   620 fun mk_map_id0_tac ctxt map_id0s unique =
   621   (rtac ctxt sym THEN' rtac ctxt unique THEN'
   622   EVERY' (map (fn thm =>
   623     EVERY' [rtac ctxt trans, rtac ctxt @{thm id_comp}, rtac ctxt trans, rtac ctxt sym, rtac ctxt @{thm comp_id},
   624       rtac ctxt (thm RS sym RS arg_cong)]) map_id0s)) 1;
   625 
   626 fun mk_map_comp0_tac ctxt map_comp0s ctor_maps unique iplus1 =
   627   let
   628     val i = iplus1 - 1;
   629     val unique' = Thm.permute_prems 0 i unique;
   630     val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
   631     val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
   632     fun mk_comp comp simp =
   633       EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, rtac ctxt o_apply,
   634         rtac ctxt trans, rtac ctxt (simp RS arg_cong), rtac ctxt trans, rtac ctxt simp,
   635         rtac ctxt trans, rtac ctxt (comp RS arg_cong), rtac ctxt sym, rtac ctxt o_apply];
   636   in
   637     (rtac ctxt sym THEN' rtac ctxt unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
   638   end;
   639 
   640 fun mk_set_map0_tac ctxt set_nat =
   641   EVERY' (map (rtac ctxt) [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
   642 
   643 fun mk_bd_card_order_tac ctxt bd_card_orders =
   644   CONJ_WRAP_GEN' (rtac ctxt @{thm card_order_csum}) (rtac ctxt) bd_card_orders 1;
   645 
   646 fun mk_wit_tac ctxt n ctor_set wit =
   647   REPEAT_DETERM (assume_tac ctxt 1 ORELSE
   648     EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
   649     REPEAT_DETERM o
   650       (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
   651         (eresolve_tac ctxt wit ORELSE'
   652         (dresolve_tac ctxt wit THEN'
   653           (etac ctxt FalseE ORELSE'
   654           EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
   655             REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
   656 
   657 fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
   658   ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
   659   let
   660     val m = length ctor_set_incls;
   661     val n = length ctor_set_set_inclss;
   662 
   663     val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
   664     val in_Irel = nth in_Irels (i - 1);
   665     val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
   666     val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
   667     val if_tac =
   668       EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
   669         rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
   670         EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
   671           EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
   672             rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
   673             rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor])
   674         passive_set_map0s ctor_set_incls),
   675         CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
   676           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
   677             rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
   678             CONJ_WRAP' (fn thm =>
   679               EVERY' (map (etac ctxt) [thm RS subset_trans, le_arg_cong_ctor_dtor]))
   680             ctor_set_set_incls,
   681             rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
   682         (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
   683         CONJ_WRAP' (fn conv =>
   684           EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
   685           REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
   686           REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
   687           rtac ctxt (ctor_inject RS iffD1), rtac ctxt trans, rtac ctxt sym, rtac ctxt ctor_map,
   688           etac ctxt eq_arg_cong_ctor_dtor])
   689         fst_snd_convs];
   690     val only_if_tac =
   691       EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
   692         rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
   693         CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
   694           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
   695             rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
   696             rtac ctxt passive_set_map0, rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
   697             CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
   698               (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
   699                 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
   700                 dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
   701                 dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
   702                 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   703                   @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   704                 hyp_subst_tac ctxt,
   705                 dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
   706                 REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
   707             (rev (active_set_map0s ~~ in_Irels))])
   708         (ctor_sets ~~ passive_set_map0s),
   709         rtac ctxt conjI,
   710         REPEAT_DETERM_N 2 o EVERY' [rtac ctxt trans, rtac ctxt ctor_map, rtac ctxt (ctor_inject RS iffD2),
   711           rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
   712           REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
   713           EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
   714             dtac ctxt set_rev_mp, assume_tac ctxt,
   715             dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
   716             REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
   717               @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
   718             hyp_subst_tac ctxt,
   719             dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
   720             REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
   721           in_Irels),
   722           assume_tac ctxt]]
   723   in
   724     EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
   725   end;
   726 
   727 fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
   728     ctor_rels =
   729   CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
   730       REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
   731       unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
   732       HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN'
   733         etac ctxt (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
   734         EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
   735           etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
   736           rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
   737           rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
   738           REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
   739           REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN'
   740           rtac ctxt rel_funI THEN'
   741           etac ctxt (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
   742     (ctor_rec_defs ~~ ctor_fold_transfers);
   743 
   744 fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
   745   let val n = length ks;
   746   in
   747     unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
   748     EVERY' [REPEAT_DETERM o rtac ctxt allI, rtac ctxt ctor_induct2,
   749       EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
   750         EVERY' [rtac ctxt impI, dtac ctxt (ctor_rel RS iffD1), rtac ctxt (IH RS @{thm spec2} RS mp),
   751           etac ctxt rel_mono_strong0,
   752           REPEAT_DETERM_N m o rtac ctxt @{thm ballI[OF ballI[OF imp_refl]]},
   753           EVERY' (map (fn j =>
   754             EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) j, rtac ctxt @{thm ballI[OF ballI]},
   755               Goal.assume_rule_tac ctxt]) ks)])
   756       IHs ctor_rels rel_mono_strong0s)] 1
   757   end;
   758 
   759 fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =
   760   let
   761     val n = length map_transfers;
   762   in
   763     unfold_thms_tac ctxt
   764       @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
   765     unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
   766     HEADGOAL (EVERY'
   767       [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctxt ctor_rel_induct,
   768       EVERY' (map (fn map_transfer => EVERY'
   769         [REPEAT_DETERM o resolve_tac ctxt [allI, impI, @{thm vimage2pI}],
   770         SELECT_GOAL (unfold_thms_tac ctxt folds),
   771         etac ctxt @{thm predicate2D_vimage2p},
   772         rtac ctxt (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
   773         REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer},
   774         REPEAT_DETERM_N n o rtac ctxt @{thm vimage2p_rel_fun},
   775         assume_tac ctxt])
   776       map_transfers)])
   777   end;
   778 
   779 end;