# HG changeset patch
# User mueller
# Date 924771323 -7200
# Node ID 4086e4f2edc46999d045594c85dd3284e21b6dff
# Parent  9a71c0c2ac71c2db7b347663792f9c4caab1960e
delete old files for adding second modelchecker connection;

diff -r 9a71c0c2ac71 -r 4086e4f2edc4 src/HOL/Modelcheck/Example.ML
--- 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";
diff -r 9a71c0c2ac71 -r 4086e4f2edc4 src/HOL/Modelcheck/Example.thy
--- 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
diff -r 9a71c0c2ac71 -r 4086e4f2edc4 src/HOL/Modelcheck/MCSyn.ML
--- 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];
diff -r 9a71c0c2ac71 -r 4086e4f2edc4 src/HOL/Modelcheck/MCSyn.thy
--- 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
diff -r 9a71c0c2ac71 -r 4086e4f2edc4 src/HOL/Modelcheck/ROOT.ML
--- 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";