# HG changeset patch
# User wenzelm
# Date 1378751055 -7200
# Node ID c413adedef469f88996675a5f5493da27a75f355
# Parent  662149d029158dbf7fcb90ea32d4ef2041c61610# Parent  97222a86aec009b0fda526fd7df93fd33d8a94aa
merged

diff -r 97222a86aec0 -r c413adedef46 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/ATP.thy	Mon Sep 09 20:24:15 2013 +0200
@@ -11,7 +11,6 @@
 
 ML_file "Tools/lambda_lifting.ML"
 ML_file "Tools/monomorph.ML"
-ML_file "Tools/legacy_monomorph.ML"
 ML_file "Tools/ATP/atp_util.ML"
 ML_file "Tools/ATP/atp_problem.ML"
 ML_file "Tools/ATP/atp_proof.ML"
diff -r 97222a86aec0 -r c413adedef46 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -23,7 +23,11 @@
      split_asm: thm,
      disc_thmss: thm list list,
      discIs: thm list,
-     sel_thmss: thm list list};
+     sel_thmss: thm list list,
+     disc_exhausts: thm list,
+     collapses: thm list,
+     expands: thm list,
+     case_convs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
 
@@ -68,10 +72,15 @@
    split_asm: thm,
    disc_thmss: thm list list,
    discIs: thm list,
-   sel_thmss: thm list list};
+   sel_thmss: thm list list,
+   disc_exhausts: thm list,
+   collapses: thm list,
+   expands: thm list,
+   case_convs: thm list};
 
 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
-    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} =
+    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
+    disc_exhausts, collapses, expands, case_convs} =
   {ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
@@ -87,7 +96,11 @@
    split_asm = Morphism.thm phi split_asm,
    disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    discIs = map (Morphism.thm phi) discIs,
-   sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
+   sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
+   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
+   collapses = map (Morphism.thm phi) collapses,
+   expands = map (Morphism.thm phi) expands,
+   case_convs = map (Morphism.thm phi) case_convs};
 
 val rep_compat_prefix = "new";
 
@@ -762,7 +775,8 @@
           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
-          discIs = discI_thms, sel_thmss = sel_thmss},
+          discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+          collapses = collapse_thms, expands = expand_thms, case_convs = case_conv_thms},
          lthy
          |> not rep_compat ?
             (Local_Theory.declaration {syntax = false, pervasive = true}
diff -r 97222a86aec0 -r c413adedef46 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -18,8 +18,11 @@
      ctr_defss: thm list list,
      ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
      co_iterss: term list list,
+     mapss: thm list list,
      co_inducts: thm list,
-     co_iter_thmsss: thm list list list};
+     co_iter_thmsss: thm list list list,
+     disc_co_itersss: thm list list list,
+     sel_co_iterssss: thm list list list list};
 
   val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
@@ -80,7 +83,7 @@
     * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
+    * (thm list list list * thm list list list * Args.src list)
 
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -118,8 +121,11 @@
    ctr_defss: thm list list,
    ctr_sugars: ctr_sugar list,
    co_iterss: term list list,
+   mapss: thm list list,
    co_inducts: thm list,
-   co_iter_thmsss: thm list list list};
+   co_iter_thmsss: thm list list list,
+   disc_co_itersss: thm list list list,
+   sel_co_iterssss: thm list list list list};
 
 fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
 
@@ -128,15 +134,18 @@
   T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
-    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
+    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
   {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
     nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    fp_res = morph_fp_result phi fp_res,
    ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    co_iterss = map (map (Morphism.term phi)) co_iterss,
+   mapss = map (map (Morphism.thm phi)) mapss,
    co_inducts = map (Morphism.thm phi) co_inducts,
-   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss};
+   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
+   disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
+   sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
 
 structure Data = Generic_Data
 (
@@ -161,13 +170,14 @@
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
-    ctr_sugars co_iterss co_inducts co_iter_thmsss lthy =
+    ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
         nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
-        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
-        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
+        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss,
+        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
+        sel_co_iterssss = sel_co_iterssss}
       lthy)) Ts
   |> snd;
 
