src/HOL/BNF/Tools/bnf_gfp_tactics.ML
author blanchet
Fri Jun 07 09:30:13 2013 +0200 (2013-06-07)
changeset 52334 705bc4f5fc70
parent 51925 e3b7917186f1
child 52506 eb80a16a2b72
permissions -rw-r--r--
tuning
blanchet@49509
     1
(*  Title:      HOL/BNF/Tools/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
wenzelm@51798
    12
  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
wenzelm@51798
    13
    thm list list -> tactic
blanchet@48975
    14
  val mk_bd_card_order_tac: thm -> tactic
blanchet@48975
    15
  val mk_bd_cinfinite_tac: thm -> tactic
blanchet@48975
    16
  val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
blanchet@48975
    17
    {prems: 'a, context: Proof.context} -> tactic
wenzelm@51798
    18
  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
blanchet@48975
    19
  val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    20
  val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
traytel@51893
    21
  val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
wenzelm@51798
    22
    thm list list -> tactic
blanchet@48975
    23
  val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
blanchet@48975
    24
    {prems: 'a, context: Proof.context} -> tactic
wenzelm@51798
    25
  val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
wenzelm@51798
    26
    thm list -> tactic
blanchet@48975
    27
  val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
blanchet@48975
    28
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    29
  val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
blanchet@48975
    30
    tactic
blanchet@48975
    31
  val mk_coalg_set_tac: thm -> tactic
blanchet@48975
    32
  val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->
blanchet@48975
    33
    {prems: 'a, context: Proof.context} -> tactic
traytel@49104
    34
  val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
traytel@49104
    35
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    36
  val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
blanchet@48975
    37
    thm list list -> tactic
blanchet@48975
    38
  val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
blanchet@48975
    39
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    40
  val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
blanchet@48975
    41
  val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
blanchet@48975
    42
    {prems: 'a, context: Proof.context} -> tactic
traytel@51739
    43
  val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
traytel@51739
    44
    tactic
blanchet@49581
    45
  val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
blanchet@49581
    46
  val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
blanchet@49581
    47
    thm -> thm -> tactic
blanchet@49585
    48
  val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
traytel@51893
    49
  val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
traytel@51893
    50
  val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
wenzelm@51798
    51
    cterm option list -> thm -> thm list -> thm list -> tactic
traytel@51893
    52
  val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
wenzelm@51798
    53
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
blanchet@49501
    54
  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
blanchet@49501
    55
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    56
  val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
blanchet@48975
    57
  val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    58
  val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
blanchet@48975
    59
    {prems: 'a, context: Proof.context} -> tactic
wenzelm@51798
    60
  val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
wenzelm@51798
    61
    thm -> thm -> thm -> thm -> thm -> thm -> tactic
blanchet@48975
    62
  val mk_incl_lsbis_tac: int -> int -> thm -> tactic
blanchet@48975
    63
  val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    64
  val mk_length_Lev'_tac: thm -> tactic
wenzelm@51798
    65
  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
blanchet@48975
    66
  val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
wenzelm@51798
    67
  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
wenzelm@51798
    68
    thm list list -> thm list list -> thm list list list -> tactic
blanchet@48975
    69
  val mk_map_id_tac: thm list -> thm -> thm -> tactic
blanchet@48975
    70
  val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
blanchet@49543
    71
  val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    72
  val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    73
  val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
blanchet@48975
    74
    thm list -> {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    75
  val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
blanchet@48975
    76
  val mk_mor_UNIV_tac: thm list -> thm -> tactic
blanchet@48975
    77
  val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
blanchet@48975
    78
    thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
blanchet@48975
    79
    thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
blanchet@48975
    80
    thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
blanchet@48975
    81
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
    82
  val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
blanchet@48975
    83
  val mk_mor_elim_tac: thm -> tactic
blanchet@48975
    84
  val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
blanchet@48975
    85
    thm list -> thm list list -> thm list list -> tactic
blanchet@48975
    86
  val mk_mor_hset_tac: thm -> thm -> tactic
blanchet@48975
    87
  val mk_mor_incl_tac: thm -> thm list -> tactic
blanchet@48975
    88
  val mk_mor_str_tac: 'a list -> thm -> tactic
blanchet@48975
    89
  val mk_mor_sum_case_tac: 'a list -> thm -> tactic
blanchet@48975
    90
  val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
blanchet@48975
    91
    {prems: thm list, context: Proof.context} -> tactic
blanchet@48975
    92
  val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
blanchet@48975
    93
    {prems: thm list, context: Proof.context} -> tactic
blanchet@48975
    94
  val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
blanchet@48975
    95
    {prems: 'a, context: Proof.context} -> tactic
blanchet@49504
    96
  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
blanchet@49504
    97
    thm list -> tactic
wenzelm@51798
    98
  val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
blanchet@48975
    99
  val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
blanchet@48975
   100
  val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
blanchet@48975
   101
    thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
blanchet@48975
   102
    tactic
blanchet@48975
   103
  val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
blanchet@48975
   104
    thm list -> thm list -> thm -> thm list -> tactic
traytel@51925
   105
  val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
traytel@51925
   106
    {prems: 'a, context: Proof.context} -> tactic
traytel@51925
   107
  val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
traytel@51925
   108
    thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
traytel@51925
   109
  val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
traytel@51925
   110
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
   111
  val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
wenzelm@51798
   112
  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
wenzelm@51798
   113
  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
wenzelm@51798
   114
    thm list -> thm list list -> tactic
blanchet@48975
   115
  val mk_set_bd_tac: thm -> thm -> thm -> tactic
blanchet@48975
   116
  val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
wenzelm@51798
   117
  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
wenzelm@51798
   118
    thm list -> thm list -> thm list list -> thm list list -> tactic
blanchet@48975
   119
  val mk_set_incl_hin_tac: thm list -> tactic
blanchet@48975
   120
  val mk_set_incl_hset_tac: thm -> thm -> tactic
blanchet@48975
   121
  val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
blanchet@51766
   122
  val mk_set_map_tac: thm -> thm -> tactic
wenzelm@51798
   123
  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
wenzelm@51798
   124
    thm list -> thm list -> thm list list -> thm list list -> tactic
wenzelm@51798
   125
  val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
wenzelm@51798
   126
    ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
wenzelm@51798
   127
    thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
blanchet@49504
   128
  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
blanchet@48975
   129
  val mk_unique_mor_tac: thm list -> thm -> tactic
traytel@49104
   130
  val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
blanchet@48975
   131
    {prems: 'a, context: Proof.context} -> tactic
blanchet@48975
   132
  val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic
blanchet@48975
   133
end;
blanchet@48975
   134
blanchet@48975
   135
structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
blanchet@48975
   136
struct
blanchet@48975
   137
blanchet@48975
   138
open BNF_Tactics
blanchet@48975
   139
open BNF_Util
blanchet@51850
   140
open BNF_FP_Util
blanchet@48975
   141
open BNF_GFP_Util
blanchet@48975
   142
blanchet@49305
   143
val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
traytel@49488
   144
val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
blanchet@49305
   145
val nat_induct = @{thm nat_induct};
blanchet@49305
   146
val o_apply_trans_sym = o_apply RS trans RS sym;
blanchet@49305
   147
val ord_eq_le_trans = @{thm ord_eq_le_trans};
blanchet@49305
   148
val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
blanchet@49305
   149
  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
blanchet@49305
   150
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
blanchet@49305
   151
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
blanchet@49328
   152
val sum_case_weak_cong = @{thm sum_case_weak_cong};
blanchet@49305
   153
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
traytel@51925
   154
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}
blanchet@49305
   155
blanchet@48975
   156
fun mk_coalg_set_tac coalg_def =
traytel@49488
   157
  dtac (coalg_def RS iffD1) 1 THEN
blanchet@48975
   158
  REPEAT_DETERM (etac conjE 1) THEN
blanchet@48975
   159
  EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
blanchet@48975
   160
  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
blanchet@48975
   161
blanchet@48975
   162
fun mk_mor_elim_tac mor_def =
blanchet@48975
   163
  (dtac (subst OF [mor_def]) THEN'
blanchet@48975
   164
  REPEAT o etac conjE THEN'
blanchet@48975
   165
  TRY o rtac @{thm image_subsetI} THEN'
blanchet@48975
   166
  etac bspec THEN'
blanchet@48975
   167
  atac) 1;
blanchet@48975
   168
blanchet@48975
   169
fun mk_mor_incl_tac mor_def map_id's =
blanchet@48975
   170
  (stac mor_def THEN'
blanchet@48975
   171
  rtac conjI THEN'
blanchet@49585
   172
  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
blanchet@48975
   173
  CONJ_WRAP' (fn thm =>
blanchet@49585
   174
   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
blanchet@48975
   175
blanchet@48975
   176
fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
blanchet@48975
   177
  let
blanchet@48975
   178
    fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
blanchet@48975
   179
    fun mor_tac ((mor_image, morE), map_comp_id) =
blanchet@48975
   180
      EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
blanchet@48975
   181
        etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
blanchet@48975
   182
  in
blanchet@48975
   183
    (stac mor_def THEN' rtac conjI THEN'
blanchet@48975
   184
    CONJ_WRAP' fbetw_tac mor_images THEN'
blanchet@48975
   185
    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
blanchet@48975
   186
  end;
blanchet@48975
   187
blanchet@48975
   188
fun mk_mor_UNIV_tac morEs mor_def =
blanchet@48975
   189
  let
blanchet@48975
   190
    val n = length morEs;
blanchet@48975
   191
    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
blanchet@48975
   192
      rtac UNIV_I, rtac sym, rtac o_apply];
blanchet@48975
   193
  in
blanchet@48975
   194
    EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
blanchet@48975
   195
    stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
blanchet@48975
   196
    CONJ_WRAP' (fn i =>
blanchet@48975
   197
      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1
blanchet@48975
   198
  end;
blanchet@48975
   199
blanchet@48975
   200
fun mk_mor_str_tac ks mor_UNIV =
blanchet@48975
   201
  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
blanchet@48975
   202
blanchet@48975
   203
fun mk_mor_sum_case_tac ks mor_UNIV =
blanchet@48975
   204
  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1;
blanchet@48975
   205
blanchet@48975
   206
fun mk_set_incl_hset_tac def rec_Suc =
blanchet@48975
   207
  EVERY' (stac def ::
blanchet@48975
   208
    map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
blanchet@48975
   209
      sym, rec_Suc]) 1;
blanchet@48975
   210
blanchet@48975
   211
fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
blanchet@48975
   212
  EVERY' (map (TRY oo stac) defs @
blanchet@49305
   213
    map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
blanchet@49366
   214
      mk_UnIN n i] @
blanchet@48975
   215
    [etac @{thm UN_I}, atac]) 1;
blanchet@48975
   216
blanchet@48975
   217
fun mk_set_incl_hin_tac incls =
traytel@49490
   218
  if null incls then rtac subset_UNIV 1
blanchet@48975
   219
  else EVERY' [rtac subsetI, rtac CollectI,
blanchet@48975
   220
    CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
blanchet@48975
   221
blanchet@48975
   222
fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
blanchet@49305
   223
  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   224
    REPEAT_DETERM o rtac allI,
blanchet@48975
   225
    CONJ_WRAP' (fn thm => EVERY'
blanchet@49305
   226
      [rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
blanchet@48975
   227
    REPEAT_DETERM o rtac allI,
blanchet@48975
   228
    CONJ_WRAP' (fn rec_Suc => EVERY'
blanchet@49305
   229
      [rtac ord_eq_le_trans, rtac rec_Suc,
blanchet@48975
   230
        if m = 0 then K all_tac
blanchet@48975
   231
        else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
blanchet@48975
   232
        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
blanchet@48975
   233
          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
blanchet@48975
   234
            rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
blanchet@48975
   235
      rec_Sucs] 1;
blanchet@48975
   236
blanchet@48975
   237
fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
blanchet@49305
   238
  (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
blanchet@48975
   239
    rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
blanchet@48975
   240
    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
blanchet@48975
   241
    REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
blanchet@48975
   242
blanchet@51766
   243
fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss =
blanchet@49305
   244
  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   245
    REPEAT_DETERM o rtac allI,
blanchet@48975
   246
    CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
blanchet@48975
   247
    REPEAT_DETERM o rtac allI,
blanchet@48975
   248
    CONJ_WRAP'
blanchet@51766
   249
      (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
blanchet@48975
   250
        EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
blanchet@48975
   251
          if m = 0 then K all_tac
blanchet@48975
   252
          else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
blanchet@51766
   253
            rtac (nth passive_set_maps (j - 1) RS sym),
blanchet@49305
   254
            rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
blanchet@48975
   255
          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
blanchet@51766
   256
            (fn (i, (set_map, coalg_set)) =>
blanchet@48975
   257
              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
blanchet@51766
   258
                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
blanchet@48975
   259
                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
blanchet@49305
   260
                ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
blanchet@48975
   261
                REPEAT_DETERM o etac allE, atac, atac])
blanchet@51766
   262
            (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
blanchet@51766
   263
      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
blanchet@48975
   264
blanchet@48975
   265
fun mk_mor_hset_tac hset_def mor_hset_rec =
blanchet@48975
   266
  EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
blanchet@48975
   267
    atac, atac, rtac (hset_def RS sym)] 1
blanchet@48975
   268
traytel@51893
   269
fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
blanchet@48975
   270
  let
traytel@51893
   271
    val n = length rel_OO_Grps;
traytel@51893
   272
    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
blanchet@48975
   273
traytel@51893
   274
    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
blanchet@48975
   275
      EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
blanchet@48975
   276
        etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
traytel@51893
   277
        rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@51893
   278
        rtac @{thm relcomppI}, rtac @{thm conversepI},
blanchet@48975
   279
        EVERY' (map (fn thm =>
traytel@51893
   280
          EVERY' [rtac @{thm GrpI},
traytel@51893
   281
            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
traytel@51893
   282
            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
traytel@51893
   283
            REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
blanchet@48975
   284
            CONJ_WRAP' (fn (i, thm) =>
blanchet@48975
   285
              if i <= m
blanchet@49305
   286
              then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
traytel@51893
   287
                etac @{thm image_mono}, rtac @{thm image_subsetI},
traytel@51893
   288
                etac @{thm Collect_split_in_relI[OF Id_onI]}]
blanchet@49305
   289
              else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
traytel@51893
   290
                rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
traytel@51893
   291
            (1 upto (m + n) ~~ set_maps)])
blanchet@48975
   292
          @{thms fst_diag_id snd_diag_id})];
blanchet@48975
   293
traytel@51893
   294
    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
blanchet@48975
   295
      EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
blanchet@48975
   296
        etac allE, etac allE, etac impE, atac,
traytel@51893
   297
        dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@51893
   298
        REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
traytel@51893
   299
          @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
wenzelm@51798
   300
        hyp_subst_tac ctxt,
blanchet@51761
   301
        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
traytel@49684
   302
        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
traytel@49684
   303
        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
traytel@51893
   304
        atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
traytel@49684
   305
        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
traytel@49684
   306
        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
blanchet@51761
   307
        rtac trans, rtac map_cong0,
traytel@51447
   308
        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
blanchet@48975
   309
        REPEAT_DETERM_N n o rtac refl,
traytel@51893
   310
        atac, rtac CollectI,
blanchet@48975
   311
        CONJ_WRAP' (fn (i, thm) =>
blanchet@48975
   312
          if i <= m
blanchet@49305
   313
          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
traytel@51447
   314
            rtac @{thm Id_on_fst}, etac set_mp, atac]
blanchet@49305
   315
          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
blanchet@49305
   316
            rtac trans_fun_cong_image_id_id_apply, atac])
