--- 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>