@@ -999,10 +1009,10 @@
       end;
 
     fun mk_sel_coiter_thms coiter_thmss =
-      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat;
+      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
 
-    val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss;
-    val sel_corec_thmss = mk_sel_coiter_thms corec_thmss;
+    val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
+    val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
 
     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
@@ -1018,7 +1028,7 @@
      (safe_unfold_thmss, safe_corec_thmss),
      (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
-     (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
+     (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1407,7 +1417,7 @@
           @ rel_distincts @ flat setss);
 
     fun derive_and_note_induct_iters_thms_for_types
-        ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (iterss, iter_defss)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
@@ -1419,7 +1429,7 @@
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
         val simp_thmss =
-          mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapsx rel_injects rel_distincts setss;
+          mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1435,11 +1445,11 @@
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
-          iterss [induct_thm] (transpose [fold_thmss, rec_thmss])
+          iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
       end;
 
     fun derive_and_note_coinduct_coiters_thms_for_types
-        ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
           (coiterss, coiter_defss)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1448,11 +1458,14 @@
              (safe_unfold_thmss, safe_corec_thmss),
              (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
-             (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
+             (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
 
+        val sel_unfold_thmss = map flat sel_unfold_thmsss;
+        val sel_corec_thmss = map flat sel_corec_thmsss;
+
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
         fun flat_coiter_thms coiters disc_coiters sel_coiters =
@@ -1462,7 +1475,7 @@
           mk_simp_thmss ctr_sugars
             (map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
             (map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
-            mapsx rel_injects rel_distincts setss;
+            mapss rel_injects rel_distincts setss;
 
         val anonymous_notes =
           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
@@ -1494,8 +1507,9 @@
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
         |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
-          ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
-          (transpose [unfold_thmss, corec_thmss])
+          ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
+          (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
+          (transpose [sel_unfold_thmsss, sel_corec_thmsss])
       end;
 
     val lthy'' = lthy'
diff -r 97222a86aec0 -r c413adedef46 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -59,6 +59,7 @@
         end;
 
       val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
+      val mapss = map (of_fp_sugar #mapss) fp_sugars0;
       val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
       val ctrss = map #ctrs ctr_sugars0;
@@ -145,27 +146,33 @@
 
       val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
 
-      val (co_inducts, un_fold_thmss, co_rec_thmss) =
+      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
+           sel_unfold_thmsss, sel_corec_thmsss) =
         if fp = Least_FP then
           derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
             xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
             co_iterss co_iter_defss lthy
           |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
-            ([induct], fold_thmss, rec_thmss))
+            ([induct], fold_thmss, rec_thmss, [], [], [], []))
         else
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
-            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
+          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
+                  (disc_unfold_thmss, disc_corec_thmss, _),
+                  (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
+            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
+             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
 
       val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
       fun mk_target_fp_sugar (kk, T) =
         {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
          nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
-         ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
-         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
+         ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
+         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
+         disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
+         sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
         |> morph_fp_sugar phi;
     in
       ((true, map_index mk_target_fp_sugar fpTs), lthy)
diff -r 97222a86aec0 -r c413adedef46 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -54,8 +54,8 @@
 fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
   mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
-  mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
+fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
+  mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
   unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
     maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
 
diff -r 97222a86aec0 -r c413adedef46 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -31,7 +31,10 @@
      sels: term list,
      pred: int option,
      calls: corec_call list,
-     corec_thm: thm}
+     collapse: thm,
+     corec_thm: thm,
+     disc_corec: thm,
+     sel_corecs: thm list}
 
   type rec_spec =
     {recx: term,
@@ -41,6 +44,9 @@
 
   type corec_spec =
     {corec: term,
+     nested_maps: thm list,
+     nested_map_idents: thm list,
+     nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
@@ -90,7 +96,10 @@
    sels: term list,
    pred: int option,
    calls: corec_call list,
-   corec_thm: thm};
+   collapse: thm,
+   corec_thm: thm,
+   disc_corec: thm,
+   sel_corecs: thm list};
 
 type rec_spec =
   {recx: term,
@@ -100,6 +109,9 @@
 
 type corec_spec =
   {corec: term,
+   nested_maps: thm list,
+   nested_map_idents: thm list,
+   nested_map_comps: thm list,
    ctr_specs: corec_ctr_spec list};
 
 val id_def = @{thm id_def};
@@ -260,6 +272,18 @@
 
 fun find_index_eq hs h = find_index (curry (op =) h) hs;
 
+(*FIXME: remove special cases for products and sum once they are registered as datatypes*)
+fun map_thms_of_typ ctxt (Type (s, _)) =
+    if s = @{type_name prod} then
+      @{thms map_pair_simp}
+    else if s = @{type_name sum} then
+      @{thms sum_map.simps}
+    else
+      (case fp_sugar_of ctxt s of
+        SOME {index, mapss, ...} => nth mapss index
+      | NONE => [])
+  | map_thms_of_typ _ _ = [];
+
 val lose_co_rec = false (*FIXME: try true?*);
 
 fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
@@ -348,8 +372,8 @@
     val thy = Proof_Context.theory_of lthy;
 
     val ((nontriv, missing_res_Ts, perm0_kks,
-          fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
-          co_inducts = coinduct_thms, ...} :: _), lthy') =
+          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
+            co_inducts = coinduct_thms, ...} :: _), lthy') =
       nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
@@ -407,27 +431,38 @@
          else No_Corec) g_i
       | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
 
-    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
+    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
       let val nullary = not (can dest_funT (fastype_of ctr)) in
         {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
-         calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
+         calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
+         corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
       end;
 
-    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss =
+    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
+        sel_coiterssss =
       let
         val ctrs = #ctrs (nth ctr_sugars index);
         val discs = #discs (nth ctr_sugars index);
         val selss = #selss (nth ctr_sugars index);
         val p_ios = map SOME p_is @ [NONE];
-        val corec_thmss = co_rec_of (nth coiter_thmsss index);
+        val collapses = #collapses (nth ctr_sugars index);
+        val corec_thms = co_rec_of (nth coiter_thmsss index);
+        val disc_corecs = co_rec_of (nth disc_coitersss index);
+        val sel_corecss = co_rec_of (nth sel_coiterssss index);
       in
-        map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
+        map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
+          disc_corecs sel_corecss
       end;
 
-    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
+    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
+          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
         p_is q_isss f_isss f_Tsss =
       {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
-       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
+       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
+       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
+       nested_map_comps = map map_comp_of_bnf nested_bnfs,
+       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
+         disc_coitersss sel_coiterssss};
   in
     ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
diff -r 97222a86aec0 -r c413adedef46 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -215,9 +215,8 @@
       else
         conj_clauses @ fact_clauses
         |> map (pair 0)
-        |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false)
-        |-> Legacy_Monomorph.monomorph atp_schematic_consts_of
-        |> fst |> chop (length conj_clauses)
+        |> Monomorph.monomorph atp_schematic_consts_of ctxt
+        |> chop (length conj_clauses)
         |> pairself (maps (map (zero_var_indexes o snd)))
     val num_conjs = length conj_clauses
     (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
diff -r 97222a86aec0 -r c413adedef46 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -650,19 +650,14 @@
       | _ => (maybe_isar_name, [])
   in minimize_command override_params min_name end
 
-fun repair_legacy_monomorph_context max_iters best_max_iters max_new_instances
-                                    best_max_new_instances =
-  Config.put Legacy_Monomorph.max_rounds
-      (max_iters |> the_default best_max_iters)
-  #> Config.put Legacy_Monomorph.max_new_instances
-         (max_new_instances |> the_default best_max_new_instances)
-  #> Config.put Legacy_Monomorph.keep_partial_instances false
+val max_fact_instances = 10 (* FUDGE *)
 
 fun repair_monomorph_context max_iters best_max_iters max_new_instances
                              best_max_new_instances =
   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   #> Config.put Monomorph.max_new_instances
          (max_new_instances |> the_default best_max_new_instances)
+  #> Config.put Monomorph.max_thm_instances max_fact_instances
 
 fun suffix_of_mode Auto_Try = "_try"
   | suffix_of_mode Try = "_try"
@@ -757,7 +752,7 @@
           let
             val ctxt =
               ctxt
-              |> repair_legacy_monomorph_context max_mono_iters
+              |> repair_monomorph_context max_mono_iters
                      best_max_mono_iters max_new_mono_instances
                      best_max_new_mono_instances
             (* pseudo-theorem involving the same constants as the subgoal *)
@@ -770,9 +765,8 @@
                     |> op @
                     |> cons (0, subgoal_th)
           in
-            Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt
-            |> fst |> tl
-            |> curry ListPair.zip (map fst facts)
+            Monomorph.monomorph atp_schematic_consts_of ctxt rths
+            |> tl |> curry ListPair.zip (map fst facts)
             |> maps (fn (name, rths) =>
                         map (pair name o zero_var_indexes o snd) rths)
           end
diff -r 97222a86aec0 -r c413adedef46 src/HOL/Tools/legacy_monomorph.ML
--- a/src/HOL/Tools/legacy_monomorph.ML	Mon Sep 09 17:28:08 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,331 +0,0 @@
-(*  Title:      HOL/Tools/legacy_monomorph.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Monomorphization of theorems, i.e., computation of all (necessary)
-instances.  This procedure is incomplete in general, but works well for
-most practical problems.
-
-For a list of universally closed theorems (without schematic term
-variables), monomorphization computes a list of theorems with schematic
-term variables: all polymorphic constants (i.e., constants occurring both
-with ground types and schematic type variables) are instantiated with all
-(necessary) ground types; thereby theorems containing these constants are
-copied.  To prevent nontermination, there is an upper limit for the number
-of iterations involved in the fixpoint construction.
-
-The search for instances is performed on the constants with schematic
-types, which are extracted from the initial set of theorems.  The search
-constructs, for each theorem with those constants, a set of substitutions,
-which, in the end, is applied to all corresponding theorems.  Remaining
-schematic type variables are substituted with fresh types.
-
-Searching for necessary substitutions is an iterative fixpoint
-construction: each iteration computes all required instances required by
-the ground instances computed in the previous step and which haven't been
-found before.  Computed substitutions are always nontrivial: schematic type
-variables are never mapped to schematic type variables.
-*)
-
-signature LEGACY_MONOMORPH =
-sig
-  (* utility function *)
-  val typ_has_tvars: typ -> bool
-  val all_schematic_consts_of: term -> typ list Symtab.table
-  val add_schematic_consts_of: term -> typ list Symtab.table ->
-    typ list Symtab.table
-
-  (* configuration options *)
-  val max_rounds: int Config.T
-  val max_new_instances: int Config.T
-  val keep_partial_instances: bool Config.T
-
-  (* monomorphization *)
-  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
-    Proof.context -> (int * thm) list list * Proof.context
-end
-
-structure Legacy_Monomorph: LEGACY_MONOMORPH =
-struct
-
-(* utility functions *)
-
-val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
-
-fun add_schematic_const (c as (_, T)) =
-  if typ_has_tvars T then Symtab.insert_list (op =) c else I
-
-fun add_schematic_consts_of t =
-  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
-
-fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
-
-
-
-(* configuration options *)
-
-val max_rounds = Attrib.setup_config_int @{binding legacy_monomorph_max_rounds} (K 5)
-val max_new_instances =
-  Attrib.setup_config_int @{binding legacy_monomorph_max_new_instances} (K 300)
-val keep_partial_instances =
-  Attrib.setup_config_bool @{binding legacy_monomorph_keep_partial_instances} (K true)
-
-
-
-(* monomorphization *)
-
-(** preparing the problem **)
-
-datatype thm_info =
-  Ground of thm |
-  Schematic of {
-    index: int,
-    theorem: thm,
-    tvars: (indexname * sort) list,
-    schematics: typ list Symtab.table,
-    initial_round: int }
-
-fun prepare schematic_consts_of rthms =
-  let
-    val empty_sub = ((0, false, false), Vartab.empty)
-
-    fun prep (r, thm) ((i, idx), (consts, subs)) =
-      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
-        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
-      else
-        let
-          (* increase indices to avoid clashes of type variables *)
-          val thm' = Thm.incr_indexes idx thm
-          val idx' = Thm.maxidx_of thm' + 1
-          val schematics = schematic_consts_of (Thm.prop_of thm')
-          val consts' =
-            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
-          val subs' = Inttab.update (i, [empty_sub]) subs
-          val thm_info = Schematic {
-            index = i,
-            theorem = thm',
-            tvars = Term.add_tvars (Thm.prop_of thm') [],
-            schematics = schematics,
-            initial_round = r }
-      in (thm_info, ((i+1, idx'), (consts', subs'))) end
-  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
-
-
-
-(** collecting substitutions **)
-
-fun exceeded limit = (limit <= 0)
-fun exceeded_limit (limit, _, _) = exceeded limit
-
-
-fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => 
-  Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
-
-fun eq_subst (subst1, subst2) =
-  derived_subst subst1 subst2 andalso derived_subst subst2 subst1
-
-
-fun with_all_grounds cx grounds f =
-  if exceeded_limit cx then I else Symtab.fold f grounds
-
-fun with_all_type_combinations cx schematics f (n, Ts) =
-  if exceeded_limit cx then I
-  else fold_product f (Symtab.lookup_list schematics n) Ts
-
-fun derive_new_substs thy cx new_grounds schematics subst =
-  with_all_grounds cx new_grounds
-    (with_all_type_combinations cx schematics (fn T => fn U =>
-      (case try (Sign.typ_match thy (T, U)) subst of
-        NONE => I
-      | SOME subst' => insert eq_subst subst'))) []
-
-
-fun known_subst sub subs1 subs2 subst' =
-  let fun derived (_, subst) = derived_subst subst' subst
-  in derived sub orelse exists derived subs1 orelse exists derived subs2 end
-
-fun within_limit f cx = if exceeded_limit cx then cx else f cx
-
-fun fold_partial_substs derive add = within_limit (
-  let
-    fun fold_partial [] cx = cx
-      | fold_partial (sub :: subs) (limit, subs', next) =
-          if exceeded limit then (limit, sub :: subs @ subs', next)
-          else sub |> (fn ((generation, full, _), subst) =>
-            if full then fold_partial subs (limit, sub :: subs', next)
-            else
-              (case filter_out (known_subst sub subs subs') (derive subst) of
-                [] => fold_partial subs (limit, sub :: subs', next)
-              | substs =>
-                  (limit, ((generation, full, true), subst) :: subs', next)
-                  |> fold (within_limit o add) substs
-                  |> fold_partial subs))
-  in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
-
-
-fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val count_partial = Config.get ctxt keep_partial_instances
-
-    fun add_new_ground subst n T =
-      let val T' = Envir.subst_type subst T
-      in
-        (* FIXME: maybe keep types in a table or net for known_grounds,
-           that might improve efficiency here
-        *)
-        if typ_has_tvars T' then I
-        else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
-        else Symtab.cons_list (n, T')
-      end
-
-    fun add_new_subst subst (limit, subs, next_grounds) =
-      let
-        val full = forall (Vartab.defined subst o fst) tvars
-        val limit' =
-          if full orelse count_partial then limit - 1 else limit
-        val sub = ((round, full, false), subst)
-        val next_grounds' =
-          (schematics, next_grounds)
-          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
-      in (limit', sub :: subs, next_grounds') end
-  in
-    fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
-      add_new_subst cx
-  end
-
-
-(*
-  'known_grounds' are all constant names known to occur schematically
-  associated with all ground instances considered so far
-*)
-fun add_relevant_instances known_grounds (Const (c as (n, T))) =
-      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
-      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
-      else Symtab.insert_list (op =) c
-  | add_relevant_instances _ _ = I
-
-fun collect_instances known_grounds thm =
-  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
-
-
-fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
-  let
-    (* The total limit of returned (ground) facts is the number of facts
-       given to the monomorphizer increased by max_new_instances.  Since
-       initially ground facts are returned anyway, the limit here is not
-       counting them. *)
-    val limit = Config.get ctxt max_new_instances + 
-      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
-
-    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
-      | add_ground_consts (Schematic _) = I
-    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
-  in (known_grounds, (limit, substitutions, initial_grounds)) end
-
-fun is_new round initial_round = (round = initial_round)
-fun is_active round initial_round = (round > initial_round)
-
-fun fold_schematic pred f = fold (fn
-    Schematic {index, theorem, tvars, schematics, initial_round} =>
-      if pred initial_round then f theorem (index, tvars, schematics) else I
-  | Ground _ => I)
-
-fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
-  let
-    val (limit', isubs', next_grounds') =
-      (limit, Inttab.lookup_list subs index, next_grounds)
-      |> f (tvars, schematics)
-  in (limit', Inttab.update (index, isubs') subs, next_grounds') end
-
-fun collect_substitutions thm_infos ctxt round subst_ctxt =
-  let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
-  in
-    if exceeded limit then subst_ctxt
-    else
-      let
-        fun collect thm _ = collect_instances known_grounds thm
-        val new = fold_schematic (is_new round) collect thm_infos next_grounds
-
-        val known' = Symtab.merge_list (op =) (known_grounds, new)
-        val step = focus o refine ctxt round known'
-      in
-        (limit, subs, Symtab.empty)
-        |> not (Symtab.is_empty new) ?
-            fold_schematic (is_active round) (step new) thm_infos
-        |> fold_schematic (is_new round) (step known') thm_infos
-        |> pair known'
-      end
-  end
-
-
-
-(** instantiating schematic theorems **)
-
-fun super_sort (Ground _) S = S
-  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
-
-fun new_super_type ctxt thm_infos =
-  let val S = fold super_sort thm_infos @{sort type}
-  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
-
-fun add_missing_tvar T (ix, S) subst =
-  if Vartab.defined subst ix then subst
-  else Vartab.update (ix, (S, T)) subst
-
-fun complete tvars subst T =
-  subst
-  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
-  |> fold (add_missing_tvar T) tvars
-
-fun instantiate_all' (mT, ctxt) subs thm_infos =
-  let
-    val thy = Proof_Context.theory_of ctxt
-
-    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
-    fun cert' subst = Vartab.fold (cons o cert) subst []
-    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
-
-    fun with_subst tvars f ((generation, full, _), subst) =
-      if full then SOME (generation, f subst)
-      else Option.map (pair generation o f o complete tvars subst) mT
-
-    fun inst (Ground thm) = [(0, thm)]
-      | inst (Schematic {theorem, tvars, index, ...}) =
-          Inttab.lookup_list subs index
-          |> map_filter (with_subst tvars (instantiate theorem))
-  in (map inst thm_infos, ctxt) end
-
-fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
-  if Config.get ctxt keep_partial_instances then
-    let fun is_refined ((_, _, refined), _) = refined
-    in
-      (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
-      |-> instantiate_all' (new_super_type ctxt thm_infos)
-    end
-  else instantiate_all' (NONE, ctxt) subs thm_infos
-
-
-
-(** overall procedure **)
-
-fun limit_rounds ctxt f =
-  let
-    val max = Config.get ctxt max_rounds
-    fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
-  in round 1 end
-
-fun monomorph schematic_consts_of rthms ctxt =
-  let
-    val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
-  in
-    if Symtab.is_empty known_grounds then
-      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
-    else
-      make_subst_ctxt ctxt thm_infos known_grounds subs
-      |> limit_rounds ctxt (collect_substitutions thm_infos)
-      |> instantiate_all ctxt thm_infos
-  end
-
-
-end
-
diff -r 97222a86aec0 -r c413adedef46 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Mon Sep 09 17:28:08 2013 +0200
+++ b/src/HOL/Tools/monomorph.ML	Mon Sep 09 20:24:15 2013 +0200
@@ -35,6 +35,7 @@
   (* configuration options *)
   val max_rounds: int Config.T
   val max_new_instances: int Config.T
+  val max_thm_instances: int Config.T
 
   (* monomorphization *)
   val monomorph: (term -> typ list Symtab.table) -> Proof.context ->
@@ -67,14 +68,15 @@
 val max_new_instances =
   Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
 
+val max_thm_instances =
+  Attrib.setup_config_int @{binding max_thm_instances} (K 20)
+
 fun limit_rounds ctxt f =
   let
     val max = Config.get ctxt max_rounds
     fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
   in round 1 end
 
-fun reached_limit ctxt n = (n >= Config.get ctxt max_new_instances)
-
 
 
 (* theorem information and related functions *)
@@ -175,25 +177,31 @@
   in Term.fold_aterms add (Thm.prop_of thm) end
 
 
-fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx =
+fun add_insts max_instances max_thm_instances ctxt round used_grounds
+    new_grounds id thm tvars schematics cx =
   let
     exception ENOUGH of
       typ list Symtab.table * (int * (int * thm) list Inttab.table)
 
     val thy = Proof_Context.theory_of ctxt
 
-    fun add subst (next_grounds, (n, insts)) =
-      let
-        val thm' = instantiate thy subst thm
-        val rthm = (round, thm')
-        val n_insts' =
-          if member (eq_snd Thm.eq_thm) (Inttab.lookup_list insts id) rthm then
-            (n, insts)
-          else (n + 1, Inttab.cons_list (id, rthm) insts)
-        val next_grounds' =
-          add_new_grounds used_grounds new_grounds thm' next_grounds
-        val cx' = (next_grounds', n_insts')
-      in if reached_limit ctxt n then raise ENOUGH cx' else cx' end
+    fun add subst (cx as (next_grounds, (n, insts))) =
+      if n >= max_instances then
+        raise ENOUGH cx
+      else
+        let
+          val thm' = instantiate thy subst thm
+          val rthm = (round, thm')
+          val rthms = Inttab.lookup_list insts id;
+          val n_insts' =
+            if member (eq_snd Thm.eq_thm) rthms rthm orelse
+               length rthms >= max_thm_instances then
+              (n, insts)
+            else
+              (n + 1, Inttab.cons_list (id, rthm) insts)
+          val next_grounds' =
+            add_new_grounds used_grounds new_grounds thm' next_grounds
+        in (next_grounds', n_insts') end
 
     fun with_grounds (n, T) f subst (n', Us) =
       let
@@ -239,12 +247,12 @@
 fun is_active round initial_round = (round > initial_round)
 
 
-fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) =
+fun find_instances max_instances max_thm_instances thm_infos ctxt round
+    (known_grounds, new_grounds, insts) =
   let
-    val add_new = add_insts ctxt round
+    val add_new = add_insts max_instances max_thm_instances ctxt round
     fun consider_all pred f (cx as (_, (n, _))) =
-      if reached_limit ctxt n then cx
-      else fold_schematics pred f thm_infos cx
+      if n >= max_instances then cx else fold_schematics pred f thm_infos cx
 
     val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
     val empty_grounds = clear_grounds known_grounds'
@@ -266,9 +274,13 @@
   let
     val known_grounds = fold_grounds add_ground_types thm_infos consts
     val empty_grounds = clear_grounds known_grounds
+    val max_instances = Config.get ctxt max_new_instances
+      |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos
+    val max_thm_instances = Config.get ctxt max_thm_instances
   in
     (empty_grounds, known_grounds, (0, Inttab.empty))
-    |> limit_rounds ctxt (find_instances thm_infos)
+    |> limit_rounds ctxt
+      (find_instances max_instances max_thm_instances thm_infos)
     |> (fn (_, _, (_, insts)) => insts)
   end