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