# HG changeset patch
# User haftmann
# Date 1273655879 -7200
# Node ID 5135adb331577626af5be1fc34e73038cf8e333a
# Parent  ce939b5fd77b056f755597635fa455cba72b0a17
added lemmas concerning last, butlast, insort

diff -r ce939b5fd77b -r 5135adb33157 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 11 21:55:41 2010 -0700
+++ b/src/HOL/List.thy	Wed May 12 11:17:59 2010 +0200
@@ -1529,6 +1529,14 @@
 apply(simp add:list_update_append split:nat.splits)
 done
 
+lemma last_map:
+  "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
+  by (cases xs rule: rev_cases) simp_all
+
+lemma map_butlast:
+  "map f (butlast xs) = butlast (map f xs)"
+  by (induct xs) simp_all
+
 
 subsubsection {* @{text take} and @{text drop} *}
 
@@ -2910,6 +2918,14 @@
   "remdups (remdups xs) = remdups xs"
   by (induct xs) simp_all
 
+lemma distinct_butlast:
+  assumes "xs \<noteq> []" and "distinct xs"
+  shows "distinct (butlast xs)"
+proof -
+  from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+  with `distinct xs` show ?thesis by simp
+qed
+
 
 subsubsection {* @{const insert} *}
 
@@ -3605,6 +3621,18 @@
 theorem sorted_sort[simp]: "sorted (sort xs)"
 by(induct xs)(auto simp:sorted_insort)
 
+lemma sorted_butlast:
+  assumes "xs \<noteq> []" and "sorted xs"
+  shows "sorted (butlast xs)"
+proof -
+  from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+  with `sorted xs` show ?thesis by (simp add: sorted_append)
+qed
+  
+lemma insort_not_Nil [simp]:
+  "insort_key f a xs \<noteq> []"
+  by (induct xs) simp_all
+
 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto