author | wenzelm |
Wed, 07 Jan 1998 13:55:54 +0100 | |
changeset 4520 | d430a1b34928 |
parent 4477 | b3e5857d8d99 |
child 4678 | 78715f589655 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/CompoTraces.ML |
3080 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1996 TU Muenchen |
|
3275 | 5 |
|
3071 | 6 |
Compositionality on Trace level. |
7 |
*) |
|
8 |
||
9 |
||
3275 | 10 |
|
3071 | 11 |
(* ---------------------------------------------------------------- *) |
12 |
section "mksch rewrite rules"; |
|
13 |
(* ---------------------------------------------------------------- *) |
|
14 |
||
15 |
||
16 |
||
17 |
||
18 |
bind_thm ("mksch_unfold", fix_prover2 thy mksch_def |
|
19 |
"mksch A B = (LAM tr schA schB. case tr of \ |
|
20 |
\ nil => nil\ |
|
21 |
\ | x##xs => \ |
|
22 |
\ (case x of \ |
|
23 |
\ Undef => UU \ |
|
24 |
\ | Def y => \ |
|
25 |
\ (if y:act A then \ |
|
26 |
\ (if y:act B then \ |
|
3842 | 27 |
\ ((Takewhile (%a. a:int A)`schA) \ |
28 |
\ @@(Takewhile (%a. a:int B)`schB) \ |
|
3071 | 29 |
\ @@(y>>(mksch A B`xs \ |
3842 | 30 |
\ `(TL`(Dropwhile (%a. a:int A)`schA)) \ |
31 |
\ `(TL`(Dropwhile (%a. a:int B)`schB)) \ |
|
3071 | 32 |
\ ))) \ |
33 |
\ else \ |
|
3842 | 34 |
\ ((Takewhile (%a. a:int A)`schA) \ |
3071 | 35 |
\ @@ (y>>(mksch A B`xs \ |
3842 | 36 |
\ `(TL`(Dropwhile (%a. a:int A)`schA)) \ |
3071 | 37 |
\ `schB))) \ |
38 |
\ ) \ |
|
39 |
\ else \ |
|
40 |
\ (if y:act B then \ |
|
3842 | 41 |
\ ((Takewhile (%a. a:int B)`schB) \ |
3071 | 42 |
\ @@ (y>>(mksch A B`xs \ |
43 |
\ `schA \ |
|
3842 | 44 |
\ `(TL`(Dropwhile (%a. a:int B)`schB)) \ |
3071 | 45 |
\ ))) \ |
46 |
\ else \ |
|
47 |
\ UU \ |
|
48 |
\ ) \ |
|
49 |
\ ) \ |
|
50 |
\ ))"); |
|
51 |
||
52 |
||
53 |
goal thy "mksch A B`UU`schA`schB = UU"; |
|
54 |
by (stac mksch_unfold 1); |
|
55 |
by (Simp_tac 1); |
|
56 |
qed"mksch_UU"; |
|
57 |
||
58 |
goal thy "mksch A B`nil`schA`schB = nil"; |
|
59 |
by (stac mksch_unfold 1); |
|
60 |
by (Simp_tac 1); |
|
61 |
qed"mksch_nil"; |
|
62 |
||
63 |
goal thy "!!x.[|x:act A;x~:act B|] \ |
|
64 |
\ ==> mksch A B`(x>>tr)`schA`schB = \ |
|
3842 | 65 |
\ (Takewhile (%a. a:int A)`schA) \ |
66 |
\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \ |
|
3071 | 67 |
\ `schB))"; |
3457 | 68 |
by (rtac trans 1); |
3071 | 69 |
by (stac mksch_unfold 1); |
4098 | 70 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1); |
71 |
by (simp_tac (simpset() addsimps [Cons_def]) 1); |
|
3071 | 72 |
qed"mksch_cons1"; |
73 |
||
74 |
goal thy "!!x.[|x~:act A;x:act B|] \ |
|
75 |
\ ==> mksch A B`(x>>tr)`schA`schB = \ |
|
3842 | 76 |
\ (Takewhile (%a. a:int B)`schB) \ |
77 |
\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB)) \ |
|
3071 | 78 |
\ ))"; |
3457 | 79 |
by (rtac trans 1); |
3071 | 80 |
by (stac mksch_unfold 1); |
4098 | 81 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1); |
82 |
by (simp_tac (simpset() addsimps [Cons_def]) 1); |
|
3071 | 83 |
qed"mksch_cons2"; |
84 |
||
85 |
goal thy "!!x.[|x:act A;x:act B|] \ |
|
86 |
\ ==> mksch A B`(x>>tr)`schA`schB = \ |
|
3842 | 87 |
\ (Takewhile (%a. a:int A)`schA) \ |
88 |
\ @@ ((Takewhile (%a. a:int B)`schB) \ |
|
89 |
\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \ |
|
90 |
\ `(TL`(Dropwhile (%a. a:int B)`schB)))) \ |
|
3071 | 91 |
\ )"; |
3457 | 92 |
by (rtac trans 1); |
3071 | 93 |
by (stac mksch_unfold 1); |
4098 | 94 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1); |
95 |
by (simp_tac (simpset() addsimps [Cons_def]) 1); |
|
3071 | 96 |
qed"mksch_cons3"; |
97 |
||
98 |
val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3]; |
|
99 |
||
100 |
Addsimps compotr_simps; |
|
101 |
||
102 |
||
103 |
(* ------------------------------------------------------------------ *) |
|
104 |
(* The following lemmata aim for *) |
|
105 |
(* COMPOSITIONALITY on TRACE Level *) |
|
106 |
(* ------------------------------------------------------------------ *) |
|
107 |
||
108 |
||
109 |
(* ---------------------------------------------------------------------------- *) |
|
3275 | 110 |
section"Lemmata for ==>"; |
3071 | 111 |
(* ---------------------------------------------------------------------------- *) |
112 |
||
113 |
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of |
|
114 |
the compatibility of IOA, in particular out of the condition that internals are |
|
115 |
really hidden. *) |
|
116 |
||
117 |
goal thy "(eB & ~eA --> ~A) --> \ |
|
118 |
\ (A & (eA | eB)) = (eA & A)"; |
|
119 |
by (Fast_tac 1); |
|
120 |
qed"compatibility_consequence1"; |
|
121 |
||
122 |
||
123 |
(* very similar to above, only the commutativity of | is used to make a slight change *) |
|
124 |
||
125 |
goal thy "(eB & ~eA --> ~A) --> \ |
|
126 |
\ (A & (eB | eA)) = (eA & A)"; |
|
127 |
by (Fast_tac 1); |
|
128 |
qed"compatibility_consequence2"; |
|
129 |
||
130 |
||
3275 | 131 |
(* ---------------------------------------------------------------------------- *) |
132 |
section"Lemmata for <=="; |
|
133 |
(* ---------------------------------------------------------------------------- *) |
|
3071 | 134 |
|
135 |
||
3275 | 136 |
(* Lemma for substitution of looping assumption in another specific assumption *) |
137 |
val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"; |
|
138 |
by (cut_facts_tac [p1] 1); |
|
3457 | 139 |
by (etac (p2 RS subst) 1); |
3275 | 140 |
qed"subst_lemma1"; |
3071 | 141 |
|
3275 | 142 |
(* Lemma for substitution of looping assumption in another specific assumption *) |
143 |
val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"; |
|
144 |
by (cut_facts_tac [p1] 1); |
|
3457 | 145 |
by (etac (p2 RS subst) 1); |
3275 | 146 |
qed"subst_lemma2"; |
3071 | 147 |
|
148 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
149 |
goal thy "!!A B. compatible A B ==> \ |
3071 | 150 |
\ ! schA schB. Forall (%x. x:act (A||B)) tr \ |
151 |
\ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)"; |
|
152 |
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
|
153 |
by (safe_tac set_cs); |
|
4098 | 154 |
by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1); |
3071 | 155 |
by (case_tac "a:act A" 1); |
156 |
by (case_tac "a:act B" 1); |
|
157 |
(* a:A, a:B *) |
|
158 |
by (Asm_full_simp_tac 1); |
|
3457 | 159 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 160 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
3457 | 161 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 162 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
3071 | 163 |
(* a:A,a~:B *) |
164 |
by (Asm_full_simp_tac 1); |
|
3457 | 165 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 166 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
3071 | 167 |
by (case_tac "a:act B" 1); |
168 |
(* a~:A, a:B *) |
|
169 |
by (Asm_full_simp_tac 1); |
|
3457 | 170 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 171 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
3071 | 172 |
(* a~:A,a~:B *) |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
173 |
by Auto_tac; |
3275 | 174 |
qed"ForallAorB_mksch1"; |
3071 | 175 |
|
3275 | 176 |
bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp); |
3071 | 177 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
178 |
goal thy "!!A B. compatible B A ==> \ |
3071 | 179 |
\ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \ |
180 |
\ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))"; |
|
181 |
||
182 |
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
|
183 |
by (safe_tac set_cs); |
|
3457 | 184 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 185 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, |
3275 | 186 |
intA_is_not_actB,int_is_act]) 1); |
3071 | 187 |
qed"ForallBnA_mksch"; |
188 |
||
3275 | 189 |
bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp); |
190 |
||
191 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
192 |
goal thy "!!A B. compatible A B ==> \ |
3071 | 193 |
\ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \ |
194 |
\ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))"; |
|
195 |
||
196 |
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
|
197 |
by (safe_tac set_cs); |
|
198 |
by (Asm_full_simp_tac 1); |
|
3457 | 199 |
by (rtac (Forall_Conc_impl RS mp) 1); |
4098 | 200 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, |
3275 | 201 |
intA_is_not_actB,int_is_act]) 1); |
3071 | 202 |
qed"ForallAnB_mksch"; |
203 |
||
3275 | 204 |
bind_thm ("ForallAnBmksch",ForallAnB_mksch RS spec RS spec RS mp); |
205 |
||
3071 | 206 |
|
3275 | 207 |
(* safe-tac makes too many case distinctions with this lemma in the next proof *) |
208 |
Delsimps [FiniteConc]; |
|
3071 | 209 |
|
3275 | 210 |
goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
3842 | 211 |
\ ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \ |
3275 | 212 |
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \ |
3071 | 213 |
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\ |
214 |
\ Forall (%x. x:ext (A||B)) tr \ |
|
215 |
\ --> Finite (mksch A B`tr`x`y)"; |
|
216 |
||
3457 | 217 |
by (etac Seq_Finite_ind 1); |
3071 | 218 |
by (Asm_full_simp_tac 1); |
219 |
(* main case *) |
|
4098 | 220 |
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1); |
3071 | 221 |
by (safe_tac set_cs); |
3275 | 222 |
|
223 |
(* a: act A; a: act B *) |
|
224 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
225 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
226 |
back(); |
|
227 |
by (REPEAT (etac conjE 1)); |
|
228 |
(* Finite (tw iA x) and Finite (tw iB y) *) |
|
4098 | 229 |
by (asm_full_simp_tac (simpset() addsimps |
3275 | 230 |
[not_ext_is_int_or_not_act,FiniteConc]) 1); |
231 |
(* now for conclusion IH applicable, but assumptions have to be transformed *) |
|
232 |
by (dres_inst_tac [("x","x"), |
|
233 |
("g","Filter (%a. a:act A)`s")] subst_lemma2 1); |
|
3457 | 234 |
by (assume_tac 1); |
3275 | 235 |
by (dres_inst_tac [("x","y"), |
236 |
("g","Filter (%a. a:act B)`s")] subst_lemma2 1); |
|
3457 | 237 |
by (assume_tac 1); |
3275 | 238 |
(* IH *) |
4098 | 239 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
3275 | 240 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
241 |
||
242 |
(* a: act B; a~: act A *) |
|
243 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
3071 | 244 |
|
3275 | 245 |
by (REPEAT (etac conjE 1)); |
246 |
(* Finite (tw iB y) *) |
|
4098 | 247 |
by (asm_full_simp_tac (simpset() addsimps |
3275 | 248 |
[not_ext_is_int_or_not_act,FiniteConc]) 1); |
249 |
(* now for conclusion IH applicable, but assumptions have to be transformed *) |
|
250 |
by (dres_inst_tac [("x","y"), |
|
251 |
("g","Filter (%a. a:act B)`s")] subst_lemma2 1); |
|
3457 | 252 |
by (assume_tac 1); |
3275 | 253 |
(* IH *) |
4098 | 254 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
3275 | 255 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
3071 | 256 |
|
3275 | 257 |
(* a~: act B; a: act A *) |
258 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
3071 | 259 |
|
3275 | 260 |
by (REPEAT (etac conjE 1)); |
261 |
(* Finite (tw iA x) *) |
|
4098 | 262 |
by (asm_full_simp_tac (simpset() addsimps |
3275 | 263 |
[not_ext_is_int_or_not_act,FiniteConc]) 1); |
264 |
(* now for conclusion IH applicable, but assumptions have to be transformed *) |
|
265 |
by (dres_inst_tac [("x","x"), |
|
266 |
("g","Filter (%a. a:act A)`s")] subst_lemma2 1); |
|
3457 | 267 |
by (assume_tac 1); |
3275 | 268 |
(* IH *) |
4098 | 269 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
3275 | 270 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
271 |
||
272 |
(* a~: act B; a~: act A *) |
|
4098 | 273 |
by (fast_tac (claset() addSIs [ext_is_act] |
274 |
addss (simpset() addsimps [externals_of_par]) ) 1); |
|
3071 | 275 |
qed"FiniteL_mksch"; |
276 |
||
3275 | 277 |
bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp); |
278 |
||
279 |
Addsimps [FiniteConc]; |
|
280 |
||
281 |
||
282 |
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
|
283 |
Delsimps [FilterConc]; |
|
284 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
285 |
goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \ |
3842 | 286 |
\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\ |
3275 | 287 |
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \ |
288 |
\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \ |
|
289 |
\ Forall (%x. x:act B & x~:act A) y1 & \ |
|
290 |
\ Finite y1 & y = (y1 @@ y2) & \ |
|
291 |
\ Filter (%a. a:ext B)`y1 = bs)"; |
|
4473 | 292 |
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); |
3457 | 293 |
by (etac Seq_Finite_ind 1); |
3275 | 294 |
by (REPEAT (rtac allI 1)); |
3071 | 295 |
by (rtac impI 1); |
296 |
by (res_inst_tac [("x","nil")] exI 1); |
|
297 |
by (res_inst_tac [("x","y")] exI 1); |
|
298 |
by (Asm_full_simp_tac 1); |
|
299 |
(* main case *) |
|
3275 | 300 |
by (REPEAT (rtac allI 1)); |
3071 | 301 |
by (rtac impI 1); |
302 |
by (Asm_full_simp_tac 1); |
|
303 |
by (REPEAT (etac conjE 1)); |
|
3275 | 304 |
by (Asm_full_simp_tac 1); |
305 |
(* divide_Seq on s *) |
|
306 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
307 |
by (REPEAT (etac conjE 1)); |
|
308 |
(* transform assumption f eB y = f B (s@z) *) |
|
309 |
by (dres_inst_tac [("x","y"), |
|
310 |
("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1); |
|
3457 | 311 |
by (assume_tac 1); |
3275 | 312 |
Addsimps [FilterConc]; |
4098 | 313 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1); |
3275 | 314 |
(* apply IH *) |
3842 | 315 |
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1); |
4098 | 316 |
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); |
3275 | 317 |
by (REPEAT (etac exE 1)); |
318 |
by (REPEAT (etac conjE 1)); |
|
319 |
by (Asm_full_simp_tac 1); |
|
320 |
(* for replacing IH in conclusion *) |
|
321 |
by (rotate_tac ~2 1); |
|
322 |
by (Asm_full_simp_tac 1); |
|
323 |
(* instantiate y1a and y2a *) |
|
3842 | 324 |
by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1); |
3275 | 325 |
by (res_inst_tac [("x","y2")] exI 1); |
326 |
(* elminate all obligations up to two depending on Conc_assoc *) |
|
4098 | 327 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, |
3275 | 328 |
int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); |
4098 | 329 |
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
3275 | 330 |
qed"reduceA_mksch1"; |
331 |
||
332 |
bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp))); |
|
333 |
||
334 |
||
335 |
||
336 |
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
|
337 |
Delsimps [FilterConc]; |
|
338 |
||
339 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
340 |
goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \ |
3842 | 341 |
\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\ |
3275 | 342 |
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \ |
343 |
\ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \ |
|
344 |
\ Forall (%x. x:act A & x~:act B) x1 & \ |
|
345 |
\ Finite x1 & x = (x1 @@ x2) & \ |
|
346 |
\ Filter (%a. a:ext A)`x1 = as)"; |
|
4473 | 347 |
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); |
3457 | 348 |
by (etac Seq_Finite_ind 1); |
3275 | 349 |
by (REPEAT (rtac allI 1)); |
350 |
by (rtac impI 1); |
|
351 |
by (res_inst_tac [("x","nil")] exI 1); |
|
352 |
by (res_inst_tac [("x","x")] exI 1); |
|
353 |
by (Asm_full_simp_tac 1); |
|
354 |
(* main case *) |
|
355 |
by (REPEAT (rtac allI 1)); |
|
356 |
by (rtac impI 1); |
|
357 |
by (Asm_full_simp_tac 1); |
|
358 |
by (REPEAT (etac conjE 1)); |
|
359 |
by (Asm_full_simp_tac 1); |
|
360 |
(* divide_Seq on s *) |
|
361 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
362 |
by (REPEAT (etac conjE 1)); |
|
363 |
(* transform assumption f eA x = f A (s@z) *) |
|
364 |
by (dres_inst_tac [("x","x"), |
|
365 |
("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1); |
|
3457 | 366 |
by (assume_tac 1); |
3275 | 367 |
Addsimps [FilterConc]; |
4098 | 368 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1); |
3275 | 369 |
(* apply IH *) |
3842 | 370 |
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1); |
4098 | 371 |
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); |
3275 | 372 |
by (REPEAT (etac exE 1)); |
373 |
by (REPEAT (etac conjE 1)); |
|
374 |
by (Asm_full_simp_tac 1); |
|
375 |
(* for replacing IH in conclusion *) |
|
376 |
by (rotate_tac ~2 1); |
|
377 |
by (Asm_full_simp_tac 1); |
|
378 |
(* instantiate y1a and y2a *) |
|
3842 | 379 |
by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1); |
3275 | 380 |
by (res_inst_tac [("x","x2")] exI 1); |
381 |
(* elminate all obligations up to two depending on Conc_assoc *) |
|
4098 | 382 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, |
3275 | 383 |
int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); |
4098 | 384 |
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
3275 | 385 |
qed"reduceB_mksch1"; |
386 |
||
387 |
bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp))); |
|
3071 | 388 |
|
389 |
||
390 |
||
3314 | 391 |
(* |
3071 | 392 |
|
393 |
||
3314 | 394 |
goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \ |
395 |
\ y = z @@ mksch A B`tr`a`b\ |
|
396 |
\ --> Finite tr"; |
|
3457 | 397 |
by (etac Seq_Finite_ind 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
398 |
by Auto_tac; |
3314 | 399 |
by (Seq_case_simp_tac "tr" 1); |
400 |
(* tr = UU *) |
|
4098 | 401 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1); |
3314 | 402 |
(* tr = nil *) |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
403 |
by Auto_tac; |
3314 | 404 |
(* tr = Conc *) |
405 |
ren "s ss" 1; |
|
406 |
||
407 |
by (case_tac "s:act A" 1); |
|
408 |
by (case_tac "s:act B" 1); |
|
409 |
by (rotate_tac ~2 1); |
|
410 |
by (rotate_tac ~2 2); |
|
4098 | 411 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1); |
412 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1); |
|
3314 | 413 |
by (case_tac "s:act B" 1); |
414 |
by (rotate_tac ~2 1); |
|
4098 | 415 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1); |
416 |
by (fast_tac (claset() addSIs [ext_is_act] |
|
417 |
addss (simpset() addsimps [externals_of_par]) ) 1); |
|
3314 | 418 |
(* main case *) |
419 |
by (Seq_case_simp_tac "tr" 1); |
|
420 |
(* tr = UU *) |
|
4098 | 421 |
by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
422 |
by Auto_tac; |
3314 | 423 |
(* tr = nil ok *) |
424 |
(* tr = Conc *) |
|
425 |
by (Seq_case_simp_tac "z" 1); |
|
426 |
(* z = UU ok *) |
|
427 |
(* z = nil *) |
|
428 |
||
429 |
(* z= Cons *) |
|
430 |
||
431 |
||
432 |
by (case_tac "aaa:act A" 2); |
|
433 |
by (case_tac "aaa:act B" 2); |
|
434 |
by (rotate_tac ~2 2); |
|
435 |
by (rotate_tac ~2 3); |
|
436 |
by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2); |
|
3842 | 437 |
by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2); |
3314 | 438 |
by (eres_inst_tac [("x","sa")] allE 2); |
4098 | 439 |
by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2); |
3314 | 440 |
|
441 |
||
442 |
||
443 |
by (eres_inst_tac [("x","sa")] allE 1); |
|
444 |
by (Asm_full_simp_tac 1); |
|
445 |
by (case_tac "aaa:act A" 1); |
|
446 |
by (case_tac "aaa:act B" 1); |
|
447 |
by (rotate_tac ~2 1); |
|
448 |
by (rotate_tac ~2 2); |
|
4098 | 449 |
by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1); |
3314 | 450 |
|
451 |
||
452 |
||
453 |
goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))"; |
|
454 |
by (Seq_case_simp_tac "y" 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
455 |
by Auto_tac; |
3314 | 456 |
qed"Conc_Conc_eq"; |
457 |
||
458 |
goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU"; |
|
3457 | 459 |
by (etac Seq_Finite_ind 1); |
3314 | 460 |
by (Seq_case_simp_tac "x" 1); |
461 |
by (Seq_case_simp_tac "x" 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
462 |
by Auto_tac; |
3314 | 463 |
qed"FiniteConcUU1"; |
464 |
||
465 |
goal thy "~ Finite ((x::'a Seq)@@UU)"; |
|
3457 | 466 |
by (rtac (FiniteConcUU1 COMP rev_contrapos) 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
467 |
by Auto_tac; |
3314 | 468 |
qed"FiniteConcUU"; |
469 |
||
470 |
finiteR_mksch |
|
471 |
"Finite (mksch A B`tr`x`y) --> Finite tr" |
|
472 |
*) |
|
473 |
||
3071 | 474 |
|
475 |
||
3275 | 476 |
(*------------------------------------------------------------------------------------- *) |
477 |
section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"; |
|
478 |
(* structural induction |
|
479 |
------------------------------------------------------------------------------------- *) |
|
3071 | 480 |
|
3275 | 481 |
goal thy |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
482 |
"!! A B. [| compatible A B; compatible B A;\ |
3275 | 483 |
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
3842 | 484 |
\ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \ |
485 |
\ Forall (%x. x:ext (A||B)) tr & \ |
|
486 |
\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\ |
|
487 |
\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB \ |
|
488 |
\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr"; |
|
3071 | 489 |
|
490 |
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
|
491 |
||
492 |
(* main case *) |
|
493 |
(* splitting into 4 cases according to a:A, a:B *) |
|
4098 | 494 |
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1); |
3071 | 495 |
by (safe_tac set_cs); |
496 |
||
497 |
(* Case a:A, a:B *) |
|
498 |
by (forward_tac [divide_Seq] 1); |
|
499 |
by (forward_tac [divide_Seq] 1); |
|
500 |
back(); |
|
501 |
by (REPEAT (etac conjE 1)); |
|
3275 | 502 |
(* filtering internals of A in schA and of B in schB is nil *) |
4098 | 503 |
by (asm_full_simp_tac (simpset() addsimps |
3275 | 504 |
[FilterPTakewhileQnil,not_ext_is_int_or_not_act, |
505 |
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); |
|
3071 | 506 |
(* conclusion of IH ok, but assumptions of IH have to be transformed *) |
507 |
by (dres_inst_tac [("x","schA")] subst_lemma1 1); |
|
3457 | 508 |
by (assume_tac 1); |
3071 | 509 |
by (dres_inst_tac [("x","schB")] subst_lemma1 1); |
3457 | 510 |
by (assume_tac 1); |
3275 | 511 |
(* IH *) |
4098 | 512 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
3275 | 513 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
4520 | 514 |
|
515 |
(* Case a:A, a~:B *) |
|
516 |
by (forward_tac [divide_Seq] 1); |
|
517 |
by (REPEAT (etac conjE 1)); |
|
518 |
(* filtering internals of A is nil *) |
|
519 |
by (asm_full_simp_tac (simpset() addsimps |
|
520 |
[FilterPTakewhileQnil,not_ext_is_int_or_not_act, |
|
521 |
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); |
|
522 |
by (dres_inst_tac [("x","schA")] subst_lemma1 1); |
|
523 |
by (assume_tac 1); |
|
524 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
|
525 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
|
526 |
||
3071 | 527 |
(* Case a:B, a~:A *) |
528 |
by (forward_tac [divide_Seq] 1); |
|
529 |
by (REPEAT (etac conjE 1)); |
|
530 |
(* filtering internals of A is nil *) |
|
4098 | 531 |
by (asm_full_simp_tac (simpset() addsimps |
3275 | 532 |
[FilterPTakewhileQnil,not_ext_is_int_or_not_act, |
533 |
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); |
|
3071 | 534 |
by (dres_inst_tac [("x","schB")] subst_lemma1 1); |
535 |
back(); |
|
3457 | 536 |
by (assume_tac 1); |
4098 | 537 |
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, |
3275 | 538 |
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); |
3071 | 539 |
|
540 |
(* Case a~:A, a~:B *) |
|
4098 | 541 |
by (fast_tac (claset() addSIs [ext_is_act] |
542 |
addss (simpset() addsimps [externals_of_par]) ) 1); |
|
3275 | 543 |
qed"FilterA_mksch_is_tr"; |
3071 | 544 |
|
545 |
||
546 |
||
3314 | 547 |
(* |
548 |
||
549 |
***************************************************************8 |
|
550 |
With uncomplete take lemma rule should be reused afterwards !!!!!!!!!!!!!!!!! |
|
551 |
********************************************************************** |
|
552 |
||
553 |
(*--------------------------------------------------------------------------- |
|
554 |
Filter of mksch(tr,schA,schB) to A is schA |
|
555 |
take lemma |
|
556 |
--------------------------------------------------------------------------- *) |
|
557 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
558 |
goal thy "!! A B. [| compatible A B; compatible B A; \ |
3314 | 559 |
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
3842 | 560 |
\ Forall (%x. x:ext (A||B)) tr & \ |
561 |
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \ |
|
562 |
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\ |
|
563 |
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\ |
|
3314 | 564 |
\ LastActExtsch A schA & LastActExtsch B schB \ |
3842 | 565 |
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA"; |
3314 | 566 |
|
567 |
by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1); |
|
568 |
by (REPEAT (etac conjE 1)); |
|
569 |
||
570 |
by (case_tac "Finite s" 1); |
|
571 |
||
572 |
(* both sides of this equation are nil *) |
|
573 |
by (subgoal_tac "schA=nil" 1); |
|
574 |
by (Asm_simp_tac 1); |
|
575 |
(* first side: mksch = nil *) |
|
4098 | 576 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch], |
577 |
simpset())) 1); |
|
3314 | 578 |
(* second side: schA = nil *) |
579 |
by (eres_inst_tac [("A","A")] LastActExtimplnil 1); |
|
580 |
by (Asm_simp_tac 1); |
|
4098 | 581 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil], |
582 |
simpset())) 1); |
|
3314 | 583 |
|
584 |
(* case ~ Finite s *) |
|
585 |
||
586 |
(* both sides of this equation are UU *) |
|
587 |
by (subgoal_tac "schA=UU" 1); |
|
588 |
by (Asm_simp_tac 1); |
|
589 |
(* first side: mksch = UU *) |
|
4098 | 590 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU, |
3314 | 591 |
(finiteR_mksch RS mp COMP rev_contrapos), |
592 |
ForallBnAmksch], |
|
4098 | 593 |
simpset())) 1); |
3314 | 594 |
(* schA = UU *) |
595 |
by (eres_inst_tac [("A","A")] LastActExtimplUU 1); |
|
596 |
by (Asm_simp_tac 1); |
|
4098 | 597 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU], |
598 |
simpset())) 1); |
|
3314 | 599 |
|
600 |
(* case" ~ Forall (%x.x:act B & x~:act A) s" *) |
|
601 |
||
602 |
by (REPEAT (etac conjE 1)); |
|
603 |
||
604 |
(* bring in lemma reduceA_mksch *) |
|
605 |
by (forw_inst_tac [("y","schB"),("x","schA")] reduceA_mksch 1); |
|
606 |
by (REPEAT (atac 1)); |
|
607 |
by (REPEAT (etac exE 1)); |
|
608 |
by (REPEAT (etac conjE 1)); |
|
609 |
||
610 |
(* use reduceA_mksch to rewrite conclusion *) |
|
611 |
by (hyp_subst_tac 1); |
|
612 |
by (Asm_full_simp_tac 1); |
|
613 |
||
614 |
(* eliminate the B-only prefix *) |
|
615 |
||
3842 | 616 |
by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1); |
3457 | 617 |
by (etac ForallQFilterPnil 2); |
618 |
by (assume_tac 2); |
|
3314 | 619 |
by (Fast_tac 2); |
620 |
||
621 |
(* Now real recursive step follows (in y) *) |
|
622 |
||
623 |
by (Asm_full_simp_tac 1); |
|
624 |
by (case_tac "y:act A" 1); |
|
625 |
by (case_tac "y~:act B" 1); |
|
626 |
by (rotate_tac ~2 1); |
|
627 |
by (Asm_full_simp_tac 1); |
|
628 |
||
629 |
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); |
|
630 |
by (rotate_tac ~1 1); |
|
631 |
by (Asm_full_simp_tac 1); |
|
632 |
(* eliminate introduced subgoal 2 *) |
|
3457 | 633 |
by (etac ForallQFilterPnil 2); |
634 |
by (assume_tac 2); |
|
3314 | 635 |
by (Fast_tac 2); |
636 |
||
637 |
(* bring in divide Seq for s *) |
|
638 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
639 |
by (REPEAT (etac conjE 1)); |
|
640 |
||
641 |
(* subst divide_Seq in conclusion, but only at the righest occurence *) |
|
642 |
by (res_inst_tac [("t","schA")] ssubst 1); |
|
643 |
back(); |
|
644 |
back(); |
|
645 |
back(); |
|
3457 | 646 |
by (assume_tac 1); |
3314 | 647 |
|
648 |
(* reduce trace_takes from n to strictly smaller k *) |
|
3457 | 649 |
by (rtac take_reduction 1); |
3314 | 650 |
|
651 |
(* f A (tw iA) = tw ~eA *) |
|
4098 | 652 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act, |
3314 | 653 |
not_ext_is_int_or_not_act]) 1); |
3457 | 654 |
by (rtac refl 1); |
3314 | 655 |
|
656 |
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *) |
|
657 |
(* |
|
658 |
||
659 |
nacessary anymore ???????????????? |
|
660 |
by (rotate_tac ~10 1); |
|
661 |
||
662 |
*) |
|
663 |
(* assumption schB *) |
|
4098 | 664 |
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1); |
3314 | 665 |
(* assumption schA *) |
666 |
by (dres_inst_tac [("x","schA"), |
|
667 |
("g","Filter (%a. a:act A)`s2")] subst_lemma2 1); |
|
3457 | 668 |
by (assume_tac 1); |
4098 | 669 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil]) 1); |
3314 | 670 |
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) |
671 |
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1); |
|
672 |
by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1); |
|
3457 | 673 |
by (assume_tac 1); |
3314 | 674 |
|
675 |
FIX: problem: schA and schB are not quantified in the new take lemma version !!! |
|
676 |
||
677 |
by (Asm_full_simp_tac 1); |
|
678 |
||
679 |
********************************************************************************************** |
|
680 |
*) |
|
681 |
||
682 |
||
683 |
||
3275 | 684 |
(*--------------------------------------------------------------------------- *) |
3071 | 685 |
|
3275 | 686 |
section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"; |
687 |
||
688 |
(* --------------------------------------------------------------------------- *) |
|
3071 | 689 |
|
690 |
||
691 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
692 |
goal thy "!! A B. [| compatible A B; compatible B A; \ |
3275 | 693 |
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
3842 | 694 |
\ Forall (%x. x:ext (A||B)) tr & \ |
695 |
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \ |
|
696 |
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\ |
|
697 |
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\ |
|
3275 | 698 |
\ LastActExtsch A schA & LastActExtsch B schB \ |
3842 | 699 |
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA"; |
3071 | 700 |
|
3275 | 701 |
by (strip_tac 1); |
4042 | 702 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 703 |
by (rtac mp 1); |
704 |
by (assume_tac 2); |
|
3275 | 705 |
back();back();back();back(); |
706 |
by (res_inst_tac [("x","schA")] spec 1); |
|
707 |
by (res_inst_tac [("x","schB")] spec 1); |
|
708 |
by (res_inst_tac [("x","tr")] spec 1); |
|
709 |
by (thin_tac' 5 1); |
|
3457 | 710 |
by (rtac less_induct 1); |
3275 | 711 |
by (REPEAT (rtac allI 1)); |
712 |
ren "tr schB schA" 1; |
|
713 |
by (strip_tac 1); |
|
714 |
by (REPEAT (etac conjE 1)); |
|
3071 | 715 |
|
3275 | 716 |
by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1); |
717 |
||
3457 | 718 |
by (rtac (seq_take_lemma RS iffD2 RS spec) 1); |
3275 | 719 |
by (thin_tac' 5 1); |
3071 | 720 |
|
721 |
||
3275 | 722 |
by (case_tac "Finite tr" 1); |
3071 | 723 |
|
3275 | 724 |
(* both sides of this equation are nil *) |
725 |
by (subgoal_tac "schA=nil" 1); |
|
3071 | 726 |
by (Asm_simp_tac 1); |
3275 | 727 |
(* first side: mksch = nil *) |
4098 | 728 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1], |
729 |
simpset())) 1); |
|
3275 | 730 |
(* second side: schA = nil *) |
3071 | 731 |
by (eres_inst_tac [("A","A")] LastActExtimplnil 1); |
732 |
by (Asm_simp_tac 1); |
|
3842 | 733 |
by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1); |
3457 | 734 |
by (assume_tac 1); |
3314 | 735 |
by (Fast_tac 1); |
3275 | 736 |
|
737 |
(* case ~ Finite s *) |
|
3071 | 738 |
|
3275 | 739 |
(* both sides of this equation are UU *) |
740 |
by (subgoal_tac "schA=UU" 1); |
|
741 |
by (Asm_simp_tac 1); |
|
742 |
(* first side: mksch = UU *) |
|
4098 | 743 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU, |
3275 | 744 |
(finiteR_mksch RS mp COMP rev_contrapos), |
745 |
ForallBnAmksch], |
|
4098 | 746 |
simpset())) 1); |
3071 | 747 |
(* schA = UU *) |
748 |
by (eres_inst_tac [("A","A")] LastActExtimplUU 1); |
|
749 |
by (Asm_simp_tac 1); |
|
3842 | 750 |
by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1); |
3457 | 751 |
by (assume_tac 1); |
3314 | 752 |
by (Fast_tac 1); |
3275 | 753 |
|
754 |
(* case" ~ Forall (%x.x:act B & x~:act A) s" *) |
|
755 |
||
3457 | 756 |
by (dtac divide_Seq3 1); |
3071 | 757 |
|
3275 | 758 |
by (REPEAT (etac exE 1)); |
759 |
by (REPEAT (etac conjE 1)); |
|
760 |
by (hyp_subst_tac 1); |
|
3071 | 761 |
|
3275 | 762 |
(* bring in lemma reduceA_mksch *) |
763 |
by (forw_inst_tac [("x","schB"),("xa","schA"),("A","A"),("B","B")] reduceA_mksch 1); |
|
3071 | 764 |
by (REPEAT (atac 1)); |
765 |
by (REPEAT (etac exE 1)); |
|
766 |
by (REPEAT (etac conjE 1)); |
|
767 |
||
3275 | 768 |
(* use reduceA_mksch to rewrite conclusion *) |
3071 | 769 |
by (hyp_subst_tac 1); |
770 |
by (Asm_full_simp_tac 1); |
|
771 |
||
772 |
(* eliminate the B-only prefix *) |
|
3275 | 773 |
|
3842 | 774 |
by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1); |
3457 | 775 |
by (etac ForallQFilterPnil 2); |
776 |
by (assume_tac 2); |
|
3275 | 777 |
by (Fast_tac 2); |
778 |
||
779 |
(* Now real recursive step follows (in y) *) |
|
3071 | 780 |
|
3275 | 781 |
by (Asm_full_simp_tac 1); |
782 |
by (case_tac "x:act A" 1); |
|
783 |
by (case_tac "x~:act B" 1); |
|
3071 | 784 |
by (rotate_tac ~2 1); |
3275 | 785 |
by (Asm_full_simp_tac 1); |
3071 | 786 |
|
3275 | 787 |
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); |
3071 | 788 |
by (rotate_tac ~1 1); |
789 |
by (Asm_full_simp_tac 1); |
|
790 |
(* eliminate introduced subgoal 2 *) |
|
3457 | 791 |
by (etac ForallQFilterPnil 2); |
792 |
by (assume_tac 2); |
|
3071 | 793 |
by (Fast_tac 2); |
794 |
||
3275 | 795 |
(* bring in divide Seq for s *) |
796 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
797 |
by (REPEAT (etac conjE 1)); |
|
798 |
||
799 |
(* subst divide_Seq in conclusion, but only at the righest occurence *) |
|
800 |
by (res_inst_tac [("t","schA")] ssubst 1); |
|
801 |
back(); |
|
802 |
back(); |
|
803 |
back(); |
|
3457 | 804 |
by (assume_tac 1); |
3275 | 805 |
|
806 |
(* reduce trace_takes from n to strictly smaller k *) |
|
3457 | 807 |
by (rtac take_reduction 1); |
3275 | 808 |
|
809 |
(* f A (tw iA) = tw ~eA *) |
|
4098 | 810 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act, |
3275 | 811 |
not_ext_is_int_or_not_act]) 1); |
3457 | 812 |
by (rtac refl 1); |
4098 | 813 |
by (asm_full_simp_tac (simpset() addsimps [int_is_act, |
3275 | 814 |
not_ext_is_int_or_not_act]) 1); |
815 |
by (rotate_tac ~11 1); |
|
816 |
||
817 |
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *) |
|
3071 | 818 |
|
3275 | 819 |
(* assumption Forall tr *) |
4098 | 820 |
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1); |
3275 | 821 |
(* assumption schB *) |
4098 | 822 |
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1); |
3275 | 823 |
by (REPEAT (etac conjE 1)); |
824 |
(* assumption schA *) |
|
825 |
by (dres_inst_tac [("x","schA"), |
|
826 |
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); |
|
3457 | 827 |
by (assume_tac 1); |
4098 | 828 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1); |
3275 | 829 |
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) |
830 |
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1); |
|
831 |
by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1); |
|
3457 | 832 |
by (assume_tac 1); |
3275 | 833 |
|
834 |
(* assumption Forall schA *) |
|
835 |
by (dres_inst_tac [("s","schA"), |
|
3842 | 836 |
("P","Forall (%x. x:act A)")] subst 1); |
3457 | 837 |
by (assume_tac 1); |
4098 | 838 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1); |
3275 | 839 |
|
840 |
(* case x:actions(asig_of A) & x: actions(asig_of B) *) |
|
841 |
||
842 |
||
843 |
by (rotate_tac ~2 1); |
|
844 |
by (Asm_full_simp_tac 1); |
|
845 |
||
846 |
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); |
|
847 |
by (rotate_tac ~1 1); |
|
848 |
by (Asm_full_simp_tac 1); |
|
849 |
(* eliminate introduced subgoal 2 *) |
|
3457 | 850 |
by (etac ForallQFilterPnil 2); |
851 |
by (assume_tac 2); |
|
3275 | 852 |
by (Fast_tac 2); |
853 |
||
854 |
(* bring in divide Seq for s *) |
|
855 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
856 |
by (REPEAT (etac conjE 1)); |
|
857 |
||
858 |
(* subst divide_Seq in conclusion, but only at the righest occurence *) |
|
3071 | 859 |
by (res_inst_tac [("t","schA")] ssubst 1); |
860 |
back(); |
|
861 |
back(); |
|
862 |
back(); |
|
3457 | 863 |
by (assume_tac 1); |
3275 | 864 |
|
865 |
(* f A (tw iA) = tw ~eA *) |
|
4098 | 866 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act, |
3275 | 867 |
not_ext_is_int_or_not_act]) 1); |
3071 | 868 |
|
3275 | 869 |
(* rewrite assumption forall and schB *) |
870 |
by (rotate_tac 13 1); |
|
4098 | 871 |
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1); |
3275 | 872 |
|
873 |
(* divide_Seq for schB2 *) |
|
874 |
by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1); |
|
3071 | 875 |
by (REPEAT (etac conjE 1)); |
876 |
(* assumption schA *) |
|
877 |
by (dres_inst_tac [("x","schA"), |
|
3275 | 878 |
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); |
3457 | 879 |
by (assume_tac 1); |
4098 | 880 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1); |
3275 | 881 |
|
882 |
(* f A (tw iB schB2) = nil *) |
|
4098 | 883 |
by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act, |
3275 | 884 |
FilterPTakewhileQnil,intA_is_not_actB]) 1); |
885 |
||
886 |
||
887 |
(* reduce trace_takes from n to strictly smaller k *) |
|
3457 | 888 |
by (rtac take_reduction 1); |
889 |
by (rtac refl 1); |
|
890 |
by (rtac refl 1); |
|
3275 | 891 |
|
892 |
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *) |
|
893 |
||
894 |
(* assumption schB *) |
|
895 |
by (dres_inst_tac [("x","y2"), |
|
896 |
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); |
|
3457 | 897 |
by (assume_tac 1); |
4098 | 898 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1); |
3275 | 899 |
|
900 |
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) |
|
901 |
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1); |
|
902 |
by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1); |
|
3457 | 903 |
by (assume_tac 1); |
3275 | 904 |
by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1); |
905 |
||
906 |
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *) |
|
4098 | 907 |
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1); |
3275 | 908 |
|
909 |
(* case x~:A & x:B *) |
|
910 |
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *) |
|
911 |
by (case_tac "x:act B" 1); |
|
912 |
by (Fast_tac 1); |
|
913 |
||
914 |
(* case x~:A & x~:B *) |
|
915 |
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *) |
|
916 |
by (rotate_tac ~9 1); |
|
917 |
(* reduce forall assumption from tr to (x>>rs) *) |
|
4098 | 918 |
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1); |
3071 | 919 |
by (REPEAT (etac conjE 1)); |
4098 | 920 |
by (fast_tac (claset() addSIs [ext_is_act]) 1); |
3275 | 921 |
|
922 |
qed"FilterAmksch_is_schA"; |
|
923 |
||
924 |
||
925 |
||
926 |
(*--------------------------------------------------------------------------- *) |
|
927 |
||
928 |
section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"; |
|
929 |
||
930 |
(* --------------------------------------------------------------------------- *) |
|
931 |
||
932 |
||
933 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
934 |
goal thy "!! A B. [| compatible A B; compatible B A; \ |
3275 | 935 |
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
3842 | 936 |
\ Forall (%x. x:ext (A||B)) tr & \ |
937 |
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \ |
|
938 |
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\ |
|
939 |
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\ |
|
3275 | 940 |
\ LastActExtsch A schA & LastActExtsch B schB \ |
3842 | 941 |
\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB"; |
3275 | 942 |
|
943 |
by (strip_tac 1); |
|
4042 | 944 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 945 |
by (rtac mp 1); |
946 |
by (assume_tac 2); |
|
3275 | 947 |
back();back();back();back(); |
948 |
by (res_inst_tac [("x","schA")] spec 1); |
|
949 |
by (res_inst_tac [("x","schB")] spec 1); |
|
950 |
by (res_inst_tac [("x","tr")] spec 1); |
|
951 |
by (thin_tac' 5 1); |
|
3457 | 952 |
by (rtac less_induct 1); |
3275 | 953 |
by (REPEAT (rtac allI 1)); |
954 |
ren "tr schB schA" 1; |
|
955 |
by (strip_tac 1); |
|
956 |
by (REPEAT (etac conjE 1)); |
|
957 |
||
958 |
by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1); |
|
959 |
||
3457 | 960 |
by (rtac (seq_take_lemma RS iffD2 RS spec) 1); |
3275 | 961 |
by (thin_tac' 5 1); |
962 |
||
963 |
||
964 |
by (case_tac "Finite tr" 1); |
|
965 |
||
966 |
(* both sides of this equation are nil *) |
|
967 |
by (subgoal_tac "schB=nil" 1); |
|
968 |
by (Asm_simp_tac 1); |
|
969 |
(* first side: mksch = nil *) |
|
4098 | 970 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1], |
971 |
simpset())) 1); |
|
3275 | 972 |
(* second side: schA = nil *) |
973 |
by (eres_inst_tac [("A","B")] LastActExtimplnil 1); |
|
974 |
by (Asm_simp_tac 1); |
|
3842 | 975 |
by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1); |
3457 | 976 |
by (assume_tac 1); |
3314 | 977 |
by (Fast_tac 1); |
3275 | 978 |
|
979 |
(* case ~ Finite tr *) |
|
980 |
||
981 |
(* both sides of this equation are UU *) |
|
982 |
by (subgoal_tac "schB=UU" 1); |
|
983 |
by (Asm_simp_tac 1); |
|
984 |
(* first side: mksch = UU *) |
|
4098 | 985 |
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU, |
3275 | 986 |
(finiteR_mksch RS mp COMP rev_contrapos), |
987 |
ForallAnBmksch], |
|
4098 | 988 |
simpset())) 1); |
3275 | 989 |
(* schA = UU *) |
990 |
by (eres_inst_tac [("A","B")] LastActExtimplUU 1); |
|
991 |
by (Asm_simp_tac 1); |
|
3842 | 992 |
by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1); |
3457 | 993 |
by (assume_tac 1); |
3314 | 994 |
by (Fast_tac 1); |
3275 | 995 |
|
996 |
(* case" ~ Forall (%x.x:act B & x~:act A) s" *) |
|
997 |
||
3457 | 998 |
by (dtac divide_Seq3 1); |
3275 | 999 |
|
1000 |
by (REPEAT (etac exE 1)); |
|
1001 |
by (REPEAT (etac conjE 1)); |
|
1002 |
by (hyp_subst_tac 1); |
|
1003 |
||
1004 |
(* bring in lemma reduceB_mksch *) |
|
1005 |
by (forw_inst_tac [("y","schB"),("x","schA"),("A","A"),("B","B")] reduceB_mksch 1); |
|
1006 |
by (REPEAT (atac 1)); |
|
1007 |
by (REPEAT (etac exE 1)); |
|
1008 |
by (REPEAT (etac conjE 1)); |
|
1009 |
||
1010 |
(* use reduceB_mksch to rewrite conclusion *) |
|
1011 |
by (hyp_subst_tac 1); |
|
1012 |
by (Asm_full_simp_tac 1); |
|
1013 |
||
1014 |
(* eliminate the A-only prefix *) |
|
1015 |
||
3842 | 1016 |
by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1); |
3457 | 1017 |
by (etac ForallQFilterPnil 2); |
1018 |
by (assume_tac 2); |
|
3275 | 1019 |
by (Fast_tac 2); |
1020 |
||
1021 |
(* Now real recursive step follows (in x) *) |
|
1022 |
||
1023 |
by (Asm_full_simp_tac 1); |
|
1024 |
by (case_tac "x:act B" 1); |
|
1025 |
by (case_tac "x~:act A" 1); |
|
1026 |
by (rotate_tac ~2 1); |
|
3071 | 1027 |
by (Asm_full_simp_tac 1); |
1028 |
||
3275 | 1029 |
by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1); |
3071 | 1030 |
by (rotate_tac ~1 1); |
1031 |
by (Asm_full_simp_tac 1); |
|
1032 |
(* eliminate introduced subgoal 2 *) |
|
3457 | 1033 |
by (etac ForallQFilterPnil 2); |
1034 |
by (assume_tac 2); |
|
3071 | 1035 |
by (Fast_tac 2); |
1036 |
||
3275 | 1037 |
(* bring in divide Seq for s *) |
1038 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
1039 |
by (REPEAT (etac conjE 1)); |
|
3071 | 1040 |
|
3275 | 1041 |
(* subst divide_Seq in conclusion, but only at the righest occurence *) |
1042 |
by (res_inst_tac [("t","schB")] ssubst 1); |
|
3071 | 1043 |
back(); |
1044 |
back(); |
|
1045 |
back(); |
|
3457 | 1046 |
by (assume_tac 1); |
3275 | 1047 |
|
1048 |
(* reduce trace_takes from n to strictly smaller k *) |
|
3457 | 1049 |
by (rtac take_reduction 1); |
3275 | 1050 |
|
1051 |
(* f B (tw iB) = tw ~eB *) |
|
4098 | 1052 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act, |
3275 | 1053 |
not_ext_is_int_or_not_act]) 1); |
3457 | 1054 |
by (rtac refl 1); |
4098 | 1055 |
by (asm_full_simp_tac (simpset() addsimps [int_is_act, |
3275 | 1056 |
not_ext_is_int_or_not_act]) 1); |
1057 |
by (rotate_tac ~11 1); |
|
1058 |
||
1059 |
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *) |
|
1060 |
||
1061 |
(* assumption Forall tr *) |
|
4098 | 1062 |
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1); |
3275 | 1063 |
(* assumption schA *) |
4098 | 1064 |
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1); |
3071 | 1065 |
by (REPEAT (etac conjE 1)); |
3275 | 1066 |
(* assumption schB *) |
1067 |
by (dres_inst_tac [("x","schB"), |
|
1068 |
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); |
|
3457 | 1069 |
by (assume_tac 1); |
4098 | 1070 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1); |
3275 | 1071 |
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) |
1072 |
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1); |
|
1073 |
by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1); |
|
3457 | 1074 |
by (assume_tac 1); |
3275 | 1075 |
|
1076 |
(* assumption Forall schB *) |
|
1077 |
by (dres_inst_tac [("s","schB"), |
|
3842 | 1078 |
("P","Forall (%x. x:act B)")] subst 1); |
3457 | 1079 |
by (assume_tac 1); |
4098 | 1080 |
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1); |
3275 | 1081 |
|
1082 |
(* case x:actions(asig_of A) & x: actions(asig_of B) *) |
|
1083 |
||
1084 |
||
1085 |
by (rotate_tac ~2 1); |
|
1086 |
by (Asm_full_simp_tac 1); |
|
1087 |
||
1088 |
by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1); |
|
1089 |
by (rotate_tac ~1 1); |
|
1090 |
by (Asm_full_simp_tac 1); |
|
1091 |
(* eliminate introduced subgoal 2 *) |
|
3457 | 1092 |
by (etac ForallQFilterPnil 2); |
1093 |
by (assume_tac 2); |
|
3275 | 1094 |
by (Fast_tac 2); |
1095 |
||
1096 |
(* bring in divide Seq for s *) |
|
1097 |
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); |
|
3071 | 1098 |
by (REPEAT (etac conjE 1)); |
1099 |
||
3275 | 1100 |
(* subst divide_Seq in conclusion, but only at the righest occurence *) |
1101 |
by (res_inst_tac [("t","schB")] ssubst 1); |
|
1102 |
back(); |
|
1103 |
back(); |
|
1104 |
back(); |
|
3457 | 1105 |
by (assume_tac 1); |
3275 | 1106 |
|
1107 |
(* f B (tw iB) = tw ~eB *) |
|
4098 | 1108 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act, |
3275 | 1109 |
not_ext_is_int_or_not_act]) 1); |
1110 |
||
1111 |
(* rewrite assumption forall and schB *) |
|
1112 |
by (rotate_tac 13 1); |
|
4098 | 1113 |
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1); |
3275 | 1114 |
|
1115 |
(* divide_Seq for schB2 *) |
|
1116 |
by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1); |
|
1117 |
by (REPEAT (etac conjE 1)); |
|
1118 |
(* assumption schA *) |
|
1119 |
by (dres_inst_tac [("x","schB"), |
|
1120 |
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); |
|
3457 | 1121 |
by (assume_tac 1); |
4098 | 1122 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1); |
3275 | 1123 |
|
1124 |
(* f B (tw iA schA2) = nil *) |
|
4098 | 1125 |
by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act, |
3275 | 1126 |
FilterPTakewhileQnil,intA_is_not_actB]) 1); |
1127 |
||
1128 |
||
1129 |
(* reduce trace_takes from n to strictly smaller k *) |
|
3457 | 1130 |
by (rtac take_reduction 1); |
1131 |
by (rtac refl 1); |
|
1132 |
by (rtac refl 1); |
|
3275 | 1133 |
|
1134 |
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *) |
|
1135 |
||
1136 |
(* assumption schA *) |
|
1137 |
by (dres_inst_tac [("x","x2"), |
|
1138 |
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); |
|
3457 | 1139 |
by (assume_tac 1); |
4098 | 1140 |
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1); |
3275 | 1141 |
|
1142 |
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) |
|
1143 |
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1); |
|
1144 |
by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1); |
|
3457 | 1145 |
by (assume_tac 1); |
3275 | 1146 |
by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1); |
1147 |
||
1148 |
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *) |
|
4098 | 1149 |
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1); |
3275 | 1150 |
|
1151 |
(* case x~:B & x:A *) |
|
3071 | 1152 |
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *) |
3275 | 1153 |
by (case_tac "x:act A" 1); |
3071 | 1154 |
by (Fast_tac 1); |
1155 |
||
3275 | 1156 |
(* case x~:B & x~:A *) |
1157 |
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *) |
|
1158 |
by (rotate_tac ~9 1); |
|
1159 |
(* reduce forall assumption from tr to (x>>rs) *) |
|
4098 | 1160 |
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1); |
3071 | 1161 |
by (REPEAT (etac conjE 1)); |
4098 | 1162 |
by (fast_tac (claset() addSIs [ext_is_act]) 1); |
3071 | 1163 |
|
3275 | 1164 |
qed"FilterBmksch_is_schB"; |
3071 | 1165 |
|
1166 |
||
1167 |
||
1168 |
(* ------------------------------------------------------------------ *) |
|
3275 | 1169 |
section"COMPOSITIONALITY on TRACE Level -- Main Theorem"; |
3071 | 1170 |
(* ------------------------------------------------------------------ *) |
1171 |
||
1172 |
goal thy |
|
3521 | 1173 |
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \ |
3071 | 1174 |
\ is_asig(asig_of A); is_asig(asig_of B)|] \ |
3275 | 1175 |
\ ==> tr: traces(A||B) = \ |
3842 | 1176 |
\ (Filter (%a. a:act A)`tr : traces A &\ |
1177 |
\ Filter (%a. a:act B)`tr : traces B &\ |
|
3275 | 1178 |
\ Forall (%x. x:ext(A||B)) tr)"; |
3071 | 1179 |
|
4098 | 1180 |
by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1); |
3071 | 1181 |
by (safe_tac set_cs); |
1182 |
||
1183 |
(* ==> *) |
|
1184 |
(* There is a schedule of A *) |
|
3842 | 1185 |
by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1); |
4098 | 1186 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); |
1187 |
by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1, |
|
3071 | 1188 |
externals_of_par,ext1_ext2_is_not_act1]) 1); |
1189 |
(* There is a schedule of B *) |
|
3842 | 1190 |
by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1); |
4098 | 1191 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); |
1192 |
by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2, |
|
3071 | 1193 |
externals_of_par,ext1_ext2_is_not_act2]) 1); |
1194 |
(* Traces of A||B have only external actions from A or B *) |
|
3457 | 1195 |
by (rtac ForallPFilterP 1); |
3071 | 1196 |
|
1197 |
(* <== *) |
|
1198 |
||
3275 | 1199 |
(* replace schA and schB by Cut(schA) and Cut(schB) *) |
3071 | 1200 |
by (dtac exists_LastActExtsch 1); |
3457 | 1201 |
by (assume_tac 1); |
3071 | 1202 |
by (dtac exists_LastActExtsch 1); |
3457 | 1203 |
by (assume_tac 1); |
3071 | 1204 |
by (REPEAT (etac exE 1)); |
1205 |
by (REPEAT (etac conjE 1)); |
|
3275 | 1206 |
(* Schedules of A(B) have only actions of A(B) *) |
3457 | 1207 |
by (dtac scheds_in_sig 1); |
1208 |
by (assume_tac 1); |
|
1209 |
by (dtac scheds_in_sig 1); |
|
1210 |
by (assume_tac 1); |
|
3071 | 1211 |
|
3275 | 1212 |
ren "h1 h2 schA schB" 1; |
3071 | 1213 |
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr, |
1214 |
we need here *) |
|
3275 | 1215 |
by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1); |
3071 | 1216 |
|
1217 |
(* External actions of mksch are just the oracle *) |
|
4098 | 1218 |
by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1); |
3071 | 1219 |
|
1220 |
(* mksch is a schedule -- use compositionality on sch-level *) |
|
4098 | 1221 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 1); |
1222 |
by (asm_full_simp_tac (simpset() addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1); |
|
3457 | 1223 |
by (etac ForallAorB_mksch 1); |
1224 |
by (etac ForallPForallQ 1); |
|
1225 |
by (etac ext_is_act 1); |
|
3275 | 1226 |
qed"compositionality_tr"; |
3071 | 1227 |
|
1228 |
||
1229 |
||
3521 | 1230 |
(* ------------------------------------------------------------------ *) |
1231 |
(* COMPOSITIONALITY on TRACE Level *) |
|
1232 |
(* For Modules *) |
|
1233 |
(* ------------------------------------------------------------------ *) |
|
1234 |
||
1235 |
goalw thy [Traces_def,par_traces_def] |
|
1236 |
||
1237 |
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \ |
|
1238 |
\ is_asig(asig_of A); is_asig(asig_of B)|] \ |
|
1239 |
\==> Traces (A||B) = par_traces (Traces A) (Traces B)"; |
|
1240 |
||
4098 | 1241 |
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1); |
4423 | 1242 |
by (rtac set_ext 1); |
4098 | 1243 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1); |
3521 | 1244 |
qed"compositionality_tr_modules"; |
3071 | 1245 |
|
1246 |
||
1247 |
||
1248 |
||
1249 |
||
1250 |
||
3521 | 1251 |