src/HOL/Tools/BNF/bnf_gfp_tactics.ML
author haftmann
Sat Mar 22 08:37:43 2014 +0100 (2014-03-22)
changeset 56248 67dc9549fa15
parent 56179 6b5c46582260
child 56765 644f0d4820a1
permissions -rw-r--r--
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_gfp_tactics.ML
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     5
    Copyright   2012
blanchet@48975
     6
blanchet@48975
     7
Tactics for the codatatype construction.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@48975
    10
signature BNF_GFP_TACTICS =
blanchet@48975
    11
sig
traytel@55197
    12
  val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
wenzelm@51798
    13
  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
traytel@55197
    14
  val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
blanchet@48975
    15
  val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
traytel@56017
    16
  val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list ->
wenzelm@51798
    17
    thm list list -> tactic
traytel@55197
    18
  val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
blanchet@48975
    19
  val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
blanchet@48975
    20
    tactic
blanchet@48975
    21
  val mk_coalg_set_tac: thm -> tactic
traytel@55197
    22
  val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
blanchet@48975
    23
  val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
blanchet@48975
    24
    thm list list -> tactic
traytel@55197
    25
  val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
traytel@55197
    26
    thm list list -> tactic
blanchet@48975
    27
  val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
traytel@55197
    28
  val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
traytel@55197
    29
  val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
traytel@51893
    30
  val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
traytel@51893
    31
  val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
wenzelm@51798
    32
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
traytel@55197
    33
  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
blanchet@48975
    34
  val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
traytel@56179
    35
  val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic
traytel@56113
    36
  val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
traytel@55197
    37
    tactic
blanchet@48975
    38
  val mk_incl_lsbis_tac: int -> int -> thm -> tactic
blanchet@48975
    39
  val mk_length_Lev'_tac: thm -> tactic
wenzelm@51798
    40
  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
traytel@54841
    41
  val mk_map_comp0_tac: thm list -> thm list -> thm -> tactic
wenzelm@51798
    42
  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
traytel@55644
    43
    thm list list -> thm list list -> thm list list list -> thm list -> tactic
blanchet@53270
    44
  val mk_map_id0_tac: thm list -> thm -> thm -> tactic
traytel@55602
    45
  val mk_map_tac: int -> int -> thm -> thm -> thm -> thm -> tactic
traytel@55197
    46
  val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
traytel@55197
    47
  val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
traytel@55541
    48
  val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
traytel@55197
    49
    thm list -> thm list -> tactic
blanchet@48975
    50
  val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
blanchet@48975
    51
  val mk_mor_UNIV_tac: thm list -> thm -> tactic
traytel@55197
    52
  val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
traytel@55197
    53
    thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
traytel@55577
    54
    thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
traytel@55577
    55
    thm list list -> thm list -> thm list -> tactic
blanchet@55414
    56
  val mk_mor_case_sum_tac: 'a list -> thm -> tactic
blanchet@48975
    57
  val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
blanchet@48975
    58
  val mk_mor_elim_tac: thm -> tactic
traytel@56113
    59
  val mk_mor_col_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
blanchet@48975
    60
    thm list -> thm list list -> thm list list -> tactic
blanchet@48975
    61
  val mk_mor_incl_tac: thm -> thm list -> tactic
blanchet@48975
    62
  val mk_mor_str_tac: 'a list -> thm -> tactic
blanchet@49504
    63
  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
blanchet@49504
    64
    thm list -> tactic
blanchet@48975
    65
  val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
blanchet@48975
    66
    thm list -> thm list -> thm -> thm list -> tactic
traytel@55197
    67
  val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
traytel@55197
    68
    thm list -> thm list -> tactic
traytel@55644
    69
  val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list ->
traytel@55644
    70
    thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic
traytel@55197
    71
  val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
traytel@55197
    72
    int -> thm -> tactic
blanchet@48975
    73
  val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
wenzelm@51798
    74
  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
wenzelm@51798
    75
  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
wenzelm@51798
    76
    thm list -> thm list list -> tactic
traytel@56113
    77
  val mk_set_bd_tac: thm -> thm -> tactic
traytel@56179
    78
  val mk_set_Jset_incl_Jset_tac: int -> thm -> int -> tactic
wenzelm@51798
    79
  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
wenzelm@51798
    80
    thm list -> thm list -> thm list list -> thm list list -> tactic
traytel@56179
    81
  val mk_set_incl_Jset_tac: thm -> tactic
traytel@54841
    82
  val mk_set_ge_tac: int  -> thm -> thm list -> tactic
blanchet@48975
    83
  val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
traytel@56113
    84
  val mk_set_map0_tac: thm -> tactic
blanchet@49504
    85
  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
traytel@55197
    86
  val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
traytel@55197
    87
  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
traytel@54841
    88
  val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic
blanchet@48975
    89
end;
blanchet@48975
    90
blanchet@48975
    91
structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
blanchet@48975
    92
struct
blanchet@48975
    93
blanchet@48975
    94
open BNF_Tactics
blanchet@48975
    95
open BNF_Util
blanchet@51850
    96
open BNF_FP_Util
blanchet@48975
    97
open BNF_GFP_Util
blanchet@48975
    98
traytel@55644
    99
val fst_convol_fun_cong_sym = @{thm fst_convol[unfolded convol_def]} RS fun_cong RS sym;
traytel@49488
   100
val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
blanchet@49305
   101
val nat_induct = @{thm nat_induct};
blanchet@49305
   102
val o_apply_trans_sym = o_apply RS trans RS sym;
blanchet@49305
   103
val ord_eq_le_trans = @{thm ord_eq_le_trans};
blanchet@49305
   104
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
traytel@55644
   105
val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
blanchet@55393
   106
val sum_weak_case_cong = @{thm sum.weak_case_cong};
blanchet@49305
   107
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
traytel@52659
   108
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
traytel@52659
   109
val rev_bspec = Drule.rotate_prems 1 bspec;
traytel@52749
   110
val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
traytel@52749
   111
val converse_shift = @{thm converse_subset_swap} RS iffD1;
blanchet@49305
   112
blanchet@48975
   113
fun mk_coalg_set_tac coalg_def =
traytel@49488
   114
  dtac (coalg_def RS iffD1) 1 THEN
blanchet@48975
   115
  REPEAT_DETERM (etac conjE 1) THEN
traytel@52659
   116
  EVERY' [dtac rev_bspec, atac] 1 THEN
blanchet@48975
   117
  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
blanchet@48975
   118
blanchet@48975
   119
fun mk_mor_elim_tac mor_def =
traytel@56114
   120
  (dtac (mor_def RS iffD1) THEN'
blanchet@48975
   121
  REPEAT o etac conjE THEN'
blanchet@48975
   122
  TRY o rtac @{thm image_subsetI} THEN'
blanchet@48975
   123
  etac bspec THEN'
blanchet@48975
   124
  atac) 1;
blanchet@48975
   125
blanchet@53285
   126
fun mk_mor_incl_tac mor_def map_ids =
traytel@56114
   127
  (rtac (mor_def RS iffD2) THEN'
blanchet@48975
   128
  rtac conjI THEN'
traytel@56114
   129
  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})]))
traytel@56114
   130
    map_ids THEN'
