--- 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}
--- 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
--- 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;