# HG changeset patch
# User wenzelm
# Date 1177598371 -7200
# Node ID a7b425bb668cdd734f2b514d0124e969f17d590c
# Parent  c0695a818c091ba14437021e8a180584665daea0
removed legacy ML files;

diff -r c0695a818c09 -r a7b425bb668c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 26 16:39:31 2007 +0200
@@ -469,11 +469,10 @@
 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
 
 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
-  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.ML \
-  Modelcheck/EindhovenSyn.thy Modelcheck/MuCalculus.thy \
-  Modelcheck/MuckeExample1.thy Modelcheck/MuckeExample2.thy \
-  Modelcheck/MuckeSyn.ML Modelcheck/MuckeSyn.thy Modelcheck/ROOT.ML \
-  Modelcheck/mucke_oracle.ML
+  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
+  Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
+  Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
+  Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
 
 
diff -r c0695a818c09 -r a7b425bb668c src/HOL/Modelcheck/EindhovenSyn.ML
--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Thu Apr 26 16:39:14 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      HOL/Modelcheck/EindhovenSyn.ML
-    ID:         $Id$
-    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
-    Copyright   1997  TU Muenchen
-*)
-
-fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
-  let
-    val thy = Thm.theory_of_thm state;
-    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
-  in cut_facts_tac [assertion] i THEN atac i end) i state;
-
-val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
-
-val pair_eta_expand_proc =
-  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
-  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
-
-val Eindhoven_ss =
-  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
-
-(*check if user has pmu installed*)
-fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
-fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
diff -r c0695a818c09 -r a7b425bb668c src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:31 2007 +0200
@@ -59,4 +59,25 @@
 end
 *}
 
+ML {*
+fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
+  let
+    val thy = Thm.theory_of_thm state;
+    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
+  in cut_facts_tac [assertion] i THEN atac i end) i state;
+
+val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
+
+val pair_eta_expand_proc =
+  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
+
+val Eindhoven_ss =
+  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+
+(*check if user has pmu installed*)
+fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
+fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
+*}
+
 end