blanchet@48975
   131
  CONJ_WRAP' (fn thm =>
traytel@56114
   132
    (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
blanchet@48975
   133
blanchet@48975
   134
fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
blanchet@48975
   135
  let
traytel@56114
   136
    fun fbetw_tac image = EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac image,
traytel@56114
   137
      etac image, atac];
blanchet@48975
   138
    fun mor_tac ((mor_image, morE), map_comp_id) =
blanchet@48975
   139
      EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
blanchet@48975
   140
        etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
blanchet@48975
   141
  in
traytel@56114
   142
    (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
blanchet@48975
   143
    CONJ_WRAP' fbetw_tac mor_images THEN'
blanchet@48975
   144
    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
blanchet@48975
   145
  end;
blanchet@48975
   146
blanchet@48975
   147
fun mk_mor_UNIV_tac morEs mor_def =
blanchet@48975
   148
  let
blanchet@48975
   149
    val n = length morEs;
wenzelm@55990
   150
    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
blanchet@48975
   151
      rtac UNIV_I, rtac sym, rtac o_apply];
blanchet@48975
   152
  in
blanchet@48975
   153
    EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
traytel@56114
   154
    rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
blanchet@48975
   155
    CONJ_WRAP' (fn i =>
traytel@52659
   156
      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1
blanchet@48975
   157
  end;
blanchet@48975
   158
blanchet@48975
   159
fun mk_mor_str_tac ks mor_UNIV =
traytel@56114
   160
  (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
blanchet@48975
   161
blanchet@55414
   162
fun mk_mor_case_sum_tac ks mor_UNIV =
traytel@56114
   163
  (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
blanchet@48975
   164
traytel@56179
   165
fun mk_set_incl_Jset_tac rec_Suc =
traytel@56113
   166
  EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
traytel@56113
   167
    rec_Suc]) 1;
blanchet@48975
   168
traytel@56179
   169
fun mk_set_Jset_incl_Jset_tac n rec_Suc i =
traytel@56113
   170
  EVERY' (map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc,
traytel@56113
   171
      UnI2, mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1;
blanchet@48975
   172
traytel@56113
   173
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
blanchet@49305
   174
  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   175
    REPEAT_DETERM o rtac allI,
blanchet@48975
   176
    CONJ_WRAP' (fn thm => EVERY'
blanchet@49305
   177
      [rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
blanchet@48975
   178
    REPEAT_DETERM o rtac allI,
blanchet@48975
   179
    CONJ_WRAP' (fn rec_Suc => EVERY'
blanchet@49305
   180
      [rtac ord_eq_le_trans, rtac rec_Suc,
blanchet@48975
   181
        if m = 0 then K all_tac
blanchet@48975
   182
        else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
blanchet@48975
   183
        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
blanchet@48975
   184
          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
blanchet@48975
   185
            rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
blanchet@48975
   186
      rec_Sucs] 1;
blanchet@48975
   187
traytel@56179
   188
fun mk_Jset_minimal_tac ctxt n col_minimal =
traytel@56113
   189
  (CONJ_WRAP' (K (EVERY' [rtac @{thm UN_least}, rtac rev_mp, rtac col_minimal,
blanchet@48975
   190
    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
traytel@56113
   191
    REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1
blanchet@48975
   192
traytel@56113
   193
fun mk_mor_col_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
blanchet@49305
   194
  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   195
    REPEAT_DETERM o rtac allI,
blanchet@48975
   196
    CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
blanchet@48975
   197
    REPEAT_DETERM o rtac allI,
blanchet@48975
   198
    CONJ_WRAP'
blanchet@53289
   199
      (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
blanchet@48975
   200
        EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
blanchet@48975
   201
          if m = 0 then K all_tac
wenzelm@55990
   202
          else EVERY' [rtac Un_cong, rtac @{thm box_equals},
blanchet@53289
   203
            rtac (nth passive_set_map0s (j - 1) RS sym),
blanchet@49305
   204
            rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
traytel@52659
   205
          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
blanchet@53289
   206
            (fn (i, (set_map0, coalg_set)) =>
haftmann@56248
   207
              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm SUP_cong})),
blanchet@53289
   208
                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
haftmann@56248
   209
                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm SUP_cong}),
blanchet@49305
   210
                ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
blanchet@48975
   211
                REPEAT_DETERM o etac allE, atac, atac])
blanchet@53289
   212
            (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
blanchet@53289
   213
      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
blanchet@48975
   214
traytel@56017
   215
fun mk_bis_rel_tac m bis_def in_rels map_comp0s map_cong0s set_map0ss =
blanchet@48975
   216
  let
traytel@56017
   217
    val n = length in_rels;
traytel@56017
   218
    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);
blanchet@48975
   219
traytel@56017
   220
    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
blanchet@48975
   221
      EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
traytel@56017
   222
        etac allE, etac allE, etac impE, atac, etac bexE,
traytel@56017
   223
        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
traytel@56017
   224
        rtac (in_rel RS iffD2), rtac exI, rtac (Drule.rotate_prems 1 conjI),
traytel@56017
   225
        CONJ_WRAP' (fn thm => EVERY' [rtac trans, rtac trans, rtac map_comp0, rtac map_cong0,
traytel@56017
   226
          REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
traytel@56017
   227
          atac])
traytel@56017
   228
        @{thms fst_diag_id snd_diag_id},
traytel@56017
   229
        rtac CollectI,
traytel@56017
   230
        CONJ_WRAP' (fn (i, thm) =>
traytel@56017
   231
          if i <= m
traytel@56017
   232
          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
traytel@56017
   233
            etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
traytel@56017
   234
            rtac @{thm case_prodI}, rtac refl]
traytel@56017
   235
          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
traytel@56017
   236
            rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
traytel@56017
   237
        (1 upto (m + n) ~~ set_map0s)];
blanchet@48975
   238
traytel@56017
   239
    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
blanchet@48975
   240
      EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
blanchet@48975
   241
        etac allE, etac allE, etac impE, atac,
traytel@56017
   242
        dtac (in_rel RS @{thm iffD1}),
traytel@51893
   243
        REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
traytel@56017
   244
          @{thms CollectE Collect_split_in_rel_leE}),
blanchet@53287
   245
        rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
blanchet@55067
   246
        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
blanchet@55067
   247
        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
blanchet@53287
   248
        atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
blanchet@55067
   249
        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
blanchet@55067
   250
        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
blanchet@51761
   251
        rtac trans, rtac map_cong0,
traytel@55541
   252
        REPEAT_DETERM_N m o EVERY' [rtac @{thm Collect_splitD}, etac set_mp, atac],
blanchet@48975
   253
        REPEAT_DETERM_N n o rtac refl,
traytel@51893
   254
        atac, rtac CollectI,
blanchet@48975
   255
        CONJ_WRAP' (fn (i, thm) =>
traytel@55541
   256
          if i <= m then rtac subset_UNIV
blanchet@49305
   257
          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
blanchet@49305
   258
            rtac trans_fun_cong_image_id_id_apply, atac])
blanchet@53289
   259
        (1 upto (m + n) ~~ set_map0s)];
blanchet@48975
   260
  in
blanchet@48975
   261
    EVERY' [rtac (bis_def RS trans),
blanchet@48975
   262
      rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
