--- 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
--- 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;