equal
deleted
inserted
replaced
135 by blast |
135 by blast |
136 |
136 |
137 lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)" |
137 lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)" |
138 by simp |
138 by simp |
139 |
139 |
|
140 lemma prod_set_simps: |
|
141 "fsts (x, y) = {x}" |
|
142 "snds (x, y) = {y}" |
|
143 unfolding fsts_def snds_def by simp+ |
|
144 |
|
145 lemma sum_set_simps: |
|
146 "sum_setl (Inl x) = {x}" |
|
147 "sum_setl (Inr x) = {}" |
|
148 "sum_setr (Inl x) = {}" |
|
149 "sum_setr (Inr x) = {x}" |
|
150 unfolding sum_setl_def sum_setr_def by simp+ |
|
151 |
140 lemma induct_set_step: |
152 lemma induct_set_step: |
141 "\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x" |
153 "\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x" |
142 "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C" |
154 "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C" |
143 by blast+ |
155 by blast+ |
144 |
156 |