# HG changeset patch
# User mueller
# Date 866126835 -7200
# Node ID 2de17c994071f348f8da22caa70cf66f98f6ba82
# Parent  04412cfe6861e00130a119e4118c7e8411eaaf50
added deadlock freedom, polished definitions and proofs

diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Asig.ML
--- 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";
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Asig.thy
--- 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) = {})    & 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Automata.ML
--- 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";
+
+
 
 (* ---------------------------------------------------------------------------------- *)
 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Automata.thy
--- 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 ==                                                   
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- 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;
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- 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 @ 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- 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 &\
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- 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)";
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- /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";
+
+
+
+
+
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Deadlock.thy
--- /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
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- 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);
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- 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) )))"
  
 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- 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";
 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- 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 ==                          
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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";
+
+
 (* ----------------------------------------------------------------------------------- *)
 
 
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- 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;
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Traces.ML
--- 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);
diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Traces.thy
--- 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 ------------------------------ *)