new hd/rev/last lemmas

--- a/src/HOL/List.thy	Tue Oct 04 23:30:46 2005 +0200
+++ b/src/HOL/List.thy	Tue Oct 04 23:39:42 2005 +0200
@@ -995,6 +995,13 @@
 by(simp add:last_append)
 
 
+lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
+by(rule rev_exhaust[of xs]) simp_all
+
+lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
+by(cases xs) simp_all
+
+
 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
 by (induct xs rule: rev_induct) auto