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