1(* Title: HOL/HOLCF/IOA/CompoScheds.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Compositionality on Schedule level\<close> 6 7theory CompoScheds 8imports CompoExecs 9begin 10 11definition mkex2 :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow> 12 ('a, 's) pairs \<rightarrow> ('a, 't) pairs \<rightarrow> ('s \<Rightarrow> 't \<Rightarrow> ('a, 's \<times> 't) pairs)" 13 where "mkex2 A B = 14 (fix \<cdot> 15 (LAM h sch exA exB. 16 (\<lambda>s t. 17 case sch of 18 nil \<Rightarrow> nil 19 | x ## xs \<Rightarrow> 20 (case x of 21 UU \<Rightarrow> UU 22 | Def y \<Rightarrow> 23 (if y \<in> act A then 24 (if y \<in> act B then 25 (case HD \<cdot> exA of 26 UU \<Rightarrow> UU 27 | Def a \<Rightarrow> 28 (case HD \<cdot> exB of 29 UU \<Rightarrow> UU 30 | Def b \<Rightarrow> 31 (y, (snd a, snd b)) \<leadsto> 32 (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b))) 33 else 34 (case HD \<cdot> exA of 35 UU \<Rightarrow> UU 36 | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t)) 37 else 38 (if y \<in> act B then 39 (case HD \<cdot> exB of 40 UU \<Rightarrow> UU 41 | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b)) 42 else UU))))))" 43 44definition mkex :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<Rightarrow> 45 ('a, 's) execution \<Rightarrow> ('a, 't) execution \<Rightarrow> ('a, 's \<times> 't) execution" 46 where "mkex A B sch exA exB = 47 ((fst exA, fst exB), (mkex2 A B \<cdot> sch \<cdot> (snd exA) \<cdot> (snd exB)) (fst exA) (fst exB))" 48 49definition par_scheds :: "'a schedule_module \<Rightarrow> 'a schedule_module \<Rightarrow> 'a schedule_module" 50 where "par_scheds SchedsA SchedsB = 51 (let 52 schA = fst SchedsA; sigA = snd SchedsA; 53 schB = fst SchedsB; sigB = snd SchedsB 54 in 55 ({sch. Filter (\<lambda>a. a\<in>actions sigA)\<cdot>sch \<in> schA} \<inter> 56 {sch. Filter (\<lambda>a. a\<in>actions sigB)\<cdot>sch \<in> schB} \<inter> 57 {sch. Forall (\<lambda>x. x\<in>(actions sigA Un actions sigB)) sch}, 58 asig_comp sigA sigB))" 59 60 61subsection \<open>\<open>mkex\<close> rewrite rules\<close> 62 63lemma mkex2_unfold: 64 "mkex2 A B = 65 (LAM sch exA exB. 66 (\<lambda>s t. 67 case sch of 68 nil \<Rightarrow> nil 69 | x ## xs \<Rightarrow> 70 (case x of 71 UU \<Rightarrow> UU 72 | Def y \<Rightarrow> 73 (if y \<in> act A then 74 (if y \<in> act B then 75 (case HD \<cdot> exA of 76 UU \<Rightarrow> UU 77 | Def a \<Rightarrow> 78 (case HD \<cdot> exB of 79 UU \<Rightarrow> UU 80 | Def b \<Rightarrow> 81 (y, (snd a, snd b)) \<leadsto> 82 (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b))) 83 else 84 (case HD \<cdot> exA of 85 UU \<Rightarrow> UU 86 | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t)) 87 else 88 (if y \<in> act B then 89 (case HD \<cdot> exB of 90 UU \<Rightarrow> UU 91 | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b)) 92 else UU)))))" 93 apply (rule trans) 94 apply (rule fix_eq2) 95 apply (simp only: mkex2_def) 96 apply (rule beta_cfun) 97 apply simp 98 done 99 100lemma mkex2_UU: "(mkex2 A B \<cdot> UU \<cdot> exA \<cdot> exB) s t = UU" 101 apply (subst mkex2_unfold) 102 apply simp 103 done 104 105lemma mkex2_nil: "(mkex2 A B \<cdot> nil \<cdot> exA \<cdot> exB) s t = nil" 106 apply (subst mkex2_unfold) 107 apply simp 108 done 109 110lemma mkex2_cons_1: 111 "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow> 112 (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t = 113 (x, snd a,t) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t" 114 apply (rule trans) 115 apply (subst mkex2_unfold) 116 apply (simp add: Consq_def If_and_if) 117 apply (simp add: Consq_def) 118 done 119 120lemma mkex2_cons_2: 121 "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow> 122 (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t = 123 (x, s, snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b)" 124 apply (rule trans) 125 apply (subst mkex2_unfold) 126 apply (simp add: Consq_def If_and_if) 127 apply (simp add: Consq_def) 128 done 129 130lemma mkex2_cons_3: 131 "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow> 132 (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t = 133 (x, snd a,snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)" 134 apply (rule trans) 135 apply (subst mkex2_unfold) 136 apply (simp add: Consq_def If_and_if) 137 apply (simp add: Consq_def) 138 done 139 140declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp] 141 mkex2_cons_2 [simp] mkex2_cons_3 [simp] 142 143 144subsection \<open>\<open>mkex\<close>\<close> 145 146lemma mkex_UU: "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)" 147 by (simp add: mkex_def) 148 149lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)" 150 by (simp add: mkex_def) 151 152lemma mkex_cons_1: 153 "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> 154 mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, exB) = 155 ((s, t), (x, snd a, t) \<leadsto> snd (mkex A B sch (snd a, exA) (t, exB)))" 156 apply (unfold mkex_def) 157 apply (cut_tac exA = "a \<leadsto> exA" in mkex2_cons_1) 158 apply auto 159 done 160 161lemma mkex_cons_2: 162 "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> 163 mkex A B (x \<leadsto> sch) (s, exA) (t, b \<leadsto> exB) = 164 ((s, t), (x, s, snd b) \<leadsto> snd (mkex A B sch (s, exA) (snd b, exB)))" 165 apply (unfold mkex_def) 166 apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2) 167 apply auto 168 done 169 170lemma mkex_cons_3: 171 "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> 172 mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, b \<leadsto> exB) = 173 ((s, t), (x, snd a, snd b) \<leadsto> snd (mkex A B sch (snd a, exA) (snd b, exB)))" 174 apply (unfold mkex_def) 175 apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>exA" in mkex2_cons_3) 176 apply auto 177 done 178 179declare mkex2_UU [simp del] mkex2_nil [simp del] 180 mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del] 181 182lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3 183 184declare composch_simps [simp] 185 186 187subsection \<open>Compositionality on schedule level\<close> 188 189subsubsection \<open>Lemmas for \<open>\<Longrightarrow>\<close>\<close> 190 191lemma lemma_2_1a: 192 \<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close> 193 "filter_act \<cdot> (Filter_ex2 (asig_of A) \<cdot> xs) = 194 Filter (\<lambda>a. a \<in> act A) \<cdot> (filter_act \<cdot> xs)" 195 apply (unfold filter_act_def Filter_ex2_def) 196 apply (simp add: MapFilter o_def) 197 done 198 199lemma lemma_2_1b: 200 \<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close> 201 "filter_act \<cdot> (ProjA2 \<cdot> xs) = filter_act \<cdot> xs \<and> 202 filter_act \<cdot> (ProjB2 \<cdot> xs) = filter_act \<cdot> xs" 203 by (pair_induct xs) 204 205 206text \<open> 207 Schedules of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions. 208 209 Very similar to \<open>lemma_1_1c\<close>, but it is not checking if every action element 210 of an \<open>ex\<close> is in \<open>A\<close> or \<open>B\<close>, but after projecting it onto the action 211 schedule. Of course, this is the same proposition, but we cannot change this 212 one, when then rather \<open>lemma_1_1c\<close>. 213\<close> 214 215lemma sch_actions_in_AorB: 216 "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act \<cdot> xs)" 217 apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def) 218 text \<open>main case\<close> 219 apply auto 220 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) 221 done 222 223 224subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close> 225 226text \<open> 227 Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close> 228 structural induction. 229\<close> 230 231lemma Mapfst_mkex_is_sch: 232 "\<forall>exA exB s t. 233 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> 234 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 235 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 236 filter_act \<cdot> (snd (mkex A B sch (s, exA) (t, exB))) = sch" 237 apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def) 238 239 text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close> 240 apply auto 241 242 text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close> 243 apply (Seq_case_simp exA) 244 text \<open>Case \<open>exA = UU\<close>, Case \<open>exA = nil\<close>\<close> 245 text \<open> 246 These \<open>UU\<close> and \<open>nil\<close> cases are the only places where the assumption 247 \<open>filter A sch \<sqsubseteq> f_act exA\<close> is used! 248 \<open>\<longrightarrow>\<close> to generate a contradiction using \<open>\<not> a \<leadsto> ss \<sqsubseteq> UU nil\<close>, 249 using theorems \<open>Cons_not_less_UU\<close> and \<open>Cons_not_less_nil\<close>.\<close> 250 apply (Seq_case_simp exB) 251 text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close> 252 text \<open> 253 Here it is important that @{method Seq_case_simp} uses no \<open>!full!_simp_tac\<close> 254 for the cons case, as otherwise \<open>mkex_cons_3\<close> would not be rewritten 255 without use of \<open>rotate_tac\<close>: then tactic would not be generally 256 applicable.\<close> 257 apply simp 258 259 text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close> 260 apply (Seq_case_simp exA) 261 apply simp 262 263 text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close> 264 apply (Seq_case_simp exB) 265 apply simp 266 267 text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close> 268 apply (simp add: asig_of_par actions_asig_comp) 269 done 270 271 272text \<open>Generalizing the proof above to a proof method:\<close> 273ML \<open> 274fun mkex_induct_tac ctxt sch exA exB = 275 EVERY' [ 276 Seq_induct_tac ctxt sch 277 @{thms Filter_def Forall_def sforall_def mkex_def stutter_def}, 278 asm_full_simp_tac ctxt, 279 SELECT_GOAL 280 (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) \<^theory_context>\<open>Fun\<close>)), 281 Seq_case_simp_tac ctxt exA, 282 Seq_case_simp_tac ctxt exB, 283 asm_full_simp_tac ctxt, 284 Seq_case_simp_tac ctxt exA, 285 asm_full_simp_tac ctxt, 286 Seq_case_simp_tac ctxt exB, 287 asm_full_simp_tac ctxt, 288 asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})] 289\<close> 290 291method_setup mkex_induct = \<open> 292 Scan.lift (Args.embedded -- Args.embedded -- Args.embedded) 293 >> (fn ((sch, exA), exB) => fn ctxt => 294 SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB)) 295\<close> 296 297 298text \<open> 299 Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close> 300 structural induction. 301\<close> 302 303lemma stutterA_mkex: 304 "\<forall>exA exB s t. 305 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> 306 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 307 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 308 stutter (asig_of A) (s, ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))" 309 by (mkex_induct sch exA exB) 310 311lemma stutter_mkex_on_A: 312 "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> 313 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow> 314 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow> 315 stutter (asig_of A) (ProjA (mkex A B sch exA exB))" 316 apply (cut_tac stutterA_mkex) 317 apply (simp add: stutter_def ProjA_def mkex_def) 318 apply (erule allE)+ 319 apply (drule mp) 320 prefer 2 apply (assumption) 321 apply simp 322 done 323 324 325text \<open> 326 Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close> 327 structural induction. 328\<close> 329 330lemma stutterB_mkex: 331 "\<forall>exA exB s t. 332 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> 333 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 334 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 335 stutter (asig_of B) (t, ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))" 336 by (mkex_induct sch exA exB) 337 338 339lemma stutter_mkex_on_B: 340 "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> 341 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow> 342 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow> 343 stutter (asig_of B) (ProjB (mkex A B sch exA exB))" 344 apply (cut_tac stutterB_mkex) 345 apply (simp add: stutter_def ProjB_def mkex_def) 346 apply (erule allE)+ 347 apply (drule mp) 348 prefer 2 apply (assumption) 349 apply simp 350 done 351 352 353text \<open> 354 Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>, 355 using \<open>zip \<cdot> (proj1 \<cdot> exA) \<cdot> (proj2 \<cdot> exA)\<close> instead of \<open>exA\<close>, 356 because of admissibility problems structural induction. 357\<close> 358 359lemma filter_mkex_is_exA_tmp: 360 "\<forall>exA exB s t. 361 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> 362 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 363 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 364 Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) = 365 Zip \<cdot> (Filter (\<lambda>a. a \<in> act A) \<cdot> sch) \<cdot> (Map snd \<cdot> exA)" 366 by (mkex_induct sch exB exA) 367 368text \<open> 369 \<open>zip \<cdot> (proj1 \<cdot> y) \<cdot> (proj2 \<cdot> y) = y\<close> (using the lift operations) 370 lemma for admissibility problems 371\<close> 372 373lemma Zip_Map_fst_snd: "Zip \<cdot> (Map fst \<cdot> y) \<cdot> (Map snd \<cdot> y) = y" 374 by (Seq_induct y) 375 376 377text \<open> 378 \<open>filter A \<cdot> sch = proj1 \<cdot> ex \<longrightarrow> zip \<cdot> (filter A \<cdot> sch) \<cdot> (proj2 \<cdot> ex) = ex\<close> 379 lemma for eliminating non admissible equations in assumptions 380\<close> 381 382lemma trick_against_eq_in_ass: 383 "Filter (\<lambda>a. a \<in> act AB) \<cdot> sch = filter_act \<cdot> ex \<Longrightarrow> 384 ex = Zip \<cdot> (Filter (\<lambda>a. a \<in> act AB) \<cdot> sch) \<cdot> (Map snd \<cdot> ex)" 385 apply (simp add: filter_act_def) 386 apply (rule Zip_Map_fst_snd [symmetric]) 387 done 388 389text \<open> 390 Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close> 391 using the above trick. 392\<close> 393 394lemma filter_mkex_is_exA: 395 "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> 396 Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow> 397 Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow> 398 Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" 399 apply (simp add: ProjA_def Filter_ex_def) 400 apply (pair exA) 401 apply (pair exB) 402 apply (rule conjI) 403 apply (simp (no_asm) add: mkex_def) 404 apply (simplesubst trick_against_eq_in_ass) 405 back 406 apply assumption 407 apply (simp add: filter_mkex_is_exA_tmp) 408 done 409 410text \<open> 411 Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close> 412 using \<open>zip \<cdot> (proj1 \<cdot> exB) \<cdot> (proj2 \<cdot> exB)\<close> instead of \<open>exB\<close> 413 because of admissibility problems structural induction. 414\<close> 415 416lemma filter_mkex_is_exB_tmp: 417 "\<forall>exA exB s t. 418 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> 419 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 420 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 421 Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) = 422 Zip \<cdot> (Filter (\<lambda>a. a \<in> act B) \<cdot> sch) \<cdot> (Map snd \<cdot> exB)" 423 (*notice necessary change of arguments exA and exB*) 424 by (mkex_induct sch exA exB) 425 426text \<open> 427 Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>B\<close> is \<open>exB\<close> 428 using the above trick. 429\<close> 430 431lemma filter_mkex_is_exB: 432 "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> 433 Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow> 434 Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow> 435 Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" 436 apply (simp add: ProjB_def Filter_ex_def) 437 apply (pair exA) 438 apply (pair exB) 439 apply (rule conjI) 440 apply (simp add: mkex_def) 441 apply (simplesubst trick_against_eq_in_ass) 442 back 443 apply assumption 444 apply (simp add: filter_mkex_is_exB_tmp) 445 done 446 447lemma mkex_actions_in_AorB: 448 \<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close> 449 "\<forall>s t exA exB. 450 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch & 451 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and> 452 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow> 453 Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))" 454 by (mkex_induct sch exA exB) 455 456 457theorem compositionality_sch: 458 "sch \<in> schedules (A \<parallel> B) \<longleftrightarrow> 459 Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<in> schedules A \<and> 460 Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<in> schedules B \<and> 461 Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch" 462 apply (simp add: schedules_def has_schedule_def) 463 apply auto 464 text \<open>\<open>\<Longrightarrow>\<close>\<close> 465 apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI) 466 prefer 2 467 apply (simp add: compositionality_ex) 468 apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b) 469 apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI) 470 prefer 2 471 apply (simp add: compositionality_ex) 472 apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b) 473 apply (simp add: executions_def) 474 apply (pair ex) 475 apply (erule conjE) 476 apply (simp add: sch_actions_in_AorB) 477 text \<open>\<open>\<Longleftarrow>\<close>\<close> 478 text \<open>\<open>mkex\<close> is exactly the construction of \<open>exA\<parallel>B\<close> out of \<open>exA\<close>, \<open>exB\<close>, 479 and the oracle \<open>sch\<close>, we need here\<close> 480 apply (rename_tac exA exB) 481 apply (rule_tac x = "mkex A B sch exA exB" in bexI) 482 text \<open>\<open>mkex\<close> actions are just the oracle\<close> 483 apply (pair exA) 484 apply (pair exB) 485 apply (simp add: Mapfst_mkex_is_sch) 486 text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close> 487 apply (simp add: compositionality_ex) 488 apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA) 489 apply (pair exA) 490 apply (pair exB) 491 apply (simp add: mkex_actions_in_AorB) 492 done 493 494theorem compositionality_sch_modules: 495 "Scheds (A \<parallel> B) = par_scheds (Scheds A) (Scheds B)" 496 apply (unfold Scheds_def par_scheds_def) 497 apply (simp add: asig_of_par) 498 apply (rule set_eqI) 499 apply (simp add: compositionality_sch actions_of_par) 500 done 501 502declare compoex_simps [simp del] 503declare composch_simps [simp del] 504 505end 506