19 (* ProjA2 *) |
19 (* ProjA2 *) |
20 (* ---------------------------------------------------------------- *) |
20 (* ---------------------------------------------------------------- *) |
21 |
21 |
22 |
22 |
23 goal thy "ProjA2`UU = UU"; |
23 goal thy "ProjA2`UU = UU"; |
24 by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
24 by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
25 qed"ProjA2_UU"; |
25 qed"ProjA2_UU"; |
26 |
26 |
27 goal thy "ProjA2`nil = nil"; |
27 goal thy "ProjA2`nil = nil"; |
28 by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
28 by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
29 qed"ProjA2_nil"; |
29 qed"ProjA2_nil"; |
30 |
30 |
31 goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs"; |
31 goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs"; |
32 by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
32 by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
33 qed"ProjA2_cons"; |
33 qed"ProjA2_cons"; |
34 |
34 |
35 |
35 |
36 (* ---------------------------------------------------------------- *) |
36 (* ---------------------------------------------------------------- *) |
37 (* ProjB2 *) |
37 (* ProjB2 *) |
38 (* ---------------------------------------------------------------- *) |
38 (* ---------------------------------------------------------------- *) |
39 |
39 |
40 |
40 |
41 goal thy "ProjB2`UU = UU"; |
41 goal thy "ProjB2`UU = UU"; |
42 by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
42 by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
43 qed"ProjB2_UU"; |
43 qed"ProjB2_UU"; |
44 |
44 |
45 goal thy "ProjB2`nil = nil"; |
45 goal thy "ProjB2`nil = nil"; |
46 by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
46 by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
47 qed"ProjB2_nil"; |
47 qed"ProjB2_nil"; |
48 |
48 |
49 goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs"; |
49 goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs"; |
50 by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
50 by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
51 qed"ProjB2_cons"; |
51 qed"ProjB2_cons"; |
52 |
52 |
53 |
53 |
54 |
54 |
55 (* ---------------------------------------------------------------- *) |
55 (* ---------------------------------------------------------------- *) |
56 (* Filter_ex2 *) |
56 (* Filter_ex2 *) |
57 (* ---------------------------------------------------------------- *) |
57 (* ---------------------------------------------------------------- *) |
58 |
58 |
59 |
59 |
60 goal thy "Filter_ex2 sig`UU=UU"; |
60 goal thy "Filter_ex2 sig`UU=UU"; |
61 by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
61 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
62 qed"Filter_ex2_UU"; |
62 qed"Filter_ex2_UU"; |
63 |
63 |
64 goal thy "Filter_ex2 sig`nil=nil"; |
64 goal thy "Filter_ex2 sig`nil=nil"; |
65 by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
65 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
66 qed"Filter_ex2_nil"; |
66 qed"Filter_ex2_nil"; |
67 |
67 |
68 goal thy "Filter_ex2 sig`(at >> xs) = \ |
68 goal thy "Filter_ex2 sig`(at >> xs) = \ |
69 \ (if (fst at:actions sig) \ |
69 \ (if (fst at:actions sig) \ |
70 \ then at >> (Filter_ex2 sig`xs) \ |
70 \ then at >> (Filter_ex2 sig`xs) \ |
71 \ else Filter_ex2 sig`xs)"; |
71 \ else Filter_ex2 sig`xs)"; |
72 |
72 |
73 by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
73 by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
74 qed"Filter_ex2_cons"; |
74 qed"Filter_ex2_cons"; |
75 |
75 |
76 |
76 |
77 (* ---------------------------------------------------------------- *) |
77 (* ---------------------------------------------------------------- *) |
78 (* stutter2 *) |
78 (* stutter2 *) |
108 goal thy "(stutter2 sig`(at>>xs)) s = \ |
108 goal thy "(stutter2 sig`(at>>xs)) s = \ |
109 \ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \ |
109 \ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \ |
110 \ andalso (stutter2 sig`xs) (snd at))"; |
110 \ andalso (stutter2 sig`xs) (snd at))"; |
111 br trans 1; |
111 br trans 1; |
112 by (stac stutter2_unfold 1); |
112 by (stac stutter2_unfold 1); |
113 by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1); |
113 by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1); |
114 by (Simp_tac 1); |
114 by (Simp_tac 1); |
115 qed"stutter2_cons"; |
115 qed"stutter2_cons"; |
116 |
116 |
117 |
117 |
118 Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
118 Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
121 (* ---------------------------------------------------------------- *) |
121 (* ---------------------------------------------------------------- *) |
122 (* stutter *) |
122 (* stutter *) |
123 (* ---------------------------------------------------------------- *) |
123 (* ---------------------------------------------------------------- *) |
124 |
124 |
125 goal thy "stutter sig (s, UU)"; |
125 goal thy "stutter sig (s, UU)"; |
126 by (simp_tac (!simpset addsimps [stutter_def]) 1); |
126 by (simp_tac (simpset() addsimps [stutter_def]) 1); |
127 qed"stutter_UU"; |
127 qed"stutter_UU"; |
128 |
128 |
129 goal thy "stutter sig (s, nil)"; |
129 goal thy "stutter sig (s, nil)"; |
130 by (simp_tac (!simpset addsimps [stutter_def]) 1); |
130 by (simp_tac (simpset() addsimps [stutter_def]) 1); |
131 qed"stutter_nil"; |
131 qed"stutter_nil"; |
132 |
132 |
133 goal thy "stutter sig (s, (a,t)>>ex) = \ |
133 goal thy "stutter sig (s, (a,t)>>ex) = \ |
134 \ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"; |
134 \ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"; |
135 by (simp_tac (!simpset addsimps [stutter_def] |
135 by (simp_tac (simpset() addsimps [stutter_def] |
136 setloop (split_tac [expand_if]) ) 1); |
136 setloop (split_tac [expand_if]) ) 1); |
137 qed"stutter_cons"; |
137 qed"stutter_cons"; |
138 |
138 |
139 (* ----------------------------------------------------------------------------------- *) |
139 (* ----------------------------------------------------------------------------------- *) |
140 |
140 |
181 \ stutter (asig_of B) (snd s,ProjB2`xs)"; |
181 \ stutter (asig_of B) (snd s,ProjB2`xs)"; |
182 |
182 |
183 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); |
183 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); |
184 (* main case *) |
184 (* main case *) |
185 by (safe_tac set_cs); |
185 by (safe_tac set_cs); |
186 by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 |
186 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 |
187 setloop (split_tac [expand_if])) 1)); |
187 setloop (split_tac [expand_if])) 1)); |
188 qed"lemma_1_1b"; |
188 qed"lemma_1_1b"; |
189 |
189 |
190 |
190 |
191 (* --------------------------------------------------------------------- *) |
191 (* --------------------------------------------------------------------- *) |
196 \ --> Forall (%x. fst x:act (A||B)) xs)"; |
196 \ --> Forall (%x. fst x:act (A||B)) xs)"; |
197 |
197 |
198 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1); |
198 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1); |
199 (* main case *) |
199 (* main case *) |
200 by (safe_tac set_cs); |
200 by (safe_tac set_cs); |
201 by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ |
201 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ |
202 [actions_asig_comp,asig_of_par]) 1)); |
202 [actions_asig_comp,asig_of_par]) 1)); |
203 qed"lemma_1_1c"; |
203 qed"lemma_1_1c"; |
204 |
204 |
205 |
205 |
206 (* ----------------------------------------------------------------------- *) |
206 (* ----------------------------------------------------------------------- *) |
218 by (pair_induct_tac "xs" [Forall_def,sforall_def, |
218 by (pair_induct_tac "xs" [Forall_def,sforall_def, |
219 is_exec_frag_def, stutter_def] 1); |
219 is_exec_frag_def, stutter_def] 1); |
220 (* main case *) |
220 (* main case *) |
221 by (rtac allI 1); |
221 by (rtac allI 1); |
222 ren "ss a t s" 1; |
222 ren "ss a t s" 1; |
223 by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par] |
223 by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par] |
224 setloop (split_tac [expand_if])) 1); |
224 setloop (split_tac [expand_if])) 1); |
225 by (safe_tac set_cs); |
225 by (safe_tac set_cs); |
226 (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) |
226 (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) |
227 by (rotate_tac ~4 1); |
227 by (rotate_tac ~4 1); |
228 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
228 by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1); |
229 by (rotate_tac ~4 1); |
229 by (rotate_tac ~4 1); |
230 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
230 by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1); |
231 qed"lemma_1_2"; |
231 qed"lemma_1_2"; |
232 |
232 |
233 |
233 |
234 (* ------------------------------------------------------------------ *) |
234 (* ------------------------------------------------------------------ *) |
235 (* COMPOSITIONALITY on EXECUTION Level *) |
235 (* COMPOSITIONALITY on EXECUTION Level *) |
242 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\ |
242 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\ |
243 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\ |
243 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\ |
244 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\ |
244 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\ |
245 \ Forall (%x. fst x:act (A||B)) (snd ex))"; |
245 \ Forall (%x. fst x:act (A||B)) (snd ex))"; |
246 |
246 |
247 by (simp_tac (!simpset addsimps [executions_def,ProjB_def, |
247 by (simp_tac (simpset() addsimps [executions_def,ProjB_def, |
248 Filter_ex_def,ProjA_def,starts_of_par]) 1); |
248 Filter_ex_def,ProjA_def,starts_of_par]) 1); |
249 by (pair_tac "ex" 1); |
249 by (pair_tac "ex" 1); |
250 by (rtac iffI 1); |
250 by (rtac iffI 1); |
251 (* ==> *) |
251 (* ==> *) |
252 by (REPEAT (etac conjE 1)); |
252 by (REPEAT (etac conjE 1)); |
253 by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp, |
253 by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp, |
254 lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1); |
254 lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1); |
255 (* <== *) |
255 (* <== *) |
256 by (REPEAT (etac conjE 1)); |
256 by (REPEAT (etac conjE 1)); |
257 by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1); |
257 by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1); |
258 qed"compositionality_ex"; |
258 qed"compositionality_ex"; |
259 |
259 |
260 |
260 |
261 (* ------------------------------------------------------------------ *) |
261 (* ------------------------------------------------------------------ *) |
262 (* COMPOSITIONALITY on EXECUTION Level *) |
262 (* COMPOSITIONALITY on EXECUTION Level *) |