--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Jul 05 22:47:48 2016 +0200
@@ -64,11 +64,11 @@
fun mk_in_mono_tac ctxt n =
if n = 0 then rtac ctxt subset_UNIV 1
else
- (rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN
- REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN
+ (rtac ctxt @{thm subsetI} THEN' rtac ctxt @{thm CollectI}) 1 THEN
+ REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN
REPEAT_DETERM_N (n - 1)
- ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
- (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
+ ((rtac ctxt conjI THEN' etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1) THEN
+ (etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1;
fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
let
@@ -109,13 +109,12 @@
resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1
else
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
- REPEAT_DETERM o eresolve_tac ctxt
- [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
rtac ctxt map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
etac ctxt @{thm set_mp}, assume_tac ctxt],
- rtac ctxt CollectI,
+ rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
etac ctxt @{thm set_mp}, assume_tac ctxt])
@@ -127,8 +126,8 @@
EVERY' [rtac ctxt @{thm GrpI},
rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong),
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
- rtac ctxt CollectI,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
+ rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm =>
EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
@@ -141,7 +140,8 @@
rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
(if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl
else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
- rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, rtac ctxt subsetI, rtac ctxt CollectI,
+ rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV,
+ rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI},
CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;
fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
@@ -156,10 +156,10 @@
Goal.conjunction_tac 1 THEN
unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
- resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
+ resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
- resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
+ resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
@@ -187,11 +187,11 @@
else
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
REPEAT_DETERM o
- eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans,
rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm,
- rtac ctxt (map_comp RS sym), rtac ctxt CollectI,
+ rtac ctxt (map_comp RS sym), rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
@@ -204,7 +204,7 @@
fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
let
val n = length set_maps;
- fun in_tac nthO_in = rtac ctxt CollectI THEN'
+ fun in_tac nthO_in = rtac ctxt @{thm CollectI} THEN'
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
@@ -215,8 +215,7 @@
if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1
else
EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
- REPEAT_DETERM o
- eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
hyp_subst_tac ctxt,
rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
@@ -224,7 +223,7 @@
in_tac @{thm fstOp_in},
rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
- rtac ctxt ballE, rtac ctxt subst,
+ rtac ctxt @{thm ballE}, rtac ctxt subst,
rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
in_tac @{thm fstOp_in},
@@ -241,7 +240,7 @@
if null set_maps then assume_tac ctxt 1
else
unfold_tac ctxt [in_rel] THEN
- REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN
+ REPEAT_DETERM (eresolve_tac ctxt @{thms exE CollectE conjE} 1) THEN
hyp_subst_tac ctxt 1 THEN
EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
CONJ_WRAP' (fn thm =>
@@ -266,18 +265,20 @@
fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
let
val n = length set_maps;
- val in_tac = if n = 0 then rtac ctxt UNIV_I else
- rtac ctxt CollectI THEN' CONJ_WRAP' (fn thm =>
- etac ctxt (thm RS
- @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
- set_maps;
+ val in_tac =
+ if n = 0 then rtac ctxt @{thm UNIV_I}
+ else
+ rtac ctxt @{thm CollectI} THEN' CONJ_WRAP' (fn thm =>
+ etac ctxt (thm RS
+ @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
+ set_maps;
in
REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
- REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms exE CollectE conjE}, hyp_subst_tac ctxt,
rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
rtac ctxt conjI,
EVERY' (map (fn convol =>
@@ -322,9 +323,11 @@
rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
- EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
+ EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst,
+ rtac ctxt @{thm subsetI},
Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
- REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
+ REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1],
+ etac ctxt @{thm CollectE},
if live = 1 then K all_tac
else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
@@ -337,8 +340,10 @@
REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
rtac ctxt refl,
- rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
- REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
+ rtac ctxt @{thm surj_imp_ordLeq},
+ rtac ctxt @{thm subsetI},
+ rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
+ REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
CONJ_WRAP' (fn thm =>
rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]})
set_maps,
@@ -350,7 +355,8 @@
fun mk_trivial_wit_tac ctxt wit_defs set_maps =
unfold_thms_tac ctxt wit_defs THEN
HEADGOAL (EVERY' (map (fn thm =>
- dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN
+ dtac ctxt (thm RS @{thm equalityD1} RS set_mp) THEN'
+ etac ctxt @{thm imageE} THEN' assume_tac ctxt) set_maps)) THEN
ALLGOALS (assume_tac ctxt);
fun mk_set_transfer_tac ctxt in_rel set_maps =
@@ -360,9 +366,10 @@
@{thms exE conjE CollectE}))) THEN
HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
rtac ctxt @{thm rel_setI}) THEN
- REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
+ REPEAT (HEADGOAL (etac ctxt @{thm imageE} THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
- rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
+ rtac ctxt @{thm bexI} THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt @{thm imageI})))
+ set_maps);
fun mk_rel_cong_tac ctxt (eqs, prems) mono =
let
@@ -391,7 +398,7 @@
fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
- REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
(etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]);