src/HOL/Library/Assert.thy
author bulwahn
Sat Jul 19 19:27:13 2008 +0200 (2008-07-19)
changeset 27656 d4f6e64ee7cc
permissions -rw-r--r--
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn@27656
     1
theory Assert
bulwahn@27656
     2
imports Heap_Monad
bulwahn@27656
     3
begin
bulwahn@27656
     4
bulwahn@27656
     5
section {* The Assert command *}
bulwahn@27656
     6
bulwahn@27656
     7
text {* We define a command Assert a property P.
bulwahn@27656
     8
 This property does not consider any statement about the heap but only about functional values in the program. *}
bulwahn@27656
     9
bulwahn@27656
    10
definition
bulwahn@27656
    11
  assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
bulwahn@27656
    12
where
bulwahn@27656
    13
  "assert P x = (if P x then return x else raise (''assert''))"
bulwahn@27656
    14
bulwahn@27656
    15
lemma assert_cong[fundef_cong]:
bulwahn@27656
    16
assumes "P = P'"
bulwahn@27656
    17
assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
bulwahn@27656
    18
shows "(assert P x >>= f) = (assert P' x >>= f')"
bulwahn@27656
    19
using assms
bulwahn@27656
    20
by (auto simp add: assert_def return_bind raise_bind)
bulwahn@27656
    21
bulwahn@27656
    22
section {* Example : Using Assert for showing termination of functions *}
bulwahn@27656
    23
bulwahn@27656
    24
function until_zero :: "int \<Rightarrow> int Heap"
bulwahn@27656
    25
where
bulwahn@27656
    26
  "until_zero a = (if a \<le> 0 then return a else (do x \<leftarrow> return (a - 1); until_zero x done))" 
bulwahn@27656
    27
by (pat_completeness, auto)
bulwahn@27656
    28
bulwahn@27656
    29
termination
bulwahn@27656
    30
apply (relation "measure (\<lambda>x. nat x)")
bulwahn@27656
    31
apply simp
bulwahn@27656
    32
apply simp
bulwahn@27656
    33
oops
bulwahn@27656
    34
bulwahn@27656
    35
bulwahn@27656
    36
function until_zero' :: "int \<Rightarrow> int Heap"
bulwahn@27656
    37
where
bulwahn@27656
    38
  "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
    39
by (pat_completeness, auto)
bulwahn@27656
    40
bulwahn@27656
    41
termination
bulwahn@27656
    42
apply (relation "measure (\<lambda>x. nat x)")
bulwahn@27656
    43
apply simp
bulwahn@27656
    44
apply simp
bulwahn@27656
    45
done
bulwahn@27656
    46
bulwahn@27656
    47
hide (open) const until_zero until_zero'
bulwahn@27656
    48
bulwahn@27656
    49
text {* Also look at lemmas about assert in Relational theory. *}
bulwahn@27656
    50
bulwahn@27656
    51
end