src/HOLCF/IOA/meta_theory/ShortExecutions.thy
author wenzelm
Sat, 03 Sep 2005 22:27:06 +0200
changeset 17256 526ff7cfd6ea
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted to Isar theory format;
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$
12218
wenzelm
parents: 12028
diff changeset
     3
    Author:     Olaf Müller
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     4
*)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
theory ShortExecutions
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
imports Traces
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
begin
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     9
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
text {*
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    11
  Some properties about @{text "Cut ex"}, defined as follows:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    12
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    13
  For every execution ex there is another shorter execution @{text "Cut ex"}
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    14
  that has the same trace as ex, but its schedule ends with an external action.
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    15
*}
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    17
consts
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
4283
92707e24b62b managed merge details;
mueller
parents: 3847
diff changeset
    19
(*  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    20
  LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    22
  Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    23
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    24
  oraclebuild       ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    27
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    28
LastActExtsch_def:
3847
d5905b98291f fixed dots;
wenzelm
parents: 3361
diff changeset
    29
  "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    30
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    31
(* LastActExtex_def:
10835
nipkow
parents: 4283
diff changeset
    32
  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    33
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    34
Cut_def:
10835
nipkow
parents: 4283
diff changeset
    35
  "Cut P s == oraclebuild P$s$(Filter P$s)"
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    36
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    37
oraclebuild_def:
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    38
  "oraclebuild P == (fix$(LAM h s t. case t of
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    39
       nil => nil
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    40
    | x##xs =>
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    41
      (case x of
12028
52aa183c15bb replaced Undef by UU;
wenzelm
parents: 10835
diff changeset
    42
        UU => UU
10835
nipkow
parents: 4283
diff changeset
    43
      | Def y => (Takewhile (%x.~P x)$s)
nipkow
parents: 4283
diff changeset
    44
                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
3275
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
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    48
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    49
axioms
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    50
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    51
Cut_prefixcl_Finite:
3361
1877e333f66c Last changes for new release 94-8
mueller
parents: 3275
diff changeset
    52
  "Finite s ==> (? y. s = Cut P s @@ y)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    53
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    54
LastActExtsmall1:
10835
nipkow
parents: 4283
diff changeset
    55
  "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    56
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    57
LastActExtsmall2:
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
    58
  "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    59
17256
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    60
ML {* use_legacy_bindings (the_context ()) *}
526ff7cfd6ea converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    61
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62
end