3071

1 
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy

3275

2 
ID: $Id$

12218

3 
Author: Olaf Müller

3071

4 
*)


5 

17233

6 
header {* Compositionality on Trace level *}


7 


8 
theory CompoTraces


9 
imports CompoScheds ShortExecutions


10 
begin

3071

11 


12 


13 
consts


14 

3521

15 
mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq > 'a Seq > 'a Seq > 'a Seq"


16 
par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"

3071

17 


18 
defs


19 

17233

20 
mksch_def:

10835

21 
"mksch A B == (fix$(LAM h tr schA schB. case tr of

3071

22 
nil => nil


23 
 x##xs =>


24 
(case x of

12028

25 
UU => UU

3071

26 
 Def y =>


27 
(if y:act A then


28 
(if y:act B then

10835

29 
((Takewhile (%a. a:int A)$schA)


30 
@@ (Takewhile (%a. a:int B)$schB)


31 
@@ (y>>(h$xs


32 
$(TL$(Dropwhile (%a. a:int A)$schA))


33 
$(TL$(Dropwhile (%a. a:int B)$schB))

3071

34 
)))


35 
else

10835

36 
((Takewhile (%a. a:int A)$schA)


37 
@@ (y>>(h$xs


38 
$(TL$(Dropwhile (%a. a:int A)$schA))


39 
$schB)))

3071

40 
)


41 
else


42 
(if y:act B then

10835

43 
((Takewhile (%a. a:int B)$schB)


44 
@@ (y>>(h$xs


45 
$schA


46 
$(TL$(Dropwhile (%a. a:int B)$schB))

3071

47 
)))


48 
else


49 
UU


50 
)


51 
)


52 
)))"


53 


54 

17233

55 
par_traces_def:

3521

56 
"par_traces TracesA TracesB ==


57 
let trA = fst TracesA; sigA = snd TracesA;


58 
trB = fst TracesB; sigB = snd TracesB


59 
in

10835

60 
( {tr. Filter (%a. a:actions sigA)$tr : trA}


61 
Int {tr. Filter (%a. a:actions sigB)$tr : trB}

3521

62 
Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},


63 
asig_comp sigA sigB)"


64 

17233

65 
axioms

3071

66 

17233

67 
finiteR_mksch:

10835

68 
"Finite (mksch A B$tr$x$y) > Finite tr"

3071

69 

19741

70 

26339

71 
declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}

19741

72 


73 


74 
subsection "mksch rewrite rules"


75 


76 
lemma mksch_unfold:


77 
"mksch A B = (LAM tr schA schB. case tr of


78 
nil => nil


79 
 x##xs =>


80 
(case x of


81 
UU => UU


82 
 Def y =>


83 
(if y:act A then


84 
(if y:act B then


85 
((Takewhile (%a. a:int A)$schA)


86 
@@(Takewhile (%a. a:int B)$schB)


87 
@@(y>>(mksch A B$xs


88 
$(TL$(Dropwhile (%a. a:int A)$schA))


89 
$(TL$(Dropwhile (%a. a:int B)$schB))


90 
)))


91 
else


92 
((Takewhile (%a. a:int A)$schA)


93 
@@ (y>>(mksch A B$xs


94 
$(TL$(Dropwhile (%a. a:int A)$schA))


95 
$schB)))


96 
)


97 
else


98 
(if y:act B then


99 
((Takewhile (%a. a:int B)$schB)


100 
@@ (y>>(mksch A B$xs


101 
$schA


102 
$(TL$(Dropwhile (%a. a:int B)$schB))


103 
)))


104 
else


105 
UU


106 
)


107 
)


108 
))"


109 
apply (rule trans)


110 
apply (rule fix_eq2)


111 
apply (rule mksch_def)


112 
apply (rule beta_cfun)


113 
apply simp


114 
done


115 


116 
lemma mksch_UU: "mksch A B$UU$schA$schB = UU"


117 
apply (subst mksch_unfold)


118 
apply simp


119 
done


120 


121 
lemma mksch_nil: "mksch A B$nil$schA$schB = nil"


122 
apply (subst mksch_unfold)


