bulwahn@27656: theory Assert
bulwahn@27656: imports Heap_Monad
bulwahn@27656: begin
bulwahn@27656: 
bulwahn@27656: section {* The Assert command *}
bulwahn@27656: 
bulwahn@27656: text {* We define a command Assert a property P.
bulwahn@27656:  This property does not consider any statement about the heap but only about functional values in the program. *}
bulwahn@27656: 
bulwahn@27656: definition
bulwahn@27656:   assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
bulwahn@27656: where
bulwahn@27656:   "assert P x = (if P x then return x else raise (''assert''))"
bulwahn@27656: 
bulwahn@27656: lemma assert_cong[fundef_cong]:
bulwahn@27656: assumes "P = P'"
bulwahn@27656: assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
bulwahn@27656: shows "(assert P x >>= f) = (assert P' x >>= f')"
bulwahn@27656: using assms
bulwahn@27656: by (auto simp add: assert_def return_bind raise_bind)
bulwahn@27656: 
bulwahn@27656: section {* Example : Using Assert for showing termination of functions *}
bulwahn@27656: 
bulwahn@27656: function until_zero :: "int \<Rightarrow> int Heap"
bulwahn@27656: where
bulwahn@27656:   "until_zero a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); until_zero x done))" 
bulwahn@27656: by (pat_completeness, auto)
bulwahn@27656: 
bulwahn@27656: termination
bulwahn@27656: apply (relation "measure (\<lambda>x. nat x)")
bulwahn@27656: apply simp
bulwahn@27656: apply simp
bulwahn@27656: oops
bulwahn@27656: 
bulwahn@27656: 
bulwahn@27656: function until_zero' :: "int \<Rightarrow> int Heap"
bulwahn@27656: where
bulwahn@27656:   "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))" 
bulwahn@27656: by (pat_completeness, auto)
bulwahn@27656: 
bulwahn@27656: termination
bulwahn@27656: apply (relation "measure (\<lambda>x. nat x)")
bulwahn@27656: apply simp
bulwahn@27656: apply simp
bulwahn@27656: done
bulwahn@27656: 
bulwahn@27656: hide (open) const until_zero until_zero'
bulwahn@27656: 
bulwahn@27656: text {* Also look at lemmas about assert in Relational theory. *}
bulwahn@27656: 
bulwahn@27656: end