22 "((asig_of (x,y,z,w,s)) = x) & \ |
22 "((asig_of (x,y,z,w,s)) = x) & \ |
23 \ ((starts_of (x,y,z,w,s)) = y) & \ |
23 \ ((starts_of (x,y,z,w,s)) = y) & \ |
24 \ ((trans_of (x,y,z,w,s)) = z) & \ |
24 \ ((trans_of (x,y,z,w,s)) = z) & \ |
25 \ ((wfair_of (x,y,z,w,s)) = w) & \ |
25 \ ((wfair_of (x,y,z,w,s)) = w) & \ |
26 \ ((sfair_of (x,y,z,w,s)) = s)"; |
26 \ ((sfair_of (x,y,z,w,s)) = s)"; |
27 by (simp_tac (!simpset addsimps ioa_projections) 1); |
27 by (simp_tac (simpset() addsimps ioa_projections) 1); |
28 qed "ioa_triple_proj"; |
28 qed "ioa_triple_proj"; |
29 |
29 |
30 goalw thy [is_trans_of_def,actions_def, is_asig_def] |
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"; |
31 "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A"; |
32 by (REPEAT(etac conjE 1)); |
32 by (REPEAT(etac conjE 1)); |
48 \ & \ |
48 \ & \ |
49 \ (if a:act B then \ |
49 \ (if a:act B then \ |
50 \ (snd(s),a,snd(t)):trans_of(B) \ |
50 \ (snd(s),a,snd(t)):trans_of(B) \ |
51 \ else snd(t) = snd(s))}"; |
51 \ else snd(t) = snd(s))}"; |
52 |
52 |
53 by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
53 by(simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); |
54 qed "trans_of_par"; |
54 qed "trans_of_par"; |
55 |
55 |
56 |
56 |
57 (* ----------------------------------------------------------------------------------- *) |
57 (* ----------------------------------------------------------------------------------- *) |
58 |
58 |
59 section "actions and par"; |
59 section "actions and par"; |
60 |
60 |
61 |
61 |
62 goal thy |
62 goal thy |
63 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
63 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
64 by (simp_tac (!simpset addsimps |
64 by (simp_tac (simpset() addsimps |
65 ([actions_def,asig_comp_def]@asig_projections)) 1); |
65 ([actions_def,asig_comp_def]@asig_projections)) 1); |
66 by (fast_tac (set_cs addSIs [equalityI]) 1); |
66 by (fast_tac (set_cs addSIs [equalityI]) 1); |
67 qed "actions_asig_comp"; |
67 qed "actions_asig_comp"; |
68 |
68 |
69 |
69 |
70 goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; |
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); |
71 by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); |
72 qed "asig_of_par"; |
72 qed "asig_of_par"; |
73 |
73 |
74 |
74 |
75 goal thy "ext (A1||A2) = \ |
75 goal thy "ext (A1||A2) = \ |
76 \ (ext A1) Un (ext A2)"; |
76 \ (ext A1) Un (ext A2)"; |
77 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def, |
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); |
78 asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); |
79 by (rtac set_ext 1); |
79 by (rtac set_ext 1); |
80 by (fast_tac set_cs 1); |
80 by (fast_tac set_cs 1); |
81 qed"externals_of_par"; |
81 qed"externals_of_par"; |
82 |
82 |
83 goal thy "act (A1||A2) = \ |
83 goal thy "act (A1||A2) = \ |
84 \ (act A1) Un (act A2)"; |
84 \ (act A1) Un (act A2)"; |
85 by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, |
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); |
86 asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); |
87 by (rtac set_ext 1); |
87 by (rtac set_ext 1); |
88 by (fast_tac set_cs 1); |
88 by (fast_tac set_cs 1); |
89 qed"actions_of_par"; |
89 qed"actions_of_par"; |
90 |
90 |
91 goal thy "inp (A1||A2) =\ |
91 goal thy "inp (A1||A2) =\ |
92 \ ((inp A1) Un (inp A2)) - ((out A1) Un (out 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, |
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); |
94 asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); |
95 qed"inputs_of_par"; |
95 qed"inputs_of_par"; |
96 |
96 |
97 goal thy "out (A1||A2) =\ |
97 goal thy "out (A1||A2) =\ |
98 \ (out A1) Un (out A2)"; |
98 \ (out A1) Un (out A2)"; |
99 by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, |
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); |
100 asig_outputs_def,Un_def,set_diff_def]) 1); |
101 qed"outputs_of_par"; |
101 qed"outputs_of_par"; |
102 |
102 |
103 goal thy "int (A1||A2) =\ |
103 goal thy "int (A1||A2) =\ |
104 \ (int A1) Un (int A2)"; |
104 \ (int A1) Un (int A2)"; |
105 by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, |
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); |
106 asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); |
107 qed"internals_of_par"; |
107 qed"internals_of_par"; |
108 |
108 |
109 (* ---------------------------------------------------------------------------------- *) |
109 (* ---------------------------------------------------------------------------------- *) |
110 |
110 |
111 section "actions and compatibility"; |
111 section "actions and compatibility"; |
112 |
112 |
113 goal thy"compatible A B = compatible B A"; |
113 goal thy"compatible A B = compatible B A"; |
114 by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1); |
114 by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1); |
115 by (Auto_tac()); |
115 by (Auto_tac()); |
116 qed"compat_commute"; |
116 qed"compat_commute"; |
117 |
117 |
118 goalw thy [externals_def,actions_def,compatible_def] |
118 goalw thy [externals_def,actions_def,compatible_def] |
119 "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2"; |
119 "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2"; |
168 1. inpAAactB_is_inpBoroutB ie. internals are really hidden. |
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 *) |
169 2. inputs_of_par: outputs are no longer inputs of par. This is important here *) |
170 goalw thy [input_enabled_def] |
170 goalw thy [input_enabled_def] |
171 "!!A. [| compatible A B; input_enabled A; input_enabled B|] \ |
171 "!!A. [| compatible A B; input_enabled A; input_enabled B|] \ |
172 \ ==> input_enabled (A||B)"; |
172 \ ==> input_enabled (A||B)"; |
173 by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1); |
173 by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1); |
174 by (safe_tac set_cs); |
174 by (safe_tac set_cs); |
175 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
175 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); |
176 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2); |
176 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2); |
177 (* a: inp A *) |
177 (* a: inp A *) |
178 by (case_tac "a:act B" 1); |
178 by (case_tac "a:act B" 1); |
179 (* a:act B *) |
179 (* a:act B *) |
180 by (eres_inst_tac [("x","a")] allE 1); |
180 by (eres_inst_tac [("x","a")] allE 1); |
181 by (Asm_full_simp_tac 1); |
181 by (Asm_full_simp_tac 1); |
187 by (eres_inst_tac [("x","aa")] allE 1); |
187 by (eres_inst_tac [("x","aa")] allE 1); |
188 by (eres_inst_tac [("x","b")] allE 1); |
188 by (eres_inst_tac [("x","b")] allE 1); |
189 be exE 1; |
189 be exE 1; |
190 be exE 1; |
190 be exE 1; |
191 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
191 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
192 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
192 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); |
193 (* a~: act B*) |
193 (* a~: act B*) |
194 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
194 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); |
195 by (eres_inst_tac [("x","a")] allE 1); |
195 by (eres_inst_tac [("x","a")] allE 1); |
196 by (Asm_full_simp_tac 1); |
196 by (Asm_full_simp_tac 1); |
197 by (eres_inst_tac [("x","aa")] allE 1); |
197 by (eres_inst_tac [("x","aa")] allE 1); |
198 be exE 1; |
198 be exE 1; |
199 by (res_inst_tac [("x","(s2,b)")] exI 1); |
199 by (res_inst_tac [("x","(s2,b)")] exI 1); |
216 by (eres_inst_tac [("x","aa")] allE 1); |
216 by (eres_inst_tac [("x","aa")] allE 1); |
217 by (eres_inst_tac [("x","b")] allE 1); |
217 by (eres_inst_tac [("x","b")] allE 1); |
218 be exE 1; |
218 be exE 1; |
219 be exE 1; |
219 be exE 1; |
220 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
220 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
221 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
221 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); |
222 (* a~: act B*) |
222 (* a~: act B*) |
223 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
223 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); |
224 by (eres_inst_tac [("x","a")] allE 1); |
224 by (eres_inst_tac [("x","a")] allE 1); |
225 by (Asm_full_simp_tac 1); |
225 by (Asm_full_simp_tac 1); |
226 by (eres_inst_tac [("x","a")] allE 1); |
226 by (eres_inst_tac [("x","a")] allE 1); |
227 by (Asm_full_simp_tac 1); |
227 by (Asm_full_simp_tac 1); |
228 by (eres_inst_tac [("x","b")] allE 1); |
228 by (eres_inst_tac [("x","b")] allE 1); |
266 section "restrict"; |
266 section "restrict"; |
267 |
267 |
268 |
268 |
269 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
269 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
270 \ trans_of(restrict ioa acts) = trans_of(ioa)"; |
270 \ trans_of(restrict ioa acts) = trans_of(ioa)"; |
271 by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1); |
271 by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1); |
272 qed "cancel_restrict_a"; |
272 qed "cancel_restrict_a"; |
273 |
273 |
274 goal thy "reachable (restrict ioa acts) s = reachable ioa s"; |
274 goal thy "reachable (restrict ioa acts) s = reachable ioa s"; |
275 by (rtac iffI 1); |
275 by (rtac iffI 1); |
276 by (etac reachable.induct 1); |
276 by (etac reachable.induct 1); |
277 by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1); |
277 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1); |
278 by (etac reachable_n 1); |
278 by (etac reachable_n 1); |
279 by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); |
279 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); |
280 (* <-- *) |
280 (* <-- *) |
281 by (etac reachable.induct 1); |
281 by (etac reachable.induct 1); |
282 by (rtac reachable_0 1); |
282 by (rtac reachable_0 1); |
283 by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); |
283 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); |
284 by (etac reachable_n 1); |
284 by (etac reachable_n 1); |
285 by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); |
285 by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1); |
286 qed "cancel_restrict_b"; |
286 qed "cancel_restrict_b"; |
287 |
287 |
288 goal thy "act (restrict A acts) = act A"; |
288 goal thy "act (restrict A acts) = act A"; |
289 by (simp_tac (!simpset addsimps [actions_def,asig_internals_def, |
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, |
290 asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def, |
291 restrict_asig_def]) 1); |
291 restrict_asig_def]) 1); |
292 auto(); |
292 auto(); |
293 qed"acts_restrict"; |
293 qed"acts_restrict"; |
294 |
294 |
295 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
295 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
296 \ trans_of(restrict ioa acts) = trans_of(ioa) & \ |
296 \ trans_of(restrict ioa acts) = trans_of(ioa) & \ |
297 \ reachable (restrict ioa acts) s = reachable ioa s & \ |
297 \ reachable (restrict ioa acts) s = reachable ioa s & \ |
298 \ act (restrict A acts) = act A"; |
298 \ act (restrict A acts) = act A"; |
299 by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1); |
299 by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1); |
300 qed"cancel_restrict"; |
300 qed"cancel_restrict"; |
301 |
301 |
302 (* ---------------------------------------------------------------------------------- *) |
302 (* ---------------------------------------------------------------------------------- *) |
303 |
303 |
304 section "rename"; |
304 section "rename"; |
305 |
305 |
306 |
306 |
307 |
307 |
308 goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)"; |
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); |
309 by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1); |
310 qed"trans_rename"; |
310 qed"trans_rename"; |
311 |
311 |
312 |
312 |
313 goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; |
313 goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; |
314 by (etac reachable.induct 1); |
314 by (etac reachable.induct 1); |
315 by (rtac reachable_0 1); |
315 by (rtac reachable_0 1); |
316 by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1); |
316 by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1); |
317 by (dtac trans_rename 1); |
317 by (dtac trans_rename 1); |
318 by (etac exE 1); |
318 by (etac exE 1); |
319 by (etac conjE 1); |
319 by (etac conjE 1); |
320 by (etac reachable_n 1); |
320 by (etac reachable_n 1); |
321 by (assume_tac 1); |
321 by (assume_tac 1); |
328 section "trans_of(A||B)"; |
328 section "trans_of(A||B)"; |
329 |
329 |
330 |
330 |
331 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \ |
331 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \ |
332 \ ==> (fst s,a,fst t):trans_of 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); |
333 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
334 qed"trans_A_proj"; |
334 qed"trans_A_proj"; |
335 |
335 |
336 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \ |
336 goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \ |
337 \ ==> (snd s,a,snd t):trans_of 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); |
338 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
339 qed"trans_B_proj"; |
339 qed"trans_B_proj"; |
340 |
340 |
341 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\ |
341 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\ |
342 \ ==> fst s = fst t"; |
342 \ ==> fst s = fst t"; |
343 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
343 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
344 qed"trans_A_proj2"; |
344 qed"trans_A_proj2"; |
345 |
345 |
346 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\ |
346 goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\ |
347 \ ==> snd s = snd t"; |
347 \ ==> snd s = snd t"; |
348 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
348 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
349 qed"trans_B_proj2"; |
349 qed"trans_B_proj2"; |
350 |
350 |
351 goal thy "!!A.(s,a,t):trans_of (A||B) \ |
351 goal thy "!!A.(s,a,t):trans_of (A||B) \ |
352 \ ==> a :act A | a :act B"; |
352 \ ==> a :act A | a :act B"; |
353 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
353 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
354 qed"trans_AB_proj"; |
354 qed"trans_AB_proj"; |
355 |
355 |
356 goal thy "!!A. [|a:act A;a:act B;\ |
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|]\ |
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)"; |
358 \ ==> (s,a,t):trans_of (A||B)"; |
359 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
359 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
360 qed"trans_AB"; |
360 qed"trans_AB"; |
361 |
361 |
362 goal thy "!!A. [|a:act A;a~:act B;\ |
362 goal thy "!!A. [|a:act A;a~:act B;\ |
363 \ (fst s,a,fst t):trans_of A;snd s=snd t|]\ |
363 \ (fst s,a,fst t):trans_of A;snd s=snd t|]\ |
364 \ ==> (s,a,t):trans_of (A||B)"; |
364 \ ==> (s,a,t):trans_of (A||B)"; |
365 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
365 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
366 qed"trans_A_notB"; |
366 qed"trans_A_notB"; |
367 |
367 |
368 goal thy "!!A. [|a~:act A;a:act B;\ |
368 goal thy "!!A. [|a~:act A;a:act B;\ |
369 \ (snd s,a,snd t):trans_of B;fst s=fst t|]\ |
369 \ (snd s,a,snd t):trans_of B;fst s=fst t|]\ |
370 \ ==> (s,a,t):trans_of (A||B)"; |
370 \ ==> (s,a,t):trans_of (A||B)"; |
371 by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); |
371 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1); |
372 qed"trans_notA_B"; |
372 qed"trans_notA_B"; |
373 |
373 |
374 val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B]; |
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, |
375 val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2, |
376 trans_B_proj2,trans_AB_proj]; |
376 trans_B_proj2,trans_AB_proj]; |
402 section "proof obligation generator for IOA requirements"; |
402 section "proof obligation generator for IOA requirements"; |
403 |
403 |
404 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *) |
404 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *) |
405 goalw thy [is_trans_of_def] |
405 goalw thy [is_trans_of_def] |
406 "is_trans_of (A||B)"; |
406 "is_trans_of (A||B)"; |
407 by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1); |
407 by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1); |
408 qed"is_trans_of_par"; |
408 qed"is_trans_of_par"; |
409 |
409 |
410 goalw thy [is_trans_of_def] |
410 goalw thy [is_trans_of_def] |
411 "!!A. is_trans_of A ==> is_trans_of (restrict A acts)"; |
411 "!!A. is_trans_of A ==> is_trans_of (restrict A acts)"; |
412 by (asm_simp_tac (!simpset addsimps [cancel_restrict,acts_restrict])1); |
412 by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1); |
413 qed"is_trans_of_restrict"; |
413 qed"is_trans_of_restrict"; |
414 |
414 |
415 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] |
415 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] |
416 "!!A. is_trans_of A ==> is_trans_of (rename A f)"; |
416 "!!A. is_trans_of A ==> is_trans_of (rename A f)"; |
417 by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def, |
417 by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def, |
418 asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def, |
418 asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def, |
419 asig_of_def,rename_def,rename_set_def]) 1); |
419 asig_of_def,rename_def,rename_set_def]) 1); |
420 auto(); |
420 auto(); |
421 qed"is_trans_of_rename"; |
421 qed"is_trans_of_rename"; |
422 |
422 |
423 goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \ |
423 goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \ |
424 \ ==> is_asig_of (A||B)"; |
424 \ ==> is_asig_of (A||B)"; |
425 by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,asig_of_par, |
425 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par, |
426 asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def, |
426 asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def, |
427 asig_inputs_def,actions_def,is_asig_def]) 1); |
427 asig_inputs_def,actions_def,is_asig_def]) 1); |
428 by (asm_full_simp_tac (!simpset addsimps [asig_of_def]) 1); |
428 by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1); |
429 auto(); |
429 auto(); |
430 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
430 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
431 qed"is_asig_of_par"; |
431 qed"is_asig_of_par"; |
432 |
432 |
433 goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def, |
433 goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def, |
437 auto(); |
437 auto(); |
438 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
438 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
439 qed"is_asig_of_restrict"; |
439 qed"is_asig_of_restrict"; |
440 |
440 |
441 goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)"; |
441 goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)"; |
442 by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def, |
442 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def, |
443 rename_def,rename_set_def,asig_internals_def,asig_outputs_def, |
443 rename_def,rename_set_def,asig_internals_def,asig_outputs_def, |
444 asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1); |
444 asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1); |
445 auto(); |
445 auto(); |
446 by (dres_inst_tac [("s","Some xb")] sym 1); |
446 by (dres_inst_tac [("s","Some xb")] sym 1); |
447 by (rotate_tac ~1 1); |
447 by (rotate_tac ~1 1); |
462 is_trans_of_par,is_trans_of_restrict,is_trans_of_rename]; |
462 is_trans_of_par,is_trans_of_restrict,is_trans_of_rename]; |
463 |
463 |
464 |
464 |
465 goalw thy [compatible_def] |
465 goalw thy [compatible_def] |
466 "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)"; |
466 "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)"; |
467 by (asm_full_simp_tac (!simpset addsimps [internals_of_par, |
467 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, |
468 outputs_of_par,actions_of_par]) 1); |
468 outputs_of_par,actions_of_par]) 1); |
469 auto(); |
469 auto(); |
470 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
470 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
471 qed"compatible_par"; |
471 qed"compatible_par"; |
472 |
472 |
473 (* FIX: better derive by previous one and compat_commute *) |
473 (* FIX: better derive by previous one and compat_commute *) |
474 goalw thy [compatible_def] |
474 goalw thy [compatible_def] |
475 "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C"; |
475 "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C"; |
476 by (asm_full_simp_tac (!simpset addsimps [internals_of_par, |
476 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, |
477 outputs_of_par,actions_of_par]) 1); |
477 outputs_of_par,actions_of_par]) 1); |
478 auto(); |
478 auto(); |
479 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
479 by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1)); |
480 qed"compatible_par2"; |
480 qed"compatible_par2"; |
481 |
481 |
482 goalw thy [compatible_def] |
482 goalw thy [compatible_def] |
483 "!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \ |
483 "!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \ |
484 \ ==> compatible A (restrict B S)"; |
484 \ ==> compatible A (restrict B S)"; |
485 by (asm_full_simp_tac (!simpset addsimps [ioa_triple_proj,asig_triple_proj, |
485 by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj, |
486 externals_def,restrict_def,restrict_asig_def,actions_def]) 1); |
486 externals_def,restrict_def,restrict_asig_def,actions_def]) 1); |
487 by (auto_tac (!claset addEs [equalityCE],!simpset)); |
487 by (auto_tac (claset() addEs [equalityCE],simpset())); |
488 qed"compatible_restrict"; |
488 qed"compatible_restrict"; |
489 |
489 |