src/HOL/Library/Assert.thy
changeset 27656 d4f6e64ee7cc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Assert.thy	Sat Jul 19 19:27:13 2008 +0200
     1.3 @@ -0,0 +1,51 @@
     1.4 +theory Assert
     1.5 +imports Heap_Monad
     1.6 +begin
     1.7 +
     1.8 +section {* The Assert command *}
     1.9 +
    1.10 +text {* We define a command Assert a property P.
    1.11 + This property does not consider any statement about the heap but only about functional values in the program. *}
    1.12 +
    1.13 +definition
    1.14 +  assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
    1.15 +where
    1.16 +  "assert P x = (if P x then return x else raise (''assert''))"
    1.17 +
    1.18 +lemma assert_cong[fundef_cong]:
    1.19 +assumes "P = P'"
    1.20 +assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
    1.21 +shows "(assert P x >>= f) = (assert P' x >>= f')"
    1.22 +using assms
    1.23 +by (auto simp add: assert_def return_bind raise_bind)
    1.24 +
    1.25 +section {* Example : Using Assert for showing termination of functions *}
    1.26 +
    1.27 +function until_zero :: "int \<Rightarrow> int Heap"
    1.28 +where
    1.29 +  "until_zero a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); until_zero x done))" 
    1.30 +by (pat_completeness, auto)
    1.31 +
    1.32 +termination
    1.33 +apply (relation "measure (\<lambda>x. nat x)")
    1.34 +apply simp
    1.35 +apply simp
    1.36 +oops
    1.37 +
    1.38 +
    1.39 +function until_zero' :: "int \<Rightarrow> int Heap"
    1.40 +where
    1.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))" 
    1.42 +by (pat_completeness, auto)
    1.43 +
    1.44 +termination
    1.45 +apply (relation "measure (\<lambda>x. nat x)")
    1.46 +apply simp
    1.47 +apply simp
    1.48 +done
    1.49 +
    1.50 +hide (open) const until_zero until_zero'
    1.51 +
    1.52 +text {* Also look at lemmas about assert in Relational theory. *}
    1.53 +
    1.54 +end