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