# HG changeset patch
# User blanchet
# Date 1347617367 -7200
# Node ID c6216518897127270a9072d79c2091655e760c0d
# Parent  9fa21648d0a197ee2ee8e8e320f34b1cc9c611c7
polished the induction

diff -r 9fa21648d0a1 -r c62165188971 src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 14 12:09:27 2012 +0200
@@ -107,6 +107,7 @@
 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+
 
 lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
diff -r 9fa21648d0a1 -r c62165188971 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -496,7 +496,6 @@
         ((wrap, define_iter_likes), lthy')
       end;
 
-    (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there ### *)
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
@@ -572,7 +571,7 @@
               fold_rev Logic.all
                 (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
 
-            fun mk_prem_triple phi ctr ctr_Ts =
+            fun mk_raw_prem phi ctr ctr_Ts =
               let
                 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
                 val prem_prems =
@@ -581,17 +580,17 @@
                 (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
               end;
 
-            val prem_tripless = map3 (map2 o mk_prem_triple) phis ctrss ctr_Tsss;
+            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
 
             fun mk_prem (xs, prem_prems, concl) =
               fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
 
             val goal =
-              Library.foldr (Logic.list_implies o apfst (map mk_prem)) (prem_tripless,
+              Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                   (map2 (curry (op $)) phis vs)));
 
-            val rss = map (map (length o #2)) prem_tripless;
+            val rss = map (map (length o #2)) raw_premss;
 
             val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
 
@@ -672,7 +671,7 @@
     fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
         discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
       let
-        val (vs', names_lthy) =
+        val (vs', _) =
           lthy
           |> Variable.variant_fixes (map Binding.name_of fp_bs);
 
diff -r 9fa21648d0a1 -r c62165188971 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -10,8 +10,8 @@
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
   val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
-  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
-    -> tactic
+  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
+    tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
   val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list ->
     thm -> thm list list -> thm list -> tactic
@@ -95,45 +95,49 @@
   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;
 
-fun mk_induct_prepare_prem_prems_tac _ _ 0 = all_tac
-  | mk_induct_prepare_prem_prems_tac nn kk r =
-    REPEAT_DETERM_N r (rotate_tac (~1 + kk - nn) 1 THEN dtac meta_mp 1 THEN
+fun mk_induct_prepare_prem_prems_tac 0 = all_tac
+  | mk_induct_prepare_prem_prems_tac r =
+    REPEAT_DETERM_N r ((rotate_tac ~1) 1 THEN dtac meta_mp 1 THEN
       defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
     PRIMITIVE Raw_Simplifier.norm_hhf;
 
 val induct_prem_prem_thms =
   @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
-      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv fsts_def[abs_def] image_def
-      map_pair_simp o_apply snd_conv snds_def[abs_def] sum.cases sum_map.simps sum_setl_def[abs_def]
-      sum_setr_def[abs_def] sup_bot_right};
+      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
+      snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
 
+(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
+   delay them. *)
+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 the "blast_tac" *)
 fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's =
   EVERY' (maps (fn i =>
     [dtac meta_spec, rotate_tac ~1, etac meta_mp,
+     SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs),
+     SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
      SELECT_GOAL (Local_Defs.unfold_tac ctxt
-       (set_natural's @ pre_set_defs @ induct_prem_prem_thms)),
-     rtac (mk_UnIN r i),
+       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
+     TRY o rtac (mk_UnIN r i), (* FIXME: crude hack, doesn't work in the general case *)
      atac ORELSE'
      rtac @{thm singletonI} ORELSE'
-     (REPEAT_DETERM o (atac ORELSE'
-        SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
-        etac @{thm induct_set_step}))]) (r downto 1)) 1;
+     (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))]) (r downto 1)) 1;
 
-fun mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's =
+fun mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's =
   EVERY [mk_induct_prepare_prem_tac n m k,
-    mk_induct_prepare_prem_prems_tac nn kk r, atac 1,
+    mk_induct_prepare_prem_prems_tac r, atac 1,
     mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's];
 
 fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's =
-  let
-    val nn = length ns;
-    val n = Integer.sum ns;
-  in
+  let val n = Integer.sum ns in
     mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
-    EVERY (map5 (fn kk => fn pre_set_defs =>
+    EVERY (map4 (fn pre_set_defs =>
         EVERY ooo map3 (fn m => fn k => fn r =>
-            mk_induct_discharge_prem_tac ctxt nn kk n m k r pre_set_defs set_natural's))
-      (1 upto nn) pre_set_defss mss (unflat mss (1 upto Integer.sum ns)) rss)
+            mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's))
+      pre_set_defss mss (unflat mss (1 upto n)) rss)
   end;
 
 end;