# HG changeset patch
# User haftmann
# Date 1272960163 -7200
# Node ID 74a5c04bf29dc34c792589da57c2e92a1c73f78f
# Parent  080b755377c0c8738a8456930a67bcf7010a69e1
avoid if on rhs of default simp rules

diff -r 080b755377c0 -r 74a5c04bf29d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue May 04 08:55:43 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 04 10:02:43 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: