--- a/src/HOL/Modelcheck/MuckeExample2.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample2.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,24 +4,29 @@
Copyright 1997 TU Muenchen
*)
-
-MuckeExample2 = MuckeSyn +
-
-consts
-
- Init :: "bool pred"
- R :: "[bool,bool] => bool"
- Reach :: "bool pred"
- Reach2:: "bool pred"
+theory MuckeExample2
+imports MuckeSyn
+begin
-defs
-
- Init_def " Init x == x"
-
- R_def "R x y == (x & ~y) | (~x & y)"
+constdefs
+ Init :: "bool pred"
+ "Init x == x"
+ R :: "[bool,bool] => bool"
+ "R x y == (x & ~y) | (~x & y)"
+ Reach :: "bool pred"
+ "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+ Reach2:: "bool pred"
+ "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
- Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
- Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
+lemma Reach: "Reach2 True"
+ apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
+ apply (tactic {* mc_mucke_tac [] 1 *})
+ done
-end
\ No newline at end of file
+(*alternative:*)
+lemma Reach': "Reach2 True"
+ by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
+
+end