123 
apply simp


124 
done


125 


126 
lemma mksch_cons1: "[x:act A;x~:act B]


127 
==> mksch A B$(x>>tr)$schA$schB =


128 
(Takewhile (%a. a:int A)$schA)


129 
@@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))


130 
$schB))"


131 
apply (rule trans)


132 
apply (subst mksch_unfold)


133 
apply (simp add: Consq_def If_and_if)


134 
apply (simp add: Consq_def)


135 
done


136 


137 
lemma mksch_cons2: "[x~:act A;x:act B]


138 
==> mksch A B$(x>>tr)$schA$schB =


139 
(Takewhile (%a. a:int B)$schB)


140 
@@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))


141 
))"


142 
apply (rule trans)


143 
apply (subst mksch_unfold)


144 
apply (simp add: Consq_def If_and_if)


145 
apply (simp add: Consq_def)


146 
done


147 


148 
lemma mksch_cons3: "[x:act A;x:act B]


149 
==> mksch A B$(x>>tr)$schA$schB =


150 
(Takewhile (%a. a:int A)$schA)


151 
@@ ((Takewhile (%a. a:int B)$schB)


152 
@@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))


153 
$(TL$(Dropwhile (%a. a:int B)$schB))))


154 
)"


155 
apply (rule trans)


156 
apply (subst mksch_unfold)


157 
apply (simp add: Consq_def If_and_if)


158 
apply (simp add: Consq_def)


159 
done


160 


161 
lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3


162 


163 
declare compotr_simps [simp]


164 


165 


166 
subsection {* COMPOSITIONALITY on TRACE Level *}


167 


168 
subsubsection "Lemmata for ==>"


169 


170 
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of


171 
the compatibility of IOA, in particular out of the condition that internals are


172 
really hidden. *)


173 


174 
lemma compatibility_consequence1: "(eB & ~eA > ~A) >


175 
(A & (eA  eB)) = (eA & A)"


176 
apply fast


177 
done


178 


179 


180 
(* very similar to above, only the commutativity of  is used to make a slight change *)


181 


182 
lemma compatibility_consequence2: "(eB & ~eA > ~A) >


183 
(A & (eB  eA)) = (eA & A)"


184 
apply fast


185 
done


186 


187 


188 
subsubsection "Lemmata for <=="


189 


190 
(* Lemma for substitution of looping assumption in another specific assumption *)


191 
lemma subst_lemma1: "[ f << (g x) ; x=(h x) ] ==> f << g (h x)"


192 
by (erule subst)


193 


194 
(* Lemma for substitution of looping assumption in another specific assumption *)


195 
lemma subst_lemma2: "[ (f x) = y >> g; x=(h x) ] ==> (f (h x)) = y >> g"


196 
by (erule subst)


197 


198 
lemma ForallAorB_mksch [rule_format]:


199 
"!!A B. compatible A B ==>


200 
! schA schB. Forall (%x. x:act (AB)) tr


201 
> Forall (%x. x:act (AB)) (mksch A B$tr$schA$schB)"


202 
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})


203 
apply (tactic "safe_tac set_cs")


204 
apply (simp add: actions_of_par)


205 
apply (case_tac "a:act A")


206 
apply (case_tac "a:act B")


207 
(* a:A, a:B *)


208 
apply simp


209 
apply (rule Forall_Conc_impl [THEN mp])


210 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


211 
apply (rule Forall_Conc_impl [THEN mp])


212 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


213 
(* a:A,a~:B *)


214 
apply simp


215 
apply (rule Forall_Conc_impl [THEN mp])


216 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


217 
apply (case_tac "a:act B")


218 
(* a~:A, a:B *)


219 
apply simp


220 
apply (rule Forall_Conc_impl [THEN mp])


221 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


222 
(* a~:A,a~:B *)


223 
apply auto


224 
done


225 


226 
lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>


227 
! schA schB. (Forall (%x. x:act B & x~:act A) tr


228 
> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"


229 
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})


230 
apply (tactic "safe_tac set_cs")


231 
apply (rule Forall_Conc_impl [THEN mp])


232 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


