--- a/src/HOL/Modelcheck/Example.ML Wed Apr 21 19:03:11 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Modelcheck/Example.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-val reach_rws = [reach_def,INIT_def,N_def];
-
-
-Goal "reach (True,True,True)";
-by (simp_tac (MC_ss addsimps reach_rws) 1);
-
-(*show the current proof state using the model checker syntax*)
-setmp print_mode ["Eindhoven"] pr ();
-
-(* actually invoke the model checker *)
-(* try out after installing the model checker: see the README file *)
-
-(* by (mc_tac 1); *)
-
-(*qed "reach_ex_thm";*)
-
-
-
-(* just to make a proof in this file :-) *)
-Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
-by (Simp_tac 1);
-qed"init_state";
--- a/src/HOL/Modelcheck/Example.thy Wed Apr 21 19:03:11 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: HOL/Modelcheck/Example.thy
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-Example = CTL + MCSyn +
-
-
-types
- state = "bool * bool * bool"
-
-consts
-
- INIT :: "state pred"
- N :: "[state,state] => bool"
- reach:: "state pred"
-
-defs
-
- INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
-
- 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))"
-
-
-end
--- a/src/HOL/Modelcheck/MCSyn.ML Wed Apr 21 19:03:11 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* Title: HOL/Modelcheck/MCSyn.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-fun mc_tac i state =
-let val sign = #sign (rep_thm state)
-in
-case drop(i-1,prems_of state) of
- [] => Seq.empty |
- subgoal::_ =>
- let val concl = Logic.strip_imp_concl subgoal;
- val OraAss = invoke_oracle MCSyn.thy "mc" (sign,MCOracleExn concl);
- in
- ((cut_facts_tac [OraAss] i) THEN (atac i)) state
- end
-end;
-
-
-Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
- by (rtac ext 1);
- by (stac (surjective_pairing RS sym) 1);
- by (rtac refl 1);
-qed "pair_eta_expand";
-
-local
- val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
- val rew = mk_meta_eq pair_eta_expand;
-
- fun proc _ _ (Abs _) = Some rew
- | proc _ _ _ = None;
-in
- val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
-end;
-
-
-val MC_ss =
- simpset() addsimprocs [pair_eta_expand_proc]
- addsimps [split_paired_Ex, Let_def];
--- a/src/HOL/Modelcheck/MCSyn.thy Wed Apr 21 19:03:11 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: HOL/Modelcheck/MCSyn.thy
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-MCSyn = MuCalculus +
-
-syntax (Eindhoven output)
-
- True :: bool ("TRUE")
- False :: bool ("FALSE")
-
- Not :: bool => bool ("NOT _" [40] 40)
- "op &" :: [bool, bool] => bool (infixr "AND" 35)
- "op |" :: [bool, bool] => bool (infixr "OR" 30)
-
- "! " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
- "? " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
- "ALL " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
- "EX " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
- "_lambda" :: [pttrns, 'a] => 'b ("(3L _./ _)" 10)
-
- "_idts" :: [idt, idts] => idts ("_,/_" [1, 0] 0)
- "_pattern" :: [pttrn, patterns] => pttrn ("_,/_" [1, 0] 0)
-
- "Mu " :: [idts, 'a pred] => 'a pred ("(3[mu _./ _])" 1000)
- "Nu " :: [idts, 'a pred] => 'a pred ("(3[nu _./ _])" 1000)
-
-oracle
- mc = mk_mc_oracle
-
-end
--- a/src/HOL/Modelcheck/ROOT.ML Wed Apr 21 19:03:11 1999 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML Thu Apr 22 10:55:23 1999 +0200
@@ -1,10 +1,13 @@
(* Title: HOL/Modelcheck/ROOT.ML
ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Author: Olaf Mueller, Tobias Hamberger, Robert Sandner
Copyright 1997 TU Muenchen
-This is the ROOT file for the Eindhoven Modelchecker example
+This is the ROOT file for the Modelchecker examples
*)
+use_thy"EindhovenExample";
-use_thy"Example";
+use"mucke_oracle.ML";
+use_thy"MuckeExample1";
+use_thy"MuckeExample2";