src/HOLCF/IOA/meta_theory/CompoScheds.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 35215 a03462cbf86f
child 39302 d7728f65b353
permissions -rw-r--r--
more antiquotations;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
wenzelm@12218
     2
    Author:     Olaf Müller
wenzelm@17233
     3
*)
mueller@3071
     4
wenzelm@17233
     5
header {* Compositionality on Schedule level *}
mueller@3071
     6
wenzelm@17233
     7
theory CompoScheds
wenzelm@17233
     8
imports CompoExecs
wenzelm@17233
     9
begin
mueller@3071
    10
wenzelm@25135
    11
definition
wenzelm@25135
    12
  mkex2 :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
wenzelm@17233
    13
              ('a,'s)pairs -> ('a,'t)pairs ->
wenzelm@25135
    14
              ('s => 't => ('a,'s*'t)pairs)" where
wenzelm@25135
    15
  "mkex2 A B = (fix$(LAM h sch exA exB. (%s t. case sch of
mueller@3071
    16
       nil => nil
wenzelm@17233
    17
    | x##xs =>
wenzelm@17233
    18
      (case x of
wenzelm@12028
    19
        UU => UU
wenzelm@17233
    20
      | Def y =>
wenzelm@17233
    21
         (if y:act A then
wenzelm@17233
    22
             (if y:act B then
nipkow@10835
    23
                (case HD$exA of
wenzelm@12028
    24
                   UU => UU
nipkow@10835
    25
                 | Def a => (case HD$exB of
wenzelm@12028
    26
                              UU => UU
wenzelm@17233
    27
                            | Def b =>
mueller@3071
    28
                   (y,(snd a,snd b))>>
nipkow@10835
    29
                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
mueller@3071
    30
              else
nipkow@10835
    31
                (case HD$exA of
wenzelm@12028
    32
                   UU => UU
wenzelm@17233
    33
                 | Def a =>
nipkow@10835
    34
                   (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
mueller@3071
    35
              )
wenzelm@17233
    36
          else
wenzelm@17233
    37
             (if y:act B then
nipkow@10835
    38
                (case HD$exB of
wenzelm@12028
    39
                   UU => UU
wenzelm@17233
    40
                 | Def b =>
nipkow@10835
    41
                   (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
mueller@3071
    42
             else
mueller@3071
    43
               UU
mueller@3071
    44
             )
mueller@3071
    45
         )
mueller@3071
    46
       ))))"
mueller@3071
    47
wenzelm@25135
    48
definition
wenzelm@25135
    49
  mkex :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
wenzelm@25135
    50
              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" where
wenzelm@25135
    51
  "mkex A B sch exA exB =
wenzelm@25135
    52
       ((fst exA,fst exB),
wenzelm@25135
    53
        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
wenzelm@25135
    54
wenzelm@25135
    55
definition
wenzelm@25135
    56
  par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" where
wenzelm@25135
    57
  "par_scheds SchedsA SchedsB =
wenzelm@25135
    58
      (let schA = fst SchedsA; sigA = snd SchedsA;
wenzelm@17233
    59
           schB = fst SchedsB; sigB = snd SchedsB
mueller@3521
    60
       in
nipkow@10835
    61
       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
nipkow@10835
    62
        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
mueller@3521
    63
        Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
wenzelm@25135
    64
        asig_comp sigA sigB))"
mueller@3521
    65
wenzelm@19741
    66
wenzelm@19741
    67
subsection "mkex rewrite rules"
wenzelm@19741
    68
wenzelm@19741
    69
wenzelm@19741
    70
lemma mkex2_unfold:
wenzelm@25135
    71
"mkex2 A B = (LAM sch exA exB. (%s t. case sch of
wenzelm@25135
    72
      nil => nil
wenzelm@25135
    73
   | x##xs =>
wenzelm@25135
    74
     (case x of
wenzelm@25135
    75
       UU => UU
wenzelm@25135
    76
     | Def y =>
wenzelm@25135
    77
        (if y:act A then
wenzelm@25135
    78
            (if y:act B then
wenzelm@25135
    79
               (case HD$exA of
wenzelm@25135
    80
                  UU => UU
wenzelm@25135
    81
                | Def a => (case HD$exB of
wenzelm@25135
    82
                             UU => UU
wenzelm@25135
    83
                           | Def b =>
wenzelm@25135
    84
                  (y,(snd a,snd b))>>
wenzelm@25135
    85
                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
wenzelm@25135
    86
             else
wenzelm@25135
    87
               (case HD$exA of
wenzelm@25135
    88
                  UU => UU
wenzelm@25135
    89
                | Def a =>
wenzelm@25135
    90
                  (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)
wenzelm@25135
    91
             )
wenzelm@25135
    92
         else
wenzelm@25135
    93
            (if y:act B then
wenzelm@25135
    94
               (case HD$exB of
wenzelm@25135
    95
                  UU => UU
wenzelm@25135
    96
                | Def b =>
wenzelm@25135
    97
                  (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))
wenzelm@25135
    98
            else
wenzelm@25135
    99
              UU
wenzelm@25135
   100
            )
wenzelm@25135
   101
        )
wenzelm@19741
   102
      )))"
wenzelm@19741
   103
apply (rule trans)
wenzelm@19741
   104
apply (rule fix_eq2)
wenzelm@25135
   105
apply (simp only: mkex2_def)
wenzelm@19741
   106
apply (rule beta_cfun)
wenzelm@19741
   107
apply simp
wenzelm@19741
   108
done
wenzelm@19741
   109
wenzelm@19741
   110
lemma mkex2_UU: "(mkex2 A B$UU$exA$exB) s t = UU"
wenzelm@19741
   111
apply (subst mkex2_unfold)
wenzelm@19741
   112
apply simp
wenzelm@19741
   113
done
wenzelm@19741
   114
wenzelm@19741
   115
lemma mkex2_nil: "(mkex2 A B$nil$exA$exB) s t= nil"
wenzelm@19741
   116
apply (subst mkex2_unfold)
wenzelm@19741
   117
apply simp
wenzelm@19741
   118
done
wenzelm@19741
   119
wenzelm@25135
   120
lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|]
wenzelm@25135
   121
    ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
wenzelm@19741
   122
        (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t"
wenzelm@19741
   123
apply (rule trans)
wenzelm@19741
   124
apply (subst mkex2_unfold)
wenzelm@19741
   125
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   126
apply (simp add: Consq_def)
wenzelm@19741
   127
done
wenzelm@19741
   128
wenzelm@25135
   129
lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|]
wenzelm@25135
   130
    ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
wenzelm@19741
   131
        (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)"
wenzelm@19741
   132
apply (rule trans)
wenzelm@19741
   133
apply (subst mkex2_unfold)
wenzelm@19741
   134
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   135
apply (simp add: Consq_def)
wenzelm@19741
   136
done
wenzelm@19741
   137
wenzelm@25135
   138
lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|]
wenzelm@25135
   139
    ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
wenzelm@25135
   140
         (x,snd a,snd b) >>
wenzelm@19741
   141
            (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"
wenzelm@19741
   142
apply (rule trans)
wenzelm@19741
   143
apply (subst mkex2_unfold)
wenzelm@19741
   144
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   145
apply (simp add: Consq_def)
wenzelm@19741
   146
done
wenzelm@19741
   147
wenzelm@19741
   148
declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp]
wenzelm@19741
   149
  mkex2_cons_2 [simp] mkex2_cons_3 [simp]
wenzelm@19741
   150
wenzelm@19741
   151
wenzelm@19741
   152
subsection {* mkex *}
wenzelm@19741
   153
wenzelm@19741
   154
lemma mkex_UU: "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)"
wenzelm@19741
   155
apply (simp add: mkex_def)
wenzelm@19741
   156
done
wenzelm@19741
   157
wenzelm@19741
   158
lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"
wenzelm@19741
   159
apply (simp add: mkex_def)
wenzelm@19741
   160
done
wenzelm@19741
   161
wenzelm@25135
   162
lemma mkex_cons_1: "[| x:act A; x~:act B |]
wenzelm@25135
   163
    ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =
wenzelm@19741
   164
        ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"
wenzelm@19741
   165
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   166
apply (cut_tac exA = "a>>exA" in mkex2_cons_1)
wenzelm@19741
   167
apply auto
wenzelm@19741
   168
done
wenzelm@19741
   169
wenzelm@25135
   170
lemma mkex_cons_2: "[| x~:act A; x:act B |]
wenzelm@25135
   171
    ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =
wenzelm@19741
   172
        ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"
wenzelm@19741
   173
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   174
apply (cut_tac exB = "b>>exB" in mkex2_cons_2)
wenzelm@19741
   175
apply auto
wenzelm@19741
   176
done
wenzelm@19741
   177
wenzelm@25135
   178
lemma mkex_cons_3: "[| x:act A; x:act B |]
wenzelm@25135
   179
    ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) =
wenzelm@19741
   180
         ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"
wenzelm@19741
   181
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   182
apply (cut_tac exB = "b>>exB" and exA = "a>>exA" in mkex2_cons_3)
wenzelm@19741
   183
apply auto
wenzelm@19741
   184
done
wenzelm@19741
   185
wenzelm@19741
   186
declare mkex2_UU [simp del] mkex2_nil [simp del]
wenzelm@19741
   187
  mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del]
wenzelm@19741
   188
wenzelm@19741
   189
lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3
wenzelm@19741
   190
wenzelm@19741
   191
declare composch_simps [simp]
wenzelm@19741
   192
wenzelm@19741
   193
wenzelm@19741
   194
subsection {* COMPOSITIONALITY on SCHEDULE Level *}
wenzelm@19741
   195
wenzelm@19741
   196
subsubsection "Lemmas for ==>"
wenzelm@19741
   197
wenzelm@19741
   198
(* --------------------------------------------------------------------- *)
wenzelm@19741
   199
(*    Lemma_2_1 :  tfilter(ex) and filter_act are commutative            *)
wenzelm@19741
   200
(* --------------------------------------------------------------------- *)
wenzelm@19741
   201
wenzelm@25135
   202
lemma lemma_2_1a:
wenzelm@25135
   203
   "filter_act$(Filter_ex2 (asig_of A)$xs)=
wenzelm@19741
   204
    Filter (%a. a:act A)$(filter_act$xs)"
wenzelm@19741
   205
wenzelm@19741
   206
apply (unfold filter_act_def Filter_ex2_def)
wenzelm@19741
   207
apply (simp (no_asm) add: MapFilter o_def)
wenzelm@19741
   208
done
wenzelm@19741
   209
wenzelm@19741
   210
wenzelm@19741
   211
(* --------------------------------------------------------------------- *)
wenzelm@19741
   212
(*    Lemma_2_2 : State-projections do not affect filter_act             *)
wenzelm@19741
   213
(* --------------------------------------------------------------------- *)
wenzelm@19741
   214
wenzelm@25135
   215
lemma lemma_2_1b:
wenzelm@25135
   216
   "filter_act$(ProjA2$xs) =filter_act$xs &
wenzelm@19741
   217
    filter_act$(ProjB2$xs) =filter_act$xs"
wenzelm@27208
   218
apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
wenzelm@19741
   219
done
wenzelm@19741
   220
wenzelm@19741
   221
wenzelm@19741
   222
(* --------------------------------------------------------------------- *)
wenzelm@19741
   223
(*             Schedules of A||B have only  A- or B-actions              *)
wenzelm@19741
   224
(* --------------------------------------------------------------------- *)
wenzelm@19741
   225
wenzelm@19741
   226
(* very similar to lemma_1_1c, but it is not checking if every action element of
wenzelm@19741
   227
   an ex is in A or B, but after projecting it onto the action schedule. Of course, this
wenzelm@19741
   228
   is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
wenzelm@19741
   229
wenzelm@25135
   230
lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
wenzelm@19741
   231
   --> Forall (%x. x:act (A||B)) (filter_act$xs)"
wenzelm@19741
   232
wenzelm@27208
   233
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
wenzelm@27208
   234
  @{thm sforall_def}] 1 *})
