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