blanchet@51766
   317
        (1 upto (m + n) ~~ set_maps)];
blanchet@48975
   318
  in
blanchet@48975
   319
    EVERY' [rtac (bis_def RS trans),
blanchet@48975
   320
      rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
blanchet@48975
   321
      etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
blanchet@48975
   322
  end;
blanchet@48975
   323
traytel@51893
   324
fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
traytel@51893
   325
  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
blanchet@48975
   326
    REPEAT_DETERM o etac conjE, rtac conjI,
blanchet@48975
   327
    CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
traytel@51893
   328
      rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
traytel@51893
   329
    CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
traytel@51893
   330
      EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
   331
        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@51893
   332
        REPEAT_DETERM_N m o rtac @{thm conversep_in_rel_Id_on},
traytel@51893
   333
        REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
traytel@51893
   334
        rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
blanchet@48975
   335
        REPEAT_DETERM o etac allE,
traytel@51893
   336
        rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
blanchet@48975
   337
traytel@51893
   338
fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
traytel@51893
   339
  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
blanchet@48975
   340
    REPEAT_DETERM o etac conjE, rtac conjI,
traytel@51893
   341
    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
traytel@51893
   342
    CONJ_WRAP' (fn (rel_cong, rel_OO) =>
traytel@51893
   343
      EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
   344
        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@51893
   345
        REPEAT_DETERM_N m o rtac @{thm relcompp_in_rel_Id_on},
traytel@51893
   346
        REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
traytel@51893
   347
        rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
blanchet@48975
   348
        etac @{thm relcompE},
traytel@49488
   349
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
   350
        etac conjE, hyp_subst_tac ctxt,
traytel@51893
   351
        REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
traytel@51893
   352
        etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
blanchet@48975
   353
traytel@51893
   354
fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
blanchet@48975
   355
  {context = ctxt, prems = _} =
traytel@51893
   356
  unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
blanchet@48975
   357
  EVERY' [rtac conjI,
blanchet@48975
   358
    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
blanchet@48975
   359
    CONJ_WRAP' (fn (coalg_in, morE) =>
traytel@51893
   360
      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
traytel@51893
   361
        etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
traytel@51893
   362
    (coalg_ins ~~ morEs)] 1;
blanchet@48975
   363
blanchet@48975
   364
fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
blanchet@48975
   365
  let
blanchet@48975
   366
    val n = length in_monos;
blanchet@48975
   367
    val ks = 1 upto n;
blanchet@48975
   368
  in
blanchet@49504
   369
    unfold_thms_tac ctxt [bis_def] THEN
blanchet@48975
   370
    EVERY' [rtac conjI,
blanchet@48975
   371
      CONJ_WRAP' (fn i =>
blanchet@48975
   372
        EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
blanchet@48975
   373
          dtac conjunct1, etac (mk_conjunctN n i)]) ks,
blanchet@48975
   374
      CONJ_WRAP' (fn (i, in_mono) =>
blanchet@48975
   375
        EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
blanchet@48975
   376
          dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
blanchet@48975
   377
          atac, etac bexE, rtac bexI, atac, rtac in_mono,
blanchet@48975
   378
          REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},
blanchet@48975
   379
          atac]) (ks ~~ in_monos)] 1
blanchet@48975
   380
  end;
blanchet@48975
   381
wenzelm@51798
   382
fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
blanchet@48975
   383
  let
blanchet@48975
   384
    val n = length lsbis_defs;
blanchet@48975
   385
  in
blanchet@48975
   386
    EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
blanchet@48975
   387
      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
wenzelm@51798
   388
      hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
blanchet@48975
   389
  end;
blanchet@48975
   390
blanchet@48975
   391
fun mk_incl_lsbis_tac n i lsbis_def =
blanchet@48975
   392
  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
blanchet@48975
   393
    REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
blanchet@48975
   394
    rtac (mk_nth_conv n i)] 1;
blanchet@48975
   395
traytel@51447
   396
fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
traytel@49488
   397
  EVERY' [rtac (@{thm equiv_def} RS iffD2),
blanchet@48975
   398
traytel@49488
   399
    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
blanchet@49305
   400
    rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
traytel@51447
   401
    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
blanchet@48975
   402
traytel@49488
   403
    rtac conjI, rtac (@{thm sym_def} RS iffD2),
blanchet@49305
   404
    rtac allI, rtac allI, rtac impI, rtac set_mp,
blanchet@48975
   405
    rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
blanchet@48975
   406
traytel@49488
   407
    rtac (@{thm trans_def} RS iffD2),
blanchet@49305
   408
    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
blanchet@48975
   409
    rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
blanchet@48975
   410
    etac @{thm relcompI}, atac] 1;
blanchet@48975
   411
blanchet@51766
   412
fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} =
blanchet@48975
   413
  let
blanchet@48975
   414
    val n = length strT_defs;
blanchet@48975
   415
    val ks = 1 upto n;
blanchet@48975
   416
    fun coalg_tac (i, ((passive_sets, active_sets), def)) =
blanchet@48975
   417
      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
wenzelm@51798
   418
        hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
blanchet@48975
   419
        rtac (mk_sum_casesN n i), rtac CollectI,
blanchet@49305
   420
        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
blanchet@49585
   421
          etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
blanchet@49305
   422
          passive_sets),
blanchet@49305
   423
        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
