src/HOLCF/IOA/meta_theory/ShortExecutions.thy
author mueller
Wed, 21 May 1997 15:08:52 +0200
changeset 3275 3f53f2c876f4
parent 3071 981258186b71
child 3361 1877e333f66c
permissions -rw-r--r--
changes for release 94-8
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/ShortExecutions.thy
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     3
    Author:     Olaf M"uller
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     6
Some properties about (Cut ex), defined as follows:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     8
For every execution ex there is another shorter execution (Cut ex) 
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     9
that has the same trace as ex, but its schedule ends with an external action.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    10
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    14
ShortExecutions = Traces + 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
consts 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    18
  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    19
  LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    21
  Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    22
 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    23
  oraclebuild       ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    24
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    27
LastActExtsch_def
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    28
  "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    29
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    30
LastActExtex_def
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    31
  "LastActExtex A ex == LastActExtsch A (filter_act`ex)"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    32
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    33
Cut_def
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    34
  "Cut P s == oraclebuild P`s`(Filter P`s)"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    35
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    36
oraclebuild_def
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    37
  "oraclebuild P == (fix`(LAM h s t. case t of 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    38
       nil => nil
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    39
    | x##xs => 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    40
      (case x of 
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    41
        Undef => UU
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    42
      | Def y => (Takewhile (%x.~P x)`s)
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    43
                  @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs))
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    44
      )
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    45
    ))"
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    46
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    47
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    49
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    50
rules
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    51
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    52
execThruCut
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    53
  "is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    54
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    55
LastActExtsmall1
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    56
  "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    57
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    58
LastActExtsmall2
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    59
  "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    60
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    61
end
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62