--- a/src/HOL/Modelcheck/EindhovenExample.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenExample.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,28 +4,39 @@
Copyright 1997 TU Muenchen
*)
-EindhovenExample = CTL + EindhovenSyn +
-
+theory EindhovenExample
+imports EindhovenSyn CTL
+begin
types
- state = "bool * bool * bool"
+ state = "bool * bool * bool"
-consts
+constdefs
+ INIT :: "state pred"
+ "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
- INIT :: "state pred"
- N :: "[state,state] => bool"
+ N :: "[state,state] => bool"
+ "N == % (x1,x2,x3) (y1,y2,y3).
+ (~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))"
-defs
-
- INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
+ by (simp add: INIT_def)
+
+
+lemmas reach_rws = reach_def INIT_def N_def
- N_def "N == % (x1,x2,x3) (y1,y2,y3).
- (~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))"
-
+lemma reach_ex: "reach (True, True, True)"
+ apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
+ txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
+ pr (Eindhoven)
+ txt {* actually invoke the model checker, try out after installing
+ the model checker: see the README file *}
+ apply (tactic {* mc_eindhoven_tac 1 *})
+ done
end