# File CompoExecs.ML

    (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
        ID:         $Id: CompoExecs.ML,v 1.17 2005/09/02 15:24:00 wenzelm Exp $
        Author:     Olaf Müller
    *)

    Delsimps (ex_simps @ all_simps);
    Delsimps [split_paired_All];

    (* ----------------------------------------------------------------------------------- *)

    section "recursive equations of operators";

    (* ---------------------------------------------------------------- *)
    (*                               ProjA2                             *)
    (* ---------------------------------------------------------------- *)

    Goal  "ProjA2$UU = UU";
    by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    qed"ProjA2_UU";

    Goal  "ProjA2$nil = nil";
    by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    qed"ProjA2_nil";

    Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs";
    by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    qed"ProjA2_cons";

    (* ---------------------------------------------------------------- *)
    (*                               ProjB2                             *)
    (* ---------------------------------------------------------------- *)

    Goal  "ProjB2$UU = UU";
    by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    qed"ProjB2_UU";

    Goal  "ProjB2$nil = nil";
    by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    qed"ProjB2_nil";

    Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs";
    by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    qed"ProjB2_cons";

    (* ---------------------------------------------------------------- *)
    (*                             Filter_ex2                           *)
    (* ---------------------------------------------------------------- *)

    Goal "Filter_ex2 sig$UU=UU";
    by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    qed"Filter_ex2_UU";

    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) \
    \                 else        Filter_ex2 sig$xs)";

    by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    qed"Filter_ex2_cons";

    (* ---------------------------------------------------------------- *)
    (*                             stutter2                             *)
    (* ---------------------------------------------------------------- *)

    Goal "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) \
    \           ))";
    by (rtac trans 1);
    by (rtac fix_eq2 1);
    by (rtac stutter2_def 1);
    by (rtac beta_cfun 1);
    by (simp_tac (simpset() addsimps [flift1_def]) 1);
    qed"stutter2_unfold";

    Goal "(stutter2 sig$UU) s=UU";
    by (stac stutter2_unfold 1);
    by (Simp_tac 1);
    qed"stutter2_UU";

    Goal "(stutter2 sig$nil) s = TT";
    by (stac stutter2_unfold 1);
    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))";
    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";

    Addsimps [stutter2_UU,stutter2_nil,stutter2_cons];

    (* ---------------------------------------------------------------- *)
    (*                             stutter                              *)
    (* ---------------------------------------------------------------- *)

    Goal "stutter sig (s, UU)";
    by (simp_tac (simpset() addsimps [stutter_def]) 1);
    qed"stutter_UU";

    Goal "stutter sig (s, nil)";
    by (simp_tac (simpset() addsimps [stutter_def]) 1);
    qed"stutter_nil";

    Goal "stutter sig (s, (a,t)>>ex) = \
    \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
    by (simp_tac (simpset() addsimps [stutter_def]) 1);
    qed"stutter_cons";

    (* ----------------------------------------------------------------------------------- *)

    Delsimps [stutter2_UU,stutter2_nil,stutter2_cons];

    val 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];

    Addsimps compoex_simps;

    (* ------------------------------------------------------------------ *)
    (*                      The following lemmata aim for                 *)
    (*             COMPOSITIONALITY   on    EXECUTION     Level           *)
    (* ------------------------------------------------------------------ *)

    (* --------------------------------------------------------------------- *)
    (*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
    (* --------------------------------------------------------------------- *)

    Goal "!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))";

    by (pair_induct_tac "xs" [is_exec_frag_def] 1);
    (* main case *)
    ren "ss a t" 1;
    by (safe_tac set_cs);
    by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
    qed"lemma_1_1a";

    (* --------------------------------------------------------------------- *)
    (*  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)";

    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));
    qed"lemma_1_1b";

    (* --------------------------------------------------------------------- *)
    (*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
    (* --------------------------------------------------------------------- *)

    Goal "!s. (is_exec_frag (A||B) (s,xs) \
    \  --> 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 @
                                    [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
    "!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)";

    by (pair_induct_tac "xs" [Forall_def,sforall_def,
             is_exec_frag_def, stutter_def] 1);
    by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 1);
    by (safe_tac set_cs);
    (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
    by (rotate_tac ~4 1);
    by (Asm_full_simp_tac 1);
    by (rotate_tac ~4 1);
    by (Asm_full_simp_tac 1);
    qed"lemma_1_2";

    (* ------------------------------------------------------------------ *)
    (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
    (*                          Main Theorem                              *)
    (* ------------------------------------------------------------------ *)

    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 (simp_tac (simpset() addsimps [executions_def,ProjB_def,
                                     Filter_ex_def,ProjA_def,starts_of_par]) 1);
    by (pair_tac "ex" 1);
    by (rtac iffI 1);
    (* ==>  *)
    by (REPEAT (etac conjE 1));
    by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp,
                   lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
    (* <==  *)
    by (REPEAT (etac conjE 1));
    by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1);
    qed"compositionality_ex";

    (* ------------------------------------------------------------------ *)
    (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
    (*                            For Modules                             *)
    (* ------------------------------------------------------------------ *)

    Goalw [Execs_def,par_execs_def]

    "Execs (A||B) = par_execs (Execs A) (Execs B)";

    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";