--- a/src/HOL/Data_Structures/Isin2.thy Tue Sep 22 16:05:19 2015 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy Tue Sep 22 17:13:13 2015 +0200
@@ -13,9 +13,9 @@
"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps dest: sortedD)
+by (induction t) (auto simp: elems_simps2)
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/List_Ins_Del.thy Tue Sep 22 16:05:19 2015 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Tue Sep 22 17:13:13 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>
--- a/src/HOL/Data_Structures/Tree_Set.thy Tue Sep 22 16:05:19 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy Tue Sep 22 17:13:13 2015 +0200
@@ -35,10 +35,10 @@
subsection "Functional Correctness Proofs"
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps0 dest: sortedD)
+by (induction t) (auto simp: elems_simps2)
lemma inorder_insert: