# Theory CompoExecs

theory CompoExecs
imports Traces
```(*  Title:      HOL/HOLCF/IOA/CompoExecs.thy
Author:     Olaf MÃ¼ller
*)

section ‹Compositionality on Execution level›

theory CompoExecs
imports Traces
begin

definition ProjA2 :: "('a, 's × 't) pairs → ('a, 's) pairs"
where "ProjA2 = Map (λx. (fst x, fst (snd x)))"

definition ProjA :: "('a, 's × 't) execution ⇒ ('a, 's) execution"
where "ProjA ex = (fst (fst ex), ProjA2 ⋅ (snd ex))"

definition ProjB2 :: "('a, 's × 't) pairs → ('a, 't) pairs"
where "ProjB2 = Map (λx. (fst x, snd (snd x)))"

definition ProjB :: "('a, 's × 't) execution ⇒ ('a, 't) execution"
where "ProjB ex = (snd (fst ex), ProjB2 ⋅ (snd ex))"

definition Filter_ex2 :: "'a signature ⇒ ('a, 's) pairs → ('a, 's) pairs"
where "Filter_ex2 sig = Filter (λx. fst x ∈ actions sig)"

definition Filter_ex :: "'a signature ⇒ ('a, 's) execution ⇒ ('a, 's) execution"
where "Filter_ex sig ex = (fst ex, Filter_ex2 sig ⋅ (snd ex))"

definition stutter2 :: "'a signature ⇒ ('a, 's) pairs → ('s ⇒ tr)"
where "stutter2 sig =
(fix ⋅
(LAM h ex.
(λs.
case ex of
nil ⇒ TT
| x ## xs ⇒
(flift1
(λp.
(If Def (fst p ∉ actions sig) then Def (s = snd p) else TT)
andalso (h⋅xs) (snd p)) ⋅ x))))"

definition stutter :: "'a signature ⇒ ('a, 's) execution ⇒ bool"
where "stutter sig ex ⟷ (stutter2 sig ⋅ (snd ex)) (fst ex) ≠ FF"

definition par_execs ::
"('a, 's) execution_module ⇒ ('a, 't) execution_module ⇒ ('a, 's × 't) execution_module"
where "par_execs ExecsA ExecsB =
(let
exA = fst ExecsA; sigA = snd ExecsA;
exB = fst ExecsB; sigB = snd ExecsB
in
({ex. Filter_ex sigA (ProjA ex) ∈ exA} ∩
{ex. Filter_ex sigB (ProjB ex) ∈ exB} ∩
{ex. stutter sigA (ProjA ex)} ∩
{ex. stutter sigB (ProjB ex)} ∩
{ex. Forall (λx. fst x ∈ actions sigA ∪ actions sigB) (snd ex)},
asig_comp sigA sigB))"

lemmas [simp del] = split_paired_All

section ‹Recursive equations of operators›

subsection ‹‹ProjA2››

lemma ProjA2_UU: "ProjA2 ⋅ UU = UU"

lemma ProjA2_nil: "ProjA2 ⋅ nil = nil"

lemma ProjA2_cons: "ProjA2 ⋅ ((a, t) ↝ xs) = (a, fst t) ↝ ProjA2 ⋅ xs"

subsection ‹‹ProjB2››

lemma ProjB2_UU: "ProjB2 ⋅ UU = UU"

lemma ProjB2_nil: "ProjB2 ⋅ nil = nil"

lemma ProjB2_cons: "ProjB2 ⋅ ((a, t) ↝ xs) = (a, snd t) ↝ ProjB2 ⋅ xs"

subsection ‹‹Filter_ex2››

lemma Filter_ex2_UU: "Filter_ex2 sig ⋅ UU = UU"

lemma Filter_ex2_nil: "Filter_ex2 sig ⋅ nil = nil"

lemma Filter_ex2_cons:
"Filter_ex2 sig ⋅ (at ↝ xs) =
(if fst at ∈ actions sig
then at ↝ (Filter_ex2 sig ⋅ xs)
else Filter_ex2 sig ⋅ xs)"

subsection ‹‹stutter2››

lemma stutter2_unfold:
"stutter2 sig =
(LAM ex.
(λs.
case ex of
nil ⇒ TT
| x ## xs ⇒
(flift1
(λp.
(If Def (fst p ∉ actions sig) then Def (s= snd p) else TT)
andalso (stutter2 sig⋅xs) (snd p)) ⋅ x)))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: stutter2_def)
apply (rule beta_cfun)
done

lemma stutter2_UU: "(stutter2 sig ⋅ UU) s = UU"
apply (subst stutter2_unfold)
apply simp
done

lemma stutter2_nil: "(stutter2 sig ⋅ nil) s = TT"
apply (subst stutter2_unfold)
apply simp
done

lemma stutter2_cons:
"(stutter2 sig ⋅ (at ↝ xs)) s =
((if fst at ∉ actions sig then Def (s = snd at) else TT)
andalso (stutter2 sig ⋅ xs) (snd at))"
apply (rule trans)
apply (subst stutter2_unfold)
apply (simp add: Consq_def flift1_def If_and_if)
apply simp
done

declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp]

subsection ‹‹stutter››

lemma stutter_UU: "stutter sig (s, UU)"

lemma stutter_nil: "stutter sig (s, nil)"

lemma stutter_cons:
"stutter sig (s, (a, t) ↝ ex) ⟷ (a ∉ actions sig ⟶ (s = t)) ∧ stutter sig (t, ex)"

declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del]

lemmas compoex_simps = ProjA2_UU ProjA2_nil ProjA2_cons
ProjB2_UU ProjB2_nil ProjB2_cons
Filter_ex2_UU Filter_ex2_nil Filter_ex2_cons
stutter_UU stutter_nil stutter_cons

declare compoex_simps [simp]

section ‹Compositionality on execution level›

lemma lemma_1_1a:
― ‹‹is_ex_fr› propagates from ‹A ∥ B› to projections ‹A› and ‹B››
"∀s. is_exec_frag (A ∥ B) (s, xs) ⟶
is_exec_frag A (fst s, Filter_ex2 (asig_of A) ⋅ (ProjA2 ⋅ xs)) ∧
is_exec_frag B (snd s, Filter_ex2 (asig_of B) ⋅ (ProjB2 ⋅ xs))"
apply (pair_induct xs simp: is_exec_frag_def)
text ‹main case›
done

lemma lemma_1_1b:
― ‹‹is_ex_fr (A ∥ B)› implies stuttering on projections›
"∀s. is_exec_frag (A ∥ B) (s, xs) ⟶
stutter (asig_of A) (fst s, ProjA2 ⋅ xs) ∧
stutter (asig_of B) (snd s, ProjB2 ⋅ xs)"
apply (pair_induct xs simp: stutter_def is_exec_frag_def)
text ‹main case›
done

lemma lemma_1_1c:
― ‹Executions of ‹A ∥ B› have only ‹A›- or ‹B›-actions›
"∀s. is_exec_frag (A ∥ B) (s, xs) ⟶ Forall (λx. fst x ∈ act (A ∥ B)) xs"
apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def)
text ‹main case›
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
done

lemma lemma_1_2:
― ‹‹ex A›, ‹exB›, stuttering and forall ‹a ∈ A ∥ B› implies ‹ex (A ∥ B)››
"∀s.
is_exec_frag A (fst s, Filter_ex2 (asig_of A) ⋅ (ProjA2 ⋅ xs)) ∧
is_exec_frag B (snd s, Filter_ex2 (asig_of B) ⋅ (ProjB2 ⋅ xs)) ∧
stutter (asig_of A) (fst s, ProjA2 ⋅ xs) ∧
stutter (asig_of B) (snd s, ProjB2 ⋅ xs) ∧
Forall (λx. fst x ∈ act (A ∥ B)) xs ⟶
is_exec_frag (A ∥ B) (s, xs)"
apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def)
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
done

theorem compositionality_ex:
"ex ∈ executions (A ∥ B) ⟷
Filter_ex (asig_of A) (ProjA ex) : executions A ∧
Filter_ex (asig_of B) (ProjB ex) : executions B ∧
stutter (asig_of A) (ProjA ex) ∧
stutter (asig_of B) (ProjB ex) ∧
Forall (λx. fst x ∈ act (A ∥ B)) (snd ex)"
apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
apply (pair ex)
apply (rule iffI)
text ‹‹⟹››
apply (erule conjE)+
apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c)
text ‹‹⟸››
apply (erule conjE)+