--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,49 +9,33 @@
imports Traces
begin
-consts
+definition
+ ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where
+ "ProjA2 = Map (%x.(fst x,fst(snd x)))"
- 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)"
+definition
+ ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where
+ "ProjA ex = (fst (fst ex), ProjA2$(snd ex))"
- 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))"
+definition
+ ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where
+ "ProjB2 = Map (%x.(fst x,snd(snd x)))"
-ProjB_def:
- "ProjB ex == (snd (fst ex), ProjB2$(snd ex))"
-
+definition
+ ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where
+ "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)))"
-
+definition
+ Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where
+ "Filter_ex2 sig = Filter (%x. fst x:actions sig)"
-Filter_ex_def:
- "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
-
+definition
+ Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where
+ "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
+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)
@@ -61,9 +45,14 @@
$x)
)))"
-par_execs_def:
- "par_execs ExecsA ExecsB ==
- let exA = fst ExecsA; sigA = snd ExecsA;
+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}
@@ -71,8 +60,7 @@
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)"
-
+ asig_comp sigA sigB))"
lemmas [simp del] = ex_simps all_simps split_paired_All
@@ -131,9 +119,9 @@
apply (simp add: Filter_ex2_def)
done
-lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) =
- (if (fst at:actions sig)
- then at >> (Filter_ex2 sig$xs)
+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)"
apply (simp add: Filter_ex2_def)
@@ -145,18 +133,18 @@
(* ---------------------------------------------------------------- *)
-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 fi)
- andalso (stutter2 sig$xs) (snd p))
- $x)
+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 fi)
+ andalso (stutter2 sig$xs) (snd p))
+ $x)
))"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule stutter2_def)
+apply (simp only: stutter2_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
done
@@ -171,8 +159,8 @@
apply simp
done
-lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s =
- ((if (fst at)~:actions sig then Def (s=snd at) else TT)
+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)
@@ -196,7 +184,7 @@
apply (simp add: stutter_def)
done
-lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
+lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
apply (simp add: stutter_def)
done
@@ -224,8 +212,8 @@
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
- --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
+lemma 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))"
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
@@ -240,8 +228,8 @@
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
- --> stutter (asig_of A) (fst s,ProjA2$xs) &
+lemma 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)"
apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
@@ -255,7 +243,7 @@
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
+lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
--> Forall (%x. fst x:act (A||B)) xs)"
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
@@ -270,12 +258,12 @@
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *)
(* ----------------------------------------------------------------------- *)
-lemma 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
+lemma 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)"
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
@@ -289,11 +277,11 @@
subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
-lemma 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) &
+lemma 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 (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
@@ -310,7 +298,7 @@
subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
-lemma compositionality_ex_modules:
+lemma compositionality_ex_modules:
"Execs (A||B) = par_execs (Execs A) (Execs B)"
apply (unfold Execs_def par_execs_def)
apply (simp add: asig_of_par)