src/HOL/BNF/Tools/bnf_comp_tactics.ML
author blanchet
Fri Jun 07 09:30:13 2013 +0200 (2013-06-07)
changeset 52334 705bc4f5fc70
parent 51893 596baae88a88
child 52635 4f84b730c489
permissions -rw-r--r--
tuning
blanchet@49509
     1
(*  Title:      HOL/BNF/Tools/bnf_comp_tactics.ML
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Tactics for composition of bounded natural functors.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
signature BNF_COMP_TACTICS =
blanchet@48975
    10
sig
blanchet@48975
    11
  val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
blanchet@48975
    12
  val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
blanchet@48975
    13
  val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
blanchet@48975
    14
  val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
blanchet@48975
    15
  val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
blanchet@51761
    16
  val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
traytel@49630
    17
  val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
blanchet@48975
    18
  val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
blanchet@48975
    19
  val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
blanchet@51766
    20
  val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
blanchet@48975
    21
  val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
blanchet@48975
    22
blanchet@49304
    23
  val mk_kill_bd_card_order_tac: int -> thm -> tactic
blanchet@49304
    24
  val mk_kill_bd_cinfinite_tac: thm -> tactic
blanchet@49304
    25
  val kill_in_alt_tac: tactic
blanchet@49304
    26
  val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
blanchet@51761
    27
  val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
blanchet@49304
    28
  val mk_kill_set_bd_tac: thm -> thm -> tactic
blanchet@48975
    29
blanchet@48975
    30
  val empty_natural_tac: tactic
blanchet@49304
    31
  val lift_in_alt_tac: tactic
blanchet@49304
    32
  val mk_lift_in_bd_tac: int -> thm -> thm -> thm -> tactic
blanchet@49304
    33
  val mk_lift_set_bd_tac: thm -> tactic
blanchet@48975
    34
blanchet@48975
    35
  val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
blanchet@48975
    36
  val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
blanchet@49284
    37
blanchet@49284
    38
  val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
traytel@51893
    39
  val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
blanchet@49284
    40
  val mk_simple_wit_tac: thm list -> tactic
blanchet@48975
    41
end;
blanchet@48975
    42
blanchet@48975
    43
structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
blanchet@48975
    44
struct
blanchet@48975
    45
blanchet@48975
    46
open BNF_Util
blanchet@48975
    47
open BNF_Tactics
blanchet@48975
    48
blanchet@49305
    49
val Card_order_csum = @{thm Card_order_csum};
blanchet@49305
    50
val Card_order_ctwo = @{thm Card_order_ctwo};
blanchet@49305
    51
val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
blanchet@48975
    52
val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
blanchet@49305
    53
val card_of_Card_order = @{thm card_of_Card_order};
blanchet@49305
    54
val csum_Cnotzero1 = @{thm csum_Cnotzero1};
blanchet@48975
    55
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
blanchet@49305
    56
val ordIso_transitive = @{thm ordIso_transitive};
blanchet@49305
    57
val ordLeq_csum2 = @{thm ordLeq_csum2};
blanchet@48975
    58
val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
blanchet@48975
    59
val trans_o_apply = @{thm trans[OF o_apply]};
blanchet@48975
    60
blanchet@48975
    61
blanchet@48975
    62
blanchet@48975
    63
(* Composition *)
blanchet@48975
    64
blanchet@51766
    65
fun mk_comp_set_alt_tac ctxt collect_set_map =
blanchet@49504
    66
  unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
blanchet@51766
    67
  unfold_thms_tac ctxt [collect_set_map RS sym] THEN
blanchet@48975
    68
  rtac refl 1;
blanchet@48975
    69
blanchet@51761
    70
fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
blanchet@51761
    71
  EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
traytel@49630
    72
    map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
traytel@49630
    73
blanchet@51761
    74
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
blanchet@48975
    75
  EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
blanchet@51761
    76
    rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
blanchet@48975
    77
    map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
blanchet@48975
    78
blanchet@51766
    79
fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
blanchet@48975
    80
  EVERY' ([rtac ext] @
blanchet@48975
    81
    replicate 3 (rtac trans_o_apply) @
blanchet@48975
    82
    [rtac (arg_cong_Union RS trans),
blanchet@48975
    83
     rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
blanchet@48975
    84
     rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
blanchet@51761
    85
     rtac Gmap_cong0] @
blanchet@51766
    86
     map (fn thm => rtac (thm RS fun_cong)) set_maps @
blanchet@51766
    87
     [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
blanchet@48975
    88
     rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
blanchet@51766
    89
     rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
blanchet@48975
    90
     rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
blanchet@48975
    91
     rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
blanchet@48975
    92
     rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
blanchet@51766
    93
     [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
blanchet@48975
    94
        rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
blanchet@49305
    95
        rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
blanchet@48975
    96
        rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
blanchet@48975
    97
     rtac @{thm image_empty}]) 1;
blanchet@48975
    98
blanchet@51761
    99
fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
blanchet@48975
   100
  let
blanchet@48975
   101
     val n = length comp_set_alts;
blanchet@48975
   102
  in
blanchet@48975
   103
    (if n = 0 then rtac refl 1
blanchet@51761
   104
    else rtac map_cong0 1 THEN
blanchet@51761
   105
      EVERY' (map_index (fn (i, map_cong0) =>
blanchet@51761
   106
        rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
blanchet@49585
   107
          EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
blanchet@48975
   108
            rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
blanchet@48975
   109
            rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
blanchet@48975
   110
            rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2},
blanchet@48975
   111
            rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp),
