1.1 --- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:21:15 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:27:49 2010 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  text {* The remove function removes an element from a sorted list *}
     1.6  
     1.7 -fun remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
     1.8 +primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
     1.9  where
    1.10    "remove a [] = []"
    1.11    |  "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" 
    1.12 @@ -86,16 +86,13 @@
    1.13  apply (auto simp add: sorted_Cons)
    1.14  done
    1.15  
    1.16 -subsection {* Efficient member function for sorted lists: smem *}
    1.17 +subsection {* Efficient member function for sorted lists *}
    1.18  
    1.19 -fun smember :: "('a::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "smem" 55)
    1.20 -where
    1.21 -  "x smem [] = False"
    1.22 -|  "x smem (y#ys) = (if x = y then True else (if (x > y) then x smem ys else False))" 
    1.23 +primrec smember :: "'a list \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
    1.24 +  "smember [] x \<longleftrightarrow> False"
    1.25 +| "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)"
    1.26  
    1.27 -lemma "sorted xs \<Longrightarrow> x smem xs = (x \<in> set xs)" 
    1.28 -apply (induct xs)
    1.29 -apply (auto simp add: sorted_Cons)
    1.30 -done
    1.31 +lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" 
    1.32 +  by (induct xs) (auto simp add: sorted_Cons)
    1.33  
    1.34  end
    1.35 \ No newline at end of file