equal
deleted
inserted
replaced
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 theory MuckeExample1 |
|
8 imports MuckeSyn |
|
9 begin |
|
10 |
|
11 types |
|
12 state = "bool * bool * bool" |
|
13 |
|
14 definition INIT :: "state pred" where |
|
15 "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
|
16 N :: "[state,state] => bool" |
|
17 "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x)); |
|
18 y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y)) |
|
19 in (~x1&~x2&~x3 & y1&~y2&~y3) | |
|
20 (x1&~x2&~x3 & ~y1&~y2&~y3) | |
|
21 (x1&~x2&~x3 & y1&y2&y3)" |
|
22 reach:: "state pred" |
|
23 "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
|
24 |
|
25 lemmas reach_rws = INIT_def N_def reach_def |
|
26 |
|
27 lemma reach_ex1: "reach (True,True,True)" |
|
28 apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *}) |
|
29 apply (tactic {* mc_mucke_tac [] 1 *}) |
|
30 done |
|
31 |
|
32 (*alternative*) |
|
33 lemma reach_ex' "reach (True,True,True)" |
|
34 by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *}) |
|
35 |
|
36 end |
|