src/HOL/Predicate_Compile_Examples/IMP_2.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40924 a9be7f26b4e6
child 41413 64cd30d6b0b8
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 theory IMP_2
     2 imports "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, IF and While.
     9 *}
    10 
    11 types
    12   var = unit
    13   state = bool
    14 
    15 datatype com =
    16   Skip |
    17   Ass bool |
    18   Seq com com |
    19   IF com com |
    20   While com
    21 
    22 inductive exec :: "com => state => state => bool" where
    23   "exec Skip s s" |
    24   "exec (Ass e) s e" |
    25   "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
    26   "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
    27   "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
    28   "\<not> s ==> exec (While c) s s" |
    29   "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''"
    30 
    31 lemma
    32   "exec c s s' ==> exec (Seq c c) s s'"
    33 quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
    34 oops
    35 
    36 
    37 end