--- 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"