# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID a28817253b31659e19d1313836771a7a22b72ada
# Parent  2f90476e3e61c4230458d8a9c6678f1b8743a024
removed (co)iterators from documentation

diff -r 2f90476e3e61 -r a28817253b31 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -619,9 +619,9 @@
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
-\item The old-style, nested-as-mutual induction rule, iterator theorems, and
-recursor theorems are generated under their usual names but with ``@{text
-"compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
+\item The old-style, nested-as-mutual induction rule and recursor theorems are
+generated under their usual names but with ``@{text "compat_"}'' prefixed
+(e.g., @{text compat_tree.induct}).
 
 \item All types through which recursion takes place must be new-style datatypes
 or the function type. In principle, it should be possible to support old-style
@@ -665,8 +665,6 @@
   @{text t.map_t} \\
 Relator: &
   @{text t.rel_t} \\
-Iterator: &
-   @{text t.fold_t} \\
 Recursor: &
   @{text t.rec_t}
 \end{tabular}
@@ -934,10 +932,6 @@
 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
 prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
-@{thm list.fold(1)[no_vars]} \\
-@{thm list.fold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]}
@@ -951,7 +945,7 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
 @{text t.rel_distinct} @{text t.set}
 
 \end{description}
@@ -1402,7 +1396,7 @@
 %  * induct
 %    * mutualized
 %    * without some needless induction hypotheses if not used
-%  * fold, rec
+%  * rec
 %    * mutualized
 *}
 *)
@@ -1627,13 +1621,11 @@
 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
-iterator and the recursor are replaced by dual concepts:
+recursor is replaced by a dual concept:
 
 \medskip
 
 \begin{tabular}{@ {}ll@ {}}
-Coiterator: &
-  @{text unfold_t} \\
 Corecursor: &
   @{text corec_t}
 \end{tabular}
@@ -1696,34 +1688,18 @@
 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
 used to prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{unfold}\rm:] ~ \\
-@{thm llist.unfold(1)[no_vars]} \\
-@{thm llist.unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
 @{thm llist.corec(1)[no_vars]} \\
 @{thm llist.corec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
-@{thm llist.disc_unfold(1)[no_vars]} \\
-@{thm llist.disc_unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
 @{thm llist.disc_corec(1)[no_vars]} \\
 @{thm llist.disc_corec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.disc_unfold_iff(1)[no_vars]} \\
-@{thm llist.disc_unfold_iff(2)[no_vars]}
-
 \item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
 @{thm llist.disc_corec_iff(1)[no_vars]} \\
 @{thm llist.disc_corec_iff(2)[no_vars]}
 
-\item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.sel_unfold(1)[no_vars]} \\
-@{thm llist.sel_unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
 @{thm llist.sel_corec(1)[no_vars]} \\
 @{thm llist.sel_corec(2)[no_vars]}
@@ -1738,8 +1714,7 @@
 \begin{description}
 
 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
-@{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
-@{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
+@{text t.sel_corec} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
 
 \end{description}
 \end{indentblock}
diff -r 2f90476e3e61 -r a28817253b31 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -228,11 +228,11 @@
 
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
-fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
+fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss);
 
-fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss
-  | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
-    p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
+fun flat_corec_preds_predsss_gettersss [] [qss] [gss] = flat_corec_predss_getterss qss gss
+  | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (gss :: gsss) =
+    p :: flat_corec_predss_getterss qss gss @ flat_corec_preds_predsss_gettersss ps qsss gsss;
 
 fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
   Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
@@ -334,14 +334,14 @@
   * (thm list list list * Args.src list);
 
 fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
-    (corecss, corec_attrs), (disc_corecss, disc_rec_attrs),
-    (disc_corec_iffss, disc_rec_iff_attrs), (sel_corecsss, sel_rec_attrs)) =
+    (corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
+    (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
   ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
     coinduct_attrs),
    (map (map (Morphism.thm phi)) corecss, corec_attrs),
-   (map (map (Morphism.thm phi)) disc_corecss, disc_rec_attrs),
-   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_rec_iff_attrs),
-   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_rec_attrs)) : gfp_sugar_thms;
+   (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
+   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
+   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
 
 val transfer_gfp_sugar_thms =
   morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -408,10 +408,10 @@
 
     fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
 
-    fun build_dtor_corec_arg _ [] [cf] = cf
-      | build_dtor_corec_arg T [cq] [cf, cf'] =
-        mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
-          (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
+    fun build_dtor_corec_arg _ [] [cg] = cg
+      | build_dtor_corec_arg T [cq] [cg, cg'] =
+        mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg)
+          (build_sum_inj Inr_const (fastype_of cg', T) $ cg');
 
     val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss;
     val cqssss = map2 (map o map o map o rapp) cs qssss;
@@ -612,7 +612,7 @@
       let
         val frecs = map (lists_bmoc fss) recs;
 
-        fun mk_goal fss frec xctr f xs fxs =
+        fun mk_goal frec xctr f xs fxs =
           fold_rev (fold_rev Logic.all) (xs :: fss)
             (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs)));
 
@@ -630,7 +630,7 @@
               (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
 
         val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
-        val goalss = map5 (map4 o mk_goal fss) frecs xctrss fss xsss fxsss;
+        val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
 
         val tacss =
           map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
@@ -652,8 +652,7 @@
      (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
   end;
 
-fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss,
-      corecs_args_types as ((pgss, cqgsss), _))
+fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
     dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
     mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
     corecs corec_defs export_args lthy =
@@ -1343,10 +1342,8 @@
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
               coinduct_attrs),
-             (corec_thmss, corec_attrs),
-             (disc_corec_thmss, disc_corec_attrs),
-             (disc_corec_iff_thmss, disc_corec_iff_attrs),
-             (sel_corec_thmsss, sel_corec_attrs)) =
+             (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
+             (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
           derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
             abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
diff -r 2f90476e3e61 -r a28817253b31 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -374,9 +374,8 @@
   let
     val thy = Proof_Context.theory_of lthy0;
 
-    val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_rec = corec,
-            common_co_inducts = common_coinduct_thms, ...} :: _,
-          (_, gfp_sugar_thms)), lthy) =
+    val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
+          common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
@@ -924,8 +923,8 @@
     val frees = map (fst #>> Binding.name_of #> Free) fixes;
     val has_call = exists_subterm (member (op =) frees);
     val eqns_data =
-      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
-        of_specs_opt []
+      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
+        (tag_list 0 (map snd specs)) of_specs_opt []
       |> flat o fst;
 
     val callssss =
@@ -1296,8 +1295,8 @@
           disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
           |> map sort_list_duplicates;
 
-        val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) disc_eqnss
-          sel_eqnss ctr_specss;
+        val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists)
+          disc_eqnss sel_eqnss ctr_specss;
         val ctr_thmss' = map (map snd) ctr_alists;
         val ctr_thmss = map (map snd o order_list) ctr_alists;