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 @@ -137,6 +137,18 @@
     1.4  lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
     1.5  by simp
     1.6  
     1.7 +lemma prod_set_simps:
     1.8 +"fsts (x, y) = {x}"
     1.9 +"snds (x, y) = {y}"
    1.10 +unfolding fsts_def snds_def by simp+
    1.11 +
    1.12 +lemma sum_set_simps:
    1.13 +"sum_setl (Inl x) = {x}"
    1.14 +"sum_setl (Inr x) = {}"
    1.15 +"sum_setr (Inl x) = {}"
    1.16 +"sum_setr (Inr x) = {x}"
    1.17 +unfolding sum_setl_def sum_setr_def by simp+
    1.18 +
    1.19  lemma induct_set_step:
    1.20  "\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
    1.21  "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"