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