# HG changeset patch
# User nipkow
# Date 1128461982 -7200
# Node ID 478869f444ca72b4cdb6dbb80145f5afcf1ab5e3
# Parent  2c42d0a94f58ce1512d52242dbf846cd0cd428f7
new hd/rev/last lemmas

diff -r 2c42d0a94f58 -r 478869f444ca src/HOL/List.thy
--- 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