233 
done


234 


235 
lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>


236 
! schA schB. (Forall (%x. x:act A & x~:act B) tr


237 
> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"


238 
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})


239 
apply (tactic "safe_tac set_cs")


240 
apply simp


241 
apply (rule Forall_Conc_impl [THEN mp])


242 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


243 
done


244 


245 
(* safetac makes too many case distinctions with this lemma in the next proof *)


246 
declare FiniteConc [simp del]


247 


248 
lemma FiniteL_mksch [rule_format (no_asm)]: "[ Finite tr; is_asig(asig_of A); is_asig(asig_of B) ] ==>


249 
! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &


250 
Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &


251 
Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &


252 
Forall (%x. x:ext (AB)) tr


253 
> Finite (mksch A B$tr$x$y)"


254 


255 
apply (erule Seq_Finite_ind)


256 
apply simp


257 
(* main case *)


258 
apply simp


259 
apply (tactic "safe_tac set_cs")


260 


261 
(* a: act A; a: act B *)


262 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


263 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


264 
back


265 
apply (erule conjE)+


266 
(* Finite (tw iA x) and Finite (tw iB y) *)


267 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


268 
(* now for conclusion IH applicable, but assumptions have to be transformed *)


269 
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)


270 
apply assumption


271 
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)


272 
apply assumption


273 
(* IH *)


274 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


275 


276 
(* a: act B; a~: act A *)


277 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


278 


279 
apply (erule conjE)+


280 
(* Finite (tw iB y) *)


281 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


282 
(* now for conclusion IH applicable, but assumptions have to be transformed *)


283 
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)


284 
apply assumption


285 
(* IH *)


286 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


287 


288 
(* a~: act B; a: act A *)


289 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


290 


291 
apply (erule conjE)+


292 
(* Finite (tw iA x) *)


293 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


294 
(* now for conclusion IH applicable, but assumptions have to be transformed *)


295 
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)


296 
apply assumption


297 
(* IH *)


298 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


299 


300 
(* a~: act B; a~: act A *)


301 
apply (fastsimp intro!: ext_is_act simp: externals_of_par)


302 
done


303 


304 
declare FiniteConc [simp]


305 


306 
declare FilterConc [simp del]


307 


308 
lemma reduceA_mksch1 [rule_format (no_asm)]: " [ Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B] ==>


309 
! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &


310 
Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)


311 
> (? y1 y2. (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &


312 
Forall (%x. x:act B & x~:act A) y1 &


313 
Finite y1 & y = (y1 @@ y2) &


314 
Filter (%a. a:ext B)$y1 = bs)"


315 
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])


316 
apply (erule Seq_Finite_ind)


317 
apply (rule allI)+


318 
apply (rule impI)


319 
apply (rule_tac x = "nil" in exI)


320 
apply (rule_tac x = "y" in exI)


321 
apply simp


322 
(* main case *)


323 
apply (rule allI)+


324 
apply (rule impI)


325 
apply simp


326 
apply (erule conjE)+


327 
apply simp


328 
(* divide_Seq on s *)


329 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


330 
apply (erule conjE)+


331 
(* transform assumption f eB y = f B (s@z) *)


332 
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)


333 
apply assumption


334 
apply (simp add: not_ext_is_int_or_not_act FilterConc)


335 
(* apply IH *)


336 
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)


337 
apply (simp add: ForallTL ForallDropwhile FilterConc)


338 
apply (erule exE)+


339 
apply (erule conjE)+


340 
apply (simp add: FilterConc)


341 
(* for replacing IH in conclusion *)


342 
apply (rotate_tac 2)


343 
(* instantiate y1a and y2a *)


344 
apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)


345 
apply (rule_tac x = "y2" in exI)


346 
(* elminate all obligations up to two depending on Conc_assoc *)


347 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)


348 
apply (simp (no_asm) add: Conc_assoc FilterConc)


349 
done


350 


351 
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]


352 


353 
declare FilterConc [simp del]


354 


355 
lemma reduceB_mksch1 [rule_format]:


356 
" [ Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B] ==>


357 
! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &


358 
Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)


