author  oheimb 
Thu, 08 Jan 1998 18:09:47 +0100  
changeset 4536  74f7c556fd90 
parent 4477  b3e5857d8d99 
child 4814  0277a026f99d 
permissions  rwrr 
3071  1 
(* Title: HOLCF/IOA/meta_theory/Automata.ML 
3275  2 
ID: $Id$ 
3071  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 HOLsimpset, who knows why? *) 

10 
Addsimps [Let_def]; 

4536  11 
Delsimps [split_paired_Ex]; 
3071  12 

13 
open reachable; 

14 

3521  15 
val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def]; 
3071  16 

17 
(*  *) 

18 

19 
section "asig_of, starts_of, trans_of"; 

20 

21 

22 
goal thy 

3521  23 
"((asig_of (x,y,z,w,s)) = x) & \ 
24 
\ ((starts_of (x,y,z,w,s)) = y) & \ 

25 
\ ((trans_of (x,y,z,w,s)) = z) & \ 

26 
\ ((wfair_of (x,y,z,w,s)) = w) & \ 

27 
\ ((sfair_of (x,y,z,w,s)) = s)"; 

4098  28 
by (simp_tac (simpset() addsimps ioa_projections) 1); 
3071  29 
qed "ioa_triple_proj"; 
30 

3521  31 
goalw thy [is_trans_of_def,actions_def, is_asig_def] 
32 
"!!A. [ is_trans_of A; (s1,a,s2):trans_of(A) ] ==> a:act A"; 

3071  33 
by (REPEAT(etac conjE 1)); 
34 
by (EVERY1[etac allE, etac impE, atac]); 

35 
by (Asm_full_simp_tac 1); 

36 
qed "trans_in_actions"; 

37 

38 
goal thy 

39 
"starts_of(A  B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; 

4098  40 
by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); 
3071  41 
qed "starts_of_par"; 
42 

3521  43 
goal thy 
44 
"trans_of(A  B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \ 

45 
\ in (a:act A  a:act B) & \ 

46 
\ (if a:act A then \ 

47 
\ (fst(s),a,fst(t)):trans_of(A) \ 

48 
\ else fst(t) = fst(s)) \ 

49 
\ & \ 

50 
\ (if a:act B then \ 

51 
\ (snd(s),a,snd(t)):trans_of(B) \ 

52 
\ else snd(t) = snd(s))}"; 

53 

4423  54 
by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); 
3521  55 
qed "trans_of_par"; 
56 

3071  57 

58 
(*  *) 

59 

60 
section "actions and par"; 

61 

62 

63 
goal thy 

64 
"actions(asig_comp a b) = actions(a) Un actions(b)"; 

4098  65 
by (simp_tac (simpset() addsimps 
3071  66 
([actions_def,asig_comp_def]@asig_projections)) 1); 
67 
by (fast_tac (set_cs addSIs [equalityI]) 1); 

68 
qed "actions_asig_comp"; 

69 

70 

71 
goal thy "asig_of(A  B) = asig_comp (asig_of A) (asig_of B)"; 

4098  72 
by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); 
3071  73 
qed "asig_of_par"; 
74 

75 

76 
goal thy "ext (A1A2) = \ 

77 
\ (ext A1) Un (ext A2)"; 

4098  78 
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def, 
3071  79 
asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); 
80 
by (rtac set_ext 1); 

81 
by (fast_tac set_cs 1); 

82 
qed"externals_of_par"; 

83 

84 
goal thy "act (A1A2) = \ 

85 
\ (act A1) Un (act A2)"; 

4098  86 
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, 
3071  87 
asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); 
88 
by (rtac set_ext 1); 

89 
by (fast_tac set_cs 1); 

90 
qed"actions_of_par"; 

91 

92 
goal thy "inp (A1A2) =\ 

93 
\ ((inp A1) Un (inp A2))  ((out A1) Un (out A2))"; 

4098  94 
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, 
3071  95 
asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); 
96 
qed"inputs_of_par"; 

97 

98 
goal thy "out (A1A2) =\ 

99 
\ (out A1) Un (out A2)"; 

4098  100 
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, 
3071  101 
asig_outputs_def,Un_def,set_diff_def]) 1); 
102 
qed"outputs_of_par"; 

103 

3656  104 
goal thy "int (A1A2) =\ 
105 
\ (int A1) Un (int A2)"; 

