rationalized internals
authorblanchet
Mon Mar 03 12:48:20 2014 +0100 (2014-03-03)
changeset 5586779b915f26533
parent 55866 a6fa341a6d66
child 55868 37b99986d435
rationalized internals
NEWS
src/HOL/BNF_LFP.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Option.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/NEWS	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/NEWS	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -169,10 +169,12 @@
     1.4      Option.set ~> set_option
     1.5      Option.map ~> map_option
     1.6      option_rel ~> rel_option
     1.7 +    option_rec ~> case_option
     1.8    Renamed theorems:
     1.9      set_def ~> set_rec[abs_def]
    1.10      map_def ~> map_rec[abs_def]
    1.11      Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    1.12 +    option.recs ~> option.case
    1.13      list_all2_def ~> list_all2_iff
    1.14      set.simps ~> set_simps (or the slightly different "list.set")
    1.15      map.simps ~> list.map
     2.1 --- a/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
     2.2 +++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
     2.3 @@ -264,10 +264,10 @@
     2.4  
     2.5  hide_fact (open) id_transfer
     2.6  
     2.7 -datatype_new 'a F = F 'a
     2.8 +datatype_new 'a F = F0 | F 'a "'a F"
     2.9  datatype_compat F
    2.10  
    2.11  primrec f where
    2.12 -  "f (F x) = x"
    2.13 +  "f (F x y) = F x (f y)"
    2.14  
    2.15  end
     3.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 12:48:20 2014 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 12:48:20 2014 +0100
     3.3 @@ -585,20 +585,6 @@
     3.4  nitpick [expect = genuine]
     3.5  oops
     3.6  
     3.7 -lemma "rec_option n s None = n"
     3.8 -nitpick [expect = none]
     3.9 -apply simp
    3.10 -done
    3.11 -
    3.12 -lemma "rec_option n s (Some x) = s x"
    3.13 -nitpick [expect = none]
    3.14 -apply simp
    3.15 -done
    3.16 -
    3.17 -lemma "P (rec_option n s x)"
    3.18 -nitpick [expect = genuine]
    3.19 -oops
    3.20 -
    3.21  lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
    3.22  nitpick [expect = genuine]
    3.23  oops
     4.1 --- a/src/HOL/Option.thy	Mon Mar 03 12:48:20 2014 +0100
     4.2 +++ b/src/HOL/Option.thy	Mon Mar 03 12:48:20 2014 +0100
     4.3 @@ -28,7 +28,6 @@
     4.4  setup {* Sign.mandatory_path "option" *}
     4.5  
     4.6  lemmas inducts = option.induct
     4.7 -lemmas recs = option.rec
     4.8  lemmas cases = option.case
     4.9  
    4.10  setup {* Sign.parent_path *}
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     5.3 @@ -56,34 +56,34 @@
     5.4    val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
     5.5    val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
     5.6  
     5.7 -  val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
     5.8 -     typ list -> typ list -> int list -> int list list -> term list list -> Proof.context ->
     5.9 -     (term list list * (typ list list * typ list list list list * term list list
    5.10 -        * term list list list list) option
    5.11 +  val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
    5.12 +     typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
    5.13 +     (term list
    5.14 +      * (typ list list * typ list list list list * term list list * term list list list list) option
    5.15        * (string * term list * term list list
    5.16 -        * ((term list list * term list list list) * typ list)) option)
    5.17 +         * ((term list list * term list list list) * typ list)) option)
    5.18       * Proof.context
    5.19    val repair_nullary_single_ctr: typ list list -> typ list list
    5.20 -  val mk_coiter_p_pred_types: typ list -> int list -> typ list list
    5.21 -  val mk_coiter_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
    5.22 +  val mk_corec_p_pred_types: typ list -> int list -> typ list list
    5.23 +  val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
    5.24      int list list -> term ->
    5.25      typ list list
    5.26      * (typ list list list list * typ list list list * typ list list list list * typ list)
    5.27 -  val define_iter:
    5.28 +  val define_rec:
    5.29      (typ list list * typ list list list list * term list list * term list list list list) option ->
    5.30      (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
    5.31      (term * thm) * Proof.context
    5.32 -  val define_coiter: 'a * term list * term list list
    5.33 +  val define_corec: 'a * term list * term list list
    5.34        * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
    5.35      typ list -> term list -> term -> Proof.context -> (term * thm) * local_theory
    5.36 -  val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
    5.37 -     ('a * typ list list list list * term list list * 'b) option -> thm -> thm list list ->
    5.38 +  val derive_induct_recs_thms_for_types: BNF_Def.bnf list ->
    5.39 +     ('a * typ list list list list * term list list * 'b) option -> thm -> thm list ->
    5.40       BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
    5.41       typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
    5.42       term list -> thm list -> Proof.context -> lfp_sugar_thms
    5.43 -  val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
    5.44 +  val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
    5.45      string * term list * term list list * ((term list list * term list list list) * typ list) ->
    5.46 -    thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
    5.47 +    thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
    5.48      typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
    5.49      thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
    5.50      thm list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
    5.51 @@ -254,7 +254,7 @@
    5.52  val mk_ctor = mk_ctor_or_dtor range_type;
    5.53  val mk_dtor = mk_ctor_or_dtor domain_type;
    5.54  
    5.55 -fun mk_co_iters thy fp fpTs Cs ts0 =
    5.56 +fun mk_xtor_co_recs thy fp fpTs Cs ts0 =
    5.57    let
    5.58      val nn = length fpTs;
    5.59      val (fpTs0, Cs0) =
    5.60 @@ -318,9 +318,9 @@
    5.61  type lfp_sugar_thms =
    5.62    (thm list * thm * Args.src list) * (thm list list * Args.src list);
    5.63  
    5.64 -fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, iter_attrs)) =
    5.65 +fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) =
    5.66    ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
    5.67 -   (map (map (Morphism.thm phi)) recss, iter_attrs))
    5.68 +   (map (map (Morphism.thm phi)) recss, rec_attrs))
    5.69    : lfp_sugar_thms;
    5.70  
    5.71  val transfer_lfp_sugar_thms =
    5.72 @@ -334,48 +334,43 @@
    5.73    * (thm list list list * Args.src list);
    5.74  
    5.75  fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
    5.76 -    (corecss, coiter_attrs), (disc_corecss, disc_iter_attrs),
    5.77 -    (disc_corec_iffss, disc_iter_iff_attrs), (sel_corecsss, sel_iter_attrs)) =
    5.78 +    (corecss, corec_attrs), (disc_corecss, disc_rec_attrs),
    5.79 +    (disc_corec_iffss, disc_rec_iff_attrs), (sel_corecsss, sel_rec_attrs)) =
    5.80    ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
    5.81      coinduct_attrs),
    5.82 -   (map (map (Morphism.thm phi)) corecss, coiter_attrs),
    5.83 -   (map (map (Morphism.thm phi)) disc_corecss, disc_iter_attrs),
    5.84 -   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_iter_iff_attrs),
    5.85 -   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
    5.86 +   (map (map (Morphism.thm phi)) corecss, corec_attrs),
    5.87 +   (map (map (Morphism.thm phi)) disc_corecss, disc_rec_attrs),
    5.88 +   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_rec_iff_attrs),
    5.89 +   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_rec_attrs)) : gfp_sugar_thms;
    5.90  
    5.91  val transfer_gfp_sugar_thms =
    5.92    morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
    5.93  
    5.94 -fun mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss ctor_iter_fun_Tss lthy =
    5.95 +fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
    5.96    let
    5.97      val Css = map2 replicate ns Cs;
    5.98 -    val y_Tsss = map5 (fn absT => fn repT => fn n => fn ms =>
    5.99 -        dest_absumprodT absT repT n ms o domain_type)
   5.100 -      absTs repTs ns mss (map un_fold_of ctor_iter_fun_Tss);
   5.101 -
   5.102      val z_Tssss =
   5.103 -      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
   5.104 +      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
   5.105            map2 (map2 unzip_recT)
   5.106 -            ctr_Tss (dest_absumprodT absT repT n ms (domain_type (co_rec_of ctor_iter_fun_Ts))))
   5.107 -        absTs repTs ns mss ctr_Tsss ctor_iter_fun_Tss;
   5.108 +            ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T)))
   5.109 +        absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts;
   5.110  
   5.111      val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
   5.112      val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
   5.113  
   5.114 -    val (((hss, ysss), zssss), lthy) =
   5.115 +    val ((hss, zssss), lthy) =
   5.116        lthy
   5.117        |> mk_Freess "f" h_Tss
   5.118 -      ||>> mk_Freesss "x" (*###*)y_Tsss
   5.119 -      ||>> mk_Freessss "y" z_Tssss;
   5.120 +      ||>> mk_Freessss "x" z_Tssss;
   5.121    in
   5.122      ((h_Tss, z_Tssss, hss, zssss), lthy)
   5.123    end;
   5.124  
   5.125 -(*avoid "'a itself" arguments in coiterators*)
   5.126 +(*avoid "'a itself" arguments in corecursors*)
   5.127  fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
   5.128    | repair_nullary_single_ctr Tss = Tss;
   5.129  
   5.130 -fun mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
   5.131 +fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
   5.132    let
   5.133      val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
   5.134      val f_absTs = map range_type fun_Ts;
   5.135 @@ -387,27 +382,19 @@
   5.136      (q_Tssss, f_Tsss, f_Tssss, f_absTs)
   5.137    end;
   5.138  
   5.139 -fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
   5.140 +fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
   5.141  
   5.142 -fun mk_coiter_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter =
   5.143 -  (mk_coiter_p_pred_types Cs ns,
   5.144 -   mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
   5.145 -     (binder_fun_types (fastype_of dtor_coiter)));
   5.146 -
   5.147 -fun mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter_fun_Tss lthy =
   5.148 -  let
   5.149 -    val p_Tss = mk_coiter_p_pred_types Cs ns;
   5.150 +fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec =
   5.151 +  (mk_corec_p_pred_types Cs ns,
   5.152 +   mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
   5.153 +     (binder_fun_types (fastype_of dtor_corec)));
   5.154  
   5.155 -    fun mk_types get_Ts =
   5.156 -      let
   5.157 -        val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
   5.158 -        val (q_Tssss, f_Tsss, f_Tssss, f_repTs) =
   5.159 -          mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts;
   5.160 -      in
   5.161 -        (q_Tssss, f_Tsss, f_Tssss, f_repTs)
   5.162 -      end;
   5.163 +fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
   5.164 +  let
   5.165 +    val p_Tss = mk_corec_p_pred_types Cs ns;
   5.166  
   5.167 -    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of;
   5.168 +    val (s_Tssss, h_Tsss, h_Tssss, corec_types) =
   5.169 +      mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
   5.170  
   5.171      val (((((Free (z, _), cs), pss), sssss), hssss), lthy) =
   5.172        lthy
   5.173 @@ -421,8 +408,8 @@
   5.174  
   5.175      fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
   5.176  
   5.177 -    fun build_dtor_coiter_arg _ [] [cf] = cf
   5.178 -      | build_dtor_coiter_arg T [cq] [cf, cf'] =
   5.179 +    fun build_dtor_corec_arg _ [] [cf] = cf
   5.180 +      | build_dtor_corec_arg T [cq] [cf, cf'] =
   5.181          mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
   5.182            (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
   5.183  
   5.184 @@ -431,7 +418,7 @@
   5.185          val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss;
   5.186          val cqssss = map2 (map o map o map o rapp) cs qssss;
   5.187          val cfssss = map2 (map o map o map o rapp) cs fssss;
   5.188 -        val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
   5.189 +        val cqfsss = map3 (map3 (map3 build_dtor_corec_arg)) f_Tsss cqssss cfssss;
   5.190        in (pfss, cqfsss) end;
   5.191  
   5.192      val corec_args = mk_args sssss hssss h_Tsss;
   5.193 @@ -439,28 +426,26 @@
   5.194      ((z, cs, cpss, (corec_args, corec_types)), lthy)
   5.195    end;
   5.196  
   5.197 -fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy =
   5.198 +fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
   5.199    let
   5.200      val thy = Proof_Context.theory_of lthy;
   5.201      val nn = length fpTs;
   5.202  
   5.203 -    val (xtor_co_iter_fun_Tss, xtor_co_iterss) =
   5.204 -      map (mk_co_iters thy fp fpTs Cs #> `(binder_fun_types o fastype_of o hd))
   5.205 -        (transpose xtor_co_iterss0)
   5.206 -      |> apsnd transpose o apfst transpose o split_list;
   5.207 +    val (xtor_co_rec_fun_Ts, xtor_co_recs) =
   5.208 +      mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
   5.209  
   5.210 -    val ((iters_args_types, coiters_args_types), lthy') =
   5.211 +    val ((recs_args_types, corecs_args_types), lthy') =
   5.212        if fp = Least_FP then
   5.213          if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then
   5.214            ((NONE, NONE), lthy)
   5.215          else
   5.216 -          mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
   5.217 +          mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
   5.218            |>> (rpair NONE o SOME)
   5.219        else
   5.220 -        mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
   5.221 +        mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
   5.222          |>> (pair NONE o SOME);
   5.223    in
   5.224 -    ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
   5.225 +    ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
   5.226    end;
   5.227  
   5.228  fun mk_preds_getterss_join c cps absT abs cqfss =
   5.229 @@ -471,7 +456,7 @@
   5.230      Term.lambda c (mk_IfN absT cps ts)
   5.231    end;
   5.232  
   5.233 -fun define_co_iter fp fpT Cs b rhs lthy0 =
   5.234 +fun define_co_rec fp fpT Cs b rhs lthy0 =
   5.235    let
   5.236      val thy = Proof_Context.theory_of lthy0;
   5.237  
   5.238 @@ -490,32 +475,32 @@
   5.239      ((cst', def'), lthy')
   5.240    end;
   5.241  
   5.242 -fun define_iter NONE _ _ _ _ _ = pair (Term.dummy, refl)
   5.243 -  | define_iter (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_iter =
   5.244 +fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl)
   5.245 +  | define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec =
   5.246      let
   5.247        val nn = length fpTs;
   5.248 -      val (ctor_iter_absTs, fpT) = strip_typeN nn (fastype_of ctor_iter)
   5.249 +      val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
   5.250          |>> map domain_type ||> domain_type;
   5.251      in
   5.252 -      define_co_iter Least_FP fpT Cs (mk_binding recN)
   5.253 -        (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
   5.254 -           map4 (fn ctor_iter_absT => fn rep => fn fs => fn xsss =>
   5.255 -               mk_case_absumprod ctor_iter_absT rep fs
   5.256 +      define_co_rec Least_FP fpT Cs (mk_binding recN)
   5.257 +        (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
   5.258 +           map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
   5.259 +               mk_case_absumprod ctor_rec_absT rep fs
   5.260                   (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
   5.261 -             ctor_iter_absTs reps fss xssss)))
   5.262 +             ctor_rec_absTs reps fss xssss)))
   5.263      end;
   5.264  
   5.265 -fun define_coiter (_, cs, cpss, ((pfss, cqfsss), f_absTs)) mk_binding fpTs Cs abss dtor_coiter =
   5.266 +fun define_corec (_, cs, cpss, ((pfss, cqfsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
   5.267    let
   5.268      val nn = length fpTs;
   5.269 -    val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_coiter)));
   5.270 +    val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   5.271    in
   5.272 -    define_co_iter Greatest_FP fpT Cs (mk_binding corecN)
   5.273 -      (fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
   5.274 +    define_co_rec Greatest_FP fpT Cs (mk_binding corecN)
   5.275 +      (fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_corec,
   5.276           map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss)))
   5.277    end;
   5.278  
   5.279 -fun derive_induct_iters_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_iter_thmss
   5.280 +fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
   5.281      nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
   5.282      ctrss ctr_defss recs rec_defs lthy =
   5.283    let
   5.284 @@ -628,13 +613,13 @@
   5.285  
   5.286      val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
   5.287  
   5.288 -    fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms =
   5.289 +    fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms =
   5.290        let
   5.291 -        val fiters = map (lists_bmoc fss) iters;
   5.292 +        val frecs = map (lists_bmoc fss) recs;
   5.293  
   5.294 -        fun mk_goal fss fiter xctr f xs fxs =
   5.295 +        fun mk_goal fss frec xctr f xs fxs =
   5.296            fold_rev (fold_rev Logic.all) (xs :: fss)
   5.297 -            (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
   5.298 +            (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs)));
   5.299  
   5.300          fun maybe_tick (T, U) u f =
   5.301            if try (fst o HOLogic.dest_prodT) U = SOME T then
   5.302 @@ -642,20 +627,20 @@
   5.303            else
   5.304              f;
   5.305  
   5.306 -        fun build_iter (x as Free (_, T)) U =
   5.307 +        fun build_rec (x as Free (_, T)) U =
   5.308            if T = U then
   5.309              x
   5.310            else
   5.311              build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
   5.312 -              (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x;
   5.313 +              (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
   5.314  
   5.315 -        val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss;
   5.316 +        val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
   5.317  
   5.318 -        val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
   5.319 +        val goalss = map5 (map4 o mk_goal fss) frecs xctrss fss xsss fxsss;
   5.320  
   5.321          val tacss =
   5.322 -          map4 (map ooo mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs)
   5.323 -            ctor_iter_thms fp_abs_inverses abs_inverses ctr_defss;
   5.324 +          map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
   5.325 +            ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
   5.326  
   5.327          fun prove goal tac =
   5.328            Goal.prove_sorry lthy [] [] goal (tac o #context)
   5.329 @@ -666,25 +651,23 @@
   5.330  
   5.331      val rec_thmss =
   5.332        (case rec_args_typess of
   5.333 -        SOME types =>
   5.334 -        mk_iter_thmss types recs rec_defs (map co_rec_of ctor_iter_thmss)
   5.335 +        SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms
   5.336        | NONE => replicate nn []);
   5.337    in
   5.338      ((induct_thms, induct_thm, [induct_case_names_attr]),
   5.339       (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
   5.340    end;
   5.341  
   5.342 -fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
   5.343 -      coiters_args_types as ((phss, cshsss), _))
   5.344 -    dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
   5.345 +fun derive_coinduct_corecs_thms_for_types pre_bnfs (z, cs, cpss,
   5.346 +      corecs_args_types as ((phss, cshsss), _))
   5.347 +    dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
   5.348      mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
   5.349      corecs corec_defs export_args lthy =
   5.350    let
   5.351 -    fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
   5.352 -      iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
   5.353 +    fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
   5.354 +      iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
   5.355  
   5.356 -    val ctor_dtor_coiter_thmss =
   5.357 -      map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
   5.358 +    val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
   5.359  
   5.360      val nn = length pre_bnfs;
   5.361  
   5.362 @@ -798,15 +781,15 @@
   5.363  
   5.364      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   5.365  
   5.366 -    val fcoiterss' as [hcorecs] =
   5.367 -      map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst coiters_args_types] [corecs];
   5.368 +    val fcorecss' as [hcorecs] =
   5.369 +      map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst corecs_args_types] [corecs];
   5.370  
   5.371      val corec_thmss =
   5.372        let
   5.373 -        fun mk_goal pfss c cps fcoiter n k ctr m cfs' =
   5.374 +        fun mk_goal pfss c cps fcorec n k ctr m cfs' =
   5.375            fold_rev (fold_rev Logic.all) ([c] :: pfss)
   5.376              (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   5.377 -               mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs'))));
   5.378 +               mk_Trueprop_eq (fcorec $ c, Term.list_comb (ctr, take m cfs'))));
   5.379  
   5.380          fun mk_U maybe_mk_sumT =
   5.381            typ_subst_nonatomic (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
   5.382 @@ -816,25 +799,25 @@
   5.383              Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z)
   5.384            end;
   5.385  
   5.386 -        fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf =
   5.387 +        fun build_corec fcorecs maybe_mk_sumT maybe_tack cqf =
   5.388            let val T = fastype_of cqf in
   5.389              if exists_subtype_in Cs T then
   5.390                let val U = mk_U maybe_mk_sumT T in
   5.391                  build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ =>
   5.392 -                  maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf
   5.393 +                  maybe_tack (nth cs kk, nth us kk) (nth fcorecs kk))) (T, U) $ cqf
   5.394                end
   5.395              else
   5.396                cqf
   5.397            end;
   5.398  
   5.399 -        val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z))))
   5.400 +        val cshsss' = map (map (map (build_corec (co_rec_of fcorecss') (curry mk_sumT) (tack z))))
   5.401            cshsss;
   5.402  
   5.403          val goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
   5.404  
   5.405          val tacss =
   5.406 -          map4 (map ooo mk_coiter_tac corec_defs nesting_map_idents)
   5.407 -            (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss;
   5.408 +          map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
   5.409 +            ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
   5.410  
   5.411          fun prove goal tac =
   5.412            Goal.prove_sorry lthy [] [] goal (tac o #context)
   5.413 @@ -846,8 +829,8 @@
   5.414  
   5.415      val disc_corec_iff_thmss =
   5.416        let
   5.417 -        fun mk_goal c cps fcoiter n k disc =
   5.418 -          mk_Trueprop_eq (disc $ (fcoiter $ c),
   5.419 +        fun mk_goal c cps fcorec n k disc =
   5.420 +          mk_Trueprop_eq (disc $ (fcorec $ c),
   5.421              if n = 1 then @{const True}
   5.422              else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   5.423  
   5.424 @@ -857,7 +840,7 @@
   5.425  
   5.426          val case_splitss' = map (map mk_case_split') cpss;
   5.427  
   5.428 -        val tacss = map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss;
   5.429 +        val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
   5.430  
   5.431          fun prove goal tac =
   5.432            Goal.prove_sorry lthy [] [] goal (tac o #context)
   5.433 @@ -871,11 +854,11 @@
   5.434          map2 proves goalss tacss
   5.435        end;
   5.436  
   5.437 -    fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs);
   5.438 +    fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs);
   5.439  
   5.440 -    val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss;
   5.441 +    val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
   5.442  
   5.443 -    fun mk_sel_coiter_thm coiter_thm sel sel_thm =
   5.444 +    fun mk_sel_corec_thm corec_thm sel sel_thm =
   5.445        let
   5.446          val (domT, ranT) = dest_funT (fastype_of sel);
   5.447          val arg_cong' =
   5.448 @@ -884,13 +867,13 @@
   5.449            |> Thm.varifyT_global;
   5.450          val sel_thm' = sel_thm RSN (2, trans);
   5.451        in
   5.452 -        coiter_thm RS arg_cong' RS sel_thm'
   5.453 +        corec_thm RS arg_cong' RS sel_thm'
   5.454        end;
   5.455  
   5.456 -    fun mk_sel_coiter_thms coiter_thmss =
   5.457 -      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
   5.458 +    fun mk_sel_corec_thms corec_thmss =
   5.459 +      map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
   5.460  
   5.461 -    val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
   5.462 +    val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
   5.463  
   5.464      val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   5.465      val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   5.466 @@ -1110,11 +1093,12 @@
   5.467      val kss = map (fn n => 1 upto n) ns;
   5.468      val mss = map (map length) ctr_Tsss;
   5.469  
   5.470 -    val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
   5.471 -      mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
   5.472 +    val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
   5.473 +      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
   5.474 +        lthy;
   5.475  
   5.476      fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
   5.477 -              xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
   5.478 +              xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
   5.479              pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
   5.480            abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
   5.481          disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
   5.482 @@ -1305,15 +1289,14 @@
   5.483  
   5.484          fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
   5.485  
   5.486 -        fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
   5.487 -          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
   5.488 +        fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) =
   5.489 +          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
   5.490        in
   5.491          (wrap_ctrs
   5.492           #> derive_maps_sets_rels
   5.493           ##>>
   5.494 -           (if fp = Least_FP then define_iter iters_args_types mk_binding fpTs Cs reps
   5.495 -           else define_coiter (the coiters_args_types) mk_binding fpTs Cs abss)
   5.496 -             (co_rec_of xtor_co_iters)
   5.497 +           (if fp = Least_FP then define_rec recs_args_types mk_binding fpTs Cs reps
   5.498 +           else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
   5.499           #> massage_res, lthy')
   5.500        end;
   5.501  
   5.502 @@ -1326,19 +1309,19 @@
   5.503          rel_distincts setss =
   5.504        injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
   5.505  
   5.506 -    fun derive_note_induct_iters_thms_for_types
   5.507 +    fun derive_note_induct_recs_thms_for_types
   5.508          ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
   5.509            (recs, rec_defs)), lthy) =
   5.510        let
   5.511          val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) =
   5.512 -          derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct
   5.513 -            xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
   5.514 -            type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
   5.515 +          derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
   5.516 +            (map co_rec_of xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss
   5.517 +            abs_inverses type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
   5.518  
   5.519          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   5.520  
   5.521          val (recs', rec_thmss') =
   5.522 -          if is_some iters_args_types then (recs, rec_thmss)
   5.523 +          if is_some recs_args_types then (recs, rec_thmss)
   5.524            else (map #casex ctr_sugars, map #case_thms ctr_sugars);
   5.525  
   5.526          val simp_thmss =
   5.527 @@ -1355,7 +1338,7 @@
   5.528            |> massage_multi_notes;
   5.529        in
   5.530          lthy
   5.531 -        |> (if is_some iters_args_types then
   5.532 +        |> (if is_some recs_args_types then
   5.533                Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
   5.534              else
   5.535                I)
   5.536 @@ -1365,30 +1348,30 @@
   5.537            rec_thmss' (replicate nn []) (replicate nn [])
   5.538        end;
   5.539  
   5.540 -    fun derive_note_coinduct_coiters_thms_for_types
   5.541 +    fun derive_note_coinduct_corecs_thms_for_types
   5.542          ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
   5.543 -          (coiters, corec_defs)), lthy) =
   5.544 +          (corecs, corec_defs)), lthy) =
   5.545        let
   5.546          val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
   5.547                coinduct_attrs),
   5.548 -             (corec_thmss, coiter_attrs),
   5.549 -             (disc_corec_thmss, disc_coiter_attrs),
   5.550 -             (disc_corec_iff_thmss, disc_coiter_iff_attrs),
   5.551 -             (sel_corec_thmsss, sel_coiter_attrs)) =
   5.552 -          derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
   5.553 -            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
   5.554 -            abs_inverses abs_inverses I ctr_defss ctr_sugars coiters corec_defs
   5.555 +             (corec_thmss, corec_attrs),
   5.556 +             (disc_corec_thmss, disc_corec_attrs),
   5.557 +             (disc_corec_iff_thmss, disc_corec_iff_attrs),
   5.558 +             (sel_corec_thmsss, sel_corec_attrs)) =
   5.559 +          derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
   5.560 +            dtor_injects dtor_ctors (map co_rec_of xtor_co_iter_thmss) nesting_bnfs fpTs Cs Xs
   5.561 +            ctrXs_Tsss kss mss ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   5.562              (Proof_Context.export lthy' no_defs_lthy) lthy;
   5.563  
   5.564          val sel_corec_thmss = map flat sel_corec_thmsss;
   5.565  
   5.566          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
   5.567  
   5.568 -        val flat_coiter_thms = append oo append;
   5.569 +        val flat_corec_thms = append oo append;
   5.570  
   5.571          val simp_thmss =
   5.572            map6 mk_simp_thms ctr_sugars
   5.573 -            (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
   5.574 +            (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
   5.575              mapss rel_injects rel_distincts setss;
   5.576  
   5.577          val common_notes =
   5.578 @@ -1402,35 +1385,34 @@
   5.579          val notes =
   5.580            [(coinductN, map single coinduct_thms,
   5.581              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   5.582 -           (corecN, corec_thmss, K coiter_attrs),
   5.583 -           (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
   5.584 -           (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
   5.585 -           (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
   5.586 +           (corecN, corec_thmss, K corec_attrs),
   5.587 +           (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
   5.588 +           (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
   5.589 +           (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
   5.590             (simpsN, simp_thmss, K []),
   5.591             (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
   5.592            |> massage_multi_notes;
   5.593        in
   5.594          lthy
   5.595          (* TODO: code theorems *)
   5.596 -        |> fold (curry (Spec_Rules.add Spec_Rules.Equational) coiters)
   5.597 +        |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
   5.598            [flat sel_corec_thmss, flat corec_thmss]
   5.599          |> Local_Theory.notes (common_notes @ notes) |> snd
   5.600          |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
   5.601 -          ctrXs_Tsss ctr_defss ctr_sugars coiters mapss [coinduct_thm, strong_coinduct_thm]
   5.602 +          ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm]
   5.603            (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
   5.604            sel_corec_thmsss
   5.605        end;
   5.606  
   5.607      val lthy'' = lthy'
   5.608        |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
   5.609 -        xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
   5.610 -        pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
   5.611 -        kss ~~ mss ~~ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~
   5.612 -        ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
   5.613 -        raw_sel_defaultsss)
   5.614 +        xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
   5.615 +        pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
   5.616 +        abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
   5.617 +        ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
   5.618        |> wrap_types_etc
   5.619 -      |> fp_case fp derive_note_induct_iters_thms_for_types
   5.620 -           derive_note_coinduct_coiters_thms_for_types;
   5.621 +      |> fp_case fp derive_note_induct_recs_thms_for_types
   5.622 +           derive_note_coinduct_corecs_thms_for_types;
   5.623  
   5.624      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   5.625        co_prefix fp ^ "datatype"));
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 03 12:48:20 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 03 12:48:20 2014 +0100
     6.3 @@ -14,16 +14,16 @@
     6.4    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
     6.5      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
     6.6      thm list list list -> tactic
     6.7 -  val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
     6.8 +  val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
     6.9    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    6.10      tactic
    6.11 -  val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    6.12 +  val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    6.13    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
    6.14    val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
    6.15    val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
    6.16      thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    6.17    val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
    6.18 -  val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
    6.19 +  val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
    6.20      tactic
    6.21  end;
    6.22  
    6.23 @@ -87,32 +87,32 @@
    6.24    unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN
    6.25    HEADGOAL (rtac refl);
    6.26  
    6.27 -val iter_unfold_thms =
    6.28 +val rec_unfold_thms =
    6.29    @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
    6.30        case_unit_Unity} @ sum_prod_thms_map;
    6.31  
    6.32 -fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter fp_abs_inverse abs_inverse ctr_def ctxt =
    6.33 -  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: fp_abs_inverse :: abs_inverse :: iter_defs @
    6.34 -    pre_map_defs @ map_idents @ iter_unfold_thms) THEN HEADGOAL (rtac refl);
    6.35 +fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
    6.36 +  unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    6.37 +    pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
    6.38  
    6.39 -val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
    6.40 +val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
    6.41  
    6.42 -fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def abs_inverse ctr_def ctxt =
    6.43 +fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
    6.44    let
    6.45 -    val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ coiter_unfold_thms @
    6.46 +    val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @
    6.47        @{thms o_apply vimage2p_def if_True if_False}) ctxt;
    6.48    in
    6.49 -    unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
    6.50 -    HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
    6.51 +    unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN
    6.52 +    HEADGOAL (rtac (ctor_dtor_corec RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
    6.53      HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
    6.54    end;
    6.55  
    6.56 -fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
    6.57 -  EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc =>
    6.58 -      HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN
    6.59 +fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
    6.60 +  EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
    6.61 +      HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
    6.62        HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
    6.63        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
    6.64 -    (map rtac case_splits' @ [K all_tac]) coiters discs);
    6.65 +    (map rtac case_splits' @ [K all_tac]) corecs discs);
    6.66  
    6.67  fun solve_prem_prem_tac ctxt =
    6.68    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     7.3 @@ -240,31 +240,33 @@
     7.4          val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
     7.5          val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
     7.6  
     7.7 -        val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
     7.8 -          mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
     7.9 +        val xtor_co_rec_thms = map co_rec_of xtor_co_iter_thmss;
    7.10 +        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
    7.11 +          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
    7.12 +            lthy;
    7.13  
    7.14          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
    7.15  
    7.16          val ((co_recs, co_rec_defs), lthy) =
    7.17            fold_map2 (fn b =>
    7.18 -            if fp = Least_FP then define_iter iters_args_types (mk_binding b) fpTs Cs reps
    7.19 -            else define_coiter (the coiters_args_types) (mk_binding b) fpTs Cs abss)
    7.20 -            fp_bs (map co_rec_of xtor_co_iterss) lthy
    7.21 +              if fp = Least_FP then define_rec recs_args_types (mk_binding b) fpTs Cs reps
    7.22 +              else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
    7.23 +            fp_bs xtor_co_recs lthy
    7.24            |>> split_list;
    7.25  
    7.26          val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
    7.27               fp_sugar_thms) =
    7.28            if fp = Least_FP then
    7.29 -            derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct
    7.30 -              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
    7.31 +            derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
    7.32 +              xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
    7.33                fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
    7.34              |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
    7.35                ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
    7.36              ||> (fn info => (SOME info, NONE))
    7.37            else
    7.38 -            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    7.39 -              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
    7.40 -              ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
    7.41 +            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
    7.42 +              dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    7.43 +              fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
    7.44                ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
    7.45              |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
    7.46                       (sel_corec_thmsss, _)) =>
     8.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Mar 03 12:48:20 2014 +0100
     8.2 +++ b/src/HOL/ex/Refute_Examples.thy	Mon Mar 03 12:48:20 2014 +0100
     8.3 @@ -547,18 +547,6 @@
     8.4  refute [expect = genuine]
     8.5  oops
     8.6  
     8.7 -lemma "rec_option n s None = n"
     8.8 -refute [expect = none]
     8.9 -by simp
    8.10 -
    8.11 -lemma "rec_option n s (Some x) = s x"
    8.12 -refute [maxsize = 4, expect = none]
    8.13 -by simp
    8.14 -
    8.15 -lemma "P (rec_option n s x)"
    8.16 -refute [expect = genuine]
    8.17 -oops
    8.18 -
    8.19  lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
    8.20  refute [expect = genuine]
    8.21  oops