src/HOLCF/IOA/meta_theory/CompoTraces.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4473 803d1e302af1
child 4520 d430a1b34928
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.ML
mueller@3080
     2
    ID:		$Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3275
     5
 
mueller@3071
     6
Compositionality on Trace level.
mueller@3071
     7
*) 
mueller@3071
     8
mueller@3071
     9
mueller@3275
    10
mueller@3071
    11
(* ---------------------------------------------------------------- *)
mueller@3071
    12
                   section "mksch rewrite rules";
mueller@3071
    13
(* ---------------------------------------------------------------- *)
mueller@3071
    14
mueller@3071
    15
mueller@3071
    16
mueller@3071
    17
mueller@3071
    18
bind_thm ("mksch_unfold", fix_prover2 thy mksch_def 
mueller@3071
    19
"mksch A B = (LAM tr schA schB. case tr of \
mueller@3071
    20
\       nil => nil\
mueller@3071
    21
\    | x##xs => \
mueller@3071
    22
\      (case x of  \ 
mueller@3071
    23
\        Undef => UU  \
mueller@3071
    24
\      | Def y => \
mueller@3071
    25
\         (if y:act A then \
mueller@3071
    26
\             (if y:act B then \ 
wenzelm@3842
    27
\                   ((Takewhile (%a. a:int A)`schA) \
wenzelm@3842
    28
\                         @@(Takewhile (%a. a:int B)`schB) \
mueller@3071
    29
\                              @@(y>>(mksch A B`xs   \
wenzelm@3842
    30
\                                       `(TL`(Dropwhile (%a. a:int A)`schA))  \
wenzelm@3842
    31
\                                       `(TL`(Dropwhile (%a. a:int B)`schB))  \
mueller@3071
    32
\                    )))   \
mueller@3071
    33
\              else  \
wenzelm@3842
    34
\                 ((Takewhile (%a. a:int A)`schA)  \
mueller@3071
    35
\                      @@ (y>>(mksch A B`xs  \
wenzelm@3842
    36
\                              `(TL`(Dropwhile (%a. a:int A)`schA))  \
mueller@3071
    37
\                              `schB)))  \
mueller@3071
    38
\              )   \
mueller@3071
    39
\          else    \
mueller@3071
    40
\             (if y:act B then  \ 
wenzelm@3842
    41
\                 ((Takewhile (%a. a:int B)`schB)  \
mueller@3071
    42
\                       @@ (y>>(mksch A B`xs   \
mueller@3071
    43
\                              `schA   \
wenzelm@3842
    44
\                              `(TL`(Dropwhile (%a. a:int B)`schB))  \
mueller@3071
    45
\                              )))  \
mueller@3071
    46
\             else  \
mueller@3071
    47
\               UU  \
mueller@3071
    48
\             )  \
mueller@3071
    49
\         )  \
mueller@3071
    50
\       ))");
mueller@3071
    51
mueller@3071
    52
mueller@3071
    53
goal thy "mksch A B`UU`schA`schB = UU";
mueller@3071
    54
by (stac mksch_unfold 1);
mueller@3071
    55
by (Simp_tac 1);
mueller@3071
    56
qed"mksch_UU";
mueller@3071
    57
mueller@3071
    58
goal thy "mksch A B`nil`schA`schB = nil";
mueller@3071
    59
by (stac mksch_unfold 1);
mueller@3071
    60
by (Simp_tac 1);
mueller@3071
    61
qed"mksch_nil";
mueller@3071
    62
mueller@3071
    63
goal thy "!!x.[|x:act A;x~:act B|]  \
mueller@3071
    64
\   ==> mksch A B`(x>>tr)`schA`schB = \
wenzelm@3842
    65
\         (Takewhile (%a. a:int A)`schA) \
wenzelm@3842
    66
\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
mueller@3071
    67
\                             `schB))";
paulson@3457
    68
by (rtac trans 1);
mueller@3071
    69
by (stac mksch_unfold 1);
wenzelm@4098
    70
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
wenzelm@4098
    71
by (simp_tac (simpset() addsimps [Cons_def]) 1);
mueller@3071
    72
qed"mksch_cons1";
mueller@3071
    73
mueller@3071
    74
goal thy "!!x.[|x~:act A;x:act B|] \
mueller@3071
    75
\   ==> mksch A B`(x>>tr)`schA`schB = \
wenzelm@3842
    76
\        (Takewhile (%a. a:int B)`schB)  \
wenzelm@3842
    77
\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
mueller@3071
    78
\                            ))";
paulson@3457
    79
by (rtac trans 1);
mueller@3071
    80
by (stac mksch_unfold 1);
wenzelm@4098
    81
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
wenzelm@4098
    82
by (simp_tac (simpset() addsimps [Cons_def]) 1);
mueller@3071
    83
qed"mksch_cons2";
mueller@3071
    84
mueller@3071
    85
goal thy "!!x.[|x:act A;x:act B|] \
mueller@3071
    86
\   ==> mksch A B`(x>>tr)`schA`schB = \
wenzelm@3842
    87
\            (Takewhile (%a. a:int A)`schA) \
wenzelm@3842
    88
\         @@ ((Takewhile (%a. a:int B)`schB)  \
wenzelm@3842
    89
\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
wenzelm@3842
    90
\                            `(TL`(Dropwhile (%a. a:int B)`schB))))  \
mueller@3071
    91
\             )";
paulson@3457
    92
by (rtac trans 1);
mueller@3071
    93
by (stac mksch_unfold 1);
wenzelm@4098
    94
by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
wenzelm@4098
    95
by (simp_tac (simpset() addsimps [Cons_def]) 1);
mueller@3071
    96
qed"mksch_cons3";
mueller@3071
    97
mueller@3071
    98
val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
mueller@3071
    99
mueller@3071
   100
Addsimps compotr_simps;
mueller@3071
   101
mueller@3071
   102
mueller@3071
   103
(* ------------------------------------------------------------------ *)
mueller@3071
   104
(*                      The following lemmata aim for                 *)
mueller@3071
   105
(*               COMPOSITIONALITY   on    TRACE     Level             *)
mueller@3071
   106
(* ------------------------------------------------------------------ *)
mueller@3071
   107
mueller@3071
   108
mueller@3071
   109
(* ---------------------------------------------------------------------------- *)
mueller@3275
   110
                      section"Lemmata for ==>";                      
mueller@3071
   111
(* ---------------------------------------------------------------------------- *)
mueller@3071
   112
mueller@3071
   113
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of 
mueller@3071
   114
   the compatibility of IOA, in particular out of the condition that internals are 
mueller@3071
   115
   really hidden. *)
mueller@3071
   116
mueller@3071
   117
goal thy "(eB & ~eA --> ~A) -->       \
mueller@3071
   118
\         (A & (eA | eB)) = (eA & A)";
mueller@3071
   119
by (Fast_tac 1);
mueller@3071
   120
qed"compatibility_consequence1";
mueller@3071
   121
mueller@3071
   122
mueller@3071
   123
(* very similar to above, only the commutativity of | is used to make a slight change *)
mueller@3071
   124
mueller@3071
   125
goal thy "(eB & ~eA --> ~A) -->       \
mueller@3071
   126
\         (A & (eB | eA)) = (eA & A)";
mueller@3071
   127
by (Fast_tac 1);
mueller@3071
   128
qed"compatibility_consequence2";
mueller@3071
   129
mueller@3071
   130
mueller@3275
   131
(* ---------------------------------------------------------------------------- *)
mueller@3275
   132
                      section"Lemmata for <==";                      
mueller@3275
   133
(* ---------------------------------------------------------------------------- *)
mueller@3071
   134
mueller@3071
   135
mueller@3275
   136
(* Lemma for substitution of looping assumption in another specific assumption *) 
mueller@3275
   137
val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
mueller@3275
   138
by (cut_facts_tac [p1] 1);
paulson@3457
   139
by (etac (p2 RS subst) 1);
mueller@3275
   140
qed"subst_lemma1";
mueller@3071
   141
mueller@3275
   142
(* Lemma for substitution of looping assumption in another specific assumption *) 
mueller@3275
   143
val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
mueller@3275
   144
by (cut_facts_tac [p1] 1);
paulson@3457
   145
by (etac (p2 RS subst) 1);
mueller@3275
   146
qed"subst_lemma2";
mueller@3071
   147
mueller@3071
   148
mueller@3433
   149
goal thy "!!A B. compatible A B ==> \
mueller@3071
   150
\   ! schA schB. Forall (%x. x:act (A||B)) tr \
mueller@3071
   151
\   --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
mueller@3071
   152
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
mueller@3071
   153
by (safe_tac set_cs);
wenzelm@4098
   154
by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
mueller@3071
   155
by (case_tac "a:act A" 1);
mueller@3071
   156
by (case_tac "a:act B" 1);
mueller@3071
   157
(* a:A, a:B *)
mueller@3071
   158
by (Asm_full_simp_tac 1);
paulson@3457
   159
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   160
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
paulson@3457
   161
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   162
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
mueller@3071
   163
(* a:A,a~:B *)
mueller@3071
   164
by (Asm_full_simp_tac 1);
paulson@3457
   165
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   166
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
mueller@3071
   167
by (case_tac "a:act B" 1);
mueller@3071
   168
(* a~:A, a:B *)
mueller@3071
   169
by (Asm_full_simp_tac 1);
paulson@3457
   170
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   171
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
mueller@3071
   172
(* a~:A,a~:B *)
paulson@4477
   173
by Auto_tac;
mueller@3275
   174
qed"ForallAorB_mksch1";
mueller@3071
   175
mueller@3275
   176
bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
mueller@3071
   177
mueller@3433
   178
goal thy "!!A B. compatible B A  ==> \
mueller@3071
   179
\   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
mueller@3071
   180
\   --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
mueller@3071
   181
mueller@3071
   182
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
mueller@3071
   183
by (safe_tac set_cs);
paulson@3457
   184
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   185
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
mueller@3275
   186
                            intA_is_not_actB,int_is_act]) 1);
mueller@3071
   187
qed"ForallBnA_mksch";
mueller@3071
   188
mueller@3275
   189
bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp);
mueller@3275
   190
mueller@3275
   191
mueller@3433
   192
goal thy "!!A B. compatible A B ==> \
mueller@3071
   193
\   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
mueller@3071
   194
\   --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
mueller@3071
   195
mueller@3071
   196
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
mueller@3071
   197
by (safe_tac set_cs);
mueller@3071
   198
by (Asm_full_simp_tac 1);
paulson@3457
   199
by (rtac (Forall_Conc_impl RS mp) 1);
wenzelm@4098
   200
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
mueller@3275
   201
                       intA_is_not_actB,int_is_act]) 1);
mueller@3071
   202
qed"ForallAnB_mksch";
mueller@3071
   203
mueller@3275
   204
bind_thm ("ForallAnBmksch",ForallAnB_mksch RS spec RS spec RS mp);
mueller@3275
   205
mueller@3071
   206
mueller@3275
   207
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
mueller@3275
   208
Delsimps [FiniteConc];
mueller@3071
   209
mueller@3275
   210
goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
wenzelm@3842
   211
\   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
mueller@3275
   212
\          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
mueller@3071
   213
\          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
mueller@3071
   214
\          Forall (%x. x:ext (A||B)) tr \
mueller@3071
   215
\          --> Finite (mksch A B`tr`x`y)";
mueller@3071
   216
paulson@3457
   217
by (etac Seq_Finite_ind  1);
mueller@3071
   218
by (Asm_full_simp_tac 1);
mueller@3071
   219
(* main case *)
wenzelm@4098
   220
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@3071
   221
by (safe_tac set_cs);
mueller@3275
   222
mueller@3275
   223
(* a: act A; a: act B *)
mueller@3275
   224
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   225
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   226
back();
mueller@3275
   227
by (REPEAT (etac conjE 1));
mueller@3275
   228
(* Finite (tw iA x) and Finite (tw iB y) *)
wenzelm@4098
   229
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   230
          [not_ext_is_int_or_not_act,FiniteConc]) 1);
mueller@3275
   231
(* now for conclusion IH applicable, but assumptions have to be transformed *)
mueller@3275
   232
by (dres_inst_tac [("x","x"),
mueller@3275
   233
                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
paulson@3457
   234
by (assume_tac 1);
mueller@3275
   235
by (dres_inst_tac [("x","y"),
mueller@3275
   236
                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
paulson@3457
   237
by (assume_tac 1);
mueller@3275
   238
(* IH *)
wenzelm@4098
   239
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   240
                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3275
   241
mueller@3275
   242
(* a: act B; a~: act A *)
mueller@3275
   243
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3071
   244
mueller@3275
   245
by (REPEAT (etac conjE 1));
mueller@3275
   246
(* Finite (tw iB y) *)
wenzelm@4098
   247
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   248
          [not_ext_is_int_or_not_act,FiniteConc]) 1);
mueller@3275
   249
(* now for conclusion IH applicable, but assumptions have to be transformed *)
mueller@3275
   250
by (dres_inst_tac [("x","y"),
mueller@3275
   251
                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
paulson@3457
   252
by (assume_tac 1);
mueller@3275
   253
(* IH *)
wenzelm@4098
   254
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   255
                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3071
   256
mueller@3275
   257
(* a~: act B; a: act A *)
mueller@3275
   258
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3071
   259
mueller@3275
   260
by (REPEAT (etac conjE 1));
mueller@3275
   261
(* Finite (tw iA x) *)
wenzelm@4098
   262
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   263
          [not_ext_is_int_or_not_act,FiniteConc]) 1);
mueller@3275
   264
(* now for conclusion IH applicable, but assumptions have to be transformed *)
mueller@3275
   265
by (dres_inst_tac [("x","x"),
mueller@3275
   266
                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
paulson@3457
   267
by (assume_tac 1);
mueller@3275
   268
(* IH *)
wenzelm@4098
   269
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   270
                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3275
   271
mueller@3275
   272
(* a~: act B; a~: act A *)
wenzelm@4098
   273
by (fast_tac (claset() addSIs [ext_is_act] 
wenzelm@4098
   274
                      addss (simpset() addsimps [externals_of_par]) ) 1);
mueller@3071
   275
qed"FiniteL_mksch";
mueller@3071
   276
mueller@3275
   277
bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp);
mueller@3275
   278
 
mueller@3275
   279
Addsimps [FiniteConc];
mueller@3275
   280
mueller@3275
   281
mueller@3275
   282
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
mueller@3275
   283
Delsimps [FilterConc]; 
mueller@3275
   284
mueller@3433
   285
goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
wenzelm@3842
   286
\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
mueller@3275
   287
\    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
mueller@3275
   288
\    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
mueller@3275
   289
\                   Forall (%x. x:act B & x~:act A) y1 & \
mueller@3275
   290
\                   Finite y1 & y = (y1 @@ y2) & \
mueller@3275
   291
\                   Filter (%a. a:ext B)`y1 = bs)";
paulson@4473
   292
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
paulson@3457
   293
by (etac Seq_Finite_ind  1);
mueller@3275
   294
by (REPEAT (rtac allI 1));
mueller@3071
   295
by (rtac impI 1);
mueller@3071
   296
by (res_inst_tac [("x","nil")] exI 1);
mueller@3071
   297
by (res_inst_tac [("x","y")] exI 1);
mueller@3071
   298
by (Asm_full_simp_tac 1);
mueller@3071
   299
(* main case *)
mueller@3275
   300
by (REPEAT (rtac allI 1));
mueller@3071
   301
by (rtac impI 1);
mueller@3071
   302
by (Asm_full_simp_tac 1);
mueller@3071
   303
by (REPEAT (etac conjE 1));
mueller@3275
   304
by (Asm_full_simp_tac 1);
mueller@3275
   305
(* divide_Seq on s *)
mueller@3275
   306
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   307
by (REPEAT (etac conjE 1));
mueller@3275
   308
(* transform assumption f eB y = f B (s@z) *)
mueller@3275
   309
by (dres_inst_tac [("x","y"),
mueller@3275
   310
                   ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
paulson@3457
   311
by (assume_tac 1);
mueller@3275
   312
Addsimps [FilterConc]; 
wenzelm@4098
   313
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
mueller@3275
   314
(* apply IH *)
wenzelm@3842
   315
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
wenzelm@4098
   316
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
mueller@3275
   317
by (REPEAT (etac exE 1));
mueller@3275
   318
by (REPEAT (etac conjE 1));
mueller@3275
   319
by (Asm_full_simp_tac 1); 
mueller@3275
   320
(* for replacing IH in conclusion *)
mueller@3275
   321
by (rotate_tac ~2 1); 
mueller@3275
   322
by (Asm_full_simp_tac 1); 
mueller@3275
   323
(* instantiate y1a and y2a *)
wenzelm@3842
   324
by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
mueller@3275
   325
by (res_inst_tac [("x","y2")] exI 1);
mueller@3275
   326
(* elminate all obligations up to two depending on Conc_assoc *)
wenzelm@4098
   327
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
mueller@3275
   328
             int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
wenzelm@4098
   329
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
mueller@3275
   330
qed"reduceA_mksch1";
mueller@3275
   331
mueller@3275
   332
bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp)));
mueller@3275
   333
mueller@3275
   334
mueller@3275
   335
mueller@3275
   336
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
mueller@3275
   337
Delsimps [FilterConc]; 
mueller@3275
   338
mueller@3275
   339
mueller@3433
   340
goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
wenzelm@3842
   341
\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
mueller@3275
   342
\    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
mueller@3275
   343
\    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
mueller@3275
   344
\                   Forall (%x. x:act A & x~:act B) x1 & \
mueller@3275
   345
\                   Finite x1 & x = (x1 @@ x2) & \
mueller@3275
   346
\                   Filter (%a. a:ext A)`x1 = as)";
paulson@4473
   347
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
paulson@3457
   348
by (etac Seq_Finite_ind  1);
mueller@3275
   349
by (REPEAT (rtac allI 1));
mueller@3275
   350
by (rtac impI 1);
mueller@3275
   351
by (res_inst_tac [("x","nil")] exI 1);
mueller@3275
   352
by (res_inst_tac [("x","x")] exI 1);
mueller@3275
   353
by (Asm_full_simp_tac 1);
mueller@3275
   354
(* main case *)
mueller@3275
   355
by (REPEAT (rtac allI 1));
mueller@3275
   356
by (rtac impI 1);
mueller@3275
   357
by (Asm_full_simp_tac 1);
mueller@3275
   358
by (REPEAT (etac conjE 1));
mueller@3275
   359
by (Asm_full_simp_tac 1);
mueller@3275
   360
(* divide_Seq on s *)
mueller@3275
   361
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   362
by (REPEAT (etac conjE 1));
mueller@3275
   363
(* transform assumption f eA x = f A (s@z) *)
mueller@3275
   364
by (dres_inst_tac [("x","x"),
mueller@3275
   365
                   ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
paulson@3457
   366
by (assume_tac 1);
mueller@3275
   367
Addsimps [FilterConc]; 
wenzelm@4098
   368
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
mueller@3275
   369
(* apply IH *)
wenzelm@3842
   370
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
wenzelm@4098
   371
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
mueller@3275
   372
by (REPEAT (etac exE 1));
mueller@3275
   373
by (REPEAT (etac conjE 1));
mueller@3275
   374
by (Asm_full_simp_tac 1); 
mueller@3275
   375
(* for replacing IH in conclusion *)
mueller@3275
   376
by (rotate_tac ~2 1); 
mueller@3275
   377
by (Asm_full_simp_tac 1); 
mueller@3275
   378
(* instantiate y1a and y2a *)
wenzelm@3842
   379
by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
mueller@3275
   380
by (res_inst_tac [("x","x2")] exI 1);
mueller@3275
   381
(* elminate all obligations up to two depending on Conc_assoc *)
wenzelm@4098
   382
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
mueller@3275
   383
             int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
wenzelm@4098
   384
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
mueller@3275
   385
qed"reduceB_mksch1";
mueller@3275
   386
mueller@3275
   387
bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp)));
mueller@3071
   388
mueller@3071
   389
mueller@3071
   390
mueller@3314
   391
(*
mueller@3071
   392
mueller@3071
   393
mueller@3314
   394
goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
mueller@3314
   395
\                             y = z @@ mksch A B`tr`a`b\
mueller@3314
   396
\                             --> Finite tr";
paulson@3457
   397
by (etac Seq_Finite_ind  1);
paulson@4477
   398
by Auto_tac;
mueller@3314
   399
by (Seq_case_simp_tac "tr" 1);
mueller@3314
   400
(* tr = UU *)
wenzelm@4098
   401
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
mueller@3314
   402
(* tr = nil *)
paulson@4477
   403
by Auto_tac;
mueller@3314
   404
(* tr = Conc *)
mueller@3314
   405
ren "s ss" 1;
mueller@3314
   406
mueller@3314
   407
by (case_tac "s:act A" 1);
mueller@3314
   408
by (case_tac "s:act B" 1);
mueller@3314
   409
by (rotate_tac ~2 1);
mueller@3314
   410
by (rotate_tac ~2 2);
wenzelm@4098
   411
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
wenzelm@4098
   412
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
mueller@3314
   413
by (case_tac "s:act B" 1);
mueller@3314
   414
by (rotate_tac ~2 1);
wenzelm@4098
   415
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
wenzelm@4098
   416
by (fast_tac (claset() addSIs [ext_is_act] 
wenzelm@4098
   417
                      addss (simpset() addsimps [externals_of_par]) ) 1);
mueller@3314
   418
(* main case *)
mueller@3314
   419
by (Seq_case_simp_tac "tr" 1);
mueller@3314
   420
(* tr = UU *)
wenzelm@4098
   421
by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
paulson@4477
   422
by Auto_tac;
mueller@3314
   423
(* tr = nil ok *)
mueller@3314
   424
(* tr = Conc *)
mueller@3314
   425
by (Seq_case_simp_tac "z" 1);
mueller@3314
   426
(* z = UU ok *)
mueller@3314
   427
(* z = nil *)
mueller@3314
   428
mueller@3314
   429
(* z= Cons *)
mueller@3314
   430
mueller@3314
   431
mueller@3314
   432
by (case_tac "aaa:act A" 2);
mueller@3314
   433
by (case_tac "aaa:act B" 2);
mueller@3314
   434
by (rotate_tac ~2 2);
mueller@3314
   435
by (rotate_tac ~2 3);
mueller@3314
   436
by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
wenzelm@3842
   437
by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
mueller@3314
   438
by (eres_inst_tac [("x","sa")] allE 2);
wenzelm@4098
   439
by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
mueller@3314
   440
mueller@3314
   441
mueller@3314
   442
mueller@3314
   443
by (eres_inst_tac [("x","sa")] allE 1);
mueller@3314
   444
by (Asm_full_simp_tac 1);
mueller@3314
   445
by (case_tac "aaa:act A" 1);
mueller@3314
   446
by (case_tac "aaa:act B" 1);
mueller@3314
   447
by (rotate_tac ~2 1);
mueller@3314
   448
by (rotate_tac ~2 2);
wenzelm@4098
   449
by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
mueller@3314
   450
mueller@3314
   451
mueller@3314
   452
mueller@3314
   453
goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
mueller@3314
   454
by (Seq_case_simp_tac "y" 1);
paulson@4477
   455
by Auto_tac;
mueller@3314
   456
qed"Conc_Conc_eq";
mueller@3314
   457
mueller@3314
   458
goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
paulson@3457
   459
by (etac Seq_Finite_ind 1);
mueller@3314
   460
by (Seq_case_simp_tac "x" 1);
mueller@3314
   461
by (Seq_case_simp_tac "x" 1);
paulson@4477
   462
by Auto_tac;
mueller@3314
   463
qed"FiniteConcUU1";
mueller@3314
   464
mueller@3314
   465
goal thy "~ Finite ((x::'a Seq)@@UU)";
paulson@3457
   466
by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
paulson@4477
   467
by Auto_tac;
mueller@3314
   468
qed"FiniteConcUU";
mueller@3314
   469
mueller@3314
   470
finiteR_mksch
mueller@3314
   471
  "Finite (mksch A B`tr`x`y) --> Finite tr"
mueller@3314
   472
*)
mueller@3314
   473
mueller@3071
   474
mueller@3071
   475
 
mueller@3275
   476
(*------------------------------------------------------------------------------------- *)
mueller@3275
   477
 section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr";
mueller@3275
   478
(*                             structural induction
mueller@3275
   479
  ------------------------------------------------------------------------------------- *)
mueller@3071
   480
mueller@3275
   481
goal thy 
mueller@3433
   482
"!! A B. [| compatible A B; compatible B A;\
mueller@3275
   483
\           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
wenzelm@3842
   484
\ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
wenzelm@3842
   485
\ Forall (%x. x:ext (A||B)) tr & \
wenzelm@3842
   486
\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
wenzelm@3842
   487
\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB  \
wenzelm@3842
   488
\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
mueller@3071
   489
mueller@3071
   490
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
mueller@3071
   491
mueller@3071
   492
(* main case *) 
mueller@3071
   493
(* splitting into 4 cases according to a:A, a:B *)
wenzelm@4098
   494
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@3071
   495
by (safe_tac set_cs);
mueller@3071
   496
mueller@3071
   497
(* Case a:A, a:B *)
mueller@3071
   498
by (forward_tac [divide_Seq] 1);
mueller@3071
   499
by (forward_tac [divide_Seq] 1);
mueller@3071
   500
back();
mueller@3071
   501
by (REPEAT (etac conjE 1));
mueller@3275
   502
(* filtering internals of A in schA and of B in schB is nil *)
wenzelm@4098
   503
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   504
          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
mueller@3275
   505
           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
mueller@3071
   506
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
mueller@3071
   507
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
paulson@3457
   508
by (assume_tac 1);
mueller@3071
   509
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
paulson@3457
   510
by (assume_tac 1);
mueller@3275
   511
(* IH *)
wenzelm@4098
   512
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   513
                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3071
   514
(* Case a:B, a~:A *)
mueller@3071
   515
mueller@3071
   516
by (forward_tac [divide_Seq] 1);
mueller@3071
   517
by (REPEAT (etac conjE 1));
mueller@3071
   518
(* filtering internals of A is nil *)
wenzelm@4098
   519
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   520
          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
mueller@3275
   521
           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
mueller@3071
   522
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
mueller@3071
   523
back();
paulson@3457
   524
by (assume_tac 1);
wenzelm@4098
   525
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   526
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3071
   527
(* Case a:A, a~:B *)
mueller@3071
   528
mueller@3071
   529
by (forward_tac [divide_Seq] 1);
mueller@3071
   530
by (REPEAT (etac conjE 1));
mueller@3071
   531
(* filtering internals of A is nil *)
wenzelm@4098
   532
by (asm_full_simp_tac (simpset() addsimps 
mueller@3275
   533
          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
mueller@3275
   534
           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
mueller@3071
   535
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
paulson@3457
   536
by (assume_tac 1);
wenzelm@4098
   537
by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
mueller@3275
   538
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
mueller@3071
   539
(* Case a~:A, a~:B *)
mueller@3071
   540
wenzelm@4098
   541
by (fast_tac (claset() addSIs [ext_is_act] 
wenzelm@4098
   542
                      addss (simpset() addsimps [externals_of_par]) ) 1);
mueller@3275
   543
qed"FilterA_mksch_is_tr";
mueller@3071
   544
mueller@3071
   545
mueller@3071
   546
mueller@3314
   547
(*
mueller@3314
   548
mueller@3314
   549
***************************************************************8
mueller@3314
   550
With uncomplete take lemma rule should be reused afterwards !!!!!!!!!!!!!!!!!
mueller@3314
   551
**********************************************************************
mueller@3314
   552
mueller@3314
   553
(*---------------------------------------------------------------------------
mueller@3314
   554
              Filter of mksch(tr,schA,schB) to A is schA 
mueller@3314
   555
                             take lemma
mueller@3314
   556
  --------------------------------------------------------------------------- *)
mueller@3314
   557
mueller@3433
   558
goal thy "!! A B. [| compatible A B; compatible B A; \
mueller@3314
   559
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
wenzelm@3842
   560
\ Forall (%x. x:ext (A||B)) tr & \
wenzelm@3842
   561
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
wenzelm@3842
   562
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
wenzelm@3842
   563
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
mueller@3314
   564
\ LastActExtsch A schA & LastActExtsch B schB  \
wenzelm@3842
   565
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
mueller@3314
   566
mueller@3314
   567
by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
mueller@3314
   568
by (REPEAT (etac conjE 1));
mueller@3314
   569
mueller@3314
   570
by (case_tac "Finite s" 1);
mueller@3314
   571
mueller@3314
   572
(* both sides of this equation are nil *)
mueller@3314
   573
by (subgoal_tac "schA=nil" 1);
mueller@3314
   574
by (Asm_simp_tac 1);
mueller@3314
   575
(* first side: mksch = nil *)
wenzelm@4098
   576
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
wenzelm@4098
   577
                           simpset())) 1);
mueller@3314
   578
(* second side: schA = nil *)
mueller@3314
   579
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
mueller@3314
   580
by (Asm_simp_tac 1);
wenzelm@4098
   581
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil],
wenzelm@4098
   582
                           simpset())) 1);
mueller@3314
   583
mueller@3314
   584
(* case ~ Finite s *)
mueller@3314
   585
mueller@3314
   586
(* both sides of this equation are UU *)
mueller@3314
   587
by (subgoal_tac "schA=UU" 1);
mueller@3314
   588
by (Asm_simp_tac 1);
mueller@3314
   589
(* first side: mksch = UU *)
wenzelm@4098
   590
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
mueller@3314
   591
                                           (finiteR_mksch RS mp COMP rev_contrapos),
mueller@3314
   592
                                            ForallBnAmksch],
wenzelm@4098
   593
                           simpset())) 1);