4098  106 
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, 
3656  107 
asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); 
108 
qed"internals_of_par"; 

3071  109 

110 
(*  *) 

111 

112 
section "actions and compatibility"; 

113 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

114 
goal thy"compatible A B = compatible B A"; 
4098  115 
by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

116 
by Auto_tac; 
3071  117 
qed"compat_commute"; 
118 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

119 
goalw thy [externals_def,actions_def,compatible_def] 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

120 
"!! a. [ compatible A1 A2; a:ext A1] ==> a~:int A2"; 
3071  121 
by (Asm_full_simp_tac 1); 
122 
by (best_tac (set_cs addEs [equalityCE]) 1); 

123 
qed"ext1_is_not_int2"; 

124 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

125 
(* just commuting the previous one: better commute compatible *) 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

126 
goalw thy [externals_def,actions_def,compatible_def] 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

127 
"!! a. [ compatible A2 A1 ; a:ext A1] ==> a~:int A2"; 
3071  128 
by (Asm_full_simp_tac 1); 
129 
by (best_tac (set_cs addEs [equalityCE]) 1); 

130 
qed"ext2_is_not_int1"; 

131 

132 
bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act); 

133 
bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act); 

134 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

135 
goalw thy [externals_def,actions_def,compatible_def] 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

136 
"!! x. [ compatible A B; x:int A ] ==> x~:ext B"; 
3071  137 
by (Asm_full_simp_tac 1); 
138 
by (best_tac (set_cs addEs [equalityCE]) 1); 

139 
qed"intA_is_not_extB"; 

140 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

141 
goalw thy [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def] 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

142 
"!! a. [ compatible A B; a:int A ] ==> a ~: act B"; 
3071  143 
by (Asm_full_simp_tac 1); 
144 
by (best_tac (set_cs addEs [equalityCE]) 1); 

145 
qed"intA_is_not_actB"; 

146 

3521  147 
(* the only one that needs disjointness of outputs and of internals and _all_ acts *) 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

148 
goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def, 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

149 
compatible_def,is_asig_def,asig_of_def] 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

150 
"!! a. [ compatible A B; a:out A ;a:act B] ==> a : inp B"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

151 
by (Asm_full_simp_tac 1); 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

152 
by (best_tac (set_cs addEs [equalityCE]) 1); 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

153 
qed"outAactB_is_inpB"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

154 

3521  155 
(* needed for propagation of input_enabledness from A,B to AB *) 
156 
goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def, 

157 
compatible_def,is_asig_def,asig_of_def] 

158 
"!! a. [ compatible A B; a:inp A ;a:act B] ==> a : inp B  a: out B"; 

159 
by (Asm_full_simp_tac 1); 

160 
by (best_tac (set_cs addEs [equalityCE]) 1); 

161 
qed"inpAAactB_is_inpBoroutB"; 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

162 

3521  163 
(*  *) 
164 

165 
section "input_enabledness and par"; 

166 

167 

168 
(* ugly case distinctions. Heart of proof: 

169 
1. inpAAactB_is_inpBoroutB ie. internals are really hidden. 

170 
2. inputs_of_par: outputs are no longer inputs of par. This is important here *) 

171 
goalw thy [input_enabled_def] 

172 
"!!A. [ compatible A B; input_enabled A; input_enabled B] \ 

173 
\ ==> input_enabled (AB)"; 

4098  174 
by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1); 
3521  175 
by (safe_tac set_cs); 
4098  176 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
177 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2); 

3521  178 
(* a: inp A *) 
179 
by (case_tac "a:act B" 1); 

180 
(* a:act B *) 

181 
by (eres_inst_tac [("x","a")] allE 1); 

182 
by (Asm_full_simp_tac 1); 

4423  183 
by (dtac inpAAactB_is_inpBoroutB 1); 
184 
by (assume_tac 1); 

185 
by (assume_tac 1); 

3521  186 
by (eres_inst_tac [("x","a")] allE 1); 
187 
by (Asm_full_simp_tac 1); 

188 
by (eres_inst_tac [("x","aa")] allE 1); 

189 
by (eres_inst_tac [("x","b")] allE 1); 

4423  190 
by (etac exE 1); 
191 
by (etac exE 1); 

