# HG changeset patch # User mueller # Date 862392254 -7200 # Node ID a31419014be588494662008f27cd8b1fde7949c1 # Parent 981258186b712c0a3b8e40d5e32322e5899401bd Old ABP files now running under the IOA meta theory based on HOLCF; diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Abschannel.thy --- /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 + + + + + + + + + + + + + + + + + + diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Abschannel_finite.thy --- /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 + + + + + + + + + + + + + + + + + + diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Action.ML --- /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()]; diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Action.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Check.ML --- /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]; + +*) diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Correctness.ML --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Correctness.thy --- /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 + + diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Env.thy --- /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 + diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Impl.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Impl_finite.thy --- /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 + diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Lemmas.ML --- /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"; diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Lemmas.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Packet.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/ROOT.ML --- /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"; diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Read_me --- /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. diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Receiver.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Sender.thy --- /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 diff -r 981258186b71 -r a31419014be5 src/HOLCF/IOA/ABP/Spec.thy --- /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