blanchet@48975
   424
          rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
blanchet@48975
   425
          rtac conjI,
blanchet@49305
   426
          rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
blanchet@48975
   427
            etac equalityD1, etac CollectD,
blanchet@48975
   428
          rtac conjI, etac @{thm Shift_clists},
blanchet@48975
   429
          rtac conjI, etac @{thm Shift_prefCl},
blanchet@48975
   430
          rtac conjI, rtac ballI,
blanchet@48975
   431
            rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
blanchet@49504
   432
            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
blanchet@48975
   433
            etac bspec, etac @{thm ShiftD},
blanchet@48975
   434
            CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
blanchet@48975
   435
              dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
blanchet@48975
   436
              dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
blanchet@48975
   437
              REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
blanchet@48975
   438
              rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
blanchet@48975
   439
              rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
blanchet@48975
   440
              REPEAT_DETERM_N m o (rtac conjI THEN' atac),
blanchet@48975
   441
              CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
blanchet@48975
   442
                rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
blanchet@48975
   443
                rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
blanchet@48975
   444
          rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],
blanchet@48975
   445
          etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,
blanchet@48975
   446
          dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,
blanchet@48975
   447
          etac @{thm set_mp[OF equalityD1]}, atac,
blanchet@48975
   448
          REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
blanchet@48975
   449
          rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
blanchet@48975
   450
          etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
blanchet@48975
   451
          REPEAT_DETERM_N m o (rtac conjI THEN' atac),
blanchet@48975
   452
          CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
blanchet@48975
   453
            rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
blanchet@48975
   454
            rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
blanchet@48975
   455
  in
blanchet@49504
   456
    unfold_thms_tac ctxt defs THEN
blanchet@51766
   457
    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
blanchet@48975
   458
  end;
blanchet@48975
   459
wenzelm@51798
   460
fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
blanchet@48975
   461
  sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
blanchet@48975
   462
  let
blanchet@48975
   463
    val n = length isNode_defs;
blanchet@48975
   464
  in
blanchet@48975
   465
    EVERY' [rtac (Thm.permute_prems 0 1 ctrans),
blanchet@48975
   466
      rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp},
blanchet@48975
   467
      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
blanchet@48975
   468
      rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},
blanchet@48975
   469
      rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,
blanchet@48975
   470
      rtac ctrans, rtac @{thm card_of_diff},
blanchet@49305
   471
      rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},
blanchet@49305
   472
      rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,
traytel@51782
   473
      rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1},
blanchet@48975
   474
      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
traytel@51782
   475
      rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_clists},
blanchet@49305
   476
      rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,
blanchet@48975
   477
      rtac @{thm clists_Cinfinite},
blanchet@48975
   478
      if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
blanchet@49305
   479
      rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
blanchet@48975
   480
      rtac sbd_Cinfinite,
traytel@51782
   481
      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
blanchet@48975
   482
      rtac @{thm Cnotzero_clists},
blanchet@49305
   483
      rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc},
blanchet@49305
   484
      rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},
blanchet@48975
   485
      rtac ctrans, rtac @{thm cexp_mono},
blanchet@48975
   486
      rtac @{thm ordLeq_ordIso_trans},
blanchet@48975
   487
      CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1
blanchet@48975
   488
          (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}
blanchet@48975
   489
        RSN (3, @{thm Un_Cinfinite_bound}))))
blanchet@48975
   490
        (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),
traytel@51782
   491
      rtac @{thm cexp_cong1}, rtac @{thm csum_cong1},
blanchet@48975
   492
      REPEAT_DETERM_N m o rtac @{thm csum_cong2},
blanchet@48975
   493
      CONJ_WRAP_GEN' (rtac @{thm csum_cong})
blanchet@48975
   494
        (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,
blanchet@48975
   495
      rtac sbd_Card_order,
blanchet@48975
   496
      rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},
blanchet@48975
   497
      rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,
traytel@51782
   498
      rtac FalseE, etac @{thm cpow_clists_czero}, atac,
blanchet@48975
   499
      rtac @{thm card_of_Card_order},
blanchet@49305
   500
      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},
traytel@51782
   501
      rtac @{thm Card_order_csum},
traytel@51782
   502
      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2},
blanchet@48975
   503
      rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
blanchet@48975
   504
      rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
traytel@51782
   505
      rtac @{thm Card_order_csum}, rtac @{thm Card_order_cprod},
traytel@51782
   506
      rtac ctrans, rtac @{thm cexp_mono1},
blanchet@49305
   507
      rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
blanchet@48975
   508
      rtac @{thm ordIso_transitive},
blanchet@48975
   509
      REPEAT_DETERM_N m o rtac @{thm csum_cong2},
blanchet@48975
   510
      rtac sbd_sbd,
blanchet@48975
   511
      BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
blanchet@48975
   512
        FIRST' [rtac @{thm card_of_Card_order},
blanchet@48975
   513
          rtac @{thm Card_order_csum}, rtac sbd_Card_order])
blanchet@48975
   514
        @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
blanchet@48975
   515
        (1 upto m + 1) (m + 1 :: (1 upto m)),
blanchet@48975
   516
      if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}],
blanchet@48975
   517
      rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,
blanchet@48975
   518
      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
blanchet@48975
   519
      if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
traytel@51782
   520
      rtac @{thm Card_order_ctwo}, rtac sbd_Card_order,
blanchet@49305
   521
      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},
traytel@51782
   522
      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
blanchet@48975
   523
      rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
blanchet@48975
   524
      rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
blanchet@48975
   525
      rtac sbd_Cinfinite,
traytel@51782
   526
      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
blanchet@48975
   527
      rtac sbd_Cnotzero,
blanchet@48975
   528
      rtac @{thm card_of_mono1}, rtac subsetI,
wenzelm@51798
   529
      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
blanchet@49305
   530
      rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
blanchet@48975
   531
      rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
blanchet@48975
   532
      rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
wenzelm@51798
   533
      hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
blanchet@48975
   534
      rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
blanchet@48975
   535
      CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
traytel@49488
   536
        [rtac (mk_UnIN n i), dtac (def RS iffD1),
blanchet@48975
   537
        REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
blanchet@48975
   538
        REPEAT_DETERM_N m o (rtac conjI THEN' atac),
blanchet@49305
   539
        CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
traytel@49490
   540
          rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},
blanchet@48975
   541
          rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
blanchet@48975
   542
      atac] 1
blanchet@48975
   543
  end;
blanchet@48975
   544
blanchet@51766
   545
fun mk_carT_set_tac n i carT_def strT_def isNode_def set_map {context = ctxt, prems = _}=
blanchet@49305
   546
  EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
blanchet@48975
   547
    REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
traytel@49488
   548
    dtac Pair_eqD,
wenzelm@51798
   549
    etac conjE, hyp_subst_tac ctxt,
traytel@49488
   550
    dtac (isNode_def RS iffD1),
blanchet@48975
   551
    REPEAT_DETERM o eresolve_tac [exE, conjE],
blanchet@49305
   552
    rtac (equalityD2 RS set_mp),
blanchet@48975
   553
    rtac (strT_def RS arg_cong RS trans),
blanchet@48975
   554
    etac (arg_cong RS trans),
blanchet@48975
   555
    fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
blanchet@51766
   556
    rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
blanchet@48975
   557
    etac @{thm prefCl_Succ}, atac] 1;
blanchet@48975
   558
wenzelm@51798
   559
fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
blanchet@51766
   560
  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
blanchet@48975
   561
  let
blanchet@51766
   562
    val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
blanchet@48975
   563
    val ks = 1 upto n;
blanchet@51766
   564
    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_map)))) =
blanchet@48975
   565
      CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
blanchet@48975
   566
        (if i = i'
blanchet@48975
   567
        then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
blanchet@48975
   568
          rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
blanchet@51766
   569
          rtac (Thm.permute_prems 0 1 (set_map RS box_equals)),
blanchet@49585
   570
          rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
blanchet@48975
   571
          rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
blanchet@49305
   572
        else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
blanchet@48975
   573
          REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
traytel@49488
   574
          dtac conjunct2, dtac Pair_eqD, etac conjE,
wenzelm@51798
   575
          hyp_subst_tac ctxt, dtac (isNode_def RS iffD1),
blanchet@48975
   576
          REPEAT_DETERM o eresolve_tac [exE, conjE],
blanchet@48975
   577
          rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
blanchet@48975
   578
      (ks ~~ (carT_defs ~~ isNode_defs));
blanchet@48975
   579
    fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =
blanchet@48975
   580
      dtac (mk_conjunctN n i) THEN'
blanchet@48975
   581
      CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>
blanchet@48975
   582
        EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,
blanchet@49305
   583
          rtac (coalgT RS coalg_set RS set_mp), atac, etac carT_set, atac, atac,
blanchet@48975
   584
          etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,
blanchet@48975
   585
          rtac set_hset_incl_hset, etac carT_set, atac, atac])
blanchet@48975
   586
      (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));
blanchet@48975
   587
  in
blanchet@48975
   588
    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
blanchet@48975
   589
      REPEAT_DETERM o rtac allI, rtac impI,
blanchet@48975
   590
      CONJ_WRAP' base_tac
blanchet@51766
   591
        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_maps)))),
blanchet@48975
   592
      REPEAT_DETERM o rtac allI, rtac impI,
blanchet@48975
   593
      REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
blanchet@48975
   594
      CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
blanchet@48975
   595
        CONJ_WRAP_GEN' (K all_tac) step_tac
blanchet@48975
   596
          (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1
blanchet@48975
   597
  end;
blanchet@48975
   598
blanchet@48975
   599
fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} =
blanchet@48975
   600
  let
blanchet@48975
   601
    val m = length strT_hsets;
blanchet@48975
   602
  in
blanchet@48975
   603
    if m = 0 then atac 1
blanchet@49504
   604
    else (unfold_thms_tac ctxt [isNode_def] THEN
blanchet@48975
   605
      EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
blanchet@48975
   606
        rtac exI, rtac conjI, atac,
blanchet@48975
   607
        CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
blanchet@48975
   608
          else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac])
