1 (* Title: HOL/Modelcheck/EindhovenExample.thy |
1 (* Title: HOL/Modelcheck/EindhovenExample.thy |
2 ID: $Id$ |
|
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
2 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
4 Copyright 1997 TU Muenchen |
3 Copyright 1997 TU Muenchen |
5 *) |
4 *) |
6 |
5 |
7 theory EindhovenExample |
6 theory EindhovenExample |
9 begin |
8 begin |
10 |
9 |
11 types |
10 types |
12 state = "bool * bool * bool" |
11 state = "bool * bool * bool" |
13 |
12 |
14 constdefs |
13 definition INIT :: "state pred" where |
15 INIT :: "state pred" |
|
16 "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
14 "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
17 |
15 |
18 N :: "[state,state] => bool" |
16 definition N :: "[state,state] => bool" where |
19 "N == % (x1,x2,x3) (y1,y2,y3). |
17 "N == % (x1,x2,x3) (y1,y2,y3). |
20 (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
18 (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
21 ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
19 ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
22 ( x1 & ~x2 & ~x3 & y1 & y2 & y3)" |
20 ( x1 & ~x2 & ~x3 & y1 & y2 & y3)" |
23 |
21 |
24 reach:: "state pred" |
22 definition reach:: "state pred" where |
25 "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
23 "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
26 |
24 |
27 lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)" |
25 lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)" |
28 by (simp add: INIT_def) |
26 by (simp add: INIT_def) |
29 |
27 |