equal
deleted
inserted
replaced
202 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P" |
202 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P" |
203 by simp |
203 by simp |
204 |
204 |
205 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} |
205 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} |
206 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}" |
206 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}" |
207 by (erule parts.induct, blast+) |
207 by (erule parts.induct, fast+) |
208 |
208 |
209 |
209 |
210 subsubsection{*Unions *} |
210 subsubsection{*Unions *} |
211 |
211 |
212 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)" |
212 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)" |