added last in set lemma
authornipkow
Wed Oct 05 14:01:32 2005 +0200 (2005-10-05 ago)
changeset 17765e3cd31bc2e40
parent 17764 fde495b9e24b
child 17766 10319da54a47
added last in set lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Oct 05 11:18:06 2005 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 05 14:01:32 2005 +0200
     1.3 @@ -994,13 +994,14 @@
     1.4  lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
     1.5  by(simp add:last_append)
     1.6  
     1.7 -
     1.8  lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
     1.9  by(rule rev_exhaust[of xs]) simp_all
    1.10  
    1.11  lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
    1.12  by(cases xs) simp_all
    1.13  
    1.14 +lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
    1.15 +by (induct as) auto
    1.16  
    1.17  lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
    1.18  by (induct xs rule: rev_induct) auto