src/HOLCF/IOA/meta_theory/CompoExecs.ML

 (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
     ID:         $Id$
     Author:     Olaf Müller
-
-Compositionality on Execution level.
-*)  
-
-Delsimps (ex_simps @ all_simps); 
+*)
+
+Delsimps (ex_simps @ all_simps);
 Delsimps [split_paired_All];
 
 (* ----------------------------------------------------------------------------------- *)
 
 

 Goal "Filter_ex2 sig$nil=nil";
 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_nil";
 
 Goal "Filter_ex2 sig$(at >> xs) =    \
-\            (if (fst at:actions sig)    \       
-\                 then at >> (Filter_ex2 sig$xs) \   
+\            (if (fst at:actions sig)    \
+\                 then at >> (Filter_ex2 sig$xs) \
 \                 else        Filter_ex2 sig$xs)";
 
 by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_cons";
 

 (* ---------------------------------------------------------------- *)
 
 
 Goal "stutter2 sig = (LAM ex. (%s. case ex of \
 \      nil => TT \
-\    | x##xs => (flift1 \ 
+\    | 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) \

 by (Simp_tac 1);
 qed"stutter2_nil";
 
 Goal "(stutter2 sig$(at>>xs)) s = \
 \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
-\                andalso (stutter2 sig$xs) (snd at))"; 
+\                andalso (stutter2 sig$xs) (snd at))";
 by (rtac trans 1);
 by (stac stutter2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
 by (Simp_tac 1);
 qed"stutter2_cons";

 (*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
 (* --------------------------------------------------------------------- *)
 
 Goal "!s. is_exec_frag (A||B) (s,xs) \
 \      --> stutter (asig_of A) (fst s,ProjA2$xs)  &\
-\          stutter (asig_of B) (snd s,ProjB2$xs)"; 
+\          stutter (asig_of B) (snd s,ProjB2$xs)";
 
 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
 (* main case *)
 by (safe_tac set_cs);
 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));

 \  --> Forall (%x. fst x:act (A||B)) xs)";
 
 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
 (* main case *)
 by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @
                                 [actions_asig_comp,asig_of_par]) 1));
 qed"lemma_1_1c";
 
 
 (* ----------------------------------------------------------------------- *)
 (*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
 (* ----------------------------------------------------------------------- *)
 
-Goal 
+Goal
 "!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 \

 (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
 (*                          Main Theorem                              *)
 (* ------------------------------------------------------------------ *)
 
 
-Goal 
+Goal
 "(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))";

 
 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
 by (rtac set_ext 1);
 by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
 qed"compositionality_ex_modules";
-
-
-
-
-
-
-