src/HOL/Predicate_Compile_Examples/IMP_1.thy
author bulwahn
Wed Jul 06 13:52:42 2011 +0200 (2011-07-06)
changeset 43686 bc7d63c7fd6f
parent 42397 13798dcbdca5
child 45451 74515e8e6046
permissions -rw-r--r--
tuning options to avoid spurious isabelle test failures
     1 theory IMP_1
     2 imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     3 begin
     4 
     5 subsection {* IMP *}
     6 
     7 text {*
     8   In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
     9 *}
    10 
    11 type_synonym var = unit
    12 type_synonym state = bool
    13 
    14 datatype com =
    15   Skip |
    16   Ass bool |
    17   Seq com com |
    18   IF com com
    19 
    20 inductive exec :: "com => state => state => bool" where
    21   "exec Skip s s" |
    22   "exec (Ass e) s e" |
    23   "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
    24   "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
    25   "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t"
    26 
    27 lemma
    28   "exec c s s' ==> exec (Seq c c) s s'"
    29 quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
    30 oops
    31 
    32 
    33 end