# HG changeset patch # User nipkow # Date 797784914 -7200 # Node ID 0c36c6a52a1d7801959e12998b50c7d93740a858 # Parent 92de80b43d28cd487fe794e70f0c82b3d1290032 ABP: Alternating bit protocol example diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Abschannel.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Abschannel.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,99 @@ +(* Title: HOL/IOA/ABP/Abschannels.thy + ID: $Id$ + Author: Olaf Mueller + Copyright 1995 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" + + +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)" + +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 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Abschannel_finite.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Abschannel_finite.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,80 @@ +(* Title: HOL/IOA/ABP/Abschannel_finite.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 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 + + + + + + + + + + + + + + + + + + diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Action.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Action.ML Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/IOA/ABP/Action.ML + ID: $Id$ + Author: Tobias Nipkow & 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 HOL_ss 1); + +val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps; diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Action.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Action.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/IOA/ABP/Action.thy + ID: $Id$ + Author: Tobias Nipkow & 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 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Check.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Check.ML Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,140 @@ +(* Title: HOL/IOA/ABP/Check.ML + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +Simple ModelChecker prototype checking Spec against +the finite version of the ABP-protocol. +*) + + +(* model checker function prototype *) + +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; + + +(* datatypes for ABP example *) + +datatype msg = m; +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; + +fun transA((u,s),a,(v,t)) = + (case a of + Next => v andalso t = s | + S_msg(m) => u andalso not(v) andalso t = s@[m] | + R_msg(m) => u = v andalso s = (m::t) | + S_pkt(b,m) => false | + R_pkt(b,m) => false | + S_ack(b) => false | + R_ack(b) => false); + +fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p)); + +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(m) => if env then [(false,p@[m],a,q,b,ch1,ch2)] else [] | + R_msg(m) => if (q<>[] andalso m=hd(q)) + then [(env,p,a,tl(q),b,ch1,ch2)] + else [] | + S_pkt(h,m) => if (p<>[] andalso m=hd(p) andalso h=a) + then (if (ch1<>[] andalso hd(rev(ch1))=(h,m)) + then [s] + else [s,(env,p,a,q,b,ch1@[(h,m)],ch2)]) + else [] | + R_pkt(h,m) => if (ch1<>[] andalso hd(ch1)=(h,m)) + then (if (h<>b andalso q=[]) + then [(env,p,a,q@[m],not(b),ch1,ch2), + (env,p,a,q@[m],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)]; +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)]; + + +(* Input / Output auxiliary functions *) + +fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) = + let fun prec x = (prs ","; pre x) + in + (case l of + [] => (prs lpar; prs rpar) + | x::l => (prs lpar; pre x; seq prec l; 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"); + +fun pr_act a = output(std_out, case a of + Next => "Next"| + S_msg(m) => "S_msg(m)" | + R_msg(m) => "R_msg(m)" | + S_pkt(b,m) => "S_pkt(b,m)" | + R_pkt(b,m) => "R_pkt(b,m)" | + S_ack(b) => "S_ack(b)" | + R_ack(b) => "R_ack(b)"); + +fun pr_pkt (b,m) = (prs "<"; pr_bool b;prs ", "; pr_msg m; 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 check function call *) +(* ----------------------------*) + +check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], + pr_tuple, nexts, hom, transA, [(true,[])]); + + diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Correctness.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Correctness.ML Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,371 @@ + (* Title: HOL/IOA/ABP/Correctness.ML + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +*) + +open Correctness; open Abschannel; open Abschannel_finite; + +goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)"; +by (fast_tac HOL_cs 1); +qed"exis_elim"; + +val abschannel_ss = action_ss 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] + @ Option.option.simps @ act.simps @ 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]; +val abschannel_fin_ss = abschannel_ss 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]; +val impl_ss = merge_ss(action_ss,list_ss) + 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; +val hom_ss = (impl_ss addsimps hom_ioas); + +val red_ss = impl_ss addsimps [reduce_Nil,reduce_Cons]; +val red_ss_ch = merge_ss(abschannel_fin_ss,red_ss); + + +(* 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 HOL_cs 1); + by (List.list.induct_tac "l" 1); + by (simp_tac red_ss 1); + by (simp_tac red_ss 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 (hyp_subst_tac 1); + by (rtac (expand_if RS ssubst) 1); + by (asm_full_simp_tac list_ss 1); + by (asm_full_simp_tac red_ss 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 red_ss 1); +by (case_tac "list =[]" 1); +by (asm_full_simp_tac red_ss 1); +(* main case *) +by (rotate 1 1); +by (asm_full_simp_tac list_ss 1); +by (simp_tac red_ss 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 list_ss 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 red_ss 1); +by (case_tac "list =[]" 1); +by (asm_full_simp_tac (red_ss addsimps [reverse_Cons]) 1); +(* main case *) +by (rotate 1 1); +by (asm_full_simp_tac red_ss 1); +by (cut_inst_tac [("l","list")] cons_not_nil 1); +by (asm_full_simp_tac list_ss 1); +by (REPEAT (etac exE 1)); +by (asm_simp_tac list_ss 1); +by (rtac (expand_if RS ssubst) 1); +by (hyp_subst_tac 1); +by (asm_full_simp_tac (list_ss 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 red_ss 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"; + + +(* 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 red_ss 1); +by (case_tac "list=[]" 1); + by (asm_full_simp_tac (red_ss addsimps [reverse_Nil,reverse_Cons]) 1); + by (rtac impI 1); +by (simp_tac red_ss 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 (red_ss addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1); +by (List.list.induct_tac "l" 1); +by (simp_tac red_ss 1); +by (case_tac "list=[]" 1); + by (asm_full_simp_tac (red_ss addsimps [reverse_Nil,reverse_Cons]) 1); +by (rtac (expand_if RS ssubst) 1); + by (fast_tac HOL_cs 1); + by (rtac impI 1); +by (simp_tac red_ss 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 (rtac (expand_if RS ssubst) 1); +by (rtac (expand_if RS ssubst) 1); +by (asm_full_simp_tac impl_ss 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 red_ss 1); +by (REPEAT (etac exE 1)); +by (asm_full_simp_tac red_ss 1); +by (rtac (expand_if RS ssubst) 1); +by (rtac conjI 1); +by (simp_tac (red_ss addsimps [and_de_morgan_and_absorbe]) 2); +by (ALLGOALS (EVERY'[rtac impI,etac conjE,cut_inst_tac [("l","xs")] cons_not_nil,asm_full_simp_tac red_ss])); +by (REPEAT (etac exE 1)); +by (REPEAT (etac exE 2)); +by (hyp_subst_tac 2); +by (ALLGOALS (asm_full_simp_tac red_ss)); +val reduce_tl =result(); + + + +goal Correctness.thy + "is_weak_pmap reduce ch_ioa ch_fin_ioa"; +by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (rtac conjI 1); +(* start states *) +by (simp_tac red_ss_ch 1); +br ballI 1; +by (asm_full_simp_tac red_ss_ch 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 (red_ss_ch 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 (red_ss addsimps [l_iff_red_nil]) 1); +by (etac (hd_is_reduce_hd RS mp) 1); +by (asm_full_simp_tac (red_ss 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 (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (rtac conjI 1); +(* start states *) +br ballI 1; +by (simp_tac red_ss_ch 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 ((hom_ss 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 (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (rtac conjI 1); +(* start states *) +br ballI 1; +by (simp_tac red_ss_ch 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 ((hom_ss 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 (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (rtac conjI 1); +(* start states *) +br ballI 1; +by (simp_tac red_ss_ch 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 ((hom_ss addsimps [externals_def]) setloop (split_tac [expand_if])))); +qed"env_unchanged"; + + +goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; +by (simp_tac (red_ss_ch 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 red_ss_ch)); +val compat_single_ch = result(); + +(* totally the same as before *) +goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa"; +by (simp_tac (red_ss_ch 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 red_ss_ch)); +val compat_single_fin_ch = result(); + +goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)"; +by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (hom_ss addsimps [empty_def, compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (simp_tac red_ss_ch 1); +by (rtac set_ext 1); +by (Action.action.induct_tac "x" 1); +by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (red_ss_ch 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 (red_ss_ch addsimps [externals_def]) 1); +val ext_single_ch = result(); + +goal Correctness.thy "is_weak_pmap \ +\ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), \ +\ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p)))))))))) \ +\ (env_ioa || impl_ioa) (env_ioa || impl_fin_ioa)"; +by (simp_tac (impl_ss addsimps [Impl.impl_def,Impl_finite.impl_fin_def]) 1); +by(REPEAT(EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, + simp_tac (red_ss addsimps [env_unchanged,sender_unchanged, + receiver_unchanged,sender_abstraction,receiver_abstraction]) 1, + rtac conjI 1])); +by (ALLGOALS(simp_tac (list_ss addsimps [externals_of_par,ext_single_ch, + compat_single_ch,compat_single_fin_ch,compat_rec,compat_rec_fin, + compat_sen,compat_sen_fin,compat_env,compat_env_fin]))); +qed "system_refinement"; + diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Correctness.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Correctness.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,28 @@ +(* Title: HOL/IOA/ABP/Correctness.thy + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1994 TU Muenchen + +The main correctness proof: System_fin implements System +*) + +Correctness = Solve + Env + Impl + Impl_finite + + +consts + +reduce :: "'a list => 'a list" + +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))))" + +end + + + \ No newline at end of file diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Env.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Env.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,47 @@ +(* Title: HOL/IOA/ABP/Impl.thy + 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 + diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Impl.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Impl.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,35 @@ +(* Title: HOL/IOA/ABP/Impl.thy + ID: $Id$ + Author: Tobias Nipkow & 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 *) + + +consts + impl_ioa :: "('m action, 'm impl_state)ioa" + sen :: "'m impl_state => 'm sender_state" + rec :: "'m impl_state => 'm receiver_state" + srch :: "'m impl_state => 'm packet list" + rsch :: "'m impl_state => bool list" + +defs + + impl_def + "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" + + sen_def "sen == fst" + rec_def "rec == fst o snd" + srch_def "srch == fst o snd o snd" + rsch_def "rsch == snd o snd o snd" + +end diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Impl_finite.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Impl_finite.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,35 @@ +(* Title: HOL/IOA/ABP/Impl_finite.thy + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +The finite 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 *) + +consts + + impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" + sen_fin :: "'m impl_fin_state => 'm sender_state" + rec_fin :: "'m impl_fin_state => 'm receiver_state" + srch_fin :: "'m impl_fin_state => 'm packet list" + rsch_fin :: "'m impl_fin_state => bool list" + +defs + + impl_fin_def + "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)" + sen_fin_def "sen_fin == fst" + rec_fin_def "rec_fin == fst o snd" + srch_fin_def "srch_fin == fst o snd o snd" + rsch_fin_def "rsch_fin == snd o snd o snd" + +end + diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Lemmas.ML Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,55 @@ +(* Title: HOL/IOA/ABP/Lemmas.ML + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +*) + +(* Logic *) + +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; + by(fast_tac (HOL_cs addDs prems) 1); +qed "imp_conj_lemma"; + +goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)"; +by (fast_tac HOL_cs 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 HOL_cs 1); +val bool_if_impl_or = result(); + +(* Sets *) + +val set_lemmas = + map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 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 set_cs 1); +val singleton_set =result(); + +goal HOL.thy "((A|B)=False) = ((~A)&(~B))"; + by (fast_tac HOL_cs 1); +val de_morgan = result(); + +(* Lists *) + +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 HOL_cs 1); +qed"cons_not_nil"; \ No newline at end of file diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Lemmas.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,9 @@ +(* Title: HOL/IOA/ABP/Lemmas.thy + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +Arithmetic lemmas +*) + +Lemmas = Arith diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Packet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Packet.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,25 @@ +(* Title: HOL/IOA/ABP/Packet.thy + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +Packets +*) + +Packet = Arith + + +types + + 'msg packet = "bool * 'msg" + +consts + + hdr :: "'msg packet => bool" + msg :: "'msg packet => 'msg" + +defs + + hdr_def "hdr == fst" + msg_def "msg == snd" + +end diff -r 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Read_me --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Read_me Thu Apr 13 16:55:14 1995 +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 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Receiver.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Receiver.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,59 @@ +(* Title: HOL/IOA/ABP/Receiver.thy + ID: $Id$ + Author: Tobias Nipkow & 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 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Sender.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Sender.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,57 @@ +(* Title: HOL/IOA/ABP/Sender.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + 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 92de80b43d28 -r 0c36c6a52a1d src/HOL/IOA/ABP/Spec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Spec.thy Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,39 @@ +(* Title: HOL/IOA/ABP/Spec.thy + ID: $Id$ + Author: Tobias Nipkow & 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