src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
changeset 49504 df9b897fb254
parent 49501 acc9635a644a
child 49506 aeb0cc8889f2
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4      {prems: 'a, context: Proof.context} -> tactic
     1.5    val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
     1.6      {prems: 'a, context: Proof.context} -> tactic
     1.7 -  val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
     1.8    val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
     1.9      thm list list -> tactic
    1.10    val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
    1.11 @@ -69,8 +68,6 @@
    1.12      thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    1.13      thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    1.14      {prems: 'a, context: Proof.context} -> tactic
    1.15 -  val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    1.16 -    thm list -> tactic
    1.17    val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    1.18    val mk_mor_elim_tac: thm -> tactic
    1.19    val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
    1.20 @@ -85,6 +82,8 @@
    1.21      {prems: thm list, context: Proof.context} -> tactic
    1.22    val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
    1.23      {prems: 'a, context: Proof.context} -> tactic
    1.24 +  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    1.25 +    thm list -> tactic
    1.26    val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    1.27    val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
    1.28    val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
    1.29 @@ -115,6 +114,7 @@
    1.30    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    1.31      cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    1.32      thm list list -> thm list list -> thm -> thm list list -> tactic
    1.33 +  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
    1.34    val mk_unique_mor_tac: thm list -> thm -> tactic
    1.35    val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
    1.36      {prems: 'a, context: Proof.context} -> tactic
    1.37 @@ -345,7 +345,7 @@
    1.38  
    1.39  fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
    1.40    {context = ctxt, prems = _} =
    1.41 -  unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
    1.42 +  unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
    1.43    EVERY' [rtac conjI,
    1.44      CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
    1.45      CONJ_WRAP' (fn (coalg_in, morE) =>
    1.46 @@ -358,7 +358,7 @@
    1.47      val n = length in_monos;
    1.48      val ks = 1 upto n;
    1.49    in
    1.50 -    unfold_defs_tac ctxt [bis_def] THEN
    1.51 +    unfold_thms_tac ctxt [bis_def] THEN
    1.52      EVERY' [rtac conjI,
    1.53        CONJ_WRAP' (fn i =>
    1.54          EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
    1.55 @@ -421,7 +421,7 @@
    1.56            rtac conjI, etac @{thm Shift_prefCl},
    1.57            rtac conjI, rtac ballI,
    1.58              rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
    1.59 -            SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}),
    1.60 +            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
    1.61              etac bspec, etac @{thm ShiftD},
    1.62              CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
    1.63                dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
    1.64 @@ -445,7 +445,7 @@
    1.65              rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
    1.66              rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
    1.67    in
    1.68 -    unfold_defs_tac ctxt defs THEN
    1.69 +    unfold_thms_tac ctxt defs THEN
    1.70      CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
    1.71    end;
    1.72  
    1.73 @@ -598,7 +598,7 @@
    1.74      val m = length strT_hsets;
    1.75    in
    1.76      if m = 0 then atac 1
    1.77 -    else (unfold_defs_tac ctxt [isNode_def] THEN
    1.78 +    else (unfold_thms_tac ctxt [isNode_def] THEN
    1.79        EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
    1.80          rtac exI, rtac conjI, atac,
    1.81          CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
    1.82 @@ -987,7 +987,7 @@
    1.83                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    1.84              if n = 1 then K all_tac
    1.85              else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    1.86 -            SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl,
    1.87 +            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
    1.88              rtac refl])
    1.89          ks to_sbd_injs from_to_sbds)];
    1.90    in
    1.91 @@ -1044,7 +1044,7 @@
    1.92  
    1.93  fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
    1.94    {context = ctxt, prems = _} =
    1.95 -  unfold_defs_tac ctxt defs THEN
    1.96 +  unfold_thms_tac ctxt defs THEN
    1.97    EVERY' [rtac conjI,
    1.98      CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
    1.99      CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
   1.100 @@ -1056,21 +1056,21 @@
   1.101      (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
   1.102  
   1.103  fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
   1.104 -  unfold_defs_tac ctxt defs THEN
   1.105 +  unfold_thms_tac ctxt defs THEN
   1.106    EVERY' [rtac conjI,
   1.107      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
   1.108      CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
   1.109  
   1.110 -fun mk_mor_coiter_tac m mor_UNIV dtor_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
   1.111 +fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
   1.112    EVERY' [rtac iffD2, rtac mor_UNIV,
   1.113 -    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, coiter_def), (map_comp_id, map_cong))) =>
   1.114 +    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
   1.115        EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
   1.116 -        rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
   1.117 +        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
   1.118          rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
   1.119          rtac (o_apply RS trans RS sym), rtac map_cong,
   1.120          REPEAT_DETERM_N m o rtac refl,
   1.121 -        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)])
   1.122 -    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
   1.123 +        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
   1.124 +    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
   1.125  
   1.126  fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   1.127    sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
   1.128 @@ -1103,23 +1103,23 @@
   1.129        etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
   1.130    raw_coinds 1;
   1.131  
   1.132 -fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
   1.133 -  CONJ_WRAP' (fn (raw_coind, coiter_def) =>
   1.134 +fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
   1.135 +  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
   1.136      EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
   1.137 -      rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
   1.138 -      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
   1.139 +      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
   1.140 +      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
   1.141  
   1.142 -fun mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtors
   1.143 +fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
   1.144    {context = ctxt, prems = _} =
   1.145 -  unfold_defs_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   1.146 -    rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   1.147 +  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   1.148 +    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   1.149      EVERY' (map (fn thm =>
   1.150 -      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_dtors),
   1.151 +      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
   1.152      rtac sym, rtac @{thm id_apply}] 1;
   1.153  
   1.154 -fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
   1.155 -  unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   1.156 -    rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
   1.157 +fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
   1.158 +  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   1.159 +    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
   1.160      REPEAT_DETERM_N m o rtac refl,
   1.161      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
   1.162  
   1.163 @@ -1179,9 +1179,9 @@
   1.164      rtac impI, REPEAT_DETERM o etac conjE,
   1.165      CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
   1.166  
   1.167 -fun mk_map_tac m n cT coiter map_comp' map_cong =
   1.168 +fun mk_map_tac m n cT unfold map_comp' map_cong =
   1.169    EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
   1.170 -    rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
   1.171 +    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
   1.172      REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   1.173      REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
   1.174      rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
   1.175 @@ -1201,12 +1201,12 @@
   1.176      REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
   1.177      EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
   1.178  
   1.179 -fun mk_map_id_tac maps coiter_unique coiter_dtor =
   1.180 -  EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
   1.181 -    rtac coiter_dtor] 1;
   1.182 +fun mk_map_id_tac maps unfold_unique unfold_dtor =
   1.183 +  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
   1.184 +    rtac unfold_dtor] 1;
   1.185  
   1.186 -fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique =
   1.187 -  EVERY' [rtac coiter_unique,
   1.188 +fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
   1.189 +  EVERY' [rtac unfold_unique,
   1.190      EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
   1.191        EVERY' (map rtac
   1.192          ([@{thm o_assoc} RS trans,
   1.193 @@ -1255,9 +1255,9 @@
   1.194             rtac conjI, rtac refl, rtac refl]) ks]) 1
   1.195    end
   1.196  
   1.197 -fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
   1.198 -  rtac coiter_unique 1 THEN
   1.199 -  unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   1.200 +fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
   1.201 +  rtac unfold_unique 1 THEN
   1.202 +  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   1.203    ALLGOALS (etac sym);
   1.204  
   1.205  fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
   1.206 @@ -1266,11 +1266,11 @@
   1.207      val n = length map_simps;
   1.208    in
   1.209      EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   1.210 -      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s),
   1.211 +      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
   1.212        CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
   1.213        REPEAT_DETERM o rtac allI,
   1.214        CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
   1.215 -        [SELECT_GOAL (unfold_defs_tac ctxt
   1.216 +        [SELECT_GOAL (unfold_thms_tac ctxt
   1.217            (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
   1.218          rtac @{thm Un_cong}, rtac refl,
   1.219          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   1.220 @@ -1367,14 +1367,14 @@
   1.221  
   1.222  fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
   1.223    {context = ctxt, prems = _} =
   1.224 -  unfold_defs_tac ctxt [coalg_def] THEN
   1.225 +  unfold_thms_tac ctxt [coalg_def] THEN
   1.226    CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
   1.227      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.228        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.229        hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.230        EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
   1.231        pickWP_assms_tac,
   1.232 -      SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
   1.233 +      SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
   1.234        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.235        rtac CollectI,
   1.236        REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
   1.237 @@ -1389,16 +1389,16 @@
   1.238    let
   1.239      val n = length map_comps;
   1.240    in
   1.241 -    unfold_defs_tac ctxt [mor_def] THEN
   1.242 +    unfold_thms_tac ctxt [mor_def] THEN
   1.243      EVERY' [rtac conjI,
   1.244        CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
   1.245        CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
   1.246          EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.247            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   1.248            hyp_subst_tac,
   1.249 -          SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}),
   1.250 +          SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
   1.251            rtac (map_comp RS trans),
   1.252 -          SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})),
   1.253 +          SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
   1.254            rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
   1.255            pickWP_assms_tac])
   1.256        (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
   1.257 @@ -1407,17 +1407,17 @@
   1.258  val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
   1.259  val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
   1.260  
   1.261 -fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
   1.262 -  unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
   1.263 -  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
   1.264 -  CONJ_WRAP' (fn (coiter, map_comp) =>
   1.265 +fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
   1.266 +  unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
   1.267 +  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
   1.268 +  CONJ_WRAP' (fn (unfold, map_comp) =>
   1.269      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   1.270        hyp_subst_tac,
   1.271 -      SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
   1.272 +      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
   1.273        rtac refl])
   1.274 -  (coiters ~~ map_comps) 1;
   1.275 +  (unfolds ~~ map_comps) 1;
   1.276  
   1.277 -fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs
   1.278 +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
   1.279    {context = ctxt, prems = _} =
   1.280    let
   1.281      val n = length rec_0s;
   1.282 @@ -1428,7 +1428,7 @@
   1.283        CONJ_WRAP' (fn thm => EVERY'
   1.284          [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
   1.285        REPEAT_DETERM o rtac allI,
   1.286 -      CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
   1.287 +      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
   1.288          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.289            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.290            hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.291 @@ -1437,16 +1437,16 @@
   1.292            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.293            rtac ord_eq_le_trans, rtac rec_Suc,
   1.294            rtac @{thm Un_least},
   1.295 -          SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1),
   1.296 +          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
   1.297              @{thm prod.cases}]),
   1.298            etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
   1.299            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
   1.300              EVERY' [rtac @{thm UN_least},
   1.301 -              SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
   1.302 +              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
   1.303                etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
   1.304                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
   1.305            (ks ~~ rev (drop m set_naturals))])
   1.306 -      (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   1.307 +      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   1.308    end;
   1.309  
   1.310  fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   1.311 @@ -1477,7 +1477,7 @@
   1.312    ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   1.313    REPEAT_DETERM (atac 1 ORELSE
   1.314      EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
   1.315 -    K (unfold_defs_tac ctxt dtor_ctors),
   1.316 +    K (unfold_thms_tac ctxt dtor_ctors),
   1.317      REPEAT_DETERM_N n o etac UnE,
   1.318      REPEAT_DETERM o
   1.319        (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
   1.320 @@ -1485,11 +1485,11 @@
   1.321          (dresolve_tac wit THEN'
   1.322            (etac FalseE ORELSE'
   1.323            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
   1.324 -            K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   1.325 +            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   1.326  
   1.327 -fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
   1.328 +fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   1.329    rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
   1.330 -  unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
   1.331 +  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   1.332    ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
   1.333    ALLGOALS (TRY o
   1.334      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])