1 (* Title: HOL/Modelcheck/EindhovenExample.thy |
|
2 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
3 Copyright 1997 TU Muenchen |
|
4 *) |
|
5 |
|
6 theory EindhovenExample |
|
7 imports EindhovenSyn CTL |
|
8 begin |
|
9 |
|
10 types |
|
11 state = "bool * bool * bool" |
|
12 |
|
13 definition INIT :: "state pred" where |
|
14 "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
|
15 |
|
16 definition N :: "[state,state] => bool" where |
|
17 "N == % (x1,x2,x3) (y1,y2,y3). |
|
18 (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
|
19 ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
|
20 ( x1 & ~x2 & ~x3 & y1 & y2 & y3)" |
|
21 |
|
22 definition reach:: "state pred" where |
|
23 "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
|
24 |
|
25 lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)" |
|
26 by (simp add: INIT_def) |
|
27 |
|
28 |
|
29 lemmas reach_rws = reach_def INIT_def N_def |
|
30 |
|
31 lemma reach_ex: "reach (True, True, True)" |
|
32 apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *}) |
|
33 txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *} |
|
34 pr (Eindhoven) |
|
35 txt {* actually invoke the model checker, try out after installing |
|
36 the model checker: see the README file *} |
|
37 apply (tactic {* mc_eindhoven_tac 1 *}) |
|
38 done |
|
39 |
|
40 end |
|