--- a/src/HOL/IOA/ABP/Abschannel.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,107 +0,0 @@
-(* Title: HOL/IOA/example/Abschannels.thy
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1994 TU Muenchen
-
-The transmission channel
-*)
-
-Abschannel = IOA + Action + Lemmas + List +
-
-
-datatype ('a)act = S('a) | R('a)
-
-
-consts
-
-ch_asig :: 'a act signature
-ch_trans :: ('a act, 'a list)transition set
-ch_ioa :: ('a act, 'a list)ioa
-
-rsch_actions :: 'm action => bool act option
-srch_actions :: "'m action =>(bool * 'm) act option"
-
-srch_asig,
-rsch_asig :: 'm action signature
-
-srch_trans :: ('m action, 'm packet list)transition set
-rsch_trans :: ('m action, bool list)transition set
-
-srch_ioa :: ('m action, 'm packet list)ioa
-rsch_ioa :: ('m action, bool list)ioa
-
-
-defs
-
-srch_asig_def "srch_asig == asig_of(srch_ioa)"
-rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
-
-srch_trans_def "srch_trans == trans_of(srch_ioa)"
-rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
-
-srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
-rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
-
-
-(**********************************************************
- G e n e r i c C h a n n e l
- *********************************************************)
-
-ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
-
-ch_trans_def "ch_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of S(b) => ((t = s) | (t = s @ [b])) |
- R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
-
-ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
-
-(**********************************************************
- C o n c r e t e C h a n n e l s b y R e n a m i n g
- *********************************************************)
-
-rsch_actions_def "rsch_actions (akt) ==
- case akt of
- Next => None |
- S_msg(m) => None |
- R_msg(m) => None |
- S_pkt(packet) => None |
- R_pkt(packet) => None |
- S_ack(b) => Some(S(b)) |
- R_ack(b) => Some(R(b))"
-
-srch_actions_def "srch_actions (akt) ==
- case akt of
- Next => None |
- S_msg(m) => None |
- R_msg(m) => None |
- S_pkt(p) => Some(S(p)) |
- R_pkt(p) => Some(R(p)) |
- S_ack(b) => None |
- R_ack(b) => None"
-
-
-end
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/IOA/example/Abschannels.thy
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1994 TU Muenchen
-
-The transmission channel -- finite version
-*)
-
-Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
-
-consts
-
-ch_fin_asig :: 'a act signature
-
-ch_fin_trans :: ('a act, 'a list)transition set
-
-ch_fin_ioa :: ('a act, 'a list)ioa
-
-srch_fin_asig,
-rsch_fin_asig :: 'm action signature
-
-srch_fin_trans :: ('m action, 'm packet list)transition set
-rsch_fin_trans :: ('m action, bool list)transition set
-
-srch_fin_ioa :: ('m action, 'm packet list)ioa
-rsch_fin_ioa :: ('m action, bool list)ioa
-
-reverse :: 'a list => 'a list
-
-primrec
- reverse List.list
- reverse_Nil "reverse([]) = []"
- reverse_Cons "reverse(x#xs) = reverse(xs)@[x]"
-
-defs
-
-srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)"
-rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)"
-
-srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)"
-rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)"
-
-srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa srch_actions"
-rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa rsch_actions"
-
-
-ch_fin_asig_def "ch_fin_asig == ch_asig"
-
-ch_fin_trans_def "ch_fin_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of S(b) => ((t = s) |
- (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
- R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
-
-ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
-
-end
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/IOA/ABP/Action.ML Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/IOA/example/Action.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-Derived rules for actions
-*)
-
-goal Action.thy "!!x. x = y ==> action_case a b c d e f g x = \
-\ action_case a b c d e f g y";
-by (Asm_simp_tac 1);
-
-Addcongs [result()];
--- a/src/HOL/IOA/ABP/Action.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/IOA/example/Action.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The set of all actions of the system
-*)
-
-Action = Packet +
-datatype 'm action = Next | S_msg ('m) | R_msg ('m)
- | S_pkt ('m packet) | R_pkt ('m packet)
- | S_ack (bool) | R_ack (bool)
-end
--- a/src/HOL/IOA/ABP/Check.ML Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,170 +0,0 @@
-
-
-
-(* ----------------------------------------------------------------
- P r o t o t y p e M o d e l C h e c k e r
- ----------------------------------------------------------------*)
-
-fun check(extacts,intacts,string_of_a,startsI,string_of_s,
- nexts,hom,transA,startsS) =
- let fun check_s(s,unchecked,checked) =
- let fun check_sa(unchecked,a) =
- let fun check_sas(unchecked,t) =
- (if a mem extacts then
- (if transA(hom s,a,hom t) then ( )
- else (writeln("Error: Mapping of Externals!");
- string_of_s s; writeln"";
- string_of_a a; writeln"";
- string_of_s t;writeln"";writeln"" ))
- else (if hom(s)=hom(t) then ( )
- else (writeln("Error: Mapping of Internals!");
- string_of_s s; writeln"";
- string_of_a a; writeln"";
- string_of_s t;writeln"";writeln"" ));
- if t mem checked then unchecked else t ins unchecked)
- in foldl check_sas (unchecked,nexts s a) end;
- val unchecked' = foldl check_sa (unchecked,extacts @ intacts)
- in (if s mem startsI then
- (if hom(s) mem startsS then ()
- else writeln("Error: At start states!"))
- else ();
- checks(unchecked',s::checked)) end
- and checks([],_) = ()
- | checks(s::unchecked,checked) = check_s(s,unchecked,checked)
- in checks(startsI,[]) end;
-
-
-(* ------------------------------------------------------
- A B P E x a m p l e
- -------------------------------------------------------*)
-
-datatype msg = m | n | l;
-datatype act = Next | S_msg of msg | R_msg of msg
- | S_pkt of bool * msg | R_pkt of bool * msg
- | S_ack of bool | R_ack of bool;
-
-(* -------------------- Transition relation of Specification -----------*)
-
-fun transA((u,s),a,(v,t)) =
- (case a of
- Next => v andalso t = s |
- S_msg(q) => u andalso not(v) andalso t = s@[q] |
- R_msg(q) => u = v andalso s = (q::t) |
- S_pkt(b,q) => false |
- R_pkt(b,q) => false |
- S_ack(b) => false |
- R_ack(b) => false);
-
-
-(* ---------------------- Abstraction function --------------------------*)
-
-fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
-
-
-(* --------------------- Transition relation of Implementation ----------*)
-
-fun nexts (s as (env,p,a,q,b,ch1,ch2)) action =
- (case action of
- Next => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] |
- S_msg(mornorl) => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] |
- R_msg(mornorl) => if (q<>[] andalso mornorl=hd(q))
- then [(env,p,a,tl(q),b,ch1,ch2)]
- else [] |
- S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a)
- then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl))
- then [s]
- else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)])
- else [] |
- R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl))
- then (if (h<>b andalso q=[])
- then [(env,p,a,q@[mornorl],not(b),ch1,ch2),
- (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)]
- else [s,(env,p,a,q,b,tl(ch1),ch2)])
- else [] |
- S_ack(h) => if (h=b)
- then (if (ch2<>[] andalso h=hd(rev(ch2)))
- then [s]
- else [s,(env,p,a,q,b,ch1,ch2@[h])])
- else [] |
- R_ack(h) => if (ch2<>[] andalso hd(ch2)=h)
- then (if h=a
- then [(env,tl(p),not(a),q,b,ch1,ch2),
- (env,tl(p),not(a),q,b,ch1,tl(ch2))]
- else [s,(env,p,a,q,b,ch1,tl(ch2))])
- else [])
-
-
-val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
-val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true),
- S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false),
- S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l),
- S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)];
-
-
-(* ------------------------------------
- Input / Output utilities
- ------------------------------------*)
-
-fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
- let fun prec x = (prs ","; pre x)
- in
- (case lll of
- [] => (prs lpar; prs rpar)
- | x::lll => (prs lpar; pre x; seq prec lll; prs rpar))
- end;
-
-fun pr_bool true = output(std_out,"true")
-| pr_bool false = output(std_out,"false");
-
-fun pr_msg m = output(std_out,"m")
-| pr_msg n = output(std_out,"n")
-| pr_msg l = output(std_out,"l");
-
-fun pr_act a = output(std_out, case a of
- Next => "Next"|
- S_msg(ma) => "S_msg(ma)" |
- R_msg(ma) => "R_msg(ma)" |
- S_pkt(b,ma) => "S_pkt(b,ma)" |
- R_pkt(b,ma) => "R_pkt(b,ma)" |
- S_ack(b) => "S_ack(b)" |
- R_ack(b) => "R_ack(b)");
-
-fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">");
-
-val pr_bool_list = print_list("[","]",pr_bool);
-val pr_msg_list = print_list("[","]",pr_msg);
-val pr_pkt_list = print_list("[","]",pr_pkt);
-
-fun pr_tuple (env,p,a,q,b,ch1,ch2) =
- (prs "{"; pr_bool env; prs ", "; pr_msg_list p; prs ", ";
- pr_bool a; prs ", "; pr_msg_list q; prs ", ";
- pr_bool b; prs ", "; pr_pkt_list ch1; prs ", ";
- pr_bool_list ch2; prs "}");
-
-
-
-(* ---------------------------------
- Main function call
- ---------------------------------*)
-
-(*
-check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])],
- pr_tuple, nexts, hom, transA, [(true,[])]);
-*)
-
-
-
-
-
-(*
- Little test example
-
-datatype act = A;
-fun transA(s,a,t) = (not(s)=t);
-fun hom(i) = i mod 2 = 0;
-fun nexts s A = [(s+1) mod 4];
-check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
-
-fun nexts s A = [(s+1) mod 5];
-
-*)
--- a/src/HOL/IOA/ABP/Correctness.ML Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,392 +0,0 @@
- (* Title: HOL/IOA/example/Correctness.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-*)
-
-open Correctness; open Abschannel; open Abschannel_finite;
-open Impl; open Impl_finite;
-
-goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
-by (Fast_tac 1);
-qed"exis_elim";
-
-Delsimps [split_paired_All];
-Addsimps
- ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def,
- ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def,
- actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def,
- trans_of_def] @ asig_projections @ set_lemmas);
-
-val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def,
- rsch_fin_ioa_def, srch_fin_ioa_def,
- ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def];
-Addsimps abschannel_fin;
-
-val impl_ioas = [Sender.sender_ioa_def,Receiver.receiver_ioa_def];
-val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def];
-val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def];
-Addcongs [let_weak_cong];
-Addsimps [Let_def, ioa_triple_proj, starts_of_par];
-
-val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def];
-val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @
- asig_projections @ set_lemmas;
-Addsimps hom_ioas;
-
-Addsimps [reduce_Nil,reduce_Cons];
-
-
-
-(* auxiliary function *)
-fun rotate n i = EVERY(replicate n (etac revcut_rl i));
-
-(* lemmas about reduce *)
-
-goal Correctness.thy "(reduce(l)=[]) = (l=[])";
- by (rtac iffI 1);
- by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
- by (Fast_tac 1);
- by (List.list.induct_tac "l" 1);
- by (Simp_tac 1);
- by (Simp_tac 1);
- by (rtac (expand_list_case RS iffD2) 1);
- by (Asm_full_simp_tac 1);
- by (REPEAT (rtac allI 1));
- by (rtac impI 1);
- by (hyp_subst_tac 1);
- by (rtac (expand_if RS ssubst) 1);
- by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
-val l_iff_red_nil = result();
-
-goal Correctness.thy "s~=[] --> hd(s)=hd(reduce(s))";
-by (List.list.induct_tac "s" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (Asm_full_simp_tac 1);
-(* main case *)
-by (rotate 1 1);
-by (asm_full_simp_tac list_ss 1);
-by (Simp_tac 1);
-by (rtac (expand_list_case RS iffD2) 1);
-by (asm_full_simp_tac list_ss 1);
-by (REPEAT (rtac allI 1));
- by (rtac impI 1);
-by (rtac (expand_if RS ssubst) 1);
-by (REPEAT(hyp_subst_tac 1));
-by (etac subst 1);
-by (Simp_tac 1);
-qed"hd_is_reduce_hd";
-
-(* to be used in the following Lemma *)
-goal Correctness.thy "l~=[] --> reverse(reduce(l))~=[]";
-by (List.list.induct_tac "l" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1);
-(* main case *)
-by (rotate 1 1);
-by (Asm_full_simp_tac 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 1);
-by (Asm_full_simp_tac 1);
-by (REPEAT (etac exE 1));
-by (Asm_simp_tac 1);
-by (rtac (expand_if RS ssubst) 1);
-by (hyp_subst_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1);
-qed"rev_red_not_nil";
-
-(* shows applicability of the induction hypothesis of the following Lemma 1 *)
-goal Correctness.thy "!!l.[| l~=[] |] ==> \
-\ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
- by (Simp_tac 1);
- by (rtac (expand_list_case RS iffD2) 1);
- by (asm_full_simp_tac list_ss 1);
- by (REPEAT (rtac allI 1));
- by (rtac impI 1);
- by (rtac (expand_if RS ssubst) 1);
- by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
- (rev_red_not_nil RS mp)]) 1);
-qed"last_ind_on_first";
-
-val impl_ss = !simpset delsimps [reduce_Cons];
-
-(* Main Lemma 1 for S_pkt in showing that reduce is refinement *)
-goal Correctness.thy
- "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then \
-\ reduce(l@[x])=reduce(l) else \
-\ reduce(l@[x])=reduce(l)@[x]";
-by (rtac (expand_if RS ssubst) 1);
-by (rtac conjI 1);
-(* --> *)
-by (List.list.induct_tac "l" 1);
-by (Simp_tac 1);
-by (case_tac "list=[]" 1);
- by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
- by (rtac impI 1);
-by (Simp_tac 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 1);
- by (asm_full_simp_tac impl_ss 1);
- by (REPEAT (etac exE 1));
- by (hyp_subst_tac 1);
-by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
-(* <-- *)
-by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
-by (List.list.induct_tac "l" 1);
-by (Simp_tac 1);
-by (case_tac "list=[]" 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 2);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (auto_tac (!claset,
- impl_ss addsimps [last_ind_on_first,l_iff_red_nil]
- setloop split_tac [expand_if]));
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-qed"reduce_hd";
-
-
-(* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
-goal Correctness.thy
- "!! s. [| s~=[] |] ==> \
-\ if hd(s)=hd(tl(s)) & tl(s)~=[] then \
-\ reduce(tl(s))=reduce(s) else \
-\ reduce(tl(s))=tl(reduce(s))";
-by (cut_inst_tac [("l","s")] cons_not_nil 1);
-by (Asm_full_simp_tac 1);
-by (REPEAT (etac exE 1));
-by (Asm_full_simp_tac 1);
-by (rtac (expand_if RS ssubst) 1);
-by (rtac conjI 1);
-by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
-by (Step_tac 1);
-by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
-by (Auto_tac());
-val reduce_tl =result();
-
-
-(*******************************************************************
- C h a n n e l A b s t r a c t i o n
- *******************************************************************)
-
-goal Correctness.thy
- "is_weak_pmap reduce ch_ioa ch_fin_ioa";
-by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-(* ---------------- main-part ------------------- *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (act.induct_tac "a" 1);
-(* ----------------- 2 cases ---------------------*)
-by (ALLGOALS (simp_tac (!simpset addsimps [externals_def])));
-(* fst case --------------------------------------*)
- by (rtac impI 1);
- by (rtac disjI2 1);
-by (rtac reduce_hd 1);
-(* snd case --------------------------------------*)
- by (rtac impI 1);
- by (REPEAT (etac conjE 1));
- by (etac disjE 1);
-by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
-by (etac (hd_is_reduce_hd RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
-by (rtac conjI 1);
-by (etac (hd_is_reduce_hd RS mp) 1);
-by (rtac (bool_if_impl_or RS mp) 1);
-by (etac reduce_tl 1);
-qed"channel_abstraction";
-
-goal Correctness.thy
- "is_weak_pmap reduce srch_ioa srch_fin_ioa";
-by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
- srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
-qed"sender_abstraction";
-
-goal Correctness.thy
- "is_weak_pmap reduce rsch_ioa rsch_fin_ioa";
-by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
- srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
-qed"receiver_abstraction";
-
-
-(* 3 thms that do not hold generally! The lucky restriction here is
- the absence of internal actions. *)
-goal Correctness.thy
- "is_weak_pmap (%id.id) sender_ioa sender_ioa";
-by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
-(* main-part *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
-(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
-qed"sender_unchanged";
-
-(* 2 copies of before *)
-goal Correctness.thy
- "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
-by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
- (* start states *)
- (Fast_tac 1)));
-(* main-part *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
-(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
-qed"receiver_unchanged";
-
-goal Correctness.thy
- "is_weak_pmap (%id.id) env_ioa env_ioa";
-by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
-(* main-part *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
-(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
-qed"env_unchanged";
-
-Delsimps [Collect_False_empty];
-
-goal Correctness.thy "compat_ioas srch_ioa rsch_ioa";
-by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS(Simp_tac));
-val compat_single_ch = result();
-
-(* totally the same as before *)
-goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa";
-by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS(Simp_tac));
-val compat_single_fin_ch = result();
-
-val ss =
- !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
- asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
- srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def,
- rsch_ioa_def, Sender.sender_trans_def,
- Receiver.receiver_trans_def] @ set_lemmas);
-
-goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,
- asig_of_par,asig_comp_def,actions_def,
- Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS Simp_tac);
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_rec = result();
-
-(* 5 proofs totally the same as before *)
-goal Correctness.thy "compat_ioas receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS Simp_tac);
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_rec_fin =result();
-
-goal Correctness.thy "compat_ioas sender_ioa \
-\ (receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS(Simp_tac));
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_sen=result();
-
-goal Correctness.thy "compat_ioas sender_ioa\
-\ (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def, compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS(Simp_tac));
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_sen_fin =result();
-
-goal Correctness.thy "compat_ioas env_ioa\
-\ (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS(Simp_tac));
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_env=result();
-
-goal Correctness.thy "compat_ioas env_ioa\
-\ (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
-by (Simp_tac 1);
-by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
-by (ALLGOALS Simp_tac);
-by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
-by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
-val compat_env_fin=result();
-
-
-(* lemmata about externals of channels *)
-goal Correctness.thy
- "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \
-\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
-by (simp_tac (!simpset addsimps [externals_def]) 1);
-val ext_single_ch = result();
-
-
-
-
-
-val ext_ss = [externals_of_par,ext_single_ch];
-val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
- compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
-val abstractions = [env_unchanged,sender_unchanged,
- receiver_unchanged,sender_abstraction,receiver_abstraction];
-
-
-(************************************************************************
- S o u n d n e s s o f A b s t r a c t i o n
-*************************************************************************)
-
-val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
- srch_fin_ioa_def, rsch_fin_ioa_def] @
- impl_ioas @ env_ioas);
-
-goal Correctness.thy
- "is_weak_pmap abs system_ioa system_fin_ioa";
-
-by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
- rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
- addsimps [system_def, system_fin_def, abs_def,
- impl_ioa_def, impl_fin_ioa_def, sys_IOA,
- sys_fin_IOA]) 1);
-
-by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1,
- simp_tac (ss addsimps abstractions) 1,
- rtac conjI 1]));
-
-by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss)));
-
-qed "system_refinement";
--- a/src/HOL/IOA/ABP/Correctness.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(* Title: HOL/IOA/example/Correctness.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The main correctness proof: System_fin implements System
-*)
-
-Correctness = Solve + Env + Impl + Impl_finite +
-
-consts
-
-reduce :: 'a list => 'a list
-
-abs :: 'c
-system_ioa :: "('m action, bool * 'm impl_state)ioa"
-system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
-
-primrec
- reduce List.list
- reduce_Nil "reduce [] = []"
- reduce_Cons "reduce(x#xs) =
- (case xs of
- [] => [x]
- | y#ys => (if (x=y)
- then reduce xs
- else (x#(reduce xs))))"
-
-
-defs
-
-system_def
- "system_ioa == (env_ioa || impl_ioa)"
-
-system_fin_def
- "system_fin_ioa == (env_ioa || impl_fin_ioa)"
-
-abs_def "abs ==
- (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
- (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
-
-rules
-
- sys_IOA "IOA system_ioa"
- sys_fin_IOA "IOA system_fin_ioa"
-
-end
-
-
--- a/src/HOL/IOA/ABP/Env.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(* Title: HOL/IOA/example/Impl.thy
-by (Action.action.induct_tac "a" 1);
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The environment
-*)
-
-Env = IOA + Action +
-
-types
-
-'m env_state = "bool"
-(* give next bit to system *)
-
-consts
-
-env_asig :: 'm action signature
-env_trans :: ('m action, 'm env_state)transition set
-env_ioa :: ('m action, 'm env_state)ioa
-next :: 'm env_state => bool
-
-defs
-
-env_asig_def
- "env_asig == ({Next},
- UN m. {S_msg(m)},
- {})"
-
-env_trans_def "env_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- Next => t=True |
- S_msg(m) => s=True & t=False |
- R_msg(m) => False |
- S_pkt(pkt) => False |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => False}"
-
-env_ioa_def "env_ioa ==
- (env_asig, {True}, env_trans)"
-
-end
-
--- a/src/HOL/IOA/ABP/Impl.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: HOL/IOA/example/Impl.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The implementation
-*)
-
-Impl = Sender + Receiver + Abschannel +
-
-types
-
-'m impl_state
-= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
-(* sender_state * receiver_state * srch_state * rsch_state *)
-
-
-constdefs
-
- impl_ioa :: ('m action, 'm impl_state)ioa
- "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
-
- sen :: 'm impl_state => 'm sender_state
- "sen == fst"
-
- rec :: 'm impl_state => 'm receiver_state
- "rec == fst o snd"
-
- srch :: 'm impl_state => 'm packet list
- "srch == fst o snd o snd"
-
- rsch :: 'm impl_state => bool list
- "rsch == snd o snd o snd"
-
-end
--- a/src/HOL/IOA/ABP/Impl_finite.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: HOL/IOA/example/Impl.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The implementation
-*)
-
-Impl_finite = Sender + Receiver + Abschannel_finite +
-
-types
-
-'m impl_fin_state
-= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
-(* sender_state * receiver_state * srch_state * rsch_state *)
-
-constdefs
-
- impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
- "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
- rsch_fin_ioa)"
-
- sen_fin :: 'm impl_fin_state => 'm sender_state
- "sen_fin == fst"
-
- rec_fin :: 'm impl_fin_state => 'm receiver_state
- "rec_fin == fst o snd"
-
- srch_fin :: 'm impl_fin_state => 'm packet list
- "srch_fin == fst o snd o snd"
-
- rsch_fin :: 'm impl_fin_state => bool list
- "rsch_fin == snd o snd o snd"
-
-end
-
--- a/src/HOL/IOA/ABP/Lemmas.ML Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(* Title: HOL/IOA/example/Lemmas.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-*)
-
-(* Logic *)
-
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
-qed "imp_conj_lemma";
-
-goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
-by (Fast_tac 1);
-val and_de_morgan_and_absorbe = result();
-
-goal HOL.thy "(if C then A else B) --> (A|B)";
-by (rtac (expand_if RS ssubst) 1);
-by (Fast_tac 1);
-val bool_if_impl_or = result();
-
-(* Sets *)
-
-val set_lemmas =
- map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
- ["f(x) : (UN x. {f(x)})",
- "f x y : (UN x y. {f x y})",
- "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
- "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
-
-(* 2 Lemmas to add to set_lemmas ... , used also for action handling,
- namely for Intersections and the empty list (compatibility of IOA!) *)
-goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})";
- by (rtac set_ext 1);
- by (Fast_tac 1);
-val singleton_set =result();
-
-goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
- by (Fast_tac 1);
-val de_morgan = result();
-
-(* Lists *)
-
-val list_ss = simpset_of "List";
-
-goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
-by (List.list.induct_tac "l" 1);
-by (simp_tac list_ss 1);
-by (simp_tac list_ss 1);
-val hd_append =result();
-
-goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
- by (List.list.induct_tac "l" 1);
- by (simp_tac list_ss 1);
- by (Fast_tac 1);
-qed"cons_not_nil";
--- a/src/HOL/IOA/ABP/Lemmas.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Title: HOL/IOA/example/Lemmas.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-Arithmetic lemmas
-*)
-
-Lemmas = Arith
--- a/src/HOL/IOA/ABP/Packet.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: HOL/IOA/example/Packet.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-Packets
-*)
-
-Packet = Arith +
-
-types
-
- 'msg packet = "bool * 'msg"
-
-constdefs
-
- hdr :: 'msg packet => bool
- "hdr == fst"
-
- msg :: 'msg packet => 'msg
- "msg == snd"
-
-end
--- a/src/HOL/IOA/ABP/ROOT.ML Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/IOA/ABP/ROOT.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-This is the ROOT file for the theory of I/O-Automata (ABP subdirectory).
-The formalization is by a semantic model of I/O-Automata.
-For details see
-
-@inproceedings{Nipkow-Slind-IOA,
-author={Tobias Nipkow and Konrad Slind},
-title={{I/O} Automata in {Isabelle/HOL}},
-booktitle={Proc.\ TYPES Workshop 1994},
-publisher=Springer,
-series=LNCS,
-note={To appear}}
-ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
-
-and
-
-@inproceedings{Mueller-Nipkow,
-author={Olaf M\"uller and Tobias Nipkow},
-title={Combining Model Checking and Deduction for {I/O}-Automata},
-booktitle={Proc.\ TACAS Workshop},
-organization={Aarhus University, BRICS report},
-year=1995}
-ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
-
-Should be executed in the subdirectory HOL/IOA/ABP.
-*)
-
-goals_limit := 1;
-
-(*Load theories from ../meta_theory without generating HTML files
- (has already been done by NTP/ROOT.ML)*)
-val old_make_html = !make_html;
-make_html := false;
-loadpath := ["../meta_theory"];
-
-use_thy "Solve";
-
-make_html := old_make_html;
-loadpath := ["."];
-
-
-use_thy "Correctness";
--- a/src/HOL/IOA/ABP/Read_me Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-Isabelle Verification of the Alternating Bit Protocol by
-combining IOA with Model Checking
-
--------------------------------------------------------------
-
-Correctness.ML contains the proof of the abstraction from unbounded
-channels to finite ones.
-
-Check.ML contains a simple ModelChecker prototype checking Spec against
-the finite version of the ABP-protocol.
--- a/src/HOL/IOA/ABP/Receiver.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: HOL/IOA/example/Receiver.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The implementation: receiver
-*)
-
-Receiver = List + IOA + Action + Lemmas +
-
-types
-
-'m receiver_state
-= "'m list * bool"
-(* messages mode *)
-
-consts
-
- receiver_asig :: 'm action signature
- receiver_trans:: ('m action, 'm receiver_state)transition set
- receiver_ioa :: ('m action, 'm receiver_state)ioa
- rq :: 'm receiver_state => 'm list
- rbit :: 'm receiver_state => bool
-
-defs
-
-rq_def "rq == fst"
-rbit_def "rbit == snd"
-
-receiver_asig_def "receiver_asig ==
- (UN pkt. {R_pkt(pkt)},
- (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
- {})"
-
-receiver_trans_def "receiver_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- Next => False |
- S_msg(m) => False |
- R_msg(m) => (rq(s) ~= []) &
- m = hd(rq(s)) &
- rq(t) = tl(rq(s)) &
- rbit(t)=rbit(s) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
- rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
- rq(t) =rq(s) & rbit(t)=rbit(s) |
- S_ack(b) => b = rbit(s) &
- rq(t) = rq(s) &
- rbit(t)=rbit(s) |
- R_ack(b) => False}"
-
-receiver_ioa_def "receiver_ioa ==
- (receiver_asig, {([],False)}, receiver_trans)"
-
-end
--- a/src/HOL/IOA/ABP/Sender.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(* Title: HOL/IOA/example/Sender.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The implementation: sender
-*)
-
-Sender = IOA + Action + List + Lemmas +
-
-types
-
-'m sender_state = "'m list * bool"
-(* messages Alternating Bit *)
-
-consts
-
-sender_asig :: 'm action signature
-sender_trans :: ('m action, 'm sender_state)transition set
-sender_ioa :: ('m action, 'm sender_state)ioa
-sq :: 'm sender_state => 'm list
-sbit :: 'm sender_state => bool
-
-defs
-
-sq_def "sq == fst"
-sbit_def "sbit == snd"
-
-sender_asig_def
- "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
- UN pkt. {S_pkt(pkt)},
- {})"
-
-sender_trans_def "sender_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- Next => if sq(s)=[] then t=s else False |
- S_msg(m) => sq(t)=sq(s)@[m] &
- sbit(t)=sbit(s) |
- R_msg(m) => False |
- S_pkt(pkt) => sq(s) ~= [] &
- hdr(pkt) = sbit(s) &
- msg(pkt) = hd(sq(s)) &
- sq(t) = sq(s) &
- sbit(t) = sbit(s) |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => if b = sbit(s) then
- sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
- sq(t)=sq(s) & sbit(t)=sbit(s)}"
-
-sender_ioa_def "sender_ioa ==
- (sender_asig, {([],True)}, sender_trans)"
-
-end
--- a/src/HOL/IOA/ABP/Spec.thy Wed Apr 30 11:42:37 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: HOL/IOA/example/Spec.thy
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The specification of reliable transmission
-*)
-
-Spec = List + IOA + Action +
-
-consts
-
-spec_sig :: 'm action signature
-spec_trans :: ('m action, 'm list)transition set
-spec_ioa :: ('m action, 'm list)ioa
-
-defs
-
-sig_def "spec_sig == (UN m.{S_msg(m)},
- UN m.{R_msg(m)} Un {Next},
- {})"
-
-trans_def "spec_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- Next => t=s |\ (* Note that there is condition as in Sender *)
- S_msg(m) => t = s@[m] |
- R_msg(m) => s = (m#t) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => False}"
-
-ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
-
-end