blanchet@48975
   263
      etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
blanchet@48975
   264
  end;
blanchet@48975
   265
traytel@51893
   266
fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
traytel@56114
   267
  EVERY' [rtac (bis_rel RS iffD2), dtac (bis_rel RS iffD1),
blanchet@48975
   268
    REPEAT_DETERM o etac conjE, rtac conjI,
traytel@52749
   269
    CONJ_WRAP' (K (EVERY' [rtac converse_shift, etac subset_trans,
traytel@51893
   270
      rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
traytel@51893
   271
    CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
traytel@51893
   272
      EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
   273
        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@55541
   274
        REPEAT_DETERM_N m o rtac @{thm conversep_eq},
traytel@51893
   275
        REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
traytel@51893
   276
        rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
blanchet@48975
   277
        REPEAT_DETERM o etac allE,
traytel@51893
   278
        rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
blanchet@48975
   279
traytel@51893
   280
fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
traytel@56114
   281
  EVERY' [rtac (bis_rel RS iffD2), REPEAT_DETERM o dtac (bis_rel RS iffD1),
blanchet@48975
   282
    REPEAT_DETERM o etac conjE, rtac conjI,
traytel@51893
   283
    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
traytel@51893
   284
    CONJ_WRAP' (fn (rel_cong, rel_OO) =>
traytel@51893
   285
      EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
   286
        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@55541
   287
        REPEAT_DETERM_N m o rtac @{thm eq_OO},
traytel@51893
   288
        REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
traytel@51893
   289
        rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
blanchet@48975
   290
        etac @{thm relcompE},
traytel@49488
   291
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
   292
        etac conjE, hyp_subst_tac ctxt,
traytel@51893
   293
        REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
traytel@51893
   294
        etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
blanchet@48975
   295
traytel@55197
   296
fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
traytel@55541
   297
  unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
blanchet@48975
   298
  EVERY' [rtac conjI,
traytel@56114
   299
    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS iffD2) THEN' etac thm) mor_images,
blanchet@48975
   300
    CONJ_WRAP' (fn (coalg_in, morE) =>
traytel@51893
   301
      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
traytel@51893
   302
        etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
traytel@51893
   303
    (coalg_ins ~~ morEs)] 1;
blanchet@48975
   304
traytel@55197
   305
fun mk_bis_Union_tac ctxt bis_def in_monos =
blanchet@48975
   306
  let
blanchet@48975
   307
    val n = length in_monos;
blanchet@48975
   308
    val ks = 1 upto n;
blanchet@48975
   309
  in
blanchet@49504
   310
    unfold_thms_tac ctxt [bis_def] THEN
blanchet@48975
   311
    EVERY' [rtac conjI,
blanchet@48975
   312
      CONJ_WRAP' (fn i =>
blanchet@48975
   313
        EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
blanchet@48975
   314
          dtac conjunct1, etac (mk_conjunctN n i)]) ks,
blanchet@48975
   315
      CONJ_WRAP' (fn (i, in_mono) =>
blanchet@48975
   316
        EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
blanchet@48975
   317
          dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
blanchet@48975
   318
          atac, etac bexE, rtac bexI, atac, rtac in_mono,
traytel@52659
   319
          REPEAT_DETERM_N n o etac @{thm SUP_upper2[OF _ subset_refl]},
blanchet@48975
   320
          atac]) (ks ~~ in_monos)] 1
blanchet@48975
   321
  end;
blanchet@48975
   322
wenzelm@51798
   323
fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
blanchet@48975
   324
  let
blanchet@48975
   325
    val n = length lsbis_defs;
blanchet@48975
   326
  in
blanchet@48975
   327
    EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
blanchet@48975
   328
      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
wenzelm@51798
   329
      hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
blanchet@48975
   330
  end;
blanchet@48975
   331
blanchet@48975
   332
fun mk_incl_lsbis_tac n i lsbis_def =
traytel@52659
   333
  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI,
blanchet@48975
   334
    REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
blanchet@48975
   335
    rtac (mk_nth_conv n i)] 1;
blanchet@48975
   336
traytel@51447
   337
fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
traytel@49488
   338
  EVERY' [rtac (@{thm equiv_def} RS iffD2),
blanchet@48975
   339
traytel@49488
   340
    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
blanchet@49305
   341
    rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
traytel@51447
   342
    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
blanchet@48975
   343
traytel@49488
   344
    rtac conjI, rtac (@{thm sym_def} RS iffD2),
blanchet@49305
   345
    rtac allI, rtac allI, rtac impI, rtac set_mp,
blanchet@48975
   346
    rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
blanchet@48975
   347
traytel@49488
   348
    rtac (@{thm trans_def} RS iffD2),
blanchet@49305
   349
    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
blanchet@48975
   350
    rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
blanchet@48975
   351
    etac @{thm relcompI}, atac] 1;
blanchet@48975
   352
traytel@55197
   353
fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
blanchet@48975
   354
  let
blanchet@48975
   355
    val n = length strT_defs;
blanchet@48975
   356
    val ks = 1 upto n;
traytel@55541
   357
    fun coalg_tac (i, (active_sets, def)) =
blanchet@48975
   358
      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
wenzelm@51798
   359
        hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
blanchet@55414
   360
        rtac (mk_sum_caseN n i), rtac CollectI,
traytel@55541
   361
        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
blanchet@49305
   362
        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
blanchet@48975
   363
          rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
blanchet@48975
   364
          rtac conjI,
blanchet@49305
   365
          rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
blanchet@48975
   366
            etac equalityD1, etac CollectD,
traytel@55577
   367
          rtac ballI,
blanchet@48975
   368
            CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
traytel@55581
   369
              dtac bspec, etac thin_rl, atac, dtac (mk_conjunctN n i),
blanchet@48975
   370
              dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
blanchet@48975
   371
              REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
blanchet@48975
   372
              rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
blanchet@48975
   373
              rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
blanchet@48975
   374
              CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
blanchet@48975
   375
                rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
blanchet@48975
   376
                rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
traytel@55581
   377
          dtac bspec, atac, dtac (mk_conjunctN n i), dtac bspec,
blanchet@48975
   378
          etac @{thm set_mp[OF equalityD1]}, atac,
blanchet@48975
   379
          REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
blanchet@48975
   380
          rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
blanchet@48975
   381
          etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
