Up to index of Isabelle/HOLCF/IOA
theory CompoExecs(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy ID: $Id: CompoExecs.thy,v 1.8 2005/09/02 15:24:00 wenzelm Exp $ Author: Olaf Müller *) header {* Compositionality on Execution level *} theory CompoExecs imports Traces begin consts ProjA ::"('a,'s * 't)execution => ('a,'s)execution" ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs" ProjB ::"('a,'s * 't)execution => ('a,'t)execution" ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs" Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution" Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs" stutter ::"'a signature => ('a,'s)execution => bool" stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)" par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" defs ProjA_def: "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" ProjB_def: "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" ProjA2_def: "ProjA2 == Map (%x.(fst x,fst(snd x)))" ProjB2_def: "ProjB2 == Map (%x.(fst x,snd(snd x)))" Filter_ex_def: "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))" Filter_ex2_def: "Filter_ex2 sig == Filter (%x. fst x:actions sig)" stutter_def: "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" stutter2_def: "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 fi) andalso (h$xs) (snd p)) $x) )))" par_execs_def: "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} Int {ex. Filter_ex sigB (ProjB ex) : exB} Int {ex. stutter sigA (ProjA ex)} Int {ex. stutter sigB (ProjB ex)} Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)}, asig_comp sigA sigB)" ML {* use_legacy_bindings (the_context ()) *} end
theorem ProjA2_UU:
ProjA2·UU = UU
theorem ProjA2_nil:
ProjA2·nil = nil
theorem ProjA2_cons:
ProjA2·((a, t)>>xs) = (a, fst t)>>ProjA2·xs
theorem ProjB2_UU:
ProjB2·UU = UU
theorem ProjB2_nil:
ProjB2·nil = nil
theorem ProjB2_cons:
ProjB2·((a, t)>>xs) = (a, snd t)>>ProjB2·xs
theorem Filter_ex2_UU:
Filter_ex2 sig·UU = UU
theorem Filter_ex2_nil:
Filter_ex2 sig·nil = nil
theorem Filter_ex2_cons:
Filter_ex2 sig·(at>>xs) = (if fst at ∈ actions sig then at>>Filter_ex2 sig·xs else Filter_ex2 sig·xs)
theorem stutter2_unfold:
stutter2 sig = (LAM ex. (%s. case ex of nil => TT | x ## xs => (FLIFT p. If Def (fst p ∉ actions sig) then Def (s = snd p) else TT fi andalso (stutter2 sig·xs) (snd p))·x))
theorem stutter2_UU:
(stutter2 sig·UU) s = UU
theorem stutter2_nil:
(stutter2 sig·nil) s = TT
theorem 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))
theorem stutter_UU:
stutter sig (s, UU)
theorem stutter_nil:
stutter sig (s, nil)
theorem stutter_cons:
stutter sig (s, (a, t)>>ex) = ((a ∉ actions sig --> s = t) ∧ stutter sig (t, ex))
theorem lemma_1_1a:
∀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))
theorem lemma_1_1b:
∀s. is_exec_frag (A || B) (s, xs) --> stutter (asig_of A) (fst s, ProjA2·xs) ∧ stutter (asig_of B) (snd s, ProjB2·xs)
theorem lemma_1_1c:
∀s. is_exec_frag (A || B) (s, xs) --> Forall (%x. fst x ∈ act (A || B)) xs
theorem lemma_1_2:
∀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)
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))
theorem compositionality_ex_modules:
Execs (A || B) = par_execs (Execs A) (Execs B)