1.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 06 09:21:15 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 06 09:27:49 2010 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4  
     1.5  subsection{* Function definitions *}
     1.6  
     1.7 -fun res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
     1.8 +primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
     1.9  where
    1.10    "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
    1.11  | "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
    1.12 @@ -419,7 +419,7 @@
    1.13          done)"
    1.14  
    1.15  
    1.16 -fun res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    1.17 +primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    1.18  where
    1.19    "res_thm2 a (l, j) cli =
    1.20    ( if l = 0 then raise(''Illegal literal'')
    1.21 @@ -632,7 +632,7 @@
    1.22  
    1.23  subsection {* Checker functions *}
    1.24  
    1.25 -fun lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
    1.26 +primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
    1.27  where
    1.28    "lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of
    1.29    None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
    1.30 @@ -666,7 +666,7 @@
    1.31  
    1.32  section {* Functional version with RedBlackTrees *}
    1.33  
    1.34 -fun tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    1.35 +primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    1.36  where
    1.37    "tres_thm t (l, j) cli =
    1.38    (case (RBT_Impl.lookup t j) of 

     2.1 --- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:21:15 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:27:49 2010 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4  
     2.5  text {* The remove function removes an element from a sorted list *}
     2.6  
     2.7 -fun remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
     2.8 +primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
     2.9  where
    2.10    "remove a [] = []"
    2.11    |  "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" 
    2.12 @@ -86,16 +86,13 @@
    2.13  apply (auto simp add: sorted_Cons)
    2.14  done
    2.15  
    2.16 -subsection {* Efficient member function for sorted lists: smem *}
    2.17 +subsection {* Efficient member function for sorted lists *}
    2.18  
    2.19 -fun smember :: "('a::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "smem" 55)
    2.20 -where
    2.21 -  "x smem [] = False"
    2.22 -|  "x smem (y#ys) = (if x = y then True else (if (x > y) then x smem ys else False))" 
    2.23 +primrec smember :: "'a list \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
    2.24 +  "smember [] x \<longleftrightarrow> False"
    2.25 +| "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)"
    2.26  
    2.27 -lemma "sorted xs \<Longrightarrow> x smem xs = (x \<in> set xs)" 
    2.28 -apply (induct xs)
    2.29 -apply (auto simp add: sorted_Cons)
    2.30 -done
    2.31 +lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" 
    2.32 +  by (induct xs) (auto simp add: sorted_Cons)
    2.33  
    2.34  end
    2.35 \ No newline at end of file