src/HOL/Predicate_Compile_Examples/IMP_1.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 45451 74515e8e6046
child 58249 180f1b3508ed
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
bulwahn@39186
     1
theory IMP_1
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 one boolean variable and the commands are Skip, Ass, Seq, and IF.
bulwahn@39186
     9
*}
bulwahn@39186
    10
bulwahn@42031
    11
type_synonym var = unit
bulwahn@42031
    12
type_synonym state = bool
bulwahn@39186
    13
bulwahn@39186
    14
datatype com =
bulwahn@39186
    15
  Skip |
bulwahn@39186
    16
  Ass bool |
bulwahn@39186
    17
  Seq com com |
bulwahn@39186
    18
  IF com com
bulwahn@39186
    19
bulwahn@39186
    20
inductive exec :: "com => state => state => bool" where
bulwahn@39186
    21
  "exec Skip s s" |
bulwahn@39186
    22
  "exec (Ass e) s e" |
bulwahn@39186
    23
  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
bulwahn@39186
    24
  "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
bulwahn@39186
    25
  "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t"
bulwahn@39186
    26
bulwahn@39186
    27
lemma
bulwahn@39186
    28
  "exec c s s' ==> exec (Seq c c) s s'"
bulwahn@45451
    29
quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
bulwahn@39186
    30
oops
bulwahn@39186
    31
bulwahn@39186
    32
bulwahn@39186
    33
end