mueller@3314
   594
(* schA = UU *)
mueller@3314
   595
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
mueller@3314
   596
by (Asm_simp_tac 1);
wenzelm@4098
   597
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU],
wenzelm@4098
   598
                           simpset())) 1);
mueller@3314
   599
mueller@3314
   600
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
mueller@3314
   601
mueller@3314
   602
by (REPEAT (etac conjE 1));
mueller@3314
   603
mueller@3314
   604
(* bring in lemma reduceA_mksch *)
mueller@3314
   605
by (forw_inst_tac [("y","schB"),("x","schA")] reduceA_mksch 1);
mueller@3314
   606
by (REPEAT (atac 1));
mueller@3314
   607
by (REPEAT (etac exE 1));
mueller@3314
   608
by (REPEAT (etac conjE 1));
mueller@3314
   609
mueller@3314
   610
(* use reduceA_mksch to rewrite conclusion *)
mueller@3314
   611
by (hyp_subst_tac 1);
mueller@3314
   612
by (Asm_full_simp_tac  1);
mueller@3314
   613
mueller@3314
   614
(* eliminate the B-only prefix *)
mueller@3314
   615
wenzelm@3842
   616
by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
paulson@3457
   617
by (etac ForallQFilterPnil 2);
paulson@3457
   618
