author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 17272 | c63e5220ed77 |
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 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
3 |
Copyright 1997 TU Muenchen |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
4 |
*) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
5 |
|
17272 | 6 |
theory EindhovenExample |
7 |
imports EindhovenSyn CTL |
|
8 |
begin |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
9 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
10 |
types |
17272 | 11 |
state = "bool * bool * bool" |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
12 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17272
diff
changeset
|
13 |
definition INIT :: "state pred" where |
17272 | 14 |
"INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
15 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17272
diff
changeset
|
16 |
definition N :: "[state,state] => bool" where |
17272 | 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 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17272
diff
changeset
|
22 |
definition reach:: "state pred" where |
17272 | 23 |
"reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
24 |
|
17272 | 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 |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
30 |
|
17272 | 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 |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
39 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
40 |
end |