src/HOL/List.thy
changeset 14589 feae7b5fd425
parent 14565 c6dc17aab88a
child 14591 7be4d5dadf15
equal deleted inserted replaced
14588:29311d81954e 14589:feae7b5fd425
    74 syntax (HTML output)
    74 syntax (HTML output)
    75   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
    75   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
    76 
    76 
    77 
    77 
    78 text {*
    78 text {*
    79   Function @{text size} is overloaded for all datatypes.Users may
    79   Function @{text size} is overloaded for all datatypes. Users may
    80   refer to the list version as @{text length}. *}
    80   refer to the list version as @{text length}. *}
    81 
    81 
    82 syntax length :: "'a list => nat"
    82 syntax length :: "'a list => nat"
    83 translations "length" => "size :: _ list => nat"
    83 translations "length" => "size :: _ list => nat"
    84 
    84 
   791 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
   791 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
   792 by(simp add:last_append)
   792 by(simp add:last_append)
   793 
   793 
   794 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
   794 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
   795 by(simp add:last_append)
   795 by(simp add:last_append)
   796 
       
   797 
   796 
   798 
   797 
   799 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
   798 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
   800 by (induct xs rule: rev_induct) auto
   799 by (induct xs rule: rev_induct) auto
   801 
   800