--- a/src/HOL/Modelcheck/MuckeExample1.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample1.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,31 +4,34 @@
Copyright 1997 TU Muenchen
*)
-MuckeExample1 = MuckeSyn +
-
-
+theory MuckeExample1
+imports MuckeSyn
+begin
types
- state = "bool * bool * bool"
-
-consts
-
- INIT :: "state pred"
- N :: "[state,state] => bool"
- reach:: "state pred"
+ state = "bool * bool * bool"
-defs
-
- INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+constdefs
+ INIT :: "state pred"
+ "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+ N :: "[state,state] => bool"
+ "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
+ y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
+ in (~x1&~x2&~x3 & y1&~y2&~y3) |
+ (x1&~x2&~x3 & ~y1&~y2&~y3) |
+ (x1&~x2&~x3 & y1&y2&y3)"
+ reach:: "state pred"
+ "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
- N_def "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
- y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
- in (~x1&~x2&~x3 & y1&~y2&~y3) |
- (x1&~x2&~x3 & ~y1&~y2&~y3) |
- (x1&~x2&~x3 & y1&y2&y3) "
-
- reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
-
+lemmas reach_rws = INIT_def N_def reach_def
+
+lemma reach_ex1: "reach (True,True,True)"
+ apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
+ apply (tactic {* mc_mucke_tac [] 1 *})
+ done
+
+(*alternative*)
+lemma reach_ex' "reach (True,True,True)"
+ by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
end
-