wenzelm@19741
   235
(* main case *)
haftmann@26359
   236
apply auto
haftmann@26359
   237
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
wenzelm@19741
   238
done
wenzelm@19741
   239
wenzelm@19741
   240
wenzelm@19741
   241
subsubsection "Lemmas for <=="
wenzelm@19741
   242
wenzelm@19741
   243
(*---------------------------------------------------------------------------
wenzelm@19741
   244
    Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
wenzelm@19741
   245
                             structural induction
wenzelm@19741
   246
  --------------------------------------------------------------------------- *)
wenzelm@19741
   247
wenzelm@25135
   248
lemma Mapfst_mkex_is_sch: "! exA exB s t.
wenzelm@25135
   249
  Forall (%x. x:act (A||B)) sch  &
wenzelm@25135
   250
  Filter (%a. a:act A)$sch << filter_act$exA &
wenzelm@25135
   251
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@19741
   252
  --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
wenzelm@19741
   253
wenzelm@27208
   254
apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
wenzelm@27208
   255
  @{thm sforall_def}, @{thm mkex_def}] 1 *})
wenzelm@19741
   256
wenzelm@19741
   257
(* main case *)
wenzelm@19741
   258
(* splitting into 4 cases according to a:A, a:B *)
haftmann@26359
   259