359 
> (? x1 x2. (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &


360 
Forall (%x. x:act A & x~:act B) x1 &


361 
Finite x1 & x = (x1 @@ x2) &


362 
Filter (%a. a:ext A)$x1 = a_s)"


363 
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])


364 
apply (erule Seq_Finite_ind)


365 
apply (rule allI)+


366 
apply (rule impI)


367 
apply (rule_tac x = "nil" in exI)


368 
apply (rule_tac x = "x" in exI)


369 
apply simp


370 
(* main case *)


371 
apply (rule allI)+


372 
apply (rule impI)


373 
apply simp


374 
apply (erule conjE)+


375 
apply simp


376 
(* divide_Seq on s *)


377 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


378 
apply (erule conjE)+


379 
(* transform assumption f eA x = f A (s@z) *)


380 
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)


381 
apply assumption


382 
apply (simp add: not_ext_is_int_or_not_act FilterConc)


383 
(* apply IH *)


384 
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)


385 
apply (simp add: ForallTL ForallDropwhile FilterConc)


386 
apply (erule exE)+


387 
apply (erule conjE)+


388 
apply (simp add: FilterConc)


389 
(* for replacing IH in conclusion *)


390 
apply (rotate_tac 2)


391 
(* instantiate y1a and y2a *)


392 
apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)


393 
apply (rule_tac x = "x2" in exI)


394 
(* elminate all obligations up to two depending on Conc_assoc *)


395 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)


396 
apply (simp (no_asm) add: Conc_assoc FilterConc)


397 
done


398 


399 
lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]


400 


401 
declare FilterConc [simp]


402 


403 


404 
subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"


405 


406 
lemma FilterA_mksch_is_tr:


407 
"!! A B. [ compatible A B; compatible B A;


408 
is_asig(asig_of A); is_asig(asig_of B) ] ==>


409 
! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &


410 
Forall (%x. x:ext (AB)) tr &


411 
Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &


412 
Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB


413 
> Filter (%a. a:ext (AB))$(mksch A B$tr$schA$schB) = tr"


414 


415 
apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})


416 
(* main case *)


417 
(* splitting into 4 cases according to a:A, a:B *)


418 
apply (tactic "safe_tac set_cs")


419 


420 
(* Case a:A, a:B *)


421 
apply (frule divide_Seq)


422 
apply (frule divide_Seq)


423 
back


424 
apply (erule conjE)+


425 
(* filtering internals of A in schA and of B in schB is nil *)


426 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


427 
(* conclusion of IH ok, but assumptions of IH have to be transformed *)


428 
apply (drule_tac x = "schA" in subst_lemma1)


429 
apply assumption


430 
apply (drule_tac x = "schB" in subst_lemma1)


431 
apply assumption


432 
(* IH *)


433 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


434 


435 
(* Case a:A, a~:B *)


436 
apply (frule divide_Seq)


437 
apply (erule conjE)+


438 
(* filtering internals of A is nil *)


439 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


440 
apply (drule_tac x = "schA" in subst_lemma1)


441 
apply assumption


442 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


443 


444 
(* Case a:B, a~:A *)


445 
apply (frule divide_Seq)


446 
apply (erule conjE)+


447 
(* filtering internals of A is nil *)


448 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


449 
apply (drule_tac x = "schB" in subst_lemma1)


450 
back


451 
apply assumption


452 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


453 


454 
(* Case a~:A, a~:B *)


455 
apply (fastsimp intro!: ext_is_act simp: externals_of_par)


456 
done


457 


458 


459 
subsection" Filter of mksch(tr,schA,schB) to A is schA  take lemma proof"


460 


461 
lemma FilterAmksch_is_schA: "!! A B. [ compatible A B; compatible B A;


462 
is_asig(asig_of A); is_asig(asig_of B) ] ==>


463 
Forall (%x. x:ext (AB)) tr &


464 
Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &


465 
Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &


466 
Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &


467 
LastActExtsch A schA & LastActExtsch B schB


468 
> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"


469 
apply (intro strip)


470 
apply (rule seq.take_lemmas)


471 
apply (rule mp)


472 
prefer 2 apply assumption


