src/HOL/Library/Assert.thy
changeset 28742 07073b1087dd
parent 28741 1b257449f804
child 28743 eda4a5f64f2e
     1.1 --- a/src/HOL/Library/Assert.thy	Thu Nov 13 15:58:38 2008 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,51 +0,0 @@
     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