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