# HG changeset patch
# User mueller
# Date 801909900 -7200
# Node ID 82fd99d5a6ffa42eaa4916053b20c565a9f92310
# Parent  1a768988f8e31fc7bf3f61c13345385396b72e68
polish

diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Abschannel.thy
--- a/src/HOL/IOA/ABP/Abschannel.thy	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel.thy	Wed May 31 10:45:00 1995 +0200
@@ -1,21 +1,21 @@
-(*  Title:      HOL/IOA/ABP/Abschannels.thy
+(*  Title:      HOL/IOA/example/Abschannels.thy
     ID:         $Id$
     Author:     Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Copyright   1994  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"
@@ -42,7 +42,11 @@
 srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
 rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
 
-
+  
+(**********************************************************
+       G e n e r i c   C h a n n e l
+ *********************************************************)
+  
 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
 
 ch_trans_def "ch_trans ==                                       \
@@ -57,6 +61,10 @@
   
 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
 
+(**********************************************************
+  C o n c r e t e  C h a n n e l s  b y   R e n a m i n g 
+ *********************************************************)
+  
 rsch_actions_def "rsch_actions (akt) ==                      \
 \	    case akt of   \
 \           Next    =>  None |          \
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Wed May 31 10:45:00 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Abschannel_finite.thy
+(*  Title:      HOL/IOA/example/Abschannels.thy
     ID:         $Id$
     Author:     Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Copyright   1994  TU Muenchen
 
 The transmission channel -- finite version
 *)
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Action.ML
--- a/src/HOL/IOA/ABP/Action.ML	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Action.ML	Wed May 31 10:45:00 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Action.ML
+(*  Title:      HOL/IOA/example/Action.ML
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 Derived rules for actions
 *)
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Action.thy
--- a/src/HOL/IOA/ABP/Action.thy	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Action.thy	Wed May 31 10:45:00 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Action.thy
+(*  Title:      HOL/IOA/example/Action.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 The set of all actions of the system
 *)
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Check.ML
--- a/src/HOL/IOA/ABP/Check.ML	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Check.ML	Wed May 31 10:45:00 1995 +0200
@@ -1,14 +1,9 @@
-(*  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 *)
+ 
+(* ----------------------------------------------------------------
+       P r o t o t y p e   M o d e l   C h e c k e r 
+   ----------------------------------------------------------------*)
 
 fun check(extacts,intacts,string_of_a,startsI,string_of_s,
           nexts,hom,transA,startsS) =
@@ -16,16 +11,16 @@
         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 ()
+                          (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 ()
+                                 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""));
+                                 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)
@@ -39,41 +34,51 @@
   in checks(startsI,[]) end;
 
 
-(* datatypes for ABP example *)
+(* ------------------------------------------------------
+                 A B P     E x a m p l e
+   -------------------------------------------------------*)
 
-datatype msg = m;
+datatype msg = m | n | l;
 datatype act = Next | S_msg of msg | R_msg of msg
                     | S_pkt of bool * msg | R_pkt of bool * msg
                     | S_ack of bool | R_ack of bool;
 
+(* -------------------- Transition relation of Specification -----------*)
+
 fun transA((u,s),a,(v,t)) = 
     (case a of 
        Next       => v andalso t = s |                         
-       S_msg(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_msg(q)   => u andalso not(v) andalso t = s@[q]   |    
+       R_msg(q)   => u = v andalso s = (q::t)  |                    
+       S_pkt(b,q) => false |                    
+       R_pkt(b,q) => false |                    
        S_ack(b)   => false |                      
        R_ack(b)   => false);
 
+
+(* ---------------------- Abstraction function --------------------------*)
+
 fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
 
+
+(* --------------------- Transition relation of Implementation ----------*)
+
 fun nexts (s as (env,p,a,q,b,ch1,ch2)) action =
     (case action of
        Next       => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] |                         
-       S_msg(m)   => if env then [(false,p@[m],a,q,b,ch1,ch2)] else [] |     
-       R_msg(m)   => if (q<>[] andalso m=hd(q)) 
+       S_msg(mornorl)   => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] |     
+       R_msg(mornorl)   => if (q<>[] andalso mornorl=hd(q)) 
                         then [(env,p,a,tl(q),b,ch1,ch2)]
                         else [] |                    
-       S_pkt(h,m) => if (p<>[] andalso m=hd(p) andalso h=a)
-                        then (if (ch1<>[] andalso hd(rev(ch1))=(h,m))
+       S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a)
+                        then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl))
                               then [s]