by (assume_tac 2);
mueller@3314
   619
by (Fast_tac 2);
mueller@3314
   620
mueller@3314
   621
(* Now real recursive step follows (in y) *)
mueller@3314
   622
mueller@3314
   623
by (Asm_full_simp_tac  1);
mueller@3314
   624
by (case_tac "y:act A" 1);
mueller@3314
   625
by (case_tac "y~:act B" 1);
mueller@3314
   626
by (rotate_tac ~2 1);
mueller@3314
   627
by (Asm_full_simp_tac 1);
mueller@3314
   628
mueller@3314
   629
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
mueller@3314
   630
by (rotate_tac ~1 1);
mueller@3314
   631
by (Asm_full_simp_tac  1);
mueller@3314
   632
(* eliminate introduced subgoal 2 *)
paulson@3457
   633
by (etac ForallQFilterPnil 2);
paulson@3457
   634
by (assume_tac 2);
mueller@3314
   635
by (Fast_tac 2);
mueller@3314
   636
 
mueller@3314
   637
(* bring in divide Seq for s *)
mueller@3314
   638
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3314
   639
by (REPEAT (etac conjE 1));
mueller@3314
   640
mueller@3314
   641
(* subst divide_Seq in conclusion, but only at the righest occurence *)
mueller@3314
   642
