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