1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 22:23:10 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 22:23:10 2012 +0200
1.3 @@ -562,48 +562,53 @@
1.4 in
1.5 flat (map2 (map o apfst o cons) xysets ppremss)
1.6 end)
1.7 - | i => [([], (i, x))])
1.8 + | i => [([], (i + 1, x))])
1.9 | mk_raw_prem_prems _ _ = [];
1.10
1.11 - fun close_prem_prem x' t =
1.12 + fun close_prem_prem xs t =
1.13 fold_rev Logic.all
1.14 - (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
1.15 + (map Free (drop (2 * nn) (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
1.16
1.17 - fun mk_prem_prem x (xysets, (i, x')) =
1.18 - close_prem_prem (dest_Free x)
1.19 - (Logic.list_implies (map (fn (x'', (y, set)) =>
1.20 - HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x''))) xysets,
1.21 - HOLogic.mk_Trueprop (nth phis i $ x')));
1.22 + fun mk_prem_prem xs (xysets, (j, x)) =
1.23 + close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
1.24 + HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
1.25 + HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
1.26
1.27 fun mk_raw_prem phi ctr ctr_Ts =
1.28 let
1.29 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
1.30 - val pprems =
1.31 - maps (fn x => map (mk_prem_prem x) (mk_raw_prem_prems names_lthy' x)) xs;
1.32 + val pprems = maps (mk_raw_prem_prems names_lthy') xs;
1.33 in
1.34 (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
1.35 end;
1.36
1.37 val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
1.38
1.39 - fun mk_prem (xs, pprems, concl) =
1.40 - fold_rev Logic.all xs (Logic.list_implies (pprems, concl));
1.41 + fun mk_prem (xs, raw_pprems, concl) =
1.42 + fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
1.43
1.44 val goal =
1.45 Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
1.46 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
1.47 (map2 (curry (op $)) phis vs)));
1.48
1.49 - (* ### WRONG *)
1.50 - val rss = map (map (length o #2)) raw_premss;
1.51 - val ppisss = map (map (fn r => map (pair r) (1 upto r))) rss;
1.52 + fun mk_prem_prems_indices raw_pprems =
1.53 + let
1.54 + val rr = length raw_pprems;
1.55 + in
1.56 + map2 (fn pp => fn (xysets, (i, _)) => ((rr, pp), i)) (1 upto rr) raw_pprems
1.57 + end;
1.58 +
1.59 + val ppjjkksss = map (map (mk_prem_prems_indices o #2)) raw_premss;
1.60 +
1.61 +val _ = tracing ("PPJJISSS:\n" ^ PolyML.makestring (ppjjkksss)) (*###*)
1.62
1.63 val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
1.64
1.65 val induct_thm =
1.66 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
1.67 - mk_induct_tac ctxt ns mss ppisss (flat ctr_defss) fld_induct' nested_set_natural's
1.68 - pre_set_defss)
1.69 + mk_induct_tac ctxt ns mss ppjjkksss (flat ctr_defss) fld_induct'
1.70 + nested_set_natural's pre_set_defss)
1.71 |> singleton (Proof_Context.export names_lthy lthy)
1.72 in
1.73 `(conj_dests nn) induct_thm