Old ABP files now running under the IOA meta theory based on HOLCF;
authormueller
Wed Apr 30 11:24:14 1997 +0200 (1997-04-30)
changeset 3072a31419014be5
parent 3071 981258186b71
child 3073 88366253a09a
Old ABP files now running under the IOA meta theory based on HOLCF;
src/HOLCF/IOA/ABP/Abschannel.thy
src/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOLCF/IOA/ABP/Action.ML
src/HOLCF/IOA/ABP/Action.thy
src/HOLCF/IOA/ABP/Check.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/IOA/ABP/Env.thy
src/HOLCF/IOA/ABP/Impl.thy
src/HOLCF/IOA/ABP/Impl_finite.thy
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/ABP/Lemmas.thy
src/HOLCF/IOA/ABP/Packet.thy
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/ABP/Read_me
src/HOLCF/IOA/ABP/Receiver.thy
src/HOLCF/IOA/ABP/Sender.thy
src/HOLCF/IOA/ABP/Spec.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy	Wed Apr 30 11:24:14 1997 +0200
     1.3 @@ -0,0 +1,107 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1995  TU Muenchen
     1.8 +
     1.9 +The transmission channel 
    1.10 +*)
    1.11 +
    1.12 +Abschannel = IOA + Action + Lemmas + List +
    1.13 +
    1.14 +
    1.15 +datatype ('a)abs_action =   S('a) | R('a)
    1.16 +
    1.17 +
    1.18 +consts
    1.19 + 
    1.20 +ch_asig  :: 'a abs_action signature
    1.21 +ch_trans :: ('a abs_action, 'a list)transition set
    1.22 +ch_ioa   :: ('a abs_action, 'a list)ioa
    1.23 +
    1.24 +rsch_actions  :: 'm action => bool abs_action option
    1.25 +srch_actions  :: "'m action =>(bool * 'm) abs_action option"
    1.26 +
    1.27 +srch_asig, 
    1.28 +rsch_asig  :: 'm action signature
    1.29 + 
    1.30 +srch_trans :: ('m action, 'm packet list)transition set
    1.31 +rsch_trans :: ('m action, bool list)transition set
    1.32 +
    1.33 +srch_ioa   :: ('m action, 'm packet list)ioa
    1.34 +rsch_ioa   :: ('m action, bool list)ioa   
    1.35 +
    1.36 +
    1.37 +defs
    1.38 +
    1.39 +srch_asig_def "srch_asig == asig_of(srch_ioa)"
    1.40 +rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
    1.41 +
    1.42 +srch_trans_def "srch_trans == trans_of(srch_ioa)"  
    1.43 +rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
    1.44 +
    1.45 +srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
    1.46 +rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
    1.47 +
    1.48 +  
    1.49 +(**********************************************************
    1.50 +       G e n e r i c   C h a n n e l
    1.51 + *********************************************************)
    1.52 +  
    1.53 +ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
    1.54 +
    1.55 +ch_trans_def "ch_trans ==                                       
    1.56 + {tr. let s = fst(tr);                                         
    1.57 +          t = snd(snd(tr))                                     
    1.58 +      in                                                       
    1.59 +      case fst(snd(tr))                                        
    1.60 +        of S(b) => ((t = s) | (t = s @ [b]))  |                
    1.61 +           R(b) => s ~= [] &                                   
    1.62 +                    b = hd(s) &                                 
    1.63 +                    ((t = s) | (t = tl(s)))    }"
    1.64 +  
    1.65 +ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
    1.66 +
    1.67 +(**********************************************************
    1.68 +  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 
    1.69 + *********************************************************)
    1.70 +  
    1.71 +rsch_actions_def "rsch_actions (akt) ==                      
    1.72 +            case akt of   
    1.73 +           Next    =>  None |          
    1.74 +           S_msg(m) => None |         
    1.75 +            R_msg(m) => None |         
    1.76 +           S_pkt(packet) => None |    
    1.77 +            R_pkt(packet) => None |    
    1.78 +            S_ack(b) => Some(S(b)) |   
    1.79 +            R_ack(b) => Some(R(b))"
    1.80 +
    1.81 +srch_actions_def "srch_actions (akt) ==                      
    1.82 +            case akt of   
    1.83 +            Next    =>  None |          
    1.84 +           S_msg(m) => None |         
    1.85 +            R_msg(m) => None |         
    1.86 +           S_pkt(p) => Some(S(p)) |   
    1.87 +            R_pkt(p) => Some(R(p)) |   
    1.88 +            S_ack(b) => None |         
    1.89 +            R_ack(b) => None"
    1.90 +
    1.91 +
    1.92 +end  
    1.93 +
    1.94 +
    1.95 +
    1.96 +
    1.97 +
    1.98 +
    1.99 +
   1.100 +
   1.101 +
   1.102 +
   1.103 +
   1.104 +
   1.105 +
   1.106 +
   1.107 +
   1.108 +
   1.109 +
   1.110 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Wed Apr 30 11:24:14 1997 +0200
     2.3 @@ -0,0 +1,80 @@
     2.4 +(*  Title:      HOLCF/IOA/ABP/Abschannels.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller
     2.7 +    Copyright   1995  TU Muenchen
     2.8 +
     2.9 +The transmission channel -- finite version
    2.10 +*)
    2.11 +
    2.12 +Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
    2.13 + 
    2.14 +consts
    2.15 + 
    2.16 +ch_fin_asig  :: 'a abs_action signature
    2.17 +
    2.18 +ch_fin_trans :: ('a abs_action, 'a list)transition set
    2.19 +
    2.20 +ch_fin_ioa   :: ('a abs_action, 'a list)ioa
    2.21 +
    2.22 +srch_fin_asig, 
    2.23 +rsch_fin_asig  :: 'm action signature
    2.24 +
    2.25 +srch_fin_trans :: ('m action, 'm packet list)transition set
    2.26 +rsch_fin_trans :: ('m action, bool list)transition set
    2.27 +
    2.28 +srch_fin_ioa   :: ('m action, 'm packet list)ioa
    2.29 +rsch_fin_ioa   :: ('m action, bool list)ioa   
    2.30 +
    2.31 +reverse        :: 'a list => 'a list
    2.32 +
    2.33 +primrec
    2.34 +  reverse List.list  
    2.35 +  reverse_Nil  "reverse([]) = []"
    2.36 +  reverse_Cons "reverse(x#xs) =  reverse(xs)@[x]"
    2.37 +
    2.38 +defs
    2.39 +
    2.40 +srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)"
    2.41 +rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)"
    2.42 +
    2.43 +srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)"  
    2.44 +rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)"
    2.45 +
    2.46 +srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa  srch_actions"
    2.47 +rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa  rsch_actions"
    2.48 +
    2.49 +
    2.50 +ch_fin_asig_def "ch_fin_asig == ch_asig"
    2.51 +
    2.52 +ch_fin_trans_def "ch_fin_trans ==                                       
    2.53 + {tr. let s = fst(tr);                                         
    2.54 +          t = snd(snd(tr))                                     
    2.55 +      in                                                       
    2.56 +      case fst(snd(tr))                                        
    2.57 +        of S(b) => ((t = s) |                                    
    2.58 +                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
    2.59 +           R(b) => s ~= [] &                                   
    2.60 +                    b = hd(s) &                                 
    2.61 +                    ((t = s) | (t = tl(s)))    }"
    2.62 +  
    2.63 +ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
    2.64 +
    2.65 +end  
    2.66 +
    2.67 +
    2.68 +
    2.69 +
    2.70 +
    2.71 +
    2.72 +
    2.73 +
    2.74 +
    2.75 +
    2.76 +
    2.77 +
    2.78 +
    2.79 +
    2.80 +
    2.81 +
    2.82 +
    2.83 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/IOA/ABP/Action.ML	Wed Apr 30 11:24:14 1997 +0200
     3.3 @@ -0,0 +1,13 @@
     3.4 +(*  Title:      HOLCF/IOA/ABP/Action.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Olaf Mueller
     3.7 +    Copyright   1995  TU Muenchen
     3.8 +
     3.9 +Derived rules for actions
    3.10 +*)
    3.11 +
    3.12 +goal Action.thy "!!x. x = y ==> action_case a b c d e f g x =     \
    3.13 +\                               action_case a b c d e f g y";
    3.14 +by (Asm_simp_tac 1);
    3.15 +
    3.16 +Addcongs [result()];
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/IOA/ABP/Action.thy	Wed Apr 30 11:24:14 1997 +0200
     4.3 @@ -0,0 +1,13 @@
     4.4 +(*  Title:      HOLCF/IOA/ABP/Action.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf Mueller
     4.7 +    Copyright   1995  TU Muenchen
     4.8 +
     4.9 +The set of all actions of the system
    4.10 +*)
    4.11 +
    4.12 +Action = Packet +
    4.13 +datatype 'm action = Next | S_msg ('m) | R_msg ('m)
    4.14 +                   | S_pkt ('m packet) | R_pkt ('m packet) 
    4.15 +                   | S_ack (bool) | R_ack (bool)         
    4.16 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed Apr 30 11:24:14 1997 +0200
     5.3 @@ -0,0 +1,176 @@
     5.4 +(*  Title:      HOLCF/IOA/ABP/Check.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Olaf Mueller
     5.7 +    Copyright   1994  TU Muenchen
     5.8 +
     5.9 +The Model Checker
    5.10 +*)
    5.11 +
    5.12 + 
    5.13 +(* ----------------------------------------------------------------
    5.14 +       P r o t o t y p e   M o d e l   C h e c k e r 
    5.15 +   ----------------------------------------------------------------*)
    5.16 +
    5.17 +fun check(extacts,intacts,string_of_a,startsI,string_of_s,
    5.18 +          nexts,hom,transA,startsS) =
    5.19 +  let fun check_s(s,unchecked,checked) =
    5.20 +        let fun check_sa(unchecked,a) =
    5.21 +              let fun check_sas(unchecked,t) =
    5.22 +                    (if a mem extacts then
    5.23 +                          (if transA(hom s,a,hom t) then ( )
    5.24 +                           else (writeln("Error: Mapping of Externals!");
    5.25 +                                 string_of_s s; writeln"";
    5.26 +                                 string_of_a a; writeln"";
    5.27 +                                 string_of_s t;writeln"";writeln"" ))
    5.28 +                     else (if hom(s)=hom(t) then ( )
    5.29 +                           else (writeln("Error: Mapping of Internals!");
    5.30 +                                 string_of_s s; writeln"";
    5.31 +                                 string_of_a a; writeln"";
    5.32 +                                 string_of_s t;writeln"";writeln"" ));
    5.33 +                     if t mem checked then unchecked else t ins unchecked)
    5.34 +              in foldl check_sas (unchecked,nexts s a) end;
    5.35 +              val unchecked' = foldl check_sa (unchecked,extacts @ intacts)
    5.36 +        in    (if s mem startsI then 
    5.37 +                    (if hom(s) mem startsS then ()
    5.38 +                     else writeln("Error: At start states!"))
    5.39 +               else ();  
    5.40 +               checks(unchecked',s::checked)) end
    5.41 +      and checks([],_) = ()
    5.42 +        | checks(s::unchecked,checked) = check_s(s,unchecked,checked)
    5.43 +  in checks(startsI,[]) end;
    5.44 +
    5.45 +
    5.46 +(* ------------------------------------------------------
    5.47 +                 A B P     E x a m p l e
    5.48 +   -------------------------------------------------------*)
    5.49 +
    5.50 +datatype msg = m | n | l;
    5.51 +datatype act = Next | S_msg of msg | R_msg of msg
    5.52 +                    | S_pkt of bool * msg | R_pkt of bool * msg
    5.53 +                    | S_ack of bool | R_ack of bool;
    5.54 +
    5.55 +(* -------------------- Transition relation of Specification -----------*)
    5.56 +
    5.57 +fun transA((u,s),a,(v,t)) = 
    5.58 +    (case a of 
    5.59 +       Next       => v andalso t = s |                         
    5.60 +       S_msg(q)   => u andalso not(v) andalso t = s@[q]   |    
    5.61 +       R_msg(q)   => u = v andalso s = (q::t)  |                    
    5.62 +       S_pkt(b,q) => false |                    
    5.63 +       R_pkt(b,q) => false |                    
    5.64 +       S_ack(b)   => false |                      
    5.65 +       R_ack(b)   => false);
    5.66 +
    5.67 +
    5.68 +(* ---------------------- Abstraction function --------------------------*)
    5.69 +
    5.70 +fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
    5.71 +
    5.72 +
    5.73 +(* --------------------- Transition relation of Implementation ----------*)
    5.74 +
    5.75 +fun nexts (s as (env,p,a,q,b,ch1,ch2)) action =
    5.76 +    (case action of
    5.77 +       Next       => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] |                         
    5.78 +       S_msg(mornorl)   => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] |     
    5.79 +       R_msg(mornorl)   => if (q<>[] andalso mornorl=hd(q)) 
    5.80 +                        then [(env,p,a,tl(q),b,ch1,ch2)]
    5.81 +                        else [] |                    
    5.82 +       S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a)
    5.83 +                        then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl))
    5.84 +                              then [s]
    5.85 +                              else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)])
    5.86 +                        else [] |
    5.87 +       R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl))
    5.88 +                         then (if (h<>b andalso q=[])
    5.89 +                               then [(env,p,a,q@[mornorl],not(b),ch1,ch2),
    5.90 +                                     (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)]
    5.91 +                               else [s,(env,p,a,q,b,tl(ch1),ch2)])
    5.92 +                          else [] | 
    5.93 +       S_ack(h)   => if (h=b)
    5.94 +                        then (if (ch2<>[] andalso h=hd(rev(ch2))) 
    5.95 +                              then [s]
    5.96 +                              else [s,(env,p,a,q,b,ch1,ch2@[h])])
    5.97 +                        else []  |                      
    5.98 +       R_ack(h)   => if (ch2<>[] andalso hd(ch2)=h)
    5.99 +                        then (if h=a
   5.100 +                              then [(env,tl(p),not(a),q,b,ch1,ch2),
   5.101 +                                    (env,tl(p),not(a),q,b,ch1,tl(ch2))]
   5.102 +                              else [s,(env,p,a,q,b,ch1,tl(ch2))]) 
   5.103 +                         else [])
   5.104 +
   5.105 +
   5.106 +val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
   5.107 +val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true),
   5.108 +                  S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false),
   5.109 +                  S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l),
   5.110 +               S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)];
   5.111 +
   5.112 +
   5.113 +(* ------------------------------------
   5.114 +           Input / Output utilities 
   5.115 +   ------------------------------------*)
   5.116 +
   5.117 +fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   5.118 +  let fun prec x = (prs ","; pre x)
   5.119 +  in
   5.120 +    (case lll of
   5.121 +      [] => (prs lpar; prs rpar)
   5.122 +    | x::lll => (prs lpar; pre x; seq prec lll; prs rpar))
   5.123 +   end;
   5.124 +
   5.125 +fun pr_bool true = output(std_out,"true")
   5.126 +|   pr_bool false = output(std_out,"false");
   5.127 +
   5.128 +fun pr_msg m = output(std_out,"m")
   5.129 +|   pr_msg n = output(std_out,"n")
   5.130 +|   pr_msg l = output(std_out,"l");
   5.131 +
   5.132 +fun pr_act a = output(std_out, case a of
   5.133 +      Next => "Next"|                         
   5.134 +      S_msg(ma) => "S_msg(ma)"  |
   5.135 +      R_msg(ma) => "R_msg(ma)"  |
   5.136 +      S_pkt(b,ma) => "S_pkt(b,ma)" |                    
   5.137 +      R_pkt(b,ma) => "R_pkt(b,ma)" |                    
   5.138 +      S_ack(b)   => "S_ack(b)" |                      
   5.139 +      R_ack(b)   => "R_ack(b)");
   5.140 +
   5.141 +fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">");
   5.142 +
   5.143 +val pr_bool_list  = print_list("[","]",pr_bool);
   5.144 +val pr_msg_list   = print_list("[","]",pr_msg);
   5.145 +val pr_pkt_list   = print_list("[","]",pr_pkt);
   5.146 +
   5.147 +fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
   5.148 +        (prs "{"; pr_bool env; prs ", "; pr_msg_list p;  prs ", ";
   5.149 +         pr_bool a;  prs ", "; pr_msg_list q; prs ", ";
   5.150 +         pr_bool b;  prs ", "; pr_pkt_list ch1;  prs ", ";
   5.151 +         pr_bool_list ch2; prs "}");
   5.152 +
   5.153 +
   5.154 +
   5.155 +(* ---------------------------------
   5.156 +         Main function call
   5.157 +   ---------------------------------*)
   5.158 +
   5.159 +(*
   5.160 +check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], 
   5.161 +      pr_tuple, nexts, hom, transA, [(true,[])]);
   5.162 +*)
   5.163 +
   5.164 +
   5.165 +
   5.166 +
   5.167 +
   5.168 +(*
   5.169 +           Little test example
   5.170 +
   5.171 +datatype act = A;
   5.172 +fun transA(s,a,t) = (not(s)=t);
   5.173 +fun hom(i) = i mod 2 = 0;
   5.174 +fun nexts s A = [(s+1) mod 4];
   5.175 +check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
   5.176 +
   5.177 +fun nexts s A = [(s+1) mod 5];
   5.178 +
   5.179 +*)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Wed Apr 30 11:24:14 1997 +0200
     6.3 @@ -0,0 +1,384 @@
     6.4 + (*  Title:      HOLCF/IOA/ABP/Correctness.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Olaf Mueller
     6.7 +    Copyright   1995  TU Muenchen
     6.8 +
     6.9 +*)
    6.10 +
    6.11 +
    6.12 +goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
    6.13 +by (Fast_tac 1);
    6.14 +qed"exis_elim";
    6.15 +
    6.16 +Delsimps [split_paired_All];
    6.17 +Addsimps 
    6.18 + ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
    6.19 +   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, 
    6.20 +   actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, 
    6.21 +   trans_of_def] @ asig_projections @ set_lemmas);
    6.22 +
    6.23 +val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, 
    6.24 +                      rsch_fin_ioa_def, srch_fin_ioa_def, 
    6.25 +                      ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def];
    6.26 +Addsimps abschannel_fin;
    6.27 +
    6.28 +val impl_ioas =  [Sender.sender_ioa_def,Receiver.receiver_ioa_def];
    6.29 +val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def];
    6.30 +val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def];
    6.31 +Addcongs [let_weak_cong];
    6.32 +Addsimps [Let_def, ioa_triple_proj, starts_of_par];
    6.33 +
    6.34 +val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def];
    6.35 +val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ 
    6.36 +               asig_projections @ set_lemmas;
    6.37 +Addsimps hom_ioas;
    6.38 +
    6.39 +Addsimps [reduce_Nil,reduce_Cons];
    6.40 +
    6.41 +
    6.42 +
    6.43 +(* auxiliary function *)
    6.44 +fun rotate n i = EVERY(replicate n (etac revcut_rl i));
    6.45 +
    6.46 +(* lemmas about reduce *)
    6.47 +
    6.48 +goal Correctness.thy "(reduce(l)=[]) = (l=[])";  
    6.49 + by (rtac iffI 1);
    6.50 + by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
    6.51 + by (Fast_tac 1); 
    6.52 + by (List.list.induct_tac "l" 1);
    6.53 + by (Simp_tac 1);
    6.54 + by (Simp_tac 1);
    6.55 + by (rtac (expand_list_case RS iffD2) 1);
    6.56 + by (Asm_full_simp_tac 1);
    6.57 + by (REPEAT (rtac allI 1)); 
    6.58 + by (rtac impI 1); 
    6.59 + by (hyp_subst_tac 1);
    6.60 + by (rtac (expand_if RS ssubst) 1);
    6.61 + by (Asm_full_simp_tac 1);
    6.62 + by (Asm_full_simp_tac 1);
    6.63 +val l_iff_red_nil = result();
    6.64 +
    6.65 +goal Correctness.thy "s~=[] --> hd(s)=hd(reduce(s))";
    6.66 +by (List.list.induct_tac "s" 1);
    6.67 +by (Simp_tac 1);
    6.68 +by (case_tac "list =[]" 1);
    6.69 +by (Asm_full_simp_tac 1);
    6.70 +(* main case *)
    6.71 +by (rotate 1 1);
    6.72 +by (asm_full_simp_tac list_ss 1);
    6.73 +by (Simp_tac 1);
    6.74 +by (rtac (expand_list_case RS iffD2) 1);
    6.75 +by (asm_full_simp_tac list_ss 1);
    6.76 +by (REPEAT (rtac allI 1)); 
    6.77 + by (rtac impI 1); 
    6.78 +by (rtac (expand_if RS ssubst) 1);
    6.79 +by (REPEAT(hyp_subst_tac 1));
    6.80 +by (etac subst 1);
    6.81 +by (Simp_tac 1);
    6.82 +qed"hd_is_reduce_hd";
    6.83 +
    6.84 +(* to be used in the following Lemma *)
    6.85 +goal Correctness.thy "l~=[] --> reverse(reduce(l))~=[]";
    6.86 +by (List.list.induct_tac "l" 1);
    6.87 +by (Simp_tac 1);
    6.88 +by (case_tac "list =[]" 1);
    6.89 +by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1);
    6.90 +(* main case *)
    6.91 +by (rotate 1 1);
    6.92 +by (Asm_full_simp_tac 1);
    6.93 +by (cut_inst_tac [("l","list")] cons_not_nil 1); 
    6.94 +by (Asm_full_simp_tac 1);
    6.95 +by (REPEAT (etac exE 1));
    6.96 +by (Asm_simp_tac 1);
    6.97 +by (rtac (expand_if RS ssubst) 1);
    6.98 +by (hyp_subst_tac 1);
    6.99 +by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); 
   6.100 +qed"rev_red_not_nil";
   6.101 +
   6.102 +(* shows applicability of the induction hypothesis of the following Lemma 1 *)
   6.103 +goal Correctness.thy "!!l.[| l~=[] |] ==>   \
   6.104 +\   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
   6.105 + by (Simp_tac 1);
   6.106 + by (rtac (expand_list_case RS iffD2) 1);
   6.107 + by (asm_full_simp_tac list_ss 1);
   6.108 + by (REPEAT (rtac allI 1)); 
   6.109 + by (rtac impI 1); 
   6.110 + by (rtac (expand_if RS ssubst) 1);
   6.111 + by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
   6.112 +                          (rev_red_not_nil RS mp)])  1);
   6.113 +qed"last_ind_on_first";
   6.114 +
   6.115 +val impl_ss = !simpset delsimps [reduce_Cons];
   6.116 +
   6.117 +(* Main Lemma 1 for S_pkt in showing that reduce is refinement  *) 
   6.118 +goal Correctness.thy 
   6.119 +   "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
   6.120 +\      reduce(l@[x])=reduce(l) else                  \
   6.121 +\      reduce(l@[x])=reduce(l)@[x]"; 
   6.122 +by (rtac (expand_if RS ssubst) 1);
   6.123 +by (rtac conjI 1);
   6.124 +(* --> *)
   6.125 +by (List.list.induct_tac "l" 1);
   6.126 +by (Simp_tac 1);
   6.127 +by (case_tac "list=[]" 1);
   6.128 + by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
   6.129 + by (rtac impI 1);
   6.130 +by (Simp_tac 1);
   6.131 +by (cut_inst_tac [("l","list")] cons_not_nil 1);
   6.132 + by (asm_full_simp_tac impl_ss 1);
   6.133 + by (REPEAT (etac exE 1));
   6.134 + by (hyp_subst_tac 1);
   6.135 +by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
   6.136 +(* <-- *)
   6.137 +by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
   6.138 +by (List.list.induct_tac "l" 1);
   6.139 +by (Simp_tac 1);
   6.140 +by (case_tac "list=[]" 1);
   6.141 +by (cut_inst_tac [("l","list")] cons_not_nil 2);
   6.142 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   6.143 +by (auto_tac (!claset, 
   6.144 +	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
   6.145 +                      setloop split_tac [expand_if]));
   6.146 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   6.147 +qed"reduce_hd";
   6.148 +
   6.149 +
   6.150 +(* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
   6.151 +goal Correctness.thy 
   6.152 +  "!! s. [| s~=[] |] ==>  \
   6.153 +\    if hd(s)=hd(tl(s)) & tl(s)~=[] then    \
   6.154 +\      reduce(tl(s))=reduce(s) else      \
   6.155 +\      reduce(tl(s))=tl(reduce(s))"; 
   6.156 +by (cut_inst_tac [("l","s")] cons_not_nil 1);
   6.157 +by (Asm_full_simp_tac 1);
   6.158 +by (REPEAT (etac exE 1));
   6.159 +by (Asm_full_simp_tac 1);
   6.160 +by (rtac (expand_if RS ssubst) 1);
   6.161 +by (rtac conjI 1);
   6.162 +by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
   6.163 +by (Step_tac 1);
   6.164 +by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
   6.165 +by (Auto_tac());
   6.166 +val reduce_tl =result();
   6.167 +
   6.168 +
   6.169 +(*******************************************************************
   6.170 +          C h a n n e l   A b s t r a c t i o n
   6.171 + *******************************************************************)
   6.172 +
   6.173 +goal Correctness.thy 
   6.174 +      "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
   6.175 +by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   6.176 +(* ---------------- main-part ------------------- *)
   6.177 +by (REPEAT (rtac allI 1));
   6.178 +by (rtac imp_conj_lemma 1);
   6.179 +by (abs_action.induct_tac "a" 1);
   6.180 +(* ----------------- 2 cases ---------------------*)
   6.181 +by (ALLGOALS (simp_tac (!simpset addsimps [externals_def])));
   6.182 +(* fst case --------------------------------------*)
   6.183 + by (rtac impI 1);
   6.184 + by (rtac disjI2 1);
   6.185 +by (rtac reduce_hd 1);
   6.186 +(* snd case --------------------------------------*)
   6.187 + by (rtac impI 1);
   6.188 + by (REPEAT (etac conjE 1));
   6.189 + by (etac disjE 1);
   6.190 +by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   6.191 +by (etac (hd_is_reduce_hd RS mp) 1); 
   6.192 +by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   6.193 +by (rtac conjI 1);
   6.194 +by (etac (hd_is_reduce_hd RS mp) 1); 
   6.195 +by (rtac (bool_if_impl_or RS mp) 1);
   6.196 +by (etac reduce_tl 1);
   6.197 +qed"channel_abstraction";
   6.198 +
   6.199 +goal Correctness.thy 
   6.200 +      "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
   6.201 +by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   6.202 + srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   6.203 +qed"sender_abstraction";
   6.204 +
   6.205 +goal Correctness.thy 
   6.206 +      "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
   6.207 +by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   6.208 + srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   6.209 +qed"receiver_abstraction";
   6.210 +
   6.211 +
   6.212 +(* 3 thms that do not hold generally! The lucky restriction here is 
   6.213 +   the absence of internal actions. *)
   6.214 +goal Correctness.thy 
   6.215 +      "is_weak_ref_map (%id.id) sender_ioa sender_ioa";
   6.216 +by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   6.217 +by (TRY(
   6.218 +   (rtac conjI 1) THEN
   6.219 +(* start states *)
   6.220 +   (Fast_tac 1)));
   6.221 +(* main-part *)
   6.222 +by (REPEAT (rtac allI 1));
   6.223 +by (rtac imp_conj_lemma 1);
   6.224 +by (Action.action.induct_tac "a" 1);
   6.225 +(* 7 cases *)
   6.226 +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   6.227 +qed"sender_unchanged";
   6.228 +
   6.229 +(* 2 copies of before *)
   6.230 +goal Correctness.thy 
   6.231 +      "is_weak_ref_map (%id.id) receiver_ioa receiver_ioa";
   6.232 +by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   6.233 +by (TRY(
   6.234 +   (rtac conjI 1) THEN
   6.235 + (* start states *)
   6.236 +   (Fast_tac 1)));
   6.237 +(* main-part *)
   6.238 +by (REPEAT (rtac allI 1));
   6.239 +by (rtac imp_conj_lemma 1);
   6.240 +by (Action.action.induct_tac "a" 1);
   6.241 +(* 7 cases *)
   6.242 +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   6.243 +qed"receiver_unchanged";
   6.244 +
   6.245 +goal Correctness.thy 
   6.246 +      "is_weak_ref_map (%id.id) env_ioa env_ioa";
   6.247 +by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   6.248 +by (TRY(
   6.249 +   (rtac conjI 1) THEN
   6.250 +(* start states *)
   6.251 +   (Fast_tac 1)));
   6.252 +(* main-part *)
   6.253 +by (REPEAT (rtac allI 1));
   6.254 +by (rtac imp_conj_lemma 1);
   6.255 +by (Action.action.induct_tac "a" 1);
   6.256 +(* 7 cases *)
   6.257 +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   6.258 +qed"env_unchanged";
   6.259 +
   6.260 +Delsimps [Collect_False_empty];
   6.261 +
   6.262 +goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; 
   6.263 +by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
   6.264 +by (rtac set_ext 1);
   6.265 +by (Action.action.induct_tac "x" 1);
   6.266 +by (ALLGOALS(Simp_tac));
   6.267 +val compat_single_ch = result();
   6.268 +
   6.269 +(* totally the same as before *)
   6.270 +goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa"; 
   6.271 +by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
   6.272 +by (rtac set_ext 1);
   6.273 +by (Action.action.induct_tac "x" 1);
   6.274 +by (ALLGOALS(Simp_tac));
   6.275 +val compat_single_fin_ch = result();
   6.276 +
   6.277 +val ss =
   6.278 +  !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
   6.279 +                      asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
   6.280 +                      srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, 
   6.281 +                      rsch_ioa_def, Sender.sender_trans_def,
   6.282 +                      Receiver.receiver_trans_def] @ set_lemmas);
   6.283 +
   6.284 +goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)";
   6.285 +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,
   6.286 +                           asig_of_par,asig_comp_def,actions_def,
   6.287 +                           Int_def]) 1);
   6.288 +by (Simp_tac 1);
   6.289 +by (rtac set_ext 1);
   6.290 +by (Action.action.induct_tac "x" 1);
   6.291 +by (ALLGOALS Simp_tac);
   6.292 +val compat_rec = result();
   6.293 +
   6.294 +(* 5 proofs totally the same as before *)
   6.295 +goal Correctness.thy "compat_ioas receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
   6.296 +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   6.297 +by (Simp_tac 1);
   6.298 +by (rtac set_ext 1);
   6.299 +by (Action.action.induct_tac "x" 1);
   6.300 +by (ALLGOALS Simp_tac);
   6.301 +val compat_rec_fin =result();
   6.302 +
   6.303 +goal Correctness.thy "compat_ioas sender_ioa \
   6.304 +\      (receiver_ioa || srch_ioa || rsch_ioa)";
   6.305 +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   6.306 +by (Simp_tac 1);
   6.307 +by (rtac set_ext 1);
   6.308 +by (Action.action.induct_tac "x" 1);
   6.309 +by (ALLGOALS(Simp_tac));
   6.310 +val compat_sen=result();
   6.311 +
   6.312 +goal Correctness.thy "compat_ioas sender_ioa\
   6.313 +\      (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   6.314 +by (simp_tac (ss addsimps [empty_def,  compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   6.315 +by (Simp_tac 1);
   6.316 +by (rtac set_ext 1);
   6.317 +by (Action.action.induct_tac "x" 1);
   6.318 +by (ALLGOALS(Simp_tac));
   6.319 +val compat_sen_fin =result();
   6.320 +
   6.321 +goal Correctness.thy "compat_ioas env_ioa\
   6.322 +\      (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
   6.323 +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   6.324 +by (Simp_tac 1);
   6.325 +by (rtac set_ext 1);
   6.326 +by (Action.action.induct_tac "x" 1);
   6.327 +by (ALLGOALS(Simp_tac));
   6.328 +val compat_env=result();
   6.329 +
   6.330 +goal Correctness.thy "compat_ioas env_ioa\
   6.331 +\      (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   6.332 +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   6.333 +by (Simp_tac 1);
   6.334 +by (rtac set_ext 1);
   6.335 +by (Action.action.induct_tac "x" 1);
   6.336 +by (ALLGOALS Simp_tac);
   6.337 +val compat_env_fin=result();
   6.338 +
   6.339 +
   6.340 +(* lemmata about externals of channels *)
   6.341 +goal Correctness.thy 
   6.342 + "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
   6.343 +\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
   6.344 +   by (simp_tac (!simpset addsimps [externals_def]) 1);
   6.345 +val ext_single_ch = result();
   6.346 +
   6.347 +
   6.348 +
   6.349 +
   6.350 +
   6.351 +val ext_ss = [externals_of_par,ext_single_ch];
   6.352 +val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
   6.353 +         compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
   6.354 +val abstractions = [env_unchanged,sender_unchanged,
   6.355 +          receiver_unchanged,sender_abstraction,receiver_abstraction];
   6.356 +
   6.357 +
   6.358 +(************************************************************************
   6.359 +            S o u n d n e s s   o f   A b s t r a c t i o n        
   6.360 +*************************************************************************)
   6.361 +
   6.362 +val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
   6.363 +                             srch_fin_ioa_def, rsch_fin_ioa_def] @
   6.364 +                            impl_ioas @ env_ioas);
   6.365 +
   6.366 +(* FIX: this proof should be done with compositionality on trace level, not on 
   6.367 +        weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA 
   6.368 +
   6.369 +goal Correctness.thy 
   6.370 +     "is_weak_ref_map  abs  system_ioa  system_fin_ioa";
   6.371 +
   6.372 +by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
   6.373 +                                 rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
   6.374 +                      addsimps [system_def, system_fin_def, abs_def,
   6.375 +                                impl_ioa_def, impl_fin_ioa_def, sys_IOA,
   6.376 +                                sys_fin_IOA]) 1);
   6.377 +
   6.378 +by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1, 
   6.379 +                  simp_tac (ss addsimps abstractions) 1,
   6.380 +                  rtac conjI 1]));
   6.381 +
   6.382 +by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); 
   6.383 +
   6.384 +qed "system_refinement";
   6.385 +
   6.386 +
   6.387 +*)
   6.388 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Wed Apr 30 11:24:14 1997 +0200
     7.3 @@ -0,0 +1,49 @@
     7.4 +(*  Title:      HOLCF/IOA/ABP/Correctness.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Olaf Mueller
     7.7 +    Copyright   1995  TU Muenchen
     7.8 +
     7.9 +The main correctness proof: System_fin implements System
    7.10 +*)
    7.11 +
    7.12 +Correctness = IOA + Env + Impl + Impl_finite + 
    7.13 +
    7.14 +consts
    7.15 +
    7.16 +reduce           :: 'a list => 'a list
    7.17 +
    7.18 +abs              :: 'c
    7.19 +system_ioa       :: "('m action, bool * 'm impl_state)ioa"
    7.20 +system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
    7.21 +  
    7.22 +primrec
    7.23 +  reduce List.list  
    7.24 +  reduce_Nil  "reduce [] = []"
    7.25 +  reduce_Cons "reduce(x#xs) =   
    7.26 +                 (case xs of   
    7.27 +                     [] => [x]   
    7.28 +               |   y#ys => (if (x=y)   
    7.29 +                              then reduce xs   
    7.30 +                              else (x#(reduce xs))))"
    7.31 +
    7.32 +  
    7.33 +defs
    7.34 +  
    7.35 +system_def
    7.36 +  "system_ioa == (env_ioa || impl_ioa)"
    7.37 +
    7.38 +system_fin_def
    7.39 +  "system_fin_ioa == (env_ioa || impl_fin_ioa)"
    7.40 +  
    7.41 +abs_def "abs  ==   
    7.42 +        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
    7.43 +         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    7.44 +
    7.45 +rules
    7.46 +
    7.47 +  sys_IOA     "IOA system_ioa"
    7.48 +  sys_fin_IOA "IOA system_fin_ioa"
    7.49 +  
    7.50 +end
    7.51 +
    7.52 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOLCF/IOA/ABP/Env.thy	Wed Apr 30 11:24:14 1997 +0200
     8.3 @@ -0,0 +1,47 @@
     8.4 +(*  Title:      HOLCF/IOA/ABP/Impl.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Olaf Mueller
     8.7 +    Copyright   1995  TU Muenchen
     8.8 +
     8.9 +The environment
    8.10 +*)
    8.11 +
    8.12 +Env = IOA + Action +
    8.13 +
    8.14 +types
    8.15 +
    8.16 +'m env_state = "bool"
    8.17 +(*              give next bit to system  *)
    8.18 +
    8.19 +consts
    8.20 +
    8.21 +env_asig   :: 'm action signature
    8.22 +env_trans  :: ('m action, 'm env_state)transition set
    8.23 +env_ioa    :: ('m action, 'm env_state)ioa
    8.24 +next       :: 'm env_state => bool
    8.25 +
    8.26 +defs
    8.27 +
    8.28 +env_asig_def
    8.29 +  "env_asig == ({Next},                 
    8.30 +               UN m. {S_msg(m)},       
    8.31 +               {})"
    8.32 +
    8.33 +env_trans_def "env_trans ==                                           
    8.34 + {tr. let s = fst(tr);                                               
    8.35 +          t = snd(snd(tr))                                           
    8.36 +      in case fst(snd(tr))                                           
    8.37 +      of                                                             
    8.38 +      Next       => t=True |                                         
    8.39 +      S_msg(m)   => s=True & t=False |                               
    8.40 +      R_msg(m)   => False |                                          
    8.41 +      S_pkt(pkt) => False |                                          
    8.42 +      R_pkt(pkt) => False |                                          
    8.43 +      S_ack(b)   => False |                                          
    8.44 +      R_ack(b)   => False}"
    8.45 +
    8.46 +env_ioa_def "env_ioa == 
    8.47 + (env_asig, {True}, env_trans)"
    8.48 +
    8.49 +end
    8.50 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOLCF/IOA/ABP/Impl.thy	Wed Apr 30 11:24:14 1997 +0200
     9.3 @@ -0,0 +1,35 @@
     9.4 +(*  Title:      HOLCF/IOA/ABP/Impl.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     Olaf Mueller
     9.7 +    Copyright   1995  TU Muenchen
     9.8 +
     9.9 +The implementation
    9.10 +*)
    9.11 +
    9.12 +Impl = Sender + Receiver +  Abschannel +
    9.13 +
    9.14 +types 
    9.15 +
    9.16 +'m impl_state 
    9.17 += "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    9.18 +(*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    9.19 +
    9.20 +
    9.21 +constdefs
    9.22 +
    9.23 + impl_ioa    :: ('m action, 'm impl_state)ioa
    9.24 + "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
    9.25 +
    9.26 + sen         :: 'm impl_state => 'm sender_state
    9.27 + "sen == fst"
    9.28 +
    9.29 + rec         :: 'm impl_state => 'm receiver_state
    9.30 + "rec == fst o snd"
    9.31 +
    9.32 + srch        :: 'm impl_state => 'm packet list
    9.33 + "srch == fst o snd o snd"
    9.34 +
    9.35 + rsch        :: 'm impl_state => bool list
    9.36 + "rsch == snd o snd o snd"
    9.37 +
    9.38 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy	Wed Apr 30 11:24:14 1997 +0200
    10.3 @@ -0,0 +1,36 @@
    10.4 +(*  Title:      HOLCF/IOA/ABP/Impl.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Olaf Mueller
    10.7 +    Copyright   1995  TU Muenchen
    10.8 +
    10.9 +The implementation
   10.10 +*)
   10.11 +
   10.12 +Impl_finite = Sender + Receiver +  Abschannel_finite +
   10.13 +  
   10.14 +types 
   10.15 +
   10.16 +'m impl_fin_state 
   10.17 += "'m sender_state * 'm receiver_state * 'm packet list * bool list"
   10.18 +(*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
   10.19 +
   10.20 +constdefs
   10.21 +
   10.22 + impl_fin_ioa    :: ('m action, 'm impl_fin_state)ioa
   10.23 + "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
   10.24 +                   rsch_fin_ioa)"
   10.25 +
   10.26 + sen_fin         :: 'm impl_fin_state => 'm sender_state
   10.27 + "sen_fin == fst"
   10.28 +
   10.29 + rec_fin         :: 'm impl_fin_state => 'm receiver_state
   10.30 + "rec_fin == fst o snd"
   10.31 +
   10.32 + srch_fin        :: 'm impl_fin_state => 'm packet list
   10.33 + "srch_fin == fst o snd o snd"
   10.34 +
   10.35 + rsch_fin        :: 'm impl_fin_state => bool list
   10.36 + "rsch_fin == snd o snd o snd"
   10.37 +
   10.38 +end
   10.39 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Wed Apr 30 11:24:14 1997 +0200
    11.3 @@ -0,0 +1,57 @@
    11.4 +(*  Title:      HOLCF/IOA/ABP/Lemmas.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Olaf Mueller
    11.7 +    Copyright   1995  TU Muenchen
    11.8 +
    11.9 +*)
   11.10 +
   11.11 +(* Logic *)
   11.12 +
   11.13 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   11.14 +  by(fast_tac (!claset addDs prems) 1);
   11.15 +qed "imp_conj_lemma";
   11.16 +
   11.17 +goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
   11.18 +by (Fast_tac 1);
   11.19 +val and_de_morgan_and_absorbe = result();
   11.20 +
   11.21 +goal HOL.thy "(if C then A else B) --> (A|B)";
   11.22 +by (rtac (expand_if RS ssubst) 1);
   11.23 +by (Fast_tac 1);
   11.24 +val bool_if_impl_or = result();
   11.25 +
   11.26 +(* Sets *)
   11.27 +
   11.28 +val set_lemmas =
   11.29 +   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
   11.30 +        ["f(x) : (UN x. {f(x)})",
   11.31 +         "f x y : (UN x y. {f x y})",
   11.32 +         "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
   11.33 +         "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
   11.34 +
   11.35 +(* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
   11.36 +   namely for Intersections and the empty list (compatibility of IOA!)  *)
   11.37 +goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
   11.38 + by (rtac set_ext 1);
   11.39 + by (Fast_tac 1);
   11.40 +val singleton_set =result();
   11.41 +
   11.42 +goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
   11.43 + by (Fast_tac 1);
   11.44 +val de_morgan = result();
   11.45 +
   11.46 +(* Lists *)
   11.47 +
   11.48 +val list_ss = simpset_of "List";
   11.49 +
   11.50 +goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
   11.51 +by (List.list.induct_tac "l" 1);
   11.52 +by (simp_tac list_ss 1);
   11.53 +by (simp_tac list_ss 1);
   11.54 +val hd_append =result();
   11.55 +
   11.56 +goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
   11.57 + by (List.list.induct_tac "l" 1);
   11.58 + by (simp_tac list_ss 1);
   11.59 + by (Fast_tac 1);
   11.60 +qed"cons_not_nil";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Wed Apr 30 11:24:14 1997 +0200
    12.3 @@ -0,0 +1,9 @@
    12.4 +(*  Title:      HOLCF/IOA/ABP/Lemmas.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Olaf Mueller
    12.7 +    Copyright   1995  TU Muenchen
    12.8 +
    12.9 +Arithmetic lemmas
   12.10 +*)
   12.11 +
   12.12 +Lemmas = Arith
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOLCF/IOA/ABP/Packet.thy	Wed Apr 30 11:24:14 1997 +0200
    13.3 @@ -0,0 +1,23 @@
    13.4 +(*  Title:      HOLCF/IOA/ABP/Packet.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Olaf Mueller
    13.7 +    Copyright   1995  TU Muenchen
    13.8 +
    13.9 +Packets
   13.10 +*)
   13.11 +
   13.12 +Packet = Arith +
   13.13 +
   13.14 +types
   13.15 +
   13.16 +   'msg packet = "bool * 'msg"
   13.17 +
   13.18 +constdefs
   13.19 +
   13.20 +  hdr  :: 'msg packet => bool
   13.21 +  "hdr == fst"
   13.22 +
   13.23 +  msg :: 'msg packet => 'msg
   13.24 +  "msg == snd"
   13.25 +
   13.26 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Wed Apr 30 11:24:14 1997 +0200
    14.3 @@ -0,0 +1,17 @@
    14.4 +(*  Title:      HOL/IOA/ABP/ROOT.ML
    14.5 +    ID:         $Id$
    14.6 +    Author:     Olaf Mueller
    14.7 +    Copyright   1995  TU Muenchen
    14.8 +
    14.9 +This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata.
   14.10 +
   14.11 +For details see the README.html file.
   14.12 +
   14.13 +Should be executed in the subdirectory HOLCF/IOA/examples/ABP.
   14.14 +*)
   14.15 +
   14.16 +goals_limit := 1;
   14.17 +
   14.18 +loadpath:=["."];
   14.19 +
   14.20 +use_thy "Correctness";
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOLCF/IOA/ABP/Read_me	Wed Apr 30 11:24:14 1997 +0200
    15.3 @@ -0,0 +1,10 @@
    15.4 +Isabelle Verification of the Alternating Bit Protocol by 
    15.5 +combining IOA with Model Checking
    15.6 +
    15.7 +-------------------------------------------------------------
    15.8 +
    15.9 +Correctness.ML contains the proof of the abstraction from unbounded
   15.10 +channels to finite ones.
   15.11 +
   15.12 +Check.ML contains a simple ModelChecker prototype checking Spec against 
   15.13 +the finite version of the ABP-protocol.
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOLCF/IOA/ABP/Receiver.thy	Wed Apr 30 11:24:14 1997 +0200
    16.3 @@ -0,0 +1,59 @@
    16.4 +(*  Title:      HOLCF/IOA/ABP/Receiver.thy
    16.5 +    ID:         $Id$
    16.6 +    Author:     Olaf Mueller
    16.7 +    Copyright   1995  TU Muenchen
    16.8 +
    16.9 +The implementation: receiver
   16.10 +*)
   16.11 +
   16.12 +Receiver = List + IOA + Action + Lemmas +
   16.13 +
   16.14 +types 
   16.15 +
   16.16 +'m receiver_state
   16.17 += "'m list * bool"
   16.18 +(* messages  mode *)
   16.19 +
   16.20 +consts
   16.21 +
   16.22 +  receiver_asig :: 'm action signature
   16.23 +  receiver_trans:: ('m action, 'm receiver_state)transition set
   16.24 +  receiver_ioa  :: ('m action, 'm receiver_state)ioa
   16.25 +  rq            :: 'm receiver_state => 'm list
   16.26 +  rbit          :: 'm receiver_state => bool
   16.27 +
   16.28 +defs
   16.29 +
   16.30 +rq_def       "rq == fst"
   16.31 +rbit_def     "rbit == snd"
   16.32 +
   16.33 +receiver_asig_def "receiver_asig ==            
   16.34 + (UN pkt. {R_pkt(pkt)},                       
   16.35 +  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
   16.36 +  {})"
   16.37 +
   16.38 +receiver_trans_def "receiver_trans ==                                    
   16.39 + {tr. let s = fst(tr);                                                  
   16.40 +          t = snd(snd(tr))                                              
   16.41 +      in                                                                
   16.42 +      case fst(snd(tr))                                                 
   16.43 +      of   
   16.44 +      Next    =>  False |     
   16.45 +      S_msg(m) => False |                                               
   16.46 +      R_msg(m) => (rq(s) ~= [])  &                                     
   16.47 +                   m = hd(rq(s))  &                             
   16.48 +                   rq(t) = tl(rq(s))   &                              
   16.49 +                  rbit(t)=rbit(s)  |                                 
   16.50 +      S_pkt(pkt) => False |                                          
   16.51 +      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
   16.52 +                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
   16.53 +                         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
   16.54 +      S_ack(b) => b = rbit(s)                        &               
   16.55 +                      rq(t) = rq(s)                    &             
   16.56 +                      rbit(t)=rbit(s) |                              
   16.57 +      R_ack(b) => False}"
   16.58 +
   16.59 +receiver_ioa_def "receiver_ioa == 
   16.60 + (receiver_asig, {([],False)}, receiver_trans)"
   16.61 +
   16.62 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOLCF/IOA/ABP/Sender.thy	Wed Apr 30 11:24:14 1997 +0200
    17.3 @@ -0,0 +1,57 @@
    17.4 +(*  Title:      HOLCF/IOA/ABP/Sender.thy
    17.5 +    ID:         $Id$
    17.6 +    Author:     Olaf Mueller
    17.7 +    Copyright   1995  TU Muenchen
    17.8 +
    17.9 +The implementation: sender
   17.10 +*)
   17.11 +
   17.12 +Sender = IOA + Action + List + Lemmas +
   17.13 +
   17.14 +types
   17.15 +
   17.16 +'m sender_state = "'m list  *  bool"
   17.17 +(*                messages     Alternating Bit   *)
   17.18 +
   17.19 +consts
   17.20 +
   17.21 +sender_asig   :: 'm action signature
   17.22 +sender_trans  :: ('m action, 'm sender_state)transition set
   17.23 +sender_ioa    :: ('m action, 'm sender_state)ioa
   17.24 +sq            :: 'm sender_state => 'm list
   17.25 +sbit          :: 'm sender_state => bool
   17.26 +
   17.27 +defs
   17.28 +
   17.29 +sq_def       "sq == fst"
   17.30 +sbit_def     "sbit == snd"
   17.31 +
   17.32 +sender_asig_def
   17.33 +  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
   17.34 +                  UN pkt. {S_pkt(pkt)},                   
   17.35 +                  {})"
   17.36 +
   17.37 +sender_trans_def "sender_trans ==                                     
   17.38 + {tr. let s = fst(tr);                                               
   17.39 +          t = snd(snd(tr))                                           
   17.40 +      in case fst(snd(tr))                                           
   17.41 +      of   
   17.42 +      Next     => if sq(s)=[] then t=s else False |                
   17.43 +      S_msg(m) => sq(t)=sq(s)@[m]   &                                
   17.44 +                  sbit(t)=sbit(s)  |                                 
   17.45 +      R_msg(m) => False |                                            
   17.46 +      S_pkt(pkt) => sq(s) ~= []  &                                   
   17.47 +                     hdr(pkt) = sbit(s)      &                        
   17.48 +                    msg(pkt) = hd(sq(s))    &                   
   17.49 +                    sq(t) = sq(s)           &                        
   17.50 +                    sbit(t) = sbit(s) |                              
   17.51 +      R_pkt(pkt) => False |                                          
   17.52 +      S_ack(b)   => False |                                          
   17.53 +      R_ack(b)   => if b = sbit(s) then                              
   17.54 +                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
   17.55 +                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
   17.56 +
   17.57 +sender_ioa_def "sender_ioa == 
   17.58 + (sender_asig, {([],True)}, sender_trans)"
   17.59 +
   17.60 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOLCF/IOA/ABP/Spec.thy	Wed Apr 30 11:24:14 1997 +0200
    18.3 @@ -0,0 +1,39 @@
    18.4 +(*  Title:      HOLCF/IOA/ABP/Spec.thy
    18.5 +    ID:         $Id$
    18.6 +    Author:     Olaf Mueller
    18.7 +    Copyright   1995  TU Muenchen
    18.8 +
    18.9 +The specification of reliable transmission
   18.10 +*)
   18.11 +
   18.12 +Spec = List + IOA + Action +
   18.13 +
   18.14 +consts
   18.15 +
   18.16 +spec_sig   :: 'm action signature
   18.17 +spec_trans :: ('m action, 'm list)transition set
   18.18 +spec_ioa   :: ('m action, 'm list)ioa
   18.19 +
   18.20 +defs
   18.21 +
   18.22 +sig_def "spec_sig == (UN m.{S_msg(m)}, 
   18.23 +                     UN m.{R_msg(m)} Un {Next}, 
   18.24 +                     {})"
   18.25 +
   18.26 +trans_def "spec_trans ==                           
   18.27 + {tr. let s = fst(tr);                            
   18.28 +          t = snd(snd(tr))                        
   18.29 +      in                                          
   18.30 +      case fst(snd(tr))                           
   18.31 +      of   
   18.32 +      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
   18.33 +      S_msg(m) => t = s@[m]  |                    
   18.34 +      R_msg(m) => s = (m#t)  |                    
   18.35 +      S_pkt(pkt) => False |                    
   18.36 +      R_pkt(pkt) => False |                    
   18.37 +      S_ack(b) => False |                      
   18.38 +      R_ack(b) => False}"
   18.39 +
   18.40 +ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
   18.41 +
   18.42 +end