# HG changeset patch
# User blanchet
# Date 1484232853 -3600
# Node ID cea327ecb8e332f24b54ccd39a4ee436217a3a2a
# Parent  205274ca16ee141537ba29babf1834abace3e4eb
added lemma

diff -r 205274ca16ee -r cea327ecb8e3 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Thu Jan 12 12:32:32 2017 +0100
+++ b/src/HOL/Library/Sublist.thy	Thu Jan 12 15:54:13 2017 +0100
@@ -92,7 +92,7 @@
   by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI)
 
 lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)"
-  by (metis prefix_order.le_less_trans prefixI strict_prefixE strict_prefixI)
+  unfolding prefix_def by fastforce
 
 lemma append_prefixD: "prefix (xs @ ys) zs \<Longrightarrow> prefix xs zs"
   by (auto simp add: prefix_def)
@@ -766,6 +766,9 @@
 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   by (auto dest: list_emb_length)
 
+lemma sublisteq_singleton_left: "sublisteq [x] ys \<longleftrightarrow> x \<in> set ys"
+  by (fastforce dest: list_emb_ConsD split_list_last)
+
 lemma list_emb_append_mono:
   "\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')"
   apply (induct rule: list_emb.induct)
diff -r 205274ca16ee -r cea327ecb8e3 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jan 12 12:32:32 2017 +0100
+++ b/src/HOL/List.thy	Thu Jan 12 15:54:13 2017 +0100
@@ -4210,7 +4210,7 @@
 lemma enumerate_Suc_eq:
   "enumerate (Suc n) xs = map (apfst Suc) (enumerate n xs)"
   by (rule pair_list_eqI)
-    (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
+    (simp_all add: not_le, simp del: map_map add: map_Suc_upt map_map [symmetric])
 
 lemma distinct_enumerate [simp]:
   "distinct (enumerate n xs)"
@@ -5890,6 +5890,10 @@
 
 end
 
+lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
+  by (induct rule: sorted.induct) (auto dest!: insort_is_Cons)
+
+
 subsubsection \<open>Lexicographic combination of measure functions\<close>
 
 text \<open>These are useful for termination proofs\<close>