src/HOLCF/IOA/meta_theory/ShortExecutions.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 4283 92707e24b62b
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1997  TU Muenchen
mueller@3071
     5
mueller@3275
     6
Some properties about (Cut ex), defined as follows:
mueller@3071
     7
mueller@3275
     8
For every execution ex there is another shorter execution (Cut ex) 
mueller@3071
     9
that has the same trace as ex, but its schedule ends with an external action.
mueller@3071
    10
mueller@3071
    11
*) 
mueller@3071
    12
mueller@3071
    13
mueller@3071
    14
ShortExecutions = Traces + 
mueller@3071
    15
mueller@3071
    16
consts 
mueller@3071
    17
mueller@4283
    18
(*  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
mueller@3275
    19
  LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
mueller@3071
    20
mueller@3275
    21
  Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
mueller@3275
    22
 
mueller@3275
    23
  oraclebuild       ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
mueller@3071
    24
mueller@3071
    25
defs
mueller@3071
    26
mueller@3071
    27
LastActExtsch_def
wenzelm@3847
    28
  "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
mueller@3275
    29
mueller@4283
    30
(* LastActExtex_def
nipkow@10835
    31
  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
mueller@3275
    32
mueller@3275
    33
Cut_def
nipkow@10835
    34
  "Cut P s == oraclebuild P$s$(Filter P$s)"
mueller@3275
    35
mueller@3275
    36
oraclebuild_def
nipkow@10835
    37
  "oraclebuild P == (fix$(LAM h s t. case t of 
mueller@3275
    38
       nil => nil
mueller@3275
    39
    | x##xs => 
mueller@3275
    40
      (case x of 
mueller@3275
    41
        Undef => UU
nipkow@10835
    42
      | Def y => (Takewhile (%x.~P x)$s)
nipkow@10835
    43
                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
mueller@3275
    44
      )
mueller@3275
    45
    ))"
mueller@3275
    46
mueller@3275
    47
mueller@3071
    48
mueller@3071
    49
mueller@3071
    50
rules
mueller@3071
    51
mueller@3361
    52
Cut_prefixcl_Finite
mueller@3361
    53
  "Finite s ==> (? y. s = Cut P s @@ y)"
mueller@3071
    54
mueller@3071
    55
LastActExtsmall1
nipkow@10835
    56
  "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
mueller@3071
    57
mueller@3071
    58
LastActExtsmall2
mueller@3275
    59
  "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
mueller@3071
    60
mueller@3071
    61
end
mueller@3071
    62