diff -r c0695a818c09 -r a7b425bb668c src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Apr 26 16:39:14 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-
-(* $Id$ *)
-
-(* 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 (the_context ()) "[| 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 = Thm.theory_of_thm move_thm;
-  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
-  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
-
-in
-
-fun move_mus i state =
-let val sign = Thm.theory_of_thm state;
-    val (subgoal::_) = Library.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;
-end;
-
-
-fun call_mucke_tac i state =
-let val thy = Thm.theory_of_thm state;
-    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
-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";
- by (rtac (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 delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
-        then (let val (_::_::_::s) = xs in delete_bold s end)
-        else (if (is_prefix (op =) ("\^["::"["::"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 thy = theory_of_thm t;
-	val fnam = Sign.string_of_term thy (getfun LHS);
-	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
-	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
-    in
-	SOME (prove_goal thy 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 *)
-
-val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
-
-val pair_eta_expand_proc =
-  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
-  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
-
-val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
-
-
-(* the interface *)
-
-fun mc_mucke_tac defs i state =
-  (case Library.drop (i - 1, Thm.prems_of state) of
-    [] => no_tac state
-  | 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 i,atac i,
-        REPEAT (rtac refl i)] state);
-
-(*check if user has mucke installed*)
-fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
-fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
diff -r c0695a818c09 -r a7b425bb668c src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Apr 26 16:39:31 2007 +0200
@@ -71,6 +71,176 @@
 oracle mc_mucke_oracle ("term") =
   mk_mc_mucke_oracle
 
-end
+ML {*
+(* 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 (the_context ()) "[| 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 = Thm.theory_of_thm move_thm;
+  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
+  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
+
+in
+
+fun move_mus i state =
+let val sign = Thm.theory_of_thm state;
+    val (subgoal::_) = Library.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;
+end;
 
 
+fun call_mucke_tac i state =
+let val thy = Thm.theory_of_thm state;
+    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
+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";
+ by (rtac (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 delete_bold [] = []
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
+        then (let val (_::_::_::s) = xs in delete_bold s end)
+        else (if (is_prefix (op =) ("\^["::"["::"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 thy = theory_of_thm t;
+	val fnam = Sign.string_of_term thy (getfun LHS);
+	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
+	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
+    in
+	SOME (prove_goal thy 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 *)
+
+val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
+
+val pair_eta_expand_proc =
+  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
+
+val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+
+
+(* the interface *)
+
+fun mc_mucke_tac defs i state =
+  (case Library.drop (i - 1, Thm.prems_of state) of
+    [] => no_tac state
+  | 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 i,atac i,
+        REPEAT (rtac refl i)] state);
+
+(*check if user has mucke installed*)
+fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
+fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
+
+*}
+
+end
diff -r c0695a818c09 -r a7b425bb668c src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 26 16:39:14 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-
-(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
-	There, implementation relations for I/O automatons are proved using
-	the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
-
-exception SimFailureExn of string;
-
-val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"];
-val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def",
-  thm "asig_internals_def", thm "actions_def"];
-val comp_simps = [thm "par_def", thm "asig_comp_def"];
-val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"];
-val hide_simps = [thm "hide_def", thm "hide_asig_def"];
-val rename_simps = [thm "rename_def", thm "rename_set_def"];
-
-local
-
-exception malformed;
-
-fun fst_type (Type("*",[a,_])) = a |
-fst_type _ = raise malformed; 
-fun snd_type (Type("*",[_,a])) = a |
-snd_type _ = raise malformed;
-
-fun element_type (Type("set",[a])) = a |
-element_type t = raise malformed;
-
-fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
-let
-val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
-val sig_typ = fst_type aut_typ;
-val int_typ = fst_type sig_typ
-in 
-Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
- (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA)
-end
-|
-IntC sg t =
-error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
-
-fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
-let
-val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
-val st_typ = fst_type(snd_type aut_typ)
-in
-Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA
-end
-|
-StartC sg t =
-error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
-
-fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
-let
-val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
-val tr_typ = fst_type(snd_type(snd_type aut_typ))
-in
-Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA
-end
-|
-TransC sg t =
-error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
-
-fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
-let
-val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
-val sig_typ = fst_type aut_typ;
-val int_typ = fst_type sig_typ
-in
-Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
- (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA)
-end
-|
-IntA sg t =
-error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
-
-fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
-let
-val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
-val st_typ = fst_type(snd_type aut_typ)
-in
-Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA
-end
-|
-StartA sg t =
-error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
-
-fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
-let
-val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
-val tr_typ = fst_type(snd_type(snd_type aut_typ))
-in
-Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA 
-end
-|
-TransA sg t =
-error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
-
-fun delete_ul [] = []
-| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
-        then (let val (_::_::_::s) = xs in delete_ul s end)
-        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
-                then  (let val (_::_::_::s) = xs in delete_ul s end)
-                else (x::delete_ul xs));
-
-fun delete_ul_string s = implode(delete_ul (explode s));
-
-fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
-type_list_of sign a = [(Sign.string_of_typ sign a)];
-
-fun structured_tuple l (Type("*",s::t::_)) =
-let
-val (r,str) = structured_tuple l s;
-in
-(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")")
-end |
-structured_tuple (a::r) t = (r,a) |
-structured_tuple [] _ = raise malformed;
-
-fun varlist_of _ _ [] = [] |
-varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
-
-fun string_of [] = "" |
-string_of (a::r) = a ^ " " ^ (string_of r);
-
-fun tupel_typed_of _ _ _ [] = "" |
-tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
-tupel_typed_of sign s n (a::r) =
- s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
-
-fun double_tupel_typed_of _ _ _ _ [] = "" |
-double_tupel_typed_of sign s t n [a] =
- s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
- t ^ (Int.toString(n)) ^ "::" ^ a |
-double_tupel_typed_of sign s t n (a::r) =
- s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
- t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
-
-fun tupel_of _ _ _ [] = "" |
-tupel_of sign s n [a] = s ^ (Int.toString(n)) |
-tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
-
-fun double_tupel_of _ _ _ _ [] = "" |
-double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
-				 t ^ (Int.toString(n)) |
-double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
-		t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
-
-fun eq_string _ _ _ [] = "" |
-eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
-			 t ^ (Int.toString(n)) |
-eq_string s t n (a::r) =
- s ^ (Int.toString(n)) ^ " = " ^
- t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
-
-fun merge_var_and_type [] [] = "" |
-merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
-merge_var_and_type _ _ = raise malformed;
-
-in
-
-fun mk_sim_oracle sign (subgoal, thl) = (
-  let
-    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
-    val concl = Logic.strip_imp_concl subgoal;
-    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
-    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
-	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
-	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
-	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
-	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
-	
-	val action_type_str =
-	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
-
-	val abs_state_type_list =
-	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
-	val con_state_type_list =
-	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
-
-	val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
-
-	val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
-	val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
-	val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
-	val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
-	
-	val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
-	val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
-	val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
-	val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
-	val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
-	val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
-	val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
-	val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
-        val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
-	val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
-
-        val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
-        val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
-        val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
-        val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
-	val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
-        val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
-
-        val abs_post_str = string_of abs_post_varlist;
-	val abs_u_str = string_of abs_u_varlist;
-	val con_post_str = string_of con_post_varlist;
-	
-	val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
-	val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
-        val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
-	val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
-
-	val abs_pre_tupel_struct = snd(
-structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
-	val abs_post_tupel_struct = snd(
-structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
-	val con_pre_tupel_struct = snd(
-structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
-	val con_post_tupel_struct = snd(
-structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
-in
-(
-OldGoals.push_proof();
-Goal 
-( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
-  "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
-  "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
-	"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
-  "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
-	"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
-  "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
-	")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
-  "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
-	")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
-  "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
-	"). ? (a::(" ^ action_type_str ^
-	")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
-  ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
-	 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
-	 ") & P(" ^ abs_u_t_tupel ^ ")))" ^
-  ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
-	")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
-	")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
-	". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
-	"Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
-  ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
-	"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
-	". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
-  ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
- ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
-	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
-	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
-by (REPEAT (rtac impI 1));
-by (REPEAT (dtac eq_reflection 1));
-(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
-                              delsimps [not_iff,split_part])
-			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
-                                        rename_simps @ ioa_simps @ asig_simps)) 1);
-by (full_simp_tac
-  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
-by (REPEAT (if_full_simp_tac
-  (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
-by (call_mucke_tac 1);
-(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
-by (atac 1);
-result();
-OldGoals.pop_proof();
-Logic.strip_imp_concl subgoal
-)
-end)
-handle malformed =>
-error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
-
-end
diff -r c0695a818c09 -r a7b425bb668c src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Apr 26 16:39:31 2007 +0200
@@ -17,4 +17,284 @@
   Move_of_A :: "'a => 'b => bool"
   isSimCA :: "'a => bool"
 
+ML {*
+
+(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
+	There, implementation relations for I/O automatons are proved using
+	the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
+
+exception SimFailureExn of string;
+
+val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"];
+val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def",
+  thm "asig_internals_def", thm "actions_def"];
+val comp_simps = [thm "par_def", thm "asig_comp_def"];
+val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"];
+val hide_simps = [thm "hide_def", thm "hide_asig_def"];
+val rename_simps = [thm "rename_def", thm "rename_set_def"];
+
+local
+
+exception malformed;
+
+fun fst_type (Type("*",[a,_])) = a |
+fst_type _ = raise malformed; 
+fun snd_type (Type("*",[_,a])) = a |
+snd_type _ = raise malformed;
+
+fun element_type (Type("set",[a])) = a |
+element_type t = raise malformed;
+
+fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
+let
+val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
+val sig_typ = fst_type aut_typ;
+val int_typ = fst_type sig_typ
+in 
+Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
+ (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA)
 end
+|
+IntC sg t =
+error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
+
+fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
+let
+val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
+val st_typ = fst_type(snd_type aut_typ)
+in
+Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA
+end
+|
+StartC sg t =
+error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
+
+fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
+let
+val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
+val tr_typ = fst_type(snd_type(snd_type aut_typ))
+in
+Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA
+end
+|
+TransC sg t =
+error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
+
+fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
+let
+val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
+val sig_typ = fst_type aut_typ;
+val int_typ = fst_type sig_typ
+in
+Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
+ (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA)
+end
+|
+IntA sg t =
+error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
+
+fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
+let
+val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
+val st_typ = fst_type(snd_type aut_typ)
+in
+Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA
+end
+|
+StartA sg t =
+error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
+
+fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
+let
+val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
+val tr_typ = fst_type(snd_type(snd_type aut_typ))
+in
+Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA 
+end
+|
+TransA sg t =
+error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
+
+fun delete_ul [] = []
+| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
+        then (let val (_::_::_::s) = xs in delete_ul s end)
+        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
+                then  (let val (_::_::_::s) = xs in delete_ul s end)
+                else (x::delete_ul xs));
+
+fun delete_ul_string s = implode(delete_ul (explode s));
+
+fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
+type_list_of sign a = [(Sign.string_of_typ sign a)];
+
+fun structured_tuple l (Type("*",s::t::_)) =
+let
+val (r,str) = structured_tuple l s;
+in
+(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")")
+end |
+structured_tuple (a::r) t = (r,a) |
+structured_tuple [] _ = raise malformed;
+
+fun varlist_of _ _ [] = [] |
+varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
+
+fun string_of [] = "" |
+string_of (a::r) = a ^ " " ^ (string_of r);
+
+fun tupel_typed_of _ _ _ [] = "" |
+tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
+tupel_typed_of sign s n (a::r) =
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
+
+fun double_tupel_typed_of _ _ _ _ [] = "" |
+double_tupel_typed_of sign s t n [a] =
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (Int.toString(n)) ^ "::" ^ a |
+double_tupel_typed_of sign s t n (a::r) =
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
+
+fun tupel_of _ _ _ [] = "" |
+tupel_of sign s n [a] = s ^ (Int.toString(n)) |
+tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
+
+fun double_tupel_of _ _ _ _ [] = "" |
+double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
+				 t ^ (Int.toString(n)) |
+double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
+		t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
+
+fun eq_string _ _ _ [] = "" |
+eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
+			 t ^ (Int.toString(n)) |
+eq_string s t n (a::r) =
+ s ^ (Int.toString(n)) ^ " = " ^
+ t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
+
+fun merge_var_and_type [] [] = "" |
+merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
+merge_var_and_type _ _ = raise malformed;
+
+in
+
+fun mk_sim_oracle sign (subgoal, thl) = (
+  let
+    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
+    val concl = Logic.strip_imp_concl subgoal;
+    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
+    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
+	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
+	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
+	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
+	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
+	
+	val action_type_str =
+	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
+
+	val abs_state_type_list =
+	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
+	val con_state_type_list =
+	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
+
+	val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
+
+	val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
+	val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
+	val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
+	val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
+	
+	val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
+	val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
+	val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
+	val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
+	val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
+	val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
+	val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
+	val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
+        val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
+	val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
+
+        val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
+        val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
+        val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
+        val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
+	val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
+        val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
+
+        val abs_post_str = string_of abs_post_varlist;
+	val abs_u_str = string_of abs_u_varlist;
+	val con_post_str = string_of con_post_varlist;
+	
+	val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
+	val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
+        val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
+	val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
+
+	val abs_pre_tupel_struct = snd(
+structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
+	val abs_post_tupel_struct = snd(
+structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
+	val con_pre_tupel_struct = snd(
+structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
+	val con_post_tupel_struct = snd(
+structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
+in
+(
+OldGoals.push_proof();
+Goal 
+( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
+  "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
+  "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
+	"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
+  "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
+	"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
+  "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
+	")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
+  "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
+	")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
+  "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
+	"). ? (a::(" ^ action_type_str ^
+	")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
+  ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
+	 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
+	 ") & P(" ^ abs_u_t_tupel ^ ")))" ^
+  ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
+	")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
+	")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
+	". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
+	"Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
+  ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
+	"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
+	". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
+  ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
+ ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
+	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
+	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
+by (REPEAT (rtac impI 1));
+by (REPEAT (dtac eq_reflection 1));
+(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
+by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
+                              delsimps [not_iff,split_part])
+			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
+                                        rename_simps @ ioa_simps @ asig_simps)) 1);
+by (full_simp_tac
+  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
+by (REPEAT (if_full_simp_tac
+  (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+by (call_mucke_tac 1);
+(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
+by (atac 1);
+result();
+OldGoals.pop_proof();
+Logic.strip_imp_concl subgoal
+)
+end)
+handle malformed =>
+error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
+
+end
+
+*}
+
+end
diff -r c0695a818c09 -r a7b425bb668c src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Apr 26 16:39:14 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-
-(* $Id$ *)
-
-(* call_sim_tac invokes oracle "Sim" *)
-fun call_sim_tac thm_list i state = 
-let val thy = Thm.theory_of_thm state;
-        val (subgoal::_) = Library.drop(i-1,prems_of state);
-        val OraAss = sim_oracle thy (subgoal,thm_list);
-in cut_facts_tac [OraAss] i state end;
-
-
-val ioa_implements_def = thm "ioa_implements_def";
-
-(* is_sim_tac makes additionally to call_sim_tac some simplifications,
-	which are suitable for implementation realtion formulas *)
-fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
-  EVERY [REPEAT (etac thin_rl i),
-	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
-         rtac conjI i,
-         rtac conjI (i+1),
-	 TRY(call_sim_tac thm_list (i+2)),
-	 TRY(atac (i+2)), 
-         REPEAT(rtac refl (i+2)),
-	 simp_tac (simpset() addsimps (thm_list @
-				       comp_simps @ restrict_simps @ hide_simps @
-				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
-	 simp_tac (simpset() addsimps (thm_list @
-				       comp_simps @ restrict_simps @ hide_simps @
-				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
diff -r c0695a818c09 -r a7b425bb668c src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:31 2007 +0200
@@ -8,4 +8,34 @@
 oracle sim_oracle ("term * thm list") =
   mk_sim_oracle
 
+ML {*
+(* call_sim_tac invokes oracle "Sim" *)
+fun call_sim_tac thm_list i state = 
+let val thy = Thm.theory_of_thm state;
+        val (subgoal::_) = Library.drop(i-1,prems_of state);
+        val OraAss = sim_oracle thy (subgoal,thm_list);
+in cut_facts_tac [OraAss] i state end;
+
+
+val ioa_implements_def = thm "ioa_implements_def";
+
+(* is_sim_tac makes additionally to call_sim_tac some simplifications,
+	which are suitable for implementation realtion formulas *)
+fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
+  EVERY [REPEAT (etac thin_rl i),
+	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
+         rtac conjI i,
+         rtac conjI (i+1),
+	 TRY(call_sim_tac thm_list (i+2)),
+	 TRY(atac (i+2)), 
+         REPEAT(rtac refl (i+2)),
+	 simp_tac (simpset() addsimps (thm_list @
+				       comp_simps @ restrict_simps @ hide_simps @
+				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
+	 simp_tac (simpset() addsimps (thm_list @
+				       comp_simps @ restrict_simps @ hide_simps @
+				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
+
+*}
+
 end
diff -r c0695a818c09 -r a7b425bb668c src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Apr 26 16:39:14 2007 +0200
+++ b/src/HOLCF/IsaMakefile	Thu Apr 26 16:39:31 2007 +0200
@@ -116,9 +116,8 @@
 IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz
 
 $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \
-  IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.ML IOA/Modelcheck/MuIOA.thy \
-  IOA/Modelcheck/MuIOAOracle.ML IOA/Modelcheck/MuIOAOracle.thy \
-  IOA/Modelcheck/Ring3.thy 
+  IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \
+  IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck