src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 58318 f95754ca7082
child 60754 02924903a6fd
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
wenzelm@40945
     2
    Author:     Olaf Müller
mueller@3071
     3
*) 
mueller@3071
     4
wenzelm@58880
     5
section {* Compositionality on Trace level *}
wenzelm@17233
     6
wenzelm@17233
     7
theory CompoTraces
wenzelm@17233
     8
imports CompoScheds ShortExecutions
wenzelm@17233
     9
begin
mueller@3071
    10
 
mueller@3071
    11
mueller@3071
    12
consts  
mueller@3071
    13
mueller@3521
    14
 mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
mueller@3521
    15
 par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
mueller@3071
    16
mueller@3071
    17
defs
mueller@3071
    18
wenzelm@17233
    19
mksch_def:
nipkow@10835
    20
  "mksch A B == (fix$(LAM h tr schA schB. case tr of 
mueller@3071
    21
       nil => nil
mueller@3071
    22
    | x##xs => 
mueller@3071
    23
      (case x of 
wenzelm@12028
    24
        UU => UU
mueller@3071
    25
      | Def y => 
mueller@3071
    26
         (if y:act A then 
mueller@3071
    27
             (if y:act B then 
nipkow@10835
    28
                   ((Takewhile (%a. a:int A)$schA)
nipkow@10835
    29
                      @@ (Takewhile (%a. a:int B)$schB)
nipkow@10835
    30
                           @@ (y>>(h$xs
nipkow@10835
    31
                                    $(TL$(Dropwhile (%a. a:int A)$schA))
nipkow@10835
    32
                                    $(TL$(Dropwhile (%a. a:int B)$schB))
mueller@3071
    33
                    )))
mueller@3071
    34
              else
nipkow@10835
    35
                 ((Takewhile (%a. a:int A)$schA)
nipkow@10835
    36
                  @@ (y>>(h$xs
nipkow@10835
    37
                           $(TL$(Dropwhile (%a. a:int A)$schA))
nipkow@10835
    38
                           $schB)))
mueller@3071
    39
              )
mueller@3071
    40
          else 
mueller@3071
    41
             (if y:act B then 
nipkow@10835
    42
                 ((Takewhile (%a. a:int B)$schB)
nipkow@10835
    43
                     @@ (y>>(h$xs
nipkow@10835
    44
                              $schA
nipkow@10835
    45
                              $(TL$(Dropwhile (%a. a:int B)$schB))
mueller@3071
    46
                              )))
mueller@3071
    47
             else
mueller@3071
    48
               UU
mueller@3071
    49
             )
mueller@3071
    50
         )
mueller@3071
    51
       )))"
mueller@3071
    52
mueller@3071
    53
wenzelm@17233
    54
par_traces_def:
mueller@3521
    55
  "par_traces TracesA TracesB == 
mueller@3521
    56
       let trA = fst TracesA; sigA = snd TracesA; 
mueller@3521
    57
           trB = fst TracesB; sigB = snd TracesB       
mueller@3521
    58
       in
nipkow@10835
    59
       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
nipkow@10835
    60
        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
mueller@3521
    61
        Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
mueller@3521
    62
        asig_comp sigA sigB)"
mueller@3521
    63
wenzelm@47026
    64
axiomatization where
mueller@3071
    65
wenzelm@17233
    66
finiteR_mksch:
wenzelm@48194
    67
  "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
wenzelm@48194
    68
wenzelm@48194
    69
lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
wenzelm@48194
    70
  by (blast intro: finiteR_mksch)
mueller@3071
    71
wenzelm@19741
    72
wenzelm@45625
    73
declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
wenzelm@19741
    74
wenzelm@19741
    75
wenzelm@19741
    76
subsection "mksch rewrite rules"
wenzelm@19741
    77
wenzelm@19741
    78
lemma mksch_unfold:
wenzelm@19741
    79
"mksch A B = (LAM tr schA schB. case tr of 
wenzelm@19741
    80
       nil => nil
wenzelm@19741
    81
    | x##xs => 
wenzelm@19741
    82
      (case x of  
wenzelm@19741
    83
        UU => UU  
wenzelm@19741
    84
      | Def y => 
wenzelm@19741
    85
         (if y:act A then 
wenzelm@19741
    86
             (if y:act B then 
wenzelm@19741
    87
                   ((Takewhile (%a. a:int A)$schA) 
wenzelm@19741
    88
                         @@(Takewhile (%a. a:int B)$schB) 
wenzelm@19741
    89
                              @@(y>>(mksch A B$xs   
wenzelm@19741
    90
                                       $(TL$(Dropwhile (%a. a:int A)$schA))  
wenzelm@19741
    91
                                       $(TL$(Dropwhile (%a. a:int B)$schB))  
wenzelm@19741
    92
                    )))   
wenzelm@19741
    93
              else  
wenzelm@19741
    94
                 ((Takewhile (%a. a:int A)$schA)  
wenzelm@19741
    95
                      @@ (y>>(mksch A B$xs  
wenzelm@19741
    96
                              $(TL$(Dropwhile (%a. a:int A)$schA))  
wenzelm@19741
    97
                              $schB)))  
wenzelm@19741
    98
              )   
wenzelm@19741
    99
          else    
wenzelm@19741
   100
             (if y:act B then  
wenzelm@19741
   101
                 ((Takewhile (%a. a:int B)$schB)  
wenzelm@19741
   102
                       @@ (y>>(mksch A B$xs   
wenzelm@19741
   103
                              $schA   
wenzelm@19741
   104
                              $(TL$(Dropwhile (%a. a:int B)$schB))  
wenzelm@19741
   105
                              )))  
wenzelm@19741
   106
             else  
wenzelm@19741
   107
               UU  
wenzelm@19741
   108
             )  
wenzelm@19741
   109
         )  
wenzelm@19741
   110
       ))"
wenzelm@19741
   111
apply (rule trans)
wenzelm@19741
   112
apply (rule fix_eq2)
wenzelm@19741
   113
apply (rule mksch_def)
wenzelm@19741
   114
apply (rule beta_cfun)
wenzelm@19741
   115
apply simp
wenzelm@19741
   116
done
wenzelm@19741
   117
wenzelm@19741
   118
lemma mksch_UU: "mksch A B$UU$schA$schB = UU"
wenzelm@19741
   119
apply (subst mksch_unfold)
wenzelm@19741
   120
apply simp
wenzelm@19741
   121
done
wenzelm@19741
   122
wenzelm@19741
   123
lemma mksch_nil: "mksch A B$nil$schA$schB = nil"
wenzelm@19741
   124
apply (subst mksch_unfold)
wenzelm@19741
   125
apply simp
wenzelm@19741
   126
done
wenzelm@19741
   127
wenzelm@19741
   128
lemma mksch_cons1: "[|x:act A;x~:act B|]   
wenzelm@19741
   129
    ==> mksch A B$(x>>tr)$schA$schB =  
wenzelm@19741
   130
          (Takewhile (%a. a:int A)$schA)  
wenzelm@19741
   131
          @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))  
wenzelm@19741
   132
                              $schB))"
wenzelm@19741
   133
apply (rule trans)
wenzelm@19741
   134
apply (subst mksch_unfold)
wenzelm@19741
   135
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   136
apply (simp add: Consq_def)
wenzelm@19741
   137
done
wenzelm@19741
   138
wenzelm@19741
   139
lemma mksch_cons2: "[|x~:act A;x:act B|]  
wenzelm@19741
   140
    ==> mksch A B$(x>>tr)$schA$schB =  
wenzelm@19741
   141
         (Takewhile (%a. a:int B)$schB)   
wenzelm@19741
   142
          @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))   
wenzelm@19741
   143
                             ))"
wenzelm@19741
   144
apply (rule trans)
wenzelm@19741
   145
apply (subst mksch_unfold)
wenzelm@19741
   146
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   147
apply (simp add: Consq_def)
wenzelm@19741
   148
done
wenzelm@19741
   149
wenzelm@19741
   150
lemma mksch_cons3: "[|x:act A;x:act B|]  
wenzelm@19741
   151
    ==> mksch A B$(x>>tr)$schA$schB =  
wenzelm@19741
   152
             (Takewhile (%a. a:int A)$schA)  
wenzelm@19741
   153
          @@ ((Takewhile (%a. a:int B)$schB)   
wenzelm@19741
   154
          @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))  
wenzelm@19741
   155
                             $(TL$(Dropwhile (%a. a:int B)$schB))))   
wenzelm@19741
   156
              )"
wenzelm@19741
   157
apply (rule trans)
wenzelm@19741
   158
apply (subst mksch_unfold)
wenzelm@19741
   159
apply (simp add: Consq_def If_and_if)
wenzelm@19741
   160
apply (simp add: Consq_def)
wenzelm@19741
   161
done
wenzelm@19741
   162
wenzelm@19741
   163
lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3
wenzelm@19741
   164
wenzelm@19741
   165
declare compotr_simps [simp]
wenzelm@19741
   166
wenzelm@19741
   167
wenzelm@19741
   168
subsection {* COMPOSITIONALITY on TRACE Level *}
wenzelm@19741
   169
wenzelm@19741
   170
subsubsection "Lemmata for ==>"
wenzelm@19741
   171
wenzelm@19741
   172
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
wenzelm@19741
   173
   the compatibility of IOA, in particular out of the condition that internals are
wenzelm@19741
   174
   really hidden. *)
wenzelm@19741
   175
wenzelm@19741
   176
lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->        
wenzelm@19741
   177
          (A & (eA | eB)) = (eA & A)"
wenzelm@19741
   178
apply fast
wenzelm@19741
   179
done
wenzelm@19741
   180
wenzelm@19741
   181
wenzelm@19741
   182
(* very similar to above, only the commutativity of | is used to make a slight change *)
wenzelm@19741
   183
wenzelm@19741
   184
lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->        
wenzelm@19741
   185
          (A & (eB | eA)) = (eA & A)"
wenzelm@19741
   186
apply fast
wenzelm@19741
   187
done
wenzelm@19741
   188
wenzelm@19741
   189
wenzelm@19741
   190
subsubsection "Lemmata for <=="
wenzelm@19741
   191
wenzelm@19741
   192
(* Lemma for substitution of looping assumption in another specific assumption *)
wenzelm@19741
   193
lemma subst_lemma1: "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"
wenzelm@19741
   194
by (erule subst)
wenzelm@19741
   195
wenzelm@19741
   196
(* Lemma for substitution of looping assumption in another specific assumption *)
wenzelm@19741
   197
lemma subst_lemma2: "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"
wenzelm@19741
   198
by (erule subst)
wenzelm@19741
   199
wenzelm@19741
   200
lemma ForallAorB_mksch [rule_format]:
wenzelm@19741
   201
  "!!A B. compatible A B ==>  
wenzelm@19741
   202
    ! schA schB. Forall (%x. x:act (A||B)) tr  
wenzelm@19741
   203
    --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
wenzelm@27208
   204
apply (tactic {* Seq_induct_tac @{context} "tr"
wenzelm@27208
   205
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
haftmann@26359
   206
apply auto
wenzelm@19741
   207
apply (simp add: actions_of_par)
wenzelm@19741
   208
apply (case_tac "a:act A")
wenzelm@19741
   209
apply (case_tac "a:act B")
wenzelm@19741
   210
(* a:A, a:B *)
wenzelm@19741
   211
apply simp
wenzelm@19741
   212
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   213
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   214
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   215
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   216
(* a:A,a~:B *)
wenzelm@19741
   217
apply simp
wenzelm@19741
   218
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   219
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   220
apply (case_tac "a:act B")
wenzelm@19741
   221
(* a~:A, a:B *)
wenzelm@19741
   222
apply simp
wenzelm@19741
   223
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   224
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   225
(* a~:A,a~:B *)
wenzelm@19741
   226
apply auto
wenzelm@19741
   227
done
wenzelm@19741
   228
wenzelm@19741
   229
lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>  
wenzelm@19741
   230
    ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
wenzelm@19741
   231
    --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
wenzelm@27208
   232
apply (tactic {* Seq_induct_tac @{context} "tr"
wenzelm@27208
   233
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
haftmann@26359
   234
apply auto
wenzelm@19741
   235
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   236
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   237
done
wenzelm@19741
   238
wenzelm@19741
   239
lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
wenzelm@19741
   240
    ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
wenzelm@19741
   241
    --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
wenzelm@27208
   242
apply (tactic {* Seq_induct_tac @{context} "tr"
wenzelm@27208
   243
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
haftmann@26359
   244
apply auto
wenzelm@19741
   245
apply (rule Forall_Conc_impl [THEN mp])
huffman@35215
   246
apply (simp add: intA_is_not_actB int_is_act)
wenzelm@19741
   247
done
wenzelm@19741
   248
wenzelm@19741
   249
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
wenzelm@19741
   250
declare FiniteConc [simp del]
wenzelm@19741
   251
wenzelm@19741
   252
lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>  
wenzelm@19741
   253
    ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &  
wenzelm@19741
   254
           Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &  
wenzelm@19741
   255
           Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr & 
wenzelm@19741
   256
           Forall (%x. x:ext (A||B)) tr  
wenzelm@19741
   257
           --> Finite (mksch A B$tr$x$y)"
wenzelm@19741
   258
wenzelm@19741
   259
apply (erule Seq_Finite_ind)
wenzelm@19741
   260
apply simp
wenzelm@19741
   261
(* main case *)
wenzelm@19741
   262
apply simp
haftmann@26359
   263
apply auto
wenzelm@19741
   264
wenzelm@19741
   265
(* a: act A; a: act B *)
huffman@40432
   266
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
huffman@40432
   267
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   268
back
wenzelm@19741
   269
apply (erule conjE)+
wenzelm@19741
   270
(* Finite (tw iA x) and Finite (tw iB y) *)
wenzelm@19741
   271
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
wenzelm@19741
   272
(* now for conclusion IH applicable, but assumptions have to be transformed *)
wenzelm@19741
   273
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
wenzelm@19741
   274
apply assumption
wenzelm@19741
   275
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
wenzelm@19741
   276
apply assumption
wenzelm@19741
   277
(* IH *)
wenzelm@19741
   278
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   279
wenzelm@19741
   280
(* a: act B; a~: act A *)
huffman@40432
   281
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   282
wenzelm@19741
   283
apply (erule conjE)+
wenzelm@19741
   284
(* Finite (tw iB y) *)
wenzelm@19741
   285
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
wenzelm@19741
   286
(* now for conclusion IH applicable, but assumptions have to be transformed *)
wenzelm@19741
   287
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
wenzelm@19741
   288
apply assumption
wenzelm@19741
   289
(* IH *)
wenzelm@19741
   290
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   291
wenzelm@19741
   292
(* a~: act B; a: act A *)
huffman@40432
   293
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   294
wenzelm@19741
   295
apply (erule conjE)+
wenzelm@19741
   296
(* Finite (tw iA x) *)
wenzelm@19741
   297
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
wenzelm@19741
   298
(* now for conclusion IH applicable, but assumptions have to be transformed *)
wenzelm@19741
   299
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
wenzelm@19741
   300
apply assumption
wenzelm@19741
   301
(* IH *)
wenzelm@19741
   302
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   303
wenzelm@19741
   304
(* a~: act B; a~: act A *)
nipkow@44890
   305
apply (fastforce intro!: ext_is_act simp: externals_of_par)
wenzelm@19741
   306
done
wenzelm@19741
   307
wenzelm@19741
   308
declare FiniteConc [simp]
wenzelm@19741
   309
wenzelm@19741
   310
declare FilterConc [simp del]
wenzelm@19741
   311
wenzelm@19741
   312
lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
wenzelm@19741
   313
 ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs & 
wenzelm@19741
   314
     Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)  
wenzelm@19741
   315
     --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &  
wenzelm@19741
   316
                    Forall (%x. x:act B & x~:act A) y1 &  
wenzelm@19741
   317
                    Finite y1 & y = (y1 @@ y2) &  
wenzelm@19741
   318
                    Filter (%a. a:ext B)$y1 = bs)"
wenzelm@19741
   319
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
wenzelm@19741
   320
apply (erule Seq_Finite_ind)
wenzelm@19741
   321
apply (rule allI)+
wenzelm@19741
   322
apply (rule impI)
wenzelm@19741
   323
apply (rule_tac x = "nil" in exI)
wenzelm@19741
   324
apply (rule_tac x = "y" in exI)
wenzelm@19741
   325
apply simp
wenzelm@19741
   326
(* main case *)
wenzelm@19741
   327
apply (rule allI)+
wenzelm@19741
   328
apply (rule impI)
wenzelm@19741
   329
apply simp
wenzelm@19741
   330
apply (erule conjE)+
wenzelm@19741
   331
apply simp
wenzelm@19741
   332
(* divide_Seq on s *)
huffman@40432
   333
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   334
apply (erule conjE)+
wenzelm@19741
   335
(* transform assumption f eB y = f B (s@z) *)
wenzelm@19741
   336
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
wenzelm@19741
   337
apply assumption
wenzelm@19741
   338
apply (simp add: not_ext_is_int_or_not_act FilterConc)
wenzelm@19741
   339
(* apply IH *)
wenzelm@19741
   340
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
wenzelm@19741
   341
apply (simp add: ForallTL ForallDropwhile FilterConc)
wenzelm@19741
   342
apply (erule exE)+
wenzelm@19741
   343
apply (erule conjE)+
wenzelm@19741
   344
apply (simp add: FilterConc)
wenzelm@19741
   345
(* for replacing IH in conclusion *)
wenzelm@19741
   346
apply (rotate_tac -2)
wenzelm@19741
   347
(* instantiate y1a and y2a *)
wenzelm@19741
   348
apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
wenzelm@19741
   349
apply (rule_tac x = "y2" in exI)
wenzelm@19741
   350
(* elminate all obligations up to two depending on Conc_assoc *)
huffman@35215
   351
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
wenzelm@19741
   352
apply (simp (no_asm) add: Conc_assoc FilterConc)
wenzelm@19741
   353
done
wenzelm@19741
   354
wenzelm@19741
   355
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
wenzelm@19741
   356
wenzelm@19741
   357
lemma reduceB_mksch1 [rule_format]:
wenzelm@19741
   358
" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
wenzelm@19741
   359
 ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s & 
wenzelm@19741
   360
     Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)  
wenzelm@19741
   361
     --> (? x1 x2.  (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &  
wenzelm@19741
   362
                    Forall (%x. x:act A & x~:act B) x1 &  
wenzelm@19741
   363
                    Finite x1 & x = (x1 @@ x2) &  
wenzelm@19741
   364
                    Filter (%a. a:ext A)$x1 = a_s)"
wenzelm@19741
   365
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
wenzelm@19741
   366
apply (erule Seq_Finite_ind)
wenzelm@19741
   367
apply (rule allI)+
wenzelm@19741
   368
apply (rule impI)
wenzelm@19741
   369
apply (rule_tac x = "nil" in exI)
wenzelm@19741
   370
apply (rule_tac x = "x" in exI)
wenzelm@19741
   371
apply simp
wenzelm@19741
   372
(* main case *)
wenzelm@19741
   373
apply (rule allI)+
wenzelm@19741
   374
apply (rule impI)
wenzelm@19741
   375
apply simp
wenzelm@19741
   376
apply (erule conjE)+
wenzelm@19741
   377
apply simp
wenzelm@19741
   378
(* divide_Seq on s *)
huffman@40432
   379
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   380
apply (erule conjE)+
wenzelm@19741
   381
(* transform assumption f eA x = f A (s@z) *)
wenzelm@19741
   382
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
wenzelm@19741
   383
apply assumption
wenzelm@19741
   384
apply (simp add: not_ext_is_int_or_not_act FilterConc)
wenzelm@19741
   385
(* apply IH *)
wenzelm@19741
   386
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
wenzelm@19741
   387
apply (simp add: ForallTL ForallDropwhile FilterConc)
wenzelm@19741
   388
apply (erule exE)+
wenzelm@19741
   389
apply (erule conjE)+
wenzelm@19741
   390
apply (simp add: FilterConc)
wenzelm@19741
   391
(* for replacing IH in conclusion *)
wenzelm@19741
   392
apply (rotate_tac -2)
wenzelm@19741
   393
(* instantiate y1a and y2a *)
wenzelm@19741
   394
apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
wenzelm@19741
   395
apply (rule_tac x = "x2" in exI)
wenzelm@19741
   396
(* elminate all obligations up to two depending on Conc_assoc *)
huffman@35215
   397
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
wenzelm@19741
   398
apply (simp (no_asm) add: Conc_assoc FilterConc)
wenzelm@19741
   399
done
wenzelm@19741
   400
wenzelm@19741
   401
lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]
wenzelm@19741
   402
wenzelm@19741
   403
declare FilterConc [simp]
wenzelm@19741
   404
wenzelm@19741
   405
wenzelm@19741
   406
subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
wenzelm@19741
   407
wenzelm@19741
   408
lemma FilterA_mksch_is_tr: 
wenzelm@19741
   409
"!! A B. [| compatible A B; compatible B A; 
wenzelm@19741
   410
            is_asig(asig_of A); is_asig(asig_of B) |] ==>  
wenzelm@19741
   411
  ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
wenzelm@19741
   412
  Forall (%x. x:ext (A||B)) tr &  
wenzelm@19741
   413
  Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA & 
wenzelm@19741
   414
  Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
wenzelm@19741
   415
  --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
wenzelm@19741
   416
wenzelm@27208
   417
apply (tactic {* Seq_induct_tac @{context} "tr"
wenzelm@27208
   418
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
wenzelm@19741
   419
(* main case *)
wenzelm@19741
   420
(* splitting into 4 cases according to a:A, a:B *)
haftmann@26359
   421
apply auto
wenzelm@19741
   422
wenzelm@19741
   423
(* Case a:A, a:B *)
wenzelm@19741
   424
apply (frule divide_Seq)
wenzelm@19741
   425
apply (frule divide_Seq)
wenzelm@19741
   426
back
wenzelm@19741
   427
apply (erule conjE)+
wenzelm@19741
   428
(* filtering internals of A in schA and of B in schB is nil *)
wenzelm@19741
   429
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
wenzelm@19741
   430
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
wenzelm@19741
   431
apply (drule_tac x = "schA" in subst_lemma1)
wenzelm@19741
   432
apply assumption
wenzelm@19741
   433
apply (drule_tac x = "schB" in subst_lemma1)
wenzelm@19741
   434
apply assumption
wenzelm@19741
   435
(* IH *)
wenzelm@19741
   436
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   437
wenzelm@19741
   438
(* Case a:A, a~:B *)
wenzelm@19741
   439
apply (frule divide_Seq)
wenzelm@19741
   440
apply (erule conjE)+
wenzelm@19741
   441
(* filtering internals of A is nil *)
wenzelm@19741
   442
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
wenzelm@19741
   443
apply (drule_tac x = "schA" in subst_lemma1)
wenzelm@19741
   444
apply assumption
wenzelm@19741
   445
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   446
wenzelm@19741
   447
(* Case a:B, a~:A *)
wenzelm@19741
   448
apply (frule divide_Seq)
wenzelm@19741
   449
apply (erule conjE)+
wenzelm@19741
   450
(* filtering internals of A is nil *)
wenzelm@19741
   451
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
wenzelm@19741
   452
apply (drule_tac x = "schB" in subst_lemma1)
wenzelm@19741
   453
back
wenzelm@19741
   454
apply assumption
wenzelm@19741
   455
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
wenzelm@19741
   456
wenzelm@19741
   457
(* Case a~:A, a~:B *)
nipkow@44890
   458
apply (fastforce intro!: ext_is_act simp: externals_of_par)
wenzelm@19741
   459
done
wenzelm@19741
   460
wenzelm@19741
   461
wenzelm@19741
   462
subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
wenzelm@19741
   463
wenzelm@19741
   464
lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;  
wenzelm@19741
   465
  is_asig(asig_of A); is_asig(asig_of B) |] ==>  
wenzelm@19741
   466
  Forall (%x. x:ext (A||B)) tr &  
wenzelm@19741
   467
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
wenzelm@19741
   468
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
wenzelm@19741
   469
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
wenzelm@19741
   470
  LastActExtsch A schA & LastActExtsch B schB   
wenzelm@19741
   471
  --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
wenzelm@19741
   472
apply (intro strip)
huffman@35642
   473
apply (rule seq.take_lemma)
wenzelm@19741
   474
apply (rule mp)
wenzelm@19741
   475
prefer 2 apply assumption
wenzelm@19741
   476
back back back back
wenzelm@19741
   477
apply (rule_tac x = "schA" in spec)
wenzelm@19741
   478
apply (rule_tac x = "schB" in spec)
wenzelm@19741
   479
apply (rule_tac x = "tr" in spec)
wenzelm@19741
   480
apply (tactic "thin_tac' 5 1")
wenzelm@19741
   481
apply (rule nat_less_induct)
wenzelm@19741
   482
apply (rule allI)+
wenzelm@19741
   483
apply (rename_tac tr schB schA)
wenzelm@19741
   484
apply (intro strip)
wenzelm@19741
   485
apply (erule conjE)+
wenzelm@19741
   486
wenzelm@19741
   487
apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
wenzelm@19741
   488
wenzelm@19741
   489
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
wenzelm@19741
   490
apply (tactic "thin_tac' 5 1")
wenzelm@19741
   491
wenzelm@19741
   492
wenzelm@19741
   493
apply (case_tac "Finite tr")
wenzelm@19741
   494
wenzelm@19741
   495
(* both sides of this equation are nil *)
wenzelm@19741
   496
apply (subgoal_tac "schA=nil")
wenzelm@19741
   497
apply (simp (no_asm_simp))
wenzelm@19741
   498
(* first side: mksch = nil *)
wenzelm@19741
   499
apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
wenzelm@19741
   500
(* second side: schA = nil *)
wenzelm@19741
   501
apply (erule_tac A = "A" in LastActExtimplnil)
wenzelm@19741
   502
apply (simp (no_asm_simp))
wenzelm@19741
   503
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
wenzelm@19741
   504
apply assumption
wenzelm@19741
   505
apply fast
wenzelm@19741
   506
wenzelm@19741
   507
(* case ~ Finite s *)
wenzelm@19741
   508
wenzelm@19741
   509
(* both sides of this equation are UU *)
wenzelm@19741
   510
apply (subgoal_tac "schA=UU")
wenzelm@19741
   511
apply (simp (no_asm_simp))
wenzelm@19741
   512
(* first side: mksch = UU *)
wenzelm@48194
   513
apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
wenzelm@19741
   514
(* schA = UU *)
wenzelm@19741
   515
apply (erule_tac A = "A" in LastActExtimplUU)
wenzelm@19741
   516
apply (simp (no_asm_simp))
wenzelm@19741
   517
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
wenzelm@19741
   518
apply assumption
wenzelm@19741
   519
apply fast
wenzelm@19741
   520
wenzelm@19741
   521
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
wenzelm@19741
   522
wenzelm@19741
   523
apply (drule divide_Seq3)
wenzelm@19741
   524
wenzelm@19741
   525
apply (erule exE)+
wenzelm@19741
   526
apply (erule conjE)+
wenzelm@19741
   527
apply hypsubst
wenzelm@19741
   528
wenzelm@19741
   529
(* bring in lemma reduceA_mksch *)
wenzelm@19741
   530
apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
wenzelm@19741
   531
apply assumption+
wenzelm@19741
   532
apply (erule exE)+
wenzelm@19741
   533
apply (erule conjE)+
wenzelm@19741
   534
wenzelm@19741
   535
(* use reduceA_mksch to rewrite conclusion *)
wenzelm@19741
   536
apply hypsubst
wenzelm@19741
   537
apply simp
wenzelm@19741
   538
wenzelm@19741
   539
(* eliminate the B-only prefix *)
wenzelm@19741
   540
wenzelm@19741
   541
apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
wenzelm@19741
   542
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   543
prefer 2 apply assumption
wenzelm@19741
   544
prefer 2 apply fast
wenzelm@19741
   545
wenzelm@19741
   546
(* Now real recursive step follows (in y) *)
wenzelm@19741
   547
wenzelm@19741
   548
apply simp
wenzelm@19741
   549
apply (case_tac "x:act A")
wenzelm@19741
   550
apply (case_tac "x~:act B")
wenzelm@19741
   551
apply (rotate_tac -2)
wenzelm@19741
   552
apply simp
wenzelm@19741
   553
wenzelm@19741
   554
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
wenzelm@19741
   555
apply (rotate_tac -1)
wenzelm@19741
   556
apply simp
wenzelm@19741
   557
(* eliminate introduced subgoal 2 *)
wenzelm@19741
   558
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   559
prefer 2 apply assumption
wenzelm@19741
   560
prefer 2 apply fast
wenzelm@19741
   561
wenzelm@19741
   562
(* bring in divide Seq for s *)
huffman@40432
   563
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   564
apply (erule conjE)+
wenzelm@19741
   565
blanchet@58318
   566
(* subst divide_Seq in conclusion, but only at the righest occurrence *)
wenzelm@19741
   567
apply (rule_tac t = "schA" in ssubst)
wenzelm@19741
   568
back
wenzelm@19741
   569
back
wenzelm@19741
   570
back
wenzelm@19741
   571
apply assumption
wenzelm@19741
   572
wenzelm@19741
   573
(* reduce trace_takes from n to strictly smaller k *)
wenzelm@19741
   574
apply (rule take_reduction)
wenzelm@19741
   575
wenzelm@19741
   576
(* f A (tw iA) = tw ~eA *)
huffman@35215
   577
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   578
apply (rule refl)
wenzelm@19741
   579
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   580
apply (rotate_tac -11)
wenzelm@19741
   581
wenzelm@19741
   582
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
wenzelm@19741
   583
wenzelm@19741
   584
(* assumption Forall tr *)
wenzelm@19741
   585
(* assumption schB *)
huffman@35215
   586
apply (simp add: ext_and_act)
wenzelm@19741
   587
(* assumption schA *)
wenzelm@19741
   588
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
wenzelm@19741
   589
apply assumption
wenzelm@19741
   590
apply (simp add: int_is_not_ext)
wenzelm@19741
   591
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
wenzelm@19741
   592
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
wenzelm@19741
   593
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
wenzelm@19741
   594
apply assumption
wenzelm@19741
   595
wenzelm@19741
   596
(* assumption Forall schA *)
wenzelm@19741
   597
apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
wenzelm@19741
   598
apply assumption
huffman@35215
   599
apply (simp add: int_is_act)
wenzelm@19741
   600
wenzelm@19741
   601
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
wenzelm@19741
   602
wenzelm@19741
   603
wenzelm@19741
   604
apply (rotate_tac -2)
wenzelm@19741
   605
apply simp
wenzelm@19741
   606
wenzelm@19741
   607
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
wenzelm@19741
   608
apply (rotate_tac -1)
wenzelm@19741
   609
apply simp
wenzelm@19741
   610
(* eliminate introduced subgoal 2 *)
wenzelm@19741
   611
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   612
prefer 2 apply (assumption)
wenzelm@19741
   613
prefer 2 apply (fast)
wenzelm@19741
   614
wenzelm@19741
   615
(* bring in divide Seq for s *)
huffman@40432
   616
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   617
apply (erule conjE)+
wenzelm@19741
   618
blanchet@58318
   619
(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
wenzelm@19741
   620
apply (rule_tac t = "schA" in ssubst)
wenzelm@19741
   621
back
wenzelm@19741
   622
back
wenzelm@19741
   623
back
wenzelm@19741
   624
apply assumption
wenzelm@19741
   625
wenzelm@19741
   626
(* f A (tw iA) = tw ~eA *)
huffman@35215
   627
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   628
wenzelm@19741
   629
(* rewrite assumption forall and schB *)
wenzelm@19741
   630
apply (rotate_tac 13)
wenzelm@19741
   631
apply (simp add: ext_and_act)
wenzelm@19741
   632
wenzelm@19741
   633
(* divide_Seq for schB2 *)
huffman@40432
   634
apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   635
apply (erule conjE)+
wenzelm@19741
   636
(* assumption schA *)
wenzelm@19741
   637
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
wenzelm@19741
   638
apply assumption
wenzelm@19741
   639
apply (simp add: int_is_not_ext)
wenzelm@19741
   640
wenzelm@19741
   641
(* f A (tw iB schB2) = nil *)
wenzelm@19741
   642
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
wenzelm@19741
   643
wenzelm@19741
   644
wenzelm@19741
   645
(* reduce trace_takes from n to strictly smaller k *)
wenzelm@19741
   646
apply (rule take_reduction)
wenzelm@19741
   647
apply (rule refl)
wenzelm@19741
   648
apply (rule refl)
wenzelm@19741
   649
wenzelm@19741
   650
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
wenzelm@19741
   651
wenzelm@19741
   652
(* assumption schB *)
wenzelm@19741
   653
apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
wenzelm@19741
   654
apply assumption
wenzelm@19741
   655
apply (simp add: intA_is_not_actB int_is_not_ext)
wenzelm@19741
   656
wenzelm@19741
   657
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
wenzelm@19741
   658
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
wenzelm@19741
   659
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
wenzelm@19741
   660
apply assumption
wenzelm@19741
   661
apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)
wenzelm@19741
   662
wenzelm@19741
   663
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
wenzelm@19741
   664
apply (simp add: ForallTL ForallDropwhile)
wenzelm@19741
   665
wenzelm@19741
   666
(* case x~:A & x:B  *)
wenzelm@19741
   667
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
wenzelm@19741
   668
apply (case_tac "x:act B")
wenzelm@19741
   669
apply fast
wenzelm@19741
   670
wenzelm@19741
   671
(* case x~:A & x~:B  *)
wenzelm@19741
   672
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
wenzelm@19741
   673
apply (rotate_tac -9)
wenzelm@19741
   674
(* reduce forall assumption from tr to (x>>rs) *)
wenzelm@19741
   675
apply (simp add: externals_of_par)
wenzelm@19741
   676
apply (fast intro!: ext_is_act)
wenzelm@19741
   677
wenzelm@19741
   678
done
wenzelm@19741
   679
wenzelm@19741
   680
wenzelm@19741
   681
wenzelm@19741
   682
subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
wenzelm@19741
   683
wenzelm@19741
   684
lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;  
wenzelm@19741
   685
  is_asig(asig_of A); is_asig(asig_of B) |] ==>  
wenzelm@19741
   686
  Forall (%x. x:ext (A||B)) tr &  
wenzelm@19741
   687
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
wenzelm@19741
   688
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
wenzelm@19741
   689
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
wenzelm@19741
   690
  LastActExtsch A schA & LastActExtsch B schB   
wenzelm@19741
   691
  --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
wenzelm@19741
   692
apply (intro strip)
huffman@35642
   693
apply (rule seq.take_lemma)
wenzelm@19741
   694
apply (rule mp)
wenzelm@19741
   695
prefer 2 apply assumption
wenzelm@19741
   696
back back back back
wenzelm@19741
   697
apply (rule_tac x = "schA" in spec)
wenzelm@19741
   698
apply (rule_tac x = "schB" in spec)
wenzelm@19741
   699
apply (rule_tac x = "tr" in spec)
wenzelm@19741
   700
apply (tactic "thin_tac' 5 1")
wenzelm@19741
   701
apply (rule nat_less_induct)
wenzelm@19741
   702
apply (rule allI)+
wenzelm@19741
   703
apply (rename_tac tr schB schA)
wenzelm@19741
   704
apply (intro strip)
wenzelm@19741
   705
apply (erule conjE)+
wenzelm@19741
   706
wenzelm@19741
   707
apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
wenzelm@19741
   708
wenzelm@19741
   709
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
wenzelm@19741
   710
apply (tactic "thin_tac' 5 1")
wenzelm@19741
   711
wenzelm@19741
   712
apply (case_tac "Finite tr")
wenzelm@19741
   713
wenzelm@19741
   714
(* both sides of this equation are nil *)
wenzelm@19741
   715
apply (subgoal_tac "schB=nil")
wenzelm@19741
   716
apply (simp (no_asm_simp))
wenzelm@19741
   717
(* first side: mksch = nil *)
wenzelm@19741
   718
apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
wenzelm@19741
   719
(* second side: schA = nil *)
wenzelm@19741
   720
apply (erule_tac A = "B" in LastActExtimplnil)
wenzelm@19741
   721
apply (simp (no_asm_simp))
wenzelm@19741
   722
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
wenzelm@19741
   723
apply assumption
wenzelm@19741
   724
apply fast
wenzelm@19741
   725
wenzelm@19741
   726
(* case ~ Finite tr *)
wenzelm@19741
   727
wenzelm@19741
   728
(* both sides of this equation are UU *)
wenzelm@19741
   729
apply (subgoal_tac "schB=UU")
wenzelm@19741
   730
apply (simp (no_asm_simp))
wenzelm@19741
   731
(* first side: mksch = UU *)
wenzelm@48194
   732
apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
wenzelm@19741
   733
(* schA = UU *)
wenzelm@19741
   734
apply (erule_tac A = "B" in LastActExtimplUU)
wenzelm@19741
   735
apply (simp (no_asm_simp))
wenzelm@19741
   736
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
wenzelm@19741
   737
apply assumption
wenzelm@19741
   738
apply fast
wenzelm@19741
   739
wenzelm@19741
   740
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
wenzelm@19741
   741
wenzelm@19741
   742
apply (drule divide_Seq3)
wenzelm@19741
   743
wenzelm@19741
   744
apply (erule exE)+
wenzelm@19741
   745
apply (erule conjE)+
wenzelm@19741
   746
apply hypsubst
wenzelm@19741
   747
wenzelm@19741
   748
(* bring in lemma reduceB_mksch *)
wenzelm@19741
   749
apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
wenzelm@19741
   750
apply assumption+
wenzelm@19741
   751
apply (erule exE)+
wenzelm@19741
   752
apply (erule conjE)+
wenzelm@19741
   753
wenzelm@19741
   754
(* use reduceB_mksch to rewrite conclusion *)
wenzelm@19741
   755
apply hypsubst
wenzelm@19741
   756
apply simp
wenzelm@19741
   757
wenzelm@19741
   758
(* eliminate the A-only prefix *)
wenzelm@19741
   759
wenzelm@19741
   760
apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
wenzelm@19741
   761
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   762
prefer 2 apply (assumption)
wenzelm@19741
   763
prefer 2 apply (fast)
wenzelm@19741
   764
wenzelm@19741
   765
(* Now real recursive step follows (in x) *)
wenzelm@19741
   766
wenzelm@19741
   767
apply simp
wenzelm@19741
   768
apply (case_tac "x:act B")
wenzelm@19741
   769
apply (case_tac "x~:act A")
wenzelm@19741
   770
apply (rotate_tac -2)
wenzelm@19741
   771
apply simp
wenzelm@19741
   772
wenzelm@19741
   773
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
wenzelm@19741
   774
apply (rotate_tac -1)
wenzelm@19741
   775
apply simp
wenzelm@19741
   776
(* eliminate introduced subgoal 2 *)
wenzelm@19741
   777
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   778
prefer 2 apply (assumption)
wenzelm@19741
   779
prefer 2 apply (fast)
wenzelm@19741
   780
wenzelm@19741
   781
(* bring in divide Seq for s *)
huffman@40432
   782
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   783
apply (erule conjE)+
wenzelm@19741
   784
blanchet@58318
   785
(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
wenzelm@19741
   786
apply (rule_tac t = "schB" in ssubst)
wenzelm@19741
   787
back
wenzelm@19741
   788
back
wenzelm@19741
   789
back
wenzelm@19741
   790
apply assumption
wenzelm@19741
   791
wenzelm@19741
   792
(* reduce trace_takes from n to strictly smaller k *)
wenzelm@19741
   793
apply (rule take_reduction)
wenzelm@19741
   794
wenzelm@19741
   795
(* f B (tw iB) = tw ~eB *)
huffman@35215
   796
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   797
apply (rule refl)
wenzelm@19741
   798
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   799
apply (rotate_tac -11)
wenzelm@19741
   800
wenzelm@19741
   801
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
wenzelm@19741
   802
wenzelm@19741
   803
(* assumption schA *)
huffman@35215
   804
apply (simp add: ext_and_act)
wenzelm@19741
   805
(* assumption schB *)
wenzelm@19741
   806
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
wenzelm@19741
   807
apply assumption
wenzelm@19741
   808
apply (simp add: int_is_not_ext)
wenzelm@19741
   809
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
wenzelm@19741
   810
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
wenzelm@19741
   811
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
wenzelm@19741
   812
apply assumption
wenzelm@19741
   813
wenzelm@19741
   814
(* assumption Forall schB *)
wenzelm@19741
   815
apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
wenzelm@19741
   816
apply assumption
huffman@35215
   817
apply (simp add: int_is_act)
wenzelm@19741
   818
wenzelm@19741
   819
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
wenzelm@19741
   820
wenzelm@19741
   821
apply (rotate_tac -2)
wenzelm@19741
   822
apply simp
wenzelm@19741
   823
wenzelm@19741
   824
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
wenzelm@19741
   825
apply (rotate_tac -1)
wenzelm@19741
   826
apply simp
wenzelm@19741
   827
(* eliminate introduced subgoal 2 *)
wenzelm@19741
   828
apply (erule_tac [2] ForallQFilterPnil)
wenzelm@19741
   829
prefer 2 apply (assumption)
wenzelm@19741
   830
prefer 2 apply (fast)
wenzelm@19741
   831
wenzelm@19741
   832
(* bring in divide Seq for s *)
huffman@40432
   833
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   834
apply (erule conjE)+
wenzelm@19741
   835
blanchet@58318
   836
(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
wenzelm@19741
   837
apply (rule_tac t = "schB" in ssubst)
wenzelm@19741
   838
back
wenzelm@19741
   839
back
wenzelm@19741
   840
back
wenzelm@19741
   841
apply assumption
wenzelm@19741
   842
wenzelm@19741
   843
(* f B (tw iB) = tw ~eB *)
huffman@35215
   844
apply (simp add: int_is_act not_ext_is_int_or_not_act)
wenzelm@19741
   845
wenzelm@19741
   846
(* rewrite assumption forall and schB *)
wenzelm@19741
   847
apply (rotate_tac 13)
wenzelm@19741
   848
apply (simp add: ext_and_act)
wenzelm@19741
   849
wenzelm@19741
   850
(* divide_Seq for schB2 *)
huffman@40432
   851
apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
wenzelm@19741
   852
apply (erule conjE)+
wenzelm@19741
   853
(* assumption schA *)
wenzelm@19741
   854
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
wenzelm@19741
   855
apply assumption
wenzelm@19741
   856
apply (simp add: int_is_not_ext)
wenzelm@19741
   857
wenzelm@19741
   858
(* f B (tw iA schA2) = nil *)
wenzelm@19741
   859
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
wenzelm@19741
   860
wenzelm@19741
   861
wenzelm@19741
   862
(* reduce trace_takes from n to strictly smaller k *)
wenzelm@19741
   863
apply (rule take_reduction)
wenzelm@19741
   864
apply (rule refl)
wenzelm@19741
   865
apply (rule refl)
wenzelm@19741
   866
wenzelm@19741
   867
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
wenzelm@19741
   868
wenzelm@19741
   869
(* assumption schA *)
wenzelm@19741
   870
apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
wenzelm@19741
   871
apply assumption
wenzelm@19741
   872
apply (simp add: intA_is_not_actB int_is_not_ext)
wenzelm@19741
   873
wenzelm@19741
   874
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
wenzelm@19741
   875
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
wenzelm@19741
   876
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
wenzelm@19741
   877
apply assumption
wenzelm@19741
   878
apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
wenzelm@19741
   879
wenzelm@19741
   880
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
wenzelm@19741
   881
apply (simp add: ForallTL ForallDropwhile)
wenzelm@19741
   882
wenzelm@19741
   883
(* case x~:B & x:A  *)
wenzelm@19741
   884
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
wenzelm@19741
   885
apply (case_tac "x:act A")
wenzelm@19741
   886
apply fast
wenzelm@19741
   887
wenzelm@19741
   888
(* case x~:B & x~:A  *)
wenzelm@19741
   889
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
wenzelm@19741
   890
apply (rotate_tac -9)
wenzelm@19741
   891
(* reduce forall assumption from tr to (x>>rs) *)
wenzelm@19741
   892
apply (simp add: externals_of_par)
wenzelm@19741
   893
apply (fast intro!: ext_is_act)
wenzelm@19741
   894
wenzelm@19741
   895
done
wenzelm@19741
   896
wenzelm@19741
   897
wenzelm@19741
   898
subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
wenzelm@19741
   899
wenzelm@19741
   900
lemma compositionality_tr: 
wenzelm@19741
   901
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
wenzelm@19741
   902
            is_asig(asig_of A); is_asig(asig_of B)|]  
wenzelm@19741
   903
        ==>  (tr: traces(A||B)) =  
wenzelm@19741
   904
             (Filter (%a. a:act A)$tr : traces A & 
wenzelm@19741
   905
              Filter (%a. a:act B)$tr : traces B & 
wenzelm@19741
   906
              Forall (%x. x:ext(A||B)) tr)"
wenzelm@19741
   907
wenzelm@19741
   908
apply (simp (no_asm) add: traces_def has_trace_def)
haftmann@26359
   909
apply auto
wenzelm@19741
   910
wenzelm@19741
   911
(* ==> *)
wenzelm@19741
   912
(* There is a schedule of A *)
wenzelm@19741
   913
apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
wenzelm@19741
   914
prefer 2
wenzelm@19741
   915
apply (simp add: compositionality_sch)
wenzelm@19741
   916
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
wenzelm@19741
   917
(* There is a schedule of B *)
wenzelm@19741
   918
apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
wenzelm@19741
   919
prefer 2
wenzelm@19741
   920
apply (simp add: compositionality_sch)
wenzelm@19741
   921
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
wenzelm@19741
   922
(* Traces of A||B have only external actions from A or B *)
wenzelm@19741
   923
apply (rule ForallPFilterP)
wenzelm@19741
   924
wenzelm@19741
   925
(* <== *)
wenzelm@19741
   926
wenzelm@19741
   927
(* replace schA and schB by Cut(schA) and Cut(schB) *)
wenzelm@19741
   928
apply (drule exists_LastActExtsch)
wenzelm@19741
   929
apply assumption
wenzelm@19741
   930
apply (drule exists_LastActExtsch)
wenzelm@19741
   931
apply assumption
wenzelm@19741
   932
apply (erule exE)+
wenzelm@19741
   933
apply (erule conjE)+
wenzelm@19741
   934
(* Schedules of A(B) have only actions of A(B) *)
wenzelm@19741
   935
apply (drule scheds_in_sig)
wenzelm@19741
   936
apply assumption
wenzelm@19741
   937
apply (drule scheds_in_sig)
wenzelm@19741
   938
apply assumption
wenzelm@19741
   939
wenzelm@19741
   940
apply (rename_tac h1 h2 schA schB)
wenzelm@19741
   941
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
wenzelm@19741
   942
   we need here *)
wenzelm@19741
   943
apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
wenzelm@19741
   944
wenzelm@19741
   945
(* External actions of mksch are just the oracle *)
wenzelm@19741
   946
apply (simp add: FilterA_mksch_is_tr)
wenzelm@19741
   947
wenzelm@19741
   948
(* mksch is a schedule -- use compositionality on sch-level *)
wenzelm@19741
   949
apply (simp add: compositionality_sch)
wenzelm@19741
   950
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
wenzelm@19741
   951
apply (erule ForallAorB_mksch)
wenzelm@19741
   952
apply (erule ForallPForallQ)
wenzelm@19741
   953
apply (erule ext_is_act)
wenzelm@19741
   954
done
wenzelm@19741
   955
wenzelm@19741
   956
wenzelm@19741
   957
wenzelm@19741
   958
subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
wenzelm@19741
   959
wenzelm@19741
   960
lemma compositionality_tr_modules: 
wenzelm@19741
   961
wenzelm@19741
   962
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
wenzelm@19741
   963
            is_asig(asig_of A); is_asig(asig_of B)|]  
wenzelm@19741
   964
 ==> Traces (A||B) = par_traces (Traces A) (Traces B)"
wenzelm@19741
   965
wenzelm@19741
   966
apply (unfold Traces_def par_traces_def)
wenzelm@19741
   967
apply (simp add: asig_of_par)
nipkow@39302
   968
apply (rule set_eqI)
wenzelm@19741
   969
apply (simp add: compositionality_tr externals_of_par)
wenzelm@19741
   970
done
wenzelm@19741
   971
wenzelm@19741
   972
wenzelm@47239
   973
declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}
mueller@3071
   974
mueller@3071
   975
mueller@3071
   976
end