# HG changeset patch # User blanchet # Date 1347654190 -7200 # Node ID c6366fd0415a474a354a61fd8e0653a03b201312 # Parent 993677c1cf2a2709263ed19f3ee1967c76cd7fab select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking diff -r 993677c1cf2a -r c6366fd0415a src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 22:23:10 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 22:23:10 2012 +0200 @@ -562,48 +562,53 @@ in flat (map2 (map o apfst o cons) xysets ppremss) end) - | i => [([], (i, x))]) + | i => [([], (i + 1, x))]) | mk_raw_prem_prems _ _ = []; - fun close_prem_prem x' t = + fun close_prem_prem xs t = fold_rev Logic.all - (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t; + (map Free (drop (2 * nn) (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t; - fun mk_prem_prem x (xysets, (i, x')) = - close_prem_prem (dest_Free x) - (Logic.list_implies (map (fn (x'', (y, set)) => - HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x''))) xysets, - HOLogic.mk_Trueprop (nth phis i $ x'))); + fun mk_prem_prem xs (xysets, (j, x)) = + close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) => + HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets, + HOLogic.mk_Trueprop (nth phis (j - 1) $ x))); fun mk_raw_prem phi ctr ctr_Ts = let val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; - val pprems = - maps (fn x => map (mk_prem_prem x) (mk_raw_prem_prems names_lthy' x)) xs; + val pprems = maps (mk_raw_prem_prems names_lthy') xs; in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end; val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss; - fun mk_prem (xs, pprems, concl) = - fold_rev Logic.all xs (Logic.list_implies (pprems, concl)); + fun mk_prem (xs, raw_pprems, concl) = + fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl)); val goal = Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs))); - (* ### WRONG *) - val rss = map (map (length o #2)) raw_premss; - val ppisss = map (map (fn r => map (pair r) (1 upto r))) rss; + fun mk_prem_prems_indices raw_pprems = + let + val rr = length raw_pprems; + in + map2 (fn pp => fn (xysets, (i, _)) => ((rr, pp), i)) (1 upto rr) raw_pprems + end; + + val ppjjkksss = map (map (mk_prem_prems_indices o #2)) raw_premss; + +val _ = tracing ("PPJJISSS:\n" ^ PolyML.makestring (ppjjkksss)) (*###*) val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); val induct_thm = Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_induct_tac ctxt ns mss ppisss (flat ctr_defss) fld_induct' nested_set_natural's - pre_set_defss) + mk_induct_tac ctxt ns mss ppjjkksss (flat ctr_defss) fld_induct' + nested_set_natural's pre_set_defss) |> singleton (Proof_Context.export names_lthy lthy) in `(conj_dests nn) induct_thm diff -r 993677c1cf2a -r c6366fd0415a src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 22:23:10 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 22:23:10 2012 +0200 @@ -13,8 +13,8 @@ val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic - val mk_induct_tac: Proof.context -> int list -> int list list -> (int * int) list list list -> - thm list -> thm -> thm list -> thm list list -> tactic + val mk_induct_tac: Proof.context -> int list -> int list list -> + ((int * int) * int) list list list -> thm list -> thm -> thm list -> thm list list -> tactic val mk_inject_tac: Proof.context -> thm -> thm -> tactic val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic end; @@ -112,30 +112,33 @@ @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; (* TODO: Get rid of the "blast_tac" *) -fun mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs = - EVERY' (maps (fn (pp, i) => - [(* ### select_prem_tac pp (dtac meta_spec) i, *) dtac meta_spec, rotate_tac ~1, etac meta_mp, +fun mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs = + EVERY' (maps (fn ((pp, jj), kk) => + [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1, etac meta_mp, SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *) SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)), SELECT_GOAL (Local_Defs.unfold_tac ctxt (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)), - TRY o rtac (mk_UnIN pp i), (*#####*) + TRY o rtac (mk_UnIN pp jj), (*#####*) atac ORELSE' rtac @{thm singletonI} ORELSE' (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN' etac @{thm induct_set_step}) THEN' - (atac ORELSE' blast_tac ctxt))]) (rev ppis)) 1; + (atac ORELSE' blast_tac ctxt))]) (rev ppjjkks)) 1; -fun mk_induct_discharge_prem_tac ctxt n set_natural's pre_set_defs m k ppis = +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjkks = EVERY [mk_induct_prepare_prem_tac n m k, - mk_induct_prepare_prem_prems_tac (length ppis), atac 1, - mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs]; + mk_induct_prepare_prem_prems_tac (length ppjjkks), atac 1, + mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs]; -fun mk_induct_tac ctxt ns mss ppisss ctr_defs fld_induct' set_natural's pre_set_defss = - let val n = Integer.sum ns in +fun mk_induct_tac ctxt ns mss ppjjkksss ctr_defs fld_induct' set_natural's pre_set_defss = + let + val nn = length ns; + val n = Integer.sum ns; + in mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN - EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt n set_natural's) - pre_set_defss mss (unflat mss (1 upto n)) ppisss) + EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) + pre_set_defss mss (unflat mss (1 upto n)) ppjjkksss) end; end;