# HG changeset patch
# User blanchet
# Date 1347736226 -7200
# Node ID da621dc65146775748f07bd0fc116a25d55492f3
# Parent  1ffd5a055acf65f7b7db9af05ba1246c7fd80323
tuning

diff -r 1ffd5a055acf -r da621dc65146 src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 20:14:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Sat Sep 15 21:10:26 2012 +0200
@@ -104,10 +104,8 @@
 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
 by simp
 
-(* TODO: cleanup *)
 lemma UN_compreh_bex:
 "\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
-"\<Union>{y. \<exists>x \<in> A. y = {x}} = A"
 "\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
 by blast+
 
diff -r 1ffd5a055acf -r da621dc65146 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 20:14:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
-Sugar for constructing LFPs and GFPs.
+Sugared datatype and codatatype constructions.
 *)
 
 signature BNF_FP_SUGAR =
@@ -580,11 +580,11 @@
                 val pprems = maps (mk_raw_prem_prems names_lthy') xs;
               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 xs) raw_pprems, concl));
 
+            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
+
             val goal =
               Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -601,14 +601,14 @@
                    (length xysets, kk))) pprems
               end;
 
-            val ixsss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
+            val ppjjqqkksss = 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 ixsss (flat ctr_defss) fld_induct' nested_set_natural's
-                  pre_set_defss)
+                mk_induct_tac ctxt ns mss ppjjqqkksss (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 1ffd5a055acf -r da621dc65146 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 20:14:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
-Tactics for the LFP/GFP sugar.
+Tactics for datatype and codatatype sugar.
 *)
 
 signature BNF_FP_SUGAR_TACTICS =
@@ -30,6 +30,9 @@
 val meta_mp = @{thm meta_mp};
 val meta_spec = @{thm meta_spec};
 
+(* FIXME: why not in "Pure"? *)
+fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
+
 fun smash_spurious_fs lthy thm =
   let
     val fs =
@@ -88,19 +91,14 @@
   Local_Defs.unfold_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
 
-fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
-  Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt;
-
-fun mk_induct_prepare_prem_tac n m k =
-  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
-    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
+(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
 
-(* FIXME: why not in "Pure"? *)
-fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
-
-fun mk_induct_prepare_prem_prems_tac r =
-  REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2) THEN
-  PRIMITIVE Raw_Simplifier.norm_hhf;
+fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
+  | mk_induct_prem_prem_endgame_tac ctxt qq =
+    REPEAT_DETERM_N qq o
+      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
+       etac @{thm induct_set_step}) THEN'
+    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
 
 val induct_prem_prem_thms =
   @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
@@ -112,38 +110,32 @@
 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]};
 
-(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
-fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
-  | mk_induct_prem_prem_endgame_tac ctxt qq =
-    REPEAT_DETERM_N qq o
-      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
-       etac @{thm induct_set_step}) THEN'
-    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
-
-fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
+fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
   EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
-      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
-       SELECT_GOAL (Local_Defs.unfold_tac ctxt
-         (pre_set_defs @ 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) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
-         SELECT_GOAL (auto_tac ctxt)])
-    (rev ixs)) 1;
+    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
+     SELECT_GOAL (Local_Defs.unfold_tac ctxt
+       (pre_set_defs @ 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) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
+       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
 
-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 ixs), atac 1,
-    mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs];
+fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
+  EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
+    REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
+  EVERY [REPEAT_DETERM_N (length ppjjqqkks)
+      (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
+    PRIMITIVE Raw_Simplifier.norm_hhf, atac 1,
+    mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs];
 
-fun mk_induct_tac ctxt ns mss ixsss ctr_defs fld_induct' set_natural's pre_set_defss =
+fun mk_induct_tac ctxt ns mss ppjjqqkksss 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
+    Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt 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)) ixsss)
+      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
   end;
 
 end;
diff -r 1ffd5a055acf -r da621dc65146 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 20:14:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -2,7 +2,7 @@
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
-Shared library for the datatype and the codatatype construction.
+Shared library for the datatype and codatatype constructions.
 *)
 
 signature BNF_FP_UTIL =