src/HOL/Modelcheck/MuckeExample1.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 6466 2eba94dc5951 child 17272 c63e5220ed77 permissions -rw-r--r--
Constant "If" is now local
```     1 (*  Title:      HOL/Modelcheck/MuckeExample1.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
```
```     4     Copyright   1997  TU Muenchen
```
```     5 *)
```
```     6
```
```     7 MuckeExample1 = MuckeSyn +
```
```     8
```
```     9
```
```    10
```
```    11 types
```
```    12     state = "bool * bool * bool"
```
```    13
```
```    14 consts
```
```    15
```
```    16   INIT :: "state pred"
```
```    17   N    :: "[state,state] => bool"
```
```    18   reach:: "state pred"
```
```    19
```
```    20 defs
```
```    21
```
```    22   INIT_def "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
```
```    23
```
```    24   N_def   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
```
```    25 	                  y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
```
```    26                      in (~x1&~x2&~x3 & y1&~y2&~y3) |
```
```    27 	                (x1&~x2&~x3 & ~y1&~y2&~y3) |
```
```    28 	                (x1&~x2&~x3 & y1&y2&y3)    "
```
```    29
```
```    30   reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
```
```    31
```
```    32
```
```    33 end
```
```    34
```