# HG changeset patch
# User haftmann
# Date 1278401269 -7200
# Node ID 17b05b104390b990450def62e1e8fe6e17227b7f
# Parent  6d28a2aea936081d51f05cb6f5596b2df273a391
even more fun with primrec

diff -r 6d28a2aea936 -r 17b05b104390 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 06 09:21:15 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 06 09:27:49 2010 +0200
@@ -171,7 +171,7 @@
 
 subsection{* Function definitions *}
 
-fun res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
+primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
   "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
 | "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
@@ -419,7 +419,7 @@
         done)"
 
 
-fun res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
+primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
   "res_thm2 a (l, j) cli =
   ( if l = 0 then raise(''Illegal literal'')
@@ -632,7 +632,7 @@
 
 subsection {* Checker functions *}
 
-fun lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
+primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
 where
   "lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of
   None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
@@ -666,7 +666,7 @@
 
 section {* Functional version with RedBlackTrees *}
 
-fun tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
+primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
   "tres_thm t (l, j) cli =
   (case (RBT_Impl.lookup t j) of 
diff -r 6d28a2aea936 -r 17b05b104390 src/HOL/Imperative_HOL/ex/Sorted_List.thy
--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:21:15 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue Jul 06 09:27:49 2010 +0200
@@ -33,7 +33,7 @@
 
 text {* The remove function removes an element from a sorted list *}
 
-fun remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
+primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "remove a [] = []"
   |  "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" 
@@ -86,16 +86,13 @@
 apply (auto simp add: sorted_Cons)
 done
 
-subsection {* Efficient member function for sorted lists: smem *}
+subsection {* Efficient member function for sorted lists *}
 
-fun smember :: "('a::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "smem" 55)
-where
-  "x smem [] = False"
-|  "x smem (y#ys) = (if x = y then True else (if (x > y) then x smem ys else False))" 
+primrec smember :: "'a list \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
+  "smember [] x \<longleftrightarrow> False"
+| "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)"
 
-lemma "sorted xs \<Longrightarrow> x smem xs = (x \<in> set xs)" 
-apply (induct xs)
-apply (auto simp add: sorted_Cons)
-done
+lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" 
+  by (induct xs) (auto simp add: sorted_Cons)
 
 end
\ No newline at end of file