diff -r 6b38551d0798 -r f65265d71426 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat May 27 21:18:51 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun May 28 19:54:20 2006 +0200
@@ -57,6 +57,45 @@
             (! exec : executions (fst CL). (exec |== (snd CL)) -->
                                            ((corresp_ex (fst AM) f exec) |== (snd AM)))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+declare split_paired_Ex [simp del]
+
+lemma live_implements_trans: 
+"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]  
+      ==> live_implements (A,LA) (C,LC)"
+apply (unfold live_implements_def)
+apply auto
+done
+
+
+subsection "Correctness of live refmap"
+	
+lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);  
+                   is_live_ref_map f (C,M) (A,L) |]  
+                ==> live_implements (C,M) (A,L)"
+apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
+apply (tactic "safe_tac set_cs")
+apply (rule_tac x = "corresp_ex A f ex" in exI)
+apply (tactic "safe_tac set_cs")
+  (* Traces coincide, Lemma 1 *)
+  apply (tactic {* pair_tac "ex" 1 *})
+  apply (erule lemma_1 [THEN spec, THEN mp])
+  apply (simp (no_asm) add: externals_def)
+  apply (auto)[1]
+  apply (simp add: executions_def reachable.reachable_0)
+ 
+  (* corresp_ex is execution, Lemma 2 *)
+  apply (tactic {* pair_tac "ex" 1 *})
+  apply (simp add: executions_def)
+  (* start state *) 
+  apply (rule conjI)
+  apply (simp add: is_ref_map_def corresp_ex_def)
+  (* is-execution-fragment *)
+  apply (erule lemma_2 [THEN spec, THEN mp])
+  apply (simp add: reachable.reachable_0)
+
+ (* Liveness *)
+apply auto
+done
 
 end