blanchet@48975
   382
          REPEAT_DETERM_N m o (rtac conjI THEN' atac),
blanchet@48975
   383
          CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
blanchet@48975
   384
            rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
blanchet@48975
   385
            rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
blanchet@48975
   386
  in
blanchet@49504
   387
    unfold_thms_tac ctxt defs THEN
traytel@55541
   388
    CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
blanchet@48975
   389
  end;
blanchet@48975
   390
wenzelm@51798
   391
fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
blanchet@48975
   392
  let
blanchet@48975
   393
    val n = length Lev_0s;
blanchet@48975
   394
    val ks = n downto 1;
blanchet@48975
   395
  in
blanchet@49305
   396
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   397
      REPEAT_DETERM o rtac allI,
blanchet@48975
   398
      CONJ_WRAP' (fn Lev_0 =>
blanchet@49305
   399
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
blanchet@48975
   400
          etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
blanchet@48975
   401
      REPEAT_DETERM o rtac allI,
blanchet@48975
   402
      CONJ_WRAP' (fn Lev_Suc =>
blanchet@49305
   403
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   404
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
wenzelm@51798
   405
            (fn i =>
wenzelm@51798
   406
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
wenzelm@51798
   407
                rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
wenzelm@51798
   408
                REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
blanchet@48975
   409
      Lev_Sucs] 1
blanchet@48975
   410
  end;
blanchet@48975
   411
blanchet@48975
   412
fun mk_length_Lev'_tac length_Lev =
blanchet@48975
   413
  EVERY' [ftac length_Lev, etac ssubst, atac] 1;
blanchet@48975
   414
blanchet@48975
   415
fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
blanchet@48975
   416
  let
blanchet@48975
   417
    val n = length rv_Nils;
blanchet@48975
   418
    val ks = 1 upto n;
blanchet@48975
   419
  in
blanchet@48975
   420
    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
blanchet@48975
   421
      REPEAT_DETERM o rtac allI,
blanchet@48975
   422
      CONJ_WRAP' (fn rv_Cons =>
blanchet@48975
   423
        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
blanchet@48975
   424
          rtac (@{thm append_Nil} RS arg_cong RS trans),
traytel@55606
   425
          rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans), rtac rv_Nil]))
blanchet@48975
   426
        (ks ~~ rv_Nils))
blanchet@48975
   427
      rv_Conss,
blanchet@48975
   428
      REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
blanchet@48975
   429
      EVERY' (map (fn i =>
blanchet@48975
   430
        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
blanchet@48975
   431
          CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
traytel@55606
   432
            rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
traytel@55606
   433
            if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
traytel@55606
   434
            rtac (mk_sum_caseN n i RS trans), atac])
blanchet@48975
   435
          ks])
blanchet@48975
   436
        rv_Conss)
blanchet@48975
   437
      ks)] 1
blanchet@48975
   438
  end;
blanchet@48975
   439
wenzelm@51798
   440
fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
blanchet@48975
   441
  let
blanchet@48975
   442
    val n = length Lev_0s;
blanchet@48975
   443
    val ks = 1 upto n;
blanchet@48975
   444
  in
blanchet@49305
   445
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   446
      REPEAT_DETERM o rtac allI,
blanchet@48975
   447
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
blanchet@49305
   448
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
wenzelm@51798
   449
          etac @{thm singletonE}, hyp_subst_tac ctxt,
blanchet@48975
   450
          CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
blanchet@48975
   451
            (if i = i'
wenzelm@51798
   452
            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
blanchet@48975
   453
              CONJ_WRAP' (fn (i'', Lev_0'') =>
blanchet@48975
   454
                EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
blanchet@49366
   455
                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
blanchet@48975
   456
                  rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
blanchet@49305
   457
                  etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
blanchet@48975
   458
                  rtac @{thm singletonI}])
blanchet@48975
   459
              (ks ~~ Lev_0s)]
blanchet@48975
   460
            else etac (mk_InN_not_InM i' i RS notE)))
blanchet@48975
   461
          ks])
blanchet@48975
   462
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
blanchet@48975
   463
      REPEAT_DETERM o rtac allI,
blanchet@48975
   464
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
blanchet@49305
   465
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   466
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   467
            (fn (i, from_to_sbd) =>
wenzelm@51798
   468
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@48975
   469
                CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   470
                  CONJ_WRAP' (fn i'' =>
blanchet@49305
   471
                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
blanchet@49366
   472
                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
blanchet@48975
   473
                      rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
blanchet@48975
   474
                      rtac conjI, atac, dtac (sym RS trans RS sym),
blanchet@55414
   475
                      rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans),
blanchet@48975
   476
                      etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
blanchet@48975
   477
                      dtac (mk_conjunctN n i), dtac mp, atac,
blanchet@48975
   478
                      dtac (mk_conjunctN n i'), dtac mp, atac,
blanchet@48975
   479
                      dtac (mk_conjunctN n i''), etac mp, atac])
blanchet@48975
   480
                  ks)
blanchet@48975
   481
                ks])
blanchet@48975
   482
          (rev (ks ~~ from_to_sbds))])
blanchet@48975
   483
      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
blanchet@48975
   484
  end;
blanchet@48975
   485
wenzelm@51798
   486
fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
blanchet@48975
   487
  let
blanchet@48975
   488
    val n = length Lev_0s;
blanchet@48975
   489
    val ks = 1 upto n;
blanchet@48975
   490
  in
blanchet@49305
   491
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   492
      REPEAT_DETERM o rtac allI,
blanchet@48975
   493
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
blanchet@49305
   494
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
wenzelm@51798
   495
          etac @{thm singletonE}, hyp_subst_tac ctxt,
blanchet@48975
   496
          CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   497
            CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
blanchet@48975
   498
              (if i = i''
blanchet@48975
   499
              then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
blanchet@49305
   500
                dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
wenzelm@51798
   501
                hyp_subst_tac ctxt,
blanchet@48975
   502
                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   503
                  (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
traytel@49488
   504
                    dtac list_inject_iffD1 THEN' etac conjE THEN'
blanchet@48975
   505
                    (if k = i'
wenzelm@51798
   506
                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
blanchet@48975
   507
                    else etac (mk_InN_not_InM i' k RS notE)))
blanchet@48975
   508
                (rev ks)]
blanchet@48975
   509
              else etac (mk_InN_not_InM i'' i RS notE)))
blanchet@48975
   510
            ks)
blanchet@48975
   511
          ks])
blanchet@48975
   512
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
blanchet@48975
   513
      REPEAT_DETERM o rtac allI,
blanchet@48975
   514
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
blanchet@49305
   515
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   516
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   517
            (fn (i, (from_to_sbd, to_sbd_inj)) =>
wenzelm@51798
   518
              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
blanchet@48975
   519
              CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   520
                dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
blanchet@49305
   521
                dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
blanchet@48975
   522
                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
blanchet@48975
   523
                  REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
traytel@49488
   524
                  dtac list_inject_iffD1 THEN' etac conjE THEN'
blanchet@48975
   525
                  (if k = i
blanchet@48975
   526
                  then EVERY' [dtac (mk_InN_inject n i),
traytel@49488
   527
                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
wenzelm@51798
   528
                    atac, atac, hyp_subst_tac ctxt] THEN'
blanchet@48975
   529
                    CONJ_WRAP' (fn i'' =>
blanchet@48975
   530
                      EVERY' [rtac impI, dtac (sym RS trans),
blanchet@55414
   531
                        rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans),
blanchet@48975
   532
                        etac (from_to_sbd RS arg_cong),
blanchet@48975
   533
                        REPEAT_DETERM o etac allE,
blanchet@48975
   534
                        dtac (mk_conjunctN n i), dtac mp, atac,
blanchet@48975
   535
                        dtac (mk_conjunctN n i'), dtac mp, atac,
blanchet@48975
   536
                        dtac (mk_conjunctN n i''), etac mp, etac sym])
blanchet@48975
   537
                    ks
blanchet@48975
   538
                  else etac (mk_InN_not_InM i k RS notE)))
blanchet@48975
   539
                (rev ks))
blanchet@48975
   540
              ks)
