# HG changeset patch
# User mueller
# Date 924771397 -7200
# Node ID 2eba94dc5951293d482dcaa6073a194aeb0a1663
# Parent  4086e4f2edc46999d045594c85dd3284e21b6dff
added modelchecker mucke besides modelchecker eindhoven;

diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/EindhovenExample.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/EindhovenExample.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,28 @@
+(*  Title:      HOL/Modelcheck/EindhovenExample.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 (Eindhoven_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_eindhoven_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 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/EindhovenExample.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/EindhovenExample.thy	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/Modelcheck/EindhovenExample.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+EindhovenExample = CTL + EindhovenSyn + 
+
+
+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 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/EindhovenSyn.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,47 @@
+(*  Title:      HOL/Modelcheck/EindhovenSyn.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+
+
+
+
+
+
+
+fun mc_eindhoven_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 EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn 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 Eindhoven_ss =
+  simpset() addsimprocs [pair_eta_expand_proc]
+    addsimps [split_paired_Ex, Let_def];
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/EindhovenSyn.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,72 @@
+(*  Title:      HOL/Modelcheck/EindhovenSyn.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+EindhovenSyn = 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
+  eindhoven_mc = mk_eindhoven_mc_oracle
+
+end
+
+
+
+ML
+
+
+exception EindhovenOracleExn of term;
+
+
+val trace_mc = ref false;
+
+local
+
+fun termtext sign term =
+  setmp print_mode ["Eindhoven"]
+    (Sign.string_of_term sign) term;
+
+fun call_mc s =
+  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
+
+in
+
+fun mk_eindhoven_mc_oracle (sign, EindhovenOracleExn trm) =
+  let
+    val tmtext = termtext sign trm;
+    val debug = writeln ("MC debugger: " ^ tmtext);
+    val result = call_mc tmtext;
+  in
+    if ! trace_mc then
+      (writeln tmtext; writeln("----"); writeln result)
+    else ();
+    (case result of
+      "TRUE\n"  =>  trm |
+      "FALSE\n" => (error "MC oracle yields FALSE") |
+    _ => (error ("MC syntax error: " ^ result)))
+  end;
+
+end;
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeExample1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeExample1.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Modelcheck/MuckeExample1.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+val reach_rws = [INIT_def,N_def,reach_def];
+
+(*
+goal thy "reach (True,True,True)";
+by (simp_tac (Mucke_ss addsimps reach_rws) 1); 
+by (mc_mucke_tac thy [] 1);
+qed "reach_ex_thm1";
+
+(* Alternative: *)
+goal thy "reach (True,True,True)";
+by (mc_mucke_tac thy reach_rws 1);
+qed "reach_ex_thm1";
+
+*)
+
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeExample1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeExample1.thy	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/Modelcheck/MuckeExample1.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+MuckeExample1 = MuckeSyn + 
+
+
+
+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 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))"
+  
+
+end
+
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeExample2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeExample2.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,28 @@
+(*  Title:      HOL/Modelcheck/MuckeExample2.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+
+(* prints the mucke output on the screen *)
+(* trace_mc := true; *)
+val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
+
+(*
+
+goal thy "Reach2 True";
+by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
+by (mc_mucke_tac thy [] 1);
+qed "Reach_thm";
+
+(* Alternative: *)
+goal thy "Reach2 True";
+by (mc_mucke_tac thy Reach_rws 1);
+qed "Reach_thm";
+
+
+*)
+
+
+  
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeExample2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeExample2.thy	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/Modelcheck/MuckeExample2.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+
+MuckeExample2 = MuckeSyn +
+
+consts
+
+  Init  :: "bool pred"
+  R	:: "[bool,bool] => bool"
+  Reach	:: "bool pred"
+  Reach2:: "bool pred"
+
+defs
+
+  Init_def " Init x == x"
+
+  R_def "R x y == (x & ~y) | (~x & y)"
+
+  Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+
+  Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
+
+end
\ No newline at end of file
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeSyn.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,192 @@
+(* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
+   it yields innermost one. If no Mu term is present, search_mu yields None
+*)
+
+(* extended for treatment of nu (TH) *)
+fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
+	(case (search_mu t2) of
+	      Some t => Some t 
+	    | None => Some ((Const("MuCalculus.mu",tp)) $ t2))
+  | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
+        (case (search_mu t2) of
+              Some t => Some t
+            | None => Some ((Const("MuCalculus.nu",tp)) $ t2))
+  | search_mu (t1 $ t2) = 
+	(case (search_mu t1) of
+	      Some t => Some t 
+	    | None     => search_mu t2)
+  | search_mu (Abs(_,_,t)) = search_mu t
+  | search_mu _ = None;
+
+
+
+
+(* seraching a variable in a term. Used in move_mus to extract the
+   term-rep of var b in hthm *)
+
+fun search_var s t =
+case t of
+     t1 $ t2 => (case (search_var s t1) of
+		             Some tt => Some tt |
+			     None => search_var s t2) |
+     Abs(_,_,t) => search_var s t |
+     Var((s1,_),_) => if s = s1 then Some t else None |
+     _ => None;
+	
+
+(* function move_mus:
+   Mucke can't deal with nested Mu terms. move_mus i searches for 
+   Mu terms in the subgoal i and replaces Mu terms in the conclusion
+   by constants and definitions in the premises recursively.
+
+   move_thm is the theorem the performs the replacement. To create NEW
+   names for the Mu terms, the indizes of move_thm are incremented by
+   max_idx of the subgoal.
+*)
+
+local
+
+  val move_thm = prove_goal MuckeSyn.thy "[| a = b ==> P a; a = b |] ==> P b"
+	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
+		     REPEAT (resolve_tac prems 1)]);
+
+  val sig_move_thm = #sign (rep_thm move_thm);
+  val bCterm = cterm_of sig_move_thm (the (search_var "b" (concl_of move_thm)));
+  val aCterm = cterm_of sig_move_thm (the (search_var "a" (hd(prems_of move_thm)))); 
+
+in
+
+fun move_mus i state =
+let val sign = #sign (rep_thm state);
+    val (subgoal::_) = drop(i-1,prems_of state);
+    val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
+    val redex = search_mu concl;
+    val idx = let val t = #maxidx (rep_thm state) in 
+	      if t < 0 then 1 else t+1 end;
+in
+case redex of
+     None => all_tac state |
+     Some redexterm => 
+	let val Credex = cterm_of sign redexterm;
+	    val aiCterm = 
+		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
+	    val inst_move_thm = cterm_instantiate 
+				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
+	in
+            ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
+		THEN (move_mus i)) state
+	end
+end; (* outer let *)
+end; (* local *)
+
+
+(* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *)
+(* Normally t can be user-instantiated by the value thy of the Isabelle context     *)
+fun call_mucke_tac t i state =
+let val sign = #sign (rep_thm state);
+    val (subgoal::_) = drop(i-1,prems_of state);
+    val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal,t));
+in 
+(cut_facts_tac [OraAss] i) state
+end;
+
+
+(* transforming fun-defs into lambda-defs *)
+
+val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
+ br (extensional eq) 1;
+qed "ext_rl";
+
+infix cc;
+
+fun None cc xl = xl
+  | (Some x) cc xl = x::xl;
+
+fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
+  | getargs (x $ (Var ((y,_),_))) = y;
+
+fun getfun ((x $ y) $ z) = getfun (x $ y)
+  | getfun (x $ _) = x;
+
+local
+
+fun is_prefix [] s = true
+| is_prefix (p::ps) [] = false
+| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
+
+fun delete_bold [] = []
+| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+        then (let val (_::_::_::s) = xs in delete_bold s end)
+        else (if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
+                then  (let val (_::_::_::s) = xs in delete_bold s end)
+                else (x::delete_bold xs));
+
+fun delete_bold_string s = implode(delete_bold (explode s));
+
+in
+
+(* extension with removing bold font (TH) *)
+fun mk_lam_def (_::_) _ _ = None  
+  | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = Some t
+  | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
+    let val tsig = #sign (rep_thm t);
+	val fnam = Sign.string_of_term tsig (getfun LHS);
+	val rhs = Sign.string_of_term tsig (freeze_thaw RHS)
+	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
+    in
+	Some (prove_goal (theory_of_sign tsig) gl (fn prems =>
+  		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
+    end
+| mk_lam_def [] _ t= None; 
+
+fun mk_lam_defs ([]:thm list) = ([]: thm list) 
+  | mk_lam_defs (t::l) = 
+      (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
+
+end;
+
+(* first simplification, then model checking *)
+
+goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
+by (Simp_tac 1);
+qed "split_paired_Ex";
+
+
+goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+  br ext 1;
+  by (stac (surjective_pairing RS sym) 1);
+  br 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 Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] 
+                      addsimps [split_paired_Ex,Let_def];
+
+(* the Interface *)
+
+(* type of mc_tac has changed: an argument t of type thy was inserted;  *)
+(* t can be user-instantiated by the value thy of the Isabelle context; *)
+(* furthermore, tactic was extended by full_simp_tac  (TH) *)
+fun mc_mucke_tac t defs i state =
+let val sign = #sign (rep_thm state);
+in
+case drop(i-1,prems_of state) of
+   [] => PureGeneral.Seq.empty |
+   subgoal::_ => 
+		EVERY[REPEAT(etac thin_rl i),
+                        cut_facts_tac (mk_lam_defs defs) i,
+                 full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
+                        move_mus i, call_mucke_tac t i,atac i,
+                        REPEAT(rtac refl i)] state 
+end;
+
diff -r 4086e4f2edc4 -r 2eba94dc5951 src/HOL/Modelcheck/MuckeSyn.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,80 @@
+(*  Title:      HOL/Modelcheck/MuckeSyn.thy
+    ID:         $Id$
+    Author:     Tobias Hamberger
+    Copyright   1999  TU Muenchen
+*)
+
+
+MuckeSyn = MuCalculus + 
+
+(* extended with some operators and case treatment (which requires postprocessing with 
+transform_case (from MuCalculus) (TH) *)
+
+types
+  mutype 
+  decl decls
+  cases_syn case_syn 
+syntax (Mucke output)
+
+
+  True		:: bool					("true")
+  False		:: bool					("false")
+  Not		:: bool => bool				("! _" [40] 40)
+  If		:: [bool, 'a, 'a] => 'a		("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
+  
+  "op &"	:: [bool, bool] => bool			(infixr "&" 35)
+  "op |"	:: [bool, bool] => bool			(infixr "|" 30)
+  "op -->"	:: [bool, bool] => bool			(infixr "->" 25)
+  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
+  "op ~="       :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
+
+  "! " 		:: [idts, bool] => bool			("'((3forall _./ _)')" [0, 10] 10)
+  "? "		:: [idts, bool] => bool			("'((3exists _./ _)')" [0, 10] 10)
+  "ALL "        :: [idts, bool] => bool                 ("'((3forall _./ _)')" [0, 10] 10)
+  "EX "         :: [idts, bool] => bool                 ("'((3exists _./ _)')" [0, 10] 10)
+
+  "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
+  "_applC"	:: [('b => 'a), cargs] => aprop		("(1_/ '(_'))" [1000,1000] 999)
+  "_cargs" 	:: ['a, cargs] => cargs         	("_,/ _" [1000,1000] 1000)
+
+  "_idts"     	:: [idt, idts] => idts		        ("_,/ _" [1, 0] 0)
+
+  "@Tuple"      :: "['a, args] => 'a * 'b"              ("(1_,/ _)")
+(* "@pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/ _" [1, 0] 0) 
+  "_pattern"    :: [pttrn, patterns] => pttrn           ("_,/ _" [1, 0] 0) *)
+
+
+  "_decl"	:: [mutype,pttrn] => decl		("_ _")
+  "_decls"	:: [decl,decls] => decls		("_,/ _")
+  ""		:: decl => decls			("_")
+  "_mu"		:: [decl,decls,'a pred] => 'a pred	("mu _ '(_') _ ;")
+  "_mudec"	:: [decl,decls] => 'a pred		("mu _ '(_') ;") 
+  "_nu"		:: [decl,decls,'a pred] => 'a pred	("nu _ '(_') _ ;") 
+  "_nudec"	:: [decl,decls] => 'a pred		("nu _ '(_') ;") 
+  "_fun"  	:: [decl,decls,'a pred] => 'a pred 	("_ '(_') _ ;")
+  "_dec"	:: [decl,decls] => 'a pred		("_ '(_') ;")
+
+  "_Ex"  	:: [decl,idts,'a pred] => 'a pred	("'((3exists _ _./ _)')")
+  "_All"	:: [decl,idts,'a pred] => 'a pred	("'((3forall _ _./ _)')")
+
+  "Mu "		:: [idts, 'a pred] => 'a pred		("(3mu _./ _)" 1000)
+  "Nu "		:: [idts, 'a pred] => 'a pred		("(3nu _./ _)" 1000)
+  
+  "@case"       :: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
+  "@case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
+  ""            :: case_syn => cases_syn            ("_")
+  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
+(* Terms containing a case statement must be post-processed with the function  *)
+(* transform_case, defined in MuCalculus.ML. There, all asterikses before the  *)
+(* "=" will be replaced by the expression between the two asterikses following *)
+(* "case" and the asteriks after esac will be deleted                          *)
+
+oracle
+  Mucke = mk_mucke_mc_oracle
+
+end
+
+
+
+  
+