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