src/HOL/Predicate_Compile_Examples/IMP_4.thy
author blanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 58249 180f1b3508ed
parent 45451 74515e8e6046
child 58310 91ea607a34d8
permissions -rw-r--r--
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
     1 theory IMP_4
     2 imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     3 begin
     4 
     5 subsection {* IMP *}
     6 
     7 text {*
     8   In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
     9 *}
    10 
    11 type_synonym var = nat
    12 type_synonym state = "int list"
    13 
    14 datatype_new com =
    15   Skip |
    16   Ass var "int" |
    17   Seq com com |
    18   IF "state list" com com |
    19   While "state list" com
    20 
    21 inductive exec :: "com => state => state => bool" where
    22   "exec Skip s s" |
    23   "exec (Ass x e) s (s[x := e])" |
    24   "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
    25   "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
    26   "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
    27   "s \<notin> set b ==> exec (While b c) s s" |
    28   "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
    29 
    30 lemma
    31   "exec c s s' ==> exec (Seq c c) s s'"
    32   nitpick (* nitpick fails here! *)
    33   quickcheck[tester = smart_exhaustive, size=2, iterations=100, expect=counterexample]
    34 oops
    35 
    36 end