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