3521  192 
by (res_inst_tac [("x","(s2,s2a)")] exI 1); 
4098  193 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
3521  194 
(* a~: act B*) 
4098  195 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
3521  196 
by (eres_inst_tac [("x","a")] allE 1); 
197 
by (Asm_full_simp_tac 1); 

198 
by (eres_inst_tac [("x","aa")] allE 1); 

4423  199 
by (etac exE 1); 
3521  200 
by (res_inst_tac [("x","(s2,b)")] exI 1); 
201 
by (Asm_full_simp_tac 1); 

202 

203 
(* a:inp B *) 

204 
by (case_tac "a:act A" 1); 

205 
(* a:act A *) 

206 
by (eres_inst_tac [("x","a")] allE 1); 

207 
by (eres_inst_tac [("x","a")] allE 1); 

4098  208 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
4473  209 
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); 
4423  210 
by (dtac inpAAactB_is_inpBoroutB 1); 
3521  211 
back(); 
4423  212 
by (assume_tac 1); 
213 
by (assume_tac 1); 

3521  214 
by (Asm_full_simp_tac 1); 
215 
by (rotate_tac ~1 1); 

216 
by (Asm_full_simp_tac 1); 

217 
by (eres_inst_tac [("x","aa")] allE 1); 

218 
by (eres_inst_tac [("x","b")] allE 1); 

4423  219 
by (etac exE 1); 
220 
by (etac exE 1); 

3521  221 
by (res_inst_tac [("x","(s2,s2a)")] exI 1); 
4098  222 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
3521  223 
(* a~: act B*) 
4098  224 
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); 
3521  225 
by (eres_inst_tac [("x","a")] allE 1); 
226 
by (Asm_full_simp_tac 1); 

227 
by (eres_inst_tac [("x","a")] allE 1); 

228 
by (Asm_full_simp_tac 1); 

229 
by (eres_inst_tac [("x","b")] allE 1); 

4423  230 
by (etac exE 1); 
3521  231 
by (res_inst_tac [("x","(aa,s2)")] exI 1); 
232 
by (Asm_full_simp_tac 1); 

233 
qed"input_enabled_par"; 

3071  234 

235 
(*  *) 

236 

237 
section "invariants"; 

238 

239 
val [p1,p2] = goalw thy [invariant_def] 

240 
"[ !!s. s:starts_of(A) ==> P(s); \ 

241 
\ !!s t a. [reachable A s; P(s)] ==> (s,a,t): trans_of(A) > P(t) ] \ 

242 
\ ==> invariant A P"; 

243 
by (rtac allI 1); 

244 
by (rtac impI 1); 

245 
by (res_inst_tac [("za","s")] reachable.induct 1); 

246 
by (atac 1); 

247 
by (etac p1 1); 

248 
by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1); 

249 
by (REPEAT (atac 1)); 

250 
qed"invariantI"; 

251 

252 

253 
val [p1,p2] = goal thy 

254 
"[ !!s. s : starts_of(A) ==> P(s); \ 

255 
\ !!s t a. reachable A s ==> P(s) > (s,a,t):trans_of(A) > P(t) \ 

256 
\ ] ==> invariant A P"; 

257 
by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); 

258 
qed "invariantI1"; 

259 

260 
val [p1,p2] = goalw thy [invariant_def] 

261 
"[ invariant A P; reachable A s ] ==> P(s)"; 

262 
br(p2 RS (p1 RS spec RS mp))1; 

263 
qed "invariantE"; 

264 

265 
(*  *) 

266 

267 
section "restrict"; 

268 

269 

270 
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ 

3656  271 
\ trans_of(restrict ioa acts) = trans_of(ioa)"; 
4098  272 
by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1); 
3071  273 
qed "cancel_restrict_a"; 
274 

275 
goal thy "reachable (restrict ioa acts) s = reachable ioa s"; 

276 
by (rtac iffI 1); 

3457  277 
by (etac reachable.induct 1); 
4098  278 
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1); 
3071  279 
by (etac reachable_n 1); 
4098  280 
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); 
3071  281 
(* < *) 
3457  282 
by (etac reachable.induct 1); 
3071  283 
by (rtac reachable_0 1); 
4098  284 
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); 
3071  285 
by (etac reachable_n 1); 
4098  286 
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); 
3071  287 
qed "cancel_restrict_b"; 
288 

