src/HOLCF/IOA/meta_theory/Automata.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4473 803d1e302af1
child 4536 74f7c556fd90
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     1 (*  Title:      HOLCF/IOA/meta_theory/Automata.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
     4     Copyright   1994, 1996  TU Muenchen
     5 
     6 The I/O automata of Lynch and Tuttle.
     7 *)
     8 
     9 (* Has been removed from HOL-simpset, who knows why? *)
    10 Addsimps [Let_def];
    11 
    12 open reachable;
    13 
    14 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
    15 
    16 (* ----------------------------------------------------------------------------------- *)
    17 
    18 section "asig_of, starts_of, trans_of";
    19 
    20 
    21 goal thy
    22  "((asig_of (x,y,z,w,s)) = x)   & \
    23 \ ((starts_of (x,y,z,w,s)) = y) & \
    24 \ ((trans_of (x,y,z,w,s)) = z)  & \
    25 \ ((wfair_of (x,y,z,w,s)) = w) & \
    26 \ ((sfair_of (x,y,z,w,s)) = s)";
    27   by (simp_tac (simpset() addsimps ioa_projections) 1);
    28 qed "ioa_triple_proj";
    29 
    30 goalw thy [is_trans_of_def,actions_def, is_asig_def]
    31   "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
    32   by (REPEAT(etac conjE 1));
    33   by (EVERY1[etac allE, etac impE, atac]);
    34   by (Asm_full_simp_tac 1);
    35 qed "trans_in_actions";
    36 
    37 goal thy
    38 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
    39   by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
    40 qed "starts_of_par";
    41 
    42 goal thy
    43 "trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \       
    44 \            in (a:act A | a:act B) & \
    45 \               (if a:act A then       \                
    46 \                  (fst(s),a,fst(t)):trans_of(A) \                    
    47 \                else fst(t) = fst(s))            \                      
    48 \               &                                  \                     
    49 \               (if a:act B then                    \   
    50 \                  (snd(s),a,snd(t)):trans_of(B)     \                
    51 \                else snd(t) = snd(s))}";
    52 
    53 by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
    54 qed "trans_of_par";
    55 
    56 
    57 (* ----------------------------------------------------------------------------------- *)
    58 
    59 section "actions and par";
    60 
    61 
    62 goal thy 
    63 "actions(asig_comp a b) = actions(a) Un actions(b)";
    64   by (simp_tac (simpset() addsimps
    65                ([actions_def,asig_comp_def]@asig_projections)) 1);
    66   by (fast_tac (set_cs addSIs [equalityI]) 1);
    67 qed "actions_asig_comp";
    68 
    69 
    70 goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
    71   by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
    72 qed "asig_of_par";
    73 
    74 
    75 goal thy "ext (A1||A2) =    \
    76 \  (ext A1) Un (ext A2)";
    77 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,
    78       asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
    79 by (rtac set_ext 1); 
    80 by (fast_tac set_cs 1);
    81 qed"externals_of_par"; 
    82 
    83 goal thy "act (A1||A2) =    \
    84 \  (act A1) Un (act A2)";
    85 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
    86       asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
    87 by (rtac set_ext 1); 
    88 by (fast_tac set_cs 1);
    89 qed"actions_of_par"; 
    90 
    91 goal thy "inp (A1||A2) =\
    92 \         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
    93 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
    94       asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
    95 qed"inputs_of_par";
    96   
    97 goal thy "out (A1||A2) =\
    98 \         (out A1) Un (out A2)";
    99 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   100       asig_outputs_def,Un_def,set_diff_def]) 1);
   101 qed"outputs_of_par";
   102 
   103 goal thy "int (A1||A2) =\
   104 \         (int A1) Un (int A2)";
   105 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
   106       asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
   107 qed"internals_of_par";
   108 
   109 (* ---------------------------------------------------------------------------------- *)
   110 
   111 section "actions and compatibility"; 
   112 
   113 goal thy"compatible A B = compatible B A";
   114 by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
   115 by Auto_tac;
   116 qed"compat_commute";
   117 
   118 goalw thy [externals_def,actions_def,compatible_def]
   119  "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
   120 by (Asm_full_simp_tac 1);
   121 by (best_tac (set_cs addEs [equalityCE]) 1);
   122 qed"ext1_is_not_int2";
   123 
   124 (* just commuting the previous one: better commute compatible *)
   125 goalw thy [externals_def,actions_def,compatible_def]
   126  "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
   127 by (Asm_full_simp_tac 1);
   128 by (best_tac (set_cs addEs [equalityCE]) 1);
   129 qed"ext2_is_not_int1";
   130 
   131 bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
   132 bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
   133 
   134 goalw thy  [externals_def,actions_def,compatible_def]
   135  "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
   136 by (Asm_full_simp_tac 1);
   137 by (best_tac (set_cs addEs [equalityCE]) 1);
   138 qed"intA_is_not_extB";
   139 
   140 goalw thy [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
   141 "!! a. [| compatible A B; a:int A |] ==> a ~: act B";
   142 by (Asm_full_simp_tac 1);
   143 by (best_tac (set_cs addEs [equalityCE]) 1);
   144 qed"intA_is_not_actB";
   145 
   146 (* the only one that needs disjointness of outputs and of internals and _all_ acts *)
   147 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
   148     compatible_def,is_asig_def,asig_of_def]
   149 "!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
   150 by (Asm_full_simp_tac 1);
   151 by (best_tac (set_cs addEs [equalityCE]) 1);
   152 qed"outAactB_is_inpB";
   153 
   154 (* needed for propagation of input_enabledness from A,B to A||B *)
   155 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
   156     compatible_def,is_asig_def,asig_of_def]
   157 "!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
   158 by (Asm_full_simp_tac 1);
   159 by (best_tac (set_cs addEs [equalityCE]) 1);
   160 qed"inpAAactB_is_inpBoroutB";
   161 
   162 (* ---------------------------------------------------------------------------------- *)
   163 
   164 section "input_enabledness and par";  
   165 
   166 
   167 (* ugly case distinctions. Heart of proof: 
   168      1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
   169      2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
   170 goalw thy [input_enabled_def] 
   171 "!!A. [| compatible A B; input_enabled A; input_enabled B|] \
   172 \     ==> input_enabled (A||B)";
   173 by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1);
   174 by (safe_tac set_cs);
   175 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   176 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2);
   177 (* a: inp A *)
   178 by (case_tac "a:act B" 1);
   179 (* a:act B *)
   180 by (eres_inst_tac [("x","a")] allE 1);
   181 by (Asm_full_simp_tac 1);
   182 by (dtac inpAAactB_is_inpBoroutB 1);
   183 by (assume_tac 1);
   184 by (assume_tac 1);
   185 by (eres_inst_tac [("x","a")] allE 1);
   186 by (Asm_full_simp_tac 1);
   187 by (eres_inst_tac [("x","aa")] allE 1);
   188 by (eres_inst_tac [("x","b")] allE 1);
   189 by (etac exE 1);
   190 by (etac exE 1);
   191 by (res_inst_tac [("x","(s2,s2a)")] exI 1);
   192 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   193 (* a~: act B*)
   194 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   195 by (eres_inst_tac [("x","a")] allE 1);
   196 by (Asm_full_simp_tac 1);
   197 by (eres_inst_tac [("x","aa")] allE 1);
   198 by (etac exE 1);
   199 by (res_inst_tac [("x","(s2,b)")] exI 1);
   200 by (Asm_full_simp_tac 1);
   201 
   202 (* a:inp B *)
   203 by (case_tac "a:act A" 1);
   204 (* a:act A *)
   205 by (eres_inst_tac [("x","a")] allE 1);
   206 by (eres_inst_tac [("x","a")] allE 1);
   207 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   208 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
   209 by (dtac inpAAactB_is_inpBoroutB 1);
   210 back();
   211 by (assume_tac 1);
   212 by (assume_tac 1);
   213 by (Asm_full_simp_tac 1);
   214 by (rotate_tac ~1 1);
   215 by (Asm_full_simp_tac 1);
   216 by (eres_inst_tac [("x","aa")] allE 1);
   217 by (eres_inst_tac [("x","b")] allE 1);
   218 by (etac exE 1);
   219 by (etac exE 1);
   220 by (res_inst_tac [("x","(s2,s2a)")] exI 1);
   221 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   222 (* a~: act B*)
   223 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   224 by (eres_inst_tac [("x","a")] allE 1);
   225 by (Asm_full_simp_tac 1);
   226 by (eres_inst_tac [("x","a")] allE 1);
   227 by (Asm_full_simp_tac 1);
   228 by (eres_inst_tac [("x","b")] allE 1);
   229 by (etac exE 1);
   230 by (res_inst_tac [("x","(aa,s2)")] exI 1);
   231 by (Asm_full_simp_tac 1);
   232 qed"input_enabled_par";
   233 
   234 (* ---------------------------------------------------------------------------------- *)
   235 
   236 section "invariants";
   237 
   238 val [p1,p2] = goalw thy [invariant_def]
   239   "[| !!s. s:starts_of(A) ==> P(s);     \
   240 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
   241 \  ==> invariant A P";
   242 by (rtac allI 1);
   243 by (rtac impI 1);
   244 by (res_inst_tac [("za","s")] reachable.induct 1);
   245 by (atac 1);
   246 by (etac p1 1);
   247 by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
   248 by (REPEAT (atac 1));
   249 qed"invariantI";
   250 
   251 
   252 val [p1,p2] = goal thy
   253  "[| !!s. s : starts_of(A) ==> P(s); \
   254 \   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
   255 \ |] ==> invariant A P";
   256   by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
   257 qed "invariantI1";
   258 
   259 val [p1,p2] = goalw thy [invariant_def]
   260 "[| invariant A P; reachable A s |] ==> P(s)";
   261    br(p2 RS (p1 RS spec RS mp))1;
   262 qed "invariantE";
   263 
   264 (* ---------------------------------------------------------------------------------- *)
   265 
   266 section "restrict";
   267 
   268 
   269 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   270 \         trans_of(restrict ioa acts) = trans_of(ioa)";
   271 by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
   272 qed "cancel_restrict_a";
   273 
   274 goal thy "reachable (restrict ioa acts) s = reachable ioa s";
   275 by (rtac iffI 1);
   276 by (etac reachable.induct 1);
   277 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1);
   278 by (etac reachable_n 1);
   279 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
   280 (* <--  *)
   281 by (etac reachable.induct 1);
   282 by (rtac reachable_0 1);
   283 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
   284 by (etac reachable_n 1);
   285 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
   286 qed "cancel_restrict_b";
   287 
   288 goal thy "act (restrict A acts) = act A";
   289 by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
   290         asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
   291         restrict_asig_def]) 1);
   292 by Auto_tac;
   293 qed"acts_restrict";
   294 
   295 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   296 \         trans_of(restrict ioa acts) = trans_of(ioa) & \
   297 \         reachable (restrict ioa acts) s = reachable ioa s & \
   298 \         act (restrict A acts) = act A";
   299   by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
   300 qed"cancel_restrict";
   301 
   302 (* ---------------------------------------------------------------------------------- *)
   303 
   304 section "rename";
   305 
   306 
   307 
   308 goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
   309 by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
   310 qed"trans_rename";
   311 
   312 
   313 goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
   314 by (etac reachable.induct 1);
   315 by (rtac reachable_0 1);
   316 by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
   317 by (dtac trans_rename 1);
   318 by (etac exE 1);
   319 by (etac conjE 1);
   320 by (etac reachable_n 1);
   321 by (assume_tac 1);
   322 qed"reachable_rename";
   323 
   324 
   325 
   326 (* ---------------------------------------------------------------------------------- *)
   327 
   328 section "trans_of(A||B)";
   329 
   330 
   331 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
   332 \             ==> (fst s,a,fst t):trans_of A";
   333 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   334 qed"trans_A_proj";
   335 
   336 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
   337 \             ==> (snd s,a,snd t):trans_of B";
   338 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   339 qed"trans_B_proj";
   340 
   341 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
   342 \             ==> fst s = fst t";
   343 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   344 qed"trans_A_proj2";
   345 
   346 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
   347 \             ==> snd s = snd t";
   348 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   349 qed"trans_B_proj2";
   350 
   351 goal thy "!!A.(s,a,t):trans_of (A||B) \
   352 \              ==> a :act A | a :act B";
   353 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   354 qed"trans_AB_proj";
   355 
   356 goal thy "!!A. [|a:act A;a:act B;\
   357 \      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
   358 \  ==> (s,a,t):trans_of (A||B)";
   359 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   360 qed"trans_AB";
   361 
   362 goal thy "!!A. [|a:act A;a~:act B;\
   363 \      (fst s,a,fst t):trans_of A;snd s=snd t|]\
   364 \  ==> (s,a,t):trans_of (A||B)";
   365 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   366 qed"trans_A_notB";
   367 
   368 goal thy "!!A. [|a~:act A;a:act B;\
   369 \      (snd s,a,snd t):trans_of B;fst s=fst t|]\
   370 \  ==> (s,a,t):trans_of (A||B)";
   371 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   372 qed"trans_notA_B";
   373 
   374 val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
   375 val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2,
   376                       trans_B_proj2,trans_AB_proj];
   377 
   378 
   379 goal thy 
   380 "(s,a,t) : trans_of(A || B || C || D) =                                      \
   381 \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
   382 \   a:actions(asig_of(D))) &                                                 \
   383 \  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
   384 \   else fst t=fst s) &                                                      \
   385 \  (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)    \
   386 \   else fst(snd(t))=fst(snd(s))) &                                          \
   387 \  (if a:actions(asig_of(C)) then                                            \
   388 \     (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                      \
   389 \   else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                \
   390 \  (if a:actions(asig_of(D)) then                                            \
   391 \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
   392 \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   393 
   394   by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
   395                             ioa_projections)
   396                   setloop (split_tac [expand_if])) 1);
   397 qed "trans_of_par4";
   398 
   399 
   400 (* ---------------------------------------------------------------------------------- *)
   401 
   402 section "proof obligation generator for IOA requirements";  
   403 
   404 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
   405 goalw thy [is_trans_of_def] 
   406 "is_trans_of (A||B)";
   407 by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1);
   408 qed"is_trans_of_par";
   409 
   410 goalw thy [is_trans_of_def] 
   411 "!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
   412 by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
   413 qed"is_trans_of_restrict";
   414 
   415 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
   416 "!!A. is_trans_of A ==> is_trans_of (rename A f)";
   417 by (asm_full_simp_tac
   418     (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
   419 			 asig_outputs_def,asig_inputs_def,externals_def,
   420 			 asig_of_def,rename_def,rename_set_def]) 1);
   421 by (Blast_tac 1);
   422 qed"is_trans_of_rename";
   423 
   424 goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
   425 \         ==> is_asig_of (A||B)";
   426 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
   427        asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
   428      asig_inputs_def,actions_def,is_asig_def]) 1);
   429 by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
   430 by Auto_tac;
   431 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   432 qed"is_asig_of_par";
   433 
   434 goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
   435            asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
   436 "!! A. is_asig_of A ==> is_asig_of (restrict A f)";
   437 by (Asm_full_simp_tac 1);
   438 by Auto_tac;
   439 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   440 qed"is_asig_of_restrict";
   441 
   442 goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
   443 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
   444      rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
   445      asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
   446 by Auto_tac; 
   447 by (dres_inst_tac [("s","Some xb")] sym 1);
   448 by (rotate_tac ~1 1);
   449 by (Asm_full_simp_tac 1);
   450 by (best_tac (set_cs addEs [equalityCE]) 1);
   451 by (dres_inst_tac [("s","Some xb")] sym 1);
   452 by (rotate_tac ~1 1);
   453 by (Asm_full_simp_tac 1);
   454 by (best_tac (set_cs addEs [equalityCE]) 1);
   455 by (dres_inst_tac [("s","Some xb")] sym 1);
   456 by (rotate_tac ~1 1);
   457 by (Asm_full_simp_tac 1);
   458 by (best_tac (set_cs addEs [equalityCE]) 1);
   459 qed"is_asig_of_rename";
   460 
   461 
   462 Addsimps [is_asig_of_par,is_asig_of_restrict,is_asig_of_rename,
   463           is_trans_of_par,is_trans_of_restrict,is_trans_of_rename];
   464 
   465 
   466 goalw thy [compatible_def]
   467 "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
   468 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   469    outputs_of_par,actions_of_par]) 1);
   470 by Auto_tac;
   471 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   472 qed"compatible_par";
   473 
   474 (* FIX: better derive by previous one and compat_commute *)
   475 goalw thy [compatible_def]
   476 "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
   477 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   478    outputs_of_par,actions_of_par]) 1);
   479 by Auto_tac;
   480 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   481 qed"compatible_par2";
   482 
   483 goalw thy [compatible_def]
   484 "!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
   485 \     ==> compatible A (restrict B S)";
   486 by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
   487           externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
   488 by (auto_tac (claset() addEs [equalityCE],simpset()));
   489 qed"compatible_restrict";
   490