# HG changeset patch # User hoelzl # Date 1273598385 -7200 # Node ID 0f67561ed5a62ff127f063dbd2a3e62c26a61897 # Parent d778c64fc35d2668faf9bc7b621eafac88740d58 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton' diff -r d778c64fc35d -r 0f67561ed5a6 src/HOL/SetInterval.thy --- 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 \ {a .. b} = {a}" by simp + lemma atLeastatMost_subset_iff[simp]: "{a..b} <= {c..d} \ (~ 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} \ a = b \ b = c" +proof + assume "{a..b} = {c}" + hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp + moreover with `{a..b} = {c}` have "c \ a \ b \ c" by auto + ultimately show "a = b \ b = c" by auto +qed simp + end lemma (in linorder) atLeastLessThan_subset_iff: diff -r d778c64fc35d -r 0f67561ed5a6 src/HOL/ex/HarmonicSeries.thy --- 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 "\ = (\n\{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 "\ = 1/2 + 1" by simp