equal
deleted
inserted
replaced
120 |
120 |
121 lemma finite_insert [simp]: "finite (insert a A) = finite A" |
121 lemma finite_insert [simp]: "finite (insert a A) = finite A" |
122 apply (subst insert_is_Un) |
122 apply (subst insert_is_Un) |
123 apply (simp only: finite_Un, blast) |
123 apply (simp only: finite_Un, blast) |
124 done |
124 done |
|
125 |
|
126 lemma finite_Union[simp, intro]: |
|
127 "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" |
|
128 by (induct rule:finite_induct) simp_all |
125 |
129 |
126 lemma finite_empty_induct: |
130 lemma finite_empty_induct: |
127 "finite A ==> |
131 "finite A ==> |
128 P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}" |
132 P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}" |
129 proof - |
133 proof - |