1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 16:57:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -104,11 +104,25 @@
     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 -lemma UN_compreh_bex:
     1.8 -"\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
     1.9 -"\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
    1.10 +lemma UN_compreh_bex_eq_empty:
    1.11 +"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
    1.12 +by blast
    1.13 +
    1.14 +lemma UN_compreh_bex_eq_singleton:
    1.15 +"\<Union>{y. \<exists>x\<in>A. y = {f x}} = {y. \<exists>x\<in>A. y = f x}"
    1.16 +by blast
    1.17 +
    1.18 +lemma mem_UN_comprehI:
    1.19 +"z \<in> {y. \<exists>x\<in>A. y = f x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}}"
    1.20 +"z \<in> {y. \<exists>x\<in>A. y = f x} \<union> B \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}} \<union> B"
    1.21 +"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> \<Union>{y. \<exists>x\<in>A. y = G x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x}"
    1.22 +"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> (\<Union>{y. \<exists>x\<in>A. y = G x} \<union> B) \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x} \<union> B"
    1.23  by blast+
    1.24  
    1.25 +lemma mem_UN_comprehI':
    1.26 +"\<exists>y. (\<exists>x\<in>A. y = F x) \<and> z \<in> y \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {y. \<exists>y'\<in>F x. y = y'}}"
    1.27 +by blast
    1.28 +
    1.29  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"
    1.30  apply (rule exI)
    1.31  apply (rule conjI)

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 16:57:22 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
     2.3 @@ -499,7 +499,9 @@
     2.4      val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
     2.5  
     2.6      fun mk_map live Ts Us t =
     2.7 -      let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
     2.8 +      let
     2.9 +        val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last
    2.10 +      in
    2.11          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    2.12        end;
    2.13  

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 16:57:22 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     3.3 @@ -97,10 +97,17 @@
     3.4         etac @{thm induct_set_step}) THEN'
     3.5      atac ORELSE' SELECT_GOAL (auto_tac ctxt);
     3.6  
     3.7 +fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
     3.8 +
     3.9 +fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'}
    3.10 +  | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1
    3.11 +  | gen_UnIN_tac n k = gen_UN_comprehI_tac @{thm UnI2} THEN' gen_UnIN_tac (n - 1) (k - 1);
    3.12 +
    3.13  val induct_prem_prem_thms =
    3.14 -  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    3.15 -      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
    3.16 -      snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
    3.17 +  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    3.18 +      UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv
    3.19 +      image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    3.20 +      sum_map.simps};
    3.21  
    3.22  (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
    3.23     delay them. *)
    3.24 @@ -114,8 +121,7 @@
    3.25         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    3.26       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.27         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    3.28 -     rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    3.29 -       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
    3.30 +     gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    3.31  
    3.32  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    3.33    let val r = length ppjjqqkks in