Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

--- a/src/HOL/SetInterval.thy	Tue May 11 19:21:39 2010 +0200
+++ b/src/HOL/SetInterval.thy	Tue May 11 19:19:45 2010 +0200
@@ -231,6 +231,8 @@
 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
 
+lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
+
 lemma atLeastatMost_subset_iff[simp]:
   "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
 unfolding atLeastAtMost_def atLeast_def atMost_def
@@ -241,6 +243,15 @@
    ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
 by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
 
+lemma atLeastAtMost_singleton_iff[simp]:
+  "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
+proof
+  assume "{a..b} = {c}"
+  hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
+  moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
+  ultimately show "a = b \<and> b = c" by auto
+qed simp
+
 end
 
 lemma (in linorder) atLeastLessThan_subset_iff:

--- a/src/HOL/ex/HarmonicSeries.thy	Tue May 11 19:21:39 2010 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy	Tue May 11 19:19:45 2010 +0200
@@ -168,13 +168,7 @@
           by simp
         also have
           "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
-        proof -
-          have "(2::nat)^0 = 1" by simp
-          then have "(2::nat)^0+1 = 2" by simp
-          moreover have "(2::nat)^1 = 2" by simp
-          ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto
-          thus ?thesis by simp
-        qed
+          by (auto simp: atLeastAtMost_singleton')
         also have
           "\<dots> = 1/2 + 1"
           by simp