3656  289 
goal thy "act (restrict A acts) = act A"; 
4098  290 
by (simp_tac (simpset() addsimps [actions_def,asig_internals_def, 
3656  291 
asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def, 
292 
restrict_asig_def]) 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

293 
by Auto_tac; 
3656  294 
qed"acts_restrict"; 
295 

3071  296 
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ 
3656  297 
\ trans_of(restrict ioa acts) = trans_of(ioa) & \ 
298 
\ reachable (restrict ioa acts) s = reachable ioa s & \ 

299 
\ act (restrict A acts) = act A"; 

4098  300 
by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1); 
3071  301 
qed"cancel_restrict"; 
302 

303 
(*  *) 

304 

305 
section "rename"; 

306 

307 

308 

309 
goal thy "!!f. s a(rename C f)> t ==> (? x. Some(x) = f(a) & s xC> t)"; 

4098  310 
by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1); 
3071  311 
qed"trans_rename"; 
312 

313 

314 
goal thy "!!s.[ reachable (rename C g) s ] ==> reachable C s"; 

3457  315 
by (etac reachable.induct 1); 
316 
by (rtac reachable_0 1); 

4098  317 
by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1); 
3457  318 
by (dtac trans_rename 1); 
319 
by (etac exE 1); 

320 
by (etac conjE 1); 

321 
by (etac reachable_n 1); 

322 
by (assume_tac 1); 

3071  323 
qed"reachable_rename"; 
324 

325 

326 

327 
(*  *) 

328 

329 
section "trans_of(AB)"; 

330 

331 

332 
goal thy "!!A.[(s,a,t):trans_of (AB); a:act A] \ 

333 
\ ==> (fst s,a,fst t):trans_of A"; 

4098  334 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  335 
qed"trans_A_proj"; 
336 

337 
goal thy "!!A.[(s,a,t):trans_of (AB); a:act B] \ 

338 
\ ==> (snd s,a,snd t):trans_of B"; 

4098  339 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  340 
qed"trans_B_proj"; 
341 

342 
goal thy "!!A.[(s,a,t):trans_of (AB); a~:act A]\ 

343 
\ ==> fst s = fst t"; 

4098  344 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  345 
qed"trans_A_proj2"; 
346 

347 
goal thy "!!A.[(s,a,t):trans_of (AB); a~:act B]\ 

348 
\ ==> snd s = snd t"; 

4098  349 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  350 
qed"trans_B_proj2"; 
351 

352 
goal thy "!!A.(s,a,t):trans_of (AB) \ 

353 
\ ==> a :act A  a :act B"; 

4098  354 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  355 
qed"trans_AB_proj"; 
356 

357 
goal thy "!!A. [a:act A;a:act B;\ 

358 
\ (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B]\ 

359 
\ ==> (s,a,t):trans_of (AB)"; 

4098  360 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  361 
qed"trans_AB"; 
362 

363 
goal thy "!!A. [a:act A;a~:act B;\ 

364 
\ (fst s,a,fst t):trans_of A;snd s=snd t]\ 

365 
\ ==> (s,a,t):trans_of (AB)"; 

4098  366 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  367 
qed"trans_A_notB"; 
368 

369 
goal thy "!!A. [a~:act A;a:act B;\ 

370 
\ (snd s,a,snd t):trans_of B;fst s=fst t]\ 

371 
\ ==> (s,a,t):trans_of (AB)"; 

4098  372 
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); 
3071  373 
qed"trans_notA_B"; 
374 

375 
val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B]; 

376 
val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2, 

377 
trans_B_proj2,trans_AB_proj]; 

378 

379 

380 
goal thy 

381 
"(s,a,t) : trans_of(A  B  C  D) = \ 

382 
\ ((a:actions(asig_of(A))  a:actions(asig_of(B))  a:actions(asig_of(C))  \ 

383 
\ a:actions(asig_of(D))) & \ 

384 
\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \ 

385 
\ else fst t=fst s) & \ 

386 
\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \ 

387 
\ else fst(snd(t))=fst(snd(s))) & \ 

388 
\ (if a:actions(asig_of(C)) then \ 

389 
\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ 

390 
\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ 

391 
\ (if a:actions(asig_of(D)) then \ 

392 
\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ 

393 
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; 

394 

4098  395 
by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@ 
3071  396 
ioa_projections) 
397 
setloop (split_tac [expand_if])) 1); 

398 
qed "trans_of_par4"; 

399 

400 

