--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:53 2014 +0200
@@ -705,26 +705,20 @@
fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
ctor_rels =
- let
- val rel_funD = @{thm rel_funD};
- fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
- val rel_funD_n_rotated = rotate_prems ~1 oo rel_funD_n;
- in
- CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
- unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
- HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
- etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN'
- EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
- etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN'
- rtac (rel_funD_n_rotated 2 @{thm comp_transfer}) THEN'
- rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
- REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
- REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
- rtac @{thm rel_funI} THEN'
- etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
- (ctor_rec_defs ~~ ctor_fold_transfers)
- end;
+ CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
+ HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
+ etac (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
+ etac (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
+ rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
+ rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
+ rtac rel_funI THEN'
+ etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
+ (ctor_rec_defs ~~ ctor_fold_transfers);
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
let val n = length ks;
@@ -754,7 +748,7 @@
[REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
SELECT_GOAL (unfold_thms_tac ctxt folds),
etac @{thm predicate2D_vimage2p},
- rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
atac])