--- 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
--- 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 ();
--- 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
--- 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 ();
--- 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
--- 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
--- 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
--- 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)]);
--- 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
--- 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