blanchet@48975
   609
        (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
blanchet@48975
   610
  end;
blanchet@48975
   611
wenzelm@51798
   612
fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
blanchet@48975
   613
  let
blanchet@48975
   614
    val n = length Lev_0s;
blanchet@48975
   615
    val ks = 1 upto n;
blanchet@48975
   616
  in
blanchet@49305
   617
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   618
      REPEAT_DETERM o rtac allI,
blanchet@48975
   619
      CONJ_WRAP' (fn Lev_0 =>
blanchet@49305
   620
        EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,
blanchet@48975
   621
      REPEAT_DETERM o rtac allI,
blanchet@48975
   622
      CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
blanchet@49305
   623
        EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
blanchet@48975
   624
          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
blanchet@48975
   625
            (fn (i, to_sbd) => EVERY' [rtac subsetI,
wenzelm@51798
   626
              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@48975
   627
              rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
blanchet@49305
   628
              etac set_rev_mp, REPEAT_DETERM o etac allE,
blanchet@48975
   629
              etac (mk_conjunctN n i)])
blanchet@48975
   630
          (rev (ks ~~ to_sbds))])
blanchet@48975
   631
      (Lev_Sucs ~~ to_sbdss)] 1
blanchet@48975
   632
  end;
blanchet@48975
   633
wenzelm@51798
   634
fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
blanchet@48975
   635
  let
blanchet@48975
   636
    val n = length Lev_0s;
blanchet@48975
   637
    val ks = n downto 1;
blanchet@48975
   638
  in
blanchet@49305
   639
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   640
      REPEAT_DETERM o rtac allI,
blanchet@48975
   641
      CONJ_WRAP' (fn Lev_0 =>
blanchet@49305
   642
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
blanchet@48975
   643
          etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
blanchet@48975
   644
      REPEAT_DETERM o rtac allI,
blanchet@48975
   645
      CONJ_WRAP' (fn Lev_Suc =>
blanchet@49305
   646
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   647
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
wenzelm@51798
   648
            (fn i =>
wenzelm@51798
   649
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
wenzelm@51798
   650
                rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
wenzelm@51798
   651
                REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
blanchet@48975
   652
      Lev_Sucs] 1
blanchet@48975
   653
  end;
blanchet@48975
   654
blanchet@48975
   655
fun mk_length_Lev'_tac length_Lev =
blanchet@48975
   656
  EVERY' [ftac length_Lev, etac ssubst, atac] 1;
blanchet@48975
   657
wenzelm@51798
   658
fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
blanchet@48975
   659
  let
blanchet@48975
   660
    val n = length Lev_0s;
blanchet@48975
   661
    val ks = n downto 1;
blanchet@48975
   662
  in
blanchet@49305
   663
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   664
      REPEAT_DETERM o rtac allI,
blanchet@48975
   665
      CONJ_WRAP' (fn Lev_0 =>
blanchet@49305
   666
        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
wenzelm@51798
   667
          etac @{thm singletonE}, hyp_subst_tac ctxt,
wenzelm@51798
   668
          dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
wenzelm@51798
   669
          hyp_subst_tac ctxt,
wenzelm@51798
   670
          rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
blanchet@48975
   671
          rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
blanchet@48975
   672
      REPEAT_DETERM o rtac allI,
blanchet@48975
   673
      CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
blanchet@49305
   674
        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   675
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
wenzelm@51798
   676
            (fn i =>
wenzelm@51798
   677
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
wenzelm@51798
   678
              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
blanchet@48975
   679
              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
blanchet@48975
   680
              rtac Lev_0, rtac @{thm singletonI},
wenzelm@51798
   681
              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
blanchet@48975
   682
              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
blanchet@49366
   683
              rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
blanchet@48975
   684
              rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
blanchet@48975
   685
              etac mp, etac conjI, atac]) ks])
blanchet@48975
   686
      (Lev_0s ~~ Lev_Sucs)] 1
blanchet@48975
   687
  end;
blanchet@48975
   688
blanchet@48975
   689
fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
blanchet@48975
   690
  let
blanchet@48975
   691
    val n = length rv_Nils;
blanchet@48975
   692
    val ks = 1 upto n;
blanchet@48975
   693
  in
blanchet@48975
   694
    EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
blanchet@48975
   695
      REPEAT_DETERM o rtac allI,
blanchet@48975
   696
      CONJ_WRAP' (fn rv_Cons =>
blanchet@48975
   697
        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
blanchet@48975
   698
          rtac (@{thm append_Nil} RS arg_cong RS trans),
blanchet@48975
   699
          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil]))
blanchet@48975
   700
        (ks ~~ rv_Nils))
blanchet@48975
   701
      rv_Conss,
blanchet@48975
   702
      REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
blanchet@48975
   703
      EVERY' (map (fn i =>
blanchet@48975
   704
        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
blanchet@48975
   705
          CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
blanchet@48975
   706
            rtac (@{thm append_Cons} RS arg_cong RS trans),
blanchet@49328
   707
            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
blanchet@48975
   708
            rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
blanchet@48975
   709
          ks])
blanchet@48975
   710
        rv_Conss)
blanchet@48975
   711
      ks)] 1
blanchet@48975
   712
  end;
blanchet@48975
   713
wenzelm@51798
   714
fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
blanchet@48975
   715
  let
blanchet@48975
   716
    val n = length Lev_0s;
blanchet@48975
   717
    val ks = 1 upto n;
blanchet@48975
   718
  in
blanchet@49305
   719
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   720
      REPEAT_DETERM o rtac allI,
blanchet@48975
   721
      CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
blanchet@48975
   722
        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
blanchet@49305
   723
          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
traytel@49488
   724
          rtac (rv_Nil RS arg_cong RS iffD2),
traytel@49488
   725
          rtac (mk_sum_casesN n i RS iffD2),
blanchet@48975
   726
          CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
blanchet@48975
   727
      (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
blanchet@48975
   728
      REPEAT_DETERM o rtac allI,
blanchet@48975
   729
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
blanchet@49305
   730
        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   731
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   732
            (fn (i, (from_to_sbd, coalg_set)) =>
wenzelm@51798
   733
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
traytel@49488
   734
              rtac (rv_Cons RS arg_cong RS iffD2),
traytel@49488
   735
              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
blanchet@48975
   736
              etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
blanchet@49305
   737
              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
blanchet@48975
   738
              etac coalg_set, atac])
blanchet@48975
   739
          (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
blanchet@48975
   740
      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
blanchet@48975
   741
  end;
blanchet@48975
   742
wenzelm@51798
   743
fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
blanchet@48975
   744
  let
blanchet@48975
   745
    val n = length Lev_0s;
blanchet@48975
   746
    val ks = 1 upto n;
blanchet@48975
   747
  in
blanchet@49305
   748
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   749
      REPEAT_DETERM o rtac allI,
blanchet@48975
   750
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
blanchet@49305
   751
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
wenzelm@51798
   752
          etac @{thm singletonE}, hyp_subst_tac ctxt,
blanchet@48975
   753
          CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
blanchet@48975
   754
            (if i = i'
wenzelm@51798
   755
            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
blanchet@48975
   756
              CONJ_WRAP' (fn (i'', Lev_0'') =>
blanchet@48975
   757
                EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
blanchet@49366
   758
                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
blanchet@48975
   759
                  rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
blanchet@49305
   760
                  etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
blanchet@48975
   761
                  rtac @{thm singletonI}])
blanchet@48975
   762
              (ks ~~ Lev_0s)]
blanchet@48975
   763
            else etac (mk_InN_not_InM i' i RS notE)))
blanchet@48975
   764
          ks])
blanchet@48975
   765
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
blanchet@48975
   766
      REPEAT_DETERM o rtac allI,
blanchet@48975
   767
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
blanchet@49305
   768
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   769
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   770
            (fn (i, from_to_sbd) =>
wenzelm@51798
   771
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@48975
   772
                CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   773
                  CONJ_WRAP' (fn i'' =>
blanchet@49305
   774
                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
blanchet@49366
   775
                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
blanchet@48975
   776
                      rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
blanchet@48975
   777
                      rtac conjI, atac, dtac (sym RS trans RS sym),
blanchet@48975
   778
                      rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
blanchet@48975
   779
                      etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
blanchet@48975
   780
                      dtac (mk_conjunctN n i), dtac mp, atac,
blanchet@48975
   781
                      dtac (mk_conjunctN n i'), dtac mp, atac,
blanchet@48975
   782
                      dtac (mk_conjunctN n i''), etac mp, atac])
blanchet@48975
   783
                  ks)
blanchet@48975
   784
                ks])
blanchet@48975
   785
          (rev (ks ~~ from_to_sbds))])
blanchet@48975
   786
      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
blanchet@48975
   787
  end;
blanchet@48975
   788
wenzelm@51798
   789
fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
blanchet@48975
   790
  let
blanchet@48975
   791
    val n = length Lev_0s;
blanchet@48975
   792
    val ks = 1 upto n;
blanchet@48975
   793
  in
blanchet@49305
   794
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
   795
      REPEAT_DETERM o rtac allI,
blanchet@48975
   796
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
blanchet@49305
   797
        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
wenzelm@51798
   798
          etac @{thm singletonE}, hyp_subst_tac ctxt,
blanchet@48975
   799
          CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   800
            CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
blanchet@48975
   801
              (if i = i''
blanchet@48975
   802
              then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
blanchet@49305
   803
                dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
wenzelm@51798
   804
                hyp_subst_tac ctxt,
blanchet@48975
   805
                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   806
                  (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
traytel@49488
   807
                    dtac list_inject_iffD1 THEN' etac conjE THEN'
blanchet@48975
   808
                    (if k = i'
wenzelm@51798
   809
                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
blanchet@48975
   810
                    else etac (mk_InN_not_InM i' k RS notE)))
blanchet@48975
   811
                (rev ks)]
blanchet@48975
   812
              else etac (mk_InN_not_InM i'' i RS notE)))
blanchet@48975
   813
            ks)
blanchet@48975
   814
          ks])
blanchet@48975
   815
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
blanchet@48975
   816
      REPEAT_DETERM o rtac allI,
blanchet@48975
   817
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
blanchet@49305
   818
        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   819
          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
blanchet@48975
   820
            (fn (i, (from_to_sbd, to_sbd_inj)) =>
wenzelm@51798
   821
              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
blanchet@48975
   822
              CONJ_WRAP' (fn i' => rtac impI THEN'
blanchet@48975
   823
                dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
blanchet@49305
   824
                dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
blanchet@48975
   825
                CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
blanchet@48975
   826
                  REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
traytel@49488
   827
                  dtac list_inject_iffD1 THEN' etac conjE THEN'
blanchet@48975
   828
                  (if k = i
blanchet@48975
   829
                  then EVERY' [dtac (mk_InN_inject n i),
traytel@49488
   830
                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
wenzelm@51798
   831
                    atac, atac, hyp_subst_tac ctxt] THEN'
blanchet@48975
   832
                    CONJ_WRAP' (fn i'' =>
blanchet@48975
   833
                      EVERY' [rtac impI, dtac (sym RS trans),
blanchet@48975
   834
                        rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
blanchet@48975
   835
                        etac (from_to_sbd RS arg_cong),
blanchet@48975
   836
                        REPEAT_DETERM o etac allE,
blanchet@48975
   837
                        dtac (mk_conjunctN n i), dtac mp, atac,
blanchet@48975
   838
                        dtac (mk_conjunctN n i'), dtac mp, atac,
blanchet@48975
   839
                        dtac (mk_conjunctN n i''), etac mp, etac sym])
