# HG changeset patch
# User nipkow
# Date 1447757050 -3600
# Node ID cb595e12451d8bd5b66620e3d9978e07235a3414
# Parent  91854ba66adb56e05ccfc5e2a37a17987f70c256
removed lemmas that were only needed for old version of isin.

diff -r 91854ba66adb -r cb595e12451d src/HOL/Data_Structures/Isin2.thy
--- a/src/HOL/Data_Structures/Isin2.thy	Mon Nov 16 19:08:38 2015 +0100
+++ b/src/HOL/Data_Structures/Isin2.thy	Tue Nov 17 11:44:10 2015 +0100
@@ -5,12 +5,17 @@
 theory Isin2
 imports
   Tree2
+  Cmp
   Set_by_Ordered
 begin
 
-fun isin :: "('a,'b) tree \<Rightarrow> ('a::order) \<Rightarrow> bool" where
+fun isin :: "('a::cmp,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
-"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
+"isin (Node _ l a r) x =
+  (case cmp x a of
+     LT \<Rightarrow> isin l x |
+     EQ \<Rightarrow> True |
+     GT \<Rightarrow> isin r x)"
 
 lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
 by (induction t) (auto simp: elems_simps1)
diff -r 91854ba66adb -r cb595e12451d src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Nov 16 19:08:38 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Nov 17 11:44:10 2015 +0100
@@ -31,21 +31,15 @@
 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)
+lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
+by (auto simp: sorted_Cons_iff)
 
-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
+lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
+by (auto simp: sorted_snoc_iff)
 
 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
+lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD
 
 
 subsection \<open>Inserting into an ordered list without duplicates:\<close>