# HG changeset patch
# User nipkow
# Date 1129697205 -7200
# Node ID 719364f5179b29d790ce11ffa6cbbffe34cf01aa
# Parent  1574533861b1df4585cd3cb0ac44020c0e741afa
added 2 lemmas

diff -r 1574533861b1 -r 719364f5179b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 19 06:33:24 2005 +0200
+++ b/src/HOL/List.thy	Wed Oct 19 06:46:45 2005 +0200
@@ -1566,6 +1566,15 @@
 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
 done
 
+
+lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
+by(simp add:upt_conv_Cons)
+
+lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
+apply(cases j)
+ apply simp
+by(simp add:upt_Suc_append)
+
 lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..<n] = [i..<i+m]"
 apply (induct m, simp)
 apply (subst upt_rec)
@@ -1773,6 +1782,11 @@
 done
 
 
+lemma nth_eq_iff_index_eq:
+ "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
+by(auto simp: distinct_conv_nth)
+
+
 subsubsection {* @{text remove1} *}
 
 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"