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