--- 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
--- 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