blanchet@48975
   112
            etac @{thm imageI}, atac])
blanchet@48975
   113
          comp_set_alts))
blanchet@51761
   114
      map_cong0s) 1)
blanchet@48975
   115
  end;
blanchet@48975
   116
blanchet@48975
   117
fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
blanchet@48975
   118
  let
blanchet@48975
   119
    val (card_orders, last_card_order) = split_last Fbd_card_orders;
blanchet@48975
   120
    fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
blanchet@48975
   121
  in
blanchet@48975
   122
    (rtac @{thm card_order_cprod} THEN'
blanchet@48975
   123
    WRAP' gen_before (K (K all_tac)) card_orders (rtac last_card_order) THEN'
blanchet@48975
   124
    rtac Gbd_card_order) 1
blanchet@48975
   125
  end;
blanchet@48975
   126
blanchet@48975
   127
fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
blanchet@48975
   128
  (rtac @{thm cinfinite_cprod} THEN'
blanchet@48975
   129
   ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
blanchet@48975
   130
     ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
blanchet@48975
   131
      rtac Fbd_cinfinite)) ORELSE'
blanchet@48975
   132
    rtac Fbd_cinfinite) THEN'
blanchet@48975
   133
   rtac Gbd_cinfinite) 1;
blanchet@48975
   134
blanchet@48975
   135
fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
blanchet@48975
   136
  let
blanchet@48975
   137
    val (bds, last_bd) = split_last Gset_Fset_bds;
blanchet@48975
   138
    fun gen_before bd =
blanchet@48975
   139
      rtac ctrans THEN' rtac @{thm Un_csum} THEN'
blanchet@48975
   140
      rtac ctrans THEN' rtac @{thm csum_mono} THEN'
blanchet@48975
   141
      rtac bd;
blanchet@48975
   142
    fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
blanchet@48975
   143
  in
blanchet@49504
   144
    unfold_thms_tac ctxt [comp_set_alt] THEN
blanchet@48975
   145
    rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
blanchet@49504
   146
    unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
blanchet@48975
   147
    (rtac ctrans THEN'
blanchet@48975
   148
     WRAP' gen_before gen_after bds (rtac last_bd) THEN'
blanchet@48975
   149
     rtac @{thm ordIso_imp_ordLeq} THEN'
blanchet@48975
   150
     rtac @{thm cprod_com}) 1
