tuning
authorblanchet
Sat Sep 15 21:10:26 2012 +0200 (2012-09-15)
changeset 49389da621dc65146
parent 49388 1ffd5a055acf
child 49390 a4202c1f4f9d
tuning
src/HOL/Codatatype/BNF_FP.thy
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
     1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 20:14:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -104,10 +104,8 @@
     1.4  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 -(* TODO: cleanup *)
     1.8  lemma UN_compreh_bex:
     1.9  "\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
    1.10 -"\<Union>{y. \<exists>x \<in> A. y = {x}} = A"
    1.11  "\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
    1.12  by blast+
    1.13  
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 20:14:29 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Jasmin Blanchette, TU Muenchen
     2.5      Copyright   2012
     2.6  
     2.7 -Sugar for constructing LFPs and GFPs.
     2.8 +Sugared datatype and codatatype constructions.
     2.9  *)
    2.10  
    2.11  signature BNF_FP_SUGAR =
    2.12 @@ -580,11 +580,11 @@
    2.13                  val pprems = maps (mk_raw_prem_prems names_lthy') xs;
    2.14                in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
    2.15  
    2.16 -            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    2.17 -
    2.18              fun mk_prem (xs, raw_pprems, concl) =
    2.19                fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
    2.20  
    2.21 +            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
    2.22 +
    2.23              val goal =
    2.24                Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
    2.25                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    2.26 @@ -601,14 +601,14 @@
    2.27                     (length xysets, kk))) pprems
    2.28                end;
    2.29  
    2.30 -            val ixsss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    2.31 +            val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    2.32  
    2.33              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    2.34  
    2.35              val induct_thm =
    2.36                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    2.37 -                mk_induct_tac ctxt ns mss ixsss (flat ctr_defss) fld_induct' nested_set_natural's
    2.38 -                  pre_set_defss)
    2.39 +                mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
    2.40 +                  nested_set_natural's pre_set_defss)
    2.41                |> singleton (Proof_Context.export names_lthy lthy)
    2.42            in
    2.43              `(conj_dests nn) induct_thm
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 20:14:29 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 21:10:26 2012 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Jasmin Blanchette, TU Muenchen
     3.5      Copyright   2012
     3.6  
     3.7 -Tactics for the LFP/GFP sugar.
     3.8 +Tactics for datatype and codatatype sugar.
     3.9  *)
    3.10  
    3.11  signature BNF_FP_SUGAR_TACTICS =
    3.12 @@ -30,6 +30,9 @@
    3.13  val meta_mp = @{thm meta_mp};
    3.14  val meta_spec = @{thm meta_spec};
    3.15  
    3.16 +(* FIXME: why not in "Pure"? *)
    3.17 +fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    3.18 +
    3.19  fun smash_spurious_fs lthy thm =
    3.20    let
    3.21      val fs =
    3.22 @@ -88,19 +91,14 @@
    3.23    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    3.24    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    3.25  
    3.26 -fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
    3.27 -  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt;
    3.28 -
    3.29 -fun mk_induct_prepare_prem_tac n m k =
    3.30 -  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    3.31 -    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
    3.32 +(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    3.33  
    3.34 -(* FIXME: why not in "Pure"? *)
    3.35 -fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
    3.36 -
    3.37 -fun mk_induct_prepare_prem_prems_tac r =
    3.38 -  REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2) THEN
    3.39 -  PRIMITIVE Raw_Simplifier.norm_hhf;
    3.40 +fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    3.41 +  | mk_induct_prem_prem_endgame_tac ctxt qq =
    3.42 +    REPEAT_DETERM_N qq o
    3.43 +      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    3.44 +       etac @{thm induct_set_step}) THEN'
    3.45 +    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    3.46  
    3.47  val induct_prem_prem_thms =
    3.48    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    3.49 @@ -112,38 +110,32 @@
    3.50  val induct_prem_prem_thms_delayed =
    3.51    @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    3.52  
    3.53 -(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    3.54 -fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    3.55 -  | mk_induct_prem_prem_endgame_tac ctxt qq =
    3.56 -    REPEAT_DETERM_N qq o
    3.57 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    3.58 -       etac @{thm induct_set_step}) THEN'
    3.59 -    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    3.60 -
    3.61 -fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    3.62 +fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    3.63    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    3.64 -      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    3.65 -       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.66 -         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    3.67 -       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.68 -         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    3.69 -       rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    3.70 -         SELECT_GOAL (auto_tac ctxt)])
    3.71 -    (rev ixs)) 1;
    3.72 +    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    3.73 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.74 +       (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    3.75 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.76 +       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    3.77 +     rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    3.78 +       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
    3.79  
    3.80 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =
    3.81 -  EVERY [mk_induct_prepare_prem_tac n m k,
    3.82 -    mk_induct_prepare_prem_prems_tac (length ixs), atac 1,
    3.83 -    mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs];
    3.84 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    3.85 +  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    3.86 +    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
    3.87 +  EVERY [REPEAT_DETERM_N (length ppjjqqkks)
    3.88 +      (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
    3.89 +    PRIMITIVE Raw_Simplifier.norm_hhf, atac 1,
    3.90 +    mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs];
    3.91  
    3.92 -fun mk_induct_tac ctxt ns mss ixsss ctr_defs fld_induct' set_natural's pre_set_defss =
    3.93 +fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
    3.94    let
    3.95      val nn = length ns;
    3.96      val n = Integer.sum ns;
    3.97    in
    3.98 -    mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
    3.99 +    Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt THEN
   3.100      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   3.101 -      pre_set_defss mss (unflat mss (1 upto n)) ixsss)
   3.102 +      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
   3.103    end;
   3.104  
   3.105  end;
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 20:14:29 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 21:10:26 2012 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4      Author:     Dmitriy Traytel, TU Muenchen
     4.5      Copyright   2012
     4.6  
     4.7 -Shared library for the datatype and the codatatype construction.
     4.8 +Shared library for the datatype and codatatype constructions.
     4.9  *)
    4.10  
    4.11  signature BNF_FP_UTIL =