3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
|
3275
|
2 |
ID: $Id$
|
12218
|
3 |
Author: Olaf Müller
|
3071
|
4 |
*)
|
|
5 |
|
17233
|
6 |
header {* Compositionality on Trace level *}
|
|
7 |
|
|
8 |
theory CompoTraces
|
|
9 |
imports CompoScheds ShortExecutions
|
|
10 |
begin
|
3071
|
11 |
|
|
12 |
|
|
13 |
consts
|
|
14 |
|
3521
|
15 |
mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
|
|
16 |
par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
|
3071
|
17 |
|
|
18 |
defs
|
|
19 |
|
17233
|
20 |
mksch_def:
|
10835
|
21 |
"mksch A B == (fix$(LAM h tr schA schB. case tr of
|
3071
|
22 |
nil => nil
|
|
23 |
| x##xs =>
|
|
24 |
(case x of
|
12028
|
25 |
UU => UU
|
3071
|
26 |
| Def y =>
|
|
27 |
(if y:act A then
|
|
28 |
(if y:act B then
|
10835
|
29 |
((Takewhile (%a. a:int A)$schA)
|
|
30 |
@@ (Takewhile (%a. a:int B)$schB)
|
|
31 |
@@ (y>>(h$xs
|
|
32 |
$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
33 |
$(TL$(Dropwhile (%a. a:int B)$schB))
|
3071
|
34 |
)))
|
|
35 |
else
|
10835
|
36 |
((Takewhile (%a. a:int A)$schA)
|
|
37 |
@@ (y>>(h$xs
|
|
38 |
$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
39 |
$schB)))
|
3071
|
40 |
)
|
|
41 |
else
|
|
42 |
(if y:act B then
|
10835
|
43 |
((Takewhile (%a. a:int B)$schB)
|
|
44 |
@@ (y>>(h$xs
|
|
45 |
$schA
|
|
46 |
$(TL$(Dropwhile (%a. a:int B)$schB))
|
3071
|
47 |
)))
|
|
48 |
else
|
|
49 |
UU
|
|
50 |
)
|
|
51 |
)
|
|
52 |
)))"
|
|
53 |
|
|
54 |
|
17233
|
55 |
par_traces_def:
|
3521
|
56 |
"par_traces TracesA TracesB ==
|
|
57 |
let trA = fst TracesA; sigA = snd TracesA;
|
|
58 |
trB = fst TracesB; sigB = snd TracesB
|
|
59 |
in
|
10835
|
60 |
( {tr. Filter (%a. a:actions sigA)$tr : trA}
|
|
61 |
Int {tr. Filter (%a. a:actions sigB)$tr : trB}
|
3521
|
62 |
Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
|
|
63 |
asig_comp sigA sigB)"
|
|
64 |
|
17233
|
65 |
axioms
|
3071
|
66 |
|
17233
|
67 |
finiteR_mksch:
|
10835
|
68 |
"Finite (mksch A B$tr$x$y) --> Finite tr"
|
3071
|
69 |
|
19741
|
70 |
|
|
71 |
ML_setup {* change_simpset (fn ss => ss setmksym (K NONE)) *}
|
|
72 |
|
|
73 |
|
|
74 |
subsection "mksch rewrite rules"
|
|
75 |
|
|
76 |
lemma mksch_unfold:
|
|
77 |
"mksch A B = (LAM tr schA schB. case tr of
|
|
78 |
nil => nil
|
|
79 |
| x##xs =>
|
|
80 |
(case x of
|
|
81 |
UU => UU
|
|
82 |
| Def y =>
|
|
83 |
(if y:act A then
|
|
84 |
(if y:act B then
|
|
85 |
((Takewhile (%a. a:int A)$schA)
|
|
86 |
@@(Takewhile (%a. a:int B)$schB)
|
|
87 |
@@(y>>(mksch A B$xs
|
|
88 |
$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
89 |
$(TL$(Dropwhile (%a. a:int B)$schB))
|
|
90 |
)))
|
|
91 |
else
|
|
92 |
((Takewhile (%a. a:int A)$schA)
|
|
93 |
@@ (y>>(mksch A B$xs
|
|
94 |
$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
95 |
$schB)))
|
|
96 |
)
|
|
97 |
else
|
|
98 |
(if y:act B then
|
|
99 |
((Takewhile (%a. a:int B)$schB)
|
|
100 |
@@ (y>>(mksch A B$xs
|
|
101 |
$schA
|
|
102 |
$(TL$(Dropwhile (%a. a:int B)$schB))
|
|
103 |
)))
|
|
104 |
else
|
|
105 |
UU
|
|
106 |
)
|
|
107 |
)
|
|
108 |
))"
|
|
109 |
apply (rule trans)
|
|
110 |
apply (rule fix_eq2)
|
|
111 |
apply (rule mksch_def)
|
|
112 |
apply (rule beta_cfun)
|
|
113 |
apply simp
|
|
114 |
done
|
|
115 |
|
|
116 |
lemma mksch_UU: "mksch A B$UU$schA$schB = UU"
|
|
117 |
apply (subst mksch_unfold)
|
|
118 |
apply simp
|
|
119 |
done
|
|
120 |
|
|
121 |
lemma mksch_nil: "mksch A B$nil$schA$schB = nil"
|
|
122 |
apply (subst mksch_unfold)
|
|
123 |
apply simp
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma mksch_cons1: "[|x:act A;x~:act B|]
|
|
127 |
==> mksch A B$(x>>tr)$schA$schB =
|
|
128 |
(Takewhile (%a. a:int A)$schA)
|
|
129 |
@@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
130 |
$schB))"
|
|
131 |
apply (rule trans)
|
|
132 |
apply (subst mksch_unfold)
|
|
133 |
apply (simp add: Consq_def If_and_if)
|
|
134 |
apply (simp add: Consq_def)
|
|
135 |
done
|
|
136 |
|
|
137 |
lemma mksch_cons2: "[|x~:act A;x:act B|]
|
|
138 |
==> mksch A B$(x>>tr)$schA$schB =
|
|
139 |
(Takewhile (%a. a:int B)$schB)
|
|
140 |
@@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
|
|
141 |
))"
|
|
142 |
apply (rule trans)
|
|
143 |
apply (subst mksch_unfold)
|
|
144 |
apply (simp add: Consq_def If_and_if)
|
|
145 |
apply (simp add: Consq_def)
|
|
146 |
done
|
|
147 |
|
|
148 |
lemma mksch_cons3: "[|x:act A;x:act B|]
|
|
149 |
==> mksch A B$(x>>tr)$schA$schB =
|
|
150 |
(Takewhile (%a. a:int A)$schA)
|
|
151 |
@@ ((Takewhile (%a. a:int B)$schB)
|
|
152 |
@@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
|
|
153 |
$(TL$(Dropwhile (%a. a:int B)$schB))))
|
|
154 |
)"
|
|
155 |
apply (rule trans)
|
|
156 |
apply (subst mksch_unfold)
|
|
157 |
apply (simp add: Consq_def If_and_if)
|
|
158 |
apply (simp add: Consq_def)
|
|
159 |
done
|
|
160 |
|
|
161 |
lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3
|
|
162 |
|
|
163 |
declare compotr_simps [simp]
|
|
164 |
|
|
165 |
|
|
166 |
subsection {* COMPOSITIONALITY on TRACE Level *}
|
|
167 |
|
|
168 |
subsubsection "Lemmata for ==>"
|
|
169 |
|
|
170 |
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
|
|
171 |
the compatibility of IOA, in particular out of the condition that internals are
|
|
172 |
really hidden. *)
|
|
173 |
|
|
174 |
lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->
|
|
175 |
(A & (eA | eB)) = (eA & A)"
|
|
176 |
apply fast
|
|
177 |
done
|
|
178 |
|
|
179 |
|
|
180 |
(* very similar to above, only the commutativity of | is used to make a slight change *)
|
|
181 |
|
|
182 |
lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->
|
|
183 |
(A & (eB | eA)) = (eA & A)"
|
|
184 |
apply fast
|
|
185 |
done
|
|
186 |
|
|
187 |
|
|
188 |
subsubsection "Lemmata for <=="
|
|
189 |
|
|
190 |
(* Lemma for substitution of looping assumption in another specific assumption *)
|
|
191 |
lemma subst_lemma1: "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"
|
|
192 |
by (erule subst)
|
|
193 |
|
|
194 |
(* Lemma for substitution of looping assumption in another specific assumption *)
|
|
195 |
lemma subst_lemma2: "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"
|
|
196 |
by (erule subst)
|
|
197 |
|
|
198 |
lemma ForallAorB_mksch [rule_format]:
|
|
199 |
"!!A B. compatible A B ==>
|
|
200 |
! schA schB. Forall (%x. x:act (A||B)) tr
|
|
201 |
--> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
|
|
202 |
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
|
|
203 |
apply (tactic "safe_tac set_cs")
|
|
204 |
apply (simp add: actions_of_par)
|
|
205 |
apply (case_tac "a:act A")
|
|
206 |
apply (case_tac "a:act B")
|
|
207 |
(* a:A, a:B *)
|
|
208 |
apply simp
|
|
209 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
210 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
211 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
212 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
213 |
(* a:A,a~:B *)
|
|
214 |
apply simp
|
|
215 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
216 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
217 |
apply (case_tac "a:act B")
|
|
218 |
(* a~:A, a:B *)
|
|
219 |
apply simp
|
|
220 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
221 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
222 |
(* a~:A,a~:B *)
|
|
223 |
apply auto
|
|
224 |
done
|
|
225 |
|
|
226 |
lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
|
|
227 |
! schA schB. (Forall (%x. x:act B & x~:act A) tr
|
|
228 |
--> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
|
|
229 |
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
|
|
230 |
apply (tactic "safe_tac set_cs")
|
|
231 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
232 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
233 |
done
|
|
234 |
|
|
235 |
lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
|
|
236 |
! schA schB. (Forall (%x. x:act A & x~:act B) tr
|
|
237 |
--> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
|
|
238 |
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
|
|
239 |
apply (tactic "safe_tac set_cs")
|
|
240 |
apply simp
|
|
241 |
apply (rule Forall_Conc_impl [THEN mp])
|
|
242 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
|
|
243 |
done
|
|
244 |
|
|
245 |
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
|
|
246 |
declare FiniteConc [simp del]
|
|
247 |
|
|
248 |
lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>
|
|
249 |
! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &
|
|
250 |
Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &
|
|
251 |
Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &
|
|
252 |
Forall (%x. x:ext (A||B)) tr
|
|
253 |
--> Finite (mksch A B$tr$x$y)"
|
|
254 |
|
|
255 |
apply (erule Seq_Finite_ind)
|
|
256 |
apply simp
|
|
257 |
(* main case *)
|
|
258 |
apply simp
|
|
259 |
apply (tactic "safe_tac set_cs")
|
|
260 |
|
|
261 |
(* a: act A; a: act B *)
|
|
262 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
263 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
264 |
back
|
|
265 |
apply (erule conjE)+
|
|
266 |
(* Finite (tw iA x) and Finite (tw iB y) *)
|
|
267 |
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
|
|
268 |
(* now for conclusion IH applicable, but assumptions have to be transformed *)
|
|
269 |
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
|
|
270 |
apply assumption
|
|
271 |
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
|
|
272 |
apply assumption
|
|
273 |
(* IH *)
|
|
274 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
275 |
|
|
276 |
(* a: act B; a~: act A *)
|
|
277 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
278 |
|
|
279 |
apply (erule conjE)+
|
|
280 |
(* Finite (tw iB y) *)
|
|
281 |
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
|
|
282 |
(* now for conclusion IH applicable, but assumptions have to be transformed *)
|
|
283 |
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
|
|
284 |
apply assumption
|
|
285 |
(* IH *)
|
|
286 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
287 |
|
|
288 |
(* a~: act B; a: act A *)
|
|
289 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
290 |
|
|
291 |
apply (erule conjE)+
|
|
292 |
(* Finite (tw iA x) *)
|
|
293 |
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
|
|
294 |
(* now for conclusion IH applicable, but assumptions have to be transformed *)
|
|
295 |
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
|
|
296 |
apply assumption
|
|
297 |
(* IH *)
|
|
298 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
299 |
|
|
300 |
(* a~: act B; a~: act A *)
|
|
301 |
apply (fastsimp intro!: ext_is_act simp: externals_of_par)
|
|
302 |
done
|
|
303 |
|
|
304 |
declare FiniteConc [simp]
|
|
305 |
|
|
306 |
declare FilterConc [simp del]
|
|
307 |
|
|
308 |
lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
|
|
309 |
! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &
|
|
310 |
Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)
|
|
311 |
--> (? y1 y2. (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &
|
|
312 |
Forall (%x. x:act B & x~:act A) y1 &
|
|
313 |
Finite y1 & y = (y1 @@ y2) &
|
|
314 |
Filter (%a. a:ext B)$y1 = bs)"
|
|
315 |
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
|
|
316 |
apply (erule Seq_Finite_ind)
|
|
317 |
apply (rule allI)+
|
|
318 |
apply (rule impI)
|
|
319 |
apply (rule_tac x = "nil" in exI)
|
|
320 |
apply (rule_tac x = "y" in exI)
|
|
321 |
apply simp
|
|
322 |
(* main case *)
|
|
323 |
apply (rule allI)+
|
|
324 |
apply (rule impI)
|
|
325 |
apply simp
|
|
326 |
apply (erule conjE)+
|
|
327 |
apply simp
|
|
328 |
(* divide_Seq on s *)
|
|
329 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
330 |
apply (erule conjE)+
|
|
331 |
(* transform assumption f eB y = f B (s@z) *)
|
|
332 |
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
|
|
333 |
apply assumption
|
|
334 |
apply (simp add: not_ext_is_int_or_not_act FilterConc)
|
|
335 |
(* apply IH *)
|
|
336 |
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
|
|
337 |
apply (simp add: ForallTL ForallDropwhile FilterConc)
|
|
338 |
apply (erule exE)+
|
|
339 |
apply (erule conjE)+
|
|
340 |
apply (simp add: FilterConc)
|
|
341 |
(* for replacing IH in conclusion *)
|
|
342 |
apply (rotate_tac -2)
|
|
343 |
(* instantiate y1a and y2a *)
|
|
344 |
apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
|
|
345 |
apply (rule_tac x = "y2" in exI)
|
|
346 |
(* elminate all obligations up to two depending on Conc_assoc *)
|
|
347 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
|
|
348 |
apply (simp (no_asm) add: Conc_assoc FilterConc)
|
|
349 |
done
|
|
350 |
|
|
351 |
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
|
|
352 |
|
|
353 |
declare FilterConc [simp del]
|
|
354 |
|
|
355 |
lemma reduceB_mksch1 [rule_format]:
|
|
356 |
" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
|
|
357 |
! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &
|
|
358 |
Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)
|
|
359 |
--> (? x1 x2. (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &
|
|
360 |
Forall (%x. x:act A & x~:act B) x1 &
|
|
361 |
Finite x1 & x = (x1 @@ x2) &
|
|
362 |
Filter (%a. a:ext A)$x1 = a_s)"
|
|
363 |
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
|
|
364 |
apply (erule Seq_Finite_ind)
|
|
365 |
apply (rule allI)+
|
|
366 |
apply (rule impI)
|
|
367 |
apply (rule_tac x = "nil" in exI)
|
|
368 |
apply (rule_tac x = "x" in exI)
|
|
369 |
apply simp
|
|
370 |
(* main case *)
|
|
371 |
apply (rule allI)+
|
|
372 |
apply (rule impI)
|
|
373 |
apply simp
|
|
374 |
apply (erule conjE)+
|
|
375 |
apply simp
|
|
376 |
(* divide_Seq on s *)
|
|
377 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
378 |
apply (erule conjE)+
|
|
379 |
(* transform assumption f eA x = f A (s@z) *)
|
|
380 |
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
|
|
381 |
apply assumption
|
|
382 |
apply (simp add: not_ext_is_int_or_not_act FilterConc)
|
|
383 |
(* apply IH *)
|
|
384 |
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
|
|
385 |
apply (simp add: ForallTL ForallDropwhile FilterConc)
|
|
386 |
apply (erule exE)+
|
|
387 |
apply (erule conjE)+
|
|
388 |
apply (simp add: FilterConc)
|
|
389 |
(* for replacing IH in conclusion *)
|
|
390 |
apply (rotate_tac -2)
|
|
391 |
(* instantiate y1a and y2a *)
|
|
392 |
apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
|
|
393 |
apply (rule_tac x = "x2" in exI)
|
|
394 |
(* elminate all obligations up to two depending on Conc_assoc *)
|
|
395 |
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
|
|
396 |
apply (simp (no_asm) add: Conc_assoc FilterConc)
|
|
397 |
done
|
|
398 |
|
|
399 |
lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]
|
|
400 |
|
|
401 |
declare FilterConc [simp]
|
|
402 |
|
|
403 |
|
|
404 |
subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
|
|
405 |
|
|
406 |
lemma FilterA_mksch_is_tr:
|
|
407 |
"!! A B. [| compatible A B; compatible B A;
|
|
408 |
is_asig(asig_of A); is_asig(asig_of B) |] ==>
|
|
409 |
! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
|
|
410 |
Forall (%x. x:ext (A||B)) tr &
|
|
411 |
Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &
|
|
412 |
Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
|
|
413 |
--> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
|
|
414 |
|
|
415 |
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
|
|
416 |
(* main case *)
|
|
417 |
(* splitting into 4 cases according to a:A, a:B *)
|
|
418 |
apply (tactic "safe_tac set_cs")
|
|
419 |
|
|
420 |
(* Case a:A, a:B *)
|
|
421 |
apply (frule divide_Seq)
|
|
422 |
apply (frule divide_Seq)
|
|
423 |
back
|
|
424 |
apply (erule conjE)+
|
|
425 |
(* filtering internals of A in schA and of B in schB is nil *)
|
|
426 |
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
|
|
427 |
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
|
|
428 |
apply (drule_tac x = "schA" in subst_lemma1)
|
|
429 |
apply assumption
|
|
430 |
apply (drule_tac x = "schB" in subst_lemma1)
|
|
431 |
apply assumption
|
|
432 |
(* IH *)
|
|
433 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
434 |
|
|
435 |
(* Case a:A, a~:B *)
|
|
436 |
apply (frule divide_Seq)
|
|
437 |
apply (erule conjE)+
|
|
438 |
(* filtering internals of A is nil *)
|
|
439 |
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
|
|
440 |
apply (drule_tac x = "schA" in subst_lemma1)
|
|
441 |
apply assumption
|
|
442 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
443 |
|
|
444 |
(* Case a:B, a~:A *)
|
|
445 |
apply (frule divide_Seq)
|
|
446 |
apply (erule conjE)+
|
|
447 |
(* filtering internals of A is nil *)
|
|
448 |
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
|
|
449 |
apply (drule_tac x = "schB" in subst_lemma1)
|
|
450 |
back
|
|
451 |
apply assumption
|
|
452 |
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
|
|
453 |
|
|
454 |
(* Case a~:A, a~:B *)
|
|
455 |
apply (fastsimp intro!: ext_is_act simp: externals_of_par)
|
|
456 |
done
|
|
457 |
|
|
458 |
|
|
459 |
subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
|
|
460 |
|
|
461 |
lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;
|
|
462 |
is_asig(asig_of A); is_asig(asig_of B) |] ==>
|
|
463 |
Forall (%x. x:ext (A||B)) tr &
|
|
464 |
Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
|
|
465 |
Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
|
|
466 |
Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
|
|
467 |
LastActExtsch A schA & LastActExtsch B schB
|
|
468 |
--> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
|
|
469 |
apply (intro strip)
|
|
470 |
apply (rule seq.take_lemmas)
|
|
471 |
apply (rule mp)
|
|
472 |
prefer 2 apply assumption
|
|
473 |
back back back back
|
|
474 |
apply (rule_tac x = "schA" in spec)
|
|
475 |
apply (rule_tac x = "schB" in spec)
|
|
476 |
apply (rule_tac x = "tr" in spec)
|
|
477 |
apply (tactic "thin_tac' 5 1")
|
|
478 |
apply (rule nat_less_induct)
|
|
479 |
apply (rule allI)+
|
|
480 |
apply (rename_tac tr schB schA)
|
|
481 |
apply (intro strip)
|
|
482 |
apply (erule conjE)+
|
|
483 |
|
|
484 |
apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
|
|
485 |
|
|
486 |
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
|
|
487 |
apply (tactic "thin_tac' 5 1")
|
|
488 |
|
|
489 |
|
|
490 |
apply (case_tac "Finite tr")
|
|
491 |
|
|
492 |
(* both sides of this equation are nil *)
|
|
493 |
apply (subgoal_tac "schA=nil")
|
|
494 |
apply (simp (no_asm_simp))
|
|
495 |
(* first side: mksch = nil *)
|
|
496 |
apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
|
|
497 |
(* second side: schA = nil *)
|
|
498 |
apply (erule_tac A = "A" in LastActExtimplnil)
|
|
499 |
apply (simp (no_asm_simp))
|
|
500 |
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
|
|
501 |
apply assumption
|
|
502 |
apply fast
|
|
503 |
|
|
504 |
(* case ~ Finite s *)
|
|
505 |
|
|
506 |
(* both sides of this equation are UU *)
|
|
507 |
apply (subgoal_tac "schA=UU")
|
|
508 |
apply (simp (no_asm_simp))
|
|
509 |
(* first side: mksch = UU *)
|
|
510 |
apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]
|
|
511 |
(* schA = UU *)
|
|
512 |
apply (erule_tac A = "A" in LastActExtimplUU)
|
|
513 |
apply (simp (no_asm_simp))
|
|
514 |
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
|
|
515 |
apply assumption
|
|
516 |
apply fast
|
|
517 |
|
|
518 |
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
|
|
519 |
|
|
520 |
apply (drule divide_Seq3)
|
|
521 |
|
|
522 |
apply (erule exE)+
|
|
523 |
apply (erule conjE)+
|
|
524 |
apply hypsubst
|
|
525 |
|
|
526 |
(* bring in lemma reduceA_mksch *)
|
|
527 |
apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
|
|
528 |
apply assumption+
|
|
529 |
apply (erule exE)+
|
|
530 |
apply (erule conjE)+
|
|
531 |
|
|
532 |
(* use reduceA_mksch to rewrite conclusion *)
|
|
533 |
apply hypsubst
|
|
534 |
apply simp
|
|
535 |
|
|
536 |
(* eliminate the B-only prefix *)
|
|
537 |
|
|
538 |
apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
|
|
539 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
540 |
prefer 2 apply assumption
|
|
541 |
prefer 2 apply fast
|
|
542 |
|
|
543 |
(* Now real recursive step follows (in y) *)
|
|
544 |
|
|
545 |
apply simp
|
|
546 |
apply (case_tac "x:act A")
|
|
547 |
apply (case_tac "x~:act B")
|
|
548 |
apply (rotate_tac -2)
|
|
549 |
apply simp
|
|
550 |
|
|
551 |
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
|
|
552 |
apply (rotate_tac -1)
|
|
553 |
apply simp
|
|
554 |
(* eliminate introduced subgoal 2 *)
|
|
555 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
556 |
prefer 2 apply assumption
|
|
557 |
prefer 2 apply fast
|
|
558 |
|
|
559 |
(* bring in divide Seq for s *)
|
|
560 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
561 |
apply (erule conjE)+
|
|
562 |
|
|
563 |
(* subst divide_Seq in conclusion, but only at the righest occurence *)
|
|
564 |
apply (rule_tac t = "schA" in ssubst)
|
|
565 |
back
|
|
566 |
back
|
|
567 |
back
|
|
568 |
apply assumption
|
|
569 |
|
|
570 |
(* reduce trace_takes from n to strictly smaller k *)
|
|
571 |
apply (rule take_reduction)
|
|
572 |
|
|
573 |
(* f A (tw iA) = tw ~eA *)
|
|
574 |
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
|
|
575 |
apply (rule refl)
|
|
576 |
apply (simp add: int_is_act not_ext_is_int_or_not_act)
|
|
577 |
apply (rotate_tac -11)
|
|
578 |
|
|
579 |
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
|
|
580 |
|
|
581 |
(* assumption Forall tr *)
|
|
582 |
(* assumption schB *)
|
|
583 |
apply (simp add: Forall_Conc ext_and_act)
|
|
584 |
(* assumption schA *)
|
|
585 |
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
|
|
586 |
apply assumption
|
|
587 |
apply (simp add: int_is_not_ext)
|
|
588 |
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
|
|
589 |
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
|
|
590 |
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
|
|
591 |
apply assumption
|
|
592 |
|
|
593 |
(* assumption Forall schA *)
|
|
594 |
apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
|
|
595 |
apply assumption
|
|
596 |
apply (simp add: ForallPTakewhileQ int_is_act)
|
|
597 |
|
|
598 |
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
|
|
599 |
|
|
600 |
|
|
601 |
apply (rotate_tac -2)
|
|
602 |
apply simp
|
|
603 |
|
|
604 |
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
|
|
605 |
apply (rotate_tac -1)
|
|
606 |
apply simp
|
|
607 |
(* eliminate introduced subgoal 2 *)
|
|
608 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
609 |
prefer 2 apply (assumption)
|
|
610 |
prefer 2 apply (fast)
|
|
611 |
|
|
612 |
(* bring in divide Seq for s *)
|
|
613 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
614 |
apply (erule conjE)+
|
|
615 |
|
|
616 |
(* subst divide_Seq in conclusion, but only at the righest occurence *)
|
|
617 |
apply (rule_tac t = "schA" in ssubst)
|
|
618 |
back
|
|
619 |
back
|
|
620 |
back
|
|
621 |
apply assumption
|
|
622 |
|
|
623 |
(* f A (tw iA) = tw ~eA *)
|
|
624 |
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
|
|
625 |
|
|
626 |
(* rewrite assumption forall and schB *)
|
|
627 |
apply (rotate_tac 13)
|
|
628 |
apply (simp add: ext_and_act)
|
|
629 |
|
|
630 |
(* divide_Seq for schB2 *)
|
|
631 |
apply (frule_tac y = "y2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
632 |
apply (erule conjE)+
|
|
633 |
(* assumption schA *)
|
|
634 |
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
|
|
635 |
apply assumption
|
|
636 |
apply (simp add: int_is_not_ext)
|
|
637 |
|
|
638 |
(* f A (tw iB schB2) = nil *)
|
|
639 |
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
|
|
640 |
|
|
641 |
|
|
642 |
(* reduce trace_takes from n to strictly smaller k *)
|
|
643 |
apply (rule take_reduction)
|
|
644 |
apply (rule refl)
|
|
645 |
apply (rule refl)
|
|
646 |
|
|
647 |
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
|
|
648 |
|
|
649 |
(* assumption schB *)
|
|
650 |
apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
|
|
651 |
apply assumption
|
|
652 |
apply (simp add: intA_is_not_actB int_is_not_ext)
|
|
653 |
|
|
654 |
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
|
|
655 |
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
|
|
656 |
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
|
|
657 |
apply assumption
|
|
658 |
apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)
|
|
659 |
|
|
660 |
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
|
|
661 |
apply (simp add: ForallTL ForallDropwhile)
|
|
662 |
|
|
663 |
(* case x~:A & x:B *)
|
|
664 |
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
|
|
665 |
apply (case_tac "x:act B")
|
|
666 |
apply fast
|
|
667 |
|
|
668 |
(* case x~:A & x~:B *)
|
|
669 |
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
|
|
670 |
apply (rotate_tac -9)
|
|
671 |
(* reduce forall assumption from tr to (x>>rs) *)
|
|
672 |
apply (simp add: externals_of_par)
|
|
673 |
apply (fast intro!: ext_is_act)
|
|
674 |
|
|
675 |
done
|
|
676 |
|
|
677 |
|
|
678 |
|
|
679 |
subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
|
|
680 |
|
|
681 |
lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;
|
|
682 |
is_asig(asig_of A); is_asig(asig_of B) |] ==>
|
|
683 |
Forall (%x. x:ext (A||B)) tr &
|
|
684 |
Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
|
|
685 |
Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
|
|
686 |
Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
|
|
687 |
LastActExtsch A schA & LastActExtsch B schB
|
|
688 |
--> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
|
|
689 |
apply (intro strip)
|
|
690 |
apply (rule seq.take_lemmas)
|
|
691 |
apply (rule mp)
|
|
692 |
prefer 2 apply assumption
|
|
693 |
back back back back
|
|
694 |
apply (rule_tac x = "schA" in spec)
|
|
695 |
apply (rule_tac x = "schB" in spec)
|
|
696 |
apply (rule_tac x = "tr" in spec)
|
|
697 |
apply (tactic "thin_tac' 5 1")
|
|
698 |
apply (rule nat_less_induct)
|
|
699 |
apply (rule allI)+
|
|
700 |
apply (rename_tac tr schB schA)
|
|
701 |
apply (intro strip)
|
|
702 |
apply (erule conjE)+
|
|
703 |
|
|
704 |
apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
|
|
705 |
|
|
706 |
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
|
|
707 |
apply (tactic "thin_tac' 5 1")
|
|
708 |
|
|
709 |
apply (case_tac "Finite tr")
|
|
710 |
|
|
711 |
(* both sides of this equation are nil *)
|
|
712 |
apply (subgoal_tac "schB=nil")
|
|
713 |
apply (simp (no_asm_simp))
|
|
714 |
(* first side: mksch = nil *)
|
|
715 |
apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
|
|
716 |
(* second side: schA = nil *)
|
|
717 |
apply (erule_tac A = "B" in LastActExtimplnil)
|
|
718 |
apply (simp (no_asm_simp))
|
|
719 |
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
|
|
720 |
apply assumption
|
|
721 |
apply fast
|
|
722 |
|
|
723 |
(* case ~ Finite tr *)
|
|
724 |
|
|
725 |
(* both sides of this equation are UU *)
|
|
726 |
apply (subgoal_tac "schB=UU")
|
|
727 |
apply (simp (no_asm_simp))
|
|
728 |
(* first side: mksch = UU *)
|
|
729 |
apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)
|
|
730 |
(* schA = UU *)
|
|
731 |
apply (erule_tac A = "B" in LastActExtimplUU)
|
|
732 |
apply (simp (no_asm_simp))
|
|
733 |
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
|
|
734 |
apply assumption
|
|
735 |
apply fast
|
|
736 |
|
|
737 |
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
|
|
738 |
|
|
739 |
apply (drule divide_Seq3)
|
|
740 |
|
|
741 |
apply (erule exE)+
|
|
742 |
apply (erule conjE)+
|
|
743 |
apply hypsubst
|
|
744 |
|
|
745 |
(* bring in lemma reduceB_mksch *)
|
|
746 |
apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
|
|
747 |
apply assumption+
|
|
748 |
apply (erule exE)+
|
|
749 |
apply (erule conjE)+
|
|
750 |
|
|
751 |
(* use reduceB_mksch to rewrite conclusion *)
|
|
752 |
apply hypsubst
|
|
753 |
apply simp
|
|
754 |
|
|
755 |
(* eliminate the A-only prefix *)
|
|
756 |
|
|
757 |
apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
|
|
758 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
759 |
prefer 2 apply (assumption)
|
|
760 |
prefer 2 apply (fast)
|
|
761 |
|
|
762 |
(* Now real recursive step follows (in x) *)
|
|
763 |
|
|
764 |
apply simp
|
|
765 |
apply (case_tac "x:act B")
|
|
766 |
apply (case_tac "x~:act A")
|
|
767 |
apply (rotate_tac -2)
|
|
768 |
apply simp
|
|
769 |
|
|
770 |
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
|
|
771 |
apply (rotate_tac -1)
|
|
772 |
apply simp
|
|
773 |
(* eliminate introduced subgoal 2 *)
|
|
774 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
775 |
prefer 2 apply (assumption)
|
|
776 |
prefer 2 apply (fast)
|
|
777 |
|
|
778 |
(* bring in divide Seq for s *)
|
|
779 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
780 |
apply (erule conjE)+
|
|
781 |
|
|
782 |
(* subst divide_Seq in conclusion, but only at the righest occurence *)
|
|
783 |
apply (rule_tac t = "schB" in ssubst)
|
|
784 |
back
|
|
785 |
back
|
|
786 |
back
|
|
787 |
apply assumption
|
|
788 |
|
|
789 |
(* reduce trace_takes from n to strictly smaller k *)
|
|
790 |
apply (rule take_reduction)
|
|
791 |
|
|
792 |
(* f B (tw iB) = tw ~eB *)
|
|
793 |
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
|
|
794 |
apply (rule refl)
|
|
795 |
apply (simp add: int_is_act not_ext_is_int_or_not_act)
|
|
796 |
apply (rotate_tac -11)
|
|
797 |
|
|
798 |
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
|
|
799 |
|
|
800 |
(* assumption schA *)
|
|
801 |
apply (simp add: Forall_Conc ext_and_act)
|
|
802 |
(* assumption schB *)
|
|
803 |
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
|
|
804 |
apply assumption
|
|
805 |
apply (simp add: int_is_not_ext)
|
|
806 |
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
|
|
807 |
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
|
|
808 |
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
|
|
809 |
apply assumption
|
|
810 |
|
|
811 |
(* assumption Forall schB *)
|
|
812 |
apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
|
|
813 |
apply assumption
|
|
814 |
apply (simp add: ForallPTakewhileQ int_is_act)
|
|
815 |
|
|
816 |
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
|
|
817 |
|
|
818 |
apply (rotate_tac -2)
|
|
819 |
apply simp
|
|
820 |
|
|
821 |
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
|
|
822 |
apply (rotate_tac -1)
|
|
823 |
apply simp
|
|
824 |
(* eliminate introduced subgoal 2 *)
|
|
825 |
apply (erule_tac [2] ForallQFilterPnil)
|
|
826 |
prefer 2 apply (assumption)
|
|
827 |
prefer 2 apply (fast)
|
|
828 |
|
|
829 |
(* bring in divide Seq for s *)
|
|
830 |
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
831 |
apply (erule conjE)+
|
|
832 |
|
|
833 |
(* subst divide_Seq in conclusion, but only at the righest occurence *)
|
|
834 |
apply (rule_tac t = "schB" in ssubst)
|
|
835 |
back
|
|
836 |
back
|
|
837 |
back
|
|
838 |
apply assumption
|
|
839 |
|
|
840 |
(* f B (tw iB) = tw ~eB *)
|
|
841 |
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
|
|
842 |
|
|
843 |
(* rewrite assumption forall and schB *)
|
|
844 |
apply (rotate_tac 13)
|
|
845 |
apply (simp add: ext_and_act)
|
|
846 |
|
|
847 |
(* divide_Seq for schB2 *)
|
|
848 |
apply (frule_tac y = "x2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
|
|
849 |
apply (erule conjE)+
|
|
850 |
(* assumption schA *)
|
|
851 |
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
|
|
852 |
apply assumption
|
|
853 |
apply (simp add: int_is_not_ext)
|
|
854 |
|
|
855 |
(* f B (tw iA schA2) = nil *)
|
|
856 |
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
|
|
857 |
|
|
858 |
|
|
859 |
(* reduce trace_takes from n to strictly smaller k *)
|
|
860 |
apply (rule take_reduction)
|
|
861 |
apply (rule refl)
|
|
862 |
apply (rule refl)
|
|
863 |
|
|
864 |
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
|
|
865 |
|
|
866 |
(* assumption schA *)
|
|
867 |
apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
|
|
868 |
apply assumption
|
|
869 |
apply (simp add: intA_is_not_actB int_is_not_ext)
|
|
870 |
|
|
871 |
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
|
|
872 |
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
|
|
873 |
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
|
|
874 |
apply assumption
|
|
875 |
apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
|
|
876 |
|
|
877 |
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
|
|
878 |
apply (simp add: ForallTL ForallDropwhile)
|
|
879 |
|
|
880 |
(* case x~:B & x:A *)
|
|
881 |
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
|
|
882 |
apply (case_tac "x:act A")
|
|
883 |
apply fast
|
|
884 |
|
|
885 |
(* case x~:B & x~:A *)
|
|
886 |
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
|
|
887 |
apply (rotate_tac -9)
|
|
888 |
(* reduce forall assumption from tr to (x>>rs) *)
|
|
889 |
apply (simp add: externals_of_par)
|
|
890 |
apply (fast intro!: ext_is_act)
|
|
891 |
|
|
892 |
done
|
|
893 |
|
|
894 |
|
|
895 |
subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
|
|
896 |
|
|
897 |
lemma compositionality_tr:
|
|
898 |
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
|
|
899 |
is_asig(asig_of A); is_asig(asig_of B)|]
|
|
900 |
==> (tr: traces(A||B)) =
|
|
901 |
(Filter (%a. a:act A)$tr : traces A &
|
|
902 |
Filter (%a. a:act B)$tr : traces B &
|
|
903 |
Forall (%x. x:ext(A||B)) tr)"
|
|
904 |
|
|
905 |
apply (simp (no_asm) add: traces_def has_trace_def)
|
|
906 |
apply (tactic "safe_tac set_cs")
|
|
907 |
|
|
908 |
(* ==> *)
|
|
909 |
(* There is a schedule of A *)
|
|
910 |
apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
|
|
911 |
prefer 2
|
|
912 |
apply (simp add: compositionality_sch)
|
|
913 |
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
|
|
914 |
(* There is a schedule of B *)
|
|
915 |
apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
|
|
916 |
prefer 2
|
|
917 |
apply (simp add: compositionality_sch)
|
|
918 |
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
|
|
919 |
(* Traces of A||B have only external actions from A or B *)
|
|
920 |
apply (rule ForallPFilterP)
|
|
921 |
|
|
922 |
(* <== *)
|
|
923 |
|
|
924 |
(* replace schA and schB by Cut(schA) and Cut(schB) *)
|
|
925 |
apply (drule exists_LastActExtsch)
|
|
926 |
apply assumption
|
|
927 |
apply (drule exists_LastActExtsch)
|
|
928 |
apply assumption
|
|
929 |
apply (erule exE)+
|
|
930 |
apply (erule conjE)+
|
|
931 |
(* Schedules of A(B) have only actions of A(B) *)
|
|
932 |
apply (drule scheds_in_sig)
|
|
933 |
apply assumption
|
|
934 |
apply (drule scheds_in_sig)
|
|
935 |
apply assumption
|
|
936 |
|
|
937 |
apply (rename_tac h1 h2 schA schB)
|
|
938 |
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
|
|
939 |
we need here *)
|
|
940 |
apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
|
|
941 |
|
|
942 |
(* External actions of mksch are just the oracle *)
|
|
943 |
apply (simp add: FilterA_mksch_is_tr)
|
|
944 |
|
|
945 |
(* mksch is a schedule -- use compositionality on sch-level *)
|
|
946 |
apply (simp add: compositionality_sch)
|
|
947 |
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
|
|
948 |
apply (erule ForallAorB_mksch)
|
|
949 |
apply (erule ForallPForallQ)
|
|
950 |
apply (erule ext_is_act)
|
|
951 |
done
|
|
952 |
|
|
953 |
|
|
954 |
|
|
955 |
subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
|
|
956 |
|
|
957 |
lemma compositionality_tr_modules:
|
|
958 |
|
|
959 |
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
|
|
960 |
is_asig(asig_of A); is_asig(asig_of B)|]
|
|
961 |
==> Traces (A||B) = par_traces (Traces A) (Traces B)"
|
|
962 |
|
|
963 |
apply (unfold Traces_def par_traces_def)
|
|
964 |
apply (simp add: asig_of_par)
|
|
965 |
apply (rule set_ext)
|
|
966 |
apply (simp add: compositionality_tr externals_of_par)
|
|
967 |
done
|
|
968 |
|
|
969 |
|
|
970 |
ML_setup {* change_simpset (fn ss => ss setmksym (SOME o symmetric_fun)) *}
|
3071
|
971 |
|
|
972 |
|
|
973 |
end
|