--- a/src/HOL/SetInterval.thy Mon Jun 06 14:11:54 2011 +0200
+++ b/src/HOL/SetInterval.thy Mon Jun 06 16:29:13 2011 +0200
@@ -461,6 +461,12 @@
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
by (auto simp add: atLeastAtMost_def)
+text {* The analogous result is useful on @{typ int}: *}
+(* here, because we don't have an own int section *)
+lemma atLeastAtMostPlus1_int_conv:
+ "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
+ by (auto intro: set_eqI)
+
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
apply (induct k)
apply (simp_all add: atLeastLessThanSuc)