src/HOLCF/IOA/meta_theory/CompoExecs.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 7229 6773ba0c36d5
child 11655 923e4d0d36d5
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5 
     6 Compositionality on Execution level.
     7 *)  
     8 
     9 Delsimps (ex_simps @ all_simps); 
    10 Delsimps [split_paired_All];
    11 
    12 (* ----------------------------------------------------------------------------------- *)
    13 
    14 
    15 section "recursive equations of operators";
    16 
    17 
    18 (* ---------------------------------------------------------------- *)
    19 (*                               ProjA2                             *)
    20 (* ---------------------------------------------------------------- *)
    21 
    22 
    23 Goal  "ProjA2$UU = UU";
    24 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    25 qed"ProjA2_UU";
    26 
    27 Goal  "ProjA2$nil = nil";
    28 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    29 qed"ProjA2_nil";
    30 
    31 Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs";
    32 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    33 qed"ProjA2_cons";
    34 
    35 
    36 (* ---------------------------------------------------------------- *)
    37 (*                               ProjB2                             *)
    38 (* ---------------------------------------------------------------- *)
    39 
    40 
    41 Goal  "ProjB2$UU = UU";
    42 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    43 qed"ProjB2_UU";
    44 
    45 Goal  "ProjB2$nil = nil";
    46 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    47 qed"ProjB2_nil";
    48 
    49 Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs";
    50 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    51 qed"ProjB2_cons";
    52 
    53 
    54 
    55 (* ---------------------------------------------------------------- *)
    56 (*                             Filter_ex2                           *)
    57 (* ---------------------------------------------------------------- *)
    58 
    59 
    60 Goal "Filter_ex2 sig$UU=UU";
    61 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    62 qed"Filter_ex2_UU";
    63 
    64 Goal "Filter_ex2 sig$nil=nil";
    65 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    66 qed"Filter_ex2_nil";
    67 
    68 Goal "Filter_ex2 sig$(at >> xs) =    \
    69 \            (if (fst at:actions sig)    \       
    70 \                 then at >> (Filter_ex2 sig$xs) \   
    71 \                 else        Filter_ex2 sig$xs)";
    72 
    73 by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    74 qed"Filter_ex2_cons";
    75 
    76 
    77 (* ---------------------------------------------------------------- *)
    78 (*                             stutter2                             *)
    79 (* ---------------------------------------------------------------- *)
    80 
    81 
    82 Goal "stutter2 sig = (LAM ex. (%s. case ex of \
    83 \      nil => TT \
    84 \    | x##xs => (flift1 \ 
    85 \            (%p.(If Def ((fst p)~:actions sig) \
    86 \                 then Def (s=(snd p)) \
    87 \                 else TT fi) \
    88 \                andalso (stutter2 sig$xs) (snd p))  \
    89 \             $x) \
    90 \           ))";
    91 by (rtac trans 1);
    92 by (rtac fix_eq2 1);
    93 by (rtac stutter2_def 1);
    94 by (rtac beta_cfun 1);
    95 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    96 qed"stutter2_unfold";
    97 
    98 Goal "(stutter2 sig$UU) s=UU";
    99 by (stac stutter2_unfold 1);
   100 by (Simp_tac 1);
   101 qed"stutter2_UU";
   102 
   103 Goal "(stutter2 sig$nil) s = TT";
   104 by (stac stutter2_unfold 1);
   105 by (Simp_tac 1);
   106 qed"stutter2_nil";
   107 
   108 Goal "(stutter2 sig$(at>>xs)) s = \
   109 \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
   110 \                andalso (stutter2 sig$xs) (snd at))"; 
   111 by (rtac trans 1);
   112 by (stac stutter2_unfold 1);
   113 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
   114 by (Simp_tac 1);
   115 qed"stutter2_cons";
   116 
   117 
   118 Addsimps [stutter2_UU,stutter2_nil,stutter2_cons];
   119 
   120 
   121 (* ---------------------------------------------------------------- *)
   122 (*                             stutter                              *)
   123 (* ---------------------------------------------------------------- *)
   124 
   125 Goal "stutter sig (s, UU)";
   126 by (simp_tac (simpset() addsimps [stutter_def]) 1);
   127 qed"stutter_UU";
   128 
   129 Goal "stutter sig (s, nil)";
   130 by (simp_tac (simpset() addsimps [stutter_def]) 1);
   131 qed"stutter_nil";
   132 
   133 Goal "stutter sig (s, (a,t)>>ex) = \
   134 \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
   135 by (simp_tac (simpset() addsimps [stutter_def]) 1);
   136 qed"stutter_cons";
   137 
   138 (* ----------------------------------------------------------------------------------- *)
   139 
   140 Delsimps [stutter2_UU,stutter2_nil,stutter2_cons];
   141 
   142 val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons,
   143                      ProjB2_UU,ProjB2_nil,ProjB2_cons,
   144                      Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons,
   145                      stutter_UU,stutter_nil,stutter_cons];
   146 
   147 Addsimps compoex_simps;
   148 
   149 
   150 
   151 (* ------------------------------------------------------------------ *)
   152 (*                      The following lemmata aim for                 *)
   153 (*             COMPOSITIONALITY   on    EXECUTION     Level           *)
   154 (* ------------------------------------------------------------------ *)
   155 
   156 
   157 (* --------------------------------------------------------------------- *)
   158 (*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
   159 (* --------------------------------------------------------------------- *)
   160 
   161 Goal "!s. is_exec_frag (A||B) (s,xs) \
   162 \      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
   163 \           is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))";
   164 
   165 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
   166 (* main case *)
   167 ren "ss a t" 1;
   168 by (safe_tac set_cs);
   169 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
   170 qed"lemma_1_1a";
   171 
   172 
   173 (* --------------------------------------------------------------------- *)
   174 (*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
   175 (* --------------------------------------------------------------------- *)
   176 
   177 Goal "!s. is_exec_frag (A||B) (s,xs) \
   178 \      --> stutter (asig_of A) (fst s,ProjA2$xs)  &\
   179 \          stutter (asig_of B) (snd s,ProjB2$xs)"; 
   180 
   181 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
   182 (* main case *)
   183 by (safe_tac set_cs);
   184 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
   185 qed"lemma_1_1b";
   186 
   187 
   188 (* --------------------------------------------------------------------- *)
   189 (*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
   190 (* --------------------------------------------------------------------- *)
   191 
   192 Goal "!s. (is_exec_frag (A||B) (s,xs) \
   193 \  --> Forall (%x. fst x:act (A||B)) xs)";
   194 
   195 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
   196 (* main case *)
   197 by (safe_tac set_cs);
   198 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
   199                                 [actions_asig_comp,asig_of_par]) 1));
   200 qed"lemma_1_1c";
   201 
   202 
   203 (* ----------------------------------------------------------------------- *)
   204 (*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
   205 (* ----------------------------------------------------------------------- *)
   206 
   207 Goal 
   208 "!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
   209 \    is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\
   210 \    stutter (asig_of A) (fst s,(ProjA2$xs)) & \
   211 \    stutter (asig_of B) (snd s,(ProjB2$xs)) & \
   212 \    Forall (%x. fst x:act (A||B)) xs \
   213 \    --> is_exec_frag (A||B) (s,xs)";
   214 
   215 by (pair_induct_tac "xs" [Forall_def,sforall_def,
   216          is_exec_frag_def, stutter_def] 1);
   217 by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 1);
   218 by (safe_tac set_cs);
   219 (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
   220 by (rotate_tac ~4 1);
   221 by (Asm_full_simp_tac 1);
   222 by (rotate_tac ~4 1);
   223 by (Asm_full_simp_tac 1);
   224 qed"lemma_1_2";
   225 
   226 
   227 (* ------------------------------------------------------------------ *)
   228 (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
   229 (*                          Main Theorem                              *)
   230 (* ------------------------------------------------------------------ *)
   231 
   232 
   233 Goal 
   234 "ex:executions(A||B) =\
   235 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\
   236 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\
   237 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
   238 \ Forall (%x. fst x:act (A||B)) (snd ex))";
   239 
   240 by (simp_tac (simpset() addsimps [executions_def,ProjB_def,
   241                                  Filter_ex_def,ProjA_def,starts_of_par]) 1);
   242 by (pair_tac "ex" 1);
   243 by (rtac iffI 1);
   244 (* ==>  *)
   245 by (REPEAT (etac conjE 1));
   246 by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp,
   247                lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
   248 (* <==  *)
   249 by (REPEAT (etac conjE 1));
   250 by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1);
   251 qed"compositionality_ex";
   252 
   253 
   254 (* ------------------------------------------------------------------ *)
   255 (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
   256 (*                            For Modules                             *)
   257 (* ------------------------------------------------------------------ *)
   258 
   259 Goalw [Execs_def,par_execs_def]
   260 
   261 "Execs (A||B) = par_execs (Execs A) (Execs B)";
   262 
   263 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
   264 by (rtac set_ext 1);
   265 by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
   266 qed"compositionality_ex_modules";
   267 
   268 
   269 
   270 
   271 
   272 
   273