blanchet@48975
   541
          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
blanchet@48975
   542
      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
blanchet@48975
   543
  end;
blanchet@48975
   544
traytel@55577
   545
fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss
traytel@55577
   546
  from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss
traytel@55577
   547
  set_image_Levsss set_map0ss map_comp_ids map_cong0s =
blanchet@48975
   548
  let
blanchet@48975
   549
    val n = length beh_defs;
blanchet@48975
   550
    val ks = 1 upto n;
blanchet@48975
   551
traytel@55577
   552
    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
traytel@55577
   553
      (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
blanchet@49305
   554
      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
blanchet@48975
   555
        rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
blanchet@48975
   556
        rtac conjI,
blanchet@49305
   557
          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
blanchet@48975
   558
          rtac @{thm singletonI},
traytel@55577
   559
        (**)
traytel@55581
   560
          rtac ballI, etac @{thm UN_E},
blanchet@53289
   561
          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
traytel@55541
   562
            (set_Levs, set_image_Levs))))) =>
blanchet@48975
   563
            EVERY' [rtac ballI,
blanchet@48975
   564
              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
traytel@56114
   565
              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
blanchet@48975
   566
              rtac exI, rtac conjI,
traytel@55577
   567
              if n = 1 then rtac refl
traytel@55577
   568
              else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
blanchet@53289
   569
              CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
blanchet@53289
   570
                EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
blanchet@48975
   571
                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
blanchet@48975
   572
                  if n = 1 then rtac refl else atac, atac, rtac subsetI,
blanchet@48975
   573
                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
blanchet@48975
   574
                  REPEAT_DETERM_N 4 o etac thin_rl,
blanchet@48975
   575
                  rtac set_image_Lev,
wenzelm@51798
   576
                  atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
blanchet@48975
   577
                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
blanchet@48975
   578
                  if n = 1 then rtac refl else atac])
blanchet@53289
   579
              (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
blanchet@53289
   580
          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
traytel@55541
   581
            (set_Levss ~~ set_image_Levss))))),
blanchet@48975
   582
        (*root isNode*)
traytel@56114
   583
          rtac (isNode_def RS iffD2), rtac exI, rtac conjI,
blanchet@48975
   584
          CONVERSION (Conv.top_conv
blanchet@48975
   585
            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
blanchet@55414
   586
          if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
blanchet@53289
   587
          CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
blanchet@53289
   588
            EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
blanchet@48975
   589
              rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
blanchet@49305
   590
              rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
blanchet@48975
   591
              atac, rtac subsetI,
blanchet@48975
   592
              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
blanchet@49305
   593
              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
blanchet@48975
   594
              rtac @{thm singletonI}, dtac length_Lev',
blanchet@48975
   595
              etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
blanchet@48975
   596
                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
blanchet@48975
   597
              rtac rv_Nil])
blanchet@53289
   598
          (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
blanchet@48975
   599
traytel@55577
   600
    fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
traytel@55577
   601
      ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
blanchet@48975
   602
      EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
blanchet@48975
   603
        CONVERSION (Conv.top_conv
blanchet@48975
   604
          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
blanchet@48975
   605
        if n = 1 then K all_tac
blanchet@55393
   606
        else (rtac (sum_weak_case_cong RS trans) THEN'
blanchet@55414
   607
          rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
blanchet@51761
   608
        rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
blanchet@48975
   609
        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
traytel@49488
   610
          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
blanchet@48975
   611
            rtac trans, rtac @{thm Shift_def},
traytel@55541
   612
            rtac equalityI, rtac subsetI, etac thin_rl, 
blanchet@48975
   613
            REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
blanchet@48975
   614
            etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
blanchet@48975
   615
            rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
blanchet@48975
   616
            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
blanchet@48975
   617
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
traytel@49488
   618
                dtac list_inject_iffD1, etac conjE,
blanchet@48975
   619
                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
traytel@49488
   620
                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
wenzelm@51798
   621
                  atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
blanchet@48975
   622
                else etac (mk_InN_not_InM i' i'' RS notE)])
blanchet@48975
   623
            (rev ks),
blanchet@48975
   624
            rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
blanchet@49366
   625
            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
blanchet@48975
   626
            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
traytel@56114
   627
            rtac trans, rtac @{thm shift_def}, rtac iffD2, rtac @{thm fun_eq_iff}, rtac allI,
blanchet@48975
   628
            CONVERSION (Conv.top_conv
blanchet@48975
   629
              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
blanchet@48975
   630
            if n = 1 then K all_tac
blanchet@55414
   631
            else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
traytel@55577
   632
            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl])
blanchet@48975
   633
        ks to_sbd_injs from_to_sbds)];
blanchet@48975
   634
  in
blanchet@48975
   635
    (rtac mor_cong THEN'
wenzelm@55990
   636
    EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN'
traytel@56114
   637
    rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
blanchet@48975
   638
    CONJ_WRAP' fbetw_tac
traytel@55577
   639
      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
traytel@55577
   640
        (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN'
blanchet@48975
   641
    CONJ_WRAP' mor_tac
traytel@55577
   642
      (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~
traytel@55577
   643
        ((map_comp_ids ~~ map_cong0s) ~~
blanchet@48975
   644
          (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
blanchet@48975
   645
  end;
blanchet@48975
   646
blanchet@51761
   647
fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
blanchet@48975
   648
  EVERY' [rtac @{thm congruentI}, dtac lsbisE,
blanchet@48975
   649
    REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
blanchet@48975
   650
    etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
blanchet@51761
   651
    rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
blanchet@48975
   652
    EVERY' (map (fn equiv_LSBIS =>
blanchet@49305
   653
      EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
blanchet@48975
   654
    equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
blanchet@48975
   655
    etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
blanchet@48975
   656
blanchet@53289
   657
fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
traytel@56114
   658
  EVERY' [rtac (coalg_def RS iffD2),
blanchet@53289
   659
    CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
blanchet@48975
   660
      EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
blanchet@48975
   661
        rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
traytel@55541
   662
        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
blanchet@53289
   663
        CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
blanchet@53289
   664
          EVERY' [rtac (set_map0 RS ord_eq_le_trans),
traytel@56114
   665
            rtac @{thm image_subsetI}, rtac iffD2, rtac @{thm proj_in_iff},
blanchet@49305
   666
            rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
traytel@55541
   667
        (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
blanchet@53289
   668
    ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
blanchet@48975
   669
blanchet@48975
   670
fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
traytel@56114
   671
  EVERY' [rtac (mor_def RS iffD2), rtac conjI,
blanchet@48975
   672
    CONJ_WRAP' (fn equiv_LSBIS =>
traytel@56114
   673
      EVERY' [rtac ballI, rtac iffD2, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
blanchet@48975
   674
    equiv_LSBISs,
blanchet@48975
   675
    CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
blanchet@48975
   676
      EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
blanchet@48975
   677
        rtac congruent_str_final, atac, rtac o_apply])
blanchet@48975
   678
    (equiv_LSBISs ~~ congruent_str_finals)] 1;
blanchet@48975
   679
traytel@55541
   680
fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
blanchet@49504
   681
  unfold_thms_tac ctxt defs THEN
blanchet@48975
   682
  EVERY' [rtac conjI,
blanchet@48975
   683
    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
blanchet@51761
   684
    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
blanchet@51761
   685
      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
blanchet@48975
   686
        EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
blanchet@48975
   687
          EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
blanchet@49305
   688
            etac set_rev_mp, rtac coalg_final_set, rtac Rep])
traytel@55541
   689
        Abs_inverses coalg_final_sets)])
