3071

1 
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy

3275

2 
ID: $Id$

12218

3 
Author: Olaf Müller

17256

4 
*)

3071

5 

17256

6 
theory ShortExecutions


7 
imports Traces


8 
begin

3071

9 

17256

10 
text {*


11 
Some properties about @{text "Cut ex"}, defined as follows:

3071

12 

17256

13 
For every execution ex there is another shorter execution @{text "Cut ex"}


14 
that has the same trace as ex, but its schedule ends with an external action.


15 
*}

3071

16 

17256

17 
consts

3071

18 

4283

19 
(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*)

3275

20 
LastActExtsch ::"('a,'s)ioa => 'a Seq => bool"

3071

21 

3275

22 
Cut ::"('a => bool) => 'a Seq => 'a Seq"

17256

23 

3275

24 
oraclebuild ::"('a => bool) => 'a Seq > 'a Seq > 'a Seq"

3071

25 


26 
defs


27 

17256

28 
LastActExtsch_def:

3847

29 
"LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"

3275

30 

17256

31 
(* LastActExtex_def:

10835

32 
"LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)

3275

33 

17256

34 
Cut_def:

10835

35 
"Cut P s == oraclebuild P$s$(Filter P$s)"

3275

36 

17256

37 
oraclebuild_def:


38 
"oraclebuild P == (fix$(LAM h s t. case t of

3275

39 
nil => nil

17256

40 
 x##xs =>


41 
(case x of

12028

42 
UU => UU

10835

43 
 Def y => (Takewhile (%x.~P x)$s)


44 
@@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))

3275

45 
)


46 
))"


47 


48 

17256

49 
axioms

3071

50 

17256

51 
Cut_prefixcl_Finite:

3361

52 
"Finite s ==> (? y. s = Cut P s @@ y)"

3071

53 

17256

54 
LastActExtsmall1:

10835

55 
"LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"

3071

56 

17256

57 
LastActExtsmall2:

3275

58 
"[ Finite sch1; LastActExtsch A (sch1 @@ sch2) ] ==> LastActExtsch A sch2"

3071

59 

17256

60 
ML {* use_legacy_bindings (the_context ()) *}


61 

3071

62 
end
