src/HOL/Predicate_Compile_Examples/IMP_4.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (20 months ago) changeset 67003 49850a679c2c parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
more robust sorted_entries;
```     1 theory IMP_4
```
```     2 imports "HOL-Library.Predicate_Compile_Quickcheck"
```
```     3 begin
```
```     4
```
```     5 subsection \<open>IMP\<close>
```
```     6
```
```     7 text \<open>
```
```     8   In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
```
```     9 \<close>
```
```    10
```
```    11 type_synonym var = nat
```
```    12 type_synonym state = "int list"
```
```    13
```
```    14 datatype 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
```