blanchet@48975
   840
                    ks
blanchet@48975
   841
                  else etac (mk_InN_not_InM i k RS notE)))
blanchet@48975
   842
                (rev ks))
blanchet@48975
   843
              ks)
blanchet@48975
   844
          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
blanchet@48975
   845
      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
blanchet@48975
   846
  end;
blanchet@48975
   847
blanchet@48975
   848
fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
blanchet@48975
   849
  to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
blanchet@51766
   850
  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_mapss coalg_setss
blanchet@51761
   851
  map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
blanchet@48975
   852
  let
blanchet@48975
   853
    val n = length beh_defs;
blanchet@48975
   854
    val ks = 1 upto n;
blanchet@48975
   855
blanchet@48975
   856
    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
blanchet@51766
   857
      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps,
blanchet@48975
   858
        (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
blanchet@49305
   859
      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
blanchet@48975
   860
        rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
blanchet@48975
   861
        rtac conjI,
blanchet@49305
   862
          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
blanchet@48975
   863
          rtac @{thm singletonI},
blanchet@48975
   864
        rtac conjI,
blanchet@48975
   865
          rtac @{thm UN_least}, rtac Lev_sbd,
blanchet@48975
   866
        rtac conjI,
blanchet@48975
   867
          rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
blanchet@48975
   868
          rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
traytel@50058
   869
          etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
blanchet@48975
   870
        rtac conjI,
blanchet@48975
   871
          rtac ballI, etac @{thm UN_E}, rtac conjI,
blanchet@48975
   872
          if n = 1 then K all_tac else rtac (mk_sumEN n),
blanchet@51766
   873
          EVERY' (map6 (fn i => fn isNode_def => fn set_maps =>
blanchet@48975
   874
            fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
blanchet@48975
   875
            EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
blanchet@48975
   876
              rtac exI, rtac conjI,
blanchet@48975
   877
              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
blanchet@48975
   878
              else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
blanchet@49328
   879
                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
blanchet@51766
   880
              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
blanchet@51766
   881
                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
blanchet@49305
   882
                  rtac trans_fun_cong_image_id_id_apply,
blanchet@48975
   883
                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
blanchet@51766
   884
              (take m set_maps) set_rv_Levs),
blanchet@51766
   885
              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
blanchet@51766
   886
                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
blanchet@48975
   887
                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
blanchet@48975
   888
                  if n = 1 then rtac refl else atac, atac, rtac subsetI,
blanchet@48975
   889
                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
wenzelm@51798
   890
                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
blanchet@48975
   891
                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
blanchet@48975
   892
                  if n = 1 then rtac refl else atac])
blanchet@51766
   893
              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
blanchet@51766
   894
          ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss),
blanchet@51766
   895
          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps,
blanchet@48975
   896
            (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
blanchet@48975
   897
            EVERY' [rtac ballI,
blanchet@48975
   898
              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
blanchet@48975
   899
              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
blanchet@48975
   900
              rtac exI, rtac conjI,
blanchet@48975
   901
              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
blanchet@48975
   902
              else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
blanchet@49328
   903
                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
blanchet@51766
   904
              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
blanchet@51766
   905
                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
blanchet@49305
   906
                  rtac trans_fun_cong_image_id_id_apply,
blanchet@48975
   907
                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
blanchet@51766
   908
              (take m set_maps) set_rv_Levs),
blanchet@51766
   909
              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
blanchet@51766
   910
                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
blanchet@48975
   911
                  rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
blanchet@48975
   912
                  if n = 1 then rtac refl else atac, atac, rtac subsetI,
blanchet@48975
   913
                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
blanchet@48975
   914
                  REPEAT_DETERM_N 4 o etac thin_rl,
blanchet@48975
   915
                  rtac set_image_Lev,
wenzelm@51798
   916
                  atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
blanchet@48975
   917
                  etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
blanchet@48975
   918
                  if n = 1 then rtac refl else atac])
blanchet@51766
   919
              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
blanchet@51766
   920
          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~
blanchet@48975
   921
            (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
blanchet@48975
   922
        (**)
blanchet@48975
   923
          rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
blanchet@48975
   924
          etac notE, etac @{thm UN_I[OF UNIV_I]},
blanchet@48975
   925
        (*root isNode*)
blanchet@48975
   926
          rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
blanchet@49305
   927
          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
blanchet@48975
   928
          CONVERSION (Conv.top_conv
blanchet@48975
   929
            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
blanchet@48975
   930
          if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
blanchet@51766
   931
          EVERY' (map2 (fn set_map => fn coalg_set =>
blanchet@51766
   932
            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
blanchet@49305
   933
              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
blanchet@51766
   934
            (take m set_maps) (take m coalg_sets)),
blanchet@51766
   935
          CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
blanchet@51766
   936
            EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
blanchet@48975
   937
              rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
blanchet@49305
   938
              rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
blanchet@48975
   939
              atac, rtac subsetI,
blanchet@48975
   940
              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
blanchet@49305
   941
              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
blanchet@48975
   942
              rtac @{thm singletonI}, dtac length_Lev',
blanchet@48975
   943
              etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
blanchet@48975
   944
                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
blanchet@48975
   945
              rtac rv_Nil])
blanchet@51766
   946
          (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
blanchet@48975
   947
blanchet@48975
   948
    fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
blanchet@51761
   949
      ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
blanchet@48975
   950
      EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
blanchet@48975
   951
        rtac (@{thm if_P} RS
blanchet@49328
   952
          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
blanchet@49305
   953
        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
blanchet@48975
   954
        rtac Lev_0, rtac @{thm singletonI},
blanchet@48975
   955
        CONVERSION (Conv.top_conv
blanchet@48975
   956
          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
blanchet@48975
   957
        if n = 1 then K all_tac
blanchet@49328
   958
        else (rtac (sum_case_weak_cong RS trans) THEN'
blanchet@48975
   959
          rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
blanchet@51761
   960
        rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
blanchet@48975
   961
        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
traytel@49488
   962
          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
blanchet@48975
   963
            rtac trans, rtac @{thm Shift_def},
blanchet@48975
   964
            rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
blanchet@48975
   965
            REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
blanchet@48975
   966
            etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
blanchet@48975
   967
            rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
blanchet@48975
   968
            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
blanchet@48975
   969
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
traytel@49488
   970
                dtac list_inject_iffD1, etac conjE,
blanchet@48975
   971
                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
traytel@49488
   972
                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
wenzelm@51798
   973
                  atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
blanchet@48975
   974
                else etac (mk_InN_not_InM i' i'' RS notE)])
blanchet@48975
   975
            (rev ks),
blanchet@48975
   976
            rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
blanchet@49366
   977
            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
blanchet@48975
   978
            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
blanchet@48975
   979
            rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
blanchet@48975
   980
            rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
blanchet@48975
   981
            dtac asm_rl, dtac asm_rl, dtac asm_rl,
blanchet@49305
   982
            dtac (Lev_Suc RS equalityD1 RS set_mp),
blanchet@48975
   983
            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
blanchet@48975
   984
              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
traytel@49488
   985
                dtac list_inject_iffD1, etac conjE,
blanchet@48975
   986
                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
traytel@49488
   987
                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
wenzelm@51798
   988
                  atac, atac, hyp_subst_tac ctxt, atac]
blanchet@48975
   989
                else etac (mk_InN_not_InM i' i'' RS notE)])
blanchet@48975
   990
            (rev ks),
blanchet@49366
   991
            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
blanchet@48975
   992
            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
blanchet@48975
   993
            CONVERSION (Conv.top_conv
blanchet@48975
   994
              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
blanchet@48975
   995
            if n = 1 then K all_tac
blanchet@49328
   996
            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
blanchet@49504
   997
            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
blanchet@48975
   998
            rtac refl])
blanchet@48975
   999
        ks to_sbd_injs from_to_sbds)];
blanchet@48975
  1000
  in
blanchet@48975
  1001
    (rtac mor_cong THEN'
blanchet@48975
  1002
    EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
blanchet@48975
  1003
    stac mor_def THEN' rtac conjI THEN'
blanchet@48975
  1004
    CONJ_WRAP' fbetw_tac
blanchet@48975
  1005
      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
blanchet@48975
  1006
        ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
blanchet@51766
  1007
          (set_mapss ~~ (coalg_setss ~~
blanchet@48975
  1008
            (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
blanchet@48975
  1009
    CONJ_WRAP' mor_tac
blanchet@48975
  1010
      (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
blanchet@51761
  1011
        ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
blanchet@48975
  1012
          (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
blanchet@48975
  1013
  end;
blanchet@48975
  1014
blanchet@51761
  1015
fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
blanchet@48975
  1016
  EVERY' [rtac @{thm congruentI}, dtac lsbisE,
blanchet@48975
  1017
    REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
blanchet@48975
  1018
    etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
blanchet@51761
  1019
    rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
blanchet@48975
  1020
    EVERY' (map (fn equiv_LSBIS =>
blanchet@49305
  1021
      EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
blanchet@48975
  1022
    equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
blanchet@48975
  1023
    etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
blanchet@48975
  1024
blanchet@51766
  1025
fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss =
blanchet@48975
  1026
  EVERY' [stac coalg_def,
blanchet@51766
  1027
    CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
blanchet@48975
  1028
      EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
blanchet@48975
  1029
        rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
blanchet@51766
  1030
        EVERY' (map2 (fn set_map => fn coalgT_set =>
blanchet@51766
  1031
          EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans),
blanchet@49305
  1032
            rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
blanchet@48975
  1033
            etac coalgT_set])
blanchet@51766
  1034
        (take m set_maps) (take m coalgT_sets)),
blanchet@51766
  1035
        CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) =>
blanchet@51766
  1036
          EVERY' [rtac (set_map RS ord_eq_le_trans),
blanchet@48975
  1037
            rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
blanchet@49305
  1038
            rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
blanchet@51766
  1039
        (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))])
blanchet@51766
  1040
    ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