473 
back back back back


474 
apply (rule_tac x = "schA" in spec)


475 
apply (rule_tac x = "schB" in spec)


476 
apply (rule_tac x = "tr" in spec)


477 
apply (tactic "thin_tac' 5 1")


478 
apply (rule nat_less_induct)


479 
apply (rule allI)+


480 
apply (rename_tac tr schB schA)


481 
apply (intro strip)


482 
apply (erule conjE)+


483 


484 
apply (case_tac "Forall (%x. x:act B & x~:act A) tr")


485 


486 
apply (rule seq_take_lemma [THEN iffD2, THEN spec])


487 
apply (tactic "thin_tac' 5 1")


488 


489 


490 
apply (case_tac "Finite tr")


491 


492 
(* both sides of this equation are nil *)


493 
apply (subgoal_tac "schA=nil")


494 
apply (simp (no_asm_simp))


495 
(* first side: mksch = nil *)


496 
apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]


497 
(* second side: schA = nil *)


498 
apply (erule_tac A = "A" in LastActExtimplnil)


499 
apply (simp (no_asm_simp))


500 
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)


501 
apply assumption


502 
apply fast


503 


504 
(* case ~ Finite s *)


505 


506 
(* both sides of this equation are UU *)


507 
apply (subgoal_tac "schA=UU")


508 
apply (simp (no_asm_simp))


509 
(* first side: mksch = UU *)


510 
apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]


511 
(* schA = UU *)


512 
apply (erule_tac A = "A" in LastActExtimplUU)


513 
apply (simp (no_asm_simp))


514 
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)


515 
apply assumption


516 
apply fast


517 


518 
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)


519 


520 
apply (drule divide_Seq3)


521 


522 
apply (erule exE)+


523 
apply (erule conjE)+


524 
apply hypsubst


525 


526 
(* bring in lemma reduceA_mksch *)


527 
apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)


528 
apply assumption+


529 
apply (erule exE)+


530 
apply (erule conjE)+


531 


532 
(* use reduceA_mksch to rewrite conclusion *)


533 
apply hypsubst


534 
apply simp


535 


536 
(* eliminate the Bonly prefix *)


537 


538 
apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")


539 
apply (erule_tac [2] ForallQFilterPnil)


540 
prefer 2 apply assumption


541 
prefer 2 apply fast


542 


543 
(* Now real recursive step follows (in y) *)


544 


545 
apply simp


546 
apply (case_tac "x:act A")


547 
apply (case_tac "x~:act B")


548 
apply (rotate_tac 2)


549 
apply simp


550 


551 
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")


552 
apply (rotate_tac 1)


553 
apply simp


554 
(* eliminate introduced subgoal 2 *)


555 
apply (erule_tac [2] ForallQFilterPnil)


556 
prefer 2 apply assumption


557 
prefer 2 apply fast


558 


559 
(* bring in divide Seq for s *)


560 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


561 
apply (erule conjE)+


562 


563 
(* subst divide_Seq in conclusion, but only at the righest occurence *)


564 
apply (rule_tac t = "schA" in ssubst)


565 
back


566 
back


567 
back


568 
apply assumption


569 


570 
(* reduce trace_takes from n to strictly smaller k *)


571 
apply (rule take_reduction)


572 


573 
(* f A (tw iA) = tw ~eA *)


574 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


575 
apply (rule refl)


576 
apply (simp add: int_is_act not_ext_is_int_or_not_act)


577 
apply (rotate_tac 11)


578 


579 
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)


580 


581 
(* assumption Forall tr *)


582 
(* assumption schB *)


583 
apply (simp add: Forall_Conc ext_and_act)


584 
(* assumption schA *)


585 
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)


586 
apply assumption


587 
apply (simp add: int_is_not_ext)


588 
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)


589 
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)


590 
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)


591 
apply assumption


592 


593 
(* assumption Forall schA *)


594 
apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)


595 
apply assumption


596 
apply (simp add: ForallPTakewhileQ int_is_act)


597 


598 
(* case x:actions(asig_of A) & x: actions(asig_of B) *)


599 


