renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
authorblanchet
Fri Sep 21 15:53:29 2012 +0200 (2012-09-21)
changeset 49504df9b897fb254
parent 49503 dbbde075a42e
child 49505 a944eefb67e6
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_def_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_tactics.ML
src/HOL/Codatatype/Tools/bnf_util.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
     1.3 @@ -242,9 +242,9 @@
     1.4                   rel_converse_of_bnf outer RS sym], outer_rel_Gr],
     1.5                 trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
     1.6                   (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
     1.7 -          |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
     1.8 +          |> unfold_thms lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
     1.9        in
    1.10 -        unfold_defs_tac lthy basic_thms THEN rtac thm 1
    1.11 +        unfold_thms_tac lthy basic_thms THEN rtac thm 1
    1.12        end;
    1.13  
    1.14      val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
    1.15 @@ -316,7 +316,7 @@
    1.16  
    1.17      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.18      fun map_comp_tac {context, ...} =
    1.19 -      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.20 +      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.21        rtac refl 1;
    1.22      fun map_cong_tac {context, ...} =
    1.23        mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
    1.24 @@ -352,7 +352,7 @@
    1.25                trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
    1.26                  (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
    1.27                   replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
    1.28 -          |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
    1.29 +          |> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
    1.30        in
    1.31          rtac thm 1
    1.32        end;
    1.33 @@ -410,7 +410,7 @@
    1.34  
    1.35      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.36      fun map_comp_tac {context, ...} =
    1.37 -      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.38 +      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.39        rtac refl 1;
    1.40      fun map_cong_tac {context, ...} =
    1.41        rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
    1.42 @@ -615,10 +615,10 @@
    1.43        set_unfoldss);
    1.44      val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
    1.45        pred_unfolds);
    1.46 -    val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
    1.47 -    val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
    1.48 -    val unfold_preds = unfold_defs lthy pred_unfolds;
    1.49 -    val unfold_rels = unfold_defs lthy rel_unfolds;
    1.50 +    val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
    1.51 +    val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
    1.52 +    val unfold_preds = unfold_thms lthy pred_unfolds;
    1.53 +    val unfold_rels = unfold_thms lthy rel_unfolds;
    1.54      val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
    1.55      val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
    1.56      val bnf_sets = map (expand_maps o expand_sets)
    1.57 @@ -665,7 +665,7 @@
    1.58        (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
    1.59        (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
    1.60        (mk_tac (map_wpull_of_bnf bnf))
    1.61 -      (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
    1.62 +      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
    1.63  
    1.64      val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    1.65  
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     2.3 @@ -64,8 +64,8 @@
     2.4  (* Composition *)
     2.5  
     2.6  fun mk_comp_set_alt_tac ctxt collect_set_natural =
     2.7 -  unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN
     2.8 -  unfold_defs_tac ctxt [collect_set_natural RS sym] THEN
     2.9 +  unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
    2.10 +  unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
    2.11    rtac refl 1;
    2.12  
    2.13  fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
    2.14 @@ -138,9 +138,9 @@
    2.15        rtac bd;
    2.16      fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
    2.17    in
    2.18 -    unfold_defs_tac ctxt [comp_set_alt] THEN
    2.19 +    unfold_thms_tac ctxt [comp_set_alt] THEN
    2.20      rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
    2.21 -    unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
    2.22 +    unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
    2.23      (rtac ctrans THEN'
    2.24       WRAP' gen_before gen_after bds (rtac last_bd) THEN'
    2.25       rtac @{thm ordIso_imp_ordLeq} THEN'
    2.26 @@ -152,12 +152,12 @@
    2.27    conj_assoc};
    2.28  
    2.29  fun mk_comp_in_alt_tac ctxt comp_set_alts =
    2.30 -  unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
    2.31 -  unfold_defs_tac ctxt @{thms set_eq_subset} THEN
    2.32 +  unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
    2.33 +  unfold_thms_tac ctxt @{thms set_eq_subset} THEN
    2.34    rtac conjI 1 THEN
    2.35    REPEAT_DETERM (
    2.36      rtac @{thm subsetI} 1 THEN
    2.37 -    unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
    2.38 +    unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
    2.39      (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
    2.40       REPEAT_DETERM (CHANGED ((
    2.41         (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
    2.42 @@ -214,7 +214,7 @@
    2.43  
    2.44  fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
    2.45    ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
    2.46 -  unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
    2.47 +  unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
    2.48    REPEAT_DETERM (
    2.49      atac 1 ORELSE
    2.50      REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
    2.51 @@ -408,7 +408,7 @@
    2.52    TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
    2.53  
    2.54  fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
    2.55 -  rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
    2.56 +  rtac (unfold_thms ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
    2.57      1;
    2.58  
    2.59  fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
     3.3 @@ -1180,7 +1180,7 @@
     3.4    let
     3.5      val wits_tac =
     3.6        K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
     3.7 -      mk_unfold_defs_then_tac lthy one_step_defs wit_tac;
     3.8 +      mk_unfold_thms_then_tac lthy one_step_defs wit_tac;
     3.9      val wit_goals = map mk_conjunction_balanced' wit_goalss;
    3.10      val wit_thms =
    3.11        Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
    3.12 @@ -1189,7 +1189,7 @@
    3.13        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
    3.14    in
    3.15      map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
    3.16 -      goals (map (mk_unfold_defs_then_tac lthy one_step_defs) tacs)
    3.17 +      goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
    3.18      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    3.19    end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
    3.20  
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     4.3 @@ -69,8 +69,8 @@
     4.4      val n = length set_naturals;
     4.5    in
     4.6      if null set_naturals then
     4.7 -      unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
     4.8 -    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
     4.9 +      unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
    4.10 +    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
    4.11        EVERY' [rtac equalityI, rtac subsetI,
    4.12          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
    4.13          REPEAT_DETERM o dtac Pair_eqD,
    4.14 @@ -105,7 +105,7 @@
    4.15    end;
    4.16  
    4.17  fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
    4.18 -  unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
    4.19 +  unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
    4.20    subst_tac ctxt [map_id] 1 THEN
    4.21      (if n = 0 then rtac refl 1
    4.22      else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
    4.23 @@ -113,7 +113,7 @@
    4.24        CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
    4.25  
    4.26  fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
    4.27 -  unfold_defs_tac ctxt rel_O_Grs THEN
    4.28 +  unfold_thms_tac ctxt rel_O_Grs THEN
    4.29      EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
    4.30        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
    4.31        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
    4.32 @@ -124,8 +124,8 @@
    4.33      val n = length set_naturals;
    4.34    in
    4.35      if null set_naturals then
    4.36 -      unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
    4.37 -    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
    4.38 +      unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
    4.39 +    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
    4.40        EVERY' [rtac @{thm subrelI},
    4.41          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
    4.42          REPEAT_DETERM o dtac Pair_eqD,
    4.43 @@ -151,8 +151,8 @@
    4.44          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    4.45            rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
    4.46    in
    4.47 -    if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
    4.48 -    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
    4.49 +    if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
    4.50 +    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
    4.51        EVERY' [rtac equalityI, rtac @{thm subrelI},
    4.52          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
    4.53          REPEAT_DETERM o dtac Pair_eqD,
    4.54 @@ -197,7 +197,7 @@
    4.55    let
    4.56      val ls' = replicate (Int.max (1, m)) ();
    4.57    in
    4.58 -    unfold_defs_tac ctxt (rel_O_Grs @
    4.59 +    unfold_thms_tac ctxt (rel_O_Grs @
    4.60        @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
    4.61      EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
    4.62        rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
     5.3 @@ -18,32 +18,30 @@
     5.4    val caseN: string
     5.5    val coN: string
     5.6    val coinductN: string
     5.7 -  val coiterN: string
     5.8 -  val coitersN: string
     5.9    val corecN: string
    5.10    val corecsN: string
    5.11    val ctorN: string
    5.12    val ctor_dtorN: string
    5.13 -  val ctor_dtor_coitersN: string
    5.14 +  val ctor_dtor_unfoldsN: string
    5.15    val ctor_dtor_corecsN: string
    5.16    val ctor_exhaustN: string
    5.17    val ctor_induct2N: string
    5.18    val ctor_inductN: string
    5.19    val ctor_injectN: string
    5.20 -  val ctor_iterN: string
    5.21 -  val ctor_iter_uniqueN: string
    5.22 -  val ctor_itersN: string
    5.23 +  val ctor_foldN: string
    5.24 +  val ctor_fold_uniqueN: string
    5.25 +  val ctor_foldsN: string
    5.26    val ctor_recN: string
    5.27    val ctor_recsN: string
    5.28 -  val disc_coiter_iffN: string
    5.29 -  val disc_coitersN: string
    5.30 +  val disc_unfold_iffN: string
    5.31 +  val disc_unfoldsN: string
    5.32    val disc_corec_iffN: string
    5.33    val disc_corecsN: string
    5.34    val dtorN: string
    5.35    val dtor_coinductN: string
    5.36 -  val dtor_coiterN: string
    5.37 -  val dtor_coiter_uniqueN: string
    5.38 -  val dtor_coitersN: string
    5.39 +  val dtor_unfoldN: string
    5.40 +  val dtor_unfold_uniqueN: string
    5.41 +  val dtor_unfoldsN: string
    5.42    val dtor_corecN: string
    5.43    val dtor_corecsN: string
    5.44    val dtor_exhaustN: string
    5.45 @@ -51,13 +49,13 @@
    5.46    val dtor_injectN: string
    5.47    val dtor_strong_coinductN: string
    5.48    val exhaustN: string
    5.49 +  val foldN: string
    5.50 +  val foldsN: string
    5.51    val hsetN: string
    5.52    val hset_recN: string
    5.53    val inductN: string
    5.54    val injectN: string
    5.55    val isNodeN: string
    5.56 -  val iterN: string
    5.57 -  val itersN: string
    5.58    val lsbisN: string
    5.59    val map_simpsN: string
    5.60    val map_uniqueN: string
    5.61 @@ -73,7 +71,7 @@
    5.62    val rel_simpN: string
    5.63    val rel_strong_coinductN: string
    5.64    val rvN: string
    5.65 -  val sel_coitersN: string
    5.66 +  val sel_unfoldsN: string
    5.67    val sel_corecsN: string
    5.68    val set_inclN: string
    5.69    val set_set_inclN: string
    5.70 @@ -83,6 +81,8 @@
    5.71    val strongN: string
    5.72    val sum_bdN: string
    5.73    val sum_bdTN: string
    5.74 +  val unfoldN: string
    5.75 +  val unfoldsN: string
    5.76    val uniqueN: string
    5.77  
    5.78    val mk_exhaustN: string -> string
    5.79 @@ -158,23 +158,24 @@
    5.80  val rawN = "raw_"
    5.81  
    5.82  val coN = "co"
    5.83 +val unN = "un"
    5.84  val algN = "alg"
    5.85  val IITN = "IITN"
    5.86 -val iterN = "iter"
    5.87 -val itersN = iterN ^ "s"
    5.88 -val coiterN = coN ^ iterN
    5.89 -val coitersN = coiterN ^ "s"
    5.90 +val foldN = "fold"
    5.91 +val foldsN = foldN ^ "s"
    5.92 +val unfoldN = unN ^ foldN
    5.93 +val unfoldsN = unfoldN ^ "s"
    5.94  val uniqueN = "_unique"
    5.95  val simpsN = "simps"
    5.96  val ctorN = "ctor"
    5.97  val dtorN = "dtor"
    5.98 -val ctor_iterN = ctorN ^ "_" ^ iterN
    5.99 -val ctor_itersN = ctor_iterN ^ "s"
   5.100 -val dtor_coiterN = dtorN ^ "_" ^ coiterN
   5.101 -val dtor_coitersN = dtor_coiterN ^ "s"
   5.102 -val ctor_iter_uniqueN = ctor_iterN ^ uniqueN
   5.103 -val dtor_coiter_uniqueN = dtor_coiterN ^ uniqueN
   5.104 -val ctor_dtor_coitersN = ctorN ^ "_" ^ dtor_coiterN ^ "s"
   5.105 +val ctor_foldN = ctorN ^ "_" ^ foldN
   5.106 +val ctor_foldsN = ctor_foldN ^ "s"
   5.107 +val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
   5.108 +val dtor_unfoldsN = dtor_unfoldN ^ "s"
   5.109 +val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
   5.110 +val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
   5.111 +val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
   5.112  val map_simpsN = mapN ^ "_" ^ simpsN
   5.113  val map_uniqueN = mapN ^ uniqueN
   5.114  val min_algN = "min_alg"
   5.115 @@ -237,13 +238,13 @@
   5.116  
   5.117  val caseN = "case"
   5.118  val discN = "disc"
   5.119 -val disc_coitersN = discN ^ "_" ^ coitersN
   5.120 +val disc_unfoldsN = discN ^ "_" ^ unfoldsN
   5.121  val disc_corecsN = discN ^ "_" ^ corecsN
   5.122  val iffN = "_iff"
   5.123 -val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN
   5.124 +val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
   5.125  val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
   5.126  val selN = "sel"
   5.127 -val sel_coitersN = selN ^ "_" ^ coitersN
   5.128 +val sel_unfoldsN = selN ^ "_" ^ unfoldsN
   5.129  val sel_corecsN = selN ^ "_" ^ corecsN
   5.130  
   5.131  val mk_common_name = space_implode "_";
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
     6.3 @@ -169,8 +169,8 @@
     6.4      val fp_eqs =
     6.5        map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
     6.6  
     6.7 -    val (pre_bnfs, ((dtors0, ctors0, fp_iters0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
     6.8 -           ctor_injects, fp_iter_thms, fp_rec_thms), lthy)) =
     6.9 +    val (pre_bnfs, ((dtors0, ctors0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
    6.10 +           ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
    6.11        fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    6.12  
    6.13      fun add_nesty_bnf_names Us =
    6.14 @@ -211,7 +211,7 @@
    6.15      val mss = map (map length) ctr_Tsss;
    6.16      val Css = map2 replicate ns Cs;
    6.17  
    6.18 -    fun mk_iter_like Ts Us t =
    6.19 +    fun mk_rec_like Ts Us t =
    6.20        let
    6.21          val (bindings, body) = strip_type (fastype_of t);
    6.22          val (f_Us, prebody) = split_last bindings;
    6.23 @@ -221,20 +221,20 @@
    6.24          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    6.25        end;
    6.26  
    6.27 -    val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0;
    6.28 -    val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0;
    6.29 +    val fp_folds as fp_fold1 :: _ = map (mk_rec_like As Cs) fp_folds0;
    6.30 +    val fp_recs as fp_rec1 :: _ = map (mk_rec_like As Cs) fp_recs0;
    6.31  
    6.32 -    val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
    6.33 +    val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
    6.34      val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
    6.35  
    6.36 -    val (((iter_only as (gss, _, _), rec_only as (hss, _, _)),
    6.37 -          (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
    6.38 +    val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
    6.39 +          (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
    6.40           names_lthy) =
    6.41        if lfp then
    6.42          let
    6.43            val y_Tsss =
    6.44              map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
    6.45 -              ns mss fp_iter_fun_Ts;
    6.46 +              ns mss fp_fold_fun_Ts;
    6.47            val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
    6.48  
    6.49            val ((gss, ysss), lthy) =
    6.50 @@ -287,7 +287,7 @@
    6.51                val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    6.52              in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
    6.53  
    6.54 -          val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
    6.55 +          val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
    6.56  
    6.57            val ((((Free (z, _), cs), pss), gssss), lthy) =
    6.58              lthy
    6.59 @@ -329,7 +329,7 @@
    6.60               (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
    6.61          end;
    6.62  
    6.63 -    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_iter), fp_rec),
    6.64 +    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
    6.65            ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
    6.66          disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
    6.67        let
    6.68 @@ -391,7 +391,7 @@
    6.69                end;
    6.70  
    6.71              val sumEN_thm' =
    6.72 -              unfold_defs lthy @{thms all_unit_eq}
    6.73 +              unfold_thms lthy @{thms all_unit_eq}
    6.74                  (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
    6.75                     (mk_sumEN_balanced n))
    6.76                |> Morphism.thm phi;
    6.77 @@ -413,25 +413,25 @@
    6.78  
    6.79          val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
    6.80  
    6.81 -        fun define_iter_rec (wrap_res, no_defs_lthy) =
    6.82 +        fun define_fold_rec (wrap_res, no_defs_lthy) =
    6.83            let
    6.84              val fpT_to_C = fpT --> C;
    6.85  
    6.86 -            fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
    6.87 +            fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xssss)) =
    6.88                let
    6.89                  val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
    6.90                  val binding = Binding.suffix_name ("_" ^ suf) fp_b;
    6.91                  val spec =
    6.92                    mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
    6.93 -                    Term.list_comb (fp_iter_like,
    6.94 +                    Term.list_comb (fp_rec_like,
    6.95                        map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
    6.96                in (binding, spec) end;
    6.97  
    6.98 -            val iter_like_infos =
    6.99 -              [(iterN, fp_iter, iter_only),
   6.100 +            val rec_like_infos =
   6.101 +              [(foldN, fp_fold, fold_only),
   6.102                 (recN, fp_rec, rec_only)];
   6.103  
   6.104 -            val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list;
   6.105 +            val (bindings, specs) = map generate_rec_like rec_like_infos |> split_list;
   6.106  
   6.107              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   6.108                |> apfst split_list o fold_map2 (fn b => fn spec =>
   6.109 @@ -441,14 +441,14 @@
   6.110  
   6.111              val phi = Proof_Context.export_morphism lthy lthy';
   6.112  
   6.113 -            val [iter_def, rec_def] = map (Morphism.thm phi) defs;
   6.114 +            val [fold_def, rec_def] = map (Morphism.thm phi) defs;
   6.115  
   6.116 -            val [iterx, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
   6.117 +            val [foldx, recx] = map (mk_rec_like As Cs o Morphism.term phi) csts;
   6.118            in
   6.119 -            ((wrap_res, ctrs, iterx, recx, xss, ctr_defs, iter_def, rec_def), lthy)
   6.120 +            ((wrap_res, ctrs, foldx, recx, xss, ctr_defs, fold_def, rec_def), lthy)
   6.121            end;
   6.122  
   6.123 -        fun define_coiter_corec (wrap_res, no_defs_lthy) =
   6.124 +        fun define_unfold_corec (wrap_res, no_defs_lthy) =
   6.125            let
   6.126              val B_to_fpT = C --> fpT;
   6.127  
   6.128 @@ -456,22 +456,22 @@
   6.129                Term.lambda c (mk_IfN sum_prod_T cps
   6.130                  (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
   6.131  
   6.132 -            fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts,
   6.133 +            fun generate_corec_like (suf, fp_rec_like, ((pfss, cqfsss), (f_sum_prod_Ts,
   6.134                  pf_Tss))) =
   6.135                let
   6.136                  val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
   6.137                  val binding = Binding.suffix_name ("_" ^ suf) fp_b;
   6.138                  val spec =
   6.139                    mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
   6.140 -                    Term.list_comb (fp_iter_like,
   6.141 +                    Term.list_comb (fp_rec_like,
   6.142                        map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
   6.143                in (binding, spec) end;
   6.144  
   6.145 -            val coiter_like_infos =
   6.146 -              [(coiterN, fp_iter, coiter_only),
   6.147 +            val corec_like_infos =
   6.148 +              [(unfoldN, fp_fold, unfold_only),
   6.149                 (corecN, fp_rec, corec_only)];
   6.150  
   6.151 -            val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list;
   6.152 +            val (bindings, specs) = map generate_corec_like corec_like_infos |> split_list;
   6.153  
   6.154              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   6.155                |> apfst split_list o fold_map2 (fn b => fn spec =>
   6.156 @@ -481,11 +481,11 @@
   6.157  
   6.158              val phi = Proof_Context.export_morphism lthy lthy';
   6.159  
   6.160 -            val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
   6.161 +            val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
   6.162  
   6.163 -            val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
   6.164 +            val [unfold, corec] = map (mk_rec_like As Cs o Morphism.term phi) csts;
   6.165            in
   6.166 -            ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
   6.167 +            ((wrap_res, ctrs, unfold, corec, xss, ctr_defs, unfold_def, corec_def), lthy)
   6.168            end;
   6.169  
   6.170          fun wrap lthy =
   6.171 @@ -494,9 +494,9 @@
   6.172                sel_defaultss))) lthy
   6.173            end;
   6.174  
   6.175 -        val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec;
   6.176 +        val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
   6.177        in
   6.178 -        ((wrap, define_iter_likes), lthy')
   6.179 +        ((wrap, define_rec_likes), lthy')
   6.180        end;
   6.181  
   6.182      val pre_map_defs = map map_def_of_bnf pre_bnfs;
   6.183 @@ -521,11 +521,11 @@
   6.184        in Term.list_comb (mapx, args) end;
   6.185  
   6.186      val mk_simp_thmss =
   6.187 -      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes =>
   6.188 -        injects @ distincts @ cases @ rec_likes @ iter_likes);
   6.189 +      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn rec_likes =>
   6.190 +        injects @ distincts @ cases @ rec_likes @ rec_likes);
   6.191  
   6.192 -    fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
   6.193 -        iter_defs, rec_defs), lthy) =
   6.194 +    fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, ctr_defss,
   6.195 +        fold_defs, rec_defs), lthy) =
   6.196        let
   6.197          val (((phis, phis'), us'), names_lthy) =
   6.198            lthy
   6.199 @@ -615,55 +615,55 @@
   6.200          (* TODO: Generate nicer names in case of clashes *)
   6.201          val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
   6.202  
   6.203 -        val (iter_thmss, rec_thmss) =
   6.204 +        val (fold_thmss, rec_thmss) =
   6.205            let
   6.206              val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
   6.207 -            val giters = map (lists_bmoc gss) iters;
   6.208 +            val gfolds = map (lists_bmoc gss) folds;
   6.209              val hrecs = map (lists_bmoc hss) recs;
   6.210  
   6.211 -            fun mk_goal fss fiter_like xctr f xs fxs =
   6.212 +            fun mk_goal fss frec_like xctr f xs fxs =
   6.213                fold_rev (fold_rev Logic.all) (xs :: fss)
   6.214 -                (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
   6.215 +                (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
   6.216  
   6.217 -            fun build_call fiter_likes maybe_tick (T, U) =
   6.218 +            fun build_call frec_likes maybe_tick (T, U) =
   6.219                if T = U then
   6.220                  id_const T
   6.221                else
   6.222                  (case find_index (curry (op =) T) fpTs of
   6.223 -                  ~1 => build_map (build_call fiter_likes maybe_tick) T U
   6.224 -                | j => maybe_tick (nth us j) (nth fiter_likes j));
   6.225 +                  ~1 => build_map (build_call frec_likes maybe_tick) T U
   6.226 +                | j => maybe_tick (nth us j) (nth frec_likes j));
   6.227  
   6.228              fun mk_U maybe_mk_prodT =
   6.229                typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
   6.230  
   6.231 -            fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
   6.232 +            fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
   6.233                if member (op =) fpTs T then
   6.234 -                maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
   6.235 +                maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
   6.236                else if exists_fp_subtype T then
   6.237 -                [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
   6.238 +                [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
   6.239                else
   6.240                  [x];
   6.241  
   6.242 -            val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss;
   6.243 +            val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
   6.244              val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
   6.245  
   6.246 -            val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss;
   6.247 +            val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
   6.248              val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
   6.249  
   6.250 -            val iter_tacss =
   6.251 -              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
   6.252 +            val fold_tacss =
   6.253 +              map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids fold_defs) fp_fold_thms
   6.254                  ctr_defss;
   6.255              val rec_tacss =
   6.256 -              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
   6.257 +              map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
   6.258                  ctr_defss;
   6.259  
   6.260              fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
   6.261            in
   6.262 -            (map2 (map2 prove) iter_goalss iter_tacss,
   6.263 +            (map2 (map2 prove) fold_goalss fold_tacss,
   6.264               map2 (map2 prove) rec_goalss rec_tacss)
   6.265            end;
   6.266  
   6.267 -        val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss;
   6.268 +        val simp_thmss = mk_simp_thmss wrap_ress rec_thmss fold_thmss;
   6.269  
   6.270          val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
   6.271          fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
   6.272 @@ -678,7 +678,7 @@
   6.273          val notes =
   6.274            [(inductN, map single induct_thms,
   6.275              fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
   6.276 -           (itersN, iter_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
   6.277 +           (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
   6.278             (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
   6.279             (simpsN, simp_thmss, K [])]
   6.280            |> maps (fn (thmN, thmss, attrs) =>
   6.281 @@ -689,8 +689,8 @@
   6.282          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   6.283        end;
   6.284  
   6.285 -    fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
   6.286 -        ctr_defss, coiter_defs, corec_defs), lthy) =
   6.287 +    fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _,
   6.288 +        ctr_defss, unfold_defs, corec_defs), lthy) =
   6.289        let
   6.290          val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
   6.291          val selsss = map #2 wrap_ress;
   6.292 @@ -714,79 +714,79 @@
   6.293          fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   6.294  
   6.295          val z = the_single zs;
   6.296 -        val gcoiters = map (lists_bmoc pgss) coiters;
   6.297 +        val gunfolds = map (lists_bmoc pgss) unfolds;
   6.298          val hcorecs = map (lists_bmoc phss) corecs;
   6.299  
   6.300 -        val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) =
   6.301 +        val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
   6.302            let
   6.303 -            fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' =
   6.304 +            fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
   6.305                fold_rev (fold_rev Logic.all) ([c] :: pfss)
   6.306                  (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   6.307 -                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
   6.308 +                   mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
   6.309  
   6.310 -            fun build_call fiter_likes maybe_tack (T, U) =
   6.311 +            fun build_call frec_likes maybe_tack (T, U) =
   6.312                if T = U then
   6.313                  id_const T
   6.314                else
   6.315                  (case find_index (curry (op =) U) fpTs of
   6.316 -                  ~1 => build_map (build_call fiter_likes maybe_tack) T U
   6.317 -                | j => maybe_tack (nth cs j, nth us j) (nth fiter_likes j));
   6.318 +                  ~1 => build_map (build_call frec_likes maybe_tack) T U
   6.319 +                | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
   6.320  
   6.321              fun mk_U maybe_mk_sumT =
   6.322                typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
   6.323  
   6.324 -            fun intr_calls fiter_likes maybe_mk_sumT maybe_tack cqf =
   6.325 +            fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
   6.326                let val T = fastype_of cqf in
   6.327                  if exists_subtype (member (op =) Cs) T then
   6.328 -                  build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
   6.329 +                  build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
   6.330                  else
   6.331                    cqf
   6.332                end;
   6.333  
   6.334 -            val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss;
   6.335 +            val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
   6.336              val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
   6.337  
   6.338 -            val coiter_goalss =
   6.339 -              map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
   6.340 +            val unfold_goalss =
   6.341 +              map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
   6.342              val corec_goalss =
   6.343                map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
   6.344  
   6.345 -            val coiter_tacss =
   6.346 -              map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
   6.347 +            val unfold_tacss =
   6.348 +              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
   6.349                  ctr_defss;
   6.350              val corec_tacss =
   6.351 -              map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
   6.352 +              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
   6.353                  ctr_defss;
   6.354  
   6.355              fun prove goal tac =
   6.356                Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
   6.357  
   6.358 -            val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss;
   6.359 +            val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   6.360              val corec_thmss =
   6.361                map2 (map2 prove) corec_goalss corec_tacss
   6.362 -              |> map (map (unfold_defs lthy @{thms sum_case_if}));
   6.363 +              |> map (map (unfold_thms lthy @{thms sum_case_if}));
   6.364  
   6.365 -            val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
   6.366 +            val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
   6.367              val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
   6.368  
   6.369              val filter_safesss =
   6.370                map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
   6.371                  curry (op ~~));
   6.372  
   6.373 -            val safe_coiter_thmss = filter_safesss coiter_safesss coiter_thmss;
   6.374 +            val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
   6.375              val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
   6.376            in
   6.377 -            (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
   6.378 +            (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
   6.379            end;
   6.380  
   6.381 -        val (disc_coiter_iff_thmss, disc_corec_iff_thmss) =
   6.382 +        val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
   6.383            let
   6.384 -            fun mk_goal c cps fcoiter_like n k disc =
   6.385 -              mk_Trueprop_eq (disc $ (fcoiter_like $ c),
   6.386 +            fun mk_goal c cps fcorec_like n k disc =
   6.387 +              mk_Trueprop_eq (disc $ (fcorec_like $ c),
   6.388                  if n = 1 then @{const True}
   6.389                  else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   6.390  
   6.391 -            val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss;
   6.392 +            val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
   6.393              val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
   6.394  
   6.395              fun mk_case_split' cp =
   6.396 @@ -794,10 +794,10 @@
   6.397  
   6.398              val case_splitss' = map (map mk_case_split') cpss;
   6.399  
   6.400 -            val coiter_tacss =
   6.401 -              map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss;
   6.402 +            val unfold_tacss =
   6.403 +              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
   6.404              val corec_tacss =
   6.405 -              map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
   6.406 +              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
   6.407  
   6.408              fun prove goal tac =
   6.409                Skip_Proof.prove lthy [] [] goal (tac o #context)
   6.410 @@ -807,17 +807,17 @@
   6.411              fun proves [_] [_] = []
   6.412                | proves goals tacs = map2 prove goals tacs;
   6.413            in
   6.414 -            (map2 proves coiter_goalss coiter_tacss,
   6.415 +            (map2 proves unfold_goalss unfold_tacss,
   6.416               map2 proves corec_goalss corec_tacss)
   6.417            end;
   6.418  
   6.419 -        fun mk_disc_coiter_like_thms coiter_likes discIs =
   6.420 -          map (op RS) (filter_out (is_triv_implies o snd) (coiter_likes ~~ discIs));
   6.421 +        fun mk_disc_corec_like_thms corec_likes discIs =
   6.422 +          map (op RS) (filter_out (is_triv_implies o snd) (corec_likes ~~ discIs));
   6.423  
   6.424 -        val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
   6.425 -        val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
   6.426 +        val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
   6.427 +        val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
   6.428  
   6.429 -        fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
   6.430 +        fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
   6.431            let
   6.432              val (domT, ranT) = dest_funT (fastype_of sel);
   6.433              val arg_cong' =
   6.434 @@ -826,25 +826,25 @@
   6.435                |> Thm.varifyT_global;
   6.436              val sel_thm' = sel_thm RSN (2, trans);
   6.437            in
   6.438 -            coiter_like_thm RS arg_cong' RS sel_thm'
   6.439 +            corec_like_thm RS arg_cong' RS sel_thm'
   6.440            end;
   6.441  
   6.442 -        fun mk_sel_coiter_like_thms coiter_likess =
   6.443 -          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_likess selsss sel_thmsss |> map flat;
   6.444 +        fun mk_sel_corec_like_thms corec_likess =
   6.445 +          map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
   6.446  
   6.447 -        val sel_coiter_thmss = mk_sel_coiter_like_thms coiter_thmss;
   6.448 -        val sel_corec_thmss = mk_sel_coiter_like_thms corec_thmss;
   6.449 +        val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
   6.450 +        val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
   6.451  
   6.452 -        fun zip_coiter_like_thms coiter_likes disc_coiter_likes sel_coiter_likes =
   6.453 -          coiter_likes @ disc_coiter_likes @ sel_coiter_likes;
   6.454 +        fun zip_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
   6.455 +          corec_likes @ disc_corec_likes @ sel_corec_likes;
   6.456  
   6.457          val simp_thmss =
   6.458            mk_simp_thmss wrap_ress
   6.459 -            (map3 zip_coiter_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
   6.460 -            (map3 zip_coiter_like_thms safe_coiter_thmss disc_coiter_thmss sel_coiter_thmss);
   6.461 +            (map3 zip_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
   6.462 +            (map3 zip_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
   6.463  
   6.464          val anonymous_notes =
   6.465 -          [(flat safe_coiter_thmss @ flat safe_corec_thmss, simp_attrs)]
   6.466 +          [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
   6.467            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   6.468  
   6.469          val common_notes =
   6.470 @@ -854,13 +854,13 @@
   6.471  
   6.472          val notes =
   6.473            [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
   6.474 -           (coitersN, coiter_thmss, []),
   6.475 +           (unfoldsN, unfold_thmss, []),
   6.476             (corecsN, corec_thmss, []),
   6.477 -           (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs),
   6.478 -           (disc_coitersN, disc_coiter_thmss, simp_attrs),
   6.479 +           (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
   6.480 +           (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
   6.481             (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
   6.482             (disc_corecsN, disc_corec_thmss, simp_attrs),
   6.483 -           (sel_coitersN, sel_coiter_thmss, simp_attrs),
   6.484 +           (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
   6.485             (sel_corecsN, sel_corec_thmss, simp_attrs),
   6.486             (simpsN, simp_thmss, [])]
   6.487            |> maps (fn (thmN, thmss, attrs) =>
   6.488 @@ -871,16 +871,16 @@
   6.489          lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
   6.490        end;
   6.491  
   6.492 -    fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
   6.493 -      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
   6.494 +    fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
   6.495 +      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
   6.496  
   6.497      val lthy' = lthy
   6.498 -      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_iters ~~
   6.499 +      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
   6.500          fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
   6.501          ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
   6.502 -      |>> split_list |> wrap_types_and_define_iter_likes
   6.503 -      |> (if lfp then derive_induct_iter_rec_thms_for_types
   6.504 -          else derive_coinduct_coiter_corec_thms_for_types);
   6.505 +      |>> split_list |> wrap_types_and_define_rec_likes
   6.506 +      |> (if lfp then derive_induct_fold_rec_thms_for_types
   6.507 +          else derive_coinduct_unfold_corec_thms_for_types);
   6.508  
   6.509      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   6.510        (if lfp then "" else "co") ^ "datatype"));
     7.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     7.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     7.3 @@ -8,16 +8,16 @@
     7.4  signature BNF_FP_SUGAR_TACTICS =
     7.5  sig
     7.6    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     7.7 -  val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
     7.8 +  val mk_corec_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
     7.9    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    7.10      tactic
    7.11 -  val mk_disc_coiter_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    7.12 +  val mk_disc_corec_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    7.13    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
    7.14    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
    7.15    val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
    7.16      thm -> thm list -> thm list list -> tactic
    7.17    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    7.18 -  val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    7.19 +  val mk_rec_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    7.20  end;
    7.21  
    7.22  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    7.23 @@ -44,14 +44,14 @@
    7.24  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
    7.25  
    7.26  fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor =
    7.27 -  unfold_defs_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
    7.28 +  unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
    7.29    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    7.30     REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
    7.31     rtac refl) 1;
    7.32  
    7.33  fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
    7.34 -  unfold_defs_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
    7.35 -  unfold_defs_tac ctxt @{thms all_prod_eq} THEN
    7.36 +  unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
    7.37 +  unfold_thms_tac ctxt @{thms all_prod_eq} THEN
    7.38    EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
    7.39      etac meta_mp, atac]) (1 upto n)) 1;
    7.40  
    7.41 @@ -59,41 +59,41 @@
    7.42    (rtac iffI THEN'
    7.43     EVERY' (map3 (fn cTs => fn cx => fn th =>
    7.44       dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    7.45 -     SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN'
    7.46 +     SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
    7.47       atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])) 1;
    7.48  
    7.49  fun mk_half_distinct_tac ctxt ctor_inject ctr_defs =
    7.50 -  unfold_defs_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
    7.51 +  unfold_thms_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
    7.52    rtac @{thm sum.distinct(1)} 1;
    7.53  
    7.54  fun mk_inject_tac ctxt ctr_def ctor_inject =
    7.55 -  unfold_defs_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
    7.56 -  unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    7.57 +  unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
    7.58 +  unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    7.59  
    7.60 -val iter_like_unfold_thms =
    7.61 +val rec_like_unfold_thms =
    7.62    @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
    7.63        split_conv};
    7.64  
    7.65 -fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs ctor_iter_like ctr_def ctxt =
    7.66 -  unfold_defs_tac ctxt (ctr_def :: ctor_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
    7.67 -    iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
    7.68 +fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt =
    7.69 +  unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @
    7.70 +    rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
    7.71  
    7.72 -val coiter_like_ss = ss_only @{thms if_True if_False};
    7.73 -val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
    7.74 +val corec_like_ss = ss_only @{thms if_True if_False};
    7.75 +val corec_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
    7.76  
    7.77 -fun mk_coiter_like_tac coiter_like_defs map_ids ctor_dtor_coiter_like pre_map_def ctr_def ctxt =
    7.78 -  unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
    7.79 -  subst_tac ctxt [ctor_dtor_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
    7.80 -  unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN
    7.81 -  unfold_defs_tac ctxt @{thms id_def} THEN
    7.82 +fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
    7.83 +  unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
    7.84 +  subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
    7.85 +  unfold_thms_tac ctxt (pre_map_def :: corec_like_unfold_thms @ map_ids) THEN
    7.86 +  unfold_thms_tac ctxt @{thms id_def} THEN
    7.87    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    7.88  
    7.89 -fun mk_disc_coiter_like_iff_tac case_splits' coiter_likes discs ctxt =
    7.90 -  EVERY (map3 (fn case_split_tac => fn coiter_like_thm => fn disc =>
    7.91 -      case_split_tac 1 THEN unfold_defs_tac ctxt [coiter_like_thm] THEN
    7.92 +fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =
    7.93 +  EVERY (map3 (fn case_split_tac => fn corec_like_thm => fn disc =>
    7.94 +      case_split_tac 1 THEN unfold_thms_tac ctxt [corec_like_thm] THEN
    7.95        asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN
    7.96        (if is_refl disc then all_tac else rtac disc 1))
    7.97 -    (map rtac case_splits' @ [K all_tac]) coiter_likes discs);
    7.98 +    (map rtac case_splits' @ [K all_tac]) corec_likes discs);
    7.99  
   7.100  val solve_prem_prem_tac =
   7.101    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
   7.102 @@ -107,7 +107,7 @@
   7.103  
   7.104  fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
   7.105    EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
   7.106 -     SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
   7.107 +     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
   7.108       solve_prem_prem_tac]) (rev kks)) 1;
   7.109  
   7.110  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
   7.111 @@ -125,7 +125,7 @@
   7.112      val nn = length ns;
   7.113      val n = Integer.sum ns;
   7.114    in
   7.115 -    unfold_defs_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   7.116 +    unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   7.117      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   7.118        pre_set_defss mss (unflat mss (1 upto n)) kkss)
   7.119    end;
     8.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
     8.3 @@ -1060,9 +1060,9 @@
     8.4  
     8.5            val sum_card_order = mk_sum_card_order bd_card_orders;
     8.6  
     8.7 -          val sbd_ordIso = fold_defs lthy [sbd_def]
     8.8 +          val sbd_ordIso = fold_thms lthy [sbd_def]
     8.9              (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
    8.10 -          val sbd_card_order =  fold_defs lthy [sbd_def]
    8.11 +          val sbd_card_order =  fold_thms lthy [sbd_def]
    8.12              (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
    8.13            val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
    8.14            val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
    8.15 @@ -1854,14 +1854,14 @@
    8.16      val sndsTs = map snd_const prodTs;
    8.17      val dtorTs = map2 (curry (op -->)) Ts FTs;
    8.18      val ctorTs = map2 (curry (op -->)) FTs Ts;
    8.19 -    val coiter_fTs = map2 (curry op -->) activeAs Ts;
    8.20 +    val unfold_fTs = map2 (curry op -->) activeAs Ts;
    8.21      val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
    8.22      val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
    8.23      val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev;
    8.24      val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
    8.25  
    8.26      val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs),
    8.27 -      FJzs), TRs), coiter_fs), coiter_fs_copy), corec_ss), phis), names_lthy) = names_lthy
    8.28 +      FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
    8.29        |> mk_Frees' "z" Ts
    8.30        ||>> mk_Frees' "z" Ts'
    8.31        ||>> mk_Frees "z" Ts
    8.32 @@ -1870,8 +1870,8 @@
    8.33        ||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
    8.34        ||>> mk_Frees "x" prodFTs
    8.35        ||>> mk_Frees "R" (map (mk_relT o `I) Ts)
    8.36 -      ||>> mk_Frees "f" coiter_fTs
    8.37 -      ||>> mk_Frees "g" coiter_fTs
    8.38 +      ||>> mk_Frees "f" unfold_fTs
    8.39 +      ||>> mk_Frees "g" unfold_fTs
    8.40        ||>> mk_Frees "s" corec_sTs
    8.41        ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
    8.42  
    8.43 @@ -1927,38 +1927,38 @@
    8.44  
    8.45      val timer = time (timer "dtor definitions & thms");
    8.46  
    8.47 -    fun coiter_bind i = Binding.suffix_name ("_" ^ dtor_coiterN) (nth bs (i - 1));
    8.48 -    val coiter_name = Binding.name_of o coiter_bind;
    8.49 -    val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind;
    8.50 -
    8.51 -    fun coiter_spec i T AT abs f z z' =
    8.52 +    fun unfold_bind i = Binding.suffix_name ("_" ^ dtor_unfoldN) (nth bs (i - 1));
    8.53 +    val unfold_name = Binding.name_of o unfold_bind;
    8.54 +    val unfold_def_bind = rpair [] o Thm.def_binding o unfold_bind;
    8.55 +
    8.56 +    fun unfold_spec i T AT abs f z z' =
    8.57        let
    8.58 -        val coiterT = Library.foldr (op -->) (sTs, AT --> T);
    8.59 -
    8.60 -        val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
    8.61 +        val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
    8.62 +
    8.63 +        val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
    8.64          val rhs = Term.absfree z' (abs $ (f $ z));
    8.65        in
    8.66          mk_Trueprop_eq (lhs, rhs)
    8.67        end;
    8.68  
    8.69 -    val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
    8.70 +    val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
    8.71        lthy
    8.72        |> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
    8.73          Specification.definition
    8.74 -          (SOME (coiter_bind i, NONE, NoSyn), (coiter_def_bind i, coiter_spec i T AT abs f z z')))
    8.75 +          (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
    8.76            ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
    8.77              (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
    8.78        |>> apsnd split_list o split_list
    8.79        ||> `Local_Theory.restore;
    8.80  
    8.81      val phi = Proof_Context.export_morphism lthy_old lthy;
    8.82 -    val coiters = map (Morphism.term phi) coiter_frees;
    8.83 -    val coiter_names = map (fst o dest_Const) coiters;
    8.84 -    fun mk_coiter Ts ss i = Term.list_comb (Const (nth coiter_names (i - 1), Library.foldr (op -->)
    8.85 +    val unfolds = map (Morphism.term phi) unfold_frees;
    8.86 +    val unfold_names = map (fst o dest_Const) unfolds;
    8.87 +    fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
    8.88        (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
    8.89 -    val coiter_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) coiter_def_frees;
    8.90 -
    8.91 -    val mor_coiter_thm =
    8.92 +    val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
    8.93 +
    8.94 +    val mor_unfold_thm =
    8.95        let
    8.96          val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
    8.97          val morEs' = map (fn thm =>
    8.98 @@ -1966,12 +1966,12 @@
    8.99        in
   8.100          Skip_Proof.prove lthy [] []
   8.101            (fold_rev Logic.all ss
   8.102 -            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_coiter Ts ss) ks))))
   8.103 -          (K (mk_mor_coiter_tac m mor_UNIV_thm dtor_defs coiter_defs Abs_inverses' morEs'
   8.104 +            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
   8.105 +          (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
   8.106              map_comp_id_thms map_congs))
   8.107          |> Thm.close_derivation
   8.108        end;
   8.109 -    val coiter_thms = map (fn thm => (thm OF [mor_coiter_thm, UNIV_I]) RS sym) morE_thms;
   8.110 +    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
   8.111  
   8.112      val (raw_coind_thms, raw_coind_thm) =
   8.113        let
   8.114 @@ -1990,15 +1990,15 @@
   8.115      val unique_mor_thms =
   8.116        let
   8.117          val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop
   8.118 -          (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors coiter_fs,
   8.119 -            mk_mor Bs ss UNIVs dtors coiter_fs_copy))];
   8.120 +          (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors unfold_fs,
   8.121 +            mk_mor Bs ss UNIVs dtors unfold_fs_copy))];
   8.122          fun mk_fun_eq B f g z = HOLogic.mk_imp
   8.123            (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z));
   8.124          val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   8.125 -          (map4 mk_fun_eq Bs coiter_fs coiter_fs_copy zs));
   8.126 +          (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs));
   8.127  
   8.128          val unique_mor = Skip_Proof.prove lthy [] []
   8.129 -          (fold_rev Logic.all (Bs @ ss @ coiter_fs @ coiter_fs_copy @ zs)
   8.130 +          (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs)
   8.131              (Logic.list_implies (prems, unique)))
   8.132            (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
   8.133            |> Thm.close_derivation;
   8.134 @@ -2006,38 +2006,38 @@
   8.135          map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
   8.136        end;
   8.137  
   8.138 -    val (coiter_unique_mor_thms, coiter_unique_mor_thm) =
   8.139 +    val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
   8.140        let
   8.141 -        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors coiter_fs);
   8.142 -        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_coiter Ts ss i);
   8.143 +        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
   8.144 +        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
   8.145          val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   8.146 -          (map2 mk_fun_eq coiter_fs ks));
   8.147 +          (map2 mk_fun_eq unfold_fs ks));
   8.148  
   8.149          val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
   8.150          val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
   8.151  
   8.152          val unique_mor = Skip_Proof.prove lthy [] []
   8.153 -          (fold_rev Logic.all (ss @ coiter_fs) (Logic.mk_implies (prem, unique)))
   8.154 -          (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs))
   8.155 +          (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
   8.156 +          (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
   8.157            |> Thm.close_derivation;
   8.158        in
   8.159          `split_conj_thm unique_mor
   8.160        end;
   8.161  
   8.162 -    val (coiter_unique_thms, coiter_unique_thm) = `split_conj_thm (split_conj_prems n
   8.163 -      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS coiter_unique_mor_thm));
   8.164 -
   8.165 -    val coiter_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) coiter_unique_mor_thms;
   8.166 -
   8.167 -    val coiter_o_dtor_thms =
   8.168 +    val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
   8.169 +      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm));
   8.170 +
   8.171 +    val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
   8.172 +
   8.173 +    val unfold_o_dtor_thms =
   8.174        let
   8.175 -        val mor = mor_comp_thm OF [mor_str_thm, mor_coiter_thm];
   8.176 +        val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm];
   8.177        in
   8.178 -        map2 (fn unique => fn coiter_ctor =>
   8.179 -          trans OF [mor RS unique, coiter_ctor]) coiter_unique_mor_thms coiter_dtor_thms
   8.180 +        map2 (fn unique => fn unfold_ctor =>
   8.181 +          trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms
   8.182        end;
   8.183  
   8.184 -    val timer = time (timer "coiter definitions & thms");
   8.185 +    val timer = time (timer "unfold definitions & thms");
   8.186  
   8.187      val map_dtors = map2 (fn Ds => fn bnf =>
   8.188        Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
   8.189 @@ -2050,7 +2050,7 @@
   8.190      fun ctor_spec i ctorT =
   8.191        let
   8.192          val lhs = Free (ctor_name i, ctorT);
   8.193 -        val rhs = mk_coiter Ts map_dtors i;
   8.194 +        val rhs = mk_unfold Ts map_dtors i;
   8.195        in
   8.196          mk_Trueprop_eq (lhs, rhs)
   8.197        end;
   8.198 @@ -2070,7 +2070,7 @@
   8.199      val ctors = mk_ctors params';
   8.200      val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
   8.201  
   8.202 -    val ctor_o_dtor_thms = map2 (fold_defs lthy o single) ctor_defs coiter_o_dtor_thms;
   8.203 +    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
   8.204  
   8.205      val dtor_o_ctor_thms =
   8.206        let
   8.207 @@ -2078,11 +2078,11 @@
   8.208           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
   8.209          val goals = map3 mk_goal dtors ctors FTs;
   8.210        in
   8.211 -        map5 (fn goal => fn ctor_def => fn coiter => fn map_comp_id => fn map_congL =>
   8.212 +        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
   8.213            Skip_Proof.prove lthy [] [] goal
   8.214 -            (mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtor_thms)
   8.215 +            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
   8.216            |> Thm.close_derivation)
   8.217 -          goals ctor_defs coiter_thms map_comp_id_thms map_congL_thms
   8.218 +          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
   8.219        end;
   8.220  
   8.221      val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
   8.222 @@ -2104,20 +2104,20 @@
   8.223      val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
   8.224      val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
   8.225  
   8.226 -    fun mk_ctor_dtor_coiter_like_thm dtor_inject dtor_ctor coiter =
   8.227 -      iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
   8.228 -
   8.229 -    val ctor_coiter_thms =
   8.230 -      map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms coiter_thms;
   8.231 +    fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold =
   8.232 +      iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]];
   8.233 +
   8.234 +    val ctor_dtor_unfold_thms =
   8.235 +      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms;
   8.236  
   8.237      val timer = time (timer "ctor definitions & thms");
   8.238  
   8.239      val corec_Inl_sum_thms =
   8.240        let
   8.241 -        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_coiter_thm];
   8.242 +        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
   8.243        in
   8.244 -        map2 (fn unique => fn coiter_dtor =>
   8.245 -          trans OF [mor RS unique, coiter_dtor]) coiter_unique_mor_thms coiter_dtor_thms
   8.246 +        map2 (fn unique => fn unfold_dtor =>
   8.247 +          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
   8.248        end;
   8.249  
   8.250      fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1));
   8.251 @@ -2132,7 +2132,7 @@
   8.252            dtors corec_ss corec_maps;
   8.253  
   8.254          val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
   8.255 -        val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
   8.256 +        val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT);
   8.257        in
   8.258          mk_Trueprop_eq (lhs, rhs)
   8.259        end;
   8.260 @@ -2155,7 +2155,7 @@
   8.261  
   8.262      val sum_cases =
   8.263        map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
   8.264 -    val corec_thms =
   8.265 +    val dtor_corec_thms =
   8.266        let
   8.267          fun mk_goal i corec_s corec_map dtor z =
   8.268            let
   8.269 @@ -2166,15 +2166,15 @@
   8.270            end;
   8.271          val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
   8.272        in
   8.273 -        map3 (fn goal => fn coiter => fn map_cong =>
   8.274 +        map3 (fn goal => fn unfold => fn map_cong =>
   8.275            Skip_Proof.prove lthy [] [] goal
   8.276 -            (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms)
   8.277 +            (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
   8.278            |> Thm.close_derivation)
   8.279 -        goals coiter_thms map_congs
   8.280 +        goals dtor_unfold_thms map_congs
   8.281        end;
   8.282  
   8.283 -    val ctor_corec_thms =
   8.284 -      map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms corec_thms;
   8.285 +    val ctor_dtor_corec_thms =
   8.286 +      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
   8.287  
   8.288      val timer = time (timer "corec definitions & thms");
   8.289  
   8.290 @@ -2216,7 +2216,7 @@
   8.291          val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
   8.292          val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
   8.293  
   8.294 -        val rel_coinduct = unfold_defs lthy @{thms diag_UNIV}
   8.295 +        val rel_coinduct = unfold_thms lthy @{thms diag_UNIV}
   8.296            (Skip_Proof.prove lthy [] [] rel_coinduct_goal
   8.297              (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
   8.298            |> Thm.close_derivation);
   8.299 @@ -2272,8 +2272,8 @@
   8.300          val pred_of_rel_thms =
   8.301            rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
   8.302  
   8.303 -        val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
   8.304 -        val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct;
   8.305 +        val pred_coinduct = unfold_thms lthy pred_of_rel_thms rel_coinduct;
   8.306 +        val pred_strong_coinduct = unfold_thms lthy pred_of_rel_thms rel_strong_coinduct;
   8.307        in
   8.308          (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct,
   8.309           dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
   8.310 @@ -2332,7 +2332,7 @@
   8.311            map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs;
   8.312          fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts);
   8.313          fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps =
   8.314 -          mk_coiter Ts' (map2 (fn dtor => fn Fmap =>
   8.315 +          mk_unfold Ts' (map2 (fn dtor => fn Fmap =>
   8.316              HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T));
   8.317          val mk_map_id = mk_map HOLogic.id_const I;
   8.318          val mk_mapsAB = mk_maps passiveAs passiveBs;
   8.319 @@ -2374,11 +2374,11 @@
   8.320              val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
   8.321              val cTs = map (SOME o certifyT lthy) FTs';
   8.322              val maps =
   8.323 -              map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
   8.324 +              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
   8.325                  Skip_Proof.prove lthy [] [] goal
   8.326 -                  (K (mk_map_tac m n cT coiter map_comp' map_cong))
   8.327 +                  (K (mk_map_tac m n cT unfold map_comp' map_cong))
   8.328                  |> Thm.close_derivation)
   8.329 -              goals cTs coiter_thms map_comp's map_congs;
   8.330 +              goals cTs dtor_unfold_thms map_comp's map_congs;
   8.331            in
   8.332              map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
   8.333            end;
   8.334 @@ -2392,7 +2392,7 @@
   8.335                  fs_maps gs_maps fgs_maps)))
   8.336            in
   8.337              split_conj_thm (Skip_Proof.prove lthy [] [] goal
   8.338 -              (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm))
   8.339 +              (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm))
   8.340                |> Thm.close_derivation)
   8.341            end;
   8.342  
   8.343 @@ -2408,7 +2408,7 @@
   8.344            in
   8.345              Skip_Proof.prove lthy [] []
   8.346                (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
   8.347 -              (mk_map_unique_tac coiter_unique_thm map_comps)
   8.348 +              (mk_map_unique_tac dtor_unfold_unique_thm map_comps)
   8.349                |> Thm.close_derivation
   8.350            end;
   8.351  
   8.352 @@ -2566,7 +2566,7 @@
   8.353            (map2 (curry (op $)) dtors Jzs) (map2 (curry (op $)) dtor's Jz's);
   8.354          val pickF_ss = map3 (fn pickF => fn z => fn z' =>
   8.355            HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's';
   8.356 -        val picks = map (mk_coiter XTs pickF_ss) ks;
   8.357 +        val picks = map (mk_unfold XTs pickF_ss) ks;
   8.358  
   8.359          val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   8.360            (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
   8.361 @@ -2613,7 +2613,7 @@
   8.362                map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
   8.363              Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
   8.364                map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
   8.365 -            Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def coiter_thms
   8.366 +            Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
   8.367                map_comp's) |> Thm.close_derivation)
   8.368            end;
   8.369  
   8.370 @@ -2637,8 +2637,8 @@
   8.371              val thms =
   8.372                map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
   8.373                  singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
   8.374 -                  (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
   8.375 -                    pickWP_assms_tacs))
   8.376 +                  (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss
   8.377 +                    map_wpull_thms pickWP_assms_tacs))
   8.378                  |> Thm.close_derivation)
   8.379                ls goals ctss hset_rec_0ss' hset_rec_Sucss';
   8.380            in
   8.381 @@ -2647,7 +2647,8 @@
   8.382  
   8.383          val timer = time (timer "helpers for BNF properties");
   8.384  
   8.385 -        val map_id_tacs = map2 (K oo mk_map_id_tac map_thms) coiter_unique_thms coiter_dtor_thms;
   8.386 +        val map_id_tacs =
   8.387 +          map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
   8.388          val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
   8.389          val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
   8.390          val set_nat_tacss =
   8.391 @@ -2716,7 +2717,7 @@
   8.392                map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
   8.393                  ((set_minimal
   8.394                    |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
   8.395 -                  |> unfold_defs lthy incls) OF
   8.396 +                  |> unfold_thms lthy incls) OF
   8.397                    (replicate n ballI @
   8.398                      maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
   8.399                  |> singleton (Proof_Context.export names_lthy lthy)
   8.400 @@ -2806,7 +2807,7 @@
   8.401            end;
   8.402  
   8.403          fun mk_coind_wits ((I, dummys), (args, thms)) =
   8.404 -          ((I, dummys), (map (fn i => mk_coiter Ts args i $ HOLogic.unit) ks, thms));
   8.405 +          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
   8.406  
   8.407          val coind_witss =
   8.408            maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
   8.409 @@ -2830,7 +2831,7 @@
   8.410            in
   8.411              map2 (fn goal => fn induct =>
   8.412                Skip_Proof.prove lthy [] [] goal
   8.413 -                (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms)
   8.414 +                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
   8.415                |> Thm.close_derivation)
   8.416              goals hset_induct_thms
   8.417              |> map split_conj_thm
   8.418 @@ -2867,10 +2868,10 @@
   8.419              |> register_bnf (Local_Theory.full_name lthy b))
   8.420            tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
   8.421  
   8.422 -        val fold_maps = fold_defs lthy (map (fn bnf =>
   8.423 +        val fold_maps = fold_thms lthy (map (fn bnf =>
   8.424            mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
   8.425  
   8.426 -        val fold_sets = fold_defs lthy (maps (fn bnf =>
   8.427 +        val fold_sets = fold_thms lthy (maps (fn bnf =>
   8.428           map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
   8.429  
   8.430          val timer = time (timer "registered new codatatypes as BNFs");
   8.431 @@ -2965,25 +2966,25 @@
   8.432            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   8.433  
   8.434        val notes =
   8.435 -        [(dtor_coitersN, coiter_thms),
   8.436 -        (dtor_coiter_uniqueN, coiter_unique_thms),
   8.437 -        (dtor_corecsN, corec_thms),
   8.438 +        [(ctor_dtorN, ctor_dtor_thms),
   8.439 +        (ctor_dtor_unfoldsN, ctor_dtor_unfold_thms),
   8.440 +        (ctor_dtor_corecsN, ctor_dtor_corec_thms),
   8.441 +        (ctor_exhaustN, ctor_exhaust_thms),
   8.442 +        (ctor_injectN, ctor_inject_thms),
   8.443 +        (dtor_corecsN, dtor_corec_thms),
   8.444          (dtor_ctorN, dtor_ctor_thms),
   8.445 -        (ctor_dtorN, ctor_dtor_thms),
   8.446 +        (dtor_exhaustN, dtor_exhaust_thms),
   8.447          (dtor_injectN, dtor_inject_thms),
   8.448 -        (dtor_exhaustN, dtor_exhaust_thms),
   8.449 -        (ctor_injectN, ctor_inject_thms),
   8.450 -        (ctor_exhaustN, ctor_exhaust_thms),
   8.451 -        (ctor_dtor_coitersN, ctor_coiter_thms),
   8.452 -        (ctor_dtor_corecsN, ctor_corec_thms)]
   8.453 +        (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
   8.454 +        (dtor_unfoldsN, dtor_unfold_thms)]
   8.455          |> map (apsnd (map single))
   8.456          |> maps (fn (thmN, thmss) =>
   8.457            map2 (fn b => fn thms =>
   8.458              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   8.459            bs thmss)
   8.460    in
   8.461 -    ((dtors, ctors, coiters, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
   8.462 -      ctor_inject_thms, ctor_coiter_thms, ctor_corec_thms),
   8.463 +    ((dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
   8.464 +      ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
   8.465       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   8.466    end;
   8.467  
     9.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     9.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
     9.3 @@ -30,7 +30,6 @@
     9.4      {prems: 'a, context: Proof.context} -> tactic
     9.5    val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
     9.6      {prems: 'a, context: Proof.context} -> tactic
     9.7 -  val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
     9.8    val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
     9.9      thm list list -> tactic
    9.10    val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
    9.11 @@ -69,8 +68,6 @@
    9.12      thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    9.13      thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    9.14      {prems: 'a, context: Proof.context} -> tactic
    9.15 -  val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    9.16 -    thm list -> tactic
    9.17    val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    9.18    val mk_mor_elim_tac: thm -> tactic
    9.19    val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
    9.20 @@ -85,6 +82,8 @@
    9.21      {prems: thm list, context: Proof.context} -> tactic
    9.22    val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
    9.23      {prems: 'a, context: Proof.context} -> tactic
    9.24 +  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    9.25 +    thm list -> tactic
    9.26    val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    9.27    val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
    9.28    val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
    9.29 @@ -115,6 +114,7 @@
    9.30    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    9.31      cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    9.32      thm list list -> thm list list -> thm -> thm list list -> tactic
    9.33 +  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
    9.34    val mk_unique_mor_tac: thm list -> thm -> tactic
    9.35    val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
    9.36      {prems: 'a, context: Proof.context} -> tactic
    9.37 @@ -345,7 +345,7 @@
    9.38  
    9.39  fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
    9.40    {context = ctxt, prems = _} =
    9.41 -  unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
    9.42 +  unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
    9.43    EVERY' [rtac conjI,
    9.44      CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
    9.45      CONJ_WRAP' (fn (coalg_in, morE) =>
    9.46 @@ -358,7 +358,7 @@
    9.47      val n = length in_monos;
    9.48      val ks = 1 upto n;
    9.49    in
    9.50 -    unfold_defs_tac ctxt [bis_def] THEN
    9.51 +    unfold_thms_tac ctxt [bis_def] THEN
    9.52      EVERY' [rtac conjI,
    9.53        CONJ_WRAP' (fn i =>
    9.54          EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
    9.55 @@ -421,7 +421,7 @@
    9.56            rtac conjI, etac @{thm Shift_prefCl},
    9.57            rtac conjI, rtac ballI,
    9.58              rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
    9.59 -            SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}),
    9.60 +            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
    9.61              etac bspec, etac @{thm ShiftD},
    9.62              CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
    9.63                dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
    9.64 @@ -445,7 +445,7 @@
    9.65              rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
    9.66              rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
    9.67    in
    9.68 -    unfold_defs_tac ctxt defs THEN
    9.69 +    unfold_thms_tac ctxt defs THEN
    9.70      CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
    9.71    end;
    9.72  
    9.73 @@ -598,7 +598,7 @@
    9.74      val m = length strT_hsets;
    9.75    in
    9.76      if m = 0 then atac 1
    9.77 -    else (unfold_defs_tac ctxt [isNode_def] THEN
    9.78 +    else (unfold_thms_tac ctxt [isNode_def] THEN
    9.79        EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
    9.80          rtac exI, rtac conjI, atac,
    9.81          CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
    9.82 @@ -987,7 +987,7 @@
    9.83                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    9.84              if n = 1 then K all_tac
    9.85              else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    9.86 -            SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl,
    9.87 +            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
    9.88              rtac refl])
    9.89          ks to_sbd_injs from_to_sbds)];
    9.90    in
    9.91 @@ -1044,7 +1044,7 @@
    9.92  
    9.93  fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
    9.94    {context = ctxt, prems = _} =
    9.95 -  unfold_defs_tac ctxt defs THEN
    9.96 +  unfold_thms_tac ctxt defs THEN
    9.97    EVERY' [rtac conjI,
    9.98      CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
    9.99      CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
   9.100 @@ -1056,21 +1056,21 @@
   9.101      (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
   9.102  
   9.103  fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
   9.104 -  unfold_defs_tac ctxt defs THEN
   9.105 +  unfold_thms_tac ctxt defs THEN
   9.106    EVERY' [rtac conjI,
   9.107      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
   9.108      CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
   9.109  
   9.110 -fun mk_mor_coiter_tac m mor_UNIV dtor_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
   9.111 +fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
   9.112    EVERY' [rtac iffD2, rtac mor_UNIV,
   9.113 -    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, coiter_def), (map_comp_id, map_cong))) =>
   9.114 +    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
   9.115        EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
   9.116 -        rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
   9.117 +        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
   9.118          rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
   9.119          rtac (o_apply RS trans RS sym), rtac map_cong,
   9.120          REPEAT_DETERM_N m o rtac refl,
   9.121 -        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)])
   9.122 -    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
   9.123 +        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
   9.124 +    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
   9.125  
   9.126  fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   9.127    sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
   9.128 @@ -1103,23 +1103,23 @@
   9.129        etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
   9.130    raw_coinds 1;
   9.131  
   9.132 -fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
   9.133 -  CONJ_WRAP' (fn (raw_coind, coiter_def) =>
   9.134 +fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
   9.135 +  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
   9.136      EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
   9.137 -      rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
   9.138 -      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
   9.139 +      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
   9.140 +      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
   9.141  
   9.142 -fun mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtors
   9.143 +fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
   9.144    {context = ctxt, prems = _} =
   9.145 -  unfold_defs_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   9.146 -    rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   9.147 +  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   9.148 +    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   9.149      EVERY' (map (fn thm =>
   9.150 -      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_dtors),
   9.151 +      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
   9.152      rtac sym, rtac @{thm id_apply}] 1;
   9.153  
   9.154 -fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
   9.155 -  unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   9.156 -    rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
   9.157 +fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
   9.158 +  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   9.159 +    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
   9.160      REPEAT_DETERM_N m o rtac refl,
   9.161      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
   9.162  
   9.163 @@ -1179,9 +1179,9 @@
   9.164      rtac impI, REPEAT_DETERM o etac conjE,
   9.165      CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
   9.166  
   9.167 -fun mk_map_tac m n cT coiter map_comp' map_cong =
   9.168 +fun mk_map_tac m n cT unfold map_comp' map_cong =
   9.169    EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
   9.170 -    rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
   9.171 +    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
   9.172      REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   9.173      REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
   9.174      rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
   9.175 @@ -1201,12 +1201,12 @@
   9.176      REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
   9.177      EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
   9.178  
   9.179 -fun mk_map_id_tac maps coiter_unique coiter_dtor =
   9.180 -  EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
   9.181 -    rtac coiter_dtor] 1;
   9.182 +fun mk_map_id_tac maps unfold_unique unfold_dtor =
   9.183 +  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
   9.184 +    rtac unfold_dtor] 1;
   9.185  
   9.186 -fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique =
   9.187 -  EVERY' [rtac coiter_unique,
   9.188 +fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
   9.189 +  EVERY' [rtac unfold_unique,
   9.190      EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
   9.191        EVERY' (map rtac
   9.192          ([@{thm o_assoc} RS trans,
   9.193 @@ -1255,9 +1255,9 @@
   9.194             rtac conjI, rtac refl, rtac refl]) ks]) 1
   9.195    end
   9.196  
   9.197 -fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
   9.198 -  rtac coiter_unique 1 THEN
   9.199 -  unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   9.200 +fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
   9.201 +  rtac unfold_unique 1 THEN
   9.202 +  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   9.203    ALLGOALS (etac sym);
   9.204  
   9.205  fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
   9.206 @@ -1266,11 +1266,11 @@
   9.207      val n = length map_simps;
   9.208    in
   9.209      EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   9.210 -      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s),
   9.211 +      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
   9.212        CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
   9.213        REPEAT_DETERM o rtac allI,
   9.214        CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
   9.215 -        [SELECT_GOAL (unfold_defs_tac ctxt
   9.216 +        [SELECT_GOAL (unfold_thms_tac ctxt
   9.217            (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
   9.218          rtac @{thm Un_cong}, rtac refl,
   9.219          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   9.220 @@ -1367,14 +1367,14 @@
   9.221  
   9.222  fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
   9.223    {context = ctxt, prems = _} =
   9.224 -  unfold_defs_tac ctxt [coalg_def] THEN
   9.225 +  unfold_thms_tac ctxt [coalg_def] THEN
   9.226    CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
   9.227      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   9.228        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   9.229        hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   9.230        EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
   9.231        pickWP_assms_tac,
   9.232 -      SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
   9.233 +      SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
   9.234        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   9.235        rtac CollectI,
   9.236        REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
   9.237 @@ -1389,16 +1389,16 @@
   9.238    let
   9.239      val n = length map_comps;
   9.240    in
   9.241 -    unfold_defs_tac ctxt [mor_def] THEN
   9.242 +    unfold_thms_tac ctxt [mor_def] THEN
   9.243      EVERY' [rtac conjI,
   9.244        CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
   9.245        CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
   9.246          EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   9.247            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   9.248            hyp_subst_tac,
   9.249 -          SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}),
   9.250 +          SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
   9.251            rtac (map_comp RS trans),
   9.252 -          SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})),
   9.253 +          SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
   9.254            rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
   9.255            pickWP_assms_tac])
   9.256        (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
   9.257 @@ -1407,17 +1407,17 @@
   9.258  val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
   9.259  val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
   9.260  
   9.261 -fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
   9.262 -  unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
   9.263 -  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
   9.264 -  CONJ_WRAP' (fn (coiter, map_comp) =>
   9.265 +fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
   9.266 +  unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
   9.267 +  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
   9.268 +  CONJ_WRAP' (fn (unfold, map_comp) =>
   9.269      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   9.270        hyp_subst_tac,
   9.271 -      SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
   9.272 +      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
   9.273        rtac refl])
   9.274 -  (coiters ~~ map_comps) 1;
   9.275 +  (unfolds ~~ map_comps) 1;
   9.276  
   9.277 -fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs
   9.278 +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
   9.279    {context = ctxt, prems = _} =
   9.280    let
   9.281      val n = length rec_0s;
   9.282 @@ -1428,7 +1428,7 @@
   9.283        CONJ_WRAP' (fn thm => EVERY'
   9.284          [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
   9.285        REPEAT_DETERM o rtac allI,
   9.286 -      CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
   9.287 +      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
   9.288          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   9.289            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   9.290            hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   9.291 @@ -1437,16 +1437,16 @@
   9.292            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   9.293            rtac ord_eq_le_trans, rtac rec_Suc,
   9.294            rtac @{thm Un_least},
   9.295 -          SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1),
   9.296 +          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
   9.297              @{thm prod.cases}]),
   9.298            etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
   9.299            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
   9.300              EVERY' [rtac @{thm UN_least},
   9.301 -              SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
   9.302 +              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
   9.303                etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
   9.304                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
   9.305            (ks ~~ rev (drop m set_naturals))])
   9.306 -      (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   9.307 +      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   9.308    end;
   9.309  
   9.310  fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   9.311 @@ -1477,7 +1477,7 @@
   9.312    ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   9.313    REPEAT_DETERM (atac 1 ORELSE
   9.314      EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
   9.315 -    K (unfold_defs_tac ctxt dtor_ctors),
   9.316 +    K (unfold_thms_tac ctxt dtor_ctors),
   9.317      REPEAT_DETERM_N n o etac UnE,
   9.318      REPEAT_DETERM o
   9.319        (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
   9.320 @@ -1485,11 +1485,11 @@
   9.321          (dresolve_tac wit THEN'
   9.322            (etac FalseE ORELSE'
   9.323            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
   9.324 -            K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   9.325 +            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   9.326  
   9.327 -fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
   9.328 +fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   9.329    rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
   9.330 -  unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
   9.331 +  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   9.332    ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
   9.333    ALLGOALS (TRY o
   9.334      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
    10.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
    10.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
    10.3 @@ -973,20 +973,20 @@
    10.4      val map_FT_inits = map2 (fn Ds =>
    10.5        mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
    10.6      val fTs = map2 (curry op -->) Ts activeAs;
    10.7 -    val iterT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
    10.8 +    val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
    10.9      val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
   10.10      val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
   10.11      val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
   10.12      val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
   10.13  
   10.14      val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
   10.15 -      (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
   10.16 +      (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
   10.17        |> mk_Frees' "z1" Ts
   10.18        ||>> mk_Frees' "z2" Ts'
   10.19        ||>> mk_Frees' "x" FTs
   10.20        ||>> mk_Frees "y" FTs'
   10.21        ||>> mk_Freess' "z" setFTss
   10.22 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
   10.23 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT
   10.24        ||>> mk_Frees "f" fTs
   10.25        ||>> mk_Frees "s" rec_sTs;
   10.26  
   10.27 @@ -1049,90 +1049,90 @@
   10.28  
   10.29      val timer = time (timer "ctor definitions & thms");
   10.30  
   10.31 -    val iter_fun = Term.absfree iter_f'
   10.32 -      (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks));
   10.33 -    val iterx = HOLogic.choice_const iterT $ iter_fun;
   10.34 +    val fold_fun = Term.absfree fold_f'
   10.35 +      (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
   10.36 +    val foldx = HOLogic.choice_const foldT $ fold_fun;
   10.37  
   10.38 -    fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1));
   10.39 -    val iter_name = Binding.name_of o iter_bind;
   10.40 -    val iter_def_bind = rpair [] o Thm.def_binding o iter_bind;
   10.41 +    fun fold_bind i = Binding.suffix_name ("_" ^ ctor_foldN) (nth bs (i - 1));
   10.42 +    val fold_name = Binding.name_of o fold_bind;
   10.43 +    val fold_def_bind = rpair [] o Thm.def_binding o fold_bind;
   10.44  
   10.45 -    fun iter_spec i T AT =
   10.46 +    fun fold_spec i T AT =
   10.47        let
   10.48 -        val iterT = Library.foldr (op -->) (sTs, T --> AT);
   10.49 +        val foldT = Library.foldr (op -->) (sTs, T --> AT);
   10.50  
   10.51 -        val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
   10.52 -        val rhs = mk_nthN n iterx i;
   10.53 +        val lhs = Term.list_comb (Free (fold_name i, foldT), ss);
   10.54 +        val rhs = mk_nthN n foldx i;
   10.55        in
   10.56          mk_Trueprop_eq (lhs, rhs)
   10.57        end;
   10.58  
   10.59 -    val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
   10.60 +    val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
   10.61        lthy
   10.62        |> fold_map3 (fn i => fn T => fn AT =>
   10.63          Specification.definition
   10.64 -          (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
   10.65 +          (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT)))
   10.66            ks Ts activeAs
   10.67        |>> apsnd split_list o split_list
   10.68        ||> `Local_Theory.restore;
   10.69  
   10.70      val phi = Proof_Context.export_morphism lthy_old lthy;
   10.71 -    val iters = map (Morphism.term phi) iter_frees;
   10.72 -    val iter_names = map (fst o dest_Const) iters;
   10.73 -    fun mk_iter Ts ss i = Term.list_comb (Const (nth iter_names (i - 1), Library.foldr (op -->)
   10.74 +    val folds = map (Morphism.term phi) fold_frees;
   10.75 +    val fold_names = map (fst o dest_Const) folds;
   10.76 +    fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
   10.77        (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
   10.78 -    val iter_defs = map (Morphism.thm phi) iter_def_frees;
   10.79 +    val fold_defs = map (Morphism.thm phi) fold_def_frees;
   10.80  
   10.81 -    val mor_iter_thm =
   10.82 +    val mor_fold_thm =
   10.83        let
   10.84          val ex_mor = talg_thm RS init_ex_mor_thm;
   10.85          val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
   10.86          val mor_comp = mor_Rep_thm RS mor_comp_thm;
   10.87 -        val cT = certifyT lthy iterT;
   10.88 -        val ct = certify lthy iter_fun
   10.89 +        val cT = certifyT lthy foldT;
   10.90 +        val ct = certify lthy fold_fun
   10.91        in
   10.92          singleton (Proof_Context.export names_lthy lthy)
   10.93            (Skip_Proof.prove lthy [] []
   10.94 -            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_iter Ts ss) ks)))
   10.95 -            (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
   10.96 +            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
   10.97 +            (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
   10.98          |> Thm.close_derivation
   10.99        end;
  10.100  
  10.101 -    val iter_thms = map (fn morE => rule_by_tactic lthy
  10.102 +    val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
  10.103        ((rtac CollectI THEN' CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n)) 1)
  10.104 -      (mor_iter_thm RS morE)) morE_thms;
  10.105 +      (mor_fold_thm RS morE)) morE_thms;
  10.106  
  10.107 -    val (iter_unique_mor_thms, iter_unique_mor_thm) =
  10.108 +    val (fold_unique_mor_thms, fold_unique_mor_thm) =
  10.109        let
  10.110          val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
  10.111 -        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_iter Ts ss i);
  10.112 +        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
  10.113          val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
  10.114          val unique_mor = Skip_Proof.prove lthy [] []
  10.115            (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
  10.116 -          (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps
  10.117 -            mor_comp_thm mor_Abs_thm mor_iter_thm))
  10.118 +          (K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
  10.119 +            mor_comp_thm mor_Abs_thm mor_fold_thm))
  10.120            |> Thm.close_derivation;
  10.121        in
  10.122          `split_conj_thm unique_mor
  10.123        end;
  10.124  
  10.125 -    val iter_unique_thms =
  10.126 +    val ctor_fold_unique_thms =
  10.127        split_conj_thm (mk_conjIN n RS
  10.128 -        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
  10.129 +        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm))
  10.130  
  10.131 -    val iter_ctor_thms =
  10.132 +    val fold_ctor_thms =
  10.133        map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
  10.134 -        iter_unique_mor_thms;
  10.135 +        fold_unique_mor_thms;
  10.136  
  10.137 -    val ctor_o_iter_thms =
  10.138 +    val ctor_o_fold_thms =
  10.139        let
  10.140 -        val mor = mor_comp_thm OF [mor_iter_thm, mor_str_thm];
  10.141 +        val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm];
  10.142        in
  10.143 -        map2 (fn unique => fn iter_ctor =>
  10.144 -          trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
  10.145 +        map2 (fn unique => fn fold_ctor =>
  10.146 +          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
  10.147        end;
  10.148  
  10.149 -    val timer = time (timer "iter definitions & thms");
  10.150 +    val timer = time (timer "fold definitions & thms");
  10.151  
  10.152      val map_ctors = map2 (fn Ds => fn bnf =>
  10.153        Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
  10.154 @@ -1147,7 +1147,7 @@
  10.155          val dtorT = T --> FT;
  10.156  
  10.157          val lhs = Free (dtor_name i, dtorT);
  10.158 -        val rhs = mk_iter Ts map_ctors i;
  10.159 +        val rhs = mk_fold Ts map_ctors i;
  10.160        in
  10.161          mk_Trueprop_eq (lhs, rhs)
  10.162        end;
  10.163 @@ -1167,7 +1167,7 @@
  10.164      val dtors = mk_dtors params';
  10.165      val dtor_defs = map (Morphism.thm phi) dtor_def_frees;
  10.166  
  10.167 -    val ctor_o_dtor_thms = map2 (fold_defs lthy o single) dtor_defs ctor_o_iter_thms;
  10.168 +    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
  10.169  
  10.170      val dtor_o_ctor_thms =
  10.171        let
  10.172 @@ -1175,11 +1175,11 @@
  10.173            mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
  10.174          val goals = map3 mk_goal dtors ctors FTs;
  10.175        in
  10.176 -        map5 (fn goal => fn dtor_def => fn iterx => fn map_comp_id => fn map_congL =>
  10.177 +        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
  10.178            Skip_Proof.prove lthy [] [] goal
  10.179 -            (K (mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iter_thms))
  10.180 +            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
  10.181            |> Thm.close_derivation)
  10.182 -        goals dtor_defs iter_thms map_comp_id_thms map_congL_thms
  10.183 +        goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
  10.184        end;
  10.185  
  10.186      val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
  10.187 @@ -1205,10 +1205,10 @@
  10.188  
  10.189      val fst_rec_pair_thms =
  10.190        let
  10.191 -        val mor = mor_comp_thm OF [mor_iter_thm, mor_convol_thm];
  10.192 +        val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
  10.193        in
  10.194 -        map2 (fn unique => fn iter_ctor =>
  10.195 -          trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
  10.196 +        map2 (fn unique => fn fold_ctor =>
  10.197 +          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
  10.198        end;
  10.199  
  10.200      fun rec_bind i = Binding.suffix_name ("_" ^ ctor_recN) (nth bs (i - 1));
  10.201 @@ -1223,7 +1223,7 @@
  10.202            ctors rec_ss rec_maps;
  10.203  
  10.204          val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
  10.205 -        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
  10.206 +        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts maps i);
  10.207        in
  10.208          mk_Trueprop_eq (lhs, rhs)
  10.209        end;
  10.210 @@ -1245,7 +1245,7 @@
  10.211      val rec_defs = map (Morphism.thm phi) rec_def_frees;
  10.212  
  10.213      val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
  10.214 -    val rec_thms =
  10.215 +    val ctor_rec_thms =
  10.216        let
  10.217          fun mk_goal i rec_s rec_map ctor x =
  10.218            let
  10.219 @@ -1256,10 +1256,10 @@
  10.220            end;
  10.221          val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
  10.222        in
  10.223 -        map2 (fn goal => fn iterx =>
  10.224 -          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iterx fst_rec_pair_thms)
  10.225 +        map2 (fn goal => fn foldx =>
  10.226 +          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
  10.227            |> Thm.close_derivation)
  10.228 -        goals iter_thms
  10.229 +        goals ctor_fold_thms
  10.230        end;
  10.231  
  10.232      val timer = time (timer "rec definitions & thms");
  10.233 @@ -1381,10 +1381,10 @@
  10.234            mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  10.235          fun mk_passive_maps ATs BTs Ts =
  10.236            map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs;
  10.237 -        fun mk_map_iter_arg fs Ts ctor fmap =
  10.238 +        fun mk_map_fold_arg fs Ts ctor fmap =
  10.239            HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts));
  10.240          fun mk_map Ts fs Ts' ctors mk_maps =
  10.241 -          mk_iter Ts (map2 (mk_map_iter_arg fs Ts') ctors (mk_maps Ts'));
  10.242 +          mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts'));
  10.243          val pmapsABT' = mk_passive_maps passiveAs passiveBs;
  10.244          val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks;
  10.245          val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks;
  10.246 @@ -1401,10 +1401,10 @@
  10.247                  HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
  10.248              val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
  10.249              val maps =
  10.250 -              map4 (fn goal => fn iterx => fn map_comp_id => fn map_cong =>
  10.251 -                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iterx map_comp_id map_cong))
  10.252 +              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
  10.253 +                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
  10.254                  |> Thm.close_derivation)
  10.255 -              goals iter_thms map_comp_id_thms map_congs;
  10.256 +              goals ctor_fold_thms map_comp_id_thms map_congs;
  10.257            in
  10.258              map (fn thm => thm RS @{thm pointfreeE}) maps
  10.259            end;
  10.260 @@ -1420,7 +1420,7 @@
  10.261                  (map2 (curry HOLogic.mk_eq) us fs_maps));
  10.262              val unique = Skip_Proof.prove lthy [] []
  10.263                (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
  10.264 -              (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
  10.265 +              (K (mk_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
  10.266                |> Thm.close_derivation;
  10.267            in
  10.268              `split_conj_thm unique
  10.269 @@ -1451,7 +1451,7 @@
  10.270            end;
  10.271  
  10.272          val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
  10.273 -        val setss_by_range = map (fn cols => map (mk_iter Ts cols) ks) colss;
  10.274 +        val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
  10.275          val setss_by_bnf = transpose setss_by_range;
  10.276  
  10.277          val set_simp_thmss =
  10.278 @@ -1461,9 +1461,9 @@
  10.279                  HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
  10.280              val goalss =
  10.281                map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
  10.282 -            val setss = map (map2 (fn iterx => fn goal =>
  10.283 -              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iterx)) |> Thm.close_derivation)
  10.284 -              iter_thms) goalss;
  10.285 +            val setss = map (map2 (fn foldx => fn goal =>
  10.286 +              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
  10.287 +              ctor_fold_thms) goalss;
  10.288  
  10.289              fun mk_simp_goal pas_set act_sets sets ctor z set =
  10.290                Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
  10.291 @@ -1712,11 +1712,11 @@
  10.292              |> register_bnf (Local_Theory.full_name lthy b))
  10.293            tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
  10.294  
  10.295 -        val fold_maps = fold_defs lthy (map (fn bnf =>
  10.296 +        val fold_maps = fold_thms lthy (map (fn bnf =>
  10.297            mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
  10.298  
  10.299 -        val fold_sets = fold_defs lthy (maps (fn bnf =>
  10.300 -         map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
  10.301 +        val fold_sets = fold_thms lthy (maps (fn bnf =>
  10.302 +          map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
  10.303  
  10.304          val timer = time (timer "registered new datatypes as BNFs");
  10.305  
  10.306 @@ -1806,10 +1806,10 @@
  10.307        val notes =
  10.308          [(ctor_dtorN, ctor_dtor_thms),
  10.309          (ctor_exhaustN, ctor_exhaust_thms),
  10.310 +        (ctor_fold_uniqueN, ctor_fold_unique_thms),
  10.311 +        (ctor_foldsN, ctor_fold_thms),
  10.312          (ctor_injectN, ctor_inject_thms),
  10.313 -        (ctor_iter_uniqueN, iter_unique_thms),
  10.314 -        (ctor_itersN, iter_thms),
  10.315 -        (ctor_recsN, rec_thms),
  10.316 +        (ctor_recsN, ctor_rec_thms),
  10.317          (dtor_ctorN, dtor_ctor_thms),
  10.318          (dtor_exhaustN, dtor_exhaust_thms),
  10.319          (dtor_injectN, dtor_inject_thms)]
  10.320 @@ -1819,8 +1819,8 @@
  10.321              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
  10.322            bs thmss)
  10.323    in
  10.324 -    ((dtors, ctors, iters, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
  10.325 -      iter_thms, rec_thms),
  10.326 +    ((dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
  10.327 +      ctor_fold_thms, ctor_rec_thms),
  10.328       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
  10.329    end;
  10.330  
    11.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    11.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    11.3 @@ -32,7 +32,7 @@
    11.4    val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    11.5      thm list -> tactic
    11.6    val mk_iso_alt_tac: thm list -> thm -> tactic
    11.7 -  val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    11.8 +  val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    11.9    val mk_least_min_alg_tac: thm -> thm -> tactic
   11.10    val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
   11.11      thm list list list -> thm list -> tactic
   11.12 @@ -56,7 +56,7 @@
   11.13    val mk_mor_elim_tac: thm -> tactic
   11.14    val mk_mor_incl_tac: thm -> thm list -> tactic
   11.15    val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
   11.16 -  val mk_mor_iter_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
   11.17 +  val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
   11.18    val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
   11.19      thm list -> tactic
   11.20    val mk_mor_str_tac: 'a list -> thm -> tactic
   11.21 @@ -386,7 +386,7 @@
   11.22  
   11.23  fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
   11.24    EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
   11.25 -  unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
   11.26 +  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
   11.27  
   11.28  fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
   11.29      alg_sets set_natural's str_init_defs =
   11.30 @@ -431,7 +431,7 @@
   11.31      rtac mor_select THEN' atac THEN' rtac CollectI THEN'
   11.32      REPEAT_DETERM o rtac exI THEN'
   11.33      rtac conjI THEN' rtac refl THEN' atac THEN'
   11.34 -    K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
   11.35 +    K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
   11.36      etac mor_comp THEN' etac mor_incl_min_alg) 1
   11.37    end;
   11.38  
   11.39 @@ -486,7 +486,7 @@
   11.40    end;
   11.41  
   11.42  fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
   11.43 -  (K (unfold_defs_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   11.44 +  (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   11.45    EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   11.46    EVERY' (map rtac inver_Abss) THEN'
   11.47    EVERY' (map rtac inver_Reps)) 1;
   11.48 @@ -497,34 +497,34 @@
   11.49      EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs])
   11.50      inver_Abss inver_Reps)) 1;
   11.51  
   11.52 -fun mk_mor_iter_tac cT ct iter_defs ex_mor mor =
   11.53 -  (EVERY' (map stac iter_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
   11.54 -  REPEAT_DETERM_N (length iter_defs) o etac exE THEN'
   11.55 +fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
   11.56 +  (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
   11.57 +  REPEAT_DETERM_N (length fold_defs) o etac exE THEN'
   11.58    rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
   11.59  
   11.60 -fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter =
   11.61 +fun mk_fold_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
   11.62    let
   11.63      fun mk_unique type_def =
   11.64        EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
   11.65          rtac ballI, resolve_tac init_unique_mors,
   11.66          EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
   11.67          rtac mor_comp, rtac mor_Abs, atac,
   11.68 -        rtac mor_comp, rtac mor_Abs, rtac mor_iter];
   11.69 +        rtac mor_comp, rtac mor_Abs, rtac mor_fold];
   11.70    in
   11.71      CONJ_WRAP' mk_unique type_defs 1
   11.72    end;
   11.73  
   11.74 -fun mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iters =
   11.75 -  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx,
   11.76 +fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
   11.77 +  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
   11.78      rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
   11.79      EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
   11.80 -      ctor_o_iters),
   11.81 +      ctor_o_folds),
   11.82      rtac sym, rtac id_apply] 1;
   11.83  
   11.84 -fun mk_rec_tac rec_defs iterx fst_recs {context = ctxt, prems = _}=
   11.85 -  unfold_defs_tac ctxt
   11.86 +fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
   11.87 +  unfold_thms_tac ctxt
   11.88      (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   11.89 -  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iterx RS @{thm arg_cong[of _ _ snd]}),
   11.90 +  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
   11.91      rtac @{thm snd_convol'}] 1;
   11.92  
   11.93  fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   11.94 @@ -570,14 +570,14 @@
   11.95        CONJ_WRAP' (K atac) ks] 1
   11.96    end;
   11.97  
   11.98 -fun mk_map_tac m n iterx map_comp_id map_cong =
   11.99 -  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac o_apply,
  11.100 +fun mk_map_tac m n foldx map_comp_id map_cong =
  11.101 +  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
  11.102      rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
  11.103      REPEAT_DETERM_N m o rtac refl,
  11.104      REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
  11.105      rtac sym, rtac o_apply] 1;
  11.106  
  11.107 -fun mk_map_unique_tac m mor_def iter_unique_mor map_comp_ids map_congs =
  11.108 +fun mk_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
  11.109    let
  11.110      val n = length map_congs;
  11.111      fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
  11.112 @@ -586,13 +586,13 @@
  11.113        REPEAT_DETERM_N m o rtac refl,
  11.114        REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
  11.115    in
  11.116 -    EVERY' [rtac iter_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
  11.117 +    EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
  11.118        CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
  11.119        CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
  11.120    end;
  11.121  
  11.122 -fun mk_set_tac iterx = EVERY' [rtac ext, rtac trans, rtac o_apply,
  11.123 -  rtac trans, rtac iterx, rtac sym, rtac o_apply] 1;
  11.124 +fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
  11.125 +  rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
  11.126  
  11.127  fun mk_set_simp_tac set set_natural' set_natural's =
  11.128    let
    12.1 --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    12.2 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    12.3 @@ -16,8 +16,8 @@
    12.4    val subst_asm_tac: Proof.context -> thm list -> int -> tactic
    12.5    val subst_tac: Proof.context -> thm list -> int -> tactic
    12.6    val substs_tac: Proof.context -> thm list -> int -> tactic
    12.7 -  val unfold_defs_tac: Proof.context -> thm list -> tactic
    12.8 -  val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
    12.9 +  val unfold_thms_tac: Proof.context -> thm list -> tactic
   12.10 +  val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
   12.11  
   12.12    val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
   12.13    val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
   12.14 @@ -57,11 +57,11 @@
   12.15      rtac (Drule.instantiate_normalize insts thm) 1
   12.16    end);
   12.17  
   12.18 -fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
   12.19 +fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
   12.20  
   12.21 -fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x;
   12.22 +fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
   12.23  
   12.24 -(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*)
   12.25 +(*unlike "unfold_thms_tac", succeeds when the RHS contains schematic variables not in the LHS*)
   12.26  fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
   12.27  fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
   12.28  fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
   12.29 @@ -99,13 +99,13 @@
   12.30    end;
   12.31  
   12.32  fun simple_rel_O_Gr_tac ctxt =
   12.33 -  unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
   12.34 +  unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
   12.35  
   12.36  fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
   12.37 -  unfold_defs_tac ctxt IJpred_defs THEN
   12.38 -  subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @
   12.39 +  unfold_thms_tac ctxt IJpred_defs THEN
   12.40 +  subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
   12.41      @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
   12.42 -  unfold_defs_tac ctxt (rel_def ::
   12.43 +  unfold_thms_tac ctxt (rel_def ::
   12.44      @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
   12.45        split_conv}) THEN
   12.46    rtac refl 1;
    13.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 15:53:29 2012 +0200
    13.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 15:53:29 2012 +0200
    13.3 @@ -134,8 +134,8 @@
    13.4    val no_refl: thm list -> thm list
    13.5    val no_reflexive: thm list -> thm list
    13.6  
    13.7 -  val fold_defs: Proof.context -> thm list -> thm -> thm
    13.8 -  val unfold_defs: Proof.context -> thm list -> thm -> thm
    13.9 +  val fold_thms: Proof.context -> thm list -> thm -> thm
   13.10 +  val unfold_thms: Proof.context -> thm list -> thm -> thm
   13.11  
   13.12    val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
   13.13    val find_indices: ''a list -> ''a list -> int list
   13.14 @@ -613,7 +613,7 @@
   13.15  val no_refl = filter_out is_refl;
   13.16  val no_reflexive = filter_out Thm.is_reflexive;
   13.17  
   13.18 -fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
   13.19 -fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
   13.20 +fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
   13.21 +fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
   13.22  
   13.23  end;
    14.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
    14.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
    14.3 @@ -443,7 +443,7 @@
    14.4                    disc_defs';
    14.5                val not_discI_thms =
    14.6                  map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
    14.7 -                    (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
    14.8 +                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
    14.9                    ms disc_defs';
   14.10  
   14.11                val (disc_thmss', disc_thmss) =
    15.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    15.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
    15.3 @@ -42,7 +42,7 @@
    15.4  
    15.5  fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
    15.6    EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    15.7 -    hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    15.8 +    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    15.9      rtac distinct, rtac uexhaust] @
   15.10      (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
   15.11       |> k = 1 ? swap |> op @)) 1;
   15.12 @@ -63,7 +63,7 @@
   15.13        atac
   15.14      else
   15.15        REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
   15.16 -      SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1;
   15.17 +      SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
   15.18  
   15.19  fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
   15.20      disc_excludesss' =
   15.21 @@ -98,7 +98,7 @@
   15.22  fun mk_case_eq_tac ctxt n uexhaust cases discss' selss =
   15.23    (rtac uexhaust THEN'
   15.24     EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   15.25 -       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex])
   15.26 +       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
   15.27       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
   15.28  
   15.29  fun mk_case_cong_tac uexhaust cases =
   15.30 @@ -117,6 +117,6 @@
   15.31  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
   15.32  
   15.33  fun mk_split_asm_tac ctxt split =
   15.34 -  rtac (split RS trans) 1 THEN unfold_defs_tac ctxt split_asm_thms THEN rtac refl 1;
   15.35 +  rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
   15.36  
   15.37  end;