blanchet@48975
  1041
blanchet@48975
  1042
fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
blanchet@48975
  1043
  EVERY' [stac mor_def, rtac conjI,
blanchet@48975
  1044
    CONJ_WRAP' (fn equiv_LSBIS =>
blanchet@48975
  1045
      EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
blanchet@48975
  1046
    equiv_LSBISs,
blanchet@48975
  1047
    CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
blanchet@48975
  1048
      EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
blanchet@48975
  1049
        rtac congruent_str_final, atac, rtac o_apply])
blanchet@48975
  1050
    (equiv_LSBISs ~~ congruent_str_finals)] 1;
blanchet@48975
  1051
blanchet@51761
  1052
fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
blanchet@48975
  1053
  {context = ctxt, prems = _} =
blanchet@49504
  1054
  unfold_thms_tac ctxt defs THEN
blanchet@48975
  1055
  EVERY' [rtac conjI,
blanchet@48975
  1056
    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
blanchet@51761
  1057
    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
blanchet@51761
  1058
      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
blanchet@48975
  1059
        EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
blanchet@48975
  1060
          EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
blanchet@49305
  1061
            etac set_rev_mp, rtac coalg_final_set, rtac Rep])
blanchet@48975
  1062
        Abs_inverses (drop m coalg_final_sets))])
blanchet@51761
  1063
    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
blanchet@48975
  1064
blanchet@48975
  1065
fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
blanchet@49504
  1066
  unfold_thms_tac ctxt defs THEN
blanchet@48975
  1067
  EVERY' [rtac conjI,
blanchet@48975
  1068
    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
blanchet@48975
  1069
    CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
blanchet@48975
  1070
blanchet@51761
  1071
fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
traytel@49488
  1072
  EVERY' [rtac iffD2, rtac mor_UNIV,
blanchet@51761
  1073
    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
blanchet@49501
  1074
      EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
blanchet@49504
  1075
        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
blanchet@48975
  1076
        rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
blanchet@51761
  1077
        rtac (o_apply RS trans RS sym), rtac map_cong0,
blanchet@48975
  1078
        REPEAT_DETERM_N m o rtac refl,
blanchet@49504
  1079
        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
blanchet@51761
  1080
    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
blanchet@48975
  1081
blanchet@48975
  1082
fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
blanchet@48975
  1083
  sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
blanchet@48975
  1084
  let
blanchet@48975
  1085
    val n = length Rep_injects;
blanchet@48975
  1086
  in
traytel@49488
  1087
    EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
blanchet@48975
  1088
      REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
blanchet@48975
  1089
      rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
blanchet@48975
  1090
      rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
blanchet@48975
  1091
      rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
blanchet@48975
  1092
      rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,
blanchet@48975
  1093
      rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls),
blanchet@48975
  1094
      rtac impI,
blanchet@48975
  1095
      CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
blanchet@48975
  1096
        EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
blanchet@48975
  1097
          rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
blanchet@49305
  1098
          rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
blanchet@48975
  1099
          rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
blanchet@48975
  1100
          rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
blanchet@48975
  1101
          rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
traytel@51447
  1102
          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
blanchet@48975
  1103
          rtac Rep_inject])
blanchet@48975
  1104
      (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
blanchet@48975
  1105
  end;
blanchet@48975
  1106
blanchet@48975
  1107
fun mk_unique_mor_tac raw_coinds bis =
blanchet@48975
  1108
  CONJ_WRAP' (fn raw_coind =>
blanchet@49305
  1109
    EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac,
blanchet@48975
  1110
      etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
blanchet@48975
  1111
  raw_coinds 1;
blanchet@48975
  1112
blanchet@49504
  1113
fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
blanchet@49504
  1114
  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
blanchet@49305
  1115
    EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
blanchet@49504
  1116
      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
blanchet@49504
  1117
      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
blanchet@48975
  1118
blanchet@51761
  1119
fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
blanchet@48975
  1120
  {context = ctxt, prems = _} =
blanchet@49504
  1121
  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
blanchet@51761
  1122
    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
blanchet@48975
  1123
    EVERY' (map (fn thm =>
blanchet@49585
  1124
      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
blanchet@49585
  1125
    rtac sym, rtac id_apply] 1;
blanchet@48975
  1126
blanchet@51761
  1127
fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
blanchet@49504
  1128
  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
blanchet@51761
  1129
    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
blanchet@48975
  1130
    REPEAT_DETERM_N m o rtac refl,
blanchet@48975
  1131
    EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
blanchet@48975
  1132
traytel@51739
  1133
fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
traytel@51739
  1134
  unfold_thms_tac ctxt
traytel@51739
  1135
    (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
traytel@51739
  1136
  etac unfold_unique_mor 1;
traytel@51739
  1137
traytel@51893
  1138
fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
traytel@51893
  1139
  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
traytel@51893
  1140
    CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
traytel@51893
  1141
    rel_congs,
traytel@51893
  1142
    CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
traytel@51893
  1143
      REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
traytel@51893
  1144
      REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
traytel@51893
  1145
      REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
traytel@51893
  1146
      etac mp, etac CollectE, etac @{thm splitD}])
traytel@51893
  1147
    rel_congs,
blanchet@48975
  1148
    rtac impI, REPEAT_DETERM o etac conjE,
blanchet@49305
  1149
    CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
traytel@51893
  1150
      rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
blanchet@48975
  1151
traytel@51893
  1152
fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs =
traytel@51893
  1153
  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
traytel@51893
  1154
    EVERY' (map2 (fn rel_mono => fn rel_eq =>
blanchet@48975
  1155
      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
traytel@51893
  1156
        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}),
traytel@51893
  1157
        REPEAT_DETERM_N m o rtac @{thm order_refl},
traytel@51893
  1158
        REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset},
traytel@51893
  1159
        rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl])
traytel@51893
  1160
    rel_monos rel_eqs),
blanchet@48975
  1161
    rtac impI, REPEAT_DETERM o etac conjE,
traytel@51893
  1162
    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1;
blanchet@48975
  1163
blanchet@49581
  1164
fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
blanchet@48975
  1165
  let
blanchet@48975
  1166
    val n = length ks;
blanchet@48975
  1167
  in
blanchet@48975
  1168
    EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI,
blanchet@48975
  1169
      CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
blanchet@48975
  1170
      CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI,
blanchet@48975
  1171
        rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
blanchet@48975
  1172
        atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
blanchet@48975
  1173
        etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
traytel@49490
  1174
        rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
blanchet@48975
  1175
        CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
blanchet@48975
  1176
          REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
blanchet@48975
  1177
        ks])
blanchet@48975
  1178
      ks,
blanchet@48975
  1179
      rtac impI,
blanchet@48975
  1180
      CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
blanchet@49305
  1181
        rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp,
blanchet@48975
  1182
        rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
blanchet@48975
  1183
  end;
blanchet@48975
  1184
traytel@51447
  1185
fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
blanchet@49581
  1186
  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
blanchet@48975
  1187
    EVERY' (map (fn i =>
blanchet@49585
  1188
      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
traytel@51447
  1189
        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
blanchet@48975
  1190
        rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
traytel@51447
  1191
        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
blanchet@48975
  1192
        rtac exI, rtac conjI, etac conjI, atac,
blanchet@48975
  1193
        CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
traytel@51447
  1194
          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
blanchet@48975
  1195
    ks),
blanchet@48975
  1196
    rtac impI, REPEAT_DETERM o etac conjE,
blanchet@48975
  1197
    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
blanchet@48975
  1198
blanchet@51761
  1199
fun mk_map_tac m n cT unfold map_comp' map_cong0 =
blanchet@48975
  1200
  EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
blanchet@51761
  1201
    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0,
blanchet@48975
  1202
    REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
blanchet@48975
  1203
    REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
blanchet@48975
  1204
    rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
blanchet@48975
  1205
blanchet@48975
  1206
fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
blanchet@48975
  1207
  EVERY' [rtac hset_minimal,
blanchet@48975
  1208
    REPEAT_DETERM_N n o rtac @{thm Un_upper1},
blanchet@48975
  1209
    REPEAT_DETERM_N n o
blanchet@48975
  1210
      EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
blanchet@49366
  1211
        EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
blanchet@48975
  1212
          etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
blanchet@48975
  1213
          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
blanchet@48975
  1214
      (1 upto n) set_hsets set_hset_hsetss)] 1;
blanchet@48975
  1215
blanchet@49585
  1216
fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
blanchet@48975
  1217
  EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
blanchet@48975
  1218
    REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
blanchet@48975
  1219
    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
blanchet@48975
  1220
blanchet@49504
  1221
fun mk_map_id_tac maps unfold_unique unfold_dtor =
blanchet@49504
  1222
  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
blanchet@49504
  1223
    rtac unfold_dtor] 1;
blanchet@48975
  1224
blanchet@51761
  1225
fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
blanchet@49504
  1226
  EVERY' [rtac unfold_unique,
blanchet@51761
  1227
    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 =>
blanchet@48975
  1228
      EVERY' (map rtac
blanchet@48975
  1229
        ([@{thm o_assoc} RS trans,
blanchet@48975
  1230
        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
blanchet@48975
  1231
        @{thm o_assoc} RS trans RS sym,
blanchet@48975
  1232
        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
blanchet@48975
  1233
        @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
blanchet@48975
  1234
        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
blanchet@51761
  1235
        ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong0] @
blanchet@48975
  1236
        replicate m (@{thm id_o} RS fun_cong) @
blanchet@48975
  1237
        replicate n (@{thm o_id} RS fun_cong))))
blanchet@51761
  1238
    maps map_comps map_cong0s)] 1;
blanchet@48975
  1239
wenzelm@51798
  1240
fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
blanchet@48975
  1241
  set_hset_hsetsss =
blanchet@48975
  1242
  let
blanchet@48975
  1243
    val n = length map_comp's;
blanchet@48975
  1244
    val ks = 1 upto n;
blanchet@48975
  1245
  in
blanchet@48975
  1246
    EVERY' ([rtac rev_mp,
blanchet@48975
  1247
      coinduct_tac] @
blanchet@51766
  1248
      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
blanchet@48975
  1249
        set_hset_hsetss) =>
wenzelm@51798
  1250
        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
wenzelm@51798
  1251
         rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
blanchet@49585
  1252
         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
blanchet@48975
  1253
         REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
blanchet@51761
  1254
         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
blanchet@48975
  1255
         EVERY' (maps (fn set_hset =>
