# 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 \ Clause \ Clause Heap" +primrec res_mem :: "Lit \ Clause \ 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 \ res_mem l xs; return (x # v) done))" @@ -419,7 +419,7 @@ done)" -fun res_thm2 :: "Clause option array \ (Lit * ClauseId) \ Clause \ Clause Heap" +primrec res_thm2 :: "Clause option array \ (Lit * ClauseId) \ Clause \ 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 \ (Lit * ClauseId) \ Clause \ Clause Heap" +primrec lres_thm :: "Clause option list \ (Lit * ClauseId) \ Clause \ Clause Heap" where "lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of None \ 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 \ Lit \ ClauseId \ Clause \ Clause Heap" +primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \ Lit \ ClauseId \ Clause \ 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) \ 'a list \ 'a list" +primrec remove :: "('a :: linorder) \ 'a list \ '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) \ 'a list \ 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 \ 'a::linorder \ bool" where + "smember [] x \ False" +| "smember (y#ys) x \ x = y \ (x > y \ smember ys x)" -lemma "sorted xs \ x smem xs = (x \ set xs)" -apply (induct xs) -apply (auto simp add: sorted_Cons) -done +lemma "sorted xs \ smember xs x \ (x \ set xs)" + by (induct xs) (auto simp add: sorted_Cons) end \ No newline at end of file