src/HOL/Predicate_Compile_Examples/IMP_3.thy
author wenzelm
Tue, 05 Nov 2019 14:28:00 +0100
changeset 71047 87c132cf5860
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
more options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
     1
theory IMP_3
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 63167
diff changeset
     2
imports "HOL-Library.Predicate_Compile_Quickcheck"
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
     3
begin
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
     4
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58310
diff changeset
     5
subsection \<open>IMP\<close>
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
     6
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58310
diff changeset
     7
text \<open>
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
     8
  In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58310
diff changeset
     9
\<close>
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    10
42031
2de57cda5b24 adapting predicate_compile_quickcheck; tuned
bulwahn
parents: 41413
diff changeset
    11
type_synonym var = unit
2de57cda5b24 adapting predicate_compile_quickcheck; tuned
bulwahn
parents: 41413
diff changeset
    12
type_synonym state = int
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    13
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    14
datatype com =
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    15
  Skip |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    16
  Ass var "int" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    17
  Seq com com |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    18
  IF "state list" com com |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    19
  While "state list" com
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    20
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    21
inductive exec :: "com => state => state => bool" where
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    22
  "exec Skip s s" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    23
  "exec (Ass x e) s e" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    24
  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    25
  "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    26
  "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    27
  "s \<notin> set b ==> exec (While b c) s s" |
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    28
  "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    29
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    30
lemma
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    31
  "exec c s s' ==> exec (Seq c c) s s'"
45451
74515e8e6046 renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
bulwahn
parents: 43686
diff changeset
    32
  quickcheck[tester = smart_exhaustive, size=2, iterations=100, quiet = false, expect = counterexample]
39186
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    33
oops
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    34
475856793715 adding IMP quickcheck examples
bulwahn
parents:
diff changeset
    35
43686
bc7d63c7fd6f tuning options to avoid spurious isabelle test failures
bulwahn
parents: 42031
diff changeset
    36
end