1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -123,8 +123,15 @@
     1.4  "\<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.5  by blast
     1.6  
     1.7 +lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
     1.8 +by blast
     1.9 +
    1.10 +lemma eq_UN_compreh_Un: "(xa = \<Union>{y. \<exists>x\<in>A. y = c_set1 x \<union> c_set2 x}) =
    1.11 +  (xa = (\<Union>{y. \<exists>x\<in>A. y = c_set1 x} \<union> \<Union>{y. \<exists>x\<in>A. y = c_set2 x}))"
    1.12 +by blast
    1.13 +
    1.14  lemma mem_compreh_eq_iff:
    1.15 -"z \<in> {y. \<exists>x\<in>Axx. y = f x} = (\<exists> x. x \<in> Axx & z \<in> {f x})"
    1.16 +"z \<in> {y. \<exists>x\<in>A. y = f x} = (\<exists> x. x \<in> A & z \<in> {f x})"
    1.17  by blast
    1.18  
    1.19  lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     2.3 @@ -43,18 +43,19 @@
     2.4  
     2.5  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
     2.6  
     2.7 -fun mk_set_rhs set_lhs T =
     2.8 +fun mk_set_rhs def T =
     2.9    let
    2.10 -    val Type (_, Ts0) = domain_type (fastype_of set_lhs);
    2.11 +    val lhs = snd (Logic.dest_equals (prop_of def));
    2.12 +    val Type (_, Ts0) = domain_type (fastype_of lhs);
    2.13      val Type (_, Ts) = domain_type T;
    2.14    in
    2.15 -    Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
    2.16 +    Term.subst_atomic_types (Ts0 ~~ Ts) lhs
    2.17    end;
    2.18  
    2.19 -val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
    2.20 -val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
    2.21 -val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
    2.22 -val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
    2.23 +val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]};
    2.24 +val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]};
    2.25 +val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]};
    2.26 +val mk_setr_rhs = mk_set_rhs @{thm sum_setr_def[abs_def]};
    2.27  
    2.28  (* TODO: Put this in "Balanced_Tree" *)
    2.29  fun balanced_tree_middle n = n div 2;
    2.30 @@ -66,14 +67,14 @@
    2.31    let
    2.32      fun unf_prod 0 f = f
    2.33        | unf_prod 1 f = f
    2.34 -      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    2.35 -          $ (t7 $ f $ g)) =
    2.36 +      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name fsts}, T1) $
    2.37 +          (t5 $ Const (@{const_name snds}, T2) $ t6)))) $ (t7 $ f $ g)) =
    2.38          t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    2.39            $ (t7 $ f $ unf_prod (m - 1) g)
    2.40        | unf_prod _ f = f;
    2.41      fun unf_sum [m] f = unf_prod m f
    2.42 -      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    2.43 -          $ (t7 $ f $ g)) =
    2.44 +      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name sum_setl}, T1) $
    2.45 +          (t5 $ Const (@{const_name sum_setr}, T2) $ t6)))) $ (t7 $ f $ g)) =
    2.46          let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    2.47            t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    2.48              $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    2.49 @@ -136,18 +137,11 @@
    2.50  
    2.51  val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    2.52  
    2.53 -fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
    2.54 -  | mk_induct_prem_prem_endgame_tac ctxt qq =
    2.55 -    REPEAT_DETERM_N qq o
    2.56 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt
    2.57 -         @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
    2.58 -       eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
    2.59 -
    2.60 -fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
    2.61 -
    2.62 -fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'}
    2.63 -  | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1
    2.64 -  | gen_UnIN_tac n k = gen_UN_comprehI_tac @{thm UnI2} THEN' gen_UnIN_tac (n - 1) (k - 1);
    2.65 +fun solve_prem_prem_tac ctxt =
    2.66 +  SELECT_GOAL (Local_Defs.unfold_tac ctxt
    2.67 +    @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN'
    2.68 +  REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    2.69 +  (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI});
    2.70  
    2.71  val induct_prem_prem_thms =
    2.72    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    2.73 @@ -160,7 +154,7 @@
    2.74      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    2.75       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    2.76         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    2.77 -     gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    2.78 +     solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1;
    2.79  
    2.80  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    2.81    let val r = length ppjjqqkks in