apply auto
wenzelm@19741
   260
wenzelm@19741
   261
(* Case y:A, y:B *)
wenzelm@27208
   262
apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
wenzelm@19741
   263
(* Case exA=UU, Case exA=nil*)
wenzelm@19741
   264
(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
wenzelm@19741
   265
   is used! --> to generate a contradiction using  ~a>>ss<< UU(nil), using theorems
wenzelm@19741
   266
   Cons_not_less_UU and Cons_not_less_nil  *)
wenzelm@27208
   267
apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
wenzelm@19741
   268
(* Case exA=a>>x, exB=b>>y *)
wenzelm@19741
   269
(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
wenzelm@19741
   270
   as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic
wenzelm@19741
   271
   would not be generally applicable *)
wenzelm@19741
   272
apply simp
wenzelm@19741
   273
wenzelm@19741
   274
(* Case y:A, y~:B *)
wenzelm@27208
   275
apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
wenzelm@19741
   276
apply simp
wenzelm@19741
   277
wenzelm@19741
   278
(* Case y~:A, y:B *)
wenzelm@27208
   279
apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
wenzelm@19741
   280
apply simp
wenzelm@19741
   281
wenzelm@19741
   282
(* Case y~:A, y~:B *)
wenzelm@19741
   283
