# HG changeset patch # User blanchet # Date 1347654190 -7200 # Node ID 19237e4650553fd4eb4ccc090e09bf267f8b1660 # Parent 7003b063a9850c2f03989fde265ea99d4272df97 fixed issue with bound variables in prem prems + tuning diff -r 7003b063a985 -r 19237e465055 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 @@ -565,12 +565,12 @@ | i => [([], (i + 1, x))]) | mk_raw_prem_prems _ _ = []; - fun close_prem_prem (Free x') t = - fold_rev Logic.all - (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t; + fun close_prem_prem xs t = + fold_rev Logic.all (map Free (drop (nn + length xs) + (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t; - fun mk_prem_prem (xysets, (j, x)) = - close_prem_prem x (Logic.list_implies (map (fn (x', (y, set)) => + 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))); @@ -578,14 +578,12 @@ let val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; val pprems = maps (mk_raw_prem_prems names_lthy') xs; - in - (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) - end; + 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, raw_pprems, concl) = - fold_rev Logic.all xs (Logic.list_implies (map mk_prem_prem 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, @@ -598,19 +596,19 @@ val buckets = Library.partition_list has_index 1 nn pprems; val pps = map length buckets; in - map (fn pprem as (_ (*xysets*), (kk, _)) => + map (fn pprem as (xysets, (kk, _)) => ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1), - kk)) pprems + (length xysets, kk))) pprems end; - val ppjjkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss; + val ixsss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss; 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 ppjjkksss (flat ctr_defss) fld_induct' - nested_set_natural's pre_set_defss) + mk_induct_tac ctxt ns mss ixsss (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 7003b063a985 -r 19237e465055 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 @@ -14,7 +14,8 @@ 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) * int) list list list -> thm list -> thm -> thm list -> thm list list -> tactic + ((int * 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; @@ -111,34 +112,37 @@ val induct_prem_prem_thms_delayed = @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]}; +fun mk_induct_prem_prem_endgame_tac ctxt qq = + 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)); + (* TODO: Get rid of the "blast_tac" *) -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, +fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs = + EVERY' (maps (fn ((pp, jj), (qq, 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)), 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 ppjjkks)) 1; + mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ixs)) 1; -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjkks = +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs = EVERY [mk_induct_prepare_prem_tac n m k, - 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]; + mk_induct_prepare_prem_prems_tac (length ixs), atac 1, + mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs]; -fun mk_induct_tac ctxt ns mss ppjjkksss ctr_defs fld_induct' set_natural's pre_set_defss = +fun mk_induct_tac ctxt ns mss ixsss 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 nn n set_natural's) - pre_set_defss mss (unflat mss (1 upto n)) ppjjkksss) + pre_set_defss mss (unflat mss (1 upto n)) ixsss) end; end;