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