author | wenzelm |
Tue, 06 Sep 2005 16:24:53 +0200 | |
changeset 17272 | c63e5220ed77 |
parent 6466 | 2eba94dc5951 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/Modelcheck/EindhovenExample.thy |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
4 |
Copyright 1997 TU Muenchen |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
5 |
*) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
6 |
|
17272 | 7 |
theory EindhovenExample |
8 |
imports EindhovenSyn CTL |
|
9 |
begin |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
10 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
11 |
types |
17272 | 12 |
state = "bool * bool * bool" |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
13 |
|
17272 | 14 |
constdefs |
15 |
INIT :: "state pred" |
|
16 |
"INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
17 |
|
17272 | 18 |
N :: "[state,state] => bool" |
19 |
"N == % (x1,x2,x3) (y1,y2,y3). |
|
20 |
(~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
|
21 |
( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
|
22 |
( x1 & ~x2 & ~x3 & y1 & y2 & y3)" |
|
23 |
||
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
24 |
reach:: "state pred" |
17272 | 25 |
"reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
26 |
|
17272 | 27 |
lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)" |
28 |
by (simp add: INIT_def) |
|
29 |
||
30 |
||
31 |
lemmas reach_rws = reach_def INIT_def N_def |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
32 |
|
17272 | 33 |
lemma reach_ex: "reach (True, True, True)" |
34 |
apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *}) |
|
35 |
txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *} |
|
36 |
pr (Eindhoven) |
|
37 |
txt {* actually invoke the model checker, try out after installing |
|
38 |
the model checker: see the README file *} |
|
39 |
apply (tactic {* mc_eindhoven_tac 1 *}) |
|
40 |
done |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
41 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
42 |
end |