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