# HG changeset patch
# User kleing
# Date 1307370553 -7200
# Node ID b505be6f029a4f21a737a5dae55b80e91a3267bd
# Parent  04aaac80183f7093aee97106d94e7c691ea3552b
atLeastAtMostSuc_conv on int

diff -r 04aaac80183f -r b505be6f029a src/HOL/SetInterval.thy
--- 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)