600 


601 
apply (rotate_tac 2)


602 
apply simp


603 


604 
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")


605 
apply (rotate_tac 1)


606 
apply simp


607 
(* eliminate introduced subgoal 2 *)


608 
apply (erule_tac [2] ForallQFilterPnil)


609 
prefer 2 apply (assumption)


610 
prefer 2 apply (fast)


611 


612 
(* bring in divide Seq for s *)


613 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


614 
apply (erule conjE)+


615 


616 
(* subst divide_Seq in conclusion, but only at the righest occurence *)


617 
apply (rule_tac t = "schA" in ssubst)


618 
back


619 
back


620 
back


621 
apply assumption


622 


623 
(* f A (tw iA) = tw ~eA *)


624 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


625 


626 
(* rewrite assumption forall and schB *)


627 
apply (rotate_tac 13)


628 
apply (simp add: ext_and_act)


629 


630 
(* divide_Seq for schB2 *)


631 
apply (frule_tac y = "y2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


632 
apply (erule conjE)+


633 
(* assumption schA *)


634 
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)


635 
apply assumption


636 
apply (simp add: int_is_not_ext)


637 


638 
(* f A (tw iB schB2) = nil *)


639 
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


640 


641 


642 
(* reduce trace_takes from n to strictly smaller k *)


643 
apply (rule take_reduction)


644 
apply (rule refl)


645 
apply (rule refl)


646 


647 
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)


648 


649 
(* assumption schB *)


650 
apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)


651 
apply assumption


652 
apply (simp add: intA_is_not_actB int_is_not_ext)


653 


654 
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)


655 
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)


656 
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)


657 
apply assumption


658 
apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)


659 


660 
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)


661 
apply (simp add: ForallTL ForallDropwhile)


662 


663 
(* case x~:A & x:B *)


664 
(* cannot occur, as just this case has been scheduled out before as the Bonly prefix *)


665 
apply (case_tac "x:act B")


666 
apply fast


667 


668 
(* case x~:A & x~:B *)


669 
(* cannot occur because of assumption: Forall (a:ext A  a:ext B) *)


670 
apply (rotate_tac 9)


671 
(* reduce forall assumption from tr to (x>>rs) *)


672 
apply (simp add: externals_of_par)


673 
apply (fast intro!: ext_is_act)


674 


675 
done


676 


677 


678 


679 
subsection" Filter of mksch(tr,schA,schB) to B is schB  take lemma proof"


680 


681 
lemma FilterBmksch_is_schB: "!! A B. [ compatible A B; compatible B A;


682 
is_asig(asig_of A); is_asig(asig_of B) ] ==>


683 
Forall (%x. x:ext (AB)) tr &


684 
Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &


685 
Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &


686 
Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &


687 
LastActExtsch A schA & LastActExtsch B schB


688 
> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"


689 
apply (intro strip)


690 
apply (rule seq.take_lemmas)


691 
apply (rule mp)


692 
prefer 2 apply assumption


693 
back back back back


694 
apply (rule_tac x = "schA" in spec)


695 
apply (rule_tac x = "schB" in spec)


696 
apply (rule_tac x = "tr" in spec)


697 
apply (tactic "thin_tac' 5 1")


698 
apply (rule nat_less_induct)


699 
apply (rule allI)+


700 
apply (rename_tac tr schB schA)


701 
apply (intro strip)


702 
apply (erule conjE)+


703 


704 
apply (case_tac "Forall (%x. x:act A & x~:act B) tr")


705 


706 
apply (rule seq_take_lemma [THEN iffD2, THEN spec])


707 
apply (tactic "thin_tac' 5 1")


708 


709 
apply (case_tac "Finite tr")


710 


711 
(* both sides of this equation are nil *)


712 
apply (subgoal_tac "schB=nil")


713 
apply (simp (no_asm_simp))


714 
(* first side: mksch = nil *)


715 
apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]


716 
(* second side: schA = nil *)


717 
apply (erule_tac A = "B" in LastActExtimplnil)


718 
apply (simp (no_asm_simp))


719 
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)


720 
apply assumption


721 
apply fast


