author | wenzelm |
Fri, 10 Oct 1997 19:02:28 +0200 | |
changeset 3842 | b55686a7b22c |
parent 3521 | bdc51b4c6050 |
child 4098 | 71e05eb27fb6 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Compositionality on Execution level. |
|
7 |
*) |
|
8 |
||
9 |
Delsimps (ex_simps @ all_simps); |
|
10 |
Delsimps [split_paired_All]; |
|
11 |
||
12 |
(* ----------------------------------------------------------------------------------- *) |
|
13 |
||
14 |
||
15 |
section "recursive equations of operators"; |
|
16 |
||
17 |
||
18 |
(* ---------------------------------------------------------------- *) |
|
19 |
(* ProjA2 *) |
|
20 |
(* ---------------------------------------------------------------- *) |
|
21 |
||
22 |
||
23 |
goal thy "ProjA2`UU = UU"; |
|
24 |
by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
|
25 |
qed"ProjA2_UU"; |
|
26 |
||
27 |
goal thy "ProjA2`nil = nil"; |
|
28 |
by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
|
29 |
qed"ProjA2_nil"; |
|
30 |
||
31 |
goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs"; |
|
32 |
by (simp_tac (!simpset addsimps [ProjA2_def]) 1); |
|
33 |
qed"ProjA2_cons"; |
|
34 |
||
35 |
||
36 |
(* ---------------------------------------------------------------- *) |
|
37 |
(* ProjB2 *) |
|
38 |
(* ---------------------------------------------------------------- *) |
|
39 |
||
40 |
||
41 |
goal thy "ProjB2`UU = UU"; |
|
42 |
by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
|
43 |
qed"ProjB2_UU"; |
|
44 |
||
45 |
goal thy "ProjB2`nil = nil"; |
|
46 |
by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
|
47 |
qed"ProjB2_nil"; |
|
48 |
||
49 |
goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs"; |
|
50 |
by (simp_tac (!simpset addsimps [ProjB2_def]) 1); |
|
51 |
qed"ProjB2_cons"; |
|
52 |
||
53 |
||
54 |
||
55 |
(* ---------------------------------------------------------------- *) |
|
56 |
(* Filter_ex2 *) |
|
57 |
(* ---------------------------------------------------------------- *) |
|
58 |
||
59 |
||
3521 | 60 |
goal thy "Filter_ex2 sig`UU=UU"; |
3071 | 61 |
by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
62 |
qed"Filter_ex2_UU"; |
|
63 |
||
3521 | 64 |
goal thy "Filter_ex2 sig`nil=nil"; |
3071 | 65 |
by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
66 |
qed"Filter_ex2_nil"; |
|
67 |
||
3521 | 68 |
goal thy "Filter_ex2 sig`(at >> xs) = \ |
69 |
\ (if (fst at:actions sig) \ |
|
70 |
\ then at >> (Filter_ex2 sig`xs) \ |
|
71 |
\ else Filter_ex2 sig`xs)"; |
|
3071 | 72 |
|
73 |
by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1); |
|
74 |
qed"Filter_ex2_cons"; |
|
75 |
||
76 |
||
77 |
(* ---------------------------------------------------------------- *) |
|
78 |
(* stutter2 *) |
|
79 |
(* ---------------------------------------------------------------- *) |
|
80 |
||
81 |
||
3521 | 82 |
goal thy "stutter2 sig = (LAM ex. (%s. case ex of \ |
3071 | 83 |
\ nil => TT \ |
84 |
\ | x##xs => (flift1 \ |
|
3521 | 85 |
\ (%p.(If Def ((fst p)~:actions sig) \ |
3071 | 86 |
\ then Def (s=(snd p)) \ |
87 |
\ else TT fi) \ |
|
3521 | 88 |
\ andalso (stutter2 sig`xs) (snd p)) \ |
3071 | 89 |
\ `x) \ |
90 |
\ ))"; |
|
91 |
by (rtac trans 1); |
|
3457 | 92 |
by (rtac fix_eq2 1); |
93 |
by (rtac stutter2_def 1); |
|
94 |
by (rtac beta_cfun 1); |
|
3071 | 95 |
by (simp_tac (!simpset addsimps [flift1_def]) 1); |
96 |
qed"stutter2_unfold"; |
|
97 |
||
3521 | 98 |
goal thy "(stutter2 sig`UU) s=UU"; |
3071 | 99 |
by (stac stutter2_unfold 1); |
100 |
by (Simp_tac 1); |
|
101 |
qed"stutter2_UU"; |
|
102 |
||
3521 | 103 |
goal thy "(stutter2 sig`nil) s = TT"; |
3071 | 104 |
by (stac stutter2_unfold 1); |
105 |
by (Simp_tac 1); |
|
106 |
qed"stutter2_nil"; |
|
107 |
||
3521 | 108 |
goal thy "(stutter2 sig`(at>>xs)) s = \ |
109 |
\ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \ |
|
110 |
\ andalso (stutter2 sig`xs) (snd at))"; |
|
111 |
br trans 1; |
|
3071 | 112 |
by (stac stutter2_unfold 1); |
113 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1); |
|
114 |
by (Simp_tac 1); |
|
115 |
qed"stutter2_cons"; |
|
116 |
||
117 |
||
118 |
Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
|
119 |
||
120 |
||
121 |
(* ---------------------------------------------------------------- *) |
|
122 |
(* stutter *) |
|
123 |
(* ---------------------------------------------------------------- *) |
|
124 |
||
3521 | 125 |
goal thy "stutter sig (s, UU)"; |
3071 | 126 |
by (simp_tac (!simpset addsimps [stutter_def]) 1); |
127 |
qed"stutter_UU"; |
|
128 |
||
3521 | 129 |
goal thy "stutter sig (s, nil)"; |
3071 | 130 |
by (simp_tac (!simpset addsimps [stutter_def]) 1); |
131 |
qed"stutter_nil"; |
|
132 |
||
3521 | 133 |
goal thy "stutter sig (s, (a,t)>>ex) = \ |
134 |
\ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"; |
|
3071 | 135 |
by (simp_tac (!simpset addsimps [stutter_def] |
136 |
setloop (split_tac [expand_if]) ) 1); |
|
137 |
qed"stutter_cons"; |
|
138 |
||
139 |
(* ----------------------------------------------------------------------------------- *) |
|
140 |
||
141 |
Delsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
|
142 |
||
143 |
val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons, |
|
144 |
ProjB2_UU,ProjB2_nil,ProjB2_cons, |
|
145 |
Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons, |
|
146 |
stutter_UU,stutter_nil,stutter_cons]; |
|
147 |
||
148 |
Addsimps compoex_simps; |
|
149 |
||
150 |
||
151 |
||
152 |
(* ------------------------------------------------------------------ *) |
|
153 |
(* The following lemmata aim for *) |
|
154 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
155 |
(* ------------------------------------------------------------------ *) |
|
156 |
||
157 |
||
158 |
(* --------------------------------------------------------------------- *) |
|
159 |
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) |
|
160 |
(* --------------------------------------------------------------------- *) |
|
161 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
162 |
goal thy "!s. is_exec_frag (A||B) (s,xs) \ |
3521 | 163 |
\ --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\ |
164 |
\ is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))"; |
|
3071 | 165 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
166 |
by (pair_induct_tac "xs" [is_exec_frag_def] 1); |
3071 | 167 |
(* main case *) |
168 |
ren "ss a t" 1; |
|
169 |
by (safe_tac set_cs); |
|
170 |
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 |
|
171 |
setloop (split_tac [expand_if])) 1)); |
|
172 |
qed"lemma_1_1a"; |
|
173 |
||
174 |
||
175 |
(* --------------------------------------------------------------------- *) |
|
176 |
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) |
|
177 |
(* --------------------------------------------------------------------- *) |
|
178 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
179 |
goal thy "!s. is_exec_frag (A||B) (s,xs) \ |
3521 | 180 |
\ --> stutter (asig_of A) (fst s,ProjA2`xs) &\ |
181 |
\ stutter (asig_of B) (snd s,ProjB2`xs)"; |
|
3071 | 182 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
183 |
by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); |
3071 | 184 |
(* main case *) |
185 |
by (safe_tac set_cs); |
|
186 |
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 |
|
187 |
setloop (split_tac [expand_if])) 1)); |
|
188 |
qed"lemma_1_1b"; |
|
189 |
||
190 |
||
191 |
(* --------------------------------------------------------------------- *) |
|
192 |
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) |
|
193 |
(* --------------------------------------------------------------------- *) |
|
194 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
195 |
goal thy "!s. (is_exec_frag (A||B) (s,xs) \ |
3842 | 196 |
\ --> Forall (%x. fst x:act (A||B)) xs)"; |
3071 | 197 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
198 |
by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1); |
3071 | 199 |
(* main case *) |
200 |
by (safe_tac set_cs); |
|
201 |
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ |
|
202 |
[actions_asig_comp,asig_of_par]) 1)); |
|
203 |
qed"lemma_1_1c"; |
|
204 |
||
205 |
||
206 |
(* ----------------------------------------------------------------------- *) |
|
207 |
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) |
|
208 |
(* ----------------------------------------------------------------------- *) |
|
209 |
||
210 |
goal thy |
|
3521 | 211 |
"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\ |
212 |
\ is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\ |
|
213 |
\ stutter (asig_of A) (fst s,(ProjA2`xs)) & \ |
|
214 |
\ stutter (asig_of B) (snd s,(ProjB2`xs)) & \ |
|
3842 | 215 |
\ Forall (%x. fst x:act (A||B)) xs \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
216 |
\ --> is_exec_frag (A||B) (s,xs)"; |
3071 | 217 |
|
218 |
by (pair_induct_tac "xs" [Forall_def,sforall_def, |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
219 |
is_exec_frag_def, stutter_def] 1); |
3071 | 220 |
(* main case *) |
221 |
by (rtac allI 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] |
|
224 |
setloop (split_tac [expand_if])) 1); |
|
225 |
by (safe_tac set_cs); |
|
226 |
(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) |
|
227 |
by (rotate_tac ~4 1); |
|
228 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
229 |
by (rotate_tac ~4 1); |
|
230 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
231 |
qed"lemma_1_2"; |
|
232 |
||
233 |
||
234 |
(* ------------------------------------------------------------------ *) |
|
235 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
236 |
(* Main Theorem *) |
|
237 |
(* ------------------------------------------------------------------ *) |
|
238 |
||
239 |
||
240 |
goal thy |
|
241 |
"ex:executions(A||B) =\ |
|
3521 | 242 |
\(Filter_ex (asig_of A) (ProjA ex) : executions A &\ |
243 |
\ Filter_ex (asig_of B) (ProjB ex) : executions B &\ |
|
244 |
\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\ |
|
3842 | 245 |
\ Forall (%x. fst x:act (A||B)) (snd ex))"; |
3071 | 246 |
|
247 |
by (simp_tac (!simpset addsimps [executions_def,ProjB_def, |
|
248 |
Filter_ex_def,ProjA_def,starts_of_par]) 1); |
|
249 |
by (pair_tac "ex" 1); |
|
250 |
by (rtac iffI 1); |
|
251 |
(* ==> *) |
|
252 |
by (REPEAT (etac conjE 1)); |
|
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); |
|
255 |
(* <== *) |
|
256 |
by (REPEAT (etac conjE 1)); |
|
257 |
by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1); |
|
258 |
qed"compositionality_ex"; |
|
259 |
||
260 |
||
3521 | 261 |
(* ------------------------------------------------------------------ *) |
262 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
263 |
(* For Modules *) |
|
264 |
(* ------------------------------------------------------------------ *) |
|
265 |
||
266 |
goalw thy [Execs_def,par_execs_def] |
|
267 |
||
268 |
"Execs (A||B) = par_execs (Execs A) (Execs B)"; |
|
269 |
||
270 |
by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1); |
|
271 |
br set_ext 1; |
|
272 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex,actions_of_par]) 1); |
|
273 |
qed"compositionality_ex_modules"; |
|
3071 | 274 |
|
275 |
||
3521 | 276 |
|
277 |
||
278 |
||
279 |
||
280 |