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 *})

26359

203 
apply auto

19741

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 *})

26359

230 
apply auto

19741

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 *})

26359

239 
apply auto

19741

240 
apply (rule Forall_Conc_impl [THEN mp])


241 
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)


242 
done


243 


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


245 
declare FiniteConc [simp del]


246 


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


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


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


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


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


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


253 


254 
apply (erule Seq_Finite_ind)


255 
apply simp


256 
(* main case *)


257 
apply simp

26359

258 
apply auto

19741

259 


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


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


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


263 
back


264 
apply (erule conjE)+


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


266 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


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


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


269 
apply assumption


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


271 
apply assumption


272 
(* IH *)


273 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


274 


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


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


277 


278 
apply (erule conjE)+


279 
(* Finite (tw iB y) *)


280 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


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


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


283 
apply assumption


284 
(* IH *)


285 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


286 


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


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


289 


290 
apply (erule conjE)+


291 
(* Finite (tw iA x) *)


292 
apply (simp add: not_ext_is_int_or_not_act FiniteConc)


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


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


295 
apply assumption


296 
(* IH *)


297 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


298 


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


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


301 
done


302 


303 
declare FiniteConc [simp]


304 


305 
declare FilterConc [simp del]


306 


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


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


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


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


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


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


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


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


315 
apply (erule Seq_Finite_ind)


316 
apply (rule allI)+


317 
apply (rule impI)


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


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


320 
apply simp


321 
(* main case *)


322 
apply (rule allI)+


323 
apply (rule impI)


324 
apply simp


325 
apply (erule conjE)+


326 
apply simp


327 
(* divide_Seq on s *)


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


329 
apply (erule conjE)+


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


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


332 
apply assumption


333 
apply (simp add: not_ext_is_int_or_not_act FilterConc)


334 
(* apply IH *)


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


336 
apply (simp add: ForallTL ForallDropwhile FilterConc)


337 
apply (erule exE)+


338 
apply (erule conjE)+


339 
apply (simp add: FilterConc)


340 
(* for replacing IH in conclusion *)


341 
apply (rotate_tac 2)


342 
(* instantiate y1a and y2a *)


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


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


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


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


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


348 
done


349 


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


351 


352 
declare FilterConc [simp del]


353 


354 
lemma reduceB_mksch1 [rule_format]:


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


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


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


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


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


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


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


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


363 
apply (erule Seq_Finite_ind)


364 
apply (rule allI)+


365 
apply (rule impI)


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


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


368 
apply simp


369 
(* main case *)


370 
apply (rule allI)+


371 
apply (rule impI)


372 
apply simp


373 
apply (erule conjE)+


374 
apply simp


375 
(* divide_Seq on s *)


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


377 
apply (erule conjE)+


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


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


380 
apply assumption


381 
apply (simp add: not_ext_is_int_or_not_act FilterConc)


382 
(* apply IH *)


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


384 
apply (simp add: ForallTL ForallDropwhile FilterConc)


385 
apply (erule exE)+


386 
apply (erule conjE)+


387 
apply (simp add: FilterConc)


388 
(* for replacing IH in conclusion *)


389 
apply (rotate_tac 2)


390 
(* instantiate y1a and y2a *)


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


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


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


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


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


396 
done


397 


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


399 


400 
declare FilterConc [simp]


401 


402 


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


404 


405 
lemma FilterA_mksch_is_tr:


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


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


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


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


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


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


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


413 


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


415 
(* main case *)


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

26359

417 
apply auto

19741

418 


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


420 
apply (frule divide_Seq)


421 
apply (frule divide_Seq)


422 
back


423 
apply (erule conjE)+


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


425 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


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


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


428 
apply assumption


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


430 
apply assumption


431 
(* IH *)


432 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


433 


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


435 
apply (frule divide_Seq)


436 
apply (erule conjE)+


437 
(* filtering internals of A is nil *)


438 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


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


