src/HOLCF/IOA/meta_theory/CompoTraces.thy
author mueller
Wed Apr 30 11:20:15 1997 +0200 (1997-04-30)
changeset 3071 981258186b71
child 3275 3f53f2c876f4
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
mueller@3071
     2
    ID:        
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Compositionality on Trace level.
mueller@3071
     7
*) 
mueller@3071
     8
mueller@3071
     9
CompoTraces = CompoScheds + ShortExecutions +
mueller@3071
    10
 
mueller@3071
    11
mueller@3071
    12
consts  
mueller@3071
    13
mueller@3071
    14
 mksch     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
mueller@3071
    15
mueller@3071
    16
mueller@3071
    17
defs
mueller@3071
    18
mueller@3071
    19
mksch_def
mueller@3071
    20
  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
mueller@3071
    21
       nil => nil
mueller@3071
    22
    | x##xs => 
mueller@3071
    23
      (case x of 
mueller@3071
    24
        Undef => UU
mueller@3071
    25
      | Def y => 
mueller@3071
    26
         (if y:act A then 
mueller@3071
    27
             (if y:act B then 
mueller@3071
    28
                   ((Takewhile (%a.a:int A)`schA)
mueller@3071
    29
                      @@ (Takewhile (%a.a:int B)`schB)
mueller@3071
    30
                           @@ (y>>(h`xs
mueller@3071
    31
                                    `(TL`(Dropwhile (%a.a:int A)`schA))
mueller@3071
    32
                                    `(TL`(Dropwhile (%a.a:int B)`schB))
mueller@3071
    33
                    )))
mueller@3071
    34
              else
mueller@3071
    35
                 ((Takewhile (%a.a:int A)`schA)
mueller@3071
    36
                  @@ (y>>(h`xs
mueller@3071
    37
                           `(TL`(Dropwhile (%a.a:int A)`schA))
mueller@3071
    38
                           `schB)))
mueller@3071
    39
              )
mueller@3071
    40
          else 
mueller@3071
    41
             (if y:act B then 
mueller@3071
    42
                 ((Takewhile (%a.a:int B)`schB)
mueller@3071
    43
                     @@ (y>>(h`xs
mueller@3071
    44
                              `schA
mueller@3071
    45
                              `(TL`(Dropwhile (%a.a:int B)`schB))
mueller@3071
    46
                              )))
mueller@3071
    47
             else
mueller@3071
    48
               UU
mueller@3071
    49
             )
mueller@3071
    50
         )
mueller@3071
    51
       )))"
mueller@3071
    52
mueller@3071
    53
mueller@3071
    54
rules
mueller@3071
    55
mueller@3071
    56
(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *)
mueller@3071
    57
not_ext_is_int_FIX
mueller@3071
    58
  "[|is_asig S|] ==> (x~:externals S) = (x: internals S)"
mueller@3071
    59
mueller@3071
    60
(* FIX: should be more general , something like subst *)
mueller@3071
    61
lemma12
mueller@3071
    62
"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)"
mueller@3071
    63
mueller@3071
    64
(* FIX: as above, should be done more intelligent *)
mueller@3071
    65
lemma22
mueller@3071
    66
"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g"
mueller@3071
    67
mueller@3071
    68
Finite_Conc
mueller@3071
    69
  "Finite (x @@ y) = (Finite x & Finite y)"
mueller@3071
    70
mueller@3071
    71
finiteR_mksch
mueller@3071
    72
  "Finite (mksch A B`tr`x`y) --> Finite tr"
mueller@3071
    73
mueller@3071
    74
finiteL_mksch
mueller@3071
    75
  "[| Finite tr; 
mueller@3071
    76
   Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr;
mueller@3071
    77
   Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr;
mueller@3071
    78
   Forall (%x. x:ext (A||B)) tr |]
mueller@3071
    79
   ==> Finite (mksch A B`tr`x`y)"
mueller@3071
    80
mueller@3071
    81
reduce_mksch
mueller@3071
    82
  "[| Finite bs; Forall (%x. x:act B & x~:act A) bs;
mueller@3071
    83
      Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) |] 
mueller@3071
    84
  ==> ? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) &
mueller@3071
    85
                Forall (%x. x:act B & x~:act A) y1 &
mueller@3071
    86
                Finite y1 & y = (y1 @@ y2) & 
mueller@3071
    87
                Filter (%a. a:ext B)`y1 = bs"
mueller@3071
    88
mueller@3071
    89
end
mueller@3071
    90
mueller@3071
    91