blanchet@51761
   690
    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
blanchet@48975
   691
traytel@55197
   692
fun mk_mor_Abs_tac ctxt defs Abs_inverses =
blanchet@49504
   693
  unfold_thms_tac ctxt defs THEN
blanchet@48975
   694
  EVERY' [rtac conjI,
blanchet@48975
   695
    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
blanchet@48975
   696
    CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
blanchet@48975
   697
blanchet@51761
   698
fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
traytel@49488
   699
  EVERY' [rtac iffD2, rtac mor_UNIV,
blanchet@51761
   700
    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
wenzelm@55990
   701
      EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
blanchet@49504
   702
        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
blanchet@48975
   703
        rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
blanchet@51761
   704
        rtac (o_apply RS trans RS sym), rtac map_cong0,
blanchet@48975
   705
        REPEAT_DETERM_N m o rtac refl,
blanchet@49504
   706
        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
blanchet@51761
   707
    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
blanchet@48975
   708
blanchet@48975
   709
fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
blanchet@48975
   710
  sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
blanchet@48975
   711
  let
blanchet@48975
   712
    val n = length Rep_injects;
blanchet@48975
   713
  in
traytel@49488
   714
    EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
blanchet@48975
   715
      REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
blanchet@48975
   716
      rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
blanchet@48975
   717
      rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
blanchet@48975
   718
      rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
blanchet@48975
   719
      rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,
blanchet@48975
   720
      rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls),
blanchet@48975
   721
      rtac impI,
blanchet@48975
   722
      CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
blanchet@48975
   723
        EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
blanchet@48975
   724
          rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
blanchet@49305
   725
          rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
blanchet@48975
   726
          rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
blanchet@48975
   727
          rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
blanchet@48975
   728
          rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
traytel@51447
   729
          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
blanchet@48975
   730
          rtac Rep_inject])
blanchet@48975
   731
      (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
blanchet@48975
   732
  end;
blanchet@48975
   733
blanchet@49504
   734
fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
blanchet@49504
   735
  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
wenzelm@55990
   736
    EVERY' [rtac @{thm ext}, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
blanchet@49504
   737
      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
blanchet@49504
   738
      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
blanchet@48975
   739
traytel@55197
   740
fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
wenzelm@55990
   741
  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
blanchet@51761
   742
    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
blanchet@48975
   743
    EVERY' (map (fn thm =>
blanchet@49585
   744
      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
blanchet@49585
   745
    rtac sym, rtac id_apply] 1;
blanchet@48975
   746
traytel@55197
   747
fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
blanchet@49504
   748
  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
blanchet@55642
   749
    rtac trans, rtac unfold, fo_rtac (@{thm sum.case(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
blanchet@48975
   750
    REPEAT_DETERM_N m o rtac refl,
blanchet@55414
   751
    EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
blanchet@48975
   752
traytel@55197
   753
fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
traytel@51739
   754
  unfold_thms_tac ctxt
blanchet@55414
   755
    (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN
traytel@51739
   756
  etac unfold_unique_mor 1;
traytel@51739
   757
traytel@51893
   758
fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
traytel@56114
   759
  EVERY' [rtac rev_mp, rtac raw_coind, rtac iffD2, rtac bis_rel, rtac conjI,
traytel@51893
   760
    CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
traytel@51893
   761
    rel_congs,
traytel@51893
   762
    CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
   763
      REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@55541
   764
      REPEAT_DETERM_N m o rtac refl,
traytel@51893
   765
      REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
traytel@51893
   766
      etac mp, etac CollectE, etac @{thm splitD}])
traytel@51893
   767
    rel_congs,
blanchet@48975
   768
    rtac impI, REPEAT_DETERM o etac conjE,
blanchet@49305
   769
    CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
blanchet@55414
   770
      rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
blanchet@48975
   771
traytel@55602
   772
fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
wenzelm@55990
   773
  EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
wenzelm@55990
   774
    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
wenzelm@55990
   775
    rtac map_cong0,
blanchet@55067
   776
    REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
blanchet@55067
   777
    REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
traytel@55602
   778
    rtac map_arg_cong, rtac (o_apply RS sym)] 1;
blanchet@48975
   779
traytel@56179
   780
fun mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss =
traytel@56179
   781
  EVERY' [rtac Jset_minimal,
blanchet@48975
   782
    REPEAT_DETERM_N n o rtac @{thm Un_upper1},
blanchet@48975
   783
    REPEAT_DETERM_N n o
traytel@56179
   784
      EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets =>
blanchet@49366
   785
        EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
traytel@56179
   786
          etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE,
traytel@56179
   787
          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)])
traytel@56179
   788
      (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
blanchet@48975
   789
traytel@56179
   790
fun mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets =
traytel@56179
   791
  EVERY' [rtac @{thm Un_least}, rtac set_incl_Jset,
blanchet@48975
   792
    REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
traytel@56179
   793
    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_Jset_incl_Jsets)] 1;
blanchet@48975
   794
blanchet@53270
   795
fun mk_map_id0_tac maps unfold_unique unfold_dtor =
traytel@52912
   796
  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
blanchet@49504
   797
    rtac unfold_dtor] 1;
blanchet@48975
   798
traytel@54841
   799
fun mk_map_comp0_tac maps map_comp0s map_unique =
traytel@54841
   800
  EVERY' [rtac map_unique,
traytel@54841
   801
    EVERY' (map2 (fn map_thm => fn map_comp0 =>
blanchet@48975
   802
      EVERY' (map rtac
blanchet@55067
   803
        [@{thm comp_assoc[symmetric]} RS trans,
blanchet@48975
   804
        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
blanchet@55067
   805
        @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans,
blanchet@55067
   806
        @{thm comp_assoc[symmetric]} RS trans,
traytel@54841
   807
        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
traytel@54841
   808
    maps map_comp0s)] 1;
blanchet@48975
   809
traytel@56179
   810
fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss
traytel@56179
   811
  set_Jset_Jsetsss in_rels =
blanchet@48975
   812
  let
blanchet@53288
   813
    val n = length map_comps;
blanchet@48975
   814
    val ks = 1 upto n;
blanchet@48975
   815
  in
traytel@55644
   816
    EVERY' ([rtac rev_mp, coinduct_tac] @
traytel@56179
   817
      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
traytel@56179
   818
        set_Jset_Jsetss), in_rel) =>
traytel@55644
   819
        [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
traytel@55644
   820
         REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
traytel@55644
   821
         rtac (Drule.rotate_prems 1 conjI),
blanchet@53288
   822
         rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
traytel@55644
   823
         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}),
blanchet@48975
   824
         REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
blanchet@53288
   825
         rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
traytel@56179
   826
         EVERY' (maps (fn set_Jset =>
traytel@55644
   827
           [rtac o_apply_trans_sym, rtac (@{thm snd_conv} RS trans), etac CollectE,
traytel@56179
   828
           REPEAT_DETERM o etac conjE, etac bspec, etac set_Jset]) set_Jsets),