blanchet@49585
  1256
           [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
blanchet@48975
  1257
           REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
blanchet@48975
  1258
         REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
blanchet@51766
  1259
         CONJ_WRAP' (fn (set_map, set_hset_hsets) =>
blanchet@48975
  1260
           EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
blanchet@51766
  1261
             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map,
blanchet@48975
  1262
             rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
blanchet@48975
  1263
             REPEAT_DETERM o etac conjE,
blanchet@48975
  1264
             CONJ_WRAP' (fn set_hset_hset =>
blanchet@48975
  1265
               EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
blanchet@51766
  1266
           (drop m set_maps ~~ set_hset_hsetss)])
blanchet@49541
  1267
        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
blanchet@51766
  1268
          map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @
blanchet@48975
  1269
      [rtac impI,
blanchet@48975
  1270
       CONJ_WRAP' (fn k =>
blanchet@48975
  1271
         EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
blanchet@48975
  1272
           rtac conjI, rtac refl, rtac refl]) ks]) 1
blanchet@48975
  1273
  end
blanchet@48975
  1274
blanchet@49543
  1275
fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
blanchet@49504
  1276
  rtac unfold_unique 1 THEN
blanchet@49504
  1277
  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
blanchet@48975
  1278
  ALLGOALS (etac sym);
blanchet@48975
  1279
blanchet@51766
  1280
fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
blanchet@48975
  1281
  {context = ctxt, prems = _} =
blanchet@48975
  1282
  let
blanchet@49541
  1283
    val n = length dtor_maps;
blanchet@48975
  1284
  in
blanchet@49305
  1285
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@49504
  1286
      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
blanchet@48975
  1287
      CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
blanchet@48975
  1288
      REPEAT_DETERM o rtac allI,
blanchet@49541
  1289
      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
blanchet@49504
  1290
        [SELECT_GOAL (unfold_thms_tac ctxt
blanchet@49541
  1291
          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
blanchet@48975
  1292
        rtac @{thm Un_cong}, rtac refl,
blanchet@48975
  1293
        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
blanchet@48975
  1294
          (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
blanchet@48975
  1295
            REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
blanchet@51766
  1296
      (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
blanchet@48975
  1297
  end;
blanchet@48975
  1298
blanchet@51766
  1299
fun mk_set_map_tac hset_def col_natural =
blanchet@48975
  1300
  EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
blanchet@48975
  1301
    (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
blanchet@48975
  1302
    (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
blanchet@48975
  1303
blanchet@48975
  1304
fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
blanchet@48975
  1305
  let
blanchet@48975
  1306
    val n = length rec_0s;
blanchet@48975
  1307
  in
blanchet@49305
  1308
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
  1309
      REPEAT_DETERM o rtac allI,
blanchet@49305
  1310
      CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [ordIso_ordLeq_trans,
blanchet@48975
  1311
        @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
blanchet@48975
  1312
      REPEAT_DETERM o rtac allI,
blanchet@48975
  1313
      CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
blanchet@49305
  1314
        [rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
blanchet@48975
  1315
        rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
blanchet@48975
  1316
        REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
blanchet@48975
  1317
        EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
blanchet@48975
  1318
          rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE,
blanchet@48975
  1319
          etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
blanchet@48975
  1320
      (rec_Sucs ~~ set_sbdss)] 1
blanchet@48975
  1321
  end;
blanchet@48975
  1322
blanchet@48975
  1323
fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
blanchet@49305
  1324
  EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def,
blanchet@49305
  1325
    ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
blanchet@48975
  1326
    @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
blanchet@48975
  1327
    ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
blanchet@48975
  1328
wenzelm@51798
  1329
fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
blanchet@48975
  1330
  sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
blanchet@48975
  1331
  let
blanchet@48975
  1332
    val n = length isNode_hsets;
blanchet@48975
  1333
    val in_hin_tac = rtac CollectI THEN'
blanchet@48975
  1334
      CONJ_WRAP' (fn mor_hset => EVERY' (map etac
blanchet@49305
  1335
        [mor_hset OF [coalgT, mor_T_final] RS sym RS ord_eq_le_trans,
blanchet@49305
  1336
        arg_cong RS sym RS ord_eq_le_trans,
blanchet@49305
  1337
        mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS ord_eq_le_trans])) mor_hsets;
blanchet@48975
  1338
  in
blanchet@48975
  1339
    EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans,
blanchet@49305
  1340
      rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans,
blanchet@48975
  1341
      rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
blanchet@48975
  1342
      rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero},
traytel@51782
  1343
      rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm Card_order_csum},
blanchet@48975
  1344
      rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order,
blanchet@48975
  1345
      rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
blanchet@48975
  1346
      rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
blanchet@49305
  1347
      rtac set_mp, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
blanchet@49305
  1348
      rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
blanchet@48975
  1349
      rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
blanchet@49305
  1350
      ftac (carT_def RS equalityD1 RS set_mp),
wenzelm@51798
  1351
      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@49305
  1352
      rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
blanchet@48975
  1353
      rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
blanchet@48975
  1354
      rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
blanchet@48975
  1355
      CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) =>
blanchet@48975
  1356
        EVERY' [rtac (mk_disjIN n i), rtac isNode_hset, atac, atac, atac, in_hin_tac])
blanchet@48975
  1357
      (1 upto n ~~ isNode_hsets),
blanchet@48975
  1358
      CONJ_WRAP' (fn isNode_hset =>
blanchet@48975
  1359
        EVERY' [rtac ballI, rtac isNode_hset, atac, ftac CollectD, etac @{thm SuccD},
blanchet@48975
  1360
          etac bspec, atac, in_hin_tac])
blanchet@48975
  1361
      isNode_hsets,
blanchet@48975
  1362
      atac, rtac isNode_hset, atac, atac, atac, in_hin_tac] 1
blanchet@48975
  1363
  end;
blanchet@48975
  1364
blanchet@48975
  1365
fun mk_bd_card_order_tac sbd_card_order =
blanchet@48975
  1366
  EVERY' (map rtac [@{thm card_order_ccexp}, sbd_card_order, sbd_card_order]) 1;
blanchet@48975
  1367
blanchet@48975
  1368
fun mk_bd_cinfinite_tac sbd_Cinfinite =
blanchet@48975
  1369
  EVERY' (map rtac [@{thm cinfinite_ccexp}, @{thm ctwo_ordLeq_Cinfinite},
blanchet@48975
  1370
    sbd_Cinfinite, sbd_Cinfinite]) 1;
blanchet@48975
  1371
blanchet@48975
  1372
fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
blanchet@48975
  1373
  let
blanchet@48975
  1374
    val m = length set_incl_hsets;
blanchet@48975
  1375
  in
blanchet@48975
  1376
    EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
blanchet@48975
  1377
      EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
blanchet@48975
  1378
      CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
blanchet@48975
  1379
      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
blanchet@48975
  1380
      EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
blanchet@48975
  1381
      CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
blanchet@48975
  1382
      REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
blanchet@48975
  1383
  end;
blanchet@48975
  1384
blanchet@51766
  1385
fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs
blanchet@48975
  1386
  {context = ctxt, prems = _} =
blanchet@49504
  1387
  unfold_thms_tac ctxt [coalg_def] THEN
blanchet@51766
  1388
  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
blanchet@48975
  1389
    EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
blanchet@48975
  1390
      REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
wenzelm@51798
  1391
      hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
blanchet@48975
  1392
      EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
blanchet@48975
  1393
      pickWP_assms_tac,
blanchet@49504
  1394
      SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
blanchet@48975
  1395
      REPEAT_DETERM o eresolve_tac [CollectE, conjE],
blanchet@48975
  1396
      rtac CollectI,
traytel@49490
  1397
      REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
blanchet@51766
  1398
      CONJ_WRAP' (fn set_map =>
blanchet@51766
  1399
        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map,
blanchet@49305
  1400
          rtac trans_fun_cong_image_id_id_apply, atac])
blanchet@51766
  1401
      (drop m set_maps)])
blanchet@51766
  1402
  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
blanchet@48975
  1403
blanchet@48975
  1404
fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
traytel@51070
  1405
  {context = ctxt, prems = _: thm list} =
blanchet@48975
  1406
  let
blanchet@48975
  1407
    val n = length map_comps;
blanchet@48975
  1408
  in
blanchet@49504
  1409
    unfold_thms_tac ctxt [mor_def] THEN
blanchet@48975
  1410
    EVERY' [rtac conjI,
blanchet@48975
  1411
      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
blanchet@48975
  1412
      CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
blanchet@48975
  1413
        EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
blanchet@48975
  1414
          REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
wenzelm@51798
  1415
          hyp_subst_tac ctxt,
blanchet@49504
  1416
          SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
blanchet@48975
  1417
          rtac (map_comp RS trans),
blanchet@49504
  1418
          SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
blanchet@48975
  1419
          rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
blanchet@48975
  1420
          pickWP_assms_tac])
blanchet@48975
  1421
      (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
blanchet@48975
  1422
  end;
blanchet@48975
  1423
blanchet@48975
  1424
val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
blanchet@48975
  1425
val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
blanchet@48975
  1426
blanchet@49504
  1427
fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
blanchet@49504
  1428
  unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
blanchet@49504
  1429
  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
blanchet@49504
  1430
  CONJ_WRAP' (fn (unfold, map_comp) =>
blanchet@48975
  1431
    EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
wenzelm@51798
  1432
      hyp_subst_tac ctxt,
blanchet@49504
  1433
      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
blanchet@48975
  1434
      rtac refl])
blanchet@49504
  1435
  (unfolds ~~ map_comps) 1;
blanchet@48975
  1436
blanchet@51766
  1437
fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
blanchet@48975
  1438
  {context = ctxt, prems = _} =
blanchet@48975
  1439
  let
blanchet@48975
  1440
    val n = length rec_0s;
blanchet@48975
  1441
    val ks = n downto 1;
blanchet@48975
  1442
  in
blanchet@49305
  1443
    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
blanchet@48975
  1444
      REPEAT_DETERM o rtac allI,
blanchet@48975
  1445
      CONJ_WRAP' (fn thm => EVERY'
blanchet@49305
  1446
        [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
blanchet@48975
  1447
      REPEAT_DETERM o rtac allI,
blanchet@51766
  1448
      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
blanchet@48975
  1449
        EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
blanchet@48975
  1450
          REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
wenzelm@51798
  1451
          hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
blanchet@48975
  1452
          EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
blanchet@48975
  1453
          pickWP_assms_tac,
blanchet@48975
  1454
          rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
blanchet@49305
  1455
          rtac ord_eq_le_trans, rtac rec_Suc,
blanchet@48975
  1456
          rtac @{thm Un_least},
blanchet@51766
  1457
          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1),
