# HG changeset patch # User blanchet # Date 1347654190 -7200 # Node ID 993677c1cf2a2709263ed19f3ee1967c76cd7fab # Parent b08c6312782b2b6282f261d5e4f8f76909cfcc4b tuned code before fixing "mk_induct_discharge_prem_prems_tac" diff -r b08c6312782b -r 993677c1cf2a src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 21:26:01 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 22:23:10 2012 +0200 @@ -546,7 +546,7 @@ Term.subst_atomic_types (Ts0 ~~ Ts) t end; - fun mk_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) = + fun mk_raw_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) = (case find_index (curry (op =) T) fpTs of ~1 => (case AList.lookup (op =) setss_nested T_name of @@ -557,47 +557,53 @@ split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0)); val sets = map (mk_set Ts0) raw_sets; val (ys, names_lthy') = names_lthy |> mk_Frees s Ts; - val heads = - map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x))) - ys sets; - val bodiess = map (mk_prem_prems names_lthy') ys; + val xysets = map (pair x) (ys ~~ sets); + val ppremss = map (mk_raw_prem_prems names_lthy') ys; in - flat (map2 (map o curry Logic.mk_implies) heads bodiess) + flat (map2 (map o apfst o cons) xysets ppremss) end) - | i => [HOLogic.mk_Trueprop (nth phis i $ x)]) - | mk_prem_prems _ _ = []; + | i => [([], (i, x))]) + | mk_raw_prem_prems _ _ = []; - fun close_prem_prem (Free x') t = + fun close_prem_prem x' t = fold_rev Logic.all (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: 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_raw_prem phi ctr ctr_Ts = let val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; - val prem_prems = - maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs; + val pprems = + maps (fn x => map (mk_prem_prem x) (mk_raw_prem_prems names_lthy' x)) xs; in - (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) + (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, prem_prems, concl) = - fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl)); + fun mk_prem (xs, pprems, concl) = + fold_rev Logic.all xs (Logic.list_implies (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; 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 rss (flat ctr_defss) fld_induct' pre_set_defss - nested_set_natural's) + mk_induct_tac ctxt ns mss ppisss (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 b08c6312782b -r 993677c1cf2a src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 21:26:01 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 list list -> thm list -> - thm -> thm list list -> 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_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,32 +112,30 @@ @{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 r pre_set_defs set_natural's = - EVERY' (maps (fn i => - [dtac meta_spec, rotate_tac ~1, etac meta_mp, - SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), +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, + 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 r i), (* FIXME: crude hack, doesn't work in the general case *) + TRY o rtac (mk_UnIN pp i), (*#####*) 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))]) (r downto 1)) 1; + (atac ORELSE' blast_tac ctxt))]) (rev ppis)) 1; -fun mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's = +fun mk_induct_discharge_prem_tac ctxt n set_natural's pre_set_defs m k ppis = EVERY [mk_induct_prepare_prem_tac n m k, - mk_induct_prepare_prem_prems_tac r, atac 1, - mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's]; + mk_induct_prepare_prem_prems_tac (length ppis), atac 1, + mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs]; -fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's = +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 mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN - EVERY (map4 (fn pre_set_defs => - EVERY ooo map3 (fn m => fn k => fn r => - mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's)) - pre_set_defss mss (unflat mss (1 upto n)) rss) + 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) end; end;