440 
apply assumption


441 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


442 


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


444 
apply (frule divide_Seq)


445 
apply (erule conjE)+


446 
(* filtering internals of A is nil *)


447 
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)


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


449 
back


450 
apply assumption


451 
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)


452 


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


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


455 
done


456 


457 


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


459 


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


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


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


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


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


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


466 
LastActExtsch A schA & LastActExtsch B schB


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


468 
apply (intro strip)


469 
apply (rule seq.take_lemmas)


470 
apply (rule mp)


471 
prefer 2 apply assumption


472 
back back back back


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


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


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


476 
apply (tactic "thin_tac' 5 1")


477 
apply (rule nat_less_induct)


478 
apply (rule allI)+


479 
apply (rename_tac tr schB schA)


480 
apply (intro strip)


481 
apply (erule conjE)+


482 


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


484 


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


486 
apply (tactic "thin_tac' 5 1")


487 


488 


489 
apply (case_tac "Finite tr")


490 


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


492 
apply (subgoal_tac "schA=nil")


493 
apply (simp (no_asm_simp))


494 
(* first side: mksch = nil *)


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


496 
(* second side: schA = nil *)


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


498 
apply (simp (no_asm_simp))


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


500 
apply assumption


501 
apply fast


502 


503 
(* case ~ Finite s *)


504 


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


506 
apply (subgoal_tac "schA=UU")


507 
apply (simp (no_asm_simp))


508 
(* first side: mksch = UU *)


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


510 
(* schA = UU *)


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


512 
apply (simp (no_asm_simp))


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


514 
apply assumption


515 
apply fast


516 


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


518 


519 
apply (drule divide_Seq3)


520 


521 
apply (erule exE)+


522 
apply (erule conjE)+


523 
apply hypsubst


524 


525 
(* bring in lemma reduceA_mksch *)


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


527 
apply assumption+


528 
apply (erule exE)+


529 
apply (erule conjE)+


530 


531 
(* use reduceA_mksch to rewrite conclusion *)


532 
apply hypsubst


533 
apply simp


534 


535 
(* eliminate the Bonly prefix *)


536 


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


538 
apply (erule_tac [2] ForallQFilterPnil)


539 
prefer 2 apply assumption


540 
prefer 2 apply fast


541 


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


543 


544 
apply simp


545 
apply (case_tac "x:act A")


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


547 
apply (rotate_tac 2)


548 
apply simp


549 


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


551 
apply (rotate_tac 1)


552 
apply simp


553 
(* eliminate introduced subgoal 2 *)


554 
apply (erule_tac [2] ForallQFilterPnil)


555 
prefer 2 apply assumption


556 
prefer 2 apply fast


557 


558 
(* bring in divide Seq for s *)


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


560 
apply (erule conjE)+


561 


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


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


564 
back


565 
back


566 
back


567 
apply assumption


568 


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


570 
apply (rule take_reduction)


571 


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


573 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


574 
apply (rule refl)


575 
apply (simp add: int_is_act not_ext_is_int_or_not_act)


576 
apply (rotate_tac 11)


577 


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


579 


580 
(* assumption Forall tr *)


581 
(* assumption schB *)


582 
apply (simp add: Forall_Conc ext_and_act)


583 
(* assumption schA *)


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


585 
apply assumption


586 
apply (simp add: int_is_not_ext)


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


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


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


590 
apply assumption


591 


592 
(* assumption Forall schA *)


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


594 
apply assumption


595 
apply (simp add: ForallPTakewhileQ int_is_act)


596 


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


598 


599 


600 
apply (rotate_tac 2)


601 
apply simp


602 


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


604 
apply (rotate_tac 1)


605 
apply simp


606 
(* eliminate introduced subgoal 2 *)


607 
apply (erule_tac [2] ForallQFilterPnil)


608 
prefer 2 apply (assumption)


609 
prefer 2 apply (fast)


610 


