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