src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61999 89291b5d0ede
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 section {* Compositionality on Execution level *}
     6 
     7 theory CompoExecs
     8 imports Traces
     9 begin
    10 
    11 definition
    12   ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where
    13   "ProjA2 = Map (%x.(fst x,fst(snd x)))"
    14 
    15 definition
    16   ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where
    17   "ProjA ex = (fst (fst ex), ProjA2$(snd ex))"
    18 
    19 definition
    20   ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where
    21   "ProjB2 = Map (%x.(fst x,snd(snd x)))"
    22 
    23 definition
    24   ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where
    25   "ProjB ex = (snd (fst ex), ProjB2$(snd ex))"
    26 
    27 definition
    28   Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where
    29   "Filter_ex2 sig = Filter (%x. fst x:actions sig)"
    30 
    31 definition
    32   Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where
    33   "Filter_ex sig ex = (fst ex,Filter_ex2 sig$(snd ex))"
    34 
    35 definition
    36   stutter2 :: "'a signature => ('a,'s)pairs -> ('s => tr)" where
    37   "stutter2 sig = (fix$(LAM h ex. (%s. case ex of
    38       nil => TT
    39     | x##xs => (flift1
    40             (%p.(If Def ((fst p)~:actions sig)
    41                  then Def (s=(snd p))
    42                  else TT)
    43                 andalso (h$xs) (snd p))
    44              $x)
    45    )))"
    46 
    47 definition
    48   stutter :: "'a signature => ('a,'s)execution => bool" where
    49   "stutter sig ex = ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
    50 
    51 definition
    52   par_execs :: "[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" where
    53   "par_execs ExecsA ExecsB =
    54       (let exA = fst ExecsA; sigA = snd ExecsA;
    55            exB = fst ExecsB; sigB = snd ExecsB
    56        in
    57        (    {ex. Filter_ex sigA (ProjA ex) : exA}
    58         Int {ex. Filter_ex sigB (ProjB ex) : exB}
    59         Int {ex. stutter sigA (ProjA ex)}
    60         Int {ex. stutter sigB (ProjB ex)}
    61         Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
    62         asig_comp sigA sigB))"
    63 
    64 
    65 lemmas [simp del] = split_paired_All
    66 
    67 
    68 section "recursive equations of operators"
    69 
    70 
    71 (* ---------------------------------------------------------------- *)
    72 (*                               ProjA2                             *)
    73 (* ---------------------------------------------------------------- *)
    74 
    75 
    76 lemma ProjA2_UU: "ProjA2$UU = UU"
    77 apply (simp add: ProjA2_def)
    78 done
    79 
    80 lemma ProjA2_nil: "ProjA2$nil = nil"
    81 apply (simp add: ProjA2_def)
    82 done
    83 
    84 lemma ProjA2_cons: "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs"
    85 apply (simp add: ProjA2_def)
    86 done
    87 
    88 
    89 (* ---------------------------------------------------------------- *)
    90 (*                               ProjB2                             *)
    91 (* ---------------------------------------------------------------- *)
    92 
    93 
    94 lemma ProjB2_UU: "ProjB2$UU = UU"
    95 apply (simp add: ProjB2_def)
    96 done
    97 
    98 lemma ProjB2_nil: "ProjB2$nil = nil"
    99 apply (simp add: ProjB2_def)
   100 done
   101 
   102 lemma ProjB2_cons: "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs"
   103 apply (simp add: ProjB2_def)
   104 done
   105 
   106 
   107 
   108 (* ---------------------------------------------------------------- *)
   109 (*                             Filter_ex2                           *)
   110 (* ---------------------------------------------------------------- *)
   111 
   112 
   113 lemma Filter_ex2_UU: "Filter_ex2 sig$UU=UU"
   114 apply (simp add: Filter_ex2_def)
   115 done
   116 
   117 lemma Filter_ex2_nil: "Filter_ex2 sig$nil=nil"
   118 apply (simp add: Filter_ex2_def)
   119 done
   120 
   121 lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) =
   122              (if (fst at:actions sig)
   123                   then at >> (Filter_ex2 sig$xs)
   124                   else        Filter_ex2 sig$xs)"
   125 
   126 apply (simp add: Filter_ex2_def)
   127 done
   128 
   129 
   130 (* ---------------------------------------------------------------- *)
   131 (*                             stutter2                             *)
   132 (* ---------------------------------------------------------------- *)
   133 
   134 
   135 lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of
   136        nil => TT
   137      | x##xs => (flift1
   138              (%p.(If Def ((fst p)~:actions sig)
   139                   then Def (s=(snd p))
   140                   else TT)
   141                  andalso (stutter2 sig$xs) (snd p))
   142               $x)
   143             ))"
   144 apply (rule trans)
   145 apply (rule fix_eq2)
   146 apply (simp only: stutter2_def)
   147 apply (rule beta_cfun)
   148 apply (simp add: flift1_def)
   149 done
   150 
   151 lemma stutter2_UU: "(stutter2 sig$UU) s=UU"
   152 apply (subst stutter2_unfold)
   153 apply simp
   154 done
   155 
   156 lemma stutter2_nil: "(stutter2 sig$nil) s = TT"
   157 apply (subst stutter2_unfold)
   158 apply simp
   159 done
   160 
   161 lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s =
   162                ((if (fst at)~:actions sig then Def (s=snd at) else TT)
   163                  andalso (stutter2 sig$xs) (snd at))"
   164 apply (rule trans)
   165 apply (subst stutter2_unfold)
   166 apply (simp add: Consq_def flift1_def If_and_if)
   167 apply simp
   168 done
   169 
   170 
   171 declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp]
   172 
   173 
   174 (* ---------------------------------------------------------------- *)
   175 (*                             stutter                              *)
   176 (* ---------------------------------------------------------------- *)
   177 
   178 lemma stutter_UU: "stutter sig (s, UU)"
   179 apply (simp add: stutter_def)
   180 done
   181 
   182 lemma stutter_nil: "stutter sig (s, nil)"
   183 apply (simp add: stutter_def)
   184 done
   185 
   186 lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
   187       ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
   188 apply (simp add: stutter_def)
   189 done
   190 
   191 (* ----------------------------------------------------------------------------------- *)
   192 
   193 declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del]
   194 
   195 lemmas compoex_simps = ProjA2_UU ProjA2_nil ProjA2_cons
   196   ProjB2_UU ProjB2_nil ProjB2_cons
   197   Filter_ex2_UU Filter_ex2_nil Filter_ex2_cons
   198   stutter_UU stutter_nil stutter_cons
   199 
   200 declare compoex_simps [simp]
   201 
   202 
   203 
   204 (* ------------------------------------------------------------------ *)
   205 (*                      The following lemmata aim for                 *)
   206 (*             COMPOSITIONALITY   on    EXECUTION     Level           *)
   207 (* ------------------------------------------------------------------ *)
   208 
   209 
   210 (* --------------------------------------------------------------------- *)
   211 (*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
   212 (* --------------------------------------------------------------------- *)
   213 
   214 lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
   215        -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
   216             is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
   217 
   218 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
   219 (* main case *)
   220 apply (auto simp add: trans_of_defs2)
   221 done
   222 
   223 
   224 (* --------------------------------------------------------------------- *)
   225 (*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
   226 (* --------------------------------------------------------------------- *)
   227 
   228 lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
   229        --> stutter (asig_of A) (fst s,ProjA2$xs)  &
   230            stutter (asig_of B) (snd s,ProjB2$xs)"
   231 
   232 apply (tactic {* pair_induct_tac @{context} "xs"
   233   [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
   234 (* main case *)
   235 apply (auto simp add: trans_of_defs2)
   236 done
   237 
   238 
   239 (* --------------------------------------------------------------------- *)
   240 (*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
   241 (* --------------------------------------------------------------------- *)
   242 
   243 lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
   244    --> Forall (%x. fst x:act (A||B)) xs)"
   245 
   246 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   247   @{thm is_exec_frag_def}] 1 *})
   248 (* main case *)
   249 apply auto
   250 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
   251 done
   252 
   253 
   254 (* ----------------------------------------------------------------------- *)
   255 (*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
   256 (* ----------------------------------------------------------------------- *)
   257 
   258 lemma lemma_1_2:
   259 "!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &
   260      is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
   261      stutter (asig_of A) (fst s,(ProjA2$xs)) &
   262      stutter (asig_of B) (snd s,(ProjB2$xs)) &
   263      Forall (%x. fst x:act (A||B)) xs
   264      --> is_exec_frag (A||B) (s,xs)"
   265 
   266 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   267   @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
   268 apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
   269 done
   270 
   271 
   272 subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
   273 
   274 lemma compositionality_ex:
   275 "(ex:executions(A||B)) =
   276  (Filter_ex (asig_of A) (ProjA ex) : executions A &
   277   Filter_ex (asig_of B) (ProjB ex) : executions B &
   278   stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
   279   Forall (%x. fst x:act (A||B)) (snd ex))"
   280 
   281 apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
   282 apply (tactic {* pair_tac @{context} "ex" 1 *})
   283 apply (rule iffI)
   284 (* ==>  *)
   285 apply (erule conjE)+
   286 apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c)
   287 (* <==  *)
   288 apply (erule conjE)+
   289 apply (simp add: lemma_1_2)
   290 done
   291 
   292 
   293 subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
   294 
   295 lemma compositionality_ex_modules:
   296   "Execs (A||B) = par_execs (Execs A) (Execs B)"
   297 apply (unfold Execs_def par_execs_def)
   298 apply (simp add: asig_of_par)
   299 apply (rule set_eqI)
   300 apply (simp add: compositionality_ex actions_of_par)
   301 done
   302 
   303 end