apply (simp add: asig_of_par actions_asig_comp)
wenzelm@19741
   284
done
wenzelm@19741
   285
wenzelm@19741
   286
wenzelm@19741
   287
(* generalizing the proof above to a tactic *)
wenzelm@19741
   288
wenzelm@19741
   289
ML {*
wenzelm@19741
   290
wenzelm@19741
   291
local
wenzelm@39159
   292
  val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
wenzelm@39159
   293
    @{thm stutter_def}]
wenzelm@39159
   294
  val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
wenzelm@19741
   295
in
wenzelm@19741
   296
wenzelm@27208
   297
fun mkex_induct_tac ctxt sch exA exB =
wenzelm@32149
   298
  let val ss = simpset_of ctxt in
wenzelm@27208
   299
    EVERY1[Seq_induct_tac ctxt sch defs,
wenzelm@27208
   300
           asm_full_simp_tac ss,
wenzelm@32149
   301
           SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
wenzelm@27208
   302
           Seq_case_simp_tac ctxt exA,
wenzelm@27208
   303
           Seq_case_simp_tac ctxt exB,
wenzelm@27208
   304
           asm_full_simp_tac ss,
wenzelm@27208
   305
           Seq_case_simp_tac ctxt exA,
wenzelm@27208
   306
           asm_full_simp_tac ss,
wenzelm@27208
   307
           Seq_case_simp_tac ctxt exB,
wenzelm@27208
   308
           asm_full_simp_tac ss,
wenzelm@27208
   309
           asm_full_simp_tac (ss addsimps asigs)
wenzelm@19741
   310
          ]
wenzelm@27208
   311
  end
wenzelm@17233
   312
mueller@3521
   313
end
wenzelm@19741
   314
*}
wenzelm@19741
   315
wenzelm@19741
   316
wenzelm@19741
   317