722 


723 
(* case ~ Finite tr *)


724 


725 
(* both sides of this equation are UU *)


726 
apply (subgoal_tac "schB=UU")


727 
apply (simp (no_asm_simp))


728 
(* first side: mksch = UU *)


729 
apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)


730 
(* schA = UU *)


731 
apply (erule_tac A = "B" in LastActExtimplUU)


732 
apply (simp (no_asm_simp))


733 
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)


734 
apply assumption


735 
apply fast


736 


737 
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)


738 


739 
apply (drule divide_Seq3)


740 


741 
apply (erule exE)+


742 
apply (erule conjE)+


743 
apply hypsubst


744 


745 
(* bring in lemma reduceB_mksch *)


746 
apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)


747 
apply assumption+


748 
apply (erule exE)+


749 
apply (erule conjE)+


750 


751 
(* use reduceB_mksch to rewrite conclusion *)


752 
apply hypsubst


753 
apply simp


754 


755 
(* eliminate the Aonly prefix *)


756 


757 
apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")


758 
apply (erule_tac [2] ForallQFilterPnil)


759 
prefer 2 apply (assumption)


760 
prefer 2 apply (fast)


761 


762 
(* Now real recursive step follows (in x) *)


763 


764 
apply simp


765 
apply (case_tac "x:act B")


766 
apply (case_tac "x~:act A")


767 
apply (rotate_tac 2)


768 
apply simp


769 


770 
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")


771 
apply (rotate_tac 1)


772 
apply simp


773 
(* eliminate introduced subgoal 2 *)


774 
apply (erule_tac [2] ForallQFilterPnil)


775 
prefer 2 apply (assumption)


776 
prefer 2 apply (fast)


777 


778 
(* bring in divide Seq for s *)


779 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


780 
apply (erule conjE)+


781 


782 
(* subst divide_Seq in conclusion, but only at the righest occurence *)


783 
apply (rule_tac t = "schB" in ssubst)


784 
back


785 
back


786 
back


787 
apply assumption


788 


789 
(* reduce trace_takes from n to strictly smaller k *)


790 
apply (rule take_reduction)


791 


792 
(* f B (tw iB) = tw ~eB *)


793 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


794 
apply (rule refl)


795 
apply (simp add: int_is_act not_ext_is_int_or_not_act)


796 
apply (rotate_tac 11)


797 


798 
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)


799 


800 
(* assumption schA *)


801 
apply (simp add: Forall_Conc ext_and_act)


802 
(* assumption schB *)


803 
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)


804 
apply assumption


805 
apply (simp add: int_is_not_ext)


806 
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)


807 
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)


808 
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)


809 
apply assumption


810 


811 
(* assumption Forall schB *)


812 
apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)


813 
apply assumption


814 
apply (simp add: ForallPTakewhileQ int_is_act)


815 


816 
(* case x:actions(asig_of A) & x: actions(asig_of B) *)


817 


818 
apply (rotate_tac 2)


819 
apply simp


820 


821 
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")


822 
apply (rotate_tac 1)


823 
apply simp


824 
(* eliminate introduced subgoal 2 *)


825 
apply (erule_tac [2] ForallQFilterPnil)


826 
prefer 2 apply (assumption)


827 
prefer 2 apply (fast)


828 


829 
(* bring in divide Seq for s *)


830 
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


831 
apply (erule conjE)+


832 


833 
(* subst divide_Seq in conclusion, but only at the righest occurence *)


834 
apply (rule_tac t = "schB" in ssubst)


835 
back


836 
back


837 
back


838 
apply assumption


839 


840 
(* f B (tw iB) = tw ~eB *)


841 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


842 


843 
(* rewrite assumption forall and schB *)


844 
apply (rotate_tac 13)


845 
apply (simp add: ext_and_act)


846 


847 
(* divide_Seq for schB2 *)


848 
apply (frule_tac y = "x2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])


849 
apply (erule conjE)+


850 
(* assumption schA *)


851 
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)


852 
apply assumption


853 
apply (simp add: int_is_not_ext)


854 


855 
(* f B (tw iA schA2) = nil *)


