changeset 17762 | 478869f444ca |
parent 17724 | e969fc0a4925 |
child 17765 | e3cd31bc2e40 |
--- 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