-                              else [s,(env,p,a,q,b,ch1@[(h,m)],ch2)])
+                              else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)])
                         else [] |
-       R_pkt(h,m) => if (ch1<>[] andalso hd(ch1)=(h,m))
+       R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl))
                          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)]
+                               then [(env,p,a,q@[mornorl],not(b),ch1,ch2),
+                                     (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)]
                                else [s,(env,p,a,q,b,tl(ch1),ch2)])
                           else [] | 
        S_ack(h)   => if (h=b)
@@ -89,36 +94,42 @@
                          else [])
 
 
-val extactions = [Next,S_msg(m),R_msg(m)];
+val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
 val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true),
-                  S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false)];
- 
+                  S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false),
+                  S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l),
+               S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)];
+
 
-(* Input / Output auxiliary functions *)
+(* ------------------------------------
+           Input / Output utilities 
+   ------------------------------------*)
 
-fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
+fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   let fun prec x = (prs ","; pre x)
   in
-    (case l of
+    (case lll of
       [] => (prs lpar; prs rpar)
-    | x::l => (prs lpar; pre x; seq prec l; prs rpar))
+    | x::lll => (prs lpar; pre x; seq prec lll; prs rpar))
    end;
 
 fun pr_bool true = output(std_out,"true")
 |   pr_bool false = output(std_out,"false");
 
-fun pr_msg m = output(std_out,"m");
+fun pr_msg m = output(std_out,"m")
+|   pr_msg n = output(std_out,"n")
+|   pr_msg l = output(std_out,"l");
 
 fun pr_act a = output(std_out, case a of
       Next => "Next"|                         
-      S_msg(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_msg(ma) => "S_msg(ma)"  |
+      R_msg(ma) => "R_msg(ma)"  |
+      S_pkt(b,ma) => "S_pkt(b,ma)" |                    
+      R_pkt(b,ma) => "R_pkt(b,ma)" |                    
       S_ack(b)   => "S_ack(b)" |                      
       R_ack(b)   => "R_ack(b)");
 
-fun pr_pkt (b,m) = (prs "<"; pr_bool b;prs ", "; pr_msg m; prs ">");
+fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">");
 
 val pr_bool_list  = print_list("[","]",pr_bool);
 val pr_msg_list   = print_list("[","]",pr_msg);
@@ -130,11 +141,30 @@
          pr_bool b;  prs ", "; pr_pkt_list ch1;  prs ", ";
          pr_bool_list ch2; prs "}");
 
-(* ----------------------------*)
-(* main check function call    *)
-(* ----------------------------*)
+
 
+(* ---------------------------------
+         Main function call
+   ---------------------------------*)
+
+(*
 check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], 
       pr_tuple, nexts, hom, transA, [(true,[])]);
+*)
+
+
+
 
 
+(*
+           Little test example
+
+datatype act = A;
+fun transA(s,a,t) = (not(s)=t);
+fun hom(i) = i mod 2 = 0;
+fun nexts s A = [(s+1) mod 4];
+check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
+
+fun nexts s A = [(s+1) mod 5];
+
+*)
\ No newline at end of file
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Wed May 31 10:45:00 1995 +0200
@@ -1,11 +1,12 @@
- (*  Title:      HOL/IOA/ABP/Correctness.ML
+ (*  Title:      HOL/IOA/example/Correctness.ML
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 *)
 
 open Correctness; open Abschannel; open Abschannel_finite;
+open Impl; open Impl_finite;
 
 goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
 by (fast_tac HOL_cs 1);
@@ -39,6 +40,8 @@
 val red_ss_ch = merge_ss(abschannel_fin_ss,red_ss);
 
 
+
+
 (* auxiliary function *)
 fun rotate n i = EVERY(replicate n (etac revcut_rl i));
 
@@ -168,31 +171,34 @@
 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 (REPEAT(hyp_subst_tac 2));
 by (ALLGOALS (asm_full_simp_tac red_ss));
 val reduce_tl =result();
 
 
+(*******************************************************************
+          C h a n n e l   A b s t r a c t i o n
+ *******************************************************************)
 
 goal Correctness.thy 
       "is_weak_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 *)
+(* --------------  start states ----------------- *)
 by (simp_tac red_ss_ch 1);
 br ballI 1;
 by (asm_full_simp_tac red_ss_ch 1);
-(* main-part *)
+(* ---------------- main-part ------------------- *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (act.induct_tac "a" 1);
-(* 2 cases *)
+(* ----------------- 2 cases ---------------------*)
 by (ALLGOALS (simp_tac (red_ss_ch addsimps [externals_def])));
-(* fst case *)
+(* fst case --------------------------------------*)
  by (rtac impI 1);
  by (rtac disjI2 1);
 by (rtac reduce_hd 1);
-(* snd case *)
+(* snd case --------------------------------------*)
  by (rtac impI 1);
  by (REPEAT (etac conjE 1));
  by (etac disjE 1);
@@ -240,7 +246,7 @@
       "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 *)
+ (* start states *)
 br ballI 1;
 by (simp_tac red_ss_ch 1);
 (* main-part *)
@@ -355,17 +361,82 @@
 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]))); 
