--- a/src/HOL/IsaMakefile Thu Nov 13 15:58:38 2008 +0100
+++ b/src/HOL/IsaMakefile Thu Nov 13 15:59:33 2008 +0100
@@ -318,7 +318,7 @@
Library/Numeral_Type.thy \
Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy \
Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \
- Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy \
+ Library/Relational.thy Library/Sublist.thy Library/Subarray.thy \
Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy \
Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Library/Assert.thy Thu Nov 13 15:58:38 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-theory Assert
-imports Heap_Monad
-begin
-
-section {* The Assert command *}
-
-text {* We define a command Assert a property P.
- This property does not consider any statement about the heap but only about functional values in the program. *}
-
-definition
- assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
-where
- "assert P x = (if P x then return x else raise (''assert''))"
-
-lemma assert_cong[fundef_cong]:
-assumes "P = P'"
-assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
-shows "(assert P x >>= f) = (assert P' x >>= f')"
-using assms
-by (auto simp add: assert_def return_bind raise_bind)
-
-section {* Example : Using Assert for showing termination of functions *}
-
-function until_zero :: "int \<Rightarrow> int Heap"
-where
- "until_zero a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); until_zero x done))"
-by (pat_completeness, auto)
-
-termination
-apply (relation "measure (\<lambda>x. nat x)")
-apply simp
-apply simp
-oops
-
-
-function until_zero' :: "int \<Rightarrow> int Heap"
-where
- "until_zero' a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); y \<leftarrow> assert (\<lambda>x. x < a) x; until_zero' y done))"
-by (pat_completeness, auto)
-
-termination
-apply (relation "measure (\<lambda>x. nat x)")
-apply simp
-apply simp
-done
-
-hide (open) const until_zero until_zero'
-
-text {* Also look at lemmas about assert in Relational theory. *}
-
-end
--- a/src/HOL/Library/Heap_Monad.thy Thu Nov 13 15:58:38 2008 +0100
+++ b/src/HOL/Library/Heap_Monad.thy Thu Nov 13 15:59:33 2008 +0100
@@ -256,6 +256,17 @@
"foldM f [] s = return s"
| "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
+definition
+ assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
+where
+ "assert P x = (if P x then return x else raise (''assert''))"
+
+lemma assert_cong [fundef_cong]:
+ assumes "P = P'"
+ assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
+ shows "(assert P x >>= f) = (assert P' x >>= f')"
+ using assms by (auto simp add: assert_def return_bind raise_bind)
+
hide (open) const heap execute