1(* Title: HOL/HOLCF/IOA/Automata.thy 2 Author: Olaf M��ller, Konrad Slind, Tobias Nipkow 3*) 4 5section \<open>The I/O automata of Lynch and Tuttle in HOLCF\<close> 6 7theory Automata 8imports Asig 9begin 10 11default_sort type 12 13type_synonym ('a, 's) transition = "'s \<times> 'a \<times> 's" 14type_synonym ('a, 's) ioa = 15 "'a signature \<times> 's set \<times> ('a, 's)transition set \<times> 'a set set \<times> 'a set set" 16 17 18subsection \<open>IO automata\<close> 19 20definition asig_of :: "('a, 's) ioa \<Rightarrow> 'a signature" 21 where "asig_of = fst" 22 23definition starts_of :: "('a, 's) ioa \<Rightarrow> 's set" 24 where "starts_of = fst \<circ> snd" 25 26definition trans_of :: "('a, 's) ioa \<Rightarrow> ('a, 's) transition set" 27 where "trans_of = fst \<circ> snd \<circ> snd" 28 29abbreviation trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81, 81, 81, 81] 100) 30 where "s \<midarrow>a\<midarrow>A\<rightarrow> t \<equiv> (s, a, t) \<in> trans_of A" 31 32definition wfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set" 33 where "wfair_of = fst \<circ> snd \<circ> snd \<circ> snd" 34 35definition sfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set" 36 where "sfair_of = snd \<circ> snd \<circ> snd \<circ> snd" 37 38definition is_asig_of :: "('a, 's) ioa \<Rightarrow> bool" 39 where "is_asig_of A = is_asig (asig_of A)" 40 41definition is_starts_of :: "('a, 's) ioa \<Rightarrow> bool" 42 where "is_starts_of A \<longleftrightarrow> starts_of A \<noteq> {}" 43 44definition is_trans_of :: "('a, 's) ioa \<Rightarrow> bool" 45 where "is_trans_of A \<longleftrightarrow> 46 (\<forall>triple. triple \<in> trans_of A \<longrightarrow> fst (snd triple) \<in> actions (asig_of A))" 47 48definition input_enabled :: "('a, 's) ioa \<Rightarrow> bool" 49 where "input_enabled A \<longleftrightarrow> 50 (\<forall>a. a \<in> inputs (asig_of A) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1, a, s2) \<in> trans_of A))" 51 52definition IOA :: "('a, 's) ioa \<Rightarrow> bool" 53 where "IOA A \<longleftrightarrow> 54 is_asig_of A \<and> 55 is_starts_of A \<and> 56 is_trans_of A \<and> 57 input_enabled A" 58 59abbreviation "act A \<equiv> actions (asig_of A)" 60abbreviation "ext A \<equiv> externals (asig_of A)" 61abbreviation int where "int A \<equiv> internals (asig_of A)" 62abbreviation "inp A \<equiv> inputs (asig_of A)" 63abbreviation "out A \<equiv> outputs (asig_of A)" 64abbreviation "local A \<equiv> locals (asig_of A)" 65 66 67text \<open>invariants\<close> 68 69inductive reachable :: "('a, 's) ioa \<Rightarrow> 's \<Rightarrow> bool" for C :: "('a, 's) ioa" 70where 71 reachable_0: "s \<in> starts_of C \<Longrightarrow> reachable C s" 72| reachable_n: "reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow> reachable C t" 73 74definition invariant :: "[('a, 's) ioa, 's \<Rightarrow> bool] \<Rightarrow> bool" 75 where "invariant A P \<longleftrightarrow> (\<forall>s. reachable A s \<longrightarrow> P s)" 76 77 78subsection \<open>Parallel composition\<close> 79 80subsubsection \<open>Binary composition of action signatures and automata\<close> 81 82definition compatible :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> bool" 83 where "compatible A B \<longleftrightarrow> 84 out A \<inter> out B = {} \<and> 85 int A \<inter> act B = {} \<and> 86 int B \<inter> act A = {}" 87 88definition asig_comp :: "'a signature \<Rightarrow> 'a signature \<Rightarrow> 'a signature" 89 where "asig_comp a1 a2 = 90 (((inputs a1 \<union> inputs a2) - (outputs a1 \<union> outputs a2), 91 (outputs a1 \<union> outputs a2), 92 (internals a1 \<union> internals a2)))" 93 94definition par :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> ('a, 's * 't) ioa" (infixr "\<parallel>" 10) 95 where "(A \<parallel> B) = 96 (asig_comp (asig_of A) (asig_of B), 97 {pr. fst pr \<in> starts_of A \<and> snd pr \<in> starts_of B}, 98 {tr. 99 let 100 s = fst tr; 101 a = fst (snd tr); 102 t = snd (snd tr) 103 in 104 (a \<in> act A \<or> a \<in> act B) \<and> 105 (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A 106 else fst t = fst s) \<and> 107 (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B 108 else snd t = snd s)}, 109 wfair_of A \<union> wfair_of B, 110 sfair_of A \<union> sfair_of B)" 111 112 113subsection \<open>Hiding\<close> 114 115subsubsection \<open>Hiding and restricting\<close> 116 117definition restrict_asig :: "'a signature \<Rightarrow> 'a set \<Rightarrow> 'a signature" 118 where "restrict_asig asig actns = 119 (inputs asig \<inter> actns, 120 outputs asig \<inter> actns, 121 internals asig \<union> (externals asig - actns))" 122 123text \<open> 124 Notice that for \<open>wfair_of\<close> and \<open>sfair_of\<close> nothing has to be changed, as 125 changes from the outputs to the internals does not touch the locals as a 126 whole, which is of importance for fairness only. 127\<close> 128definition restrict :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa" 129 where "restrict A actns = 130 (restrict_asig (asig_of A) actns, 131 starts_of A, 132 trans_of A, 133 wfair_of A, 134 sfair_of A)" 135 136definition hide_asig :: "'a signature \<Rightarrow> 'a set \<Rightarrow> 'a signature" 137 where "hide_asig asig actns = 138 (inputs asig - actns, 139 outputs asig - actns, 140 internals asig \<union> actns)" 141 142definition hide :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa" 143 where "hide A actns = 144 (hide_asig (asig_of A) actns, 145 starts_of A, 146 trans_of A, 147 wfair_of A, 148 sfair_of A)" 149 150 151subsection \<open>Renaming\<close> 152 153definition rename_set :: "'a set \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> 'c set" 154 where "rename_set A ren = {b. \<exists>x. Some x = ren b \<and> x \<in> A}" 155 156definition rename :: "('a, 'b) ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c, 'b) ioa" 157 where "rename ioa ren = 158 ((rename_set (inp ioa) ren, 159 rename_set (out ioa) ren, 160 rename_set (int ioa) ren), 161 starts_of ioa, 162 {tr. 163 let 164 s = fst tr; 165 a = fst (snd tr); 166 t = snd (snd tr) 167 in \<exists>x. Some x = ren a \<and> s \<midarrow>x\<midarrow>ioa\<rightarrow> t}, 168 {rename_set s ren | s. s \<in> wfair_of ioa}, 169 {rename_set s ren | s. s \<in> sfair_of ioa})" 170 171 172subsection \<open>Fairness\<close> 173 174subsubsection \<open>Enabledness of actions and action sets\<close> 175 176definition enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" 177 where "enabled A a s \<longleftrightarrow> (\<exists>t. s \<midarrow>a\<midarrow>A\<rightarrow> t)" 178 179definition Enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool" 180 where "Enabled A W s \<longleftrightarrow> (\<exists>w \<in> W. enabled A w s)" 181 182 183text \<open>Action set keeps enabled until probably disabled by itself.\<close> 184 185definition en_persistent :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> bool" 186 where "en_persistent A W \<longleftrightarrow> 187 (\<forall>s a t. Enabled A W s \<and> a \<notin> W \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)" 188 189 190text \<open>Post conditions for actions and action sets.\<close> 191 192definition was_enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" 193 where "was_enabled A a t \<longleftrightarrow> (\<exists>s. s \<midarrow>a\<midarrow>A\<rightarrow> t)" 194 195definition set_was_enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool" 196 where "set_was_enabled A W t \<longleftrightarrow> (\<exists>w \<in> W. was_enabled A w t)" 197 198 199text \<open>Constraints for fair IOA.\<close> 200 201definition fairIOA :: "('a, 's) ioa \<Rightarrow> bool" 202 where "fairIOA A \<longleftrightarrow> (\<forall>S \<in> wfair_of A. S \<subseteq> local A) \<and> (\<forall>S \<in> sfair_of A. S \<subseteq> local A)" 203 204definition input_resistant :: "('a, 's) ioa \<Rightarrow> bool" 205 where "input_resistant A \<longleftrightarrow> 206 (\<forall>W \<in> sfair_of A. \<forall>s a t. 207 reachable A s \<and> reachable A t \<and> a \<in> inp A \<and> 208 Enabled A W s \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)" 209 210 211declare split_paired_Ex [simp del] 212 213lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def 214 215 216subsection "\<open>asig_of\<close>, \<open>starts_of\<close>, \<open>trans_of\<close>" 217 218lemma ioa_triple_proj: 219 "asig_of (x, y, z, w, s) = x \<and> 220 starts_of (x, y, z, w, s) = y \<and> 221 trans_of (x, y, z, w, s) = z \<and> 222 wfair_of (x, y, z, w, s) = w \<and> 223 sfair_of (x, y, z, w, s) = s" 224 by (simp add: ioa_projections) 225 226lemma trans_in_actions: "is_trans_of A \<Longrightarrow> s1 \<midarrow>a\<midarrow>A\<rightarrow> s2 \<Longrightarrow> a \<in> act A" 227 by (auto simp add: is_trans_of_def actions_def is_asig_def) 228 229lemma starts_of_par: "starts_of (A \<parallel> B) = {p. fst p \<in> starts_of A \<and> snd p \<in> starts_of B}" 230 by (simp add: par_def ioa_projections) 231 232lemma trans_of_par: 233 "trans_of(A \<parallel> B) = 234 {tr. 235 let 236 s = fst tr; 237 a = fst (snd tr); 238 t = snd (snd tr) 239 in 240 (a \<in> act A \<or> a \<in> act B) \<and> 241 (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A 242 else fst t = fst s) \<and> 243 (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B 244 else snd t = snd s)}" 245 by (simp add: par_def ioa_projections) 246 247 248subsection \<open>\<open>actions\<close> and \<open>par\<close>\<close> 249 250lemma actions_asig_comp: "actions (asig_comp a b) = actions a \<union> actions b" 251 by (auto simp add: actions_def asig_comp_def asig_projections) 252 253lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)" 254 by (simp add: par_def ioa_projections) 255 256lemma externals_of_par: "ext (A1 \<parallel> A2) = ext A1 \<union> ext A2" 257 by (auto simp add: externals_def asig_of_par asig_comp_def 258 asig_inputs_def asig_outputs_def Un_def set_diff_eq) 259 260lemma actions_of_par: "act (A1 \<parallel> A2) = act A1 \<union> act A2" 261 by (auto simp add: actions_def asig_of_par asig_comp_def 262 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) 263 264lemma inputs_of_par: "inp (A1 \<parallel> A2) = (inp A1 \<union> inp A2) - (out A1 \<union> out A2)" 265 by (simp add: actions_def asig_of_par asig_comp_def 266 asig_inputs_def asig_outputs_def Un_def set_diff_eq) 267 268lemma outputs_of_par: "out (A1 \<parallel> A2) = out A1 \<union> out A2" 269 by (simp add: actions_def asig_of_par asig_comp_def 270 asig_outputs_def Un_def set_diff_eq) 271 272lemma internals_of_par: "int (A1 \<parallel> A2) = int A1 \<union> int A2" 273 by (simp add: actions_def asig_of_par asig_comp_def 274 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) 275 276 277subsection \<open>Actions and compatibility\<close> 278 279lemma compat_commute: "compatible A B = compatible B A" 280 by (auto simp add: compatible_def Int_commute) 281 282lemma ext1_is_not_int2: "compatible A1 A2 \<Longrightarrow> a \<in> ext A1 \<Longrightarrow> a \<notin> int A2" 283 by (auto simp add: externals_def actions_def compatible_def) 284 285(*just commuting the previous one: better commute compatible*) 286lemma ext2_is_not_int1: "compatible A2 A1 \<Longrightarrow> a \<in> ext A1 \<Longrightarrow> a \<notin> int A2" 287 by (auto simp add: externals_def actions_def compatible_def) 288 289lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] 290lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] 291 292lemma intA_is_not_extB: "compatible A B \<Longrightarrow> x \<in> int A \<Longrightarrow> x \<notin> ext B" 293 by (auto simp add: externals_def actions_def compatible_def) 294 295lemma intA_is_not_actB: "compatible A B \<Longrightarrow> a \<in> int A \<Longrightarrow> a \<notin> act B" 296 by (auto simp add: externals_def actions_def compatible_def is_asig_def asig_of_def) 297 298(*the only one that needs disjointness of outputs and of internals and _all_ acts*) 299lemma outAactB_is_inpB: "compatible A B \<Longrightarrow> a \<in> out A \<Longrightarrow> a \<in> act B \<Longrightarrow> a \<in> inp B" 300 by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def 301 compatible_def is_asig_def asig_of_def) 302 303(*needed for propagation of input_enabledness from A, B to A \<parallel> B*) 304lemma inpAAactB_is_inpBoroutB: 305 "compatible A B \<Longrightarrow> a \<in> inp A \<Longrightarrow> a \<in> act B \<Longrightarrow> a \<in> inp B \<or> a \<in> out B" 306 by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def 307 compatible_def is_asig_def asig_of_def) 308 309 310subsection \<open>Input enabledness and par\<close> 311 312(*ugly case distinctions. Heart of proof: 313 1. inpAAactB_is_inpBoroutB ie. internals are really hidden. 314 2. inputs_of_par: outputs are no longer inputs of par. This is important here.*) 315lemma input_enabled_par: 316 "compatible A B \<Longrightarrow> input_enabled A \<Longrightarrow> input_enabled B \<Longrightarrow> input_enabled (A \<parallel> B)" 317 apply (unfold input_enabled_def) 318 apply (simp add: Let_def inputs_of_par trans_of_par) 319 apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})") 320 apply (simp add: inp_is_act) 321 prefer 2 322 apply (simp add: inp_is_act) 323 text \<open>\<open>a \<in> inp A\<close>\<close> 324 apply (case_tac "a \<in> act B") 325 text \<open>\<open>a \<in> inp B\<close>\<close> 326 apply (erule_tac x = "a" in allE) 327 apply simp 328 apply (drule inpAAactB_is_inpBoroutB) 329 apply assumption 330 apply assumption 331 apply (erule_tac x = "a" in allE) 332 apply simp 333 apply (erule_tac x = "aa" in allE) 334 apply (erule_tac x = "b" in allE) 335 apply (erule exE) 336 apply (erule exE) 337 apply (rule_tac x = "(s2, s2a)" in exI) 338 apply (simp add: inp_is_act) 339 text \<open>\<open>a \<notin> act B\<close>\<close> 340 apply (simp add: inp_is_act) 341 apply (erule_tac x = "a" in allE) 342 apply simp 343 apply (erule_tac x = "aa" in allE) 344 apply (erule exE) 345 apply (rule_tac x = " (s2,b) " in exI) 346 apply simp 347 348 text \<open>\<open>a \<in> inp B\<close>\<close> 349 apply (case_tac "a \<in> act A") 350 text \<open>\<open>a \<in> act A\<close>\<close> 351 apply (erule_tac x = "a" in allE) 352 apply (erule_tac x = "a" in allE) 353 apply (simp add: inp_is_act) 354 apply (frule_tac A1 = "A" in compat_commute [THEN iffD1]) 355 apply (drule inpAAactB_is_inpBoroutB) 356 back 357 apply assumption 358 apply assumption 359 apply simp 360 apply (erule_tac x = "aa" in allE) 361 apply (erule_tac x = "b" in allE) 362 apply (erule exE) 363 apply (erule exE) 364 apply (rule_tac x = "(s2, s2a)" in exI) 365 apply (simp add: inp_is_act) 366 text \<open>\<open>a \<notin> act B\<close>\<close> 367 apply (simp add: inp_is_act) 368 apply (erule_tac x = "a" in allE) 369 apply (erule_tac x = "a" in allE) 370 apply simp 371 apply (erule_tac x = "b" in allE) 372 apply (erule exE) 373 apply (rule_tac x = "(aa, s2)" in exI) 374 apply simp 375 done 376 377 378subsection \<open>Invariants\<close> 379 380lemma invariantI: 381 assumes "\<And>s. s \<in> starts_of A \<Longrightarrow> P s" 382 and "\<And>s t a. reachable A s \<Longrightarrow> P s \<Longrightarrow> (s, a, t) \<in> trans_of A \<longrightarrow> P t" 383 shows "invariant A P" 384 using assms 385 apply (unfold invariant_def) 386 apply (rule allI) 387 apply (rule impI) 388 apply (rule_tac x = "s" in reachable.induct) 389 apply assumption 390 apply blast 391 apply blast 392 done 393 394lemma invariantI1: 395 assumes "\<And>s. s \<in> starts_of A \<Longrightarrow> P s" 396 and "\<And>s t a. reachable A s \<Longrightarrow> P s \<longrightarrow> (s, a, t) \<in> trans_of A \<longrightarrow> P t" 397 shows "invariant A P" 398 using assms by (blast intro: invariantI) 399 400lemma invariantE: "invariant A P \<Longrightarrow> reachable A s \<Longrightarrow> P s" 401 unfolding invariant_def by blast 402 403 404subsection \<open>\<open>restrict\<close>\<close> 405 406lemmas reachable_0 = reachable.reachable_0 407 and reachable_n = reachable.reachable_n 408 409lemma cancel_restrict_a: 410 "starts_of (restrict ioa acts) = starts_of ioa \<and> 411 trans_of (restrict ioa acts) = trans_of ioa" 412 by (simp add: restrict_def ioa_projections) 413 414lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s" 415 apply (rule iffI) 416 apply (erule reachable.induct) 417 apply (simp add: cancel_restrict_a reachable_0) 418 apply (erule reachable_n) 419 apply (simp add: cancel_restrict_a) 420 text \<open>\<open>\<longleftarrow>\<close>\<close> 421 apply (erule reachable.induct) 422 apply (rule reachable_0) 423 apply (simp add: cancel_restrict_a) 424 apply (erule reachable_n) 425 apply (simp add: cancel_restrict_a) 426 done 427 428lemma acts_restrict: "act (restrict A acts) = act A" 429 by (auto simp add: actions_def asig_internals_def 430 asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def) 431 432lemma cancel_restrict: 433 "starts_of (restrict ioa acts) = starts_of ioa \<and> 434 trans_of (restrict ioa acts) = trans_of ioa \<and> 435 reachable (restrict ioa acts) s = reachable ioa s \<and> 436 act (restrict A acts) = act A" 437 by (simp add: cancel_restrict_a cancel_restrict_b acts_restrict) 438 439 440subsection \<open>\<open>rename\<close>\<close> 441 442lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t \<Longrightarrow> (\<exists>x. Some x = f a \<and> s \<midarrow>x\<midarrow>C\<rightarrow> t)" 443 by (simp add: Let_def rename_def trans_of_def) 444 445lemma reachable_rename: "reachable (rename C g) s \<Longrightarrow> reachable C s" 446 apply (erule reachable.induct) 447 apply (rule reachable_0) 448 apply (simp add: rename_def ioa_projections) 449 apply (drule trans_rename) 450 apply (erule exE) 451 apply (erule conjE) 452 apply (erule reachable_n) 453 apply assumption 454 done 455 456 457subsection \<open>\<open>trans_of (A \<parallel> B)\<close>\<close> 458 459lemma trans_A_proj: 460 "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act A \<Longrightarrow> (fst s, a, fst t) \<in> trans_of A" 461 by (simp add: Let_def par_def trans_of_def) 462 463lemma trans_B_proj: 464 "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act B \<Longrightarrow> (snd s, a, snd t) \<in> trans_of B" 465 by (simp add: Let_def par_def trans_of_def) 466 467lemma trans_A_proj2: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<notin> act A \<Longrightarrow> fst s = fst t" 468 by (simp add: Let_def par_def trans_of_def) 469 470lemma trans_B_proj2: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<notin> act B \<Longrightarrow> snd s = snd t" 471 by (simp add: Let_def par_def trans_of_def) 472 473lemma trans_AB_proj: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act A \<or> a \<in> act B" 474 by (simp add: Let_def par_def trans_of_def) 475 476lemma trans_AB: 477 "a \<in> act A \<Longrightarrow> a \<in> act B \<Longrightarrow> 478 (fst s, a, fst t) \<in> trans_of A \<Longrightarrow> 479 (snd s, a, snd t) \<in> trans_of B \<Longrightarrow> 480 (s, a, t) \<in> trans_of (A \<parallel> B)" 481 by (simp add: Let_def par_def trans_of_def) 482 483lemma trans_A_notB: 484 "a \<in> act A \<Longrightarrow> a \<notin> act B \<Longrightarrow> 485 (fst s, a, fst t) \<in> trans_of A \<Longrightarrow> 486 snd s = snd t \<Longrightarrow> 487 (s, a, t) \<in> trans_of (A \<parallel> B)" 488 by (simp add: Let_def par_def trans_of_def) 489 490lemma trans_notA_B: 491 "a \<notin> act A \<Longrightarrow> a \<in> act B \<Longrightarrow> 492 (snd s, a, snd t) \<in> trans_of B \<Longrightarrow> 493 fst s = fst t \<Longrightarrow> 494 (s, a, t) \<in> trans_of (A \<parallel> B)" 495 by (simp add: Let_def par_def trans_of_def) 496 497lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B 498 and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj 499 500 501lemma trans_of_par4: 502 "(s, a, t) \<in> trans_of (A \<parallel> B \<parallel> C \<parallel> D) \<longleftrightarrow> 503 ((a \<in> actions (asig_of A) \<or> a \<in> actions (asig_of B) \<or> a \<in> actions (asig_of C) \<or> 504 a \<in> actions (asig_of D)) \<and> 505 (if a \<in> actions (asig_of A) 506 then (fst s, a, fst t) \<in> trans_of A 507 else fst t = fst s) \<and> 508 (if a \<in> actions (asig_of B) 509 then (fst (snd s), a, fst (snd t)) \<in> trans_of B 510 else fst (snd t) = fst (snd s)) \<and> 511 (if a \<in> actions (asig_of C) 512 then (fst (snd (snd s)), a, fst (snd (snd t))) \<in> trans_of C 513 else fst (snd (snd t)) = fst (snd (snd s))) \<and> 514 (if a \<in> actions (asig_of D) 515 then (snd (snd (snd s)), a, snd (snd (snd t))) \<in> trans_of D 516 else snd (snd (snd t)) = snd (snd (snd s))))" 517 by (simp add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections) 518 519 520subsection \<open>Proof obligation generator for IOA requirements\<close> 521 522(*without assumptions on A and B because is_trans_of is also incorporated in par_def*) 523lemma is_trans_of_par: "is_trans_of (A \<parallel> B)" 524 by (simp add: is_trans_of_def Let_def actions_of_par trans_of_par) 525 526lemma is_trans_of_restrict: "is_trans_of A \<Longrightarrow> is_trans_of (restrict A acts)" 527 by (simp add: is_trans_of_def cancel_restrict acts_restrict) 528 529lemma is_trans_of_rename: "is_trans_of A \<Longrightarrow> is_trans_of (rename A f)" 530 apply (unfold is_trans_of_def restrict_def restrict_asig_def) 531 apply (simp add: Let_def actions_def trans_of_def asig_internals_def 532 asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def) 533 apply blast 534 done 535 536lemma is_asig_of_par: "is_asig_of A \<Longrightarrow> is_asig_of B \<Longrightarrow> compatible A B \<Longrightarrow> is_asig_of (A \<parallel> B)" 537 apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def 538 asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def) 539 apply (simp add: asig_of_def) 540 apply auto 541 done 542 543lemma is_asig_of_restrict: "is_asig_of A \<Longrightarrow> is_asig_of (restrict A f)" 544 apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def 545 asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def) 546 apply simp 547 apply auto 548 done 549 550lemma is_asig_of_rename: "is_asig_of A \<Longrightarrow> is_asig_of (rename A f)" 551 apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def 552 asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def) 553 apply auto 554 apply (drule_tac [!] s = "Some _" in sym) 555 apply auto 556 done 557 558lemmas [simp] = is_asig_of_par is_asig_of_restrict 559 is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename 560 561 562lemma compatible_par: "compatible A B \<Longrightarrow> compatible A C \<Longrightarrow> compatible A (B \<parallel> C)" 563 by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par) 564 565(*better derive by previous one and compat_commute*) 566lemma compatible_par2: "compatible A C \<Longrightarrow> compatible B C \<Longrightarrow> compatible (A \<parallel> B) C" 567 by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par) 568 569lemma compatible_restrict: 570 "compatible A B \<Longrightarrow> (ext B - S) \<inter> ext A = {} \<Longrightarrow> compatible A (restrict B S)" 571 by (auto simp add: compatible_def ioa_triple_proj asig_triple_proj externals_def 572 restrict_def restrict_asig_def actions_def) 573 574declare split_paired_Ex [simp] 575 576end 577