by (res_inst_tac [("t","schA")] ssubst 1);
mueller@3314
   643
back();
mueller@3314
   644
back();
mueller@3314
   645
back();
paulson@3457
   646
by (assume_tac 1);
mueller@3314
   647
mueller@3314
   648
(* reduce trace_takes from n to strictly smaller k *)
paulson@3457
   649
by (rtac take_reduction 1);
mueller@3314
   650
mueller@3314
   651
(* f A (tw iA) = tw ~eA *)
wenzelm@4098
   652
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
mueller@3314
   653
                              not_ext_is_int_or_not_act]) 1);
paulson@3457
   654
by (rtac refl 1);
mueller@3314
   655
mueller@3314
   656
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
mueller@3314
   657
(*
mueller@3314
   658
mueller@3314
   659
nacessary anymore ???????????????? 
mueller@3314
   660
by (rotate_tac ~10 1);
mueller@3314
   661
mueller@3314
   662
*)
mueller@3314
   663
(* assumption schB *)
wenzelm@4098
   664
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
mueller@3314
   665
(* assumption schA *)
mueller@3314
   666
by (dres_inst_tac [("x","schA"),
mueller@3314
   667
                   ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
paulson@3457
   668
by (assume_tac 1);
wenzelm@4098
   669
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil]) 1);
mueller@3314
   670
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
mueller@3314
   671
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
mueller@3314
   672
