1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 21:26:01 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 22:23:10 2012 +0200
     1.3 @@ -546,7 +546,7 @@
     1.4                  Term.subst_atomic_types (Ts0 ~~ Ts) t
     1.5                end;
     1.6  
     1.7 -            fun mk_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) =
     1.8 +            fun mk_raw_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) =
     1.9                  (case find_index (curry (op =) T) fpTs of
    1.10                    ~1 =>
    1.11                    (case AList.lookup (op =) setss_nested T_name of
    1.12 @@ -557,47 +557,53 @@
    1.13                          split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0));
    1.14                        val sets = map (mk_set Ts0) raw_sets;
    1.15                        val (ys, names_lthy') = names_lthy |> mk_Frees s Ts;
    1.16 -                      val heads =
    1.17 -                        map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x)))
    1.18 -                          ys sets;
    1.19 -                      val bodiess = map (mk_prem_prems names_lthy') ys;
    1.20 +                      val xysets = map (pair x) (ys ~~ sets);
    1.21 +                      val ppremss = map (mk_raw_prem_prems names_lthy') ys;
    1.22                      in
    1.23 -                      flat (map2 (map o curry Logic.mk_implies) heads bodiess)
    1.24 +                      flat (map2 (map o apfst o cons) xysets ppremss)
    1.25                      end)
    1.26 -                | i => [HOLogic.mk_Trueprop (nth phis i $ x)])
    1.27 -              | mk_prem_prems _ _ = [];
    1.28 +                | i => [([], (i, x))])
    1.29 +              | mk_raw_prem_prems _ _ = [];
    1.30  
    1.31 -            fun close_prem_prem (Free x') t =
    1.32 +            fun close_prem_prem x' t =
    1.33                fold_rev Logic.all
    1.34                  (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
    1.35  
    1.36 +            fun mk_prem_prem x (xysets, (i, x')) =
    1.37 +              close_prem_prem (dest_Free x)
    1.38 +                (Logic.list_implies (map (fn (x'', (y, set)) =>
    1.39 +                     HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x''))) xysets,
    1.40 +                   HOLogic.mk_Trueprop (nth phis i $ x')));
    1.41 +
    1.42              fun mk_raw_prem phi ctr ctr_Ts =
    1.43                let
    1.44                  val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
    1.45 -                val prem_prems =
    1.46 -                  maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs;
    1.47 +                val pprems =
    1.48 +                  maps (fn x => map (mk_prem_prem x) (mk_raw_prem_prems names_lthy' x)) xs;
    1.49                in
    1.50 -                (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
    1.51 +                (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
    1.52                end;
    1.53  
    1.54              val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    1.55  
    1.56 -            fun mk_prem (xs, prem_prems, concl) =
    1.57 -              fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
    1.58 +            fun mk_prem (xs, pprems, concl) =
    1.59 +              fold_rev Logic.all xs (Logic.list_implies (pprems, concl));
    1.60  
    1.61              val goal =
    1.62                Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    1.63                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.64                    (map2 (curry (op $)) phis vs)));
    1.65  
    1.66 +            (* ### WRONG *)
    1.67              val rss = map (map (length o #2)) raw_premss;
    1.68 +            val ppisss = map (map (fn r => map (pair r) (1 upto r))) rss;
    1.69  
    1.70              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    1.71  
    1.72              val induct_thm =
    1.73                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.74 -                mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss
    1.75 -                  nested_set_natural's)
    1.76 +                mk_induct_tac ctxt ns mss ppisss (flat ctr_defss) fld_induct' nested_set_natural's
    1.77 +                  pre_set_defss)
    1.78                |> singleton (Proof_Context.export names_lthy lthy)
    1.79            in
    1.80              `(conj_dests nn) induct_thm