--- /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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /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;
--- /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
--- /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,[])]);
+
+
--- /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";
+
--- /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
--- /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
+
--- /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
--- /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
+
--- /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
--- /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
--- /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
--- /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.
--- /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
--- /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
--- /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