src/HOL/Predicate_Compile_Examples/IMP_4.thy
author wenzelm
Sat Apr 23 13:00:19 2011 +0200 (2011-04-23)
changeset 42463 f270e3e18be5
parent 41413 64cd30d6b0b8
child 43686 bc7d63c7fd6f
permissions -rw-r--r--
modernized specifications;
bulwahn@39186
     1
theory IMP_4
wenzelm@41413
     2
imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
bulwahn@39186
     3
begin
bulwahn@39186
     4
bulwahn@39186
     5
subsection {* IMP *}
bulwahn@39186
     6
bulwahn@39186
     7
text {*
bulwahn@39186
     8
  In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
bulwahn@39186
     9
*}
bulwahn@39186
    10
wenzelm@42463
    11
type_synonym var = nat
wenzelm@42463
    12
type_synonym state = "int list"
bulwahn@39186
    13
bulwahn@39186
    14
datatype com =
bulwahn@39186
    15
  Skip |
bulwahn@39186
    16
  Ass var "int" |
bulwahn@39186
    17
  Seq com com |
bulwahn@39186
    18
  IF "state list" com com |
bulwahn@39186
    19
  While "state list" com
bulwahn@39186
    20
bulwahn@39186
    21
inductive exec :: "com => state => state => bool" where
bulwahn@39186
    22
  "exec Skip s s" |
bulwahn@39186
    23
  "exec (Ass x e) s (s[x := e])" |
bulwahn@39186
    24
  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
bulwahn@39186
    25
  "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
bulwahn@39186
    26
  "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
bulwahn@39186
    27
  "s \<notin> set b ==> exec (While b c) s s" |
bulwahn@39186
    28
  "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
bulwahn@39186
    29
bulwahn@39186
    30
lemma
bulwahn@39186
    31
  "exec c s s' ==> exec (Seq c c) s s'"
bulwahn@39186
    32
  nitpick (* nitpick fails here! *)
bulwahn@40924
    33
  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
bulwahn@39186
    34
oops
bulwahn@39186
    35
bulwahn@39186
    36
end