--- a/CpsG.thy~	Thu Jan 28 13:46:45 2016 +0000
+++ b/CpsG.thy~	Thu Jan 28 14:26:10 2016 +0000
@@ -2707,6 +2707,57 @@
 end
 
 
+lemma Max_UNION: 
+  assumes "finite A"
+  and "A \<noteq> {}"
+  and "\<forall> M \<in> f ` A. finite M"
+  and "\<forall> M \<in> f ` A. M \<noteq> {}"
+  shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
+  using assms[simp]
+proof -
+  have "?L = Max (\<Union>(f ` A))"
+    by (fold Union_image_eq, simp)
+  also have "... = ?R"
+    by (subst Max_Union, simp+)
+  finally show ?thesis .
+qed
+
+lemma max_Max_eq:
+  assumes "finite A"
+    and "A \<noteq> {}"
+    and "x = y"
+  shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
+proof -
+  have "?R = Max (insert y A)" by simp
+  also from assms have "... = ?L"
+      by (subst Max.insert, simp+)
+  finally show ?thesis by simp
+qed
+
+lemma birth_time_lt:  
+  assumes "s \<noteq> []"
+  shows "last_set th s < length s"
+  using assms
+proof(induct s)
+  case (Cons a s)
+  show ?case
+  proof(cases "s \<noteq> []")
+    case False
+    thus ?thesis
+      by (cases a, auto)
+  next
+    case True
+    show ?thesis using Cons(1)[OF True]
+      by (cases a, auto)
+  qed
+qed simp
+
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+  by (induct s, auto)
+
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+  by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
+
 lemma eq_RAG: 
   "RAG (wq s) = RAG s"
 by (unfold cs_RAG_def s_RAG_def, auto)
@@ -3849,6 +3900,44 @@
     by (unfold cs_holding_def, auto)
 qed
 
+lemma tRAG_alt_def: 
+  "tRAG s = {(Th th1, Th th2) | th1 th2. 
+                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
+ by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
+
+sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"
+proof -
+  have "fsubtree (tRAG s)"
+  proof -
+    have "fbranch (tRAG s)"
+    proof(unfold tRAG_def, rule fbranch_compose)
+        show "fbranch (wRAG s)"
+        proof(rule finite_fbranchI)
+           from finite_RAG show "finite (wRAG s)"
+           by (unfold RAG_split, auto)
+        qed
+    next
+        show "fbranch (hRAG s)"
+        proof(rule finite_fbranchI)
+           from finite_RAG 
+           show "finite (hRAG s)" by (unfold RAG_split, auto)
+        qed
+    qed
+    moreover have "wf (tRAG s)"
+    proof(rule wf_subset)
+      show "wf (RAG s O RAG s)" using wf_RAG
+        by (fold wf_comp_self, simp)
+    next
+      show "tRAG s \<subseteq> (RAG s O RAG s)"
+        by (unfold tRAG_alt_def, auto)
+    qed
+    ultimately show ?thesis
+      by (unfold fsubtree_def fsubtree_axioms_def,auto)
+  qed
+  from this[folded tRAG_def] show "fsubtree (tRAG s)" .
+qed
+
+
 context valid_trace
 begin