611 
(* bring in divide Seq for s *)


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


613 
apply (erule conjE)+


614 


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


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


617 
back


618 
back


619 
back


620 
apply assumption


621 


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


623 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


624 


625 
(* rewrite assumption forall and schB *)


626 
apply (rotate_tac 13)


627 
apply (simp add: ext_and_act)


628 


629 
(* divide_Seq for schB2 *)


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


631 
apply (erule conjE)+


632 
(* assumption schA *)


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


634 
apply assumption


635 
apply (simp add: int_is_not_ext)


636 


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


638 
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


639 


640 


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


642 
apply (rule take_reduction)


643 
apply (rule refl)


644 
apply (rule refl)


645 


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


647 


648 
(* assumption schB *)


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


650 
apply assumption


651 
apply (simp add: intA_is_not_actB int_is_not_ext)


652 


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


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


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


656 
apply assumption


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


658 


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


660 
apply (simp add: ForallTL ForallDropwhile)


661 


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


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


664 
apply (case_tac "x:act B")


665 
apply fast


666 


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


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


669 
apply (rotate_tac 9)


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


671 
apply (simp add: externals_of_par)


672 
apply (fast intro!: ext_is_act)


673 


674 
done


675 


676 


677 


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


679 


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


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


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


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


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


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


686 
LastActExtsch A schA & LastActExtsch B schB


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


688 
apply (intro strip)


689 
apply (rule seq.take_lemmas)


690 
apply (rule mp)


691 
prefer 2 apply assumption


692 
back back back back


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


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


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


696 
apply (tactic "thin_tac' 5 1")


697 
apply (rule nat_less_induct)


698 
apply (rule allI)+


699 
apply (rename_tac tr schB schA)


700 
apply (intro strip)


701 
apply (erule conjE)+


702 


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


704 


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


706 
apply (tactic "thin_tac' 5 1")


707 


708 
apply (case_tac "Finite tr")


709 


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


711 
apply (subgoal_tac "schB=nil")


712 
apply (simp (no_asm_simp))


713 
(* first side: mksch = nil *)


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


715 
(* second side: schA = nil *)


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


717 
apply (simp (no_asm_simp))


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


719 
apply assumption


720 
apply fast


721 


722 
(* case ~ Finite tr *)


723 


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


725 
apply (subgoal_tac "schB=UU")


726 
apply (simp (no_asm_simp))


727 
(* first side: mksch = UU *)


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


729 
(* schA = UU *)


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


731 
apply (simp (no_asm_simp))


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


733 
apply assumption


734 
apply fast


735 


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


737 


738 
apply (drule divide_Seq3)


739 


740 
apply (erule exE)+


741 
apply (erule conjE)+


742 
apply hypsubst


743 


744 
(* bring in lemma reduceB_mksch *)


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


746 
apply assumption+


747 
apply (erule exE)+


748 
apply (erule conjE)+


749 


750 
(* use reduceB_mksch to rewrite conclusion *)


751 
apply hypsubst


752 
apply simp


753 


754 
(* eliminate the Aonly prefix *)


755 


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


757 
apply (erule_tac [2] ForallQFilterPnil)


758 
prefer 2 apply (assumption)


759 
prefer 2 apply (fast)


760 


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


762 


763 
apply simp


764 
apply (case_tac "x:act B")


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


766 
apply (rotate_tac 2)


767 
apply simp


768 


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


770 
apply (rotate_tac 1)


771 
apply simp


772 
(* eliminate introduced subgoal 2 *)


773 
apply (erule_tac [2] ForallQFilterPnil)


774 
prefer 2 apply (assumption)


775 
prefer 2 apply (fast)


776 


777 
(* bring in divide Seq for s *)


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


779 
apply (erule conjE)+


780 


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


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


783 
back


784 
back


785 
back


786 
apply assumption


787 


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


789 
apply (rule take_reduction)


790 


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


792 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


