# HG changeset patch
# User nipkow
# Date 1442934781 -7200
# Node ID 0b9c45c4af29787d5a5494e7e07e1ba02f3a7b7f
# Parent  1a690dce8cfce5dfdc538ab9bfdec2187cded560
unified isin-proofs

diff -r 1a690dce8cfc -r 0b9c45c4af29 src/HOL/Data_Structures/Isin2.thy
--- a/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 17:13:01 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
diff -r 1a690dce8cfc -r 0b9c45c4af29 src/HOL/Data_Structures/List_Ins_Del.thy
--- 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>
diff -r 1a690dce8cfc -r 0b9c45c4af29 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Tue Sep 22 17:13:01 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: