1 (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
1 (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
2 ID: |
2 ID: $Id$ |
3 Author: Olaf M"uller |
3 Author: Olaf M"uller |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 |
5 |
6 Some properties about cut(ex), defined as follows: |
6 Some properties about (Cut ex), defined as follows: |
7 |
7 |
8 For every execution ex there is another shorter execution cut(ex) |
8 For every execution ex there is another shorter execution (Cut ex) |
9 that has the same trace as ex, but its schedule ends with an external action. |
9 that has the same trace as ex, but its schedule ends with an external action. |
10 |
10 |
11 *) |
11 *) |
12 |
12 |
13 |
13 |
14 ShortExecutions = Traces + |
14 ShortExecutions = Traces + |
15 |
15 |
16 consts |
16 consts |
17 |
17 |
18 LastActExtsch ::"'a Seq => bool" |
18 LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool" |
19 cutsch ::"'a Seq => 'a Seq" |
19 LastActExtsch ::"('a,'s)ioa => 'a Seq => bool" |
20 |
20 |
|
21 Cut ::"('a => bool) => 'a Seq => 'a Seq" |
|
22 |
|
23 oraclebuild ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" |
21 |
24 |
22 defs |
25 defs |
23 |
26 |
24 LastActExtsch_def |
27 LastActExtsch_def |
25 "LastActExtsch sch == (cutsch sch = sch)" |
28 "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)" |
|
29 |
|
30 LastActExtex_def |
|
31 "LastActExtex A ex == LastActExtsch A (filter_act`ex)" |
|
32 |
|
33 Cut_def |
|
34 "Cut P s == oraclebuild P`s`(Filter P`s)" |
|
35 |
|
36 oraclebuild_def |
|
37 "oraclebuild P == (fix`(LAM h s t. case t of |
|
38 nil => nil |
|
39 | x##xs => |
|
40 (case x of |
|
41 Undef => UU |
|
42 | Def y => (Takewhile (%x.~P x)`s) |
|
43 @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs)) |
|
44 ) |
|
45 ))" |
|
46 |
|
47 |
26 |
48 |
27 |
49 |
28 rules |
50 rules |
29 |
51 |
30 exists_LastActExtsch |
52 execThruCut |
31 "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] |
53 "is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)" |
32 ==> ? sch. sch : schedules A & |
|
33 tr = Filter (%a.a:ext A)`sch & |
|
34 LastActExtsch sch" |
|
35 |
|
36 (* FIX: 1. LastActExtsch should have argument A also? |
|
37 2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *) |
|
38 LastActExtimplUU |
|
39 "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |] |
|
40 ==> sch=UU" |
|
41 |
|
42 (* FIX: see above *) |
|
43 LastActExtimplnil |
|
44 "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |] |
|
45 ==> sch=nil" |
|
46 |
54 |
47 LastActExtsmall1 |
55 LastActExtsmall1 |
48 "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))" |
56 "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))" |
49 |
57 |
50 LastActExtsmall2 |
58 LastActExtsmall2 |
51 "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)" |
59 "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" |
52 |
60 |
53 end |
61 end |
54 |
62 |