793 
apply (rule refl)


794 
apply (simp add: int_is_act not_ext_is_int_or_not_act)


795 
apply (rotate_tac 11)


796 


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


798 


799 
(* assumption schA *)


800 
apply (simp add: Forall_Conc ext_and_act)


801 
(* assumption schB *)


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


803 
apply assumption


804 
apply (simp add: int_is_not_ext)


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


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


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


808 
apply assumption


809 


810 
(* assumption Forall schB *)


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


812 
apply assumption


813 
apply (simp add: ForallPTakewhileQ int_is_act)


814 


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


816 


817 
apply (rotate_tac 2)


818 
apply simp


819 


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


821 
apply (rotate_tac 1)


822 
apply simp


823 
(* eliminate introduced subgoal 2 *)


824 
apply (erule_tac [2] ForallQFilterPnil)


825 
prefer 2 apply (assumption)


826 
prefer 2 apply (fast)


827 


828 
(* bring in divide Seq for s *)


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


830 
apply (erule conjE)+


831 


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


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


834 
back


835 
back


836 
back


837 
apply assumption


838 


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


840 
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)


841 


842 
(* rewrite assumption forall and schB *)


843 
apply (rotate_tac 13)


844 
apply (simp add: ext_and_act)


845 


846 
(* divide_Seq for schB2 *)


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


848 
apply (erule conjE)+


849 
(* assumption schA *)


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


851 
apply assumption


852 
apply (simp add: int_is_not_ext)


853 


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


855 
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


856 


857 


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


859 
apply (rule take_reduction)


860 
apply (rule refl)


861 
apply (rule refl)


862 


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


864 


865 
(* assumption schA *)


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


867 
apply assumption


868 
apply (simp add: intA_is_not_actB int_is_not_ext)


869 


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


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


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


873 
apply assumption


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


875 


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


877 
apply (simp add: ForallTL ForallDropwhile)


878 


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


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


881 
apply (case_tac "x:act A")


882 
apply fast


883 


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


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


886 
apply (rotate_tac 9)


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


888 
apply (simp add: externals_of_par)


889 
apply (fast intro!: ext_is_act)


890 


891 
done


892 


893 


894 
subsection "COMPOSITIONALITY on TRACE Level  Main Theorem"


895 


896 
lemma compositionality_tr:


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


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


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


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


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


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


903 


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

26359

905 
apply auto

19741

906 


907 
(* ==> *)


908 
(* There is a schedule of A *)


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


910 
prefer 2


911 
apply (simp add: compositionality_sch)


912 
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)


913 
(* There is a schedule of B *)


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


915 
prefer 2


916 
apply (simp add: compositionality_sch)


917 
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)


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


919 
apply (rule ForallPFilterP)


920 


921 
(* <== *)


922 


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


924 
apply (drule exists_LastActExtsch)


925 
apply assumption


926 
apply (drule exists_LastActExtsch)


927 
apply assumption


928 
apply (erule exE)+


929 
apply (erule conjE)+


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


931 
apply (drule scheds_in_sig)


932 
apply assumption


933 
apply (drule scheds_in_sig)


934 
apply assumption


935 


936 
apply (rename_tac h1 h2 schA schB)


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


938 
we need here *)


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


940 


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


942 
apply (simp add: FilterA_mksch_is_tr)


943 


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


945 
apply (simp add: compositionality_sch)


946 
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)


947 
apply (erule ForallAorB_mksch)


948 
apply (erule ForallPForallQ)


949 
apply (erule ext_is_act)


950 
done


951 


952 


953 


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


955 


956 
lemma compositionality_tr_modules:


957 


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


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


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


961 


962 
apply (unfold Traces_def par_traces_def)


963 
apply (simp add: asig_of_par)


964 
apply (rule set_ext)


965 
apply (simp add: compositionality_tr externals_of_par)


966 
done


967 


968 

26339

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

3071

970 


971 


972 
end
