src/HOL/Tools/BNF/bnf_def_tactics.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61242 1f92b0ac9c96
child 61760 1647bb489522
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     1 (*  Title:      HOL/Tools/BNF/bnf_def_tactics.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Author:     Martin Desharnais, TU Muenchen
     5     Copyright   2012, 2013, 2014
     6 
     7 Tactics for definition of bounded natural functors.
     8 *)
     9 
    10 signature BNF_DEF_TACTICS =
    11 sig
    12   val mk_collect_set_map_tac: Proof.context -> thm list -> tactic
    13   val mk_in_mono_tac: Proof.context -> int -> tactic
    14   val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
    15   val mk_inj_map_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
    16   val mk_map_id: thm -> thm
    17   val mk_map_ident: Proof.context -> thm -> thm
    18   val mk_map_comp: thm -> thm
    19   val mk_map_cong_tac: Proof.context -> thm -> tactic
    20   val mk_set_map: thm -> thm
    21   val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
    22 
    23   val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
    24   val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    25   val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
    26   val mk_rel_conversep_tac: Proof.context -> thm -> thm -> tactic
    27   val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
    28   val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
    29   val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
    30   val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
    31   val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
    32   val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
    33 
    34   val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
    35 
    36   val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
    37     thm -> thm -> thm -> thm -> tactic
    38 
    39   val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
    40 end;
    41 
    42 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
    43 struct
    44 
    45 open BNF_Util
    46 open BNF_Tactics
    47 
    48 val ord_eq_le_trans = @{thm ord_eq_le_trans};
    49 val ord_le_eq_trans = @{thm ord_le_eq_trans};
    50 val conversep_shift = @{thm conversep_le_swap} RS iffD1;
    51 
    52 fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
    53 fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def};
    54 fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
    55 fun mk_map_cong_tac ctxt cong0 =
    56   (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
    57    REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
    58 fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
    59 
    60 fun mk_in_mono_tac ctxt n =
    61   if n = 0 then rtac ctxt subset_UNIV 1
    62   else
    63    (rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN
    64    REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN
    65    REPEAT_DETERM_N (n - 1)
    66      ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
    67    (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
    68 
    69 fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
    70   let
    71     val map_cong' = map_cong OF (asm_rl :: replicate n refl);
    72     val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id});
    73   in
    74     HEADGOAL (rtac ctxt @{thm injI} THEN' etac ctxt (map_cong' RS box_equals) THEN'
    75       REPEAT_DETERM_N 2 o (rtac ctxt (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
    76         REPEAT_DETERM_N n o assume_tac ctxt))
    77   end;
    78 
    79 fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
    80   let
    81     val rel_eq' = rel_eq RS @{thm predicate2_eqD};
    82     val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
    83   in
    84     HEADGOAL (dtac ctxt (rel_eq' RS iffD2) THEN' rtac ctxt (rel_eq' RS iffD1)) THEN
    85     EVERY (map (HEADGOAL o dtac ctxt) rel_maps') THEN
    86     HEADGOAL (etac ctxt rel_mono_strong) THEN
    87     TRYALL (Goal.assume_rule_tac ctxt)
    88   end;
    89 
    90 fun mk_collect_set_map_tac ctxt set_map0s =
    91   (rtac ctxt (@{thm collect_comp} RS trans) THEN' rtac ctxt @{thm arg_cong[of _ _ collect]} THEN'
    92   EVERY' (map (fn set_map0 =>
    93     rtac ctxt (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
    94     rtac ctxt set_map0) set_map0s) THEN'
    95   rtac ctxt @{thm image_empty}) 1;
    96 
    97 fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
    98   let
    99     val n = length set_maps;
   100     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
   101   in
   102     if null set_maps then
   103       unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
   104       rtac ctxt @{thm Grp_UNIV_idI[OF refl]} 1
   105     else
   106       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
   107         REPEAT_DETERM o
   108           eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   109         hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   110         REPEAT_DETERM_N n o
   111           EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
   112         rtac ctxt CollectI,
   113         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   114           rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
   115           etac ctxt @{thm set_mp}, assume_tac ctxt])
   116         set_maps,
   117         rtac ctxt @{thm predicate2I}, REPEAT_DETERM o eresolve_tac ctxt [@{thm GrpE}, exE, conjE],
   118         hyp_subst_tac ctxt,
   119         rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
   120         EVERY' (map2 (fn convol => fn map_id0 =>
   121           EVERY' [rtac ctxt @{thm GrpI},
   122             rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
   123             REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong),
   124             REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
   125             rtac ctxt CollectI,
   126             CONJ_WRAP' (fn thm =>
   127               EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
   128                 rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
   129             set_maps])
   130           @{thms fst_convol snd_convol} [map_id, refl])] 1
   131   end;
   132 
   133 fun mk_rel_eq_tac ctxt n rel_Grp rel_cong map_id0 =
   134   (EVERY' (rtac ctxt (rel_cong RS trans) :: replicate n (rtac ctxt @{thm eq_alt})) THEN'
   135   rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
   136   (if n = 0 then rtac ctxt refl
   137   else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
   138     rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, rtac ctxt subsetI, rtac ctxt CollectI,
   139     CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;
   140 
   141 fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
   142   if live = 0 then
   143     HEADGOAL (Goal.conjunction_tac) THEN
   144     unfold_thms_tac ctxt @{thms id_apply} THEN
   145     ALLGOALS (rtac ctxt refl)
   146   else
   147     let
   148       val ks = 1 upto live;
   149     in
   150       Goal.conjunction_tac 1 THEN
   151       unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
   152       TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
   153         resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   154         CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt,
   155         rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   156         CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
   157         REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
   158         dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
   159     end;
   160 
   161 fun mk_rel_mono_tac ctxt rel_OO_Grps in_mono =
   162   let
   163     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
   164       else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
   165         rtac ctxt (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
   166   in
   167     EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm relcompp_mono}, rtac ctxt @{thm iffD2[OF conversep_mono]},
   168       rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono},
   169       rtac ctxt @{thm Grp_mono}, rtac ctxt in_mono, REPEAT_DETERM o etac ctxt @{thm Collect_case_prod_mono}] 1
   170   end;
   171 
   172 fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
   173   let
   174     val n = length set_maps;
   175     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
   176       else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
   177         rtac ctxt (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
   178   in
   179     if null set_maps then rtac ctxt (rel_eq RS @{thm leq_conversepI}) 1
   180     else
   181       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
   182         REPEAT_DETERM o
   183           eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   184         hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
   185         EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans,
   186           rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm,
   187           rtac ctxt (map_comp RS sym), rtac ctxt CollectI,
   188           CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   189             etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   190   end;
   191 
   192 fun mk_rel_conversep_tac ctxt le_conversep rel_mono =
   193   EVERY' [rtac ctxt @{thm antisym}, rtac ctxt le_conversep, rtac ctxt @{thm xt1(6)}, rtac ctxt conversep_shift,
   194     rtac ctxt le_conversep, rtac ctxt @{thm iffD2[OF conversep_mono]}, rtac ctxt rel_mono,
   195     REPEAT_DETERM o rtac ctxt @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
   196 
   197 fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
   198   let
   199     val n = length set_maps;
   200     fun in_tac nthO_in = rtac ctxt CollectI THEN'
   201         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   202           rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
   203     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
   204       else rtac ctxt (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
   205         rtac ctxt (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
   206           (2, ord_le_eq_trans));
   207   in
   208     if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1
   209     else
   210       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
   211         REPEAT_DETERM o
   212           eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   213         hyp_subst_tac ctxt,
   214         rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
   215         rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
   216         REPEAT_DETERM_N n o rtac ctxt @{thm fst_fstOp},
   217         in_tac @{thm fstOp_in},
   218         rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   219         REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
   220           rtac ctxt ballE, rtac ctxt subst,
   221           rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
   222           etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
   223         in_tac @{thm fstOp_in},
   224         rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
   225         rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   226         REPEAT_DETERM_N n o rtac ctxt o_apply,
   227         in_tac @{thm sndOp_in},
   228         rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
   229         REPEAT_DETERM_N n o rtac ctxt @{thm snd_sndOp},
   230         in_tac @{thm sndOp_in}] 1
   231   end;
   232 
   233 fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
   234   if null set_maps then assume_tac ctxt 1
   235   else
   236     unfold_tac ctxt [in_rel] THEN
   237     REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN
   238     hyp_subst_tac ctxt 1 THEN
   239     EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
   240       CONJ_WRAP' (fn thm =>
   241         (etac ctxt (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' assume_tac ctxt))
   242       set_maps] 1;
   243 
   244 fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong =
   245   let
   246     fun last_tac iffD =
   247       HEADGOAL (etac ctxt rel_mono_strong) THEN
   248       REPEAT_DETERM (HEADGOAL (etac ctxt (@{thm predicate2_transferD} RS iffD) THEN'
   249         REPEAT_DETERM o assume_tac ctxt));
   250   in
   251     REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
   252     (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
   253      REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
   254        @{thms exE conjE CollectE}))) THEN
   255      HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN
   256      last_tac iffD1 THEN last_tac iffD2)
   257   end;
   258 
   259 fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
   260   let
   261     val n = length set_maps;
   262     val in_tac = if n = 0 then rtac ctxt UNIV_I else
   263       rtac ctxt CollectI THEN' CONJ_WRAP' (fn thm =>
   264         etac ctxt (thm RS
   265           @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
   266       set_maps;
   267   in
   268     REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
   269     unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
   270     HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
   271       REPEAT_DETERM_N n o assume_tac ctxt,
   272       rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
   273       REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt,
   274       rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
   275       rtac ctxt conjI,
   276       EVERY' (map (fn convol =>
   277         rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
   278         REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong)) @{thms fst_convol snd_convol})])
   279   end;
   280 
   281 fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
   282   bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
   283   if live = 0 then
   284     rtac ctxt @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
   285       ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
   286   else
   287     let
   288       val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
   289       val inserts =
   290         map (fn set_bd =>
   291           iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
   292             [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
   293         set_bds;
   294     in
   295       EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt @{thm cprod_cinfinite_bound},
   296         rtac ctxt (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac ctxt @{thm card_of_Card_order},
   297         rtac ctxt @{thm ordLeq_csum2}, rtac ctxt @{thm Card_order_ctwo}, rtac ctxt @{thm Card_order_csum},
   298         rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm cexp_cong1},
   299         if live = 1 then rtac ctxt @{thm ordIso_refl[OF Card_order_csum]}
   300         else
   301           REPEAT_DETERM_N (live - 2) o rtac ctxt @{thm ordIso_transitive[OF csum_cong2]} THEN'
   302           REPEAT_DETERM_N (live - 1) o rtac ctxt @{thm csum_csum},
   303         rtac ctxt bd_Card_order, rtac ctxt (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac ctxt @{thm ordLeq_csum1},
   304         rtac ctxt bd_Card_order, rtac ctxt @{thm Card_order_csum}, rtac ctxt bd_Cnotzero,
   305         rtac ctxt @{thm csum_Cfinite_cexp_Cinfinite},
   306         rtac ctxt (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}),
   307         CONJ_WRAP_GEN' (rtac ctxt @{thm Cfinite_csum}) (K (rtac ctxt @{thm Cfinite_cone})) set_maps,
   308         rtac ctxt bd'_Cinfinite, rtac ctxt @{thm card_of_Card_order},
   309         rtac ctxt @{thm Card_order_cexp}, rtac ctxt @{thm Cinfinite_cexp}, rtac ctxt @{thm ordLeq_csum2},
   310         rtac ctxt @{thm Card_order_ctwo}, rtac ctxt bd'_Cinfinite,
   311         rtac ctxt (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))),
   312         REPEAT_DETERM_N (live - 1) o
   313           (rtac ctxt (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN'
   314            rtac ctxt @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}),
   315         rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
   316       unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
   317       unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
   318       EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
   319         Method.insert_tac inserts, REPEAT_DETERM o dtac ctxt meta_spec,
   320         REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
   321         if live = 1 then K all_tac
   322         else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
   323         rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
   324         CONJ_WRAP_GEN' (rtac ctxt @{thm SigmaI})
   325           (K (etac ctxt @{thm If_the_inv_into_in_Func} THEN' assume_tac ctxt)) set_maps,
   326         rtac ctxt sym,
   327         rtac ctxt (Drule.rotate_prems 1
   328            ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
   329              map_comp RS sym, map_id]) RSN (2, trans))),
   330         REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
   331         REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
   332         rtac ctxt refl,
   333         rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
   334         REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
   335         CONJ_WRAP' (fn thm =>
   336           rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]})
   337         set_maps,
   338         rtac ctxt sym,
   339         rtac ctxt (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
   340            map_comp RS sym, map_id])] 1
   341   end;
   342 
   343 fun mk_trivial_wit_tac ctxt wit_defs set_maps =
   344   unfold_thms_tac ctxt wit_defs THEN
   345   HEADGOAL (EVERY' (map (fn thm =>
   346     dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN
   347   ALLGOALS (assume_tac ctxt);
   348 
   349 fun mk_set_transfer_tac ctxt in_rel set_maps =
   350   Goal.conjunction_tac 1 THEN
   351   EVERY (map (fn set_map => HEADGOAL (rtac ctxt rel_funI) THEN
   352   REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
   353     @{thms exE conjE CollectE}))) THEN
   354   HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
   355     rtac ctxt @{thm rel_setI}) THEN
   356   REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
   357     REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
   358     rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
   359 
   360 fun mk_rel_cong_tac ctxt (eqs, prems) mono =
   361   let
   362     fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
   363     fun mk_tacs iffD = etac ctxt mono :: 
   364       map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
   365         |> Drule.rotate_prems ~1 |> mk_tac) prems;
   366   in
   367     unfold_thms_tac ctxt eqs THEN
   368     HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
   369   end;
   370 
   371 end;