--- a/src/HOL/Data_Structures/List_Ins_Del.thy Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Tue Sep 22 17:13:01 2015 +0200
@@ -26,15 +26,26 @@
"sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
+text{* The above two rules introduce quantifiers. It turns out
+that in practice this is not a problem because of the simplicity of
+the "isin" functions that implement @{const elems}. Nevertheless
+it is possible to avoid the quantifiers with the help of some rewrite rules: *}
+
lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
by (simp add: sorted_Cons_iff)
lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
by (simp add: sorted_snoc_iff)
-lemmas elems_simps0 = sorted_lems elems_app
-lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff
-lemmas sortedD = sorted_ConsD sorted_snocD
+lemma sorted_ConsD2: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_ConsD by blast
+
+lemma sorted_snocD2: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_snocD by blast
+
+lemmas elems_simps = sorted_lems elems_app
+lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
+lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD sorted_ConsD2 sorted_snocD2
subsection \<open>Inserting into an ordered list without duplicates:\<close>