blanchet@48975
  1458
            @{thm prod.cases}]),
blanchet@49305
  1459
          etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
blanchet@51766
  1460
          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
blanchet@48975
  1461
            EVERY' [rtac @{thm UN_least},
blanchet@51766
  1462
              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
wenzelm@51798
  1463
              etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
blanchet@49305
  1464
              dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
blanchet@51766
  1465
          (ks ~~ rev (drop m set_maps))])
blanchet@51766
  1466
      (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
blanchet@48975
  1467
  end;
blanchet@48975
  1468
blanchet@48975
  1469
fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
blanchet@48975
  1470
  mor_unique pick_cols hset_defs =
traytel@49488
  1471
  EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
blanchet@48975
  1472
    REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
blanchet@48975
  1473
    rtac box_equals, rtac mor_unique,
blanchet@48975
  1474
    rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1475
    rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1476
    rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1477
    rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
blanchet@48975
  1478
    rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv},
blanchet@48975
  1479
    rtac box_equals, rtac mor_unique,
blanchet@48975
  1480
    rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1481
    rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1482
    rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1483
    rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
blanchet@48975
  1484
    rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
blanchet@48975
  1485
    rtac CollectI,
blanchet@48975
  1486
    CONJ_WRAP' (fn (pick, def) =>
blanchet@49305
  1487
      EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least},
blanchet@48975
  1488
        rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
blanchet@48975
  1489
        rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
blanchet@48975
  1490
        rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
blanchet@48975
  1491
    (pick_cols ~~ hset_defs)] 1;
blanchet@48975
  1492
blanchet@49585
  1493
fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
traytel@49104
  1494
  ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
blanchet@48975
  1495
  REPEAT_DETERM (atac 1 ORELSE
blanchet@49585
  1496
    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
blanchet@49504
  1497
    K (unfold_thms_tac ctxt dtor_ctors),
blanchet@48975
  1498
    REPEAT_DETERM_N n o etac UnE,
blanchet@48975
  1499
    REPEAT_DETERM o
blanchet@48975
  1500
      (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
blanchet@48975
  1501
        (eresolve_tac wit ORELSE'
blanchet@48975
  1502
        (dresolve_tac wit THEN'
blanchet@48975
  1503
          (etac FalseE ORELSE'
wenzelm@51798
  1504
          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
blanchet@49504
  1505
            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
blanchet@48975
  1506
blanchet@49504
  1507
fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
wenzelm@51798
  1508
  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
blanchet@49504
  1509
  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
wenzelm@51798
  1510
  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
traytel@49104
  1511
  ALLGOALS (TRY o
traytel@49104
  1512
    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
traytel@49104
  1513
traytel@51893
  1514
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
wenzelm@51798
  1515
    dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
blanchet@48975
  1516
  let
blanchet@49544
  1517
    val m = length dtor_set_incls;
blanchet@49544
  1518
    val n = length dtor_set_set_inclss;
blanchet@51766
  1519
    val (passive_set_maps, active_set_maps) = chop m set_maps;
traytel@51893
  1520
    val in_Jrel = nth in_Jrels (i - 1);
blanchet@48975
  1521
    val if_tac =
traytel@51893
  1522
      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
traytel@51893
  1523
        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@51766
  1524
        EVERY' (map2 (fn set_map => fn set_incl =>
blanchet@51766
  1525
          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
blanchet@49305
  1526
            rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
blanchet@48975
  1527
            etac (set_incl RS @{thm subset_trans})])
blanchet@51766
  1528
        passive_set_maps dtor_set_incls),
traytel@51893
  1529
        CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) =>
traytel@51893
  1530
          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
traytel@51893
  1531
            rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@49544
  1532
            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
blanchet@48975
  1533
            rtac conjI, rtac refl, rtac refl])
traytel@51893
  1534
        (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
blanchet@48975
  1535
        CONJ_WRAP' (fn conv =>
blanchet@51761
  1536
          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
blanchet@48975
  1537
          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
blanchet@48975
  1538
          REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
blanchet@49541
  1539
          rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
blanchet@48975
  1540
        @{thms fst_conv snd_conv}];
blanchet@48975
  1541
    val only_if_tac =
traytel@51893
  1542
      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
traytel@51893
  1543
        rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
blanchet@51766
  1544
        CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
blanchet@49585
  1545
          EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
blanchet@51766
  1546
            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
blanchet@49501
  1547
            rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
blanchet@48975
  1548
            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
traytel@51893
  1549
              (fn (active_set_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
blanchet@48975
  1550
                rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
blanchet@51766
  1551
                rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
blanchet@49305
  1552
                dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
traytel@51893
  1553
                dtac @{thm ssubst_mem[OF pair_collapse]},
traytel@51893
  1554
                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
traytel@51893
  1555
                  @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
traytel@51893
  1556
                hyp_subst_tac ctxt,
traytel@51893
  1557
                dtac (in_Jrel RS iffD1),
blanchet@48975
  1558
                dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
traytel@51893
  1559
                TRY o
traytel@51893
  1560
                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
traytel@51893
  1561
                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
traytel@51893
  1562
            (rev (active_set_maps ~~ in_Jrels))])
blanchet@51766
  1563
        (dtor_sets ~~ passive_set_maps),
blanchet@48975
  1564
        rtac conjI,
blanchet@49541
  1565
        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
blanchet@49501
  1566
          rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
blanchet@51761
  1567
          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
traytel@51893
  1568
          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
traytel@51893
  1569
            dtac @{thm ssubst_mem[OF pair_collapse]},
traytel@51893
  1570
            REPEAT_DETERM o
traytel@51893
  1571
              eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
traytel@51893
  1572
            hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
traytel@51893
  1573
            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
blanchet@48975
  1574
          atac]]
blanchet@48975
  1575
  in
blanchet@48975
  1576
    EVERY' [rtac iffI, if_tac, only_if_tac] 1
blanchet@48975
  1577
  end;
blanchet@48975
  1578
traytel@51925
  1579
fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss 
traytel@51925
  1580
  dtor_unfolds dtor_maps {context = ctxt, prems = _} =
traytel@51925
  1581
  let val n = length ks;
traytel@51925
  1582
  in
traytel@51925
  1583
    EVERY' [DETERM o rtac coinduct,
traytel@51925
  1584
      EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps =>
traytel@51925
  1585
          fn dtor_unfold => fn dtor_map =>
traytel@51925
  1586
        EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
traytel@51925
  1587
          select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1588
          REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
traytel@51925
  1589
          rtac exI, rtac conjI, rtac conjI,
traytel@51925
  1590
          rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym),
traytel@51925
  1591
          rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]),
traytel@51925
  1592
          REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
traytel@51925
  1593
          REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
traytel@51925
  1594
          rtac (map_comp RS trans), rtac (map_cong RS trans),
traytel@51925
  1595
          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
traytel@51925
  1596
          REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
traytel@51925
  1597
          etac (@{thm prod.cases} RS map_arg_cong RS trans),
traytel@51925
  1598
          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
traytel@51925
  1599
          CONJ_WRAP' (fn set_map =>
traytel@51925
  1600
            EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
traytel@51925
  1601
              dtac (set_map RS equalityD1 RS set_mp),
traytel@51925
  1602
              REPEAT_DETERM o
traytel@51925
  1603
                eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}),
traytel@51925
  1604
              hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
traytel@51925
  1605
              rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
traytel@51925
  1606
          (drop m set_maps)])
traytel@51925
  1607
      ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
traytel@51925
  1608
  end;
traytel@51925
  1609
traytel@51925
  1610
val split_id_unfolds = @{thms prod.cases image_id id_apply};
traytel@51925
  1611
traytel@51925
  1612
fun mk_rel_coinduct_ind_tac m ks unfolds set_mapss j set_induct {context = ctxt, prems = _} =
traytel@51925
  1613
  let val n = length ks;
traytel@51925
  1614
  in
traytel@51925
  1615
    rtac set_induct 1 THEN
traytel@51925
  1616
    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
traytel@51925
  1617
      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
traytel@51925
  1618
        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1619
        REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
traytel@51925
  1620
        hyp_subst_tac ctxt,
traytel@51925
  1621
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_maps (j - 1)] @ split_id_unfolds)),
traytel@51925
  1622
        rtac subset_refl])
traytel@51925
  1623
    unfolds set_mapss ks) 1 THEN
traytel@51925
  1624
    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
traytel@51925
  1625
      EVERY' (map (fn set_map =>
traytel@51925
  1626
        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
traytel@51925
  1627
        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
traytel@51925
  1628
        REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
traytel@51925
  1629
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map] @ split_id_unfolds)),
traytel@51925
  1630
        etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
traytel@51925
  1631
        rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
traytel@51925
  1632
      (drop m set_maps)))
traytel@51925
  1633
    unfolds set_mapss ks) 1
traytel@51925
  1634
  end;
traytel@51925
  1635
traytel@51925
  1636
fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
traytel@51925
  1637
  {context = ctxt, prems = _} =
traytel@51925
  1638
  let val n = length in_rels;
traytel@51925
  1639
  in
traytel@51925
  1640
    unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
traytel@51925
  1641
    REPEAT_DETERM (etac exE 1) THEN
traytel@51925
  1642
    CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
traytel@51925
  1643
      EVERY' [rtac @{thm predicate2I}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI,
traytel@51925
  1644
        if null helper_inds then rtac UNIV_I
traytel@51925
  1645
        else rtac CollectI THEN'
traytel@51925
  1646
          CONJ_WRAP' (fn helper_ind =>
traytel@51925
  1647
            EVERY' [rtac (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
traytel@51925
  1648
              REPEAT_DETERM_N n o etac thin_rl, rtac impI,
traytel@51925
  1649
              REPEAT_DETERM o resolve_tac [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
traytel@51925
  1650
              dtac bspec, atac, REPEAT_DETERM o eresolve_tac [allE, mp, conjE],
traytel@51925
  1651
              etac (refl RSN (2, conjI))])
traytel@51925
  1652
          helper_inds,
traytel@51925
  1653
        rtac conjI,
traytel@51925
  1654
        rtac (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
traytel@51925
  1655
        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI)),
traytel@51925
  1656
        rtac (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
traytel@51925
  1657
        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI))])
traytel@51925
  1658
    (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
traytel@51925
  1659
  end;
traytel@51925
  1660
blanchet@48975
  1661
end;