1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -51,8 +51,6 @@
     1.4  
     1.5  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
     1.6  
     1.7 -fun mk_id T = Const (@{const_name id}, T --> T);
     1.8 -
     1.9  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    1.10  fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
    1.11  fun mk_uncurried2_fun f xss =
    1.12 @@ -499,9 +497,10 @@
    1.13          ((wrap, define_iter_likes), lthy')
    1.14        end;
    1.15  
    1.16 -    (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there *)
    1.17 +    (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there ### *)
    1.18      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.19      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.20 +    val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    1.21      val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
    1.22  
    1.23      fun mk_map Ts Us t =
    1.24 @@ -571,26 +570,36 @@
    1.25                fold_rev Logic.all
    1.26                  (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.27  
    1.28 -            fun mk_prem phi ctr ctr_Ts =
    1.29 +            fun mk_prem_triple phi ctr ctr_Ts =
    1.30                let
    1.31                  val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
    1.32                  val prem_prems =
    1.33                    maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs;
    1.34                in
    1.35 -                fold_rev Logic.all xs
    1.36 -                  (Logic.list_implies (prem_prems,
    1.37 -                     HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))))
    1.38 +                (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
    1.39                end;
    1.40  
    1.41 +            val prem_tripless = map3 (map2 o mk_prem_triple) phis ctrss ctr_Tsss;
    1.42 +
    1.43 +            fun mk_prem (xs, prem_prems, concl) =
    1.44 +              fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
    1.45 +
    1.46              val goal =
    1.47 -              fold_rev (fold_rev Logic.all) [phis, vs]
    1.48 -                (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) phis ctrss ctr_Tsss,
    1.49 -                   HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.50 -                     (map2 (curry (op $)) phis vs))));
    1.51 +              Library.foldr (Logic.list_implies o apfst (map mk_prem)) (prem_tripless,
    1.52 +                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.53 +                  (map2 (curry (op $)) phis vs)));
    1.54 +
    1.55 +            val rss = map (map (length o #2)) prem_tripless;
    1.56 +
    1.57 +            val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.58  
    1.59              val induct_thm =
    1.60                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.61 -                mk_induct_tac ctxt);
    1.62 +                mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss
    1.63 +                  nested_set_natural's)
    1.64 +              (* TODO: thread name context properly ### *)
    1.65 +              |> singleton (Proof_Context.export names_lthy lthy)
    1.66 +              |> singleton (Proof_Context.export no_defs_lthy no_defs_lthy0)
    1.67            in
    1.68              `(conj_dests nn) induct_thm
    1.69            end;
    1.70 @@ -607,7 +616,7 @@
    1.71  
    1.72              fun build_call fiter_likes maybe_tick (T, U) =
    1.73                if T = U then
    1.74 -                mk_id T
    1.75 +                id_const T
    1.76                else
    1.77                  (case find_index (curry (op =) T) fpTs of
    1.78                    ~1 => build_map (build_call fiter_likes maybe_tick) T U
    1.79 @@ -685,7 +694,7 @@
    1.80  
    1.81              fun build_call fiter_likes maybe_tack (T, U) =
    1.82                if T = U then
    1.83 -                mk_id T
    1.84 +                id_const T
    1.85                else
    1.86                  (case find_index (curry (op =) U) fpTs of
    1.87                    ~1 => build_map (build_call fiter_likes maybe_tack) T U