src/HOL/SetInterval.thy
 changeset 36846 0f67561ed5a6 parent 36755 d1b498f2f50b child 37388 793618618f78
```     1.1 --- a/src/HOL/SetInterval.thy	Tue May 11 19:21:39 2010 +0200
1.2 +++ b/src/HOL/SetInterval.thy	Tue May 11 19:19:45 2010 +0200
1.3 @@ -231,6 +231,8 @@
1.4  lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
1.5  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
1.6
1.7 +lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
1.8 +
1.9  lemma atLeastatMost_subset_iff[simp]:
1.10    "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
1.11  unfolding atLeastAtMost_def atLeast_def atMost_def
1.12 @@ -241,6 +243,15 @@
1.13     ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
1.14  by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
1.15
1.16 +lemma atLeastAtMost_singleton_iff[simp]:
1.17 +  "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
1.18 +proof
1.19 +  assume "{a..b} = {c}"
1.20 +  hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
1.21 +  moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
1.22 +  ultimately show "a = b \<and> b = c" by auto
1.23 +qed simp
1.24 +
1.25  end
1.26
1.27  lemma (in linorder) atLeastLessThan_subset_iff:
```