by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
paulson@3457
   673
by (assume_tac 1);
mueller@3314
   674
mueller@3314
   675
FIX: problem: schA and schB are not quantified in the new take lemma version !!!
mueller@3314
   676
mueller@3314
   677
by (Asm_full_simp_tac 1);
mueller@3314
   678
mueller@3314
   679
**********************************************************************************************
mueller@3314
   680
*)
mueller@3314
   681
mueller@3314
   682
mueller@3314
   683
mueller@3275
   684
(*--------------------------------------------------------------------------- *)
mueller@3071
   685
mueller@3275
   686
     section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof";  
mueller@3275
   687
  
mueller@3275
   688
(*  --------------------------------------------------------------------------- *)
mueller@3071
   689
mueller@3071
   690
mueller@3071
   691
mueller@3433
   692
goal thy "!! A B. [| compatible A B; compatible B A; \
mueller@3275
   693
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
wenzelm@3842
   694
\ Forall (%x. x:ext (A||B)) tr & \
wenzelm@3842
   695
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
wenzelm@3842
   696
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
wenzelm@3842
   697
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
mueller@3275
   698
\ LastActExtsch A schA & LastActExtsch B schB  \
wenzelm@3842
   699
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
mueller@3071
   700
mueller@3275
   701
by (strip_tac 1);
oheimb@4042
   702
by (resolve_tac seq.take_lemmas 1);
paulson@3457
   703
by (rtac mp 1);
paulson@3457
   704
by (assume_tac 2);
mueller@3275
   705
back();back();back();back();
mueller@3275
   706
by (res_inst_tac [("x","schA")] spec 1);
mueller@3275
   707
by (res_inst_tac [("x","schB")] spec 1);
mueller@3275
   708
by (res_inst_tac [("x","tr")] spec 1);
mueller@3275
   709
by (thin_tac' 5 1);
paulson@3457
   710
by (rtac less_induct 1);
mueller@3275
   711
by (REPEAT (rtac allI 1));
mueller@3275
   712
ren "tr schB schA" 1;
mueller@3275
   713
by (strip_tac 1);
mueller@3275
   714
by (REPEAT (etac conjE 1));
mueller@3071
   715
mueller@3275
   716
by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
mueller@3275
   717
paulson@3457
   718
by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
mueller@3275
   719
by (thin_tac' 5 1);
mueller@3071
   720
mueller@3071
   721
mueller@3275
   722
by (case_tac "Finite tr" 1);
mueller@3071
   723
mueller@3275
   724
(* both sides of this equation are nil *)
mueller@3275
   725
by (subgoal_tac "schA=nil" 1);
mueller@3071
   726
by (Asm_simp_tac 1);
mueller@3275
   727
(* first side: mksch = nil *)
wenzelm@4098
   728
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
wenzelm@4098
   729
                           simpset())) 1);
mueller@3275
   730
(* second side: schA = nil *)
mueller@3071
   731
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
mueller@3071
   732
by (Asm_simp_tac 1);
wenzelm@3842
   733
by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1);
paulson@3457
   734
by (assume_tac 1);
mueller@3314
   735
by (Fast_tac 1);
mueller@3275
   736
mueller@3275
   737
(* case ~ Finite s *)
mueller@3071
   738
mueller@3275
   739
(* both sides of this equation are UU *)
mueller@3275
   740
by (subgoal_tac "schA=UU" 1);
mueller@3275
   741
by (Asm_simp_tac 1);
mueller@3275
   742
(* first side: mksch = UU *)
wenzelm@4098
   743
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
mueller@3275
   744
                                           (finiteR_mksch RS mp COMP rev_contrapos),
mueller@3275
   745
                                            ForallBnAmksch],
wenzelm@4098
   746
                           simpset())) 1);
mueller@3071
   747
(* schA = UU *)
mueller@3071
   748
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
mueller@3071
   749
by (Asm_simp_tac 1);
wenzelm@3842
   750
by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
paulson@3457
   751
by (assume_tac 1);
mueller@3314
   752
by (Fast_tac 1);
mueller@3275
   753
mueller@3275
   754
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
mueller@3275
   755
paulson@3457
   756
by (dtac divide_Seq3 1);
mueller@3071
   757
mueller@3275
   758
by (REPEAT (etac exE 1));
mueller@3275
   759
by (REPEAT (etac conjE 1));
mueller@3275
   760
by (hyp_subst_tac 1);
mueller@3071
   761
mueller@3275
   762
(* bring in lemma reduceA_mksch *)
mueller@3275
   763
by (forw_inst_tac [("x","schB"),("xa","schA"),("A","A"),("B","B")] reduceA_mksch 1);
mueller@3071
   764
by (REPEAT (atac 1));
mueller@3071
   765
by (REPEAT (etac exE 1));
mueller@3071
   766
by (REPEAT (etac conjE 1));
mueller@3071
   767
mueller@3275
   768
(* use reduceA_mksch to rewrite conclusion *)
mueller@3071
   769
by (hyp_subst_tac 1);
mueller@3071
   770
by (Asm_full_simp_tac  1);
mueller@3071
   771
mueller@3071
   772
(* eliminate the B-only prefix *)
mueller@3275
   773
wenzelm@3842
   774
by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
paulson@3457
   775
by (etac ForallQFilterPnil 2);
paulson@3457
   776
by (assume_tac 2);
mueller@3275
   777
by (Fast_tac 2);
mueller@3275
   778
mueller@3275
   779
(* Now real recursive step follows (in y) *)
mueller@3071
   780
mueller@3275
   781
by (Asm_full_simp_tac  1);
mueller@3275
   782
by (case_tac "x:act A" 1);
mueller@3275
   783
by (case_tac "x~:act B" 1);
mueller@3071
   784