blanchet@48975
   829
         REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
traytel@55644
   830
         rtac CollectI,
traytel@55644
   831
         EVERY' (map (fn set_map0 => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
traytel@55644
   832
           rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac refl])
traytel@55644
   833
        (take m set_map0s)),
traytel@56179
   834
         CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
traytel@55644
   835
           EVERY' [rtac ord_eq_le_trans, rtac set_map0,
traytel@55644
   836
             rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac exI, rtac conjI,
traytel@55644
   837
             rtac CollectI, etac CollectE,
blanchet@48975
   838
             REPEAT_DETERM o etac conjE,
traytel@56179
   839
             CONJ_WRAP' (fn set_Jset_Jset =>
traytel@56179
   840
               EVERY' [rtac ballI, etac bspec, etac set_Jset_Jset, atac]) set_Jset_Jsets,
traytel@55644
   841
             rtac (conjI OF [refl, refl])])
traytel@56179
   842
           (drop m set_map0s ~~ set_Jset_Jsetss)])
blanchet@53288
   843
        (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
traytel@56179
   844
          map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
blanchet@48975
   845
      [rtac impI,
blanchet@48975
   846
       CONJ_WRAP' (fn k =>
blanchet@48975
   847
         EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
blanchet@48975
   848
           rtac conjI, rtac refl, rtac refl]) ks]) 1
blanchet@48975
   849
  end
blanchet@48975
   850
traytel@55197
   851
fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
blanchet@49504
   852
  rtac unfold_unique 1 THEN
blanchet@55067
   853
  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
blanchet@48975
   854
  ALLGOALS (etac sym);
blanchet@48975
   855
traytel@55197
   856
fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
blanchet@48975
   857
  let
blanchet@49541
   858
    val n = length dtor_maps;
blanchet@48975
   859
  in
blanchet@49305
   860
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@49504
   861
      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
blanchet@48975
   862
      CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
blanchet@48975
   863
      REPEAT_DETERM o rtac allI,
blanchet@49541
   864
      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
blanchet@49504
   865
        [SELECT_GOAL (unfold_thms_tac ctxt
blanchet@49541
   866
          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
traytel@52659
   867
        rtac Un_cong, rtac refl,
traytel@52659
   868
        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
haftmann@56248
   869
          (fn i => EVERY' [rtac @{thm SUP_cong[OF refl]},
blanchet@48975
   870
            REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
blanchet@53289
   871
      (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
blanchet@48975
   872
  end;
blanchet@48975
   873
traytel@56113
   874
fun mk_set_map0_tac col_natural =
traytel@56113
   875
  EVERY' (map rtac [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans,
haftmann@56248
   876
    refl RS @{thm SUP_cong}, col_natural]) 1;
blanchet@48975
   877
blanchet@48975
   878
fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
blanchet@48975
   879
  let
blanchet@48975
   880
    val n = length rec_0s;
blanchet@48975
   881
  in
blanchet@49305
   882
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   883
      REPEAT_DETERM o rtac allI,
blanchet@49305
   884
      CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [ordIso_ordLeq_trans,
blanchet@48975
   885
        @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
blanchet@48975
   886
      REPEAT_DETERM o rtac allI,
blanchet@48975
   887
      CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
blanchet@49305
   888
        [rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
blanchet@48975
   889
        rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
blanchet@48975
   890
        REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
blanchet@48975
   891
        EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
blanchet@48975
   892
          rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE,
blanchet@48975
   893
          etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
blanchet@48975
   894
      (rec_Sucs ~~ set_sbdss)] 1
blanchet@48975
   895
  end;
blanchet@48975
   896
traytel@56113
   897
fun mk_set_bd_tac sbd_Cinfinite col_bd =
traytel@56113
   898
  EVERY' (map rtac [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
traytel@54793
   899
    @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1;
blanchet@48975
   900
traytel@54841
   901
fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs =
traytel@54841
   902
  EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn rel_OO =>
traytel@54841
   903
    let val Jrel_imp_rel = rel_Jrel RS iffD1;
traytel@54841
   904
    in
traytel@54841
   905
      EVERY' [rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), etac @{thm relcomppE},
traytel@54841
   906
      rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel]
traytel@54841
   907
    end)
traytel@54841
   908
  rel_Jrels rel_OOs) 1;
blanchet@48975
   909
traytel@55197
   910
fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
traytel@49104
   911
  ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
blanchet@48975
   912
  REPEAT_DETERM (atac 1 ORELSE
blanchet@49585
   913
    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
blanchet@49504
   914
    K (unfold_thms_tac ctxt dtor_ctors),
blanchet@48975
   915
    REPEAT_DETERM_N n o etac UnE,
blanchet@48975
   916
    REPEAT_DETERM o
blanchet@48975
   917
      (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
blanchet@48975
   918
        (eresolve_tac wit ORELSE'
blanchet@48975
   919
        (dresolve_tac wit THEN'
blanchet@48975
   920
          (etac FalseE ORELSE'
wenzelm@51798
   921
          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
blanchet@49504
   922
            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
blanchet@48975
   923
traytel@55197
   924
fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
wenzelm@51798
   925
  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
blanchet@49504
   926
  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
wenzelm@51798
   927
  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
traytel@49104
   928
  ALLGOALS (TRY o
traytel@49104
   929
    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
traytel@49104
   930
blanchet@53287
   931
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
blanchet@53289
   932
    dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
blanchet@48975
   933
  let
blanchet@49544
   934
    val m = length dtor_set_incls;
blanchet@49544
   935
    val n = length dtor_set_set_inclss;
blanchet@53289
   936
    val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
traytel@51893
   937
    val in_Jrel = nth in_Jrels (i - 1);
blanchet@48975
   938
    val if_tac =
traytel@51893
   939
      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
traytel@51893
   940
        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@53289
   941
        EVERY' (map2 (fn set_map0 => fn set_incl =>
blanchet@53289
   942
          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
blanchet@49305
   943
            rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
blanchet@48975
   944
            etac (set_incl RS @{thm subset_trans})])
blanchet@53289
   945
        passive_set_map0s dtor_set_incls),
blanchet@53289
   946
        CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
blanchet@53289
   947
          EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
blanchet@55414
   948
            rtac @{thm case_prodI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@49544
   949
            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
blanchet@48975
   950
            rtac conjI, rtac refl, rtac refl])
blanchet@53289
   951
        (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
blanchet@48975
   952
        CONJ_WRAP' (fn conv =>
blanchet@53287
   953
          EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
blanchet@55067
   954
          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
blanchet@48975
   955
          REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
blanchet@49541
   956
          rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
blanchet@48975
   957
        @{thms fst_conv snd_conv}];
blanchet@48975
   958
    val only_if_tac =
traytel@51893
   959
      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
traytel@51893
   960
        rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@53289
   961
        CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
blanchet@49585
   962
          EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
wenzelm@55990
   963
            rtac ord_eq_le_trans, rtac @{thm box_equals}, rtac passive_set_map0,
blanchet@49501
   964
            rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
blanchet@48975
   965
            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
blanchet@53289
   966
              (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
haftmann@56248
   967
                rtac @{thm SUP_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
blanchet@53289
   968
                rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
blanchet@49305
   969
                dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
traytel@51893
   970
                dtac @{thm ssubst_mem[OF pair_collapse]},
traytel@51893
   971
                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
blanchet@55414
   972
                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
traytel@51893
   973
                hyp_subst_tac ctxt,
traytel@51893
   974
                dtac (in_Jrel RS iffD1),
blanchet@48975
   975
                dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
traytel@51893
   976
                TRY o
traytel@51893
   977
                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
traytel@51893
   978
                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
blanchet@53289
   979
            (rev (active_set_map0s ~~ in_Jrels))])
blanchet@53289
   980
        (dtor_sets ~~ passive_set_map0s),
blanchet@48975
   981
        rtac conjI,
blanchet@49541
   982
        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
wenzelm@55990
   983
          rtac @{thm box_equals}, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
blanchet@55067
   984
          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
traytel@51893
   985
          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
traytel@51893
   986
            dtac @{thm ssubst_mem[OF pair_collapse]},
traytel@51893
   987
            REPEAT_DETERM o
blanchet@55414
   988
              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
traytel@51893
   989
            hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
traytel@51893
   990
            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
blanchet@48975
   991
          atac]]
