author haftmann Tue, 04 May 2010 10:49:46 +0200 changeset 36638 4fed34e1dddd parent 36636 7dded80a953f (current diff) parent 36637 74a5c04bf29d (diff) child 36639 6243b49498ea
merged
```--- a/src/HOL/Finite_Set.thy	Tue May 04 09:25:38 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 04 10:49:46 2010 +0200
@@ -1729,12 +1729,10 @@
qed

lemma insert [simp]:
-  assumes "finite A" and "x \<notin> A"
-  shows "F (insert x A) = (if A = {} then x else x * F A)"
-proof (cases "A = {}")
-  case True then show ?thesis by simp
-next
-  case False then obtain b where "b \<in> A" by blast
+  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
+  shows "F (insert x A) = x * F A"
+proof -
+  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` have "finite B" by simp
interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
@@ -1828,8 +1826,6 @@
(simp_all add: assoc in_idem `finite A`)
qed

-declare insert [simp del]
-
lemma eq_fold_idem':
assumes "finite A"
shows "F (insert a A) = fold (op *) a A"
@@ -1839,13 +1835,13 @@
qed

lemma insert_idem [simp]:
-  assumes "finite A"
-  shows "F (insert x A) = (if A = {} then x else x * F A)"
+  assumes "finite A" and "A \<noteq> {}"
+  shows "F (insert x A) = x * F A"
proof (cases "x \<in> A")
-  case False with `finite A` show ?thesis by (rule insert)
+  case False from `finite A` `x \<notin> A` `A \<noteq> {}` show ?thesis by (rule insert)
next
-  case True then have "A \<noteq> {}" by auto
-  with `finite A` show ?thesis by (simp add: in_idem insert_absorb True)
+  case True
+  from `finite A` `A \<noteq> {}` show ?thesis by (simp add: in_idem insert_absorb True)
qed

lemma union_idem:```