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