select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
authorblanchet
Fri Sep 14 22:23:10 2012 +0200 (2012-09-14)
changeset 49376c6366fd0415a
parent 49375 993677c1cf2a
child 49377 7003b063a985
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
     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
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
     2.3 @@ -13,8 +13,8 @@
     2.4    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     2.5      tactic
     2.6    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     2.7 -  val mk_induct_tac: Proof.context -> int list -> int list list -> (int * int) list list list ->
     2.8 -    thm list -> thm -> thm list -> thm list list -> tactic
     2.9 +  val mk_induct_tac: Proof.context -> int list -> int list list ->
    2.10 +    ((int * int) * int) list list list -> thm list -> thm -> thm list -> thm list list -> tactic
    2.11    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    2.12    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    2.13  end;
    2.14 @@ -112,30 +112,33 @@
    2.15    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    2.16  
    2.17  (* TODO: Get rid of the "blast_tac" *)
    2.18 -fun mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs =
    2.19 -  EVERY' (maps (fn (pp, i) =>
    2.20 -    [(* ### select_prem_tac pp (dtac meta_spec) i, *) dtac meta_spec, rotate_tac ~1, etac meta_mp,
    2.21 +fun mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs =
    2.22 +  EVERY' (maps (fn ((pp, jj), kk) =>
    2.23 +    [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1, etac meta_mp,
    2.24       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
    2.25       SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    2.26       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    2.27         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    2.28 -     TRY o rtac (mk_UnIN pp i), (*#####*)
    2.29 +     TRY o rtac (mk_UnIN pp jj), (*#####*)
    2.30       atac ORELSE'
    2.31       rtac @{thm singletonI} ORELSE'
    2.32       (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    2.33            etac @{thm induct_set_step}) THEN'
    2.34 -      (atac ORELSE' blast_tac ctxt))]) (rev ppis)) 1;
    2.35 +      (atac ORELSE' blast_tac ctxt))]) (rev ppjjkks)) 1;
    2.36  
    2.37 -fun mk_induct_discharge_prem_tac ctxt n set_natural's pre_set_defs m k ppis =
    2.38 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjkks =
    2.39    EVERY [mk_induct_prepare_prem_tac n m k,
    2.40 -    mk_induct_prepare_prem_prems_tac (length ppis), atac 1,
    2.41 -    mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs];
    2.42 +    mk_induct_prepare_prem_prems_tac (length ppjjkks), atac 1,
    2.43 +    mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs];
    2.44  
    2.45 -fun mk_induct_tac ctxt ns mss ppisss ctr_defs fld_induct' set_natural's pre_set_defss =
    2.46 -  let val n = Integer.sum ns in
    2.47 +fun mk_induct_tac ctxt ns mss ppjjkksss ctr_defs fld_induct' set_natural's pre_set_defss =
    2.48 +  let
    2.49 +    val nn = length ns;
    2.50 +    val n = Integer.sum ns;
    2.51 +  in
    2.52      mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
    2.53 -    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt n set_natural's)
    2.54 -      pre_set_defss mss (unflat mss (1 upto n)) ppisss)
    2.55 +    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
    2.56 +      pre_set_defss mss (unflat mss (1 upto n)) ppjjkksss)
    2.57    end;
    2.58  
    2.59  end;