blanchet@48975
   151
  end;
blanchet@48975
   152
blanchet@48975
   153
val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert
blanchet@48975
   154
  Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
blanchet@48975
   155
  conj_assoc};
blanchet@48975
   156
blanchet@48975
   157
fun mk_comp_in_alt_tac ctxt comp_set_alts =
blanchet@49504
   158
  unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
blanchet@49504
   159
  unfold_thms_tac ctxt @{thms set_eq_subset} THEN
blanchet@48975
   160
  rtac conjI 1 THEN
blanchet@48975
   161
  REPEAT_DETERM (
blanchet@48975
   162
    rtac @{thm subsetI} 1 THEN
blanchet@49504
   163
    unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
blanchet@48975
   164
    (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
blanchet@48975
   165
     REPEAT_DETERM (CHANGED ((
blanchet@49305
   166
       (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
blanchet@48975
   167
       atac ORELSE'
blanchet@49305
   168
       (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
blanchet@48975
   169
blanchet@48975
   170
fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order =
blanchet@48975
   171
  let
blanchet@48975
   172
    val (bds, last_bd) = split_last Fin_bds;
blanchet@48975
   173
    val (Cinfs, _) = split_last Fbd_Cinfs;
blanchet@48975
   174
    fun gen_before (bd, _) = rtac ctrans THEN' rtac @{thm csum_mono} THEN' rtac bd;
blanchet@48975
   175
    fun gen_after (_, (bd_Cinf, next_bd_Cinf)) =
blanchet@48975
   176
      TRY o (rtac @{thm csum_cexp} THEN'
blanchet@48975
   177
        rtac bd_Cinf THEN'
blanchet@48975
   178
        (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE'
blanchet@48975
   179
           rtac next_bd_Cinf) THEN'
blanchet@49305
   180
        ((rtac Card_order_csum THEN' rtac ordLeq_csum2) ORELSE'
blanchet@49305
   181
          (rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl})) THEN'
blanchet@49305
   182
        rtac Card_order_ctwo);
blanchet@48975
   183
  in
blanchet@48975
   184
    (rtac @{thm ordIso_ordLeq_trans} THEN'
blanchet@48975
   185
     rtac @{thm card_of_ordIso_subst} THEN'
blanchet@48975
   186
     rtac comp_in_alt THEN'
blanchet@48975
   187
     rtac ctrans THEN'
blanchet@48975
   188
     rtac Gin_bd THEN'
blanchet@48975
   189
     rtac @{thm ordLeq_ordIso_trans} THEN'
blanchet@48975
   190
     rtac @{thm cexp_mono1} THEN'
blanchet@48975
   191
     rtac @{thm ordLeq_ordIso_trans} THEN'
blanchet@48975
   192
     rtac @{thm csum_mono1} THEN'
blanchet@48975
   193
     WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN'
blanchet@48975
   194
     rtac @{thm csum_absorb1} THEN'
blanchet@48975
   195
     rtac @{thm Cinfinite_cexp} THEN'
blanchet@49305
   196
     (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
blanchet@49305
   197
     rtac Card_order_ctwo THEN'
blanchet@48975
   198
     (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
blanchet@48975
   199
       rtac (hd Fbd_Cinfs)) THEN'
blanchet@48975
   200
     rtac @{thm ctwo_ordLeq_Cinfinite} THEN'
blanchet@48975
   201
     rtac @{thm Cinfinite_cexp} THEN'
blanchet@49305
   202
     (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
blanchet@49305
   203
     rtac Card_order_ctwo THEN'
blanchet@48975
   204
     (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
blanchet@48975
   205
       rtac (hd Fbd_Cinfs)) THEN'
blanchet@48975
   206
     rtac Gbd_Card_order THEN'
blanchet@48975
   207
     rtac @{thm cexp_cprod} THEN'
traytel@51782
   208
     rtac @{thm Card_order_csum}) 1
blanchet@48975
   209
  end;
blanchet@48975
   210
blanchet@48975
   211
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
blanchet@48975
   212
  Union_image_insert Union_image_empty};
blanchet@48975
   213
blanchet@51766
   214
fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
blanchet@48975
   215
  ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
blanchet@51766
   216
  unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
blanchet@48975
   217
  REPEAT_DETERM (
blanchet@48975
   218
    atac 1 ORELSE
blanchet@48975
   219
    REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
blanchet@48975
   220
    (TRY o dresolve_tac Gwit_thms THEN'
blanchet@48975
   221
    (etac FalseE ORELSE'
wenzelm@51798
   222
    hyp_subst_tac ctxt THEN'
blanchet@48975
   223
    dresolve_tac Fwit_thms THEN'
blanchet@48975
   224
    (etac FalseE ORELSE' atac))) 1);
blanchet@48975
   225
blanchet@48975
   226
blanchet@48975
   227
blanchet@48975
   228
(* Kill operation *)
blanchet@48975
   229
blanchet@51761
   230
fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
blanchet@51761
   231
  (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
blanchet@48975
   232
    EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
blanchet@48975
   233
blanchet@49304
   234
fun mk_kill_bd_card_order_tac n bd_card_order =
blanchet@48975
   235
  (rtac @{thm card_order_cprod} THEN'
blanchet@48975
   236
  K (REPEAT_DETERM_N (n - 1)
blanchet@48975
   237
    ((rtac @{thm card_order_csum} THEN'
blanchet@48975
   238
    rtac @{thm card_of_card_order_on}) 1)) THEN'
blanchet@48975
   239
  rtac @{thm card_of_card_order_on} THEN'
blanchet@48975
   240
  rtac bd_card_order) 1;
blanchet@48975
   241
blanchet@49304
   242
fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
blanchet@48975
   243
  (rtac @{thm cinfinite_cprod2} THEN'
blanchet@49305
   244
  TRY o rtac csum_Cnotzero1 THEN'
blanchet@49305
   245
  rtac Cnotzero_UNIV THEN'
blanchet@48975
   246
  rtac bd_Cinfinite) 1;
blanchet@48975
   247
blanchet@49304
   248
fun mk_kill_set_bd_tac bd_Card_order set_bd =
blanchet@48975
   249
  (rtac ctrans THEN'
blanchet@48975
   250
  rtac set_bd THEN'
blanchet@48975
   251
  rtac @{thm ordLeq_cprod2} THEN'
blanchet@49305
   252
  TRY o rtac csum_Cnotzero1 THEN'
blanchet@49305
   253
  rtac Cnotzero_UNIV THEN'
blanchet@48975
   254
  rtac bd_Card_order) 1
blanchet@48975
   255
blanchet@49304
   256
val kill_in_alt_tac =
blanchet@49305
   257
  ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
blanchet@48975
   258
  REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
blanchet@48975
   259
  REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
blanchet@49305
   260
    rtac conjI THEN' rtac subset_UNIV) 1)) THEN
blanchet@49305
   261
  (rtac subset_UNIV ORELSE' atac) 1 THEN
blanchet@48975
   262
  REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
blanchet@48975
   263
  REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE
blanchet@48975
   264
  ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
blanchet@49305
   265
    REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
blanchet@48975
   266
blanchet@49304
   267
fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero =
blanchet@48975
   268
  (rtac @{thm ordIso_ordLeq_trans} THEN'
blanchet@48975
   269
  rtac @{thm card_of_ordIso_subst} THEN'
blanchet@48975
   270
  rtac in_alt THEN'
blanchet@48975
   271
  rtac ctrans THEN'
blanchet@48975
   272
  rtac in_bd THEN'
blanchet@48975
   273
  rtac @{thm ordIso_ordLeq_trans} THEN'
blanchet@48975
   274
  rtac @{thm cexp_cong1}) 1 THEN
blanchet@49304
   275
  (if nontrivial_kill_in then
blanchet@49305
   276
    rtac ordIso_transitive 1 THEN
blanchet@48975
   277
    REPEAT_DETERM_N (n - 1)
blanchet@48975
   278
      ((rtac @{thm csum_cong1} THEN'
blanchet@48975
   279
      rtac @{thm ordIso_symmetric} THEN'
blanchet@48975
   280
      rtac @{thm csum_assoc} THEN'
blanchet@49305
   281
      rtac ordIso_transitive) 1) THEN
blanchet@48975
   282
    (rtac @{thm ordIso_refl} THEN'
blanchet@49305
   283
    rtac Card_order_csum THEN'
blanchet@49305
   284
    rtac ordIso_transitive THEN'
blanchet@48975
   285
    rtac @{thm csum_assoc} THEN'
blanchet@49305
   286
    rtac ordIso_transitive THEN'
blanchet@48975
   287
    rtac @{thm csum_cong1} THEN'
blanchet@48975
   288
    K (mk_flatten_assoc_tac
blanchet@48975
   289
      (rtac @{thm ordIso_refl} THEN'
blanchet@49305
   290
        FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
blanchet@49305
   291
      ordIso_transitive @{thm csum_assoc} @{thm csum_cong}) THEN'
blanchet@48975
   292
    rtac @{thm ordIso_refl} THEN'
blanchet@49305
   293
    (rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1
blanchet@48975
   294
  else all_tac) THEN
blanchet@48975
   295
  (rtac @{thm csum_com} THEN'
blanchet@48975
   296
  rtac bd_Card_order THEN'
blanchet@48975
   297
  rtac @{thm ordLeq_ordIso_trans} THEN'
blanchet@48975
   298
  rtac @{thm cexp_mono1} THEN'
blanchet@48975
   299
  rtac ctrans THEN'
blanchet@48975
   300
  rtac @{thm csum_mono2} THEN'
blanchet@48975
   301
  rtac @{thm ordLeq_cprod1} THEN'
blanchet@49305
   302
  (rtac card_of_Card_order ORELSE' rtac Card_order_csum) THEN'
blanchet@48975
   303
  rtac bd_Cnotzero THEN'
blanchet@48975
   304
  rtac @{thm csum_cexp'} THEN'
blanchet@48975
   305
  rtac @{thm Cinfinite_cprod2} THEN'
blanchet@49305
   306
  TRY o rtac csum_Cnotzero1 THEN'
blanchet@49305
   307
  rtac Cnotzero_UNIV THEN'
blanchet@48975
   308
  rtac bd_Cinfinite THEN'
blanchet@49305
   309
  ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
blanchet@49305
   310
    (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
blanchet@49305
   311
  rtac Card_order_ctwo THEN'
blanchet@48975
   312
  rtac bd_Card_order THEN'
blanchet@48975
   313
  rtac @{thm cexp_cprod_ordLeq} THEN'
traytel@51782
   314
  resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN'
blanchet@48975
   315
  rtac @{thm Cinfinite_cprod2} THEN'
blanchet@49305
   316
  TRY o rtac csum_Cnotzero1 THEN'
blanchet@49305
   317
  rtac Cnotzero_UNIV THEN'
blanchet@48975
   318
  rtac bd_Cinfinite THEN'
blanchet@48975
   319
  rtac bd_Cnotzero THEN'
blanchet@48975
   320
  rtac @{thm ordLeq_cprod2} THEN'
blanchet@49305
   321
  TRY o rtac csum_Cnotzero1 THEN'
blanchet@49305
   322
  rtac Cnotzero_UNIV THEN'
blanchet@48975
   323
  rtac bd_Card_order) 1;
blanchet@48975
   324
blanchet@48975
   325
blanchet@48975
   326
blanchet@48975
   327
(* Lift operation *)
blanchet@48975
   328
blanchet@48975
   329
val empty_natural_tac = rtac @{thm empty_natural} 1;
blanchet@48975
   330
blanchet@49304
   331
fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1;
blanchet@48975
   332
blanchet@49304
   333
val lift_in_alt_tac =
blanchet@49305
   334
  ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
blanchet@48975
   335
  REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
blanchet@48975
   336
  REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN
blanchet@48975
   337
  REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
blanchet@48975
   338
  REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
blanchet@48975
   339
    rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN
blanchet@48975
   340
  (rtac @{thm empty_subsetI} ORELSE' atac) 1) ORELSE
blanchet@48975
   341
  ((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
blanchet@48975
   342
    REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
blanchet@48975
   343
blanchet@49304
   344
fun mk_lift_in_bd_tac n in_alt in_bd bd_Card_order =
blanchet@48975
   345
  (rtac @{thm ordIso_ordLeq_trans} THEN'
blanchet@48975
   346
  rtac @{thm card_of_ordIso_subst} THEN'
blanchet@48975
   347
  rtac in_alt THEN'
blanchet@48975
   348
  rtac ctrans THEN'
blanchet@48975
   349
  rtac in_bd THEN'
blanchet@48975
   350
  rtac @{thm cexp_mono1}) 1 THEN
blanchet@48975
   351
  ((rtac @{thm csum_mono1} 1 THEN
blanchet@48975
   352
  REPEAT_DETERM_N (n - 1)
blanchet@48975
   353
    ((rtac ctrans THEN'
blanchet@49305
   354
    rtac ordLeq_csum2 THEN'
blanchet@49305
   355
    (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN
blanchet@49305
   356
  (rtac ordLeq_csum2 THEN'
blanchet@49305
   357
  (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
blanchet@49305
   358
  (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
traytel@51782
   359
  (rtac bd_Card_order) 1;
blanchet@48975
   360
blanchet@48975
   361
blanchet@48975
   362
blanchet@48975
   363
(* Permute operation *)
blanchet@48975
   364
blanchet@48975
   365
fun mk_permute_in_alt_tac src dest =
blanchet@48975
   366
  (rtac @{thm Collect_cong} THEN'
blanchet@48975
   367
  mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
blanchet@48975
   368
    dest src) 1;
blanchet@48975
   369
blanchet@48975
   370
fun mk_permute_in_bd_tac src dest in_alt in_bd bd_Card_order =
blanchet@48975
   371
  (rtac @{thm ordIso_ordLeq_trans} THEN'
blanchet@48975
   372
  rtac @{thm card_of_ordIso_subst} THEN'
blanchet@48975
   373
  rtac in_alt THEN'
blanchet@48975
   374
  rtac @{thm ordLeq_ordIso_trans} THEN'
blanchet@48975
   375
  rtac in_bd THEN'
blanchet@48975
   376
  rtac @{thm cexp_cong1} THEN'
blanchet@48975
   377
  rtac @{thm csum_cong1} THEN'
blanchet@48975
   378
  mk_rotate_eq_tac
blanchet@48975
   379
    (rtac @{thm ordIso_refl} THEN'
blanchet@49305
   380
      FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
blanchet@49305
   381
    ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
blanchet@48975
   382
    src dest THEN'
traytel@51782
   383
  rtac bd_Card_order) 1;
blanchet@48975
   384
blanchet@49284
   385
fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
blanchet@49284
   386
  (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
blanchet@49284
   387
  WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
blanchet@49284
   388
  TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
blanchet@49284
   389
traytel@51893
   390
fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
traytel@51893
   391
  rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
blanchet@49463
   392
blanchet@49284
   393
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
blanchet@49284
   394
blanchet@48975
   395
end;