blanchet@48975
   992
  in
blanchet@48975
   993
    EVERY' [rtac iffI, if_tac, only_if_tac] 1
blanchet@48975
   994
  end;
blanchet@48975
   995
traytel@55644
   996
fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
traytel@55644
   997
  dtor_unfolds dtor_maps in_rels =
traytel@55644
   998
  let
traytel@55644
   999
    val n = length ks;
traytel@55644
  1000
    val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd};
traytel@55644
  1001
    val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
traytel@51925
  1002
  in
traytel@55602
  1003
    EVERY' [rtac coinduct,
traytel@55644
  1004
      EVERY' (map8 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
traytel@55644
  1005
          fn dtor_unfold => fn dtor_map => fn in_rel =>
traytel@55644
  1006
        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
traytel@55644
  1007
          REPEAT_DETERM o eresolve_tac [exE, conjE],
traytel@51925
  1008
          select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1009
          REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
traytel@55644
  1010
          rtac exI, rtac (Drule.rotate_prems 1 conjI), rtac conjI,
blanchet@53287
  1011
          rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
blanchet@53287
  1012
          rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
traytel@55644
  1013
          REPEAT_DETERM_N m o rtac (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}),
traytel@51925
  1014
          REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
blanchet@53287
  1015
          rtac (map_comp0 RS trans), rtac (map_cong RS trans),
traytel@55644
  1016
          REPEAT_DETERM_N m o rtac (snd_diag_nth RS fun_cong),
traytel@51925
  1017
          REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
blanchet@55642
  1018
          etac (@{thm prod.case} RS map_arg_cong RS trans),
traytel@55644
  1019
          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}),
traytel@55644
  1020
          rtac CollectI,
blanchet@53289
  1021
          CONJ_WRAP' (fn set_map0 =>
traytel@55644
  1022
            EVERY' [rtac (set_map0 RS ord_eq_le_trans),
traytel@55644
  1023
              rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI},
traytel@55644
  1024
              FIRST' [rtac refl, EVERY'[rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
traytel@55644
  1025
                rtac (@{thm surjective_pairing} RS arg_cong)]]])
traytel@55644
  1026
          set_map0s])
traytel@55644
  1027
      ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1
traytel@51925
  1028
  end;
traytel@51925
  1029
blanchet@55642
  1030
val split_id_unfolds = @{thms prod.case image_id id_apply};
traytel@51925
  1031
traytel@55197
  1032
fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
traytel@51925
  1033
  let val n = length ks;
traytel@51925
  1034
  in
traytel@51925
  1035
    rtac set_induct 1 THEN
blanchet@53289
  1036
    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
traytel@51925
  1037
      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
traytel@51925
  1038
        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1039
        REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
traytel@51925
  1040
        hyp_subst_tac ctxt,
blanchet@53289
  1041
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
traytel@51925
  1042
        rtac subset_refl])
blanchet@53289
  1043
    unfolds set_map0ss ks) 1 THEN
blanchet@53289
  1044
    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
blanchet@53289
  1045
      EVERY' (map (fn set_map0 =>
traytel@51925
  1046
        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
traytel@51925
  1047
        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1048
        REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
blanchet@53289
  1049
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
traytel@51925
  1050
        etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
traytel@51925
  1051
        rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
blanchet@53289
  1052
      (drop m set_map0s)))
blanchet@53289
  1053
    unfolds set_map0ss ks) 1
traytel@51925
  1054
  end;
traytel@51925
  1055
traytel@55197
  1056
fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
traytel@51925
  1057
  let val n = length in_rels;
traytel@51925
  1058
  in
traytel@52506
  1059
    Method.insert_tac CIHs 1 THEN
traytel@51925
  1060
    unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
traytel@51925
  1061
    REPEAT_DETERM (etac exE 1) THEN
traytel@51925
  1062
    CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
traytel@51925
  1063
      EVERY' [rtac @{thm predicate2I}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI,
traytel@51925
  1064
        if null helper_inds then rtac UNIV_I
traytel@51925
  1065
        else rtac CollectI THEN'
traytel@51925
  1066
          CONJ_WRAP' (fn helper_ind =>
traytel@51925
  1067
            EVERY' [rtac (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
traytel@51925
  1068
              REPEAT_DETERM_N n o etac thin_rl, rtac impI,
traytel@51925
  1069
              REPEAT_DETERM o resolve_tac [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
traytel@51925
  1070
              dtac bspec, atac, REPEAT_DETERM o eresolve_tac [allE, mp, conjE],
traytel@51925
  1071
              etac (refl RSN (2, conjI))])
traytel@51925
  1072
          helper_inds,
traytel@51925
  1073
        rtac conjI,
traytel@51925
  1074
        rtac (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
traytel@51925
  1075
        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI)),
traytel@51925
  1076
        rtac (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
traytel@51925
  1077
        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI))])
traytel@51925
  1078
    (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
traytel@51925
  1079
  end;
traytel@51925
  1080
blanchet@55901
  1081
fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds =
traytel@52731
  1082
  let
traytel@52731
  1083
    val n = length map_transfers;
traytel@52731
  1084
  in
traytel@52731
  1085
    unfold_thms_tac ctxt
blanchet@55945
  1086
      @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
blanchet@55945
  1087
    unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
traytel@52731
  1088
    HEADGOAL (EVERY'
blanchet@55901
  1089
      [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
traytel@52731
  1090
      EVERY' (map (fn map_transfer => EVERY'
traytel@52731
  1091
        [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
traytel@52731
  1092
        SELECT_GOAL (unfold_thms_tac ctxt unfolds),
blanchet@55945
  1093
        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
traytel@52731
  1094
        REPEAT_DETERM_N m o rtac @{thm id_transfer},
blanchet@55945
  1095
        REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
traytel@52731
  1096
        etac @{thm predicate2D}, etac @{thm image2pI}])
traytel@52731
  1097
      map_transfers)])
traytel@52731
  1098
  end;
traytel@52731
  1099
blanchet@48975
  1100
end;