by (rotate_tac ~2 1);
mueller@3275
   785
by (Asm_full_simp_tac 1);
mueller@3071
   786
mueller@3275
   787
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
mueller@3071
   788
by (rotate_tac ~1 1);
mueller@3071
   789
by (Asm_full_simp_tac  1);
mueller@3071
   790
(* eliminate introduced subgoal 2 *)
paulson@3457
   791
by (etac ForallQFilterPnil 2);
paulson@3457
   792
by (assume_tac 2);
mueller@3071
   793
by (Fast_tac 2);
mueller@3071
   794
 
mueller@3275
   795
(* bring in divide Seq for s *)
mueller@3275
   796
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   797
by (REPEAT (etac conjE 1));
mueller@3275
   798
mueller@3275
   799
(* subst divide_Seq in conclusion, but only at the righest occurence *)
mueller@3275
   800
by (res_inst_tac [("t","schA")] ssubst 1);
mueller@3275
   801
back();
mueller@3275
   802
back();
mueller@3275
   803
back();
paulson@3457
   804
by (assume_tac 1);
mueller@3275
   805
mueller@3275
   806
(* reduce trace_takes from n to strictly smaller k *)
paulson@3457
   807
by (rtac take_reduction 1);
mueller@3275
   808
mueller@3275
   809
(* f A (tw iA) = tw ~eA *)
wenzelm@4098
   810
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
mueller@3275
   811
                              not_ext_is_int_or_not_act]) 1);
paulson@3457
   812
by (rtac refl 1);
wenzelm@4098
   813
by (asm_full_simp_tac (simpset() addsimps [int_is_act,
mueller@3275
   814
                              not_ext_is_int_or_not_act]) 1);
mueller@3275
   815
by (rotate_tac ~11 1);
mueller@3275
   816
mueller@3275
   817
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
mueller@3071
   818
mueller@3275
   819
(* assumption Forall tr *)
wenzelm@4098
   820
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
mueller@3275
   821
(* assumption schB *)
wenzelm@4098
   822
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
mueller@3275
   823
by (REPEAT (etac conjE 1));
mueller@3275
   824
(* assumption schA *)
mueller@3275
   825
by (dres_inst_tac [("x","schA"),
mueller@3275
   826
                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
paulson@3457
   827
by (assume_tac 1);
wenzelm@4098
   828
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
mueller@3275
   829
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
mueller@3275
   830
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
mueller@3275
   831
by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
paulson@3457
   832
by (assume_tac 1);
mueller@3275
   833
mueller@3275
   834
(* assumption Forall schA *)
mueller@3275
   835
by (dres_inst_tac [("s","schA"),
wenzelm@3842
   836
                   ("P","Forall (%x. x:act A)")] subst 1);
paulson@3457
   837
by (assume_tac 1);
wenzelm@4098
   838
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
mueller@3275
   839
mueller@3275
   840
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
mueller@3275
   841
mueller@3275
   842
mueller@3275
   843
by (rotate_tac ~2 1);
mueller@3275
   844
by (Asm_full_simp_tac  1);
mueller@3275
   845
mueller@3275
   846
by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
mueller@3275
   847
by (rotate_tac ~1 1);
mueller@3275
   848
by (Asm_full_simp_tac  1);
mueller@3275
   849
(* eliminate introduced subgoal 2 *)
paulson@3457
   850
by (etac ForallQFilterPnil 2);
paulson@3457
   851
by (assume_tac 2);
mueller@3275
   852
by (Fast_tac 2);
mueller@3275
   853
 
mueller@3275
   854
(* bring in divide Seq for s *)
mueller@3275
   855
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
   856
by (REPEAT (etac conjE 1));
mueller@3275
   857
mueller@3275
   858
(* subst divide_Seq in conclusion, but only at the righest occurence *)
mueller@3071
   859
by (res_inst_tac [("t","schA")] ssubst 1);
mueller@3071
   860
back();
mueller@3071
   861
back();
mueller@3071
   862
back();
paulson@3457
   863
by (assume_tac 1);
mueller@3275
   864
mueller@3275
   865
(* f A (tw iA) = tw ~eA *)
wenzelm@4098
   866
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
mueller@3275
   867
                              not_ext_is_int_or_not_act]) 1);
mueller@3071
   868
mueller@3275
   869
(* rewrite assumption forall and schB *)
mueller@3275
   870
by (rotate_tac 13 1);
wenzelm@4098
   871
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
mueller@3275
   872
mueller@3275
   873
(* divide_Seq for schB2 *)
mueller@3275
   874
by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
mueller@3071
   875
by (REPEAT (etac conjE 1));
mueller@3071
   876
(* assumption schA *)
mueller@3071
   877
by (dres_inst_tac [("x","schA"),
mueller@3275
   878
                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
paulson@3457
   879
by (assume_tac 1);
wenzelm@4098
   880
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
mueller@3275
   881
mueller@3275
   882
(* f A (tw iB schB2) = nil *) 
wenzelm@4098
   883
by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
mueller@3275
   884
             FilterPTakewhileQnil,intA_is_not_actB]) 1);
mueller@3275
   885
mueller@3275
   886
mueller@3275
   887
(* reduce trace_takes from n to strictly smaller k *)
paulson@3457
   888
by (rtac take_reduction 1);
paulson@3457
   889
by (rtac refl 1);
paulson@3457
   890
by (rtac refl 1);
mueller@3275
   891
mueller@3275
   892
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
mueller@3275
   893
mueller@3275
   894
(* assumption schB *)
mueller@3275
   895
by (dres_inst_tac [("x","y2"),
mueller@3275
   896
                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
paulson@3457
   897
by (assume_tac 1);
wenzelm@4098
   898
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
mueller@3275
   899
mueller@3275
   900
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
mueller@3275
   901
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
mueller@3275
   902
by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
paulson@3457
   903
by (assume_tac 1);
mueller@3275
   904
by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
mueller@3275
   905
mueller@3275
   906
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
wenzelm@4098
   907
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
mueller@3275
   908
mueller@3275
   909
(* case x~:A & x:B  *)
mueller@3275
   910
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
mueller@3275
   911
by (case_tac "x:act B" 1);
mueller@3275
   912
by (Fast_tac 1);
mueller@3275
   913
mueller@3275
   914
(* case x~:A & x~:B  *)
mueller@3275
   915
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
mueller@3275
   916
by (rotate_tac ~9 1);
mueller@3275
   917
(* reduce forall assumption from tr to (x>>rs) *)
wenzelm@4098
   918
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
mueller@3071
   919
by (REPEAT (etac conjE 1));
wenzelm@4098
   920
by (fast_tac (claset() addSIs [ext_is_act]) 1);
mueller@3275
   921
mueller@3275
   922
qed"FilterAmksch_is_schA";
mueller@3275
   923
mueller@3275
   924
mueller@3275
   925
mueller@3275
   926
(*---------------------------------------------------------------------------  *)
mueller@3275
   927
mueller@3275
   928
   section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof";
mueller@3275
   929
                
mueller@3275
   930
(*  --------------------------------------------------------------------------- *)
mueller@3275
   931
mueller@3275
   932
mueller@3275
   933
mueller@3433
   934
goal thy "!! A B. [| compatible A B; compatible B A; \
mueller@3275
   935
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
wenzelm@3842
   936
\ Forall (%x. x:ext (A||B)) tr & \
wenzelm@3842
   937
\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
wenzelm@3842
   938
\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
wenzelm@3842
   939
\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
mueller@3275
   940
\ LastActExtsch A schA & LastActExtsch B schB  \
wenzelm@3842
   941
\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
mueller@3275
   942
mueller@3275
   943
by (strip_tac 1);
oheimb@4042
   944
by (resolve_tac seq.take_lemmas 1);
paulson@3457
   945
by (rtac mp 1);
paulson@3457
   946
by (assume_tac 2);
mueller@3275
   947
back();back();back();back();
mueller@3275
   948
by (res_inst_tac [("x","schA")] spec 1);
mueller@3275
   949
by (res_inst_tac [("x","schB")] spec 1);
mueller@3275
   950
by (res_inst_tac [("x","tr")] spec 1);
mueller@3275
   951
by (thin_tac' 5 1);
paulson@3457
   952
by (rtac less_induct 1);
mueller@3275
   953
by (REPEAT (rtac allI 1));
mueller@3275
   954
ren "tr schB schA" 1;
mueller@3275
   955
by (strip_tac 1);
mueller@3275
   956
by (REPEAT (etac conjE 1));
mueller@3275
   957
mueller@3275
   958
by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
mueller@3275
   959
paulson@3457
   960
by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
mueller@3275
   961
by (thin_tac' 5 1);
mueller@3275
   962
mueller@3275
   963
mueller@3275
   964
by (case_tac "Finite tr" 1);
mueller@3275
   965
mueller@3275
   966
(* both sides of this equation are nil *)
mueller@3275
   967
by (subgoal_tac "schB=nil" 1);
mueller@3275
   968
by (Asm_simp_tac 1);
mueller@3275
   969
(* first side: mksch = nil *)
wenzelm@4098
   970
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
wenzelm@4098
   971
                           simpset())) 1);
mueller@3275
   972
(* second side: schA = nil *)
mueller@3275
   973
by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
mueller@3275
   974
by (Asm_simp_tac 1);
wenzelm@3842
   975
by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1);
paulson@3457
   976
