--- a/src/HOLCF/IOA/meta_theory/Asig.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Thu Jun 12 16:47:15 1997 +0200
@@ -22,6 +22,14 @@
by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
qed"int_is_act";
+goal thy "!!a.[|a:inputs S|] ==> a:actions S";
+by (asm_full_simp_tac (!simpset addsimps [asig_inputs_def,actions_def]) 1);
+qed"inp_is_act";
+
+goal thy "!!a.[|a:outputs S|] ==> a:actions S";
+by (asm_full_simp_tac (!simpset addsimps [asig_outputs_def,actions_def]) 1);
+qed"out_is_act";
+
goal thy "(x: actions S & x : externals S) = (x: externals S)";
by (fast_tac (!claset addSIs [ext_is_act]) 1 );
qed"ext_and_act";
--- a/src/HOLCF/IOA/meta_theory/Asig.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Thu Jun 12 16:47:15 1997 +0200
@@ -13,7 +13,7 @@
'a signature = "('a set * 'a set * 'a set)"
consts
- actions,inputs,outputs,internals,externals
+ actions,inputs,outputs,internals,externals,locals
::"'action signature => 'action set"
is_asig ::"'action signature => bool"
mk_ext_asig ::"'action signature => 'action signature"
@@ -31,6 +31,9 @@
externals_def
"externals(asig) == (inputs(asig) Un outputs(asig))"
+locals_def
+ "locals asig == ((internals asig) Un (outputs asig))"
+
is_asig_def
"is_asig(triple) ==
((inputs(triple) Int outputs(triple) = {}) &
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Thu Jun 12 16:47:15 1997 +0200
@@ -88,20 +88,20 @@
section "actions and compatibility";
-goal thy"compat_ioas A B = compat_ioas B A";
-by (asm_full_simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_commute]) 1);
+goal thy"compatible A B = compatible B A";
+by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
auto();
qed"compat_commute";
-goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
- "!! a. [| compat_ioas A1 A2; a:ext A1|] ==> a~:int A2";
+goalw thy [externals_def,actions_def,compatible_def]
+ "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
by (Asm_full_simp_tac 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"ext1_is_not_int2";
-(* just commuting the previous one: better commute compat_ioas *)
-goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
- "!! a. [| compat_ioas A2 A1 ; a:ext A1|] ==> a~:int A2";
+(* just commuting the previous one: better commute compatible *)
+goalw thy [externals_def,actions_def,compatible_def]
+ "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
by (Asm_full_simp_tac 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"ext2_is_not_int1";
@@ -109,18 +109,26 @@
bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
-goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
- "!! x. [| compat_ioas A B; x:int A |] ==> x~:ext B";
+goalw thy [externals_def,actions_def,compatible_def]
+ "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
by (Asm_full_simp_tac 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"intA_is_not_extB";
-goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def,is_asig_def,asig_of_def]
-"!! a. [| compat_ioas A B; a:int A |] ==> a ~: act B";
+goalw thy [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
+"!! a. [| compatible A B; a:int A |] ==> a ~: act B";
by (Asm_full_simp_tac 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"intA_is_not_actB";
+goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
+ compatible_def,is_asig_def,asig_of_def]
+"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"outAactB_is_inpB";
+
+
(* ---------------------------------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Jun 12 16:47:15 1997 +0200
@@ -18,20 +18,20 @@
consts
(* IO automata *)
- state_trans::"['a signature, ('a,'s)transition set] => bool"
- asig_of ::"('a,'s)ioa => 'a signature"
- starts_of ::"('a,'s)ioa => 's set"
- trans_of ::"('a,'s)ioa => ('a,'s)transition set"
- IOA ::"('a,'s)ioa => bool"
+ state_trans ::"['a signature, ('a,'s)transition set] => bool"
+ input_enabled::"['a signature, ('a,'s)transition set] => bool"
+ asig_of ::"('a,'s)ioa => 'a signature"
+ starts_of ::"('a,'s)ioa => 's set"
+ trans_of ::"('a,'s)ioa => ('a,'s)transition set"
+ IOA ::"('a,'s)ioa => bool"
(* reachability and invariants *)
reachable :: "('a,'s)ioa => 's set"
invariant :: "[('a,'s)ioa, 's=>bool] => bool"
(* binary composition of action signatures and automata *)
- compat_asigs ::"['a signature, 'a signature] => bool"
asig_comp ::"['a signature, 'a signature] => 'a signature"
- compat_ioas ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
+ compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
"||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
(* hiding *)
@@ -51,6 +51,7 @@
"int" :: "('a,'s)ioa => 'a set"
"inp" :: "('a,'s)ioa => 'a set"
"out" :: "('a,'s)ioa => 'a set"
+ "local" :: "('a,'s)ioa => 'a set"
syntax (symbols)
@@ -74,6 +75,8 @@
"int A" == "internals (asig_of A)"
"inp A" == "inputs (asig_of A)"
"out A" == "outputs (asig_of A)"
+ "local A" == "locals (asig_of A)"
+
defs
@@ -83,7 +86,10 @@
state_trans_def
"state_trans asig R ==
(!triple. triple:R --> fst(snd(triple)):actions(asig))"
-(* & (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" *)
+
+input_enabled_def
+ "input_enabled asig R ==
+ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
asig_of_def "asig_of == fst"
@@ -93,7 +99,8 @@
ioa_def
"IOA(ioa) == (is_asig(asig_of(ioa)) &
(~ starts_of(ioa) = {}) &
- state_trans (asig_of ioa) (trans_of ioa))"
+ state_trans (asig_of ioa) (trans_of ioa) &
+ input_enabled (asig_of ioa) (trans_of ioa))"
invariant_def "invariant A P == (!s. reachable A s --> P(s))"
@@ -101,16 +108,12 @@
(* ------------------------- parallel composition --------------------------*)
-compat_asigs_def
- "compat_asigs a1 a2 ==
- (((outputs(a1) Int outputs(a2)) = {}) &
- ((internals(a1) Int actions(a2)) = {}) &
- ((internals(a2) Int actions(a1)) = {}))"
-
-compat_ioas_def
- "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
-
+compatible_def
+ "compatible A B ==
+ (((out A Int out B) = {}) &
+ ((int A Int act B) = {}) &
+ ((int B Int act A) = {}))"
asig_comp_def
"asig_comp a1 a2 ==
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Thu Jun 12 16:47:15 1997 +0200
@@ -159,11 +159,11 @@
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *)
(* --------------------------------------------------------------------- *)
-goal thy "!s. is_execution_fragment (A||B) (s,xs) \
-\ --> is_execution_fragment A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
-\ is_execution_fragment B (snd s, Filter_ex2 B`(ProjB2`xs))";
+goal thy "!s. is_exec_frag (A||B) (s,xs) \
+\ --> is_exec_frag A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
+\ is_exec_frag B (snd s, Filter_ex2 B`(ProjB2`xs))";
-by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+by (pair_induct_tac "xs" [is_exec_frag_def] 1);
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
@@ -176,11 +176,11 @@
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *)
(* --------------------------------------------------------------------- *)
-goal thy "!s. is_execution_fragment (A||B) (s,xs) \
+goal thy "!s. is_exec_frag (A||B) (s,xs) \
\ --> stutter A (fst s,ProjA2`xs) &\
\ stutter B (snd s,ProjB2`xs)";
-by (pair_induct_tac "xs" [stutter_def,is_execution_fragment_def] 1);
+by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
(* main case *)
by (safe_tac set_cs);
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
@@ -192,10 +192,10 @@
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *)
(* --------------------------------------------------------------------- *)
-goal thy "!s. (is_execution_fragment (A||B) (s,xs) \
+goal thy "!s. (is_exec_frag (A||B) (s,xs) \
\ --> Forall (%x.fst x:act (A||B)) xs)";
-by (pair_induct_tac "xs" [Forall_def,sforall_def,is_execution_fragment_def] 1);
+by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
(* main case *)
by (safe_tac set_cs);
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
@@ -208,15 +208,15 @@
(* ----------------------------------------------------------------------- *)
goal thy
-"!s. is_execution_fragment A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
-\ is_execution_fragment B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
+"!s. is_exec_frag A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
+\ is_exec_frag B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
\ stutter A (fst s,(ProjA2`xs)) & \
\ stutter B (snd s,(ProjB2`xs)) & \
\ Forall (%x.fst x:act (A||B)) xs \
-\ --> is_execution_fragment (A||B) (s,xs)";
+\ --> is_exec_frag (A||B) (s,xs)";
by (pair_induct_tac "xs" [Forall_def,sforall_def,
- is_execution_fragment_def, stutter_def] 1);
+ is_exec_frag_def, stutter_def] 1);
(* main case *)
by (rtac allI 1);
ren "ss a t s" 1;
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Jun 12 16:47:15 1997 +0200
@@ -186,10 +186,10 @@
an ex is in A or B, but after projecting it onto the action schedule. Of course, this
is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
-goal thy "!s. is_execution_fragment (A||B) (s,xs) \
+goal thy "!s. is_exec_frag (A||B) (s,xs) \
\ --> Forall (%x.x:act (A||B)) (filter_act`xs)";
-by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
+by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
by (safe_tac set_cs);
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Jun 12 16:47:15 1997 +0200
@@ -146,7 +146,7 @@
qed"subst_lemma2";
-goal thy "!!A B. compat_ioas A B ==> \
+goal thy "!!A B. compatible A B ==> \
\ ! schA schB. Forall (%x. x:act (A||B)) tr \
\ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
@@ -175,7 +175,7 @@
bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
-goal thy "!!A B. compat_ioas B A ==> \
+goal thy "!!A B. compatible B A ==> \
\ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \
\ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
@@ -189,7 +189,7 @@
bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp);
-goal thy "!!A B. compat_ioas A B ==> \
+goal thy "!!A B. compatible A B ==> \
\ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \
\ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
@@ -282,7 +282,7 @@
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
Delsimps [FilterConc];
-goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==> \
+goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
\! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
@@ -337,7 +337,7 @@
Delsimps [FilterConc];
-goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==> \
+goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
\! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
\ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
@@ -479,7 +479,7 @@
------------------------------------------------------------------------------------- *)
goal thy
-"!! A B. [| compat_ioas A B; compat_ioas B A;\
+"!! A B. [| compatible A B; compatible B A;\
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
\ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
\ Forall (%x.x:ext (A||B)) tr & \
@@ -555,7 +555,7 @@
take lemma
--------------------------------------------------------------------------- *)
-goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \
+goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
\ Forall (%x.x:ext (A||B)) tr & \
\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
@@ -689,7 +689,7 @@
-goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \
+goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
\ Forall (%x.x:ext (A||B)) tr & \
\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
@@ -931,7 +931,7 @@
-goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \
+goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
\ Forall (%x.x:ext (A||B)) tr & \
\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
@@ -1170,7 +1170,7 @@
(* ------------------------------------------------------------------ *)
goal thy
-"!! A B. [| IOA A; IOA B; compat_ioas A B; compat_ioas B A; \
+"!! A B. [| IOA A; IOA B; compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B)|] \
\ ==> tr: traces(A||B) = \
\ (Filter (%a.a:act A)`tr : traces A &\
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Jun 12 16:47:15 1997 +0200
@@ -14,7 +14,7 @@
goal thy
-"!! A B. [| compat_ioas A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
+"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
br ForallPFilterQR 1;
ba 2;
@@ -32,7 +32,7 @@
qed"compatibility_consequence4";
goal thy
-"!! A B. [| compat_ioas A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
+"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
br ForallPFilterQR 1;
ba 2;
@@ -52,7 +52,7 @@
\ [| IOA A1; IOA A2; IOA B1; IOA B2;\
\ is_asig (asig_of A1); is_asig (asig_of A2); \
\ is_asig (asig_of B1); is_asig (asig_of B2); \
-\ compat_ioas A1 B1; compat_ioas A2 B2; \
+\ compatible A1 B1; compatible A2 B2; \
\ A1 =<| A2; \
\ B1 =<| B2 |] \
\ ==> (A1 || B1) =<| (A2 || B2)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Jun 12 16:47:15 1997 +0200
@@ -0,0 +1,91 @@
+(* Title: HOLCF/IOA/meta_theory/Deadlock.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Deadlock freedom of I/O Automata
+*)
+
+(********************************************************************************
+ input actions may always be added to a schedule
+**********************************************************************************)
+
+goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; IOA A; Finite sch|] \
+\ ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A";
+by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
+by (safe_tac set_cs);
+by (forward_tac [inp_is_act] 1);
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "ex" 1);
+ren "sch s ex" 1;
+by (subgoal_tac "Finite ex" 1);
+by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
+br (Map2Finite RS iffD1) 2;
+by (res_inst_tac [("t","Map fst`ex")] subst 2);
+ba 2;
+be FiniteFilter 2;
+(* subgoal 1 *)
+by (forward_tac [exists_laststate] 1);
+be allE 1;
+be exE 1;
+(* using input-enabledness *)
+by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
+by (REPEAT (etac conjE 1));
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","u")] allE 1);
+be exE 1;
+(* instantiate execution *)
+by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
+by (eres_inst_tac [("t","u")] lemma_2_1 1);
+by (Asm_full_simp_tac 1);
+br sym 1;
+ba 1;
+qed"scheds_input_enabled";
+
+(********************************************************************************
+ Deadlock freedom: component B cannot block an out or int action
+ of component A in every schedule
+ Needs compositionality on schedule level, input-enabledness, compatibility
+ and distributivity of is_exec_frag over @@
+**********************************************************************************)
+
+goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
+\ Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; IOA B |] \
+\ ==> (sch @@ a>>nil) : schedules (A||B)";
+
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
+br conjI 1;
+(* a : act (A||B) *)
+by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
+br disjI1 2;
+be disjE 2;
+be int_is_act 2;
+be out_is_act 2;
+(* Filter B (sch@@[a]) : schedules B *)
+
+by (case_tac "a:int A" 1);
+bd intA_is_not_actB 1;
+ba 1; (* --> a~:act B *)
+by (Asm_full_simp_tac 1);
+
+(* case a~:int A , i.e. a:out A *)
+by (case_tac "a~:act B" 1);
+by (Asm_full_simp_tac 1);
+(* case a:act B *)
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "a:out A" 1);
+by (Fast_tac 2);
+bd outAactB_is_inpB 1;
+ba 1;
+ba 1;
+br scheds_input_enabled 1;
+by (Asm_full_simp_tac 1);
+by (REPEAT (atac 1));
+qed"IOA_deadlock_free";
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Jun 12 16:47:15 1997 +0200
@@ -0,0 +1,9 @@
+(* Title: HOLCF/IOA/meta_theory/Deadlock.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+Deadlock freedom of I/O Automata
+*)
+
+Deadlock = RefCorrectness + CompoScheds
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Thu Jun 12 16:47:15 1997 +0200
@@ -14,43 +14,43 @@
(* ---------------------------------------------------------------- *)
-(* corresp_ex2 *)
+(* corresp_exC *)
(* ---------------------------------------------------------------- *)
-goal thy "corresp_ex2 A f = (LAM ex. (%s. case ex of \
+goal thy "corresp_exC A f = (LAM ex. (%s. case ex of \
\ nil => nil \
-\ | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr)))) \
-\ @@ ((corresp_ex2 A f `xs) (f (snd pr)))) \
+\ | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) \
+\ @@ ((corresp_exC A f `xs) (snd pr))) \
\ `x) ))";
by (rtac trans 1);
br fix_eq2 1;
-br corresp_ex2_def 1;
+br corresp_exC_def 1;
br beta_cfun 1;
by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"corresp_ex2_unfold";
+qed"corresp_exC_unfold";
-goal thy "(corresp_ex2 A f`UU) s=UU";
-by (stac corresp_ex2_unfold 1);
+goal thy "(corresp_exC A f`UU) s=UU";
+by (stac corresp_exC_unfold 1);
by (Simp_tac 1);
-qed"corresp_ex2_UU";
+qed"corresp_exC_UU";
-goal thy "(corresp_ex2 A f`nil) s = nil";
-by (stac corresp_ex2_unfold 1);
+goal thy "(corresp_exC A f`nil) s = nil";
+by (stac corresp_exC_unfold 1);
by (Simp_tac 1);
-qed"corresp_ex2_nil";
+qed"corresp_exC_nil";
-goal thy "(corresp_ex2 A f`(at>>xs)) s = \
-\ (snd(@cex. move A cex s (fst at) (f (snd at)))) \
-\ @@ ((corresp_ex2 A f`xs) (f (snd at)))";
+goal thy "(corresp_exC A f`(at>>xs)) s = \
+\ (@cex. move A cex (f s) (fst at) (f (snd at))) \
+\ @@ ((corresp_exC A f`xs) (snd at))";
br trans 1;
-by (stac corresp_ex2_unfold 1);
+by (stac corresp_exC_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
-qed"corresp_ex2_cons";
+qed"corresp_exC_cons";
-Addsimps [corresp_ex2_UU,corresp_ex2_nil,corresp_ex2_cons];
+Addsimps [corresp_exC_UU,corresp_exC_nil,corresp_exC_cons];
@@ -74,7 +74,7 @@
goal thy
"!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ is_execution_fragment A (@x. move A x (f s) a (f t))";
+\ is_exec_frag A (f s,@x. move A x (f s) a (f t))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
@@ -82,7 +82,7 @@
goal thy
"!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ Finite (snd (@x. move A x (f s) a (f t)))";
+\ Finite ((@x. move A x (f s) a (f t)))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
@@ -90,7 +90,7 @@
goal thy
"!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ fst (@x. move A x (f s) a (f t)) = (f s)";
+\ laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
@@ -98,49 +98,13 @@
goal thy
"!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ laststate (@x. move A x (f s) a (f t)) = (f t)";
-by (cut_inst_tac [] move_is_move 1);
-by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
-qed"move_subprop4";
-
-goal thy
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ mk_trace A`(snd(@x. move A x (f s) a (f t))) = \
+\ mk_trace A`((@x. move A x (f s) a (f t))) = \
\ (if a:ext A then a>>nil else nil)";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
-qed"move_subprop5";
-
-goal thy
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ (is_execution_fragment A (f s,(snd (@x. move A x (f s) a (f t)))))";
-by (cut_inst_tac [] move_subprop3 1);
-by (REPEAT (assume_tac 1));
-by (cut_inst_tac [] move_subprop1 1);
-by (REPEAT (assume_tac 1));
-by (res_inst_tac [("s","fst (@x. move A x (f s) a (f t))")] subst 1);
-back();
-back();
-back();
-ba 1;
-by (simp_tac (HOL_basic_ss addsimps [surjective_pairing RS sym]) 1);
-qed"move_subprop_1and3";
-
-goal thy
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\ (case Last`(snd (@x. move A x (f s) a (f t))) of \
-\ Undef => (f s) \
-\ | Def p => snd p) = (f t)";
-by (cut_inst_tac [] move_subprop3 1);
-by (REPEAT (assume_tac 1));
-by (cut_inst_tac [] move_subprop4 1);
-by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [laststate_def]) 1);
-qed"move_subprop_4and3";
-
+qed"move_subprop4";
(* ------------------------------------------------------------------ *)
@@ -168,10 +132,10 @@
goalw thy [corresp_ex_def]
"!!f.[|is_ref_map f C A; ext C = ext A|] ==> \
-\ !s. reachable C s & is_execution_fragment C (s,xs) --> \
+\ !s. reachable C s & is_exec_frag C (s,xs) --> \
\ mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
-by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+by (pair_induct_tac "xs" [is_exec_frag_def] 1);
(* cons case *)
by (safe_tac set_cs);
by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
@@ -179,7 +143,7 @@
ba 1;
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [move_subprop5]
+by (asm_full_simp_tac (!simpset addsimps [move_subprop4]
setloop split_tac [expand_if] ) 1);
qed"lemma_1";
@@ -197,9 +161,9 @@
goal thy
"Finite xs --> \
-\(!s .is_execution_fragment A (s,xs) & is_execution_fragment A (t,ys) & \
+\(!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & \
\ t = laststate (s,xs) \
-\ --> is_execution_fragment A (s,xs @@ ys))";
+\ --> is_exec_frag A (s,xs @@ ys))";
br impI 1;
by (Seq_Finite_induct_tac 1);
@@ -208,7 +172,7 @@
(* main case *)
by (safe_tac set_cs);
by (pair_tac "a" 1);
-qed"lemma_2_1";
+qed_spec_mp"lemma_2_1";
(* ----------------------------------------------------------- *)
@@ -219,22 +183,22 @@
goalw thy [corresp_ex_def]
"!!f.[| is_ref_map f C A |] ==>\
-\ !s. reachable C s & is_execution_fragment C (s,xs) \
-\ --> is_execution_fragment A (corresp_ex A f (s,xs))";
+\ !s. reachable C s & is_exec_frag C (s,xs) \
+\ --> is_exec_frag A (corresp_ex A f (s,xs))";
by (Asm_full_simp_tac 1);
-by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+by (pair_induct_tac "xs" [is_exec_frag_def] 1);
(* main case *)
by (safe_tac set_cs);
-by (res_inst_tac [("t3","f y")] (lemma_2_1 RS mp RS spec RS mp) 1);
+by (res_inst_tac [("t","f y")] lemma_2_1 1);
(* Finite *)
be move_subprop2 1;
by (REPEAT (atac 1));
by (rtac conjI 1);
-(* is_execution_fragment *)
-be move_subprop_1and3 1;
+(* is_exec_frag *)
+be move_subprop1 1;
by (REPEAT (atac 1));
by (rtac conjI 1);
@@ -246,8 +210,7 @@
ba 1;
by (Asm_full_simp_tac 1);
(* laststate *)
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
-be (move_subprop_4and3 RS sym) 1;
+be (move_subprop3 RS sym) 1;
by (REPEAT (atac 1));
qed"lemma_2";
@@ -260,7 +223,7 @@
goalw thy [traces_def]
- "!!f. [| IOA C; IOA A; ext C = ext A; is_ref_map f C A |] \
+ "!!f. [| ext C = ext A; is_ref_map f C A |] \
\ ==> traces C <= traces A";
by (simp_tac(!simpset addsimps [has_trace_def2])1);
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Jun 12 16:47:15 1997 +0200
@@ -8,26 +8,26 @@
RefCorrectness = RefMappings +
-
+
consts
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
('a,'s1)execution => ('a,'s2)execution"
- corresp_ex2 ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
- -> ('s2 => ('a,'s2)pairs)"
+ corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
+ -> ('s1 => ('a,'s2)pairs)"
defs
corresp_ex_def
- "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"
+ "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
-corresp_ex2_def
- "corresp_ex2 A f == (fix`(LAM h ex. (%s. case ex of
+corresp_exC_def
+ "corresp_exC A f == (fix`(LAM h ex. (%s. case ex of
nil => nil
- | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
- @@ ((h`xs) (f (snd pr))))
+ | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
+ @@ ((h`xs) (snd pr)))
`x) )))"
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jun 12 16:47:15 1997 +0200
@@ -8,6 +8,10 @@
+(* ---------------------------------------------------------------------------- *)
+ section "laststate";
+(* ---------------------------------------------------------------------------- *)
+
goal thy "laststate (s,UU) = s";
by (simp_tac (!simpset addsimps [laststate_def]) 1);
qed"laststate_UU";
@@ -28,6 +32,11 @@
Addsimps [laststate_UU,laststate_nil,laststate_cons];
+goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)";
+by (Seq_Finite_induct_tac 1);
+qed"exists_laststate";
+
+
(* ---------------------------------------------------------------------------- *)
section "transitions and moves";
@@ -35,14 +44,14 @@
goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
-by (res_inst_tac [("x","(s,(a,t)>>nil)")] exI 1);
+by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
qed"transition_is_ex";
-
+
goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
-by (res_inst_tac [("x","(s,nil)")] exI 1);
+by (res_inst_tac [("x","nil")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
qed"nothing_is_ex";
@@ -50,7 +59,7 @@
goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
\ ==> ? ex. move A ex s a s''";
-by (res_inst_tac [("x","(s,(a,s')>>(a',s'')>>nil)")] exI 1);
+by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
qed"ei_transitions_are_ex";
@@ -60,7 +69,7 @@
\ (~a2:ext A) & (~a3:ext A) ==> \
\ ? ex. move A ex s1 a1 s4";
-by (res_inst_tac [("x","(s1,(a1,s2)>>(a2,s3)>>(a3,s4)>>nil)")] exI 1);
+by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
qed"eii_transitions_are_ex";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Thu Jun 12 16:47:15 1997 +0200
@@ -12,7 +12,7 @@
consts
laststate ::"('a,'s)execution => 's"
- move ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool"
+ move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
@@ -23,13 +23,11 @@
Undef => fst ex
| Def at => snd at"
-(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can
- be omitted *)
move_def
"move ioa ex s a t ==
- (is_execution_fragment ioa ex & Finite (snd ex) &
- fst ex=s & laststate ex=t &
- mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))"
+ (is_exec_frag ioa (s,ex) & Finite ex &
+ laststate (s,ex)=t &
+ mk_trace ioa`ex = (if a:ext(ioa) then a>>nil else nil))"
is_ref_map_def
"is_ref_map f C A ==
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Jun 12 16:47:15 1997 +0200
@@ -473,6 +473,13 @@
be FiniteMap1 1;
qed"Map2Finite";
+
+goal thy "!! s. Finite s ==> Finite (Filter P`s)";
+by (Seq_Finite_induct_tac 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed"FiniteFilter";
+
+
(* ----------------------------------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Jun 12 16:47:15 1997 +0200
@@ -209,7 +209,7 @@
-goal thy "!!ex .is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)";
+goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
by (case_tac "Finite ex" 1);
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
ba 1;
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Thu Jun 12 16:47:15 1997 +0200
@@ -8,7 +8,7 @@
Delsimps (ex_simps @ all_simps);
-val exec_rws = [executions_def,is_execution_fragment_def];
+val exec_rws = [executions_def,is_exec_frag_def];
@@ -60,67 +60,67 @@
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
(* ---------------------------------------------------------------- *)
-(* is_ex_fr *)
+(* is_exec_fragC *)
(* ---------------------------------------------------------------- *)
-goal thy "is_ex_fr A = (LAM ex. (%s. case ex of \
+goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
\ nil => TT \
\ | x##xs => (flift1 \
-\ (%p.Def ((s,p):trans_of A) andalso (is_ex_fr A`xs) (snd p)) \
+\ (%p.Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
\ `x) \
\ ))";
by (rtac trans 1);
br fix_eq2 1;
-br is_ex_fr_def 1;
+br is_exec_fragC_def 1;
br beta_cfun 1;
by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"is_ex_fr_unfold";
+qed"is_exec_fragC_unfold";
-goal thy "(is_ex_fr A`UU) s=UU";
-by (stac is_ex_fr_unfold 1);
+goal thy "(is_exec_fragC A`UU) s=UU";
+by (stac is_exec_fragC_unfold 1);
by (Simp_tac 1);
-qed"is_ex_fr_UU";
+qed"is_exec_fragC_UU";
-goal thy "(is_ex_fr A`nil) s = TT";
-by (stac is_ex_fr_unfold 1);
+goal thy "(is_exec_fragC A`nil) s = TT";
+by (stac is_exec_fragC_unfold 1);
by (Simp_tac 1);
-qed"is_ex_fr_nil";
+qed"is_exec_fragC_nil";
-goal thy "(is_ex_fr A`(pr>>xs)) s = \
+goal thy "(is_exec_fragC A`(pr>>xs)) s = \
\ (Def ((s,pr):trans_of A) \
-\ andalso (is_ex_fr A`xs)(snd pr))";
+\ andalso (is_exec_fragC A`xs)(snd pr))";
br trans 1;
-by (stac is_ex_fr_unfold 1);
+by (stac is_exec_fragC_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
-qed"is_ex_fr_cons";
+qed"is_exec_fragC_cons";
-Addsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons];
+Addsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons];
(* ---------------------------------------------------------------- *)
-(* is_execution_fragment *)
+(* is_exec_frag *)
(* ---------------------------------------------------------------- *)
-goal thy "is_execution_fragment A (s, UU)";
-by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
-qed"is_execution_fragment_UU";
+goal thy "is_exec_frag A (s, UU)";
+by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+qed"is_exec_frag_UU";
-goal thy "is_execution_fragment A (s, nil)";
-by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
-qed"is_execution_fragment_nil";
+goal thy "is_exec_frag A (s, nil)";
+by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+qed"is_exec_frag_nil";
-goal thy "is_execution_fragment A (s, (a,t)>>ex) = \
+goal thy "is_exec_frag A (s, (a,t)>>ex) = \
\ (((s,a,t):trans_of A) & \
-\ is_execution_fragment A (t, ex))";
-by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
-qed"is_execution_fragment_cons";
+\ is_exec_frag A (t, ex))";
+by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+qed"is_exec_frag_cons";
-(* Delsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons]; *)
-Addsimps [is_execution_fragment_UU,is_execution_fragment_nil, is_execution_fragment_cons];
+(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
+Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons];
(* -------------------------------------------------------------------------------- *)
@@ -163,9 +163,9 @@
goal thy
"!! A. IOA A ==> \
-\ ! s. is_execution_fragment A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
-by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
+by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
@@ -195,8 +195,8 @@
section "executions are prefix closed";
(* only admissible in y, not if done in x !! *)
-goal thy "!x s. is_execution_fragment A (s,x) & y<<x --> is_execution_fragment A (s,y)";
-by (pair_induct_tac "y" [is_execution_fragment_def] 1);
+goal thy "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)";
+by (pair_induct_tac "y" [is_exec_frag_def] 1);
by (strip_tac 1);
by (Seq_case_simp_tac "xa" 1);
by (pair_tac "a" 1);
@@ -208,8 +208,8 @@
(* second prefix notion for Finite x *)
-goal thy "! y s.is_execution_fragment A (s,x@@y) --> is_execution_fragment A (s,x)";
-by (pair_induct_tac "x" [is_execution_fragment_def] 1);
+goal thy "! y s.is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
+by (pair_induct_tac "x" [is_exec_frag_def] 1);
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Jun 12 16:47:15 1997 +0200
@@ -19,8 +19,9 @@
consts
(* Executions *)
- is_ex_fr ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)"
- is_execution_fragment,
+
+ is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
+ is_exec_frag,
has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
executions :: "('a,'s)ioa => ('a,'s)execution set"
@@ -50,20 +51,23 @@
(* ------------------- Executions ------------------------------ *)
-is_execution_fragment_def
- "is_execution_fragment A ex == ((is_ex_fr A`(snd ex)) (fst ex) ~= FF)"
+is_exec_frag_def
+ "is_exec_frag A ex == ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)"
-is_ex_fr_def
- "is_ex_fr A ==(fix`(LAM h ex. (%s. case ex of
+
+is_exec_fragC_def
+ "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of
nil => TT
| x##xs => (flift1
(%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p))
`x)
)))"
-
+
+
+
executions_def
"executions ioa == {e. ((fst e) : starts_of(ioa)) &
- is_execution_fragment ioa e}"
+ is_exec_frag ioa e}"
(* ------------------- Schedules ------------------------------ *)