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