src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 61999 89291b5d0ede
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
wenzelm@40945
     2
    Author:     Olaf Müller
wenzelm@17233
     3
*)
mueller@3071
     4
wenzelm@58880
     5
section {* 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@46469
   287
(* generalizing the proof above to a proof method *)
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@51717
   298
  EVERY'[Seq_induct_tac ctxt sch defs,
wenzelm@51717
   299
         asm_full_simp_tac ctxt,
wenzelm@58957
   300
         SELECT_GOAL
wenzelm@58957
   301
          (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
wenzelm@51717
   302
         Seq_case_simp_tac ctxt exA,
wenzelm@51717
   303
         Seq_case_simp_tac ctxt exB,
wenzelm@51717
   304
         asm_full_simp_tac ctxt,
wenzelm@51717
   305
         Seq_case_simp_tac ctxt exA,
wenzelm@51717
   306
         asm_full_simp_tac ctxt,
wenzelm@51717
   307
         Seq_case_simp_tac ctxt exB,
wenzelm@51717
   308
         asm_full_simp_tac ctxt,
wenzelm@51717
   309
         asm_full_simp_tac (ctxt addsimps asigs)
wenzelm@51717
   310
        ]
wenzelm@17233
   311
mueller@3521
   312
end
wenzelm@19741
   313
*}
wenzelm@19741
   314
wenzelm@46469
   315
method_setup mkex_induct = {*
wenzelm@46469
   316
  Scan.lift (Args.name -- Args.name -- Args.name)
wenzelm@46469
   317
    >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
wenzelm@46469
   318
*}
wenzelm@46469
   319
wenzelm@19741
   320
wenzelm@19741
   321
(*---------------------------------------------------------------------------
wenzelm@19741
   322
               Projection of mkex(sch,exA,exB) onto A stutters on A
wenzelm@19741
   323
                             structural induction
wenzelm@19741
   324
  --------------------------------------------------------------------------- *)
wenzelm@19741
   325
wenzelm@25135
   326
lemma stutterA_mkex: "! exA exB s t.
wenzelm@25135
   327
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   328
  Filter (%a. a:act A)$sch << filter_act$exA &
wenzelm@25135
   329
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@19741
   330
  --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
wenzelm@46469
   331
  by (mkex_induct sch exA exB)
wenzelm@19741
   332
wenzelm@25135
   333
lemma stutter_mkex_on_A: "[|
wenzelm@25135
   334
  Forall (%x. x:act (A||B)) sch ;
wenzelm@25135
   335
  Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
wenzelm@25135
   336
  Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
wenzelm@19741
   337
  ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
wenzelm@19741
   338
wenzelm@19741
   339
apply (cut_tac stutterA_mkex)
wenzelm@19741
   340
apply (simp add: stutter_def ProjA_def mkex_def)
wenzelm@19741
   341
apply (erule allE)+
wenzelm@19741
   342
apply (drule mp)
wenzelm@19741
   343
prefer 2 apply (assumption)
wenzelm@19741
   344
apply simp
wenzelm@19741
   345
done
wenzelm@19741
   346
wenzelm@19741
   347
wenzelm@19741
   348
(*---------------------------------------------------------------------------
wenzelm@19741
   349
               Projection of mkex(sch,exA,exB) onto B stutters on B
wenzelm@19741
   350
                             structural induction
wenzelm@19741
   351
  --------------------------------------------------------------------------- *)
wenzelm@19741
   352
wenzelm@25135
   353
lemma stutterB_mkex: "! exA exB s t.
wenzelm@25135
   354
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   355
  Filter (%a. a:act A)$sch << filter_act$exA &
wenzelm@25135
   356
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@19741
   357
  --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
wenzelm@46469
   358
  by (mkex_induct sch exA exB)
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@46469
   388
  by (mkex_induct sch exB exA)
wenzelm@19741
   389
wenzelm@19741
   390
(*---------------------------------------------------------------------------
wenzelm@19741
   391
                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
wenzelm@19741
   392
                    lemma for admissibility problems
wenzelm@19741
   393
  --------------------------------------------------------------------------- *)
wenzelm@19741
   394
wenzelm@19741
   395
lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
wenzelm@27208
   396
apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
wenzelm@19741
   397
done
wenzelm@19741
   398
wenzelm@19741
   399
wenzelm@19741
   400
