removed legacy ML files;
authorwenzelm
Thu Apr 26 16:39:31 2007 +0200 (2007-04-26)
changeset 22819a7b425bb668c
parent 22818 c0695a818c09
child 22820 e6803064a469
removed legacy ML files;
src/HOL/IsaMakefile
src/HOL/Modelcheck/EindhovenSyn.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.ML
src/HOL/Modelcheck/MuckeSyn.thy
src/HOLCF/IOA/Modelcheck/MuIOA.ML
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
src/HOLCF/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Thu Apr 26 16:39:14 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Apr 26 16:39:31 2007 +0200
     1.3 @@ -469,11 +469,10 @@
     1.4  HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
     1.5  
     1.6  $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
     1.7 -  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.ML \
     1.8 -  Modelcheck/EindhovenSyn.thy Modelcheck/MuCalculus.thy \
     1.9 -  Modelcheck/MuckeExample1.thy Modelcheck/MuckeExample2.thy \
    1.10 -  Modelcheck/MuckeSyn.ML Modelcheck/MuckeSyn.thy Modelcheck/ROOT.ML \
    1.11 -  Modelcheck/mucke_oracle.ML
    1.12 +  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
    1.13 +  Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
    1.14 +  Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
    1.15 +  Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
    1.16  	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
    1.17  
    1.18  
     2.1 --- a/src/HOL/Modelcheck/EindhovenSyn.ML	Thu Apr 26 16:39:14 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,24 +0,0 @@
     2.4 -(*  Title:      HOL/Modelcheck/EindhovenSyn.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     2.7 -    Copyright   1997  TU Muenchen
     2.8 -*)
     2.9 -
    2.10 -fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
    2.11 -  let
    2.12 -    val thy = Thm.theory_of_thm state;
    2.13 -    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
    2.14 -  in cut_facts_tac [assertion] i THEN atac i end) i state;
    2.15 -
    2.16 -val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
    2.17 -
    2.18 -val pair_eta_expand_proc =
    2.19 -  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    2.20 -  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    2.21 -
    2.22 -val Eindhoven_ss =
    2.23 -  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    2.24 -
    2.25 -(*check if user has pmu installed*)
    2.26 -fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    2.27 -fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
     3.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:14 2007 +0200
     3.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:31 2007 +0200
     3.3 @@ -59,4 +59,25 @@
     3.4  end
     3.5  *}
     3.6  
     3.7 +ML {*
     3.8 +fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
     3.9 +  let
    3.10 +    val thy = Thm.theory_of_thm state;
    3.11 +    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
    3.12 +  in cut_facts_tac [assertion] i THEN atac i end) i state;
    3.13 +
    3.14 +val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
    3.15 +
    3.16 +val pair_eta_expand_proc =
    3.17 +  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    3.18 +  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    3.19 +
    3.20 +val Eindhoven_ss =
    3.21 +  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    3.22 +
    3.23 +(*check if user has pmu installed*)
    3.24 +fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    3.25 +fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
    3.26 +*}
    3.27 +
    3.28  end
     4.1 --- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Apr 26 16:39:14 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,171 +0,0 @@
     4.4 -
     4.5 -(* $Id$ *)
     4.6 -
     4.7 -(* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
     4.8 -   it yields innermost one. If no Mu term is present, search_mu yields NONE
     4.9 -*)
    4.10 -
    4.11 -(* extended for treatment of nu (TH) *)
    4.12 -fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
    4.13 -	(case (search_mu t2) of
    4.14 -	      SOME t => SOME t 
    4.15 -	    | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2))
    4.16 -  | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
    4.17 -        (case (search_mu t2) of
    4.18 -              SOME t => SOME t
    4.19 -            | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2))
    4.20 -  | search_mu (t1 $ t2) = 
    4.21 -	(case (search_mu t1) of
    4.22 -	      SOME t => SOME t 
    4.23 -	    | NONE     => search_mu t2)
    4.24 -  | search_mu (Abs(_,_,t)) = search_mu t
    4.25 -  | search_mu _ = NONE;
    4.26 -
    4.27 -
    4.28 -
    4.29 -
    4.30 -(* seraching a variable in a term. Used in move_mus to extract the
    4.31 -   term-rep of var b in hthm *)
    4.32 -
    4.33 -fun search_var s t =
    4.34 -case t of
    4.35 -     t1 $ t2 => (case (search_var s t1) of
    4.36 -		             SOME tt => SOME tt |
    4.37 -			     NONE => search_var s t2) |
    4.38 -     Abs(_,_,t) => search_var s t |
    4.39 -     Var((s1,_),_) => if s = s1 then SOME t else NONE |
    4.40 -     _ => NONE;
    4.41 -	
    4.42 -
    4.43 -(* function move_mus:
    4.44 -   Mucke can't deal with nested Mu terms. move_mus i searches for 
    4.45 -   Mu terms in the subgoal i and replaces Mu terms in the conclusion
    4.46 -   by constants and definitions in the premises recursively.
    4.47 -
    4.48 -   move_thm is the theorem the performs the replacement. To create NEW
    4.49 -   names for the Mu terms, the indizes of move_thm are incremented by
    4.50 -   max_idx of the subgoal.
    4.51 -*)
    4.52 -
    4.53 -local
    4.54 -
    4.55 -  val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
    4.56 -	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
    4.57 -		     REPEAT (resolve_tac prems 1)]);
    4.58 -
    4.59 -  val sig_move_thm = Thm.theory_of_thm move_thm;
    4.60 -  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
    4.61 -  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
    4.62 -
    4.63 -in
    4.64 -
    4.65 -fun move_mus i state =
    4.66 -let val sign = Thm.theory_of_thm state;
    4.67 -    val (subgoal::_) = Library.drop(i-1,prems_of state);
    4.68 -    val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    4.69 -    val redex = search_mu concl;
    4.70 -    val idx = let val t = #maxidx (rep_thm state) in 
    4.71 -	      if t < 0 then 1 else t+1 end;
    4.72 -in
    4.73 -case redex of
    4.74 -     NONE => all_tac state |
    4.75 -     SOME redexterm => 
    4.76 -	let val Credex = cterm_of sign redexterm;
    4.77 -	    val aiCterm = 
    4.78 -		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
    4.79 -	    val inst_move_thm = cterm_instantiate 
    4.80 -				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
    4.81 -	in
    4.82 -            ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
    4.83 -		THEN (move_mus i)) state
    4.84 -	end
    4.85 -end;
    4.86 -end;
    4.87 -
    4.88 -
    4.89 -fun call_mucke_tac i state =
    4.90 -let val thy = Thm.theory_of_thm state;
    4.91 -    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
    4.92 -in 
    4.93 -(cut_facts_tac [OraAss] i) state
    4.94 -end;
    4.95 -
    4.96 -
    4.97 -(* transforming fun-defs into lambda-defs *)
    4.98 -
    4.99 -val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
   4.100 - by (rtac (extensional eq) 1);
   4.101 -qed "ext_rl";
   4.102 -
   4.103 -infix cc;
   4.104 -
   4.105 -fun NONE cc xl = xl
   4.106 -  | (SOME x) cc xl = x::xl;
   4.107 -
   4.108 -fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
   4.109 -  | getargs (x $ (Var ((y,_),_))) = y;
   4.110 -
   4.111 -fun getfun ((x $ y) $ z) = getfun (x $ y)
   4.112 -  | getfun (x $ _) = x;
   4.113 -
   4.114 -local
   4.115 -
   4.116 -fun delete_bold [] = []
   4.117 -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   4.118 -        then (let val (_::_::_::s) = xs in delete_bold s end)
   4.119 -        else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
   4.120 -                then  (let val (_::_::_::s) = xs in delete_bold s end)
   4.121 -                else (x::delete_bold xs));
   4.122 -
   4.123 -fun delete_bold_string s = implode(delete_bold (explode s));
   4.124 -
   4.125 -in
   4.126 -
   4.127 -(* extension with removing bold font (TH) *)
   4.128 -fun mk_lam_def (_::_) _ _ = NONE  
   4.129 -  | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   4.130 -  | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
   4.131 -    let val thy = theory_of_thm t;
   4.132 -	val fnam = Sign.string_of_term thy (getfun LHS);
   4.133 -	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
   4.134 -	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   4.135 -    in
   4.136 -	SOME (prove_goal thy gl (fn prems =>
   4.137 -  		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
   4.138 -    end
   4.139 -| mk_lam_def [] _ t= NONE; 
   4.140 -
   4.141 -fun mk_lam_defs ([]:thm list) = ([]: thm list) 
   4.142 -  | mk_lam_defs (t::l) = 
   4.143 -      (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
   4.144 -
   4.145 -end;
   4.146 -
   4.147 -
   4.148 -(* first simplification, then model checking *)
   4.149 -
   4.150 -val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
   4.151 -
   4.152 -val pair_eta_expand_proc =
   4.153 -  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   4.154 -  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
   4.155 -
   4.156 -val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
   4.157 -
   4.158 -
   4.159 -(* the interface *)
   4.160 -
   4.161 -fun mc_mucke_tac defs i state =
   4.162 -  (case Library.drop (i - 1, Thm.prems_of state) of
   4.163 -    [] => no_tac state
   4.164 -  | subgoal :: _ =>
   4.165 -      EVERY [
   4.166 -        REPEAT (etac thin_rl i),
   4.167 -        cut_facts_tac (mk_lam_defs defs) i,
   4.168 -        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
   4.169 -        move_mus i, call_mucke_tac i,atac i,
   4.170 -        REPEAT (rtac refl i)] state);
   4.171 -
   4.172 -(*check if user has mucke installed*)
   4.173 -fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
   4.174 -fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
     5.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Apr 26 16:39:14 2007 +0200
     5.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Apr 26 16:39:31 2007 +0200
     5.3 @@ -71,6 +71,176 @@
     5.4  oracle mc_mucke_oracle ("term") =
     5.5    mk_mc_mucke_oracle
     5.6  
     5.7 -end
     5.8 +ML {*
     5.9 +(* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
    5.10 +   it yields innermost one. If no Mu term is present, search_mu yields NONE
    5.11 +*)
    5.12 +
    5.13 +(* extended for treatment of nu (TH) *)
    5.14 +fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
    5.15 +	(case (search_mu t2) of
    5.16 +	      SOME t => SOME t 
    5.17 +	    | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2))
    5.18 +  | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
    5.19 +        (case (search_mu t2) of
    5.20 +              SOME t => SOME t
    5.21 +            | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2))
    5.22 +  | search_mu (t1 $ t2) = 
    5.23 +	(case (search_mu t1) of
    5.24 +	      SOME t => SOME t 
    5.25 +	    | NONE     => search_mu t2)
    5.26 +  | search_mu (Abs(_,_,t)) = search_mu t
    5.27 +  | search_mu _ = NONE;
    5.28 +
    5.29 +
    5.30 +
    5.31 +
    5.32 +(* seraching a variable in a term. Used in move_mus to extract the
    5.33 +   term-rep of var b in hthm *)
    5.34 +
    5.35 +fun search_var s t =
    5.36 +case t of
    5.37 +     t1 $ t2 => (case (search_var s t1) of
    5.38 +		             SOME tt => SOME tt |
    5.39 +			     NONE => search_var s t2) |
    5.40 +     Abs(_,_,t) => search_var s t |
    5.41 +     Var((s1,_),_) => if s = s1 then SOME t else NONE |
    5.42 +     _ => NONE;
    5.43 +	
    5.44 +
    5.45 +(* function move_mus:
    5.46 +   Mucke can't deal with nested Mu terms. move_mus i searches for 
    5.47 +   Mu terms in the subgoal i and replaces Mu terms in the conclusion
    5.48 +   by constants and definitions in the premises recursively.
    5.49 +
    5.50 +   move_thm is the theorem the performs the replacement. To create NEW
    5.51 +   names for the Mu terms, the indizes of move_thm are incremented by
    5.52 +   max_idx of the subgoal.
    5.53 +*)
    5.54 +
    5.55 +local
    5.56 +
    5.57 +  val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
    5.58 +	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
    5.59 +		     REPEAT (resolve_tac prems 1)]);
    5.60 +
    5.61 +  val sig_move_thm = Thm.theory_of_thm move_thm;
    5.62 +  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
    5.63 +  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
    5.64 +
    5.65 +in
    5.66 +
    5.67 +fun move_mus i state =
    5.68 +let val sign = Thm.theory_of_thm state;
    5.69 +    val (subgoal::_) = Library.drop(i-1,prems_of state);
    5.70 +    val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    5.71 +    val redex = search_mu concl;
    5.72 +    val idx = let val t = #maxidx (rep_thm state) in 
    5.73 +	      if t < 0 then 1 else t+1 end;
    5.74 +in
    5.75 +case redex of
    5.76 +     NONE => all_tac state |
    5.77 +     SOME redexterm => 
    5.78 +	let val Credex = cterm_of sign redexterm;
    5.79 +	    val aiCterm = 
    5.80 +		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
    5.81 +	    val inst_move_thm = cterm_instantiate 
    5.82 +				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
    5.83 +	in
    5.84 +            ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
    5.85 +		THEN (move_mus i)) state
    5.86 +	end
    5.87 +end;
    5.88 +end;
    5.89  
    5.90  
    5.91 +fun call_mucke_tac i state =
    5.92 +let val thy = Thm.theory_of_thm state;
    5.93 +    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
    5.94 +in 
    5.95 +(cut_facts_tac [OraAss] i) state
    5.96 +end;
    5.97 +
    5.98 +
    5.99 +(* transforming fun-defs into lambda-defs *)
   5.100 +
   5.101 +val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
   5.102 + by (rtac (extensional eq) 1);
   5.103 +qed "ext_rl";
   5.104 +
   5.105 +infix cc;
   5.106 +
   5.107 +fun NONE cc xl = xl
   5.108 +  | (SOME x) cc xl = x::xl;
   5.109 +
   5.110 +fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
   5.111 +  | getargs (x $ (Var ((y,_),_))) = y;
   5.112 +
   5.113 +fun getfun ((x $ y) $ z) = getfun (x $ y)
   5.114 +  | getfun (x $ _) = x;
   5.115 +
   5.116 +local
   5.117 +
   5.118 +fun delete_bold [] = []
   5.119 +| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   5.120 +        then (let val (_::_::_::s) = xs in delete_bold s end)
   5.121 +        else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
   5.122 +                then  (let val (_::_::_::s) = xs in delete_bold s end)
   5.123 +                else (x::delete_bold xs));
   5.124 +
   5.125 +fun delete_bold_string s = implode(delete_bold (explode s));
   5.126 +
   5.127 +in
   5.128 +
   5.129 +(* extension with removing bold font (TH) *)
   5.130 +fun mk_lam_def (_::_) _ _ = NONE  
   5.131 +  | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   5.132 +  | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
   5.133 +    let val thy = theory_of_thm t;
   5.134 +	val fnam = Sign.string_of_term thy (getfun LHS);
   5.135 +	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
   5.136 +	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   5.137 +    in
   5.138 +	SOME (prove_goal thy gl (fn prems =>
   5.139 +  		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
   5.140 +    end
   5.141 +| mk_lam_def [] _ t= NONE; 
   5.142 +
   5.143 +fun mk_lam_defs ([]:thm list) = ([]: thm list) 
   5.144 +  | mk_lam_defs (t::l) = 
   5.145 +      (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
   5.146 +
   5.147 +end;
   5.148 +
   5.149 +
   5.150 +(* first simplification, then model checking *)
   5.151 +
   5.152 +val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
   5.153 +
   5.154 +val pair_eta_expand_proc =
   5.155 +  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   5.156 +  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
   5.157 +
   5.158 +val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
   5.159 +
   5.160 +
   5.161 +(* the interface *)
   5.162 +
   5.163 +fun mc_mucke_tac defs i state =
   5.164 +  (case Library.drop (i - 1, Thm.prems_of state) of
   5.165 +    [] => no_tac state
   5.166 +  | subgoal :: _ =>
   5.167 +      EVERY [
   5.168 +        REPEAT (etac thin_rl i),
   5.169 +        cut_facts_tac (mk_lam_defs defs) i,
   5.170 +        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
   5.171 +        move_mus i, call_mucke_tac i,atac i,
   5.172 +        REPEAT (rtac refl i)] state);
   5.173 +
   5.174 +(*check if user has mucke installed*)
   5.175 +fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
   5.176 +fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
   5.177 +
   5.178 +*}
   5.179 +
   5.180 +end
     6.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 26 16:39:14 2007 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,276 +0,0 @@
     6.4 -
     6.5 -(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
     6.6 -	There, implementation relations for I/O automatons are proved using
     6.7 -	the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
     6.8 -
     6.9 -exception SimFailureExn of string;
    6.10 -
    6.11 -val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"];
    6.12 -val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def",
    6.13 -  thm "asig_internals_def", thm "actions_def"];
    6.14 -val comp_simps = [thm "par_def", thm "asig_comp_def"];
    6.15 -val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"];
    6.16 -val hide_simps = [thm "hide_def", thm "hide_asig_def"];
    6.17 -val rename_simps = [thm "rename_def", thm "rename_set_def"];
    6.18 -
    6.19 -local
    6.20 -
    6.21 -exception malformed;
    6.22 -
    6.23 -fun fst_type (Type("*",[a,_])) = a |
    6.24 -fst_type _ = raise malformed; 
    6.25 -fun snd_type (Type("*",[_,a])) = a |
    6.26 -snd_type _ = raise malformed;
    6.27 -
    6.28 -fun element_type (Type("set",[a])) = a |
    6.29 -element_type t = raise malformed;
    6.30 -
    6.31 -fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
    6.32 -let
    6.33 -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    6.34 -val sig_typ = fst_type aut_typ;
    6.35 -val int_typ = fst_type sig_typ
    6.36 -in 
    6.37 -Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
    6.38 - (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA)
    6.39 -end
    6.40 -|
    6.41 -IntC sg t =
    6.42 -error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
    6.43 -
    6.44 -fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
    6.45 -let
    6.46 -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    6.47 -val st_typ = fst_type(snd_type aut_typ)
    6.48 -in
    6.49 -Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA
    6.50 -end
    6.51 -|
    6.52 -StartC sg t =
    6.53 -error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
    6.54 -
    6.55 -fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
    6.56 -let
    6.57 -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    6.58 -val tr_typ = fst_type(snd_type(snd_type aut_typ))
    6.59 -in
    6.60 -Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA
    6.61 -end
    6.62 -|
    6.63 -TransC sg t =
    6.64 -error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
    6.65 -
    6.66 -fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    6.67 -let
    6.68 -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    6.69 -val sig_typ = fst_type aut_typ;
    6.70 -val int_typ = fst_type sig_typ
    6.71 -in
    6.72 -Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
    6.73 - (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA)
    6.74 -end
    6.75 -|
    6.76 -IntA sg t =
    6.77 -error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
    6.78 -
    6.79 -fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    6.80 -let
    6.81 -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    6.82 -val st_typ = fst_type(snd_type aut_typ)
    6.83 -in
    6.84 -Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA
    6.85 -end
    6.86 -|
    6.87 -StartA sg t =
    6.88 -error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
    6.89 -
    6.90 -fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    6.91 -let
    6.92 -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    6.93 -val tr_typ = fst_type(snd_type(snd_type aut_typ))
    6.94 -in
    6.95 -Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA 
    6.96 -end
    6.97 -|
    6.98 -TransA sg t =
    6.99 -error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
   6.100 -
   6.101 -fun delete_ul [] = []
   6.102 -| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
   6.103 -        then (let val (_::_::_::s) = xs in delete_ul s end)
   6.104 -        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   6.105 -                then  (let val (_::_::_::s) = xs in delete_ul s end)
   6.106 -                else (x::delete_ul xs));
   6.107 -
   6.108 -fun delete_ul_string s = implode(delete_ul (explode s));
   6.109 -
   6.110 -fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   6.111 -type_list_of sign a = [(Sign.string_of_typ sign a)];
   6.112 -
   6.113 -fun structured_tuple l (Type("*",s::t::_)) =
   6.114 -let
   6.115 -val (r,str) = structured_tuple l s;
   6.116 -in
   6.117 -(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")")
   6.118 -end |
   6.119 -structured_tuple (a::r) t = (r,a) |
   6.120 -structured_tuple [] _ = raise malformed;
   6.121 -
   6.122 -fun varlist_of _ _ [] = [] |
   6.123 -varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
   6.124 -
   6.125 -fun string_of [] = "" |
   6.126 -string_of (a::r) = a ^ " " ^ (string_of r);
   6.127 -
   6.128 -fun tupel_typed_of _ _ _ [] = "" |
   6.129 -tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
   6.130 -tupel_typed_of sign s n (a::r) =
   6.131 - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
   6.132 -
   6.133 -fun double_tupel_typed_of _ _ _ _ [] = "" |
   6.134 -double_tupel_typed_of sign s t n [a] =
   6.135 - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
   6.136 - t ^ (Int.toString(n)) ^ "::" ^ a |
   6.137 -double_tupel_typed_of sign s t n (a::r) =
   6.138 - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
   6.139 - t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
   6.140 -
   6.141 -fun tupel_of _ _ _ [] = "" |
   6.142 -tupel_of sign s n [a] = s ^ (Int.toString(n)) |
   6.143 -tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
   6.144 -
   6.145 -fun double_tupel_of _ _ _ _ [] = "" |
   6.146 -double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
   6.147 -				 t ^ (Int.toString(n)) |
   6.148 -double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
   6.149 -		t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
   6.150 -
   6.151 -fun eq_string _ _ _ [] = "" |
   6.152 -eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
   6.153 -			 t ^ (Int.toString(n)) |
   6.154 -eq_string s t n (a::r) =
   6.155 - s ^ (Int.toString(n)) ^ " = " ^
   6.156 - t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
   6.157 -
   6.158 -fun merge_var_and_type [] [] = "" |
   6.159 -merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
   6.160 -merge_var_and_type _ _ = raise malformed;
   6.161 -
   6.162 -in
   6.163 -
   6.164 -fun mk_sim_oracle sign (subgoal, thl) = (
   6.165 -  let
   6.166 -    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
   6.167 -    val concl = Logic.strip_imp_concl subgoal;
   6.168 -    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
   6.169 -    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
   6.170 -	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
   6.171 -	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
   6.172 -	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
   6.173 -	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
   6.174 -	
   6.175 -	val action_type_str =
   6.176 -	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
   6.177 -
   6.178 -	val abs_state_type_list =
   6.179 -	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
   6.180 -	val con_state_type_list =
   6.181 -	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
   6.182 -
   6.183 -	val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
   6.184 -
   6.185 -	val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
   6.186 -	val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
   6.187 -	val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
   6.188 -	val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
   6.189 -	
   6.190 -	val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
   6.191 -	val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
   6.192 -	val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
   6.193 -	val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
   6.194 -	val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
   6.195 -	val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
   6.196 -	val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
   6.197 -	val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
   6.198 -        val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
   6.199 -	val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
   6.200 -
   6.201 -        val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
   6.202 -        val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
   6.203 -        val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
   6.204 -        val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
   6.205 -	val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
   6.206 -        val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
   6.207 -
   6.208 -        val abs_post_str = string_of abs_post_varlist;
   6.209 -	val abs_u_str = string_of abs_u_varlist;
   6.210 -	val con_post_str = string_of con_post_varlist;
   6.211 -	
   6.212 -	val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
   6.213 -	val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
   6.214 -        val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
   6.215 -	val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
   6.216 -
   6.217 -	val abs_pre_tupel_struct = snd(
   6.218 -structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   6.219 -	val abs_post_tupel_struct = snd(
   6.220 -structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   6.221 -	val con_pre_tupel_struct = snd(
   6.222 -structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   6.223 -	val con_post_tupel_struct = snd(
   6.224 -structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   6.225 -in
   6.226 -(
   6.227 -OldGoals.push_proof();
   6.228 -Goal 
   6.229 -( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
   6.230 -  "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
   6.231 -  "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
   6.232 -	"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
   6.233 -  "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
   6.234 -	"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
   6.235 -  "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   6.236 -	")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
   6.237 -  "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   6.238 -	")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
   6.239 -  "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
   6.240 -	"). ? (a::(" ^ action_type_str ^
   6.241 -	")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
   6.242 -  ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
   6.243 -	 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
   6.244 -	 ") & P(" ^ abs_u_t_tupel ^ ")))" ^
   6.245 -  ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   6.246 -	")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
   6.247 -	")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
   6.248 -	". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
   6.249 -	"Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
   6.250 -  ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
   6.251 -	"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
   6.252 -	". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
   6.253 -  ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
   6.254 - ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
   6.255 -	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
   6.256 -	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
   6.257 -by (REPEAT (rtac impI 1));
   6.258 -by (REPEAT (dtac eq_reflection 1));
   6.259 -(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
   6.260 -by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
   6.261 -                              delsimps [not_iff,split_part])
   6.262 -			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   6.263 -                                        rename_simps @ ioa_simps @ asig_simps)) 1);
   6.264 -by (full_simp_tac
   6.265 -  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
   6.266 -by (REPEAT (if_full_simp_tac
   6.267 -  (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
   6.268 -by (call_mucke_tac 1);
   6.269 -(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
   6.270 -by (atac 1);
   6.271 -result();
   6.272 -OldGoals.pop_proof();
   6.273 -Logic.strip_imp_concl subgoal
   6.274 -)
   6.275 -end)
   6.276 -handle malformed =>
   6.277 -error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
   6.278 -
   6.279 -end
     7.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Apr 26 16:39:14 2007 +0200
     7.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Apr 26 16:39:31 2007 +0200
     7.3 @@ -17,4 +17,284 @@
     7.4    Move_of_A :: "'a => 'b => bool"
     7.5    isSimCA :: "'a => bool"
     7.6  
     7.7 +ML {*
     7.8 +
     7.9 +(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
    7.10 +	There, implementation relations for I/O automatons are proved using
    7.11 +	the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
    7.12 +
    7.13 +exception SimFailureExn of string;
    7.14 +
    7.15 +val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"];
    7.16 +val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def",
    7.17 +  thm "asig_internals_def", thm "actions_def"];
    7.18 +val comp_simps = [thm "par_def", thm "asig_comp_def"];
    7.19 +val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"];
    7.20 +val hide_simps = [thm "hide_def", thm "hide_asig_def"];
    7.21 +val rename_simps = [thm "rename_def", thm "rename_set_def"];
    7.22 +
    7.23 +local
    7.24 +
    7.25 +exception malformed;
    7.26 +
    7.27 +fun fst_type (Type("*",[a,_])) = a |
    7.28 +fst_type _ = raise malformed; 
    7.29 +fun snd_type (Type("*",[_,a])) = a |
    7.30 +snd_type _ = raise malformed;
    7.31 +
    7.32 +fun element_type (Type("set",[a])) = a |
    7.33 +element_type t = raise malformed;
    7.34 +
    7.35 +fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
    7.36 +let
    7.37 +val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    7.38 +val sig_typ = fst_type aut_typ;
    7.39 +val int_typ = fst_type sig_typ
    7.40 +in 
    7.41 +Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
    7.42 + (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA)
    7.43  end
    7.44 +|
    7.45 +IntC sg t =
    7.46 +error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
    7.47 +
    7.48 +fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
    7.49 +let
    7.50 +val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    7.51 +val st_typ = fst_type(snd_type aut_typ)
    7.52 +in
    7.53 +Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA
    7.54 +end
    7.55 +|
    7.56 +StartC sg t =
    7.57 +error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
    7.58 +
    7.59 +fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
    7.60 +let
    7.61 +val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
    7.62 +val tr_typ = fst_type(snd_type(snd_type aut_typ))
    7.63 +in
    7.64 +Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA
    7.65 +end
    7.66 +|
    7.67 +TransC sg t =
    7.68 +error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
    7.69 +
    7.70 +fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    7.71 +let
    7.72 +val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    7.73 +val sig_typ = fst_type aut_typ;
    7.74 +val int_typ = fst_type sig_typ
    7.75 +in
    7.76 +Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
    7.77 + (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA)
    7.78 +end
    7.79 +|
    7.80 +IntA sg t =
    7.81 +error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
    7.82 +
    7.83 +fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    7.84 +let
    7.85 +val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    7.86 +val st_typ = fst_type(snd_type aut_typ)
    7.87 +in
    7.88 +Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA
    7.89 +end
    7.90 +|
    7.91 +StartA sg t =
    7.92 +error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
    7.93 +
    7.94 +fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
    7.95 +let
    7.96 +val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
    7.97 +val tr_typ = fst_type(snd_type(snd_type aut_typ))
    7.98 +in
    7.99 +Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA 
   7.100 +end
   7.101 +|
   7.102 +TransA sg t =
   7.103 +error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
   7.104 +
   7.105 +fun delete_ul [] = []
   7.106 +| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
   7.107 +        then (let val (_::_::_::s) = xs in delete_ul s end)
   7.108 +        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   7.109 +                then  (let val (_::_::_::s) = xs in delete_ul s end)
   7.110 +                else (x::delete_ul xs));
   7.111 +
   7.112 +fun delete_ul_string s = implode(delete_ul (explode s));
   7.113 +
   7.114 +fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   7.115 +type_list_of sign a = [(Sign.string_of_typ sign a)];
   7.116 +
   7.117 +fun structured_tuple l (Type("*",s::t::_)) =
   7.118 +let
   7.119 +val (r,str) = structured_tuple l s;
   7.120 +in
   7.121 +(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")")
   7.122 +end |
   7.123 +structured_tuple (a::r) t = (r,a) |
   7.124 +structured_tuple [] _ = raise malformed;
   7.125 +
   7.126 +fun varlist_of _ _ [] = [] |
   7.127 +varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
   7.128 +
   7.129 +fun string_of [] = "" |
   7.130 +string_of (a::r) = a ^ " " ^ (string_of r);
   7.131 +
   7.132 +fun tupel_typed_of _ _ _ [] = "" |
   7.133 +tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
   7.134 +tupel_typed_of sign s n (a::r) =
   7.135 + s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
   7.136 +
   7.137 +fun double_tupel_typed_of _ _ _ _ [] = "" |
   7.138 +double_tupel_typed_of sign s t n [a] =
   7.139 + s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
   7.140 + t ^ (Int.toString(n)) ^ "::" ^ a |
   7.141 +double_tupel_typed_of sign s t n (a::r) =
   7.142 + s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
   7.143 + t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
   7.144 +
   7.145 +fun tupel_of _ _ _ [] = "" |
   7.146 +tupel_of sign s n [a] = s ^ (Int.toString(n)) |
   7.147 +tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
   7.148 +
   7.149 +fun double_tupel_of _ _ _ _ [] = "" |
   7.150 +double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
   7.151 +				 t ^ (Int.toString(n)) |
   7.152 +double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
   7.153 +		t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
   7.154 +
   7.155 +fun eq_string _ _ _ [] = "" |
   7.156 +eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
   7.157 +			 t ^ (Int.toString(n)) |
   7.158 +eq_string s t n (a::r) =
   7.159 + s ^ (Int.toString(n)) ^ " = " ^
   7.160 + t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
   7.161 +
   7.162 +fun merge_var_and_type [] [] = "" |
   7.163 +merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
   7.164 +merge_var_and_type _ _ = raise malformed;
   7.165 +
   7.166 +in
   7.167 +
   7.168 +fun mk_sim_oracle sign (subgoal, thl) = (
   7.169 +  let
   7.170 +    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
   7.171 +    val concl = Logic.strip_imp_concl subgoal;
   7.172 +    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
   7.173 +    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
   7.174 +	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
   7.175 +	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
   7.176 +	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
   7.177 +	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
   7.178 +	
   7.179 +	val action_type_str =
   7.180 +	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
   7.181 +
   7.182 +	val abs_state_type_list =
   7.183 +	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
   7.184 +	val con_state_type_list =
   7.185 +	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
   7.186 +
   7.187 +	val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
   7.188 +
   7.189 +	val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
   7.190 +	val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
   7.191 +	val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
   7.192 +	val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
   7.193 +	
   7.194 +	val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
   7.195 +	val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
   7.196 +	val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
   7.197 +	val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
   7.198 +	val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
   7.199 +	val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
   7.200 +	val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
   7.201 +	val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
   7.202 +        val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
   7.203 +	val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
   7.204 +
   7.205 +        val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
   7.206 +        val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
   7.207 +        val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
   7.208 +        val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
   7.209 +	val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
   7.210 +        val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
   7.211 +
   7.212 +        val abs_post_str = string_of abs_post_varlist;
   7.213 +	val abs_u_str = string_of abs_u_varlist;
   7.214 +	val con_post_str = string_of con_post_varlist;
   7.215 +	
   7.216 +	val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
   7.217 +	val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
   7.218 +        val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
   7.219 +	val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
   7.220 +
   7.221 +	val abs_pre_tupel_struct = snd(
   7.222 +structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   7.223 +	val abs_post_tupel_struct = snd(
   7.224 +structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   7.225 +	val con_pre_tupel_struct = snd(
   7.226 +structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   7.227 +	val con_post_tupel_struct = snd(
   7.228 +structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   7.229 +in
   7.230 +(
   7.231 +OldGoals.push_proof();
   7.232 +Goal 
   7.233 +( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
   7.234 +  "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
   7.235 +  "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
   7.236 +	"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
   7.237 +  "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
   7.238 +	"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
   7.239 +  "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   7.240 +	")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
   7.241 +  "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   7.242 +	")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
   7.243 +  "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
   7.244 +	"). ? (a::(" ^ action_type_str ^
   7.245 +	")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
   7.246 +  ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
   7.247 +	 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
   7.248 +	 ") & P(" ^ abs_u_t_tupel ^ ")))" ^
   7.249 +  ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   7.250 +	")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
   7.251 +	")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
   7.252 +	". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
   7.253 +	"Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
   7.254 +  ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
   7.255 +	"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
   7.256 +	". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
   7.257 +  ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
   7.258 + ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
   7.259 +	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
   7.260 +	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
   7.261 +by (REPEAT (rtac impI 1));
   7.262 +by (REPEAT (dtac eq_reflection 1));
   7.263 +(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
   7.264 +by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
   7.265 +                              delsimps [not_iff,split_part])
   7.266 +			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   7.267 +                                        rename_simps @ ioa_simps @ asig_simps)) 1);
   7.268 +by (full_simp_tac
   7.269 +  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
   7.270 +by (REPEAT (if_full_simp_tac
   7.271 +  (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
   7.272 +by (call_mucke_tac 1);
   7.273 +(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
   7.274 +by (atac 1);
   7.275 +result();
   7.276 +OldGoals.pop_proof();
   7.277 +Logic.strip_imp_concl subgoal
   7.278 +)
   7.279 +end)
   7.280 +handle malformed =>
   7.281 +error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
   7.282 +
   7.283 +end
   7.284 +
   7.285 +*}
   7.286 +
   7.287 +end
     8.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Apr 26 16:39:14 2007 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,29 +0,0 @@
     8.4 -
     8.5 -(* $Id$ *)
     8.6 -
     8.7 -(* call_sim_tac invokes oracle "Sim" *)
     8.8 -fun call_sim_tac thm_list i state = 
     8.9 -let val thy = Thm.theory_of_thm state;
    8.10 -        val (subgoal::_) = Library.drop(i-1,prems_of state);
    8.11 -        val OraAss = sim_oracle thy (subgoal,thm_list);
    8.12 -in cut_facts_tac [OraAss] i state end;
    8.13 -
    8.14 -
    8.15 -val ioa_implements_def = thm "ioa_implements_def";
    8.16 -
    8.17 -(* is_sim_tac makes additionally to call_sim_tac some simplifications,
    8.18 -	which are suitable for implementation realtion formulas *)
    8.19 -fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
    8.20 -  EVERY [REPEAT (etac thin_rl i),
    8.21 -	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
    8.22 -         rtac conjI i,
    8.23 -         rtac conjI (i+1),
    8.24 -	 TRY(call_sim_tac thm_list (i+2)),
    8.25 -	 TRY(atac (i+2)), 
    8.26 -         REPEAT(rtac refl (i+2)),
    8.27 -	 simp_tac (simpset() addsimps (thm_list @
    8.28 -				       comp_simps @ restrict_simps @ hide_simps @
    8.29 -				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
    8.30 -	 simp_tac (simpset() addsimps (thm_list @
    8.31 -				       comp_simps @ restrict_simps @ hide_simps @
    8.32 -				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
     9.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:14 2007 +0200
     9.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:31 2007 +0200
     9.3 @@ -8,4 +8,34 @@
     9.4  oracle sim_oracle ("term * thm list") =
     9.5    mk_sim_oracle
     9.6  
     9.7 +ML {*
     9.8 +(* call_sim_tac invokes oracle "Sim" *)
     9.9 +fun call_sim_tac thm_list i state = 
    9.10 +let val thy = Thm.theory_of_thm state;
    9.11 +        val (subgoal::_) = Library.drop(i-1,prems_of state);
    9.12 +        val OraAss = sim_oracle thy (subgoal,thm_list);
    9.13 +in cut_facts_tac [OraAss] i state end;
    9.14 +
    9.15 +
    9.16 +val ioa_implements_def = thm "ioa_implements_def";
    9.17 +
    9.18 +(* is_sim_tac makes additionally to call_sim_tac some simplifications,
    9.19 +	which are suitable for implementation realtion formulas *)
    9.20 +fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
    9.21 +  EVERY [REPEAT (etac thin_rl i),
    9.22 +	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
    9.23 +         rtac conjI i,
    9.24 +         rtac conjI (i+1),
    9.25 +	 TRY(call_sim_tac thm_list (i+2)),
    9.26 +	 TRY(atac (i+2)), 
    9.27 +         REPEAT(rtac refl (i+2)),
    9.28 +	 simp_tac (simpset() addsimps (thm_list @
    9.29 +				       comp_simps @ restrict_simps @ hide_simps @
    9.30 +				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
    9.31 +	 simp_tac (simpset() addsimps (thm_list @
    9.32 +				       comp_simps @ restrict_simps @ hide_simps @
    9.33 +				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
    9.34 +
    9.35 +*}
    9.36 +
    9.37  end
    10.1 --- a/src/HOLCF/IsaMakefile	Thu Apr 26 16:39:14 2007 +0200
    10.2 +++ b/src/HOLCF/IsaMakefile	Thu Apr 26 16:39:31 2007 +0200
    10.3 @@ -116,9 +116,8 @@
    10.4  IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz
    10.5  
    10.6  $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \
    10.7 -  IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.ML IOA/Modelcheck/MuIOA.thy \
    10.8 -  IOA/Modelcheck/MuIOAOracle.ML IOA/Modelcheck/MuIOAOracle.thy \
    10.9 -  IOA/Modelcheck/Ring3.thy 
   10.10 +  IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \
   10.11 +  IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy
   10.12  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck
   10.13  
   10.14