by (assume_tac 1);
mueller@3314
   977
by (Fast_tac 1);
mueller@3275
   978
mueller@3275
   979
(* case ~ Finite tr *)
mueller@3275
   980
mueller@3275
   981
(* both sides of this equation are UU *)
mueller@3275
   982
by (subgoal_tac "schB=UU" 1);
mueller@3275
   983
by (Asm_simp_tac 1);
mueller@3275
   984
(* first side: mksch = UU *)
wenzelm@4098
   985
by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
mueller@3275
   986
                                           (finiteR_mksch RS mp COMP rev_contrapos),
mueller@3275
   987
                                            ForallAnBmksch],
wenzelm@4098
   988
                           simpset())) 1);
mueller@3275
   989
(* schA = UU *)
mueller@3275
   990
by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
mueller@3275
   991
by (Asm_simp_tac 1);
wenzelm@3842
   992
by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1);
paulson@3457
   993
by (assume_tac 1);
mueller@3314
   994
by (Fast_tac 1);
mueller@3275
   995
mueller@3275
   996
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
mueller@3275
   997
paulson@3457
   998
by (dtac divide_Seq3 1);
mueller@3275
   999
mueller@3275
  1000
by (REPEAT (etac exE 1));
mueller@3275
  1001
by (REPEAT (etac conjE 1));
mueller@3275
  1002
by (hyp_subst_tac 1);
mueller@3275
  1003
mueller@3275
  1004
(* bring in lemma reduceB_mksch *)
mueller@3275
  1005
by (forw_inst_tac [("y","schB"),("x","schA"),("A","A"),("B","B")] reduceB_mksch 1);
mueller@3275
  1006
by (REPEAT (atac 1));
mueller@3275
  1007
by (REPEAT (etac exE 1));
mueller@3275
  1008
by (REPEAT (etac conjE 1));
mueller@3275
  1009
mueller@3275
  1010
(* use reduceB_mksch to rewrite conclusion *)
mueller@3275
  1011
by (hyp_subst_tac 1);
mueller@3275
  1012
by (Asm_full_simp_tac  1);
mueller@3275
  1013
mueller@3275
  1014
(* eliminate the A-only prefix *)
mueller@3275
  1015
wenzelm@3842
  1016
by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
paulson@3457
  1017
by (etac ForallQFilterPnil 2);
paulson@3457
  1018
by (assume_tac 2);
mueller@3275
  1019
by (Fast_tac 2);
mueller@3275
  1020
mueller@3275
  1021
(* Now real recursive step follows (in x) *)
mueller@3275
  1022
mueller@3275
  1023
by (Asm_full_simp_tac  1);
mueller@3275
  1024
by (case_tac "x:act B" 1);
mueller@3275
  1025
by (case_tac "x~:act A" 1);
mueller@3275
  1026
by (rotate_tac ~2 1);
mueller@3071
  1027
by (Asm_full_simp_tac 1);
mueller@3071
  1028
mueller@3275
  1029
by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
mueller@3071
  1030
by (rotate_tac ~1 1);
mueller@3071
  1031
by (Asm_full_simp_tac  1);
mueller@3071
  1032
(* eliminate introduced subgoal 2 *)
paulson@3457
  1033
by (etac ForallQFilterPnil 2);
paulson@3457
  1034
by (assume_tac 2);
mueller@3071
  1035
by (Fast_tac 2);
mueller@3071
  1036
 
mueller@3275
  1037
(* bring in divide Seq for s *)
mueller@3275
  1038
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3275
  1039
by (REPEAT (etac conjE 1));
mueller@3071
  1040
mueller@3275
  1041
(* subst divide_Seq in conclusion, but only at the righest occurence *)
mueller@3275
  1042
by (res_inst_tac [("t","schB")] ssubst 1);
mueller@3071
  1043
back();
mueller@3071
  1044
back();
mueller@3071
  1045
back();
paulson@3457
  1046
by (assume_tac 1);
mueller@3275
  1047
mueller@3275
  1048
(* reduce trace_takes from n to strictly smaller k *)
paulson@3457
  1049
by (rtac take_reduction 1);
mueller@3275
  1050
mueller@3275
  1051
(* f B (tw iB) = tw ~eB *)
wenzelm@4098
  1052
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
mueller@3275
  1053
                              not_ext_is_int_or_not_act]) 1);
paulson@3457
  1054
by (rtac refl 1);
wenzelm@4098
  1055
by (asm_full_simp_tac (simpset() addsimps [int_is_act,
mueller@3275
  1056
                              not_ext_is_int_or_not_act]) 1);
mueller@3275
  1057
by (rotate_tac ~11 1);
mueller@3275
  1058
mueller@3275
  1059
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
mueller@3275
  1060
mueller@3275
  1061
(* assumption Forall tr *)
wenzelm@4098
  1062
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
mueller@3275
  1063
(* assumption schA *)
wenzelm@4098
  1064
by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
mueller@3071
  1065
by (REPEAT (etac conjE 1));
mueller@3275
  1066
(* assumption schB *)
mueller@3275
  1067
by (dres_inst_tac [("x","schB"),
mueller@3275
  1068
                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
paulson@3457
  1069
by (assume_tac 1);
wenzelm@4098
  1070
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
mueller@3275
  1071
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
mueller@3275
  1072
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
mueller@3275
  1073
by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
paulson@3457
  1074
by (assume_tac 1);
mueller@3275
  1075
mueller@3275
  1076
(* assumption Forall schB *)
mueller@3275
  1077
by (dres_inst_tac [("s","schB"),
wenzelm@3842
  1078
                   ("P","Forall (%x. x:act B)")] subst 1);
paulson@3457
  1079
by (assume_tac 1);
wenzelm@4098
  1080
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
mueller@3275
  1081
mueller@3275
  1082
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
mueller@3275
  1083
mueller@3275
  1084
mueller@3275
  1085
by (rotate_tac ~2 1);
mueller@3275
  1086
by (Asm_full_simp_tac  1);
mueller@3275
  1087
mueller@3275
  1088
by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
mueller@3275
  1089
by (rotate_tac ~1 1);
mueller@3275
  1090
by (Asm_full_simp_tac  1);
mueller@3275
  1091
(* eliminate introduced subgoal 2 *)
paulson@3457
  1092
by (etac ForallQFilterPnil 2);
paulson@3457
  1093
by (assume_tac 2);
mueller@3275
  1094
by (Fast_tac 2);
mueller@3275
  1095
 
mueller@3275
  1096
(* bring in divide Seq for s *)
mueller@3275
  1097
by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
mueller@3071
  1098
by (REPEAT (etac conjE 1));
mueller@3071
  1099
mueller@3275
  1100
(* subst divide_Seq in conclusion, but only at the righest occurence *)
mueller@3275
  1101
by (res_inst_tac [("t","schB")] ssubst 1);
mueller@3275
  1102
back();
mueller@3275
  1103
back();
mueller@3275
  1104
back();
paulson@3457
  1105
by (assume_tac 1);
mueller@3275
  1106
mueller@3275
  1107
(* f B (tw iB) = tw ~eB *)
wenzelm@4098
  1108
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
mueller@3275
  1109
                              not_ext_is_int_or_not_act]) 1);