3521  401 
(*  *) 
3071  402 

3521  403 
section "proof obligation generator for IOA requirements"; 
404 

405 
(* without assumptions on A and B because is_trans_of is also incorporated in def *) 

406 
goalw thy [is_trans_of_def] 

407 
"is_trans_of (AB)"; 

4098  408 
by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1); 
3521  409 
qed"is_trans_of_par"; 
410 

3656  411 
goalw thy [is_trans_of_def] 
3521  412 
"!!A. is_trans_of A ==> is_trans_of (restrict A acts)"; 
4098  413 
by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1); 
3656  414 
qed"is_trans_of_restrict"; 
3521  415 

416 
goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 

417 
"!!A. is_trans_of A ==> is_trans_of (rename A f)"; 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

418 
by (asm_full_simp_tac 
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

419 
(simpset() addsimps [actions_def,trans_of_def, asig_internals_def, 
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

420 
asig_outputs_def,asig_inputs_def,externals_def, 
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

421 
asig_of_def,rename_def,rename_set_def]) 1); 
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

422 
by (Blast_tac 1); 
3656  423 
qed"is_trans_of_rename"; 
3521  424 

425 
goal thy "!! A. [ is_asig_of A; is_asig_of B; compatible A B] \ 

426 
\ ==> is_asig_of (AB)"; 

4098  427 
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par, 
3656  428 
asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def, 
429 
asig_inputs_def,actions_def,is_asig_def]) 1); 

4098  430 
by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

431 
by Auto_tac; 
3656  432 
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); 
433 
qed"is_asig_of_par"; 

3521  434 

3656  435 
goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def, 
436 
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 

437 
"!! A. is_asig_of A ==> is_asig_of (restrict A f)"; 

438 
by (Asm_full_simp_tac 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

439 
by Auto_tac; 
3656  440 
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); 
441 
qed"is_asig_of_restrict"; 

3521  442 

3656  443 
goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)"; 
4098  444 
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def, 
3656  445 
rename_def,rename_set_def,asig_internals_def,asig_outputs_def, 
446 
asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

447 
by Auto_tac; 
3656  448 
by (dres_inst_tac [("s","Some xb")] sym 1); 
449 
by (rotate_tac ~1 1); 

450 
by (Asm_full_simp_tac 1); 

451 
by (best_tac (set_cs addEs [equalityCE]) 1); 

452 
by (dres_inst_tac [("s","Some xb")] sym 1); 

453 
by (rotate_tac ~1 1); 

454 
by (Asm_full_simp_tac 1); 

455 
by (best_tac (set_cs addEs [equalityCE]) 1); 

456 
by (dres_inst_tac [("s","Some xb")] sym 1); 

457 
by (rotate_tac ~1 1); 

458 
by (Asm_full_simp_tac 1); 

459 
by (best_tac (set_cs addEs [equalityCE]) 1); 

460 
qed"is_asig_of_rename"; 

3521  461 

462 

3656  463 
Addsimps [is_asig_of_par,is_asig_of_restrict,is_asig_of_rename, 
464 
is_trans_of_par,is_trans_of_restrict,is_trans_of_rename]; 

3521  465 

466 

3656  467 
goalw thy [compatible_def] 
468 
"!! A. [compatible A B; compatible A C ]==> compatible A (BC)"; 

4098  469 
by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
3656  470 
outputs_of_par,actions_of_par]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

471 
by Auto_tac; 
3656  472 
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); 
473 
qed"compatible_par"; 

3521  474 

3656  475 
(* FIX: better derive by previous one and compat_commute *) 
476 
goalw thy [compatible_def] 

477 
"!! A. [compatible A C; compatible B C ]==> compatible (AB) C"; 

4098  478 
by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
3656  479 
outputs_of_par,actions_of_par]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset

480 
by Auto_tac; 
3656  481 
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); 
482 
qed"compatible_par2"; 

3521  483 

3656  484 
goalw thy [compatible_def] 
485 
"!! A. [ compatible A B; (ext B  S) Int ext A = {}] \ 

486 
\ ==> compatible A (restrict B S)"; 

4098  487 
by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj, 
3656  488 
externals_def,restrict_def,restrict_asig_def,actions_def]) 1); 
4098  489 
by (auto_tac (claset() addEs [equalityCE],simpset())); 
3656  490 
qed"compatible_restrict"; 
491 