--- a/src/HOL/List.thy Sat Mar 06 09:58:30 2010 +0100
+++ b/src/HOL/List.thy Sat Mar 06 09:58:33 2010 +0100
@@ -290,6 +290,9 @@
abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
+definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
+
end
@@ -3703,6 +3706,20 @@
finally show "\<not> t < f x" by simp
qed
+lemma set_insort_insert:
+ "set (insort_insert x xs) = insert x (set xs)"
+ by (auto simp add: insort_insert_def set_insort)
+
+lemma distinct_insort_insert:
+ assumes "distinct xs"
+ shows "distinct (insort_insert x xs)"
+ using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
+
+lemma sorted_insort_insert:
+ assumes "sorted xs"
+ shows "sorted (insort_insert x xs)"
+ using assms by (simp add: insort_insert_def sorted_insort)
+
end
lemma sorted_upt[simp]: "sorted[i..<j]"