(*---------------------------------------------------------------------------
wenzelm@19741
   318
               Projection of mkex(sch,exA,exB) onto A stutters on A
wenzelm@19741
   319
                             structural induction
wenzelm@19741
   320
  --------------------------------------------------------------------------- *)
wenzelm@19741
   321
wenzelm@25135
   322
lemma stutterA_mkex: "! exA exB s t.
wenzelm@25135
   323
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   324
  Filter (%a. a:act A)$sch << filter_act$exA &
wenzelm@25135
   325
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@19741
   326
  --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
wenzelm@19741
   327
wenzelm@27208
   328
apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
wenzelm@19741
   329
done
wenzelm@19741
   330
wenzelm@19741
   331
wenzelm@25135
   332
lemma stutter_mkex_on_A: "[|
wenzelm@25135
   333
  Forall (%x. x:act (A||B)) sch ;
wenzelm@25135
   334
  Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
wenzelm@25135
   335
  Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
wenzelm@19741
   336
  ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
wenzelm@19741
   337
wenzelm@19741
   338
apply (cut_tac stutterA_mkex)
wenzelm@19741
   339
apply (simp add: stutter_def ProjA_def mkex_def)
wenzelm@19741
   340
apply (erule allE)+
wenzelm@19741
   341
apply (drule mp)
wenzelm@19741
   342
prefer 2 apply (assumption)
wenzelm@19741
   343
apply simp
wenzelm@19741
   344
done
wenzelm@19741
   345
wenzelm@19741
   346
wenzelm@19741
   347
(*---------------------------------------------------------------------------
wenzelm@19741
   348
               Projection of mkex(sch,exA,exB) onto B stutters on B
wenzelm@19741
   349
                             structural induction
wenzelm@19741
   350
  --------------------------------------------------------------------------- *)
wenzelm@19741
   351
wenzelm@25135
   352
lemma stutterB_mkex: "! exA exB s t.
wenzelm@25135
   353
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   354
  Filter (%a. a:act A)$sch << filter_act$exA &
wenzelm@25135
   355
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@19741
   356
  --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
wenzelm@27208
   357
apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
wenzelm@19741
   358
done
wenzelm@19741
   359
wenzelm@19741
   360
wenzelm@25135
   361
lemma stutter_mkex_on_B: "[|
wenzelm@25135
   362
  Forall (%x. x:act (A||B)) sch ;
wenzelm@25135
   363
  Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
wenzelm@25135
   364
  Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
wenzelm@19741
   365
  ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
wenzelm@19741
   366
apply (cut_tac stutterB_mkex)
wenzelm@19741
   367
apply (simp add: stutter_def ProjB_def mkex_def)
wenzelm@19741
   368
apply (erule allE)+
wenzelm@19741
   369
apply (drule mp)
wenzelm@19741
   370
prefer 2 apply (assumption)
wenzelm@19741
   371
apply simp
wenzelm@19741
   372
done
wenzelm@19741
   373
wenzelm@19741
   374
wenzelm@19741
   375
(*---------------------------------------------------------------------------
wenzelm@19741
   376
     Filter of mkex(sch,exA,exB) to A after projection onto A is exA
wenzelm@19741
   377
        --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
wenzelm@19741
   378
        --           because of admissibility problems          --
wenzelm@19741
   379
                             structural induction
wenzelm@19741
   380
  --------------------------------------------------------------------------- *)
wenzelm@19741
   381
wenzelm@25135
   382
lemma filter_mkex_is_exA_tmp: "! exA exB s t.
wenzelm@25135
   383
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   384
  Filter (%a. a:act A)$sch << filter_act$exA  &
wenzelm@25135
   385
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@25135
   386
  --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
wenzelm@19741
   387
      Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
wenzelm@27208
   388
apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
wenzelm@19741
   389
done
wenzelm@19741
   390
wenzelm@19741
   391
(*---------------------------------------------------------------------------
wenzelm@19741
   392
                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
wenzelm@19741
   393
                    lemma for admissibility problems
wenzelm@19741
   394
  --------------------------------------------------------------------------- *)
wenzelm@19741
   395
wenzelm@19741
   396
lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
wenzelm@27208
   397
apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
wenzelm@19741
   398
done
wenzelm@19741
   399
