moved assert to Heap_Monad.thy
authorhaftmann
Thu Nov 13 15:59:33 2008 +0100 (2008-11-13)
changeset 2874207073b1087dd
parent 28741 1b257449f804
child 28743 eda4a5f64f2e
moved assert to Heap_Monad.thy
src/HOL/IsaMakefile
src/HOL/Library/Assert.thy
src/HOL/Library/Heap_Monad.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Nov 13 15:58:38 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Nov 13 15:59:33 2008 +0100
     1.3 @@ -318,7 +318,7 @@
     1.4    Library/Numeral_Type.thy			\
     1.5    Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
     1.6    Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
     1.7 -  Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
     1.8 +  Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
     1.9    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
    1.10    Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
    1.11  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
     2.1 --- a/src/HOL/Library/Assert.thy	Thu Nov 13 15:58:38 2008 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,51 +0,0 @@
     2.4 -theory Assert
     2.5 -imports Heap_Monad
     2.6 -begin
     2.7 -
     2.8 -section {* The Assert command *}
     2.9 -
    2.10 -text {* We define a command Assert a property P.
    2.11 - This property does not consider any statement about the heap but only about functional values in the program. *}
    2.12 -
    2.13 -definition
    2.14 -  assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
    2.15 -where
    2.16 -  "assert P x = (if P x then return x else raise (''assert''))"
    2.17 -
    2.18 -lemma assert_cong[fundef_cong]:
    2.19 -assumes "P = P'"
    2.20 -assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
    2.21 -shows "(assert P x >>= f) = (assert P' x >>= f')"
    2.22 -using assms
    2.23 -by (auto simp add: assert_def return_bind raise_bind)
    2.24 -
    2.25 -section {* Example : Using Assert for showing termination of functions *}
    2.26 -
    2.27 -function until_zero :: "int \<Rightarrow> int Heap"
    2.28 -where
    2.29 -  "until_zero a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); until_zero x done))" 
    2.30 -by (pat_completeness, auto)
    2.31 -
    2.32 -termination
    2.33 -apply (relation "measure (\<lambda>x. nat x)")
    2.34 -apply simp
    2.35 -apply simp
    2.36 -oops
    2.37 -
    2.38 -
    2.39 -function until_zero' :: "int \<Rightarrow> int Heap"
    2.40 -where
    2.41 -  "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))" 
    2.42 -by (pat_completeness, auto)
    2.43 -
    2.44 -termination
    2.45 -apply (relation "measure (\<lambda>x. nat x)")
    2.46 -apply simp
    2.47 -apply simp
    2.48 -done
    2.49 -
    2.50 -hide (open) const until_zero until_zero'
    2.51 -
    2.52 -text {* Also look at lemmas about assert in Relational theory. *}
    2.53 -
    2.54 -end
     3.1 --- a/src/HOL/Library/Heap_Monad.thy	Thu Nov 13 15:58:38 2008 +0100
     3.2 +++ b/src/HOL/Library/Heap_Monad.thy	Thu Nov 13 15:59:33 2008 +0100
     3.3 @@ -256,6 +256,17 @@
     3.4    "foldM f [] s = return s"
     3.5    | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
     3.6  
     3.7 +definition
     3.8 +  assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
     3.9 +where
    3.10 +  "assert P x = (if P x then return x else raise (''assert''))"
    3.11 +
    3.12 +lemma assert_cong [fundef_cong]:
    3.13 +  assumes "P = P'"
    3.14 +  assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
    3.15 +  shows "(assert P x >>= f) = (assert P' x >>= f')"
    3.16 +  using assms by (auto simp add: assert_def return_bind raise_bind)
    3.17 +
    3.18  hide (open) const heap execute
    3.19  
    3.20