src/HOLCF/IOA/meta_theory/ShortExecutions.thy
author mueller
Wed, 30 Apr 1997 11:20:15 +0200
changeset 3071 981258186b71
child 3275 3f53f2c876f4
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     2
    ID:        
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
Some properties about cut(ex), defined as follows:
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     8
For every execution ex there is another shorter execution cut(ex) 
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
  LastActExtsch     ::"'a Seq  => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    19
  cutsch            ::"'a Seq => 'a Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    23
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    24
LastActExtsch_def
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
  "LastActExtsch sch == (cutsch sch = sch)"
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
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    28
rules
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
exists_LastActExtsch
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    31
  "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|]
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    32
   ==> ? sch. sch : schedules A & 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
              tr = Filter (%a.a:ext A)`sch &
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    34
              LastActExtsch sch"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    35
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    36
(* FIX: 1. LastActExtsch should have argument A also? 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
        2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
LastActExtimplUU
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    39
  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |]
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    40
   ==> sch=UU"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    41
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
(* FIX: see above *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    43
LastActExtimplnil
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    44
  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |]
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    45
   ==> sch=nil"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    46
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    47
LastActExtsmall1
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
  "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))"
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
LastActExtsmall2
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    51
  "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)"
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
end
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    54