mueller@3275
  1110
mueller@3275
  1111
(* rewrite assumption forall and schB *)
mueller@3275
  1112
by (rotate_tac 13 1);
wenzelm@4098
  1113
by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
mueller@3275
  1114
mueller@3275
  1115
(* divide_Seq for schB2 *)
mueller@3275
  1116
by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
mueller@3275
  1117
by (REPEAT (etac conjE 1));
mueller@3275
  1118
(* assumption schA *)
mueller@3275
  1119
by (dres_inst_tac [("x","schB"),
mueller@3275
  1120
                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
paulson@3457
  1121
by (assume_tac 1);
wenzelm@4098
  1122
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
mueller@3275
  1123
mueller@3275
  1124
(* f B (tw iA schA2) = nil *) 
wenzelm@4098
  1125
by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
mueller@3275
  1126
             FilterPTakewhileQnil,intA_is_not_actB]) 1);
mueller@3275
  1127
mueller@3275
  1128
mueller@3275
  1129
(* reduce trace_takes from n to strictly smaller k *)
paulson@3457
  1130
by (rtac take_reduction 1);
paulson@3457
  1131
by (rtac refl 1);
paulson@3457
  1132
by (rtac refl 1);
mueller@3275
  1133
mueller@3275
  1134
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
mueller@3275
  1135
mueller@3275
  1136
(* assumption schA *)
mueller@3275
  1137
by (dres_inst_tac [("x","x2"),
mueller@3275
  1138
                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
paulson@3457
  1139
by (assume_tac 1);
wenzelm@4098
  1140
by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
mueller@3275
  1141
mueller@3275
  1142
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
mueller@3275
  1143
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
mueller@3275
  1144
by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
paulson@3457
  1145
by (assume_tac 1);
mueller@3275
  1146
by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
mueller@3275
  1147
mueller@3275
  1148
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
wenzelm@4098
  1149
by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
mueller@3275
  1150
mueller@3275
  1151
(* case x~:B & x:A  *)
mueller@3071
  1152
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
mueller@3275
  1153
by (case_tac "x:act A" 1);
mueller@3071
  1154
by (Fast_tac 1);
mueller@3071
  1155
mueller@3275
  1156
(* case x~:B & x~:A  *)
mueller@3275
  1157
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
mueller@3275
  1158
by (rotate_tac ~9 1);
mueller@3275
  1159
(* reduce forall assumption from tr to (x>>rs) *)
wenzelm@4098
  1160
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
mueller@3071
  1161
by (REPEAT (etac conjE 1));
wenzelm@4098
  1162
by (fast_tac (claset() addSIs [ext_is_act]) 1);
mueller@3071
  1163
mueller@3275
  1164
qed"FilterBmksch_is_schB";
mueller@3071
  1165
mueller@3071
  1166
mueller@3071
  1167
mueller@3071
  1168
(* ------------------------------------------------------------------ *)
mueller@3275
  1169
         section"COMPOSITIONALITY on TRACE Level -- Main Theorem";
mueller@3071
  1170
(* ------------------------------------------------------------------ *)
mueller@3071
  1171
 
mueller@3071
  1172
goal thy 
mueller@3521
  1173
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
mueller@3071
  1174
\           is_asig(asig_of A); is_asig(asig_of B)|] \
mueller@3275
  1175
\       ==>  tr: traces(A||B) = \
wenzelm@3842
  1176
\            (Filter (%a. a:act A)`tr : traces A &\
wenzelm@3842
  1177
\             Filter (%a. a:act B)`tr : traces B &\
mueller@3275
  1178
\             Forall (%x. x:ext(A||B)) tr)";
mueller@3071
  1179
wenzelm@4098
  1180
by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
mueller@3071
  1181
by (safe_tac set_cs);
mueller@3071
  1182
 
mueller@3071
  1183
(* ==> *) 
mueller@3071
  1184
(* There is a schedule of A *)
wenzelm@3842
  1185
by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
wenzelm@4098
  1186
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
wenzelm@4098
  1187
by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
mueller@3071
  1188
                  externals_of_par,ext1_ext2_is_not_act1]) 1);
mueller@3071
  1189
(* There is a schedule of B *)
wenzelm@3842
  1190
by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
wenzelm@4098
  1191
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
wenzelm@4098
  1192
by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
mueller@3071
  1193
                  externals_of_par,ext1_ext2_is_not_act2]) 1);
mueller@3071
  1194
(* Traces of A||B have only external actions from A or B *)  
paulson@3457
  1195
by (rtac ForallPFilterP 1);
mueller@3071
  1196
mueller@3071
  1197
(* <== *)
mueller@3071
  1198
mueller@3275
  1199
(* replace schA and schB by Cut(schA) and Cut(schB) *)
mueller@3071
  1200
by (dtac exists_LastActExtsch 1);
paulson@3457
  1201
by (assume_tac 1);
mueller@3071
  1202
by (dtac exists_LastActExtsch 1);
paulson@3457
  1203
by (assume_tac 1);
mueller@3071
  1204
by (REPEAT (etac exE 1));
mueller@3071
  1205
by (REPEAT (etac conjE 1));
mueller@3275
  1206
(* Schedules of A(B) have only actions of A(B) *)
paulson@3457
  1207
by (dtac scheds_in_sig 1);
paulson@3457
  1208
by (assume_tac 1);
paulson@3457
  1209
by (dtac scheds_in_sig 1);
paulson@3457
  1210
by (assume_tac 1);
mueller@3071
  1211
mueller@3275
  1212
ren "h1 h2 schA schB" 1;
mueller@3071
  1213
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
mueller@3071
  1214
   we need here *)
mueller@3275
  1215
by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
mueller@3071
  1216
mueller@3071
  1217
(* External actions of mksch are just the oracle *)
wenzelm@4098
  1218
by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
mueller@3071
  1219
mueller@3071
  1220
(* mksch is a schedule -- use compositionality on sch-level *)
wenzelm@4098
  1221
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 1);
wenzelm@4098
  1222
by (asm_full_simp_tac (simpset() addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
paulson@3457
  1223
by (etac ForallAorB_mksch 1);
paulson@3457
  1224
by (etac ForallPForallQ 1);
paulson@3457
  1225
by (etac ext_is_act 1);
mueller@3275
  1226
qed"compositionality_tr";
mueller@3071
  1227
mueller@3071
  1228
mueller@3071
  1229
mueller@3521
  1230
(* ------------------------------------------------------------------ *)
mueller@3521
  1231
(*           COMPOSITIONALITY   on    TRACE         Level             *)
mueller@3521
  1232
(*                            For Modules                             *)
mueller@3521
  1233
(* ------------------------------------------------------------------ *)
mueller@3521
  1234
mueller@3521
  1235
goalw thy [Traces_def,par_traces_def]
mueller@3521
  1236
mueller@3521
  1237
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
mueller@3521
  1238
\           is_asig(asig_of A); is_asig(asig_of B)|] \
mueller@3521
  1239
\==> Traces (A||B) = par_traces (Traces A) (Traces B)";
mueller@3521
  1240
wenzelm@4098
  1241
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
wenzelm@4423
  1242
by (rtac set_ext 1);
wenzelm@4098
  1243
by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
mueller@3521
  1244
qed"compositionality_tr_modules";
mueller@3071
  1245
mueller@3071
  1246
mueller@3071
  1247
mueller@3071
  1248
mueller@3071
  1249
mueller@3071
  1250
mueller@3521
  1251