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: