# HG changeset patch
# User hoelzl
# Date 1283415272 -7200
# Node ID 1030b1a166efb0380630fd1afab8e37e5c4c8671
# Parent  caad9d509bc4036826b20739e660922cb93ae814
Add lessThan_Suc_eq_insert_0

diff -r caad9d509bc4 -r 1030b1a166ef src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Sep 02 09:13:28 2010 +0200
+++ b/src/HOL/SetInterval.thy	Thu Sep 02 10:14:32 2010 +0200
@@ -304,6 +304,17 @@
 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
 by (simp add: lessThan_def less_Suc_eq, blast)
 
+text {* The following proof is convinient in induction proofs where
+new elements get indices at the beginning. So it is used to transform
+@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
+
+lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
+proof safe
+  fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
+  then have "x \<noteq> Suc (x - 1)" by auto
+  with `x < Suc n` show "x = 0" by auto
+qed
+
 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
 by (simp add: lessThan_def atMost_def less_Suc_eq_le)