856 
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


857 


858 


859 
(* reduce trace_takes from n to strictly smaller k *)


860 
apply (rule take_reduction)


861 
apply (rule refl)


862 
apply (rule refl)


863 


864 
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)


865 


866 
(* assumption schA *)


867 
apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)


868 
apply assumption


869 
apply (simp add: intA_is_not_actB int_is_not_ext)


870 


871 
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)


872 
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)


873 
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)


874 
apply assumption


875 
apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)


876 


877 
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)


878 
apply (simp add: ForallTL ForallDropwhile)


879 


880 
(* case x~:B & x:A *)


881 
(* cannot occur, as just this case has been scheduled out before as the Bonly prefix *)


882 
apply (case_tac "x:act A")


883 
apply fast


884 


885 
(* case x~:B & x~:A *)


886 
(* cannot occur because of assumption: Forall (a:ext A  a:ext B) *)


887 
apply (rotate_tac 9)


888 
(* reduce forall assumption from tr to (x>>rs) *)


889 
apply (simp add: externals_of_par)


890 
apply (fast intro!: ext_is_act)


891 


892 
done


893 


894 


895 
subsection "COMPOSITIONALITY on TRACE Level  Main Theorem"


896 


897 
lemma compositionality_tr:


898 
"!! A B. [ is_trans_of A; is_trans_of B; compatible A B; compatible B A;


899 
is_asig(asig_of A); is_asig(asig_of B)]


900 
==> (tr: traces(AB)) =


901 
(Filter (%a. a:act A)$tr : traces A &


902 
Filter (%a. a:act B)$tr : traces B &


903 
Forall (%x. x:ext(AB)) tr)"


904 


905 
apply (simp (no_asm) add: traces_def has_trace_def)


906 
apply (tactic "safe_tac set_cs")


907 


908 
(* ==> *)


909 
(* There is a schedule of A *)


910 
apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)


911 
prefer 2


912 
apply (simp add: compositionality_sch)


913 
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)


914 
(* There is a schedule of B *)


915 
apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)


916 
prefer 2


917 
apply (simp add: compositionality_sch)


918 
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)


919 
(* Traces of AB have only external actions from A or B *)


920 
apply (rule ForallPFilterP)


921 


922 
(* <== *)


923 


924 
(* replace schA and schB by Cut(schA) and Cut(schB) *)


925 
apply (drule exists_LastActExtsch)


926 
apply assumption


927 
apply (drule exists_LastActExtsch)


928 
apply assumption


929 
apply (erule exE)+


930 
apply (erule conjE)+


931 
(* Schedules of A(B) have only actions of A(B) *)


932 
apply (drule scheds_in_sig)


933 
apply assumption


934 
apply (drule scheds_in_sig)


935 
apply assumption


936 


937 
apply (rename_tac h1 h2 schA schB)


938 
(* mksch is exactly the construction of trAB out of schA, schB, and the oracle tr,


939 
we need here *)


940 
apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)


941 


942 
(* External actions of mksch are just the oracle *)


943 
apply (simp add: FilterA_mksch_is_tr)


944 


945 
(* mksch is a schedule  use compositionality on schlevel *)


946 
apply (simp add: compositionality_sch)


947 
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)


948 
apply (erule ForallAorB_mksch)


949 
apply (erule ForallPForallQ)


950 
apply (erule ext_is_act)


951 
done


952 


953 


954 


955 
subsection {* COMPOSITIONALITY on TRACE Level  for Modules *}


956 


957 
lemma compositionality_tr_modules:


958 


959 
"!! A B. [ is_trans_of A; is_trans_of B; compatible A B; compatible B A;


960 
is_asig(asig_of A); is_asig(asig_of B)]


961 
==> Traces (AB) = par_traces (Traces A) (Traces B)"


962 


963 
apply (unfold Traces_def par_traces_def)


964 
apply (simp add: asig_of_par)


965 
apply (rule set_ext)


966 
apply (simp add: compositionality_tr externals_of_par)


967 
done


968 


969 

26339

970 
declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}

3071

971 


972 


973 
end
