src/HOLCF/IOA/meta_theory/CompoTraces.thy
author wenzelm
Wed, 19 Mar 2008 22:47:35 +0100
changeset 26339 7825c83c9eff
parent 19741 f65265d71426
child 26359 6d437bde2f1d
permissions -rw-r--r--
eliminated change_claset/simpset;
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 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   203
apply (tactic "safe_tac set_cs")
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 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   230
apply (tactic "safe_tac set_cs")
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 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   239
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   240
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   241
apply (rule Forall_Conc_impl [THEN mp])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   242
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   243
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   244
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   245
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   246
declare FiniteConc [simp del]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   247
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   248
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
   249
    ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   250
           Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   251
           Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   252
           Forall (%x. x:ext (A||B)) tr  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   253
           --> Finite (mksch A B$tr$x$y)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   254
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   255
apply (erule Seq_Finite_ind)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   256
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   257
(* main case *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   258
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   259
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   260
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   261
(* a: act A; a: act B *)
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
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   264
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   265
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   266
(* Finite (tw iA x) and Finite (tw iB y) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   267
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   268
(* now for conclusion IH applicable, but assumptions have to be transformed *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   269
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
   270
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   271
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
   272
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   273
(* IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   274
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   275
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   276
(* a: act B; a~: act A *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   277
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   278
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   279
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   280
(* Finite (tw iB y) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   281
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   282
(* now for conclusion IH applicable, but assumptions have to be transformed *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   283
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
   284
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   285
(* IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   286
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   287
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   288
(* a~: act B; a: act A *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   289
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   290
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   291
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   292
(* Finite (tw iA x) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   293
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   294
(* now for conclusion IH applicable, but assumptions have to be transformed *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   295
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
   296
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   297
(* IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   298
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   299
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   300
(* a~: act B; a~: act A *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   301
apply (fastsimp intro!: ext_is_act simp: externals_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   302
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   303
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   304
declare FiniteConc [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   305
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   306
declare FilterConc [simp del]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   307
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   308
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
   309
 ! 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
   310
     Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   311
     --> (? 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
   312
                    Forall (%x. x:act B & x~:act A) y1 &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   313
                    Finite y1 & y = (y1 @@ y2) &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   314
                    Filter (%a. a:ext B)$y1 = bs)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   315
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   316
apply (erule Seq_Finite_ind)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   317
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   318
apply (rule impI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   319
apply (rule_tac x = "nil" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   320
apply (rule_tac x = "y" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   321
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   322
(* main case *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   323
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   324
apply (rule impI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   325
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   326
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   327
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   328
(* divide_Seq on s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   329
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   330
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   331
(* transform assumption f eB y = f B (s@z) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   332
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
   333
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   334
apply (simp add: not_ext_is_int_or_not_act FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   335
(* apply IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   336
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   337
apply (simp add: ForallTL ForallDropwhile FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   338
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   339
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   340
apply (simp add: FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   341
(* for replacing IH in conclusion *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   342
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   343
(* instantiate y1a and y2a *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   344
apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   345
apply (rule_tac x = "y2" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   346
(* elminate all obligations up to two depending on Conc_assoc *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   347
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
   348
apply (simp (no_asm) add: Conc_assoc FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   349
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   350
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   351
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   352
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   353
declare FilterConc [simp del]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   354
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   355
lemma reduceB_mksch1 [rule_format]:
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   356
" [| 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
   357
 ! 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
   358
     Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   359
     --> (? 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
   360
                    Forall (%x. x:act A & x~:act B) x1 &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   361
                    Finite x1 & x = (x1 @@ x2) &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   362
                    Filter (%a. a:ext A)$x1 = a_s)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   363
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   364
apply (erule Seq_Finite_ind)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   365
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   366
apply (rule impI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   367
apply (rule_tac x = "nil" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   368
apply (rule_tac x = "x" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   369
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   370
(* main case *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   371
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   372
apply (rule impI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   373
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   374
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   375
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   376
(* divide_Seq on s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   377
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   378
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   379
(* transform assumption f eA x = f A (s@z) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   380
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
   381
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   382
apply (simp add: not_ext_is_int_or_not_act FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   383
(* apply IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   384
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   385
apply (simp add: ForallTL ForallDropwhile FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   386
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   387
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   388
apply (simp add: FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   389
(* for replacing IH in conclusion *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   390
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   391
(* instantiate y1a and y2a *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   392
apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   393
apply (rule_tac x = "x2" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   394
(* elminate all obligations up to two depending on Conc_assoc *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   395
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
   396
apply (simp (no_asm) add: Conc_assoc FilterConc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   397
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   398
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   399
lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   400
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   401
declare FilterConc [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   402
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   403
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   404
subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   405
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   406
lemma FilterA_mksch_is_tr: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   407
"!! A B. [| compatible A B; compatible B A; 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   408
            is_asig(asig_of A); is_asig(asig_of B) |] ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   409
  ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   410
  Forall (%x. x:ext (A||B)) tr &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   411
  Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   412
  Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   413
  --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   414
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   415
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
   416
(* main case *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   417
(* splitting into 4 cases according to a:A, a:B *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   418
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   419
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   420
(* Case a:A, a:B *)
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
apply (frule divide_Seq)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   423
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   424
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   425
(* filtering internals of A in schA and of B in schB is nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   426
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
   427
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   428
apply (drule_tac x = "schA" in subst_lemma1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   429
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   430
apply (drule_tac x = "schB" in subst_lemma1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   431
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   432
(* IH *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   433
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   434
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   435
(* Case a:A, a~:B *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   436
apply (frule divide_Seq)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   437
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   438
(* filtering internals of A is nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   439
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
   440
apply (drule_tac x = "schA" in subst_lemma1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   441
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   442
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   443
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   444
(* Case a:B, a~:A *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   445
apply (frule divide_Seq)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   446
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   447
(* filtering internals of A is nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   448
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
   449
apply (drule_tac x = "schB" in subst_lemma1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   450
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   451
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   452
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   453
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   454
(* Case a~:A, a~:B *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   455
apply (fastsimp intro!: ext_is_act simp: externals_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   456
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   457
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   458
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   459
subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   460
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   461
lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   462
  is_asig(asig_of A); is_asig(asig_of B) |] ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   463
  Forall (%x. x:ext (A||B)) tr &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   464
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   465
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   466
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   467
  LastActExtsch A schA & LastActExtsch B schB   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   468
  --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   469
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   470
apply (rule seq.take_lemmas)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   471
apply (rule mp)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   472
prefer 2 apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   473
back back back back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   474
apply (rule_tac x = "schA" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   475
apply (rule_tac x = "schB" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   476
apply (rule_tac x = "tr" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   477
apply (tactic "thin_tac' 5 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   478
apply (rule nat_less_induct)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   479
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   480
apply (rename_tac tr schB schA)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   481
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   482
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   483
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   484
apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   485
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   486
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   487
apply (tactic "thin_tac' 5 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   488
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   489
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   490
apply (case_tac "Finite tr")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   491
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   492
(* both sides of this equation are nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   493
apply (subgoal_tac "schA=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   494
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   495
(* first side: mksch = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   496
apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   497
(* second side: schA = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   498
apply (erule_tac A = "A" in LastActExtimplnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   499
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   500
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   501
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   502
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   503
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   504
(* case ~ Finite s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   505
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   506
(* both sides of this equation are UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   507
apply (subgoal_tac "schA=UU")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   508
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   509
(* first side: mksch = UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   510
apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   511
(* schA = UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   512
apply (erule_tac A = "A" in LastActExtimplUU)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   513
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   514
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   515
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   516
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   517
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   518
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   519
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   520
apply (drule divide_Seq3)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   521
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   522
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   523
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   524
apply hypsubst
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   525
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   526
(* bring in lemma reduceA_mksch *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   527
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
   528
apply assumption+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   529
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   530
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   531
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   532
(* use reduceA_mksch to rewrite conclusion *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   533
apply hypsubst
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   534
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   535
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   536
(* eliminate the B-only prefix *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   537
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   538
apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   539
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   540
prefer 2 apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   541
prefer 2 apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   542
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   543
(* Now real recursive step follows (in y) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   544
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   545
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   546
apply (case_tac "x:act A")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   547
apply (case_tac "x~:act B")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   548
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   549
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   550
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   551
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   552
apply (rotate_tac -1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   553
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   554
(* eliminate introduced subgoal 2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   555
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   556
prefer 2 apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   557
prefer 2 apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   558
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   559
(* bring in divide Seq for s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   560
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   561
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   562
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   563
(* subst divide_Seq in conclusion, but only at the righest occurence *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   564
apply (rule_tac t = "schA" in ssubst)
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
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   568
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   569
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   570
(* reduce trace_takes from n to strictly smaller k *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   571
apply (rule take_reduction)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   572
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   573
(* f A (tw iA) = tw ~eA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   574
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   575
apply (rule refl)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   576
apply (simp add: int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   577
apply (rotate_tac -11)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   578
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   579
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   580
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   581
(* assumption Forall tr *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   582
(* assumption schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   583
apply (simp add: Forall_Conc ext_and_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   584
(* assumption schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   585
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
   586
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   587
apply (simp add: int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   588
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   589
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   590
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   591
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   592
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   593
(* assumption Forall schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   594
apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   595
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   596
apply (simp add: ForallPTakewhileQ int_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   597
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   598
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   599
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   600
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   601
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   602
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   603
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   604
apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   605
apply (rotate_tac -1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   606
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   607
(* eliminate introduced subgoal 2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   608
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   609
prefer 2 apply (assumption)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   610
prefer 2 apply (fast)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   611
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   612
(* bring in divide Seq for s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   613
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   614
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   615
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   616
(* subst divide_Seq in conclusion, but only at the righest occurence *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   617
apply (rule_tac t = "schA" in ssubst)
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
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   621
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   622
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   623
(* f A (tw iA) = tw ~eA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   624
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   625
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   626
(* rewrite assumption forall and schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   627
apply (rotate_tac 13)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   628
apply (simp add: ext_and_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   629
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   630
(* divide_Seq for schB2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   631
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
   632
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   633
(* assumption schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   634
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
   635
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   636
apply (simp add: int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   637
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   638
(* f A (tw iB schB2) = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   639
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
   640
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   641
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   642
(* reduce trace_takes from n to strictly smaller k *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   643
apply (rule take_reduction)
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
apply (rule refl)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   646
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   647
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   648
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   649
(* assumption schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   650
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
   651
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   652
apply (simp add: intA_is_not_actB int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   653
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   654
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   655
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   656
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   657
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   658
apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   659
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   660
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   661
apply (simp add: ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   662
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   663
(* case x~:A & x:B  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   664
(* 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
   665
apply (case_tac "x:act B")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   666
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   667
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   668
(* case x~:A & x~:B  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   669
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   670
apply (rotate_tac -9)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   671
(* reduce forall assumption from tr to (x>>rs) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   672
apply (simp add: externals_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   673
apply (fast intro!: ext_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   674
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   675
done
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
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   679
subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   680
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   681
lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   682
  is_asig(asig_of A); is_asig(asig_of B) |] ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   683
  Forall (%x. x:ext (A||B)) tr &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   684
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   685
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   686
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   687
  LastActExtsch A schA & LastActExtsch B schB   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   688
  --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   689
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   690
apply (rule seq.take_lemmas)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   691
apply (rule mp)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   692
prefer 2 apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   693
back back back back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   694
apply (rule_tac x = "schA" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   695
apply (rule_tac x = "schB" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   696
apply (rule_tac x = "tr" in spec)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   697
apply (tactic "thin_tac' 5 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   698
apply (rule nat_less_induct)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   699
apply (rule allI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   700
apply (rename_tac tr schB schA)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   701
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   702
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   703
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   704
apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   705
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   706
apply (rule seq_take_lemma [THEN iffD2, THEN spec])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   707
apply (tactic "thin_tac' 5 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   708
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   709
apply (case_tac "Finite tr")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   710
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   711
(* both sides of this equation are nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   712
apply (subgoal_tac "schB=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   713
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   714
(* first side: mksch = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   715
apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   716
(* second side: schA = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   717
apply (erule_tac A = "B" in LastActExtimplnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   718
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   719
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   720
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   721
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   722
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   723
(* case ~ Finite tr *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   724
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   725
(* both sides of this equation are UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   726
apply (subgoal_tac "schB=UU")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   727
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   728
(* first side: mksch = UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   729
apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   730
(* schA = UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   731
apply (erule_tac A = "B" in LastActExtimplUU)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   732
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   733
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   734
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   735
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   736
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   737
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   738
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   739
apply (drule divide_Seq3)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   740
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   741
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   742
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   743
apply hypsubst
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   744
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   745
(* bring in lemma reduceB_mksch *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   746
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
   747
apply assumption+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   748
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   749
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   750
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   751
(* use reduceB_mksch to rewrite conclusion *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   752
apply hypsubst
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   753
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   754
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   755
(* eliminate the A-only prefix *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   756
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   757
apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   758
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   759
prefer 2 apply (assumption)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   760
prefer 2 apply (fast)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   761
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   762
(* Now real recursive step follows (in x) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   763
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   764
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   765
apply (case_tac "x:act B")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   766
apply (case_tac "x~:act A")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   767
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   768
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   769
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   770
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   771
apply (rotate_tac -1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   772
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   773
(* eliminate introduced subgoal 2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   774
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   775
prefer 2 apply (assumption)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   776
prefer 2 apply (fast)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   777
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   778
(* bring in divide Seq for s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   779
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   780
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   781
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   782
(* subst divide_Seq in conclusion, but only at the righest occurence *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   783
apply (rule_tac t = "schB" in ssubst)
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
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   787
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   788
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   789
(* reduce trace_takes from n to strictly smaller k *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   790
apply (rule take_reduction)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   791
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   792
(* f B (tw iB) = tw ~eB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   793
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   794
apply (rule refl)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   795
apply (simp add: int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   796
apply (rotate_tac -11)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   797
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   798
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   799
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   800
(* assumption schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   801
apply (simp add: Forall_Conc ext_and_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   802
(* assumption schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   803
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
   804
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   805
apply (simp add: int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   806
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   807
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   808
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   809
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   810
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   811
(* assumption Forall schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   812
apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   813
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   814
apply (simp add: ForallPTakewhileQ int_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   815
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   816
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   817
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   818
apply (rotate_tac -2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   819
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   820
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   821
apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   822
apply (rotate_tac -1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   823
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   824
(* eliminate introduced subgoal 2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   825
apply (erule_tac [2] ForallQFilterPnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   826
prefer 2 apply (assumption)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   827
prefer 2 apply (fast)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   828
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   829
(* bring in divide Seq for s *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   830
apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   831
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   832
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   833
(* subst divide_Seq in conclusion, but only at the righest occurence *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   834
apply (rule_tac t = "schB" in ssubst)
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
back
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   838
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   839
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   840
(* f B (tw iB) = tw ~eB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   841
apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   842
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   843
(* rewrite assumption forall and schB *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   844
apply (rotate_tac 13)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   845
apply (simp add: ext_and_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   846
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   847
(* divide_Seq for schB2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   848
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
   849
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   850
(* assumption schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   851
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
   852
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   853
apply (simp add: int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   854
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   855
(* f B (tw iA schA2) = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   856
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
   857
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   858
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   859
(* reduce trace_takes from n to strictly smaller k *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   860
apply (rule take_reduction)
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
apply (rule refl)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   863
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   864
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   865
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   866
(* assumption schA *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   867
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
   868
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   869
apply (simp add: intA_is_not_actB int_is_not_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   870
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   871
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   872
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   873
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   874
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   875
apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   876
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   877
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   878
apply (simp add: ForallTL ForallDropwhile)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   879
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   880
(* case x~:B & x:A  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   881
(* 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
   882
apply (case_tac "x:act A")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   883
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   884
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   885
(* case x~:B & x~:A  *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   886
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   887
apply (rotate_tac -9)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   888
(* reduce forall assumption from tr to (x>>rs) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   889
apply (simp add: externals_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   890
apply (fast intro!: ext_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   891
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   892
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   893
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   894
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   895
subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   896
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   897
lemma compositionality_tr: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   898
"!! 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
   899
            is_asig(asig_of A); is_asig(asig_of B)|]  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   900
        ==>  (tr: traces(A||B)) =  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   901
             (Filter (%a. a:act A)$tr : traces A & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   902
              Filter (%a. a:act B)$tr : traces B & 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   903
              Forall (%x. x:ext(A||B)) tr)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   904
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   905
apply (simp (no_asm) add: traces_def has_trace_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   906
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   907
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   908
(* ==> *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   909
(* There is a schedule of A *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   910
apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   911
prefer 2
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   912
apply (simp add: compositionality_sch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   913
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   914
(* There is a schedule of B *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   915
apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   916
prefer 2
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   917
apply (simp add: compositionality_sch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   918
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   919
(* Traces of A||B have only external actions from A or B *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   920
apply (rule ForallPFilterP)
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
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   924
(* replace schA and schB by Cut(schA) and Cut(schB) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   925
apply (drule exists_LastActExtsch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   926
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   927
apply (drule exists_LastActExtsch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   928
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   929
apply (erule exE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   930
apply (erule conjE)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   931
(* Schedules of A(B) have only actions of A(B) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   932
apply (drule scheds_in_sig)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   933
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   934
apply (drule scheds_in_sig)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   935
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   936
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   937
apply (rename_tac h1 h2 schA schB)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   938
(* 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
   939
   we need here *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   940
apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   941
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   942
(* External actions of mksch are just the oracle *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   943
apply (simp add: FilterA_mksch_is_tr)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   944
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   945
(* mksch is a schedule -- use compositionality on sch-level *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   946
apply (simp add: compositionality_sch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   947
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   948
apply (erule ForallAorB_mksch)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   949
apply (erule ForallPForallQ)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   950
apply (erule ext_is_act)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   951
done
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
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   955
subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   956
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   957
lemma compositionality_tr_modules: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   958
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   959
"!! 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
   960
            is_asig(asig_of A); is_asig(asig_of B)|]  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   961
 ==> Traces (A||B) = par_traces (Traces A) (Traces B)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   962
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   963
apply (unfold Traces_def par_traces_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   964
apply (simp add: asig_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   965
apply (rule set_ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   966
apply (simp add: compositionality_tr externals_of_par)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   967
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   968
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   969
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 19741
diff changeset
   970
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
   971
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   972
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   973
end