+
+
+
+
+val ext_ss = [externals_of_par,ext_single_ch];
+val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
+         compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
+val abstractions = [env_unchanged,sender_unchanged,
+          receiver_unchanged,sender_abstraction,receiver_abstraction];
+val impl_ss = impl_ss addsimps [impl_def,impl_fin_def,sys_IOA, sys_fin_IOA];
+val sys_ss = impl_ss addsimps [system_def, system_fin_def, abs_def];
+
+
+
+(************************************************************************
+            S o u n d n e s s   o f   A b s t r a c t i o n        
+*************************************************************************)
+
+
+goal Correctness.thy 
+     "is_weak_pmap  abs  system_ioa  system_fin_ioa";
+
+by (simp_tac sys_ss 1);
+
+by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, 
+                  simp_tac (red_ss addsimps abstractions) 1,
+                  rtac conjI 1]));
+
+by (ALLGOALS (simp_tac (red_ss addsimps ext_ss @ compat_ss))); 
+
 qed "system_refinement";
 
+
+
+(************************************************************************
+              I n t e r a c t i v e   A b s t r a c t i o n 
+*************************************************************************)
+
+goal Correctness.thy
+   "ioa_implements system_ioa system_fin_ioa"; 
+
+(* ------------------- Rewriting ----------------------------*)
+by (simp_tac (impl_ss addsimps [ioa_implements_def]) 1);
+by (rtac conjI 1);
+by (simp_tac (sys_ss addsimps ext_ss) 1);
+
+(* ------------------- Lemmata ------------------------------*)
+by (rtac trace_inclusion 1); 
+by (rtac system_refinement 4);
+
+(* -------------------- Rewriting ---------------------------*)
+by (ALLGOALS (simp_tac impl_ss));
+by (simp_tac (sys_ss addsimps ext_ss) 1);
+
+qed"interactive_abstraction";
+
+
+
+
+
+(***********************************************************************
+                   Illustrative ISABELLE Examples
+************************************************************************)
+ 
+(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
+
+goal Set.thy 
+          "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
+
+by (best_tac (set_cs addSEs [equalityCE]) 1);
+qed "cantor1";
+
+(***** Theorem 2   *)
+val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
+by (cut_facts_tac prems 1);
+by (rtac equalityI 1);
+by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+qed "inv_image_comp";
\ No newline at end of file
diff -r 1a768988f8e3 -r 82fd99d5a6ff src/HOL/IOA/ABP/Correctness.thy
--- a/src/HOL/IOA/ABP/Correctness.thy	Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.thy	Wed May 31 10:45:00 1995 +0200
@@ -1,6 +1,6 @@
-(*  Title:      HOL/IOA/ABP/Correctness.thy
+(*  Title:      HOL/IOA/example/Correctness.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
+    Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
 
 The main correctness proof: System_fin implements System
@@ -10,8 +10,12 @@
 
 consts
 
-reduce :: "'a list => 'a list"
+reduce           :: "'a list => 'a list"
 
+abs              :: "'c"
+system_ioa       :: "('m action, bool * 'm impl_state)ioa"
+system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
+  
 primrec
   reduce List.list  
   reduce_Nil  "reduce [] = []"
@@ -22,6 +26,24 @@
 \	                      then reduce xs   \
 \	                      else (x#(reduce xs))))"
 
+  
+defs
+  
+system_def
+  "system_ioa == (env_ioa || impl_ioa)"
+
+system_fin_def
+  "system_fin_ioa == (env_ioa || impl_fin_ioa)"
+  
+abs_def "abs  ==   \
+\	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   \
+\	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+
+rules
+
+  sys_IOA     "IOA system_ioa"
+  sys_fin_IOA "IOA system_fin_ioa"
+  
 end