1(* Title: HOL/HOLCF/IOA/CompoExecs.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Compositionality on Execution level\<close> 6 7theory CompoExecs 8imports Traces 9begin 10 11definition ProjA2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 's) pairs" 12 where "ProjA2 = Map (\<lambda>x. (fst x, fst (snd x)))" 13 14definition ProjA :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 's) execution" 15 where "ProjA ex = (fst (fst ex), ProjA2 \<cdot> (snd ex))" 16 17definition ProjB2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 't) pairs" 18 where "ProjB2 = Map (\<lambda>x. (fst x, snd (snd x)))" 19 20definition ProjB :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 't) execution" 21 where "ProjB ex = (snd (fst ex), ProjB2 \<cdot> (snd ex))" 22 23definition Filter_ex2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('a, 's) pairs" 24 where "Filter_ex2 sig = Filter (\<lambda>x. fst x \<in> actions sig)" 25 26definition Filter_ex :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> ('a, 's) execution" 27 where "Filter_ex sig ex = (fst ex, Filter_ex2 sig \<cdot> (snd ex))" 28 29definition stutter2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('s \<Rightarrow> tr)" 30 where "stutter2 sig = 31 (fix \<cdot> 32 (LAM h ex. 33 (\<lambda>s. 34 case ex of 35 nil \<Rightarrow> TT 36 | x ## xs \<Rightarrow> 37 (flift1 38 (\<lambda>p. 39 (If Def (fst p \<notin> actions sig) then Def (s = snd p) else TT) 40 andalso (h\<cdot>xs) (snd p)) \<cdot> x))))" 41 42definition stutter :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 43 where "stutter sig ex \<longleftrightarrow> (stutter2 sig \<cdot> (snd ex)) (fst ex) \<noteq> FF" 44 45definition par_execs :: 46 "('a, 's) execution_module \<Rightarrow> ('a, 't) execution_module \<Rightarrow> ('a, 's \<times> 't) execution_module" 47 where "par_execs ExecsA ExecsB = 48 (let 49 exA = fst ExecsA; sigA = snd ExecsA; 50 exB = fst ExecsB; sigB = snd ExecsB 51 in 52 ({ex. Filter_ex sigA (ProjA ex) \<in> exA} \<inter> 53 {ex. Filter_ex sigB (ProjB ex) \<in> exB} \<inter> 54 {ex. stutter sigA (ProjA ex)} \<inter> 55 {ex. stutter sigB (ProjB ex)} \<inter> 56 {ex. Forall (\<lambda>x. fst x \<in> actions sigA \<union> actions sigB) (snd ex)}, 57 asig_comp sigA sigB))" 58 59 60lemmas [simp del] = split_paired_All 61 62 63section \<open>Recursive equations of operators\<close> 64 65subsection \<open>\<open>ProjA2\<close>\<close> 66 67lemma ProjA2_UU: "ProjA2 \<cdot> UU = UU" 68 by (simp add: ProjA2_def) 69 70lemma ProjA2_nil: "ProjA2 \<cdot> nil = nil" 71 by (simp add: ProjA2_def) 72 73lemma ProjA2_cons: "ProjA2 \<cdot> ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 \<cdot> xs" 74 by (simp add: ProjA2_def) 75 76 77subsection \<open>\<open>ProjB2\<close>\<close> 78 79lemma ProjB2_UU: "ProjB2 \<cdot> UU = UU" 80 by (simp add: ProjB2_def) 81 82lemma ProjB2_nil: "ProjB2 \<cdot> nil = nil" 83 by (simp add: ProjB2_def) 84 85lemma ProjB2_cons: "ProjB2 \<cdot> ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 \<cdot> xs" 86 by (simp add: ProjB2_def) 87 88 89subsection \<open>\<open>Filter_ex2\<close>\<close> 90 91lemma Filter_ex2_UU: "Filter_ex2 sig \<cdot> UU = UU" 92 by (simp add: Filter_ex2_def) 93 94lemma Filter_ex2_nil: "Filter_ex2 sig \<cdot> nil = nil" 95 by (simp add: Filter_ex2_def) 96 97lemma Filter_ex2_cons: 98 "Filter_ex2 sig \<cdot> (at \<leadsto> xs) = 99 (if fst at \<in> actions sig 100 then at \<leadsto> (Filter_ex2 sig \<cdot> xs) 101 else Filter_ex2 sig \<cdot> xs)" 102 by (simp add: Filter_ex2_def) 103 104 105subsection \<open>\<open>stutter2\<close>\<close> 106 107lemma stutter2_unfold: 108 "stutter2 sig = 109 (LAM ex. 110 (\<lambda>s. 111 case ex of 112 nil \<Rightarrow> TT 113 | x ## xs \<Rightarrow> 114 (flift1 115 (\<lambda>p. 116 (If Def (fst p \<notin> actions sig) then Def (s= snd p) else TT) 117 andalso (stutter2 sig\<cdot>xs) (snd p)) \<cdot> x)))" 118 apply (rule trans) 119 apply (rule fix_eq2) 120 apply (simp only: stutter2_def) 121 apply (rule beta_cfun) 122 apply (simp add: flift1_def) 123 done 124 125lemma stutter2_UU: "(stutter2 sig \<cdot> UU) s = UU" 126 apply (subst stutter2_unfold) 127 apply simp 128 done 129 130lemma stutter2_nil: "(stutter2 sig \<cdot> nil) s = TT" 131 apply (subst stutter2_unfold) 132 apply simp 133 done 134 135lemma stutter2_cons: 136 "(stutter2 sig \<cdot> (at \<leadsto> xs)) s = 137 ((if fst at \<notin> actions sig then Def (s = snd at) else TT) 138 andalso (stutter2 sig \<cdot> xs) (snd at))" 139 apply (rule trans) 140 apply (subst stutter2_unfold) 141 apply (simp add: Consq_def flift1_def If_and_if) 142 apply simp 143 done 144 145declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp] 146 147 148subsection \<open>\<open>stutter\<close>\<close> 149 150lemma stutter_UU: "stutter sig (s, UU)" 151 by (simp add: stutter_def) 152 153lemma stutter_nil: "stutter sig (s, nil)" 154 by (simp add: stutter_def) 155 156lemma stutter_cons: 157 "stutter sig (s, (a, t) \<leadsto> ex) \<longleftrightarrow> (a \<notin> actions sig \<longrightarrow> (s = t)) \<and> stutter sig (t, ex)" 158 by (simp add: stutter_def) 159 160declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del] 161 162lemmas compoex_simps = ProjA2_UU ProjA2_nil ProjA2_cons 163 ProjB2_UU ProjB2_nil ProjB2_cons 164 Filter_ex2_UU Filter_ex2_nil Filter_ex2_cons 165 stutter_UU stutter_nil stutter_cons 166 167declare compoex_simps [simp] 168 169 170section \<open>Compositionality on execution level\<close> 171 172lemma lemma_1_1a: 173 \<comment> \<open>\<open>is_ex_fr\<close> propagates from \<open>A \<parallel> B\<close> to projections \<open>A\<close> and \<open>B\<close>\<close> 174 "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> 175 is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and> 176 is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs))" 177 apply (pair_induct xs simp: is_exec_frag_def) 178 text \<open>main case\<close> 179 apply (auto simp add: trans_of_defs2) 180 done 181 182lemma lemma_1_1b: 183 \<comment> \<open>\<open>is_ex_fr (A \<parallel> B)\<close> implies stuttering on projections\<close> 184 "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> 185 stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and> 186 stutter (asig_of B) (snd s, ProjB2 \<cdot> xs)" 187 apply (pair_induct xs simp: stutter_def is_exec_frag_def) 188 text \<open>main case\<close> 189 apply (auto simp add: trans_of_defs2) 190 done 191 192lemma lemma_1_1c: 193 \<comment> \<open>Executions of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions\<close> 194 "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs" 195 apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def) 196 text \<open>main case\<close> 197 apply auto 198 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) 199 done 200 201lemma lemma_1_2: 202 \<comment> \<open>\<open>ex A\<close>, \<open>exB\<close>, stuttering and forall \<open>a \<in> A \<parallel> B\<close> implies \<open>ex (A \<parallel> B)\<close>\<close> 203 "\<forall>s. 204 is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and> 205 is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs)) \<and> 206 stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and> 207 stutter (asig_of B) (snd s, ProjB2 \<cdot> xs) \<and> 208 Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow> 209 is_exec_frag (A \<parallel> B) (s, xs)" 210 apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def) 211 apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par) 212 done 213 214theorem compositionality_ex: 215 "ex \<in> executions (A \<parallel> B) \<longleftrightarrow> 216 Filter_ex (asig_of A) (ProjA ex) \<in> executions A \<and> 217 Filter_ex (asig_of B) (ProjB ex) \<in> executions B \<and> 218 stutter (asig_of A) (ProjA ex) \<and> 219 stutter (asig_of B) (ProjB ex) \<and> 220 Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd ex)" 221 apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par) 222 apply (pair ex) 223 apply (rule iffI) 224 text \<open>\<open>\<Longrightarrow>\<close>\<close> 225 apply (erule conjE)+ 226 apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c) 227 text \<open>\<open>\<Longleftarrow>\<close>\<close> 228 apply (erule conjE)+ 229 apply (simp add: lemma_1_2) 230 done 231 232theorem compositionality_ex_modules: "Execs (A \<parallel> B) = par_execs (Execs A) (Execs B)" 233 apply (unfold Execs_def par_execs_def) 234 apply (simp add: asig_of_par) 235 apply (rule set_eqI) 236 apply (simp add: compositionality_ex actions_of_par) 237 done 238 239end 240