9 (* Has been removed from HOL-simpset, who knows why? *) |
9 (* Has been removed from HOL-simpset, who knows why? *) |
10 Addsimps [Let_def]; |
10 Addsimps [Let_def]; |
11 |
11 |
12 open reachable; |
12 open reachable; |
13 |
13 |
14 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def]; |
14 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def]; |
15 |
15 |
16 (* ----------------------------------------------------------------------------------- *) |
16 (* ----------------------------------------------------------------------------------- *) |
17 |
17 |
18 section "asig_of, starts_of, trans_of"; |
18 section "asig_of, starts_of, trans_of"; |
19 |
19 |
20 |
20 |
21 goal thy |
21 goal thy |
22 "asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; |
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)"; |
23 by (simp_tac (!simpset addsimps ioa_projections) 1); |
27 by (simp_tac (!simpset addsimps ioa_projections) 1); |
24 qed "ioa_triple_proj"; |
28 qed "ioa_triple_proj"; |
25 |
29 |
26 goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def] |
30 goalw thy [is_trans_of_def,actions_def, is_asig_def] |
27 "!!A. [| IOA(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"; |
28 by (REPEAT(etac conjE 1)); |
32 by (REPEAT(etac conjE 1)); |
29 by (EVERY1[etac allE, etac impE, atac]); |
33 by (EVERY1[etac allE, etac impE, atac]); |
30 by (Asm_full_simp_tac 1); |
34 by (Asm_full_simp_tac 1); |
31 qed "trans_in_actions"; |
35 qed "trans_in_actions"; |
32 |
36 |
33 goal thy |
37 goal thy |
34 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
38 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
35 by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
39 by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
36 qed "starts_of_par"; |
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"; |
37 |
55 |
38 |
56 |
39 (* ----------------------------------------------------------------------------------- *) |
57 (* ----------------------------------------------------------------------------------- *) |
40 |
58 |
41 section "actions and par"; |
59 section "actions and par"; |
67 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, |
68 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); |
69 by (rtac set_ext 1); |
87 by (rtac set_ext 1); |
70 by (fast_tac set_cs 1); |
88 by (fast_tac set_cs 1); |
71 qed"actions_of_par"; |
89 qed"actions_of_par"; |
72 |
|
73 |
90 |
74 goal thy "inp (A1||A2) =\ |
91 goal thy "inp (A1||A2) =\ |
75 \ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"; |
92 \ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"; |
76 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, |
77 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); |
119 "!! a. [| compatible A B; a:int A |] ==> a ~: act B"; |
136 "!! a. [| compatible A B; a:int A |] ==> a ~: act B"; |
120 by (Asm_full_simp_tac 1); |
137 by (Asm_full_simp_tac 1); |
121 by (best_tac (set_cs addEs [equalityCE]) 1); |
138 by (best_tac (set_cs addEs [equalityCE]) 1); |
122 qed"intA_is_not_actB"; |
139 qed"intA_is_not_actB"; |
123 |
140 |
|
141 (* the only one that needs disjointness of outputs and of internals and _all_ acts *) |
124 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def, |
142 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def, |
125 compatible_def,is_asig_def,asig_of_def] |
143 compatible_def,is_asig_def,asig_of_def] |
126 "!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B"; |
144 "!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B"; |
127 by (Asm_full_simp_tac 1); |
145 by (Asm_full_simp_tac 1); |
128 by (best_tac (set_cs addEs [equalityCE]) 1); |
146 by (best_tac (set_cs addEs [equalityCE]) 1); |
129 qed"outAactB_is_inpB"; |
147 qed"outAactB_is_inpB"; |
130 |
148 |
131 |
149 (* needed for propagation of input_enabledness from A,B to A||B *) |
|
150 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def, |
|
151 compatible_def,is_asig_def,asig_of_def] |
|
152 "!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"; |
|
153 by (Asm_full_simp_tac 1); |
|
154 by (best_tac (set_cs addEs [equalityCE]) 1); |
|
155 qed"inpAAactB_is_inpBoroutB"; |
|
156 |
|
157 (* ---------------------------------------------------------------------------------- *) |
|
158 |
|
159 section "input_enabledness and par"; |
|
160 |
|
161 |
|
162 (* ugly case distinctions. Heart of proof: |
|
163 1. inpAAactB_is_inpBoroutB ie. internals are really hidden. |
|
164 2. inputs_of_par: outputs are no longer inputs of par. This is important here *) |
|
165 goalw thy [input_enabled_def] |
|
166 "!!A. [| compatible A B; input_enabled A; input_enabled B|] \ |
|
167 \ ==> input_enabled (A||B)"; |
|
168 by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1); |
|
169 by (safe_tac set_cs); |
|
170 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
171 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2); |
|
172 (* a: inp A *) |
|
173 by (case_tac "a:act B" 1); |
|
174 (* a:act B *) |
|
175 by (eres_inst_tac [("x","a")] allE 1); |
|
176 by (Asm_full_simp_tac 1); |
|
177 bd inpAAactB_is_inpBoroutB 1; |
|
178 ba 1; |
|
179 ba 1; |
|
180 by (eres_inst_tac [("x","a")] allE 1); |
|
181 by (Asm_full_simp_tac 1); |
|
182 by (eres_inst_tac [("x","aa")] allE 1); |
|
183 by (eres_inst_tac [("x","b")] allE 1); |
|
184 be exE 1; |
|
185 be exE 1; |
|
186 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
|
187 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
188 (* a~: act B*) |
|
189 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
190 by (eres_inst_tac [("x","a")] allE 1); |
|
191 by (Asm_full_simp_tac 1); |
|
192 by (eres_inst_tac [("x","aa")] allE 1); |
|
193 be exE 1; |
|
194 by (res_inst_tac [("x","(s2,b)")] exI 1); |
|
195 by (Asm_full_simp_tac 1); |
|
196 |
|
197 (* a:inp B *) |
|
198 by (case_tac "a:act A" 1); |
|
199 (* a:act A *) |
|
200 by (eres_inst_tac [("x","a")] allE 1); |
|
201 by (eres_inst_tac [("x","a")] allE 1); |
|
202 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
203 by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1); |
|
204 bd inpAAactB_is_inpBoroutB 1; |
|
205 back(); |
|
206 ba 1; |
|
207 ba 1; |
|
208 by (Asm_full_simp_tac 1); |
|
209 by (rotate_tac ~1 1); |
|
210 by (Asm_full_simp_tac 1); |
|
211 by (eres_inst_tac [("x","aa")] allE 1); |
|
212 by (eres_inst_tac [("x","b")] allE 1); |
|
213 be exE 1; |
|
214 be exE 1; |
|
215 by (res_inst_tac [("x","(s2,s2a)")] exI 1); |
|
216 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
217 (* a~: act B*) |
|
218 by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1); |
|
219 by (eres_inst_tac [("x","a")] allE 1); |
|
220 by (Asm_full_simp_tac 1); |
|
221 by (eres_inst_tac [("x","a")] allE 1); |
|
222 by (Asm_full_simp_tac 1); |
|
223 by (eres_inst_tac [("x","b")] allE 1); |
|
224 be exE 1; |
|
225 by (res_inst_tac [("x","(aa,s2)")] exI 1); |
|
226 by (Asm_full_simp_tac 1); |
|
227 qed"input_enabled_par"; |
132 |
228 |
133 (* ---------------------------------------------------------------------------------- *) |
229 (* ---------------------------------------------------------------------------------- *) |
134 |
230 |
135 section "invariants"; |
231 section "invariants"; |
136 |
232 |
286 ioa_projections) |
382 ioa_projections) |
287 setloop (split_tac [expand_if])) 1); |
383 setloop (split_tac [expand_if])) 1); |
288 qed "trans_of_par4"; |
384 qed "trans_of_par4"; |
289 |
385 |
290 |
386 |
291 |
387 (* ---------------------------------------------------------------------------------- *) |
|
388 |
|
389 section "proof obligation generator for IOA requirements"; |
|
390 |
|
391 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *) |
|
392 goalw thy [is_trans_of_def] |
|
393 "is_trans_of (A||B)"; |
|
394 by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1); |
|
395 qed"is_trans_of_par"; |
|
396 |
|
397 |
|
398 (* |
|
399 |
|
400 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] |
|
401 "!!A. is_trans_of A ==> is_trans_of (restrict A acts)"; |
|
402 by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def, |
|
403 asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1); |
|
404 |
|
405 qed""; |
|
406 |
|
407 |
|
408 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] |
|
409 "!!A. is_trans_of A ==> is_trans_of (rename A f)"; |
|
410 by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def, |
|
411 asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1); |
|
412 |
|
413 qed""; |
|
414 |
|
415 goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)"; |
|
416 |
|
417 |
|
418 goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def, |
|
419 asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def] |
|
420 "!! A. is_asig_of A ==> is_asig_of (restrict A f)"; |
|
421 by (Asm_full_simp_tac 1); |
|
422 |
|
423 |
|
424 |
|
425 |
|
426 goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \ |
|
427 \ ==> is_asig_of (A||B)"; |
|
428 |
|
429 |
|
430 |
|
431 |
|
432 |
|
433 *) |
|
434 |
|
435 |
|
436 |
|
437 |
|
438 |