wenzelm@19741
   400
wenzelm@19741
   401
(*---------------------------------------------------------------------------
wenzelm@19741
   402
      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex
wenzelm@19741
   403
         lemma for eliminating non admissible equations in assumptions
wenzelm@19741
   404
  --------------------------------------------------------------------------- *)
wenzelm@19741
   405
wenzelm@25135
   406
lemma trick_against_eq_in_ass: "!! sch ex.
wenzelm@25135
   407
  Filter (%a. a:act AB)$sch = filter_act$ex
wenzelm@19741
   408
  ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
wenzelm@19741
   409
apply (simp add: filter_act_def)
wenzelm@19741
   410
apply (rule Zip_Map_fst_snd [symmetric])
wenzelm@19741
   411
done
wenzelm@19741
   412
wenzelm@19741
   413
(*---------------------------------------------------------------------------
wenzelm@19741
   414
     Filter of mkex(sch,exA,exB) to A after projection onto A is exA
wenzelm@19741
   415
                       using the above trick
wenzelm@19741
   416
  --------------------------------------------------------------------------- *)
wenzelm@19741
   417
wenzelm@19741
   418
wenzelm@25135
   419
lemma filter_mkex_is_exA: "!!sch exA exB.
wenzelm@25135
   420
  [| Forall (%a. a:act (A||B)) sch ;
wenzelm@25135
   421
  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
wenzelm@25135
   422
  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
wenzelm@19741
   423
  ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
wenzelm@19741
   424
apply (simp add: ProjA_def Filter_ex_def)
wenzelm@27208
   425
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   426
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   427
apply (rule conjI)
wenzelm@19741
   428
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   429
apply (simplesubst trick_against_eq_in_ass)
wenzelm@19741
   430
back
wenzelm@19741
   431
apply assumption
wenzelm@19741
   432
apply (simp add: filter_mkex_is_exA_tmp)
wenzelm@19741
   433
done
wenzelm@19741
   434
wenzelm@19741
   435
wenzelm@19741
   436
(*---------------------------------------------------------------------------
wenzelm@19741
   437
     Filter of mkex(sch,exA,exB) to B after projection onto B is exB
wenzelm@19741
   438
        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
wenzelm@19741
   439
        --           because of admissibility problems          --
wenzelm@19741
   440
                             structural induction
wenzelm@19741
   441
  --------------------------------------------------------------------------- *)
wenzelm@19741
   442
wenzelm@25135
   443
lemma filter_mkex_is_exB_tmp: "! exA exB s t.
wenzelm@25135
   444
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   445
  Filter (%a. a:act A)$sch << filter_act$exA  &
wenzelm@25135
   446
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@25135
   447
  --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
wenzelm@19741
   448
      Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
wenzelm@19741
   449
wenzelm@19741
   450
(* notice necessary change of arguments exA and exB *)
wenzelm@27208
   451
apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
wenzelm@19741
   452
done
wenzelm@19741
   453
wenzelm@19741
   454
wenzelm@19741
   455
(*---------------------------------------------------------------------------
wenzelm@19741
   456
     Filter of mkex(sch,exA,exB) to A after projection onto B is exB
wenzelm@19741
   457
                       using the above trick
wenzelm@19741
   458
  --------------------------------------------------------------------------- *)
wenzelm@19741
   459
wenzelm@19741
   460
wenzelm@25135
   461
lemma filter_mkex_is_exB: "!!sch exA exB.
wenzelm@25135
   462
  [| Forall (%a. a:act (A||B)) sch ;
wenzelm@25135
   463
  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
wenzelm@25135
   464
  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
wenzelm@19741
   465
  ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
wenzelm@19741
   466
apply (simp add: ProjB_def Filter_ex_def)
wenzelm@27208
   467
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   468
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   469
apply (rule conjI)
wenzelm@19741
   470
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   471
apply (simplesubst trick_against_eq_in_ass)
wenzelm@19741
   472
back
wenzelm@19741
   473
apply assumption
wenzelm@19741
   474
apply (simp add: filter_mkex_is_exB_tmp)
wenzelm@19741
   475
done
wenzelm@19741
   476
wenzelm@19741
   477
(* --------------------------------------------------------------------- *)
wenzelm@19741
   478
(*                    mkex has only  A- or B-actions                    *)
wenzelm@19741
   479
(* --------------------------------------------------------------------- *)
wenzelm@19741
   480
wenzelm@19741
   481
wenzelm@25135
   482
lemma mkex_actions_in_AorB: "!s t exA exB.
wenzelm@25135
   483
  Forall (%x. x : act (A || B)) sch &
wenzelm@25135
   484
  Filter (%a. a:act A)$sch << filter_act$exA  &
wenzelm@25135
   485
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@25135
   486
   --> Forall (%x. fst x : act (A ||B))
wenzelm@19741
   487
         (snd (mkex A B sch (s,exA) (t,exB)))"
wenzelm@27208
   488
apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
wenzelm@19741
   489
done
wenzelm@19741
   490
wenzelm@19741
   491
wenzelm@19741
   492
(* ------------------------------------------------------------------ *)
wenzelm@19741
   493
(*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
wenzelm@19741
   494
(*                          Main Theorem                              *)
wenzelm@19741
   495
(* ------------------------------------------------------------------ *)
wenzelm@19741
   496
wenzelm@25135
   497
lemma compositionality_sch:
wenzelm@25135
   498
"(sch : schedules (A||B)) =
wenzelm@25135
   499
  (Filter (%a. a:act A)$sch : schedules A &
wenzelm@25135
   500
   Filter (%a. a:act B)$sch : schedules B &
wenzelm@19741
   501
   Forall (%x. x:act (A||B)) sch)"
wenzelm@19741
   502
apply (simp (no_asm) add: schedules_def has_schedule_def)
haftmann@26359
   503
apply auto
wenzelm@19741
   504
(* ==> *)
wenzelm@19741
   505
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
wenzelm@19741
   506
prefer 2
wenzelm@19741
   507
apply (simp add: compositionality_ex)
wenzelm@19741
   508
apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
wenzelm@19741
   509
apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
wenzelm@19741
   510
prefer 2
wenzelm@19741
   511
apply (simp add: compositionality_ex)
wenzelm@19741
   512
apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
wenzelm@19741
   513
apply (simp add: executions_def)
wenzelm@27208
   514
apply (tactic {* pair_tac @{context} "ex" 1 *})
wenzelm@19741
   515
apply (erule conjE)
wenzelm@19741
   516
apply (simp add: sch_actions_in_AorB)
wenzelm@19741
   517
wenzelm@19741
   518
(* <== *)
wenzelm@19741
   519
wenzelm@19741
   520
(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
wenzelm@19741
   521
   we need here *)
wenzelm@19741
   522
apply (rename_tac exA exB)
wenzelm@19741
   523
apply (rule_tac x = "mkex A B sch exA exB" in bexI)
wenzelm@19741
   524
(* mkex actions are just the oracle *)
wenzelm@27208
   525
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   526
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   527
apply (simp add: Mapfst_mkex_is_sch)
wenzelm@19741
   528
wenzelm@19741
   529
(* mkex is an execution -- use compositionality on ex-level *)
wenzelm@19741
   530
apply (simp add: compositionality_ex)
wenzelm@19741
   531
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
wenzelm@27208
   532
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   533
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   534
apply (simp add: mkex_actions_in_AorB)
wenzelm@19741
   535
done
wenzelm@19741
   536
wenzelm@19741
   537
wenzelm@19741
   538
subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
wenzelm@19741
   539
wenzelm@25135
   540
lemma compositionality_sch_modules:
wenzelm@19741
   541
  "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
wenzelm@19741
   542
wenzelm@19741
   543
apply (unfold Scheds_def par_scheds_def)
wenzelm@19741
   544
apply (simp add: asig_of_par)
wenzelm@19741
   545
apply (rule set_ext)
wenzelm@19741
   546
apply (simp add: compositionality_sch actions_of_par)
wenzelm@19741
   547
done
wenzelm@19741
   548
wenzelm@19741
   549
wenzelm@19741
   550
declare compoex_simps [simp del]
wenzelm@19741
   551
declare composch_simps [simp del]
wenzelm@19741
   552
wenzelm@19741
   553
end