(*---------------------------------------------------------------------------
wenzelm@19741
   401
      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex
wenzelm@19741
   402
         lemma for eliminating non admissible equations in assumptions
wenzelm@19741
   403
  --------------------------------------------------------------------------- *)
wenzelm@19741
   404
wenzelm@25135
   405
lemma trick_against_eq_in_ass: "!! sch ex.
wenzelm@25135
   406
  Filter (%a. a:act AB)$sch = filter_act$ex
wenzelm@19741
   407
  ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
wenzelm@19741
   408
apply (simp add: filter_act_def)
wenzelm@19741
   409
apply (rule Zip_Map_fst_snd [symmetric])
wenzelm@19741
   410
done
wenzelm@19741
   411
wenzelm@19741
   412
(*---------------------------------------------------------------------------
wenzelm@19741
   413
     Filter of mkex(sch,exA,exB) to A after projection onto A is exA
wenzelm@19741
   414
                       using the above trick
wenzelm@19741
   415
  --------------------------------------------------------------------------- *)
wenzelm@19741
   416
wenzelm@19741
   417
wenzelm@25135
   418
lemma filter_mkex_is_exA: "!!sch exA exB.
wenzelm@25135
   419
  [| Forall (%a. a:act (A||B)) sch ;
wenzelm@25135
   420
  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
wenzelm@25135
   421
  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
wenzelm@19741
   422
  ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
wenzelm@19741
   423
apply (simp add: ProjA_def Filter_ex_def)
wenzelm@27208
   424
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   425
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   426
apply (rule conjI)
wenzelm@19741
   427
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   428
apply (simplesubst trick_against_eq_in_ass)
wenzelm@19741
   429
back
wenzelm@19741
   430
apply assumption
wenzelm@19741
   431
apply (simp add: filter_mkex_is_exA_tmp)
wenzelm@19741
   432
done
wenzelm@19741
   433
wenzelm@19741
   434
wenzelm@19741
   435
(*---------------------------------------------------------------------------
wenzelm@19741
   436
     Filter of mkex(sch,exA,exB) to B after projection onto B is exB
wenzelm@19741
   437
        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
wenzelm@19741
   438
        --           because of admissibility problems          --
wenzelm@19741
   439
                             structural induction
wenzelm@19741
   440
  --------------------------------------------------------------------------- *)
wenzelm@19741
   441
wenzelm@25135
   442
lemma filter_mkex_is_exB_tmp: "! exA exB s t.
wenzelm@25135
   443
  Forall (%x. x:act (A||B)) sch &
wenzelm@25135
   444
  Filter (%a. a:act A)$sch << filter_act$exA  &
wenzelm@25135
   445
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@25135
   446
  --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
wenzelm@19741
   447
      Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
wenzelm@19741
   448
wenzelm@19741
   449
(* notice necessary change of arguments exA and exB *)
wenzelm@46469
   450
  by (mkex_induct sch exA exB)
wenzelm@19741
   451
wenzelm@19741
   452
wenzelm@19741
   453
(*---------------------------------------------------------------------------
wenzelm@19741
   454
     Filter of mkex(sch,exA,exB) to A after projection onto B is exB
wenzelm@19741
   455
                       using the above trick
wenzelm@19741
   456
  --------------------------------------------------------------------------- *)
wenzelm@19741
   457
wenzelm@19741
   458
wenzelm@25135
   459
lemma filter_mkex_is_exB: "!!sch exA exB.
wenzelm@25135
   460
  [| Forall (%a. a:act (A||B)) sch ;
wenzelm@25135
   461
  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
wenzelm@25135
   462
  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
wenzelm@19741
   463
  ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
wenzelm@19741
   464
apply (simp add: ProjB_def Filter_ex_def)
wenzelm@27208
   465
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   466
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   467
apply (rule conjI)
wenzelm@19741
   468
apply (simp (no_asm) add: mkex_def)
wenzelm@19741
   469
apply (simplesubst trick_against_eq_in_ass)
wenzelm@19741
   470
back
wenzelm@19741
   471
apply assumption
wenzelm@19741
   472
apply (simp add: filter_mkex_is_exB_tmp)
wenzelm@19741
   473
done
wenzelm@19741
   474
wenzelm@19741
   475
(* --------------------------------------------------------------------- *)
wenzelm@19741
   476
(*                    mkex has only  A- or B-actions                    *)
wenzelm@19741
   477
(* --------------------------------------------------------------------- *)
wenzelm@19741
   478
wenzelm@19741
   479
wenzelm@25135
   480
lemma mkex_actions_in_AorB: "!s t exA exB.
wenzelm@25135
   481
  Forall (%x. x : act (A || B)) sch &
wenzelm@25135
   482
  Filter (%a. a:act A)$sch << filter_act$exA  &
wenzelm@25135
   483
  Filter (%a. a:act B)$sch << filter_act$exB
wenzelm@25135
   484
   --> Forall (%x. fst x : act (A ||B))
wenzelm@19741
   485
         (snd (mkex A B sch (s,exA) (t,exB)))"
wenzelm@46469
   486
  by (mkex_induct sch exA exB)
wenzelm@19741
   487
wenzelm@19741
   488
wenzelm@19741
   489
(* ------------------------------------------------------------------ *)
wenzelm@19741
   490
(*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
wenzelm@19741
   491
(*                          Main Theorem                              *)
wenzelm@19741
   492
(* ------------------------------------------------------------------ *)
wenzelm@19741
   493
wenzelm@25135
   494
lemma compositionality_sch:
wenzelm@25135
   495
"(sch : schedules (A||B)) =
wenzelm@25135
   496
  (Filter (%a. a:act A)$sch : schedules A &
wenzelm@25135
   497
   Filter (%a. a:act B)$sch : schedules B &
wenzelm@19741
   498
   Forall (%x. x:act (A||B)) sch)"
wenzelm@19741
   499
apply (simp (no_asm) add: schedules_def has_schedule_def)
haftmann@26359
   500
apply auto
wenzelm@19741
   501
(* ==> *)
wenzelm@19741
   502
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
wenzelm@19741
   503
prefer 2
wenzelm@19741
   504
apply (simp add: compositionality_ex)
wenzelm@19741
   505
apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
wenzelm@19741
   506
apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
wenzelm@19741
   507
prefer 2
wenzelm@19741
   508
apply (simp add: compositionality_ex)
wenzelm@19741
   509
apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
wenzelm@19741
   510
apply (simp add: executions_def)
wenzelm@27208
   511
apply (tactic {* pair_tac @{context} "ex" 1 *})
wenzelm@19741
   512
apply (erule conjE)
wenzelm@19741
   513
apply (simp add: sch_actions_in_AorB)
wenzelm@19741
   514
wenzelm@19741
   515
(* <== *)
wenzelm@19741
   516
wenzelm@19741
   517
(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
wenzelm@19741
   518
   we need here *)
wenzelm@19741
   519
apply (rename_tac exA exB)
wenzelm@19741
   520
apply (rule_tac x = "mkex A B sch exA exB" in bexI)
wenzelm@19741
   521
(* mkex actions are just the oracle *)
wenzelm@27208
   522
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   523
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   524
apply (simp add: Mapfst_mkex_is_sch)
wenzelm@19741
   525
wenzelm@19741
   526
(* mkex is an execution -- use compositionality on ex-level *)
wenzelm@19741
   527
apply (simp add: compositionality_ex)
wenzelm@19741
   528
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
wenzelm@27208
   529
apply (tactic {* pair_tac @{context} "exA" 1 *})
wenzelm@27208
   530
apply (tactic {* pair_tac @{context} "exB" 1 *})
wenzelm@19741
   531
apply (simp add: mkex_actions_in_AorB)
wenzelm@19741
   532
done
wenzelm@19741
   533
wenzelm@19741
   534
wenzelm@19741
   535
subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
wenzelm@19741
   536
wenzelm@25135
   537
lemma compositionality_sch_modules:
wenzelm@19741
   538
  "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
wenzelm@19741
   539
wenzelm@19741
   540
apply (unfold Scheds_def par_scheds_def)
wenzelm@19741
   541
apply (simp add: asig_of_par)
nipkow@39302
   542
apply (rule set_eqI)
wenzelm@19741
   543
apply (simp add: compositionality_sch actions_of_par)
wenzelm@19741
   544
done
wenzelm@19741
   545
wenzelm@19741
   546
wenzelm@19741
   547
declare compoex_simps [simp del]
wenzelm@19741
   548
declare composch_simps [simp del]
wenzelm@19741
   549
wenzelm@19741
   550
end