--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Abschannel.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,107 @@
+(* Title: HOLCF/IOA/ABP/Abschannel.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+The transmission channel
+*)
+
+Abschannel = IOA + Action + Lemmas + List +
+
+
+datatype ('a)abs_action = S('a) | R('a)
+
+
+consts
+
+ch_asig :: 'a abs_action signature
+ch_trans :: ('a abs_action, 'a list)transition set
+ch_ioa :: ('a abs_action, 'a list)ioa
+
+rsch_actions :: 'm action => bool abs_action option
+srch_actions :: "'m action =>(bool * 'm) abs_action 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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,80 @@
+(* Title: HOLCF/IOA/ABP/Abschannels.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+The transmission channel -- finite version
+*)
+
+Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
+
+consts
+
+ch_fin_asig :: 'a abs_action signature
+
+ch_fin_trans :: ('a abs_action, 'a list)transition set
+
+ch_fin_ioa :: ('a abs_action, '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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Action.ML Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,13 @@
+(* Title: HOLCF/IOA/ABP/Action.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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()];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Action.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,13 @@
+(* Title: HOLCF/IOA/ABP/Action.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Check.ML Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,176 @@
+(* Title: HOLCF/IOA/ABP/Check.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1994 TU Muenchen
+
+The Model Checker
+*)
+
+
+(* ----------------------------------------------------------------
+ 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];
+
+*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,384 @@
+ (* Title: HOLCF/IOA/ABP/Correctness.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+*)
+
+
+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_ref_map reduce ch_ioa ch_fin_ioa";
+by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+(* ---------------- main-part ------------------- *)
+by (REPEAT (rtac allI 1));
+by (rtac imp_conj_lemma 1);
+by (abs_action.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_ref_map 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_ref_map 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_ref_map (%id.id) sender_ioa sender_ioa";
+by (simp_tac (!simpset addsimps [is_weak_ref_map_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_ref_map (%id.id) receiver_ioa receiver_ioa";
+by (simp_tac (!simpset addsimps [is_weak_ref_map_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_ref_map (%id.id) env_ioa env_ioa";
+by (simp_tac (!simpset addsimps [is_weak_ref_map_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);
+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);
+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));
+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));
+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));
+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);
+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);
+
+(* FIX: this proof should be done with compositionality on trace level, not on
+ weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA
+
+goal Correctness.thy
+ "is_weak_ref_map 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_ref_map_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";
+
+
+*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,49 @@
+(* Title: HOLCF/IOA/ABP/Correctness.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+The main correctness proof: System_fin implements System
+*)
+
+Correctness = IOA + 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
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Env.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,47 @@
+(* Title: HOLCF/IOA/ABP/Impl.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Impl.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,35 @@
+(* Title: HOLCF/IOA/ABP/Impl.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,36 @@
+(* Title: HOLCF/IOA/ABP/Impl.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,57 @@
+(* Title: HOLCF/IOA/ABP/Lemmas.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,9 @@
+(* Title: HOLCF/IOA/ABP/Lemmas.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+Arithmetic lemmas
+*)
+
+Lemmas = Arith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Packet.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,23 @@
+(* Title: HOLCF/IOA/ABP/Packet.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+Packets
+*)
+
+Packet = Arith +
+
+types
+
+ 'msg packet = "bool * 'msg"
+
+constdefs
+
+ hdr :: 'msg packet => bool
+ "hdr == fst"
+
+ msg :: 'msg packet => 'msg
+ "msg == snd"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,17 @@
+(* Title: HOL/IOA/ABP/ROOT.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 TU Muenchen
+
+This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata.
+
+For details see the README.html file.
+
+Should be executed in the subdirectory HOLCF/IOA/examples/ABP.
+*)
+
+goals_limit := 1;
+
+loadpath:=["."];
+
+use_thy "Correctness";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Read_me Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,10 @@
+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.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Receiver.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,59 @@
+(* Title: HOLCF/IOA/ABP/Receiver.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Sender.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,57 @@
+(* Title: HOLCF/IOA/ABP/Sender.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ABP/Spec.thy Wed Apr 30 11:24:14 1997 +0200
@@ -0,0